Skip to content

Instantly share code, notes, and snippets.

@dvanhorn

dvanhorn/progress.txt

Created November 20, 2012 00:55
Show Gist options
  • Save dvanhorn/4115243 to your computer and use it in GitHub Desktop.
Save dvanhorn/4115243 to your computer and use it in GitHub Desktop.
Download ZIP
Progress on running F* on mono
Raw
progress.txt
Progress:
* mono fstar.exe prints usage and then crashes
* mono fstar.exe of a trivial program crashes
$ mono fstar.exe
fstar [option] infile...
--help Display this information
--verbosity v
--z3log Dump a detailed Z3 debugging log to z3.log
--z3exe Call z3.exe instead of via the .NET API (implies --logQueries)
--dtencoding Use the new datatype encoding with Z3
--sep_qops Defer quantified assumptions when generating Z3 models
--f7
--f7backend
--trace v
--fstar_home dir Set the FSTAR_HOME variable to dir
--profile
--silent
--prims file
--prooflibvals file
--prn Print real names---you may want to use this in conjunction with logQueries
--dump_module module name
--dump_src
--dump_tgt
--z3timeout t Set the Z3 soft timeout to t milliseconds
--logQueries Log the Z3 queries in $FSTAR_HOME/bin/queries/, or in odir, if set; also see --prn
--gadt
--trace_err
--js dir
--cert
--print_certs
--debug_cert
--cert_dir dir
--dcil_logicfun
--UNSAFE
--hashcons_poly
--monadic
--addGK Use Gatekeeper
--describe_queries Print the queried formula and its location
--UNSAFE_skip_first_queries n Skip the first n queries
--restore
--parallel Use multiple threads when calling Z3
--rrf Relational mode (RRF)
--writecache Write a cached prelude
--readcache Read the cached prelude
--rc Read the cached prelude
--cachefile file Location of binary cache of prelude
--z3encode_binders Encode type-level binders in Z3 terms
--dotnet_warnings Warn about .NET compilation limitations
--relax_order Allow out-of-order let/val
--skip_translation
--to_dcil
--rdcil
--rdcil_z3eq
--genIL
--writePrims
--o file
--odir dir Place output in directory dir
--pickle
--pretty_attribs
--keyfile file
--profile_attribs
--dotnet4
--emulateContexts
--UNSAFE_skip_target_checker Do not typecheck the generated code
--partially-trusted-callers
* Assertion at mini-codegen.c:1186, condition `reginfo [sreg].born_in > 0' not met
Stacktrace:
at <Module>.<CrtImplementationDetails>.LanguageSupport.{ctor} (<CrtImplementationDetails>.LanguageSupport*) <0x00011>
at <Module>..cctor () <0x0001f>
at (wrapper runtime-invoke) object.runtime_invoke_void (object,intptr,intptr,intptr) <0xffffffff>
at Microsoft.FStar.Z3Encoding.Term.mkZ3 () <0x0004d>
at <StartupCode$z3encode>.$Microsoft.FStar.Z3Encoding.Term..cctor () <0x00189>
at (wrapper runtime-invoke) object.runtime_invoke_void (object,intptr,intptr,intptr) <0xffffffff>
at Microsoft.FStar.Z3Encoding.Term.cleanup () <0x0000d>
at Microsoft.FStar.Wrapper.cleanup () <0x00015>
at <StartupCode$fstar>.$Microsoft.FStar.Wrapper.main@ () <0x0004b>
at (wrapper runtime-invoke) object.runtime_invoke_void (object,intptr,intptr,intptr) <0xffffffff>
Native stacktrace:
0 mono 0x000b7009 mono + 745481
1 libsystem_c.dylib 0x90ce486b _sigtramp + 43
2 ??? 0xffffffff 0x0 + 4294967295
3 libsystem_c.dylib 0x90d30508 abort + 168
4 mono 0x0024ee62 mono + 2416226
5 mono 0x0024eec4 mono + 2416324
6 mono 0x000b3dbd mono + 732605
7 mono 0x00008e0c mono + 32268
8 mono 0x0000ed80 mono + 56704
9 mono 0x000107c6 mono + 63430
10 mono 0x000113da mono + 66522
11 mono 0x001b81bd mono + 1798589
12 mono 0x000bb4dc mono + 763100
13 ??? 0x0035c066 0x0 + 3522662
14 ??? 0x017f5678 0x0 + 25122424
15 ??? 0x003e303b 0x0 + 4075579
16 mono 0x000114e4 mono + 66788
17 mono 0x001bcca6 mono + 1817766
18 mono 0x001b77e0 mono + 1796064
19 mono 0x001b71d2 mono + 1794514
20 mono 0x00010b9f mono + 64415
21 mono 0x000113da mono + 66522
22 mono 0x001b81bd mono + 1798589
23 mono 0x000bb4dc mono + 763100
24 ??? 0x0035c066 0x0 + 3522662
25 ??? 0x017f1f22 0x0 + 25108258
26 ??? 0x003e303b 0x0 + 4075579
27 mono 0x000114e4 mono + 66788
28 mono 0x001bcca6 mono + 1817766
29 mono 0x001b77e0 mono + 1796064
30 mono 0x001b70ef mono + 1794287
31 mono 0x000ba1dc mono + 758236
32 ??? 0x0035c264 0x0 + 3523172
33 ??? 0x017ad166 0x0 + 24826214
34 ??? 0x003e2df4 0x0 + 4074996
35 ??? 0x003e3064 0x0 + 4075620
36 mono 0x000114e4 mono + 66788
37 mono 0x001bcca6 mono + 1817766
38 mono 0x001bf2a1 mono + 1827489
39 mono 0x001be68b mono + 1824395
40 mono 0x00088662 mono + 554594
41 mono 0x00003ca6 mono + 11430
Debug info from gdb:
/tmp/mono-gdb-commands.cpOiUD:1: Error in sourced command file:
unable to debug self
=================================================================
Got a SIGABRT while executing native code. This usually indicates
a fatal error in the mono runtime or one of the native libraries
used by your application.
=================================================================
Abort trap: 6
$ cat Hello.fst
module Hello
let pass = assert (1=1)
$ mono fstar.exe Hello.fst
* Assertion at mini-codegen.c:1186, condition `reginfo [sreg].born_in > 0' not met
Stacktrace:
at <Module>.<CrtImplementationDetails>.LanguageSupport.{ctor} (<CrtImplementationDetails>.LanguageSupport*) <0x00011>
at <Module>..cctor () <0x0001f>
at (wrapper runtime-invoke) object.runtime_invoke_void (object,intptr,intptr,intptr) <0xffffffff>
at Microsoft.FStar.ProofState.new_z3 () <0x00065>
at Microsoft.FStar.ProofState.init () <0x0000d>
at Microsoft.FStar.FStar.do_main<a> (a) <0x002b1>
at <StartupCode$fstar>.$Microsoft.FStar.Wrapper.main@ () <0x00033>
at (wrapper runtime-invoke) object.runtime_invoke_void (object,intptr,intptr,intptr) <0xffffffff>
Native stacktrace:
0 mono 0x000b7009 mono + 745481
1 libsystem_c.dylib 0x90ce486b _sigtramp + 43
2 ??? 0xffffffff 0x0 + 4294967295
3 libsystem_c.dylib 0x90d30508 abort + 168
4 mono 0x0024ee62 mono + 2416226
5 mono 0x0024eec4 mono + 2416324
6 mono 0x000b3dbd mono + 732605
7 mono 0x00008e0c mono + 32268
8 mono 0x0000ed80 mono + 56704
9 mono 0x000107c6 mono + 63430
10 mono 0x000113da mono + 66522
11 mono 0x001b81bd mono + 1798589
12 mono 0x000bb4dc mono + 763100
13 ??? 0x0035c066 0x0 + 3522662
14 ??? 0x017a44e0 0x0 + 24790240
15 ??? 0x003e303b 0x0 + 4075579
16 mono 0x000114e4 mono + 66788
17 mono 0x001bcca6 mono + 1817766
18 mono 0x001b77e0 mono + 1796064
19 mono 0x001b71d2 mono + 1794514
20 mono 0x00010b9f mono + 64415
21 mono 0x000113da mono + 66522
22 mono 0x001b81bd mono + 1798589
23 mono 0x000bb4dc mono + 763100
24 ??? 0x0035c066 0x0 + 3522662
25 ??? 0x017a368e 0x0 + 24786574
26 ??? 0x003e3332 0x0 + 4076338
27 ??? 0x003e2ddc 0x0 + 4074972
28 ??? 0x003e3064 0x0 + 4075620
29 mono 0x000114e4 mono + 66788
30 mono 0x001bcca6 mono + 1817766
31 mono 0x001bf2a1 mono + 1827489
32 mono 0x001be68b mono + 1824395
33 mono 0x00088662 mono + 554594
34 mono 0x00003ca6 mono + 11430
35 ??? 0x00000003 0x0 + 3
Debug info from gdb:
/tmp/mono-gdb-commands.ejfZcv:1: Error in sourced command file:
unable to debug self
=================================================================
Got a SIGABRT while executing native code. This usually indicates
a fatal error in the mono runtime or one of the native libraries
used by your application.
=================================================================
Abort trap: 6
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment