search

FStarLang / karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code
Apache License 2.0
395 stars 59 forks source link

WasmSupport.c:21: undefined reference to `WasmSupport_trap' #174

Open conradlz opened 4 years ago

conradlz commented 4 years ago

I'm using Ubuntu linux with a recent FStar and kreMLin from master. When attempting to run: krml -verbose Introduction.fst -no-prefix Introduction -o test.exe && ./test.exe Where Introduction is the example from the kreMLin tutorial. I get this long error:


⚙ KreMLin auto-detecting tools. Here's what we found:
readlink is: readlink
KreMLin called via: krml
KreMLin home is: /home/corn/Documents/webclones/kremlin
⚙ KreMLin will drive F*. Here's what we found:
read FSTAR_HOME via the environment
fstar is on branch master
fstar is: /home/corn/Documents/webclones/fstar/bin/fstar.exe /home/corn/Documents/webclones/kremlin/runtime/WasmSupport.fst /home/corn/Documents/webclones/fstar/ulib/FStar.UInt128.fst --trace_error --cache_checked_modules --expose_interfaces --include /home/corn/Documents/webclones/kremlin/kremlib --include /home/corn/Documents/webclones/kremlin/include
⚡ Calling F* (use -verbose to see the output)
/home/corn/Documents/webclones/fstar/bin/fstar.exe --odir . --codegen Kremlin --lax /home/corn/Documents/webclones/kremlin/runtime/WasmSupport.fst /home/corn/Documents/webclones/fstar/ulib/FStar.UInt128.fst --trace_error --cache_checked_modules --expose_interfaces --include /home/corn/Documents/webclones/kremlin/kremlib --include /home/corn/Documents/webclones/kremlin/include Introduction.fst
✔ [F*,extract]
Extracted module FStar.Pervasives.Native
Extracted module FStar.Pervasives
Extracted module FStar.Mul
Extracted module FStar.Preorder
Extracted module FStar.Calc
Extracted module FStar.Classical
Extracted module FStar.StrongExcludedMiddle
Extracted module FStar.FunctionalExtensionality
Extracted module FStar.List.Tot.Base
Extracted module FStar.List.Tot.Properties
Extracted module FStar.List.Tot
Extracted module FStar.Seq.Base
Extracted module FStar.Squash
Extracted module FStar.Seq.Properties
Extracted module FStar.Seq
Extracted module FStar.Math.Lib
Extracted module FStar.Math.Lemmas
Extracted module FStar.BitVector
Extracted module FStar.UInt
Extracted module FStar.UInt32
Extracted module FStar.UInt64
Extracted module FStar.Int
Extracted module FStar.Int64
Extracted module FStar.Int63
Extracted module FStar.Int32
Extracted module FStar.Int16
Extracted module FStar.Int8
Extracted module FStar.UInt63
Extracted module FStar.UInt16
Extracted module FStar.UInt8
Extracted module FStar.Int.Cast
Extracted module FStar.Set
Extracted module FStar.PropositionalExtensionality
Extracted module FStar.PredicateExtensionality
Extracted module FStar.TSet
Extracted module FStar.Monotonic.Heap
Extracted module FStar.Heap
Extracted module FStar.Map
Extracted module FStar.Monotonic.Witnessed
Extracted module FStar.Ghost
Extracted module FStar.Monotonic.HyperHeap
Extracted module FStar.Monotonic.HyperStack
Extracted module FStar.HyperStack
Extracted module FStar.HyperStack.ST
Extracted module WasmSupport
Extracted module FStar.UInt128
Extracted module FStar.ModifiesGen
Extracted module FStar.BigOps
Extracted module LowStar.Monotonic.Buffer
Extracted module LowStar.Buffer
Extracted module C
Extracted module Spec.Loops
Extracted module LowStar.BufferOps
Extracted module C.Loops
Extracted module LowStar.Modifies
Extracted module Introduction
Attempting to translate module FStar.Pervasives.Native
Attempting to translate module FStar.Pervasives
Attempting to translate module FStar.Mul
Attempting to translate module FStar.Preorder
Attempting to translate module FStar.Calc
Attempting to translate module FStar.Classical
Attempting to translate module FStar.StrongExcludedMiddle
Attempting to translate module FStar.FunctionalExtensionality
Attempting to translate module FStar.List.Tot.Base
Attempting to translate module FStar.List.Tot.Properties
Attempting to translate module FStar.List.Tot
Attempting to translate module FStar.Seq.Base
Attempting to translate module FStar.Squash
Attempting to translate module FStar.Seq.Properties
Attempting to translate module FStar.Seq
Attempting to translate module FStar.Math.Lib
Attempting to translate module FStar.Math.Lemmas
Attempting to translate module FStar.BitVector
Attempting to translate module FStar.UInt
Attempting to translate module FStar.UInt32
Attempting to translate module FStar.UInt64
Attempting to translate module FStar.Int
Attempting to translate module FStar.Int64
Attempting to translate module FStar.Int63
Attempting to translate module FStar.Int32
Attempting to translate module FStar.Int16
Attempting to translate module FStar.Int8
Attempting to translate module FStar.UInt63
Attempting to translate module FStar.UInt16
Attempting to translate module FStar.UInt8
Attempting to translate module FStar.Int.Cast
Attempting to translate module FStar.Set
Attempting to translate module FStar.PropositionalExtensionality
Attempting to translate module FStar.PredicateExtensionality
Attempting to translate module FStar.TSet
Attempting to translate module FStar.Monotonic.Heap
Attempting to translate module FStar.Heap
Attempting to translate module FStar.Map
Attempting to translate module FStar.Monotonic.Witnessed
Attempting to translate module FStar.Ghost
Attempting to translate module FStar.Monotonic.HyperHeap
Attempting to translate module FStar.Monotonic.HyperStack
Attempting to translate module FStar.HyperStack
Attempting to translate module FStar.HyperStack.ST
Attempting to translate module WasmSupport
Attempting to translate module FStar.UInt128
Attempting to translate module FStar.ModifiesGen
Attempting to translate module FStar.BigOps
Attempting to translate module LowStar.Monotonic.Buffer
Attempting to translate module LowStar.Buffer
Attempting to translate module C
Attempting to translate module Spec.Loops
Attempting to translate module LowStar.BufferOps
Attempting to translate module C.Loops
Attempting to translate module LowStar.Modifies
Attempting to translate module Introduction
All verification conditions discharged successfully

Introduction.fst(0,0-0,0): (Warning 241) Unable to load Introduction.fst.checked.lax since checked file Introduction.fst.checked.lax does not exist; will recheck Introduction.fst (suppressing this warning for further modules)
Not extracting FStar.FunctionalExtensionality.on_domain to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.Set.set to KreMLin (assumed type)
Not extracting type definition FStar.Set.equal to KreMLin (assumed type)
Not extracting FStar.Set.mem to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Set.empty to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Set.singleton to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Set.union to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Set.intersect to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Set.complement to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.Monotonic.Heap.heap to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.Heap.equal to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.Heap.mref to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.Heap.contains to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.Heap.addr_unused_in to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.Heap.unused_in to KreMLin (assumed type)
Not extracting FStar.Monotonic.Heap.sel_tot to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Monotonic.Heap.upd_tot to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Monotonic.Heap.alloc to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Monotonic.Heap.free_mm to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.Monotonic.Heap.aref to KreMLin (assumed type)
Not extracting FStar.Monotonic.Heap.aref_of to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.Monotonic.Heap.aref_unused_in to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.Heap.aref_live_at to KreMLin (assumed type)
Not extracting type definition FStar.Map.t to KreMLin (assumed type)
Not extracting FStar.Map.sel to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Map.upd to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Map.const to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Map.domain to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Map.contains to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Map.concat to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Map.map_val to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.Map.restrict to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.Map.equal to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.Witnessed.witnessed to KreMLin (assumed type)
Not extracting type definition FStar.Ghost.erased to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.HyperHeap.rid to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.HyperStack.map_invariant to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.HyperStack.downward_closed to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.HyperStack.tip_top to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.HyperStack.rid_ctr_pred to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.HyperStack.mem' to KreMLin (assumed type)
Not extracting FStar.Monotonic.HyperStack.as_ref to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.Monotonic.HyperStack.aref to KreMLin (assumed type)
Not extracting FStar.Monotonic.HyperStack.aref_of to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.Monotonic.HyperStack.aref_unused_in to KreMLin (assumed type)
Not extracting type definition FStar.Monotonic.HyperStack.aref_live_at to KreMLin (assumed type)
Not extracting type definition FStar.HyperStack.ST.mem_rel to KreMLin (assumed type)
Not extracting type definition FStar.HyperStack.ST.region_contains_pred to KreMLin (assumed type)
Not extracting type definition FStar.HyperStack.ST.ref_contains_pred to KreMLin (assumed type)
Not extracting type definition FStar.HyperStack.ST.stable to KreMLin (assumed type)
Not extracting type definition FStar.HyperStack.ST.witnessed to KreMLin (assumed type)
Not extracting FStar.HyperStack.ST.gst_witness to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.gst_recall to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.HyperStack.ST.same_refs_in_all_regions to KreMLin (assumed type)
Not extracting type definition FStar.HyperStack.ST.same_refs_in_stack_regions to KreMLin (assumed type)
Not extracting type definition FStar.HyperStack.ST.same_refs_in_non_tip_regions to KreMLin (assumed type)
Not extracting type definition FStar.HyperStack.ST.same_refs_in_non_tip_stack_regions to KreMLin (assumed type)
Not extracting FStar.HyperStack.ST.salloc to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.salloc_mm to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.sfree to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.ralloc to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.ralloc_mm to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.rfree to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.op_Colon_Equals to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.op_Bang to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.recall to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.witness_hsref to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.testify to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.testify_forall to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.testify_forall_region_contains_pred to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.HyperStack.ST.token_p to KreMLin (assumed type)
Not extracting FStar.HyperStack.ST.witness_p to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.recall_p to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.HyperStack.ST.drgn to KreMLin (assumed type)
Not extracting FStar.HyperStack.ST.ralloc_drgn to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.HyperStack.ST.ralloc_drgn_mm to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.ModifiesGen.loc to KreMLin (assumed type)
Not extracting FStar.ModifiesGen.loc_none to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.ModifiesGen.loc_includes to KreMLin (assumed type)
Not extracting type definition FStar.ModifiesGen.loc_disjoint to KreMLin (assumed type)
Not extracting FStar.ModifiesGen.address_liveness_insensitive_locs to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.ModifiesGen.region_liveness_insensitive_locs to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.ModifiesGen.modifies to KreMLin (assumed type)
Not extracting type definition FStar.ModifiesGen.does_not_contain_addr to KreMLin (assumed type)
Not extracting type definition FStar.ModifiesGen.aloc_union to KreMLin (assumed type)
Not extracting FStar.ModifiesGen.cls_union to KreMLin (polymorphic assumes are not supported)
Not extracting type definition FStar.ModifiesGen.raise_aloc to KreMLin (assumed type)
Not extracting FStar.ModifiesGen.raise_cls to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.ModifiesGen.raise_loc to KreMLin (polymorphic assumes are not supported)
Not extracting FStar.ModifiesGen.lower_loc to KreMLin (polymorphic assumes are not supported)
Not extracting type definition LowStar.Monotonic.Buffer.mbuffer to KreMLin (assumed type)
Not extracting LowStar.Monotonic.Buffer.mnull to KreMLin (polymorphic assumes are not supported)
Not extracting type definition LowStar.Monotonic.Buffer.unused_in to KreMLin (assumed type)
Not extracting type definition LowStar.Monotonic.Buffer.live to KreMLin (assumed type)
Not extracting type definition LowStar.Monotonic.Buffer.loc to KreMLin (assumed type)
Not extracting type definition LowStar.Monotonic.Buffer.loc_includes to KreMLin (assumed type)
Not extracting type definition LowStar.Monotonic.Buffer.loc_disjoint to KreMLin (assumed type)
Not extracting type definition LowStar.Monotonic.Buffer.modifies to KreMLin (assumed type)
Not extracting type definition LowStar.Monotonic.Buffer.does_not_contain_addr to KreMLin (assumed type)
Not extracting LowStar.Monotonic.Buffer.is_null to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.msub to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.moffset to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.index to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.upd' to KreMLin (polymorphic assumes are not supported)
Not extracting type definition LowStar.Monotonic.Buffer.recallable to KreMLin (assumed type)
Not extracting type definition LowStar.Monotonic.Buffer.region_lifetime_buf to KreMLin (assumed type)
Not extracting LowStar.Monotonic.Buffer.recall to KreMLin (polymorphic assumes are not supported)
Not extracting type definition LowStar.Monotonic.Buffer.witnessed to KreMLin (assumed type)
Not extracting LowStar.Monotonic.Buffer.witness_p to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.recall_p to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.witnessed_functorial_st to KreMLin (polymorphic assumes are not supported)
Not extracting type definition LowStar.Monotonic.Buffer.freeable to KreMLin (assumed type)
Not extracting LowStar.Monotonic.Buffer.free to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.mgcmalloc to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.mgcmalloc_and_blit to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.mmalloc to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.mmalloc_and_blit to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.malloca to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.malloca_and_blit to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.malloca_of_list to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.mgcmalloc_of_list to KreMLin (polymorphic assumes are not supported)
(Warning 250) Error while extracting LowStar.Monotonic.Buffer.mgcmalloc_of_list_partial to KreMLin (Failure("Argument of FStar.Buffer.createL is not a list literal!"))

Not extracting LowStar.Monotonic.Buffer.mmalloc_drgn to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.mmalloc_drgn_mm to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.mmalloc_drgn_and_blit to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.blit to KreMLin (polymorphic assumes are not supported)
Not extracting LowStar.Monotonic.Buffer.fill to KreMLin (polymorphic assumes are not supported)
Not extracting type definition LowStar.Monotonic.Buffer.abuffer' to KreMLin (assumed type)
Not extracting type definition C.channel to KreMLin (assumed type)
Not extracting type definition C.char to KreMLin (assumed type)
Not extracting type definition C.int to KreMLin (assumed type)
Not extracting type definition C.clock_t to KreMLin (assumed type)

✔ [F*] ⏱️ 1s and 188ms
✔ [Monomorphization] ⏱️ 16ms
✔ [Inlining] ⏱️ 3ms
✔ [Pattern matches compilation] ⏱️ 3ms
✔ [Structs + Simplify 2] ⏱️ 4ms
✔ [Drop] ⏱️ 3ms
✔ [AstToCStar] ⏱️ <1ms
✔ [CStarToC] ⏱️ <1ms
✔ [PrettyPrinting] ⏱️ <1ms
KreMLin: wrote out .c files for WasmSupport, C, Introduction
KreMLin: wrote out .h files for WasmSupport, C, Introduction
⚙ KreMLin will drive the C compiler. Here's what we found:
gcc is: gcc-8
gcc-8 options are: -I /home/corn/Documents/webclones/kremlin/kremlib/dist/minimal -I /home/corn/Documents/webclones/kremlin/kremlib -I /home/corn/Documents/webclones/kremlin/include -I . -Wall -Werror -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11
⚡ Generating object files
gcc-8 -I /home/corn/Documents/webclones/kremlin/kremlib/dist/minimal -I /home/corn/Documents/webclones/kremlin/kremlib -I /home/corn/Documents/webclones/kremlin/include -I . -Wall -Werror -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11 -c ./WasmSupport.c -o ./WasmSupport.o
✔ [CC,./WasmSupport.c]
gcc-8 -I /home/corn/Documents/webclones/kremlin/kremlib/dist/minimal -I /home/corn/Documents/webclones/kremlin/kremlib -I /home/corn/Documents/webclones/kremlin/include -I . -Wall -Werror -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11 -c ./C.c -o ./C.o
✔ [CC,./C.c]
gcc-8 -I /home/corn/Documents/webclones/kremlin/kremlib/dist/minimal -I /home/corn/Documents/webclones/kremlin/kremlib -I /home/corn/Documents/webclones/kremlin/include -I . -Wall -Werror -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11 -c ./Introduction.c -o ./Introduction.o
✔ [CC,./Introduction.c]
gcc-8 -I /home/corn/Documents/webclones/kremlin/kremlib/dist/minimal -I /home/corn/Documents/webclones/kremlin/kremlib -I /home/corn/Documents/webclones/kremlin/include -I . -Wall -Werror -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11 ./WasmSupport.o ./C.o ./Introduction.o /home/corn/Documents/webclones/kremlin/kremlib/dist/generic/libkremlib.a -o test.exe
✘ [LD]
/usr/bin/ld: ./WasmSupport.o: in function `WasmSupport_check_buffer_size':
/home/corn/Documents/webclones/transaction-verifier/Introduction/./WasmSupport.c:21: undefined reference to `WasmSupport_trap'
collect2: error: ld returned 1 exit status

Warning 3: run_or_warn: the following command failed:
gcc-8 -I /home/corn/Documents/webclones/kremlin/kremlib/dist/minimal -I /home/corn/Documents/webclones/kremlin/kremlib -I /home/corn/Documents/webclones/kremlin/include -I . -Wall -Werror -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11 ./WasmSupport.o ./C.o ./Introduction.o /home/corn/Documents/webclones/kremlin/kremlib/dist/generic/libkremlib.a -o test.exe
Warning 3 is fatal, exiting.```
msprotz commented 4 years ago

try passing -bundle WasmSupport... I'm in the process of rewriting the tutorial to explain how to properly build a project without using kremlin as a compiler driver

thanks for reminding me of this!

conradlz commented 4 years ago

@msprotz Oh wow thank you so much that worked!

conradlz commented 4 years ago

I'll leave this open so you can close it when some documentation is updated