search

FStarLang / karamel

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

Fatal error: exception Failure("[mk_expr m]: op should've been caught") #445

Open mtzguido opened 1 month ago

mtzguido commented 1 month ago

I was trying to write a test with a higher-order function (it won't work of course, I later realized), but it triggered a crash, so posting here

module Op

module U32 = FStar.UInt32

// Type annotations only due to add being partially defined and F* otherwise inferring a Tot.
let ap2
  (f : (x:U32.t -> y:U32.t ->
         Pure U32.t (requires UInt.size (U32.v x + U32.v y) 32)
                    (ensures fun c -> U32.v c = U32.v x + U32.v y)))
  x y :
         Pure U32.t (requires UInt.size (U32.v x + U32.v y) 32)
                    (ensures fun c -> U32.v c = U32.v x + U32.v y)
   = f x y

let main () =
  let c : UInt32.t = ap2 FStar.UInt32.add 4ul 2ul in
  if FStar.Int.Cast.uint32_to_int32 c = 6l
  then 0l
  else 1l

Removing the ap2 makes it work. I guess failing here is fine, just maybe with a more benign error.

msprotz commented 1 month ago

Can you post the crash details?

mtzguido commented 1 month ago 
../_build/default/src/Karamel.exe  -warn-error @4 -verbose -skip-makefiles  -tmpdir .output/Op.out -no-prefix Op \
  -o .output/Op.exe .output/FStar_Pervasives_Native.krml .output/FStar_Pervasives.krml .output/FStar_Float.krml .output/FStar_Mul.krml .output/FStar_Squash.krml .output/FStar_Classical.krml .output/FStar_Preorder.krml .output/FStar_Sealed.krml .output/FStar_Range.krml .output/FStar_Calc.krml .output/FStar_StrongExcludedMiddle.krml .output/FStar_Classical_Sugar.krml .output/FStar_List_Tot_Base.krml .output/FStar_List_Tot_Properties.krml .output/FStar_List_Tot.krml .output/FStar_Seq_Base.krml .output/FStar_Seq_Properties.krml .output/FStar_Seq.krml .output/FStar_Math_Lib.krml .output/FStar_Math_Lemmas.krml .output/FStar_BitVector.krml .output/FStar_UInt.krml .output/FStar_UInt32.krml .output/FStar_Char.krml .output/FStar_Pprint.krml .output/FStar_Issue.krml .output/FStar_TypeChecker_Core.krml .output/FStar_Errors_Msg.krml .output/FStar_Tactics_Common.krml .output/FStar_Reflection_Types.krml .output/FStar_Tactics_Types.krml .output/FStar_Tactics_Result.krml .output/FStar_Monotonic_Pure.krml .output/FStar_Tactics_Effect.krml .output/FStar_Tactics_Unseal.krml .output/FStar_Ghost.krml .output/FStar_Sealed_Inhabited.krml .output/FStar_Syntax_Syntax.krml .output/FStar_Reflection_V2_Data.krml .output/FStar_VConfig.krml .output/FStar_Order.krml .output/FStar_Reflection_V2_Builtins.krml .output/FStar_Reflection_Const.krml .output/FStar_Tactics_V2_Builtins.krml .output/FStar_FunctionalExtensionality.krml .output/FStar_Set.krml .output/FStar_ErasedLogic.krml .output/FStar_PropositionalExtensionality.krml .output/FStar_PredicateExtensionality.krml .output/FStar_TSet.krml .output/FStar_Monotonic_Heap.krml .output/FStar_Heap.krml .output/FStar_Map.krml .output/FStar_Monotonic_Witnessed.krml .output/FStar_Monotonic_HyperHeap.krml .output/FStar_Monotonic_HyperStack.krml .output/FStar_HyperStack.krml .output/FStar_HyperStack_ST.krml .output/FStar_Universe.krml .output/FStar_Tactics_SMT.krml .output/FStar_GSet.krml .output/FStar_ModifiesGen.krml .output/FStar_Tactics_Util.krml .output/FStar_Reflection_V2_TermEq.krml .output/FStar_Reflection_V2_Derived.krml .output/FStar_Reflection_V2_Derived_Lemmas.krml .output/FStar_Reflection_V2_Compare.krml .output/FStar_Reflection_V2.krml .output/FStar_Tactics_NamedView.krml .output/FStar_Reflection_V1_Data.krml .output/FStar_Reflection_V1_Builtins.krml .output/FStar_Tactics_V1_Builtins.krml .output/FStar_Tactics_Builtins.krml .output/FStar_Tactics_V2_SyntaxCoercions.krml .output/FStar_Tactics_Visit.krml .output/FStar_Tactics_V2_SyntaxHelpers.krml .output/FStar_Reflection_V2_Formula.krml .output/FStar_Tactics_V2_Derived.krml .output/FStar_Tactics_Typeclasses.krml .output/FStar_Tactics_MApply.krml .output/FStar_Tactics_Print.krml .output/FStar_IndefiniteDescription.krml .output/FStar_Tactics_V2_Logic.krml .output/FStar_Tactics_V2.krml .output/FStar_BigOps.krml .output/LowStar_Monotonic_Buffer.krml .output/LowStar_Buffer.krml .output/FStar_Int.krml .output/FStar_Int32.krml .output/FStar_UInt8.krml .output/C.krml .output/FStar_HyperStack_All.krml .output/Shift.krml .output/Rust2.krml .output/CheckedInt.krml .output/FStar_HyperStack_IO.krml .output/LowStar_Modifies.krml .output/FStar_Exn.krml .output/FStar_ST.krml .output/FStar_All.krml .output/FStar_List.krml .output/FStar_String.krml .output/FStar_UInt64.krml .output/FStar_UInt16.krml .output/FStar_Bytes.krml .output/TestKrmlBytes.krml .output/Rust3.krml .output/FStar_Int64.krml .output/FStar_Int128.krml .output/FStar_Int16.krml .output/FStar_Int8.krml .output/FStar_Int_Cast.krml .output/FStar_BV.krml .output/FStar_Reflection_V2_Arith.krml .output/FStar_Tactics_BV.krml .output/FStar_UInt128.krml .output/FStar_Integers.krml .output/C_String.krml .output/Wasm10.krml .output/FStar_Buffer.krml .output/TestLib.krml .output/Hoisting.krml .output/PolyComp.krml .output/Underspec.krml .output/FStar_Int_Cast_Full.krml .output/LowStar_ImmutableBuffer.krml .output/LowStar_Literal.krml .output/StringLit.krml .output/Op.krml .output/LowStar_Comment.krml .output/ExternalEq.krml .output/UnusedPoly.krml .output/Spec_Loops.krml .output/LowStar_BufferOps.krml .output/C_Loops.krml .output/WasmSupport.krml .output/GlobalInit2.krml .output/GlobalInit.krml .output/MonomorphizationSeparate1.krml .output/LowStar_Ignore.krml .output/Wasm2.krml .output/Abbrev.krml .output/Ghost2.krml .output/RingBuffer.krml .output/Substitute.krml .output/Unused_A.krml .output/Unused_B.krml .output/Abstract.krml .output/C_Failure.krml .output/InitializerLists.krml .output/Ctypes1.krml .output/Ctypes2.krml .output/BadMatch.krml .output/MemCpyModel.krml .output/FStar_SizeT.krml .output/LowStar_Failure.krml .output/LowStar_Lib_LinkedList.krml .output/LowStar_Lib_LinkedList2.krml .output/LowStar_Lib_AssocList.krml .output/Inline.krml .output/LinkedList4.krml .output/Ctypes3.krml .output/InlineTest.krml .output/StaticHeaderAPI.krml .output/StaticHeaderLib.krml .output/StaticHeader.krml .output/UnusedParameter.krml .output/ParamAbbrev.krml .output/Rust4.krml .output/AbstractStructParameter.krml .output/AbstractStructAbstract.krml .output/AbstractStruct2.krml .output/IfThenElse.krml .output/PrivateInclude1.krml .output/PrivateInclude2.krml .output/Server.krml .output/DepPair.krml .output/VariableMerge.krml .output/Wasm9.krml .output/ML16Externals.krml .output/TwoUnitsAreOne.krml .output/ForwardDecl.krml .output/C89.krml .output/NameCollisionHelper.krml .output/FunctionalEncoding.krml .output/MemCpy.krml .output/RecordTypingLimitation.krml .output/LowStar_Printf.krml .output/LowStar_ConstBuffer.krml .output/ConstBuffer.krml .output/Wasm8.krml .output/ProperErasure.krml .output/StructWithUnitIsUnit.krml .output/Failure.krml .output/MonomorphizationCrash.krml .output/LowStar_UninitializedBuffer.krml .output/UBuffer.krml .output/Ignore.krml .output/Ctypes4.krml .output/FStar_Endianness.krml .output/LowStar_Endianness.krml .output/DataTypesSimple.krml .output/FStar_Modifies.krml .output/Rust1.krml .output/Null.krml .output/MallocFree.krml .output/GcTypes.krml .output/Structs.krml .output/C_Nullity.krml .output/Tuples.krml .output/DataTypesMut.krml .output/Deref.krml .output/AbstractStruct.krml .output/Unsound.krml .output/EqB.krml .output/MonomorphizationSeparate2.krml .output/RecursivePoly.krml .output/Polymorphic.krml .output/LinkedList2.krml .output/BlitNull.krml .output/ML16.krml .output/IfDef.krml .output/Wasm5.krml .output/Ghost1.krml .output/TailCalls2.krml .output/Scope.krml .output/Strlen.krml .output/ColoredRegion.krml .output/EtaStruct.krml .output/NoExtract.krml .output/Flat.krml .output/Literal.krml .output/ExitCode.krml .output/TopLevelArray.krml .output/Fill.krml .output/NoShadow.krml .output/TailCalls.krml .output/Uu.krml .output/Failwith.krml .output/DataTypesEq.krml .output/EmptyStruct.krml .output/TestAlloca.krml .output/Vla.krml .output/Layered.krml .output/LinkedList1.krml .output/HigherOrder4.krml .output/NameCollision.krml .output/CustomEq.krml .output/Renaming.krml .output/Wasm3.krml .output/HigherOrder6.krml .output/Wireguard.krml .output/WasmTrap.krml .output/NoConstructor.krml .output/Parameterized.krml .output/PatternAny.krml .output/OpEq.krml .output/InlineNoExtract.krml .output/PushPop.krml .output/Wasm6.krml .output/OptimizedOption.krml .output/Structs2.krml .output/Loops.krml .output/Recursive.krml .output/Rust5.krml .output/WildCard.krml .output/HigherOrder5.krml .output/Wasm4.krml .output/Mini.krml .output/Rust6.krml .output/HigherOrder2.krml .output/Macro.krml .output/ExternErased.krml .output/DataTypes.krml .output/TotalLoops.krml .output/Intro.krml .output/Printf.krml .output/Endianness.krml .output/Wasm7.krml .output/HigherOrder.krml .output/Verbatim.krml .output/Library.krml .output/Attributes.krml .output/HigherOrder3.krml .output/Private.krml .output/MutualStruct.krml .output/IfDefKrml.krml .output/Const.krml .output/FunPtr.krml .output/Shifting.krml .output/SimpleWasm.krml .output/Wasm1.krml .output/MulDiv.krml .output/LinkedList3.krml .output/MatchNested.krml .output/MutRec.krml .output/Comment.krml -bundle Op=WindowsHack,\*
✔ [Monomorphization] ⏱️ 53ms
✔ [Inlining] ⏱️ 2ms
✔ [Pattern matches compilation] ⏱️ 7ms
✔ [Structs + Simplify 2] ⏱️ 4ms
✔ [Drop] ⏱️ <1ms
✔ [AstToCStar] ⏱️ 2ms
Fatal exception raised in main
Fatal error: exception Failure("[mk_expr m]: op should've been caught")
make[1]: *** [Makefile:139: .output/Op.exe] Error 2
make[1]: Leaving directory '/home/guido/r/karamel/test'

It's triggering this failwith: https://github.com/FStarLang/karamel/blob/b76942a3fa36c016a7fb1da96ce924c71964488a/lib/CStarToC11.ml#L1037-L1038