From 3fd81876c10f688808ed585ad1edaf798c4b24c3 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 21 Mar 2024 14:21:11 -0400 Subject: [PATCH 1/3] crucible-llvm: Don't pass around the symbolic backend explicitly `Lang.Crucible.Simulator.OverrideSim.{getSymInterface,ovrWithBackend}` can replace the explicit passing of `bak`. This should simplify some type signatures. --- .../src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs | 643 ++++++++--------- .../src/Lang/Crucible/LLVM/Intrinsics/Libc.hs | 664 +++++++++--------- 2 files changed, 661 insertions(+), 646 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs index 570f94aad..6fe9f5190 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs @@ -59,6 +59,14 @@ import Lang.Crucible.LLVM.QQ( llvmOvr ) import Lang.Crucible.LLVM.Intrinsics.Common import qualified Lang.Crucible.LLVM.Intrinsics.Libc as Libc +-- | Local helper to make a null pointer in 'OverrideSim' +mkNull + :: (IsSymInterface sym, HasPtrWidth wptr) + => OverrideSim p sym ext rtp args ret (LLVMPtr sym wptr) +mkNull = do + sym <- getSymInterface + liftIO (mkNullPointer sym PtrWidth) + ------------------------------------------------------------------------ -- ** Declarations @@ -73,7 +81,7 @@ llvmLifetimeStartOverride => LLVMOverride p sym ext (EmptyCtx ::> BVType 64 ::> LLVMPointerType wptr) UnitType llvmLifetimeStartOverride = [llvmOvr| void @llvm.lifetime.start( i64, i8* ) |] - (\_ops _sym _args -> return ()) + (\_ops _bak _args -> return ()) -- | See comment on 'llvmLifetimeStartOverride' -- @@ -83,7 +91,7 @@ llvmLifetimeEndOverride => LLVMOverride p sym ext (EmptyCtx ::> BVType 64 ::> LLVMPointerType wptr) UnitType llvmLifetimeEndOverride = [llvmOvr| void @llvm.lifetime.end( i64, i8* ) |] - (\_ops _sym _args -> return ()) + (\_ops _bak _args -> return ()) -- | This is a no-op. -- @@ -100,7 +108,7 @@ llvmLifetimeOverrideOverload llvmLifetimeOverrideOverload startOrEnd w = let nm = L.Symbol ("llvm.lifetime." ++ startOrEnd ++ ".p0i" ++ show (widthVal w)) in [llvmOvr| void $nm ( i64, #w * ) |] - (\_ops _sym _args -> return ()) + (\_ops _bak _args -> return ()) -- | Like 'llvmLifetimeOverrideOverload', but with an opaque pointer type. llvmLifetimeOverrideOverload_opaque @@ -113,7 +121,7 @@ llvmLifetimeOverrideOverload_opaque llvmLifetimeOverrideOverload_opaque startOrEnd = let nm = L.Symbol ("llvm.lifetime." ++ startOrEnd ++ ".p0") in [llvmOvr| void $nm ( i64, ptr ) |] - (\_ops _sym _args -> return ()) + (\_ops _bak _args -> return ()) -- | This intrinsic is currently a no-op. -- @@ -130,7 +138,7 @@ llvmInvariantStartOverride llvmInvariantStartOverride w = let nm = L.Symbol ("llvm.invariant.start.p0i" ++ show (widthVal w)) in [llvmOvr| {}* $nm ( i64, #w * ) |] - (\_ops bak _args -> liftIO (mkNullPointer (backendGetSym bak) PtrWidth)) + (\_ops _bak _args -> mkNull) -- | Like 'llvmInvariantStartOverride', but with an opaque pointer type. llvmInvariantStartOverride_opaque @@ -141,7 +149,7 @@ llvmInvariantStartOverride_opaque llvmInvariantStartOverride_opaque = let nm = L.Symbol "llvm.invariant.start.p0" in [llvmOvr| {}* $nm ( i64, ptr ) |] - (\_ops bak _args -> liftIO (mkNullPointer (backendGetSym bak) PtrWidth)) + (\_ops _bak _args -> mkNull) -- | See comment on 'llvmInvariantStartOverride'. llvmInvariantEndOverride @@ -218,7 +226,7 @@ llvmStacksave => LLVMOverride p sym ext EmptyCtx (LLVMPointerType wptr) llvmStacksave = [llvmOvr| i8* @llvm.stacksave() |] - (\_memOps bak _args -> liftIO (mkNullPointer (backendGetSym bak) PtrWidth)) + (\_memOps _bak _args -> mkNull) llvmStackrestore :: (IsSymInterface sym, HasPtrWidth wptr) @@ -236,8 +244,8 @@ llvmMemmoveOverride_8_8_32 UnitType llvmMemmoveOverride_8_8_32 = [llvmOvr| void @llvm.memmove.p0i8.p0i8.i32( i8*, i8*, i32, i32, i1 ) |] - (\memOps bak args -> - Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemmove bak memOps dst src len v) args) + (\memOps _bak args -> + Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemmove memOps dst src len v) args) llvmMemmoveOverride_8_8_32_noalign :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -248,7 +256,7 @@ llvmMemmoveOverride_8_8_32_noalign UnitType llvmMemmoveOverride_8_8_32_noalign = [llvmOvr| void @llvm.memmove.p0i8.p0i8.i32( i8*, i8*, i32, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (Libc.callMemmove bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemmove memOps) args) llvmMemmoveOverride_8_8_32_noalign_opaque :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -259,7 +267,7 @@ llvmMemmoveOverride_8_8_32_noalign_opaque UnitType llvmMemmoveOverride_8_8_32_noalign_opaque = [llvmOvr| void @llvm.memmove.p0.p0.i32( ptr, ptr, i32, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (Libc.callMemmove bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemmove memOps) args) llvmMemmoveOverride_8_8_64 @@ -271,8 +279,8 @@ llvmMemmoveOverride_8_8_64 UnitType llvmMemmoveOverride_8_8_64 = [llvmOvr| void @llvm.memmove.p0i8.p0i8.i64( i8*, i8*, i64, i32, i1 ) |] - (\memOps bak args -> - Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemmove bak memOps dst src len v) args) + (\memOps _bak args -> + Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemmove memOps dst src len v) args) llvmMemmoveOverride_8_8_64_noalign :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -283,7 +291,7 @@ llvmMemmoveOverride_8_8_64_noalign UnitType llvmMemmoveOverride_8_8_64_noalign = [llvmOvr| void @llvm.memmove.p0i8.p0i8.i64( i8*, i8*, i64, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (Libc.callMemmove bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemmove memOps) args) llvmMemmoveOverride_8_8_64_noalign_opaque :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -294,8 +302,8 @@ llvmMemmoveOverride_8_8_64_noalign_opaque UnitType llvmMemmoveOverride_8_8_64_noalign_opaque = [llvmOvr| void @llvm.memmove.p0.p0.i64( ptr, ptr, i64, i1 ) |] - (\memOps bak args -> - Ctx.uncurryAssignment (Libc.callMemmove bak memOps) args) + (\memOps _bak args -> + Ctx.uncurryAssignment (Libc.callMemmove memOps) args) llvmMemsetOverride_8_64 @@ -309,8 +317,8 @@ llvmMemsetOverride_8_64 UnitType llvmMemsetOverride_8_64 = [llvmOvr| void @llvm.memset.p0i8.i64( i8*, i8, i64, i32, i1 ) |] - (\memOps bak args -> - Ctx.uncurryAssignment (\dst val len _align v -> Libc.callMemset bak memOps dst val len v) args) + (\memOps _bak args -> + Ctx.uncurryAssignment (\dst val len _align v -> Libc.callMemset memOps dst val len v) args) llvmMemsetOverride_8_64_noalign :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) @@ -322,7 +330,7 @@ llvmMemsetOverride_8_64_noalign UnitType llvmMemsetOverride_8_64_noalign = [llvmOvr| void @llvm.memset.p0i8.i64( i8*, i8, i64, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (Libc.callMemset bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) llvmMemsetOverride_8_64_noalign_opaque :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) @@ -334,7 +342,7 @@ llvmMemsetOverride_8_64_noalign_opaque UnitType llvmMemsetOverride_8_64_noalign_opaque = [llvmOvr| void @llvm.memset.p0.i64( ptr, i8, i64, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (Libc.callMemset bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) llvmMemsetOverride_8_32 @@ -348,8 +356,8 @@ llvmMemsetOverride_8_32 UnitType llvmMemsetOverride_8_32 = [llvmOvr| void @llvm.memset.p0i8.i32( i8*, i8, i32, i32, i1 ) |] - (\memOps bak args -> - Ctx.uncurryAssignment (\dst val len _align v -> Libc.callMemset bak memOps dst val len v) args) + (\memOps _bak args -> + Ctx.uncurryAssignment (\dst val len _align v -> Libc.callMemset memOps dst val len v) args) llvmMemsetOverride_8_32_noalign :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) @@ -361,7 +369,7 @@ llvmMemsetOverride_8_32_noalign UnitType llvmMemsetOverride_8_32_noalign = [llvmOvr| void @llvm.memset.p0i8.i32( i8*, i8, i32, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (Libc.callMemset bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) llvmMemsetOverride_8_32_noalign_opaque :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) @@ -373,7 +381,7 @@ llvmMemsetOverride_8_32_noalign_opaque UnitType llvmMemsetOverride_8_32_noalign_opaque = [llvmOvr| void @llvm.memset.p0.i32( ptr, i8, i32, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (Libc.callMemset bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) llvmMemcpyOverride_8_8_32 @@ -385,8 +393,8 @@ llvmMemcpyOverride_8_8_32 UnitType llvmMemcpyOverride_8_8_32 = [llvmOvr| void @llvm.memcpy.p0i8.p0i8.i32( i8*, i8*, i32, i32, i1 ) |] - (\memOps bak args -> - Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemcpy bak memOps dst src len v) args) + (\memOps _bak args -> + Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemcpy memOps dst src len v) args) llvmMemcpyOverride_8_8_32_noalign :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -397,7 +405,7 @@ llvmMemcpyOverride_8_8_32_noalign UnitType llvmMemcpyOverride_8_8_32_noalign = [llvmOvr| void @llvm.memcpy.p0i8.p0i8.i32( i8*, i8*, i32, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (Libc.callMemcpy bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) llvmMemcpyOverride_8_8_32_noalign_opaque :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -408,7 +416,7 @@ llvmMemcpyOverride_8_8_32_noalign_opaque UnitType llvmMemcpyOverride_8_8_32_noalign_opaque = [llvmOvr| void @llvm.memcpy.p0.p0.i32( ptr, ptr, i32, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (Libc.callMemcpy bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) llvmMemcpyOverride_8_8_64 @@ -420,8 +428,8 @@ llvmMemcpyOverride_8_8_64 UnitType llvmMemcpyOverride_8_8_64 = [llvmOvr| void @llvm.memcpy.p0i8.p0i8.i64( i8*, i8*, i64, i32, i1 ) |] - (\memOps bak args -> - Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemcpy bak memOps dst src len v) args) + (\memOps _bak args -> + Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemcpy memOps dst src len v) args) llvmMemcpyOverride_8_8_64_noalign :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -432,7 +440,7 @@ llvmMemcpyOverride_8_8_64_noalign UnitType llvmMemcpyOverride_8_8_64_noalign = [llvmOvr| void @llvm.memcpy.p0i8.p0i8.i64( i8*, i8*, i64, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (Libc.callMemcpy bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) llvmMemcpyOverride_8_8_64_noalign_opaque :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -443,7 +451,7 @@ llvmMemcpyOverride_8_8_64_noalign_opaque UnitType llvmMemcpyOverride_8_8_64_noalign_opaque = [llvmOvr| void @llvm.memcpy.p0.p0.i64( ptr, ptr, i64, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (Libc.callMemcpy bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) llvmObjectsizeOverride_32 @@ -451,56 +459,56 @@ llvmObjectsizeOverride_32 => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1) (BVType 32) llvmObjectsizeOverride_32 = [llvmOvr| i32 @llvm.objectsize.i32.p0i8( i8*, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callObjectsize bak memOps knownNat) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize memOps knownNat) args) llvmObjectsizeOverride_32_null :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1) (BVType 32) llvmObjectsizeOverride_32_null = [llvmOvr| i32 @llvm.objectsize.i32.p0i8( i8*, i1, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callObjectsize_null bak memOps knownNat) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null memOps knownNat) args) llvmObjectsizeOverride_32_null_dynamic :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1 ::> BVType 1) (BVType 32) llvmObjectsizeOverride_32_null_dynamic = [llvmOvr| i32 @llvm.objectsize.i32.p0i8( i8*, i1, i1, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic bak memOps knownNat) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) llvmObjectsizeOverride_32_null_dynamic_opaque :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1 ::> BVType 1) (BVType 32) llvmObjectsizeOverride_32_null_dynamic_opaque = [llvmOvr| i32 @llvm.objectsize.i32.p0( ptr, i1, i1, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic bak memOps knownNat) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) llvmObjectsizeOverride_64 :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1) (BVType 64) llvmObjectsizeOverride_64 = [llvmOvr| i64 @llvm.objectsize.i64.p0i8( i8*, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callObjectsize bak memOps knownNat) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize memOps knownNat) args) llvmObjectsizeOverride_64_null :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1) (BVType 64) llvmObjectsizeOverride_64_null = [llvmOvr| i64 @llvm.objectsize.i64.p0i8( i8*, i1, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callObjectsize_null bak memOps knownNat) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null memOps knownNat) args) llvmObjectsizeOverride_64_null_dynamic :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1 ::> BVType 1) (BVType 64) llvmObjectsizeOverride_64_null_dynamic = [llvmOvr| i64 @llvm.objectsize.i64.p0i8( i8*, i1, i1, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic bak memOps knownNat) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) llvmObjectsizeOverride_64_null_dynamic_opaque :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1 ::> BVType 1) (BVType 64) llvmObjectsizeOverride_64_null_dynamic_opaque = [llvmOvr| i64 @llvm.objectsize.i64.p0( ptr, i1, i1, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic bak memOps knownNat) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) -- | This instruction is a hint to code generators, which means that it is a -- no-op for us. @@ -551,7 +559,7 @@ llvmFshl :: llvmFshl w = let nm = L.Symbol ("llvm.fshl.i" ++ show (natValue w)) in [llvmOvr| #w $nm ( #w, #w, #w ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callFshl bak w) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callFshl w) args) llvmFshr :: (1 <= w, IsSymInterface sym) => @@ -562,7 +570,7 @@ llvmFshr :: llvmFshr w = let nm = L.Symbol ("llvm.fshr.i" ++ show (natValue w)) in [llvmOvr| #w $nm ( #w, #w, #w ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callFshr bak w) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callFshr w) args) llvmSaddWithOverflow :: (1 <= w, IsSymInterface sym) @@ -573,7 +581,7 @@ llvmSaddWithOverflow llvmSaddWithOverflow w = let nm = L.Symbol ("llvm.sadd.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callSaddWithOverflow bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callSaddWithOverflow memOps) args) llvmUaddWithOverflow :: (1 <= w, IsSymInterface sym) @@ -584,7 +592,7 @@ llvmUaddWithOverflow llvmUaddWithOverflow w = let nm = L.Symbol ("llvm.uadd.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callUaddWithOverflow bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callUaddWithOverflow memOps) args) llvmSsubWithOverflow @@ -596,7 +604,7 @@ llvmSsubWithOverflow llvmSsubWithOverflow w = let nm = L.Symbol ("llvm.ssub.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callSsubWithOverflow bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callSsubWithOverflow memOps) args) llvmUsubWithOverflow @@ -608,7 +616,7 @@ llvmUsubWithOverflow llvmUsubWithOverflow w = let nm = L.Symbol ("llvm.usub.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callUsubWithOverflow bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callUsubWithOverflow memOps) args) llvmSmulWithOverflow :: (1 <= w, IsSymInterface sym) @@ -619,7 +627,7 @@ llvmSmulWithOverflow llvmSmulWithOverflow w = let nm = L.Symbol ("llvm.smul.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callSmulWithOverflow bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callSmulWithOverflow memOps) args) llvmUmulWithOverflow :: (1 <= w, IsSymInterface sym) @@ -630,7 +638,7 @@ llvmUmulWithOverflow llvmUmulWithOverflow w = let nm = L.Symbol ("llvm.umul.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callUmulWithOverflow bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callUmulWithOverflow memOps) args) llvmUmax :: (1 <= w, IsSymInterface sym) => @@ -641,7 +649,7 @@ llvmUmax :: llvmUmax w = let nm = L.Symbol ("llvm.umax.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callUmax bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callUmax memOps) args) llvmUmin :: (1 <= w, IsSymInterface sym) => @@ -652,7 +660,7 @@ llvmUmin :: llvmUmin w = let nm = L.Symbol ("llvm.umin.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callUmin bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callUmin memOps) args) llvmSmax :: (1 <= w, IsSymInterface sym) => @@ -663,7 +671,7 @@ llvmSmax :: llvmSmax w = let nm = L.Symbol ("llvm.smax.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callSmax bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callSmax memOps) args) llvmSmin :: (1 <= w, IsSymInterface sym) => @@ -674,7 +682,7 @@ llvmSmin :: llvmSmin w = let nm = L.Symbol ("llvm.smin.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callSmin bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callSmin memOps) args) llvmCtlz :: (1 <= w, IsSymInterface sym) @@ -685,7 +693,7 @@ llvmCtlz llvmCtlz w = let nm = L.Symbol ("llvm.ctlz.i" ++ show (natValue w)) in [llvmOvr| #w $nm ( #w, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callCtlz bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callCtlz memOps) args) llvmCttz :: (1 <= w, IsSymInterface sym) @@ -696,7 +704,7 @@ llvmCttz llvmCttz w = let nm = L.Symbol ("llvm.cttz.i" ++ show (natValue w)) in [llvmOvr| #w $nm ( #w, i1 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callCttz bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callCttz memOps) args) llvmCtpop :: (1 <= w, IsSymInterface sym) @@ -707,7 +715,7 @@ llvmCtpop llvmCtpop w = let nm = L.Symbol ("llvm.ctpop.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callCtpop bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callCtpop memOps) args) llvmBitreverse :: (1 <= w, IsSymInterface sym) @@ -718,7 +726,7 @@ llvmBitreverse llvmBitreverse w = let nm = L.Symbol ("llvm.bitreverse.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callBitreverse bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callBitreverse memOps) args) -- | llvmBSwapOverride @@ -739,7 +747,7 @@ llvmBSwapOverride widthRepr = -- From the LLVM docs: -- declare i16 @llvm.bswap.i16(i16 ) [llvmOvr| #width8 $nm( #width8 ) |] - (\_ bak args -> Ctx.uncurryAssignment (Libc.callBSwap bak widthRepr) args) + (\_ _bak args -> Ctx.uncurryAssignment (Libc.callBSwap widthRepr) args) }}} llvmAbsOverride :: @@ -751,9 +759,9 @@ llvmAbsOverride :: llvmAbsOverride w = let nm = L.Symbol ("llvm.abs.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, i1 ) |] - (\mvar bak args -> + (\mvar _bak args -> do callStack <- callStackFromMemVar' mvar - Ctx.uncurryAssignment (Libc.callLLVMAbs bak callStack w) args) + Ctx.uncurryAssignment (Libc.callLLVMAbs callStack w) args) llvmCopysignOverride_F32 :: IsSymInterface sym => @@ -762,7 +770,7 @@ llvmCopysignOverride_F32 :: (FloatType SingleFloat) llvmCopysignOverride_F32 = [llvmOvr| float @llvm.copysign.f32( float, float ) |] - (\_memOpts bak args -> Ctx.uncurryAssignment (callCopysign bak) args) + (\_memOpts _bak args -> Ctx.uncurryAssignment callCopysign args) llvmCopysignOverride_F64 :: IsSymInterface sym => @@ -771,7 +779,7 @@ llvmCopysignOverride_F64 :: (FloatType DoubleFloat) llvmCopysignOverride_F64 = [llvmOvr| double @llvm.copysign.f64( double, double ) |] - (\_memOpts bak args -> Ctx.uncurryAssignment (callCopysign bak) args) + (\_memOpts _bak args -> Ctx.uncurryAssignment callCopysign args) llvmFabsF32 @@ -782,7 +790,9 @@ llvmFabsF32 (FloatType SingleFloat) llvmFabsF32 = [llvmOvr| float @llvm.fabs.f32( float ) |] - (\_memOps bak (Empty :> (regValue -> x)) -> liftIO (iFloatAbs @_ @SingleFloat (backendGetSym bak) x)) + (\_memOps _bak (Empty :> (regValue -> x)) -> do + sym <- getSymInterface + liftIO (iFloatAbs @_ @SingleFloat sym x)) llvmFabsF64 @@ -793,7 +803,9 @@ llvmFabsF64 (FloatType DoubleFloat) llvmFabsF64 = [llvmOvr| double @llvm.fabs.f64( double ) |] - (\_memOps bak (Empty :> (regValue -> x)) -> liftIO (iFloatAbs @_ @DoubleFloat (backendGetSym bak) x)) + (\_memOps _bak (Empty :> (regValue -> x)) -> do + sym <- getSymInterface + liftIO (iFloatAbs @_ @DoubleFloat sym x)) llvmCeilOverride_F32 :: IsSymInterface sym => @@ -802,7 +814,7 @@ llvmCeilOverride_F32 :: (FloatType SingleFloat) llvmCeilOverride_F32 = [llvmOvr| float @llvm.ceil.f32( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callCeil bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callCeil args) llvmCeilOverride_F64 :: IsSymInterface sym => @@ -811,7 +823,7 @@ llvmCeilOverride_F64 :: (FloatType DoubleFloat) llvmCeilOverride_F64 = [llvmOvr| double @llvm.ceil.f64( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callCeil bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callCeil args) llvmFloorOverride_F32 :: IsSymInterface sym => @@ -820,7 +832,7 @@ llvmFloorOverride_F32 :: (FloatType SingleFloat) llvmFloorOverride_F32 = [llvmOvr| float @llvm.floor.f32( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callFloor bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFloor args) llvmFloorOverride_F64 :: IsSymInterface sym => @@ -829,7 +841,7 @@ llvmFloorOverride_F64 :: (FloatType DoubleFloat) llvmFloorOverride_F64 = [llvmOvr| double @llvm.floor.f64( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callFloor bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFloor args) llvmSqrtOverride_F32 :: IsSymInterface sym => @@ -838,7 +850,7 @@ llvmSqrtOverride_F32 :: (FloatType SingleFloat) llvmSqrtOverride_F32 = [llvmOvr| float @llvm.sqrt.f32( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSqrt bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callSqrt args) llvmSqrtOverride_F64 :: IsSymInterface sym => @@ -847,7 +859,7 @@ llvmSqrtOverride_F64 :: (FloatType DoubleFloat) llvmSqrtOverride_F64 = [llvmOvr| double @llvm.sqrt.f64( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSqrt bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callSqrt args) llvmSinOverride_F32 :: IsSymInterface sym => @@ -856,7 +868,7 @@ llvmSinOverride_F32 :: (FloatType SingleFloat) llvmSinOverride_F32 = [llvmOvr| float @llvm.sin.f32( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Sin) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sin) args) llvmSinOverride_F64 :: IsSymInterface sym => @@ -865,7 +877,7 @@ llvmSinOverride_F64 :: (FloatType DoubleFloat) llvmSinOverride_F64 = [llvmOvr| double @llvm.sin.f64( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Sin) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sin) args) llvmCosOverride_F32 :: IsSymInterface sym => @@ -874,7 +886,7 @@ llvmCosOverride_F32 :: (FloatType SingleFloat) llvmCosOverride_F32 = [llvmOvr| float @llvm.cos.f32( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Cos) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cos) args) llvmCosOverride_F64 :: IsSymInterface sym => @@ -883,7 +895,7 @@ llvmCosOverride_F64 :: (FloatType DoubleFloat) llvmCosOverride_F64 = [llvmOvr| double @llvm.cos.f64( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Cos) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cos) args) llvmPowOverride_F32 :: IsSymInterface sym => @@ -892,7 +904,7 @@ llvmPowOverride_F32 :: (FloatType SingleFloat) llvmPowOverride_F32 = [llvmOvr| float @llvm.pow.f32( float, float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 bak W4.Pow) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Pow) args) llvmPowOverride_F64 :: IsSymInterface sym => @@ -901,7 +913,7 @@ llvmPowOverride_F64 :: (FloatType DoubleFloat) llvmPowOverride_F64 = [llvmOvr| double @llvm.pow.f64( double, double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 bak W4.Pow) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Pow) args) llvmExpOverride_F32 :: IsSymInterface sym => @@ -910,7 +922,7 @@ llvmExpOverride_F32 :: (FloatType SingleFloat) llvmExpOverride_F32 = [llvmOvr| float @llvm.exp.f32( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Exp) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp) args) llvmExpOverride_F64 :: IsSymInterface sym => @@ -919,7 +931,7 @@ llvmExpOverride_F64 :: (FloatType DoubleFloat) llvmExpOverride_F64 = [llvmOvr| double @llvm.exp.f64( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Exp) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp) args) llvmLogOverride_F32 :: IsSymInterface sym => @@ -928,7 +940,7 @@ llvmLogOverride_F32 :: (FloatType SingleFloat) llvmLogOverride_F32 = [llvmOvr| float @llvm.log.f32( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Log) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log) args) llvmLogOverride_F64 :: IsSymInterface sym => @@ -937,7 +949,7 @@ llvmLogOverride_F64 :: (FloatType DoubleFloat) llvmLogOverride_F64 = [llvmOvr| double @llvm.log.f64( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Log) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log) args) llvmExp2Override_F32 :: IsSymInterface sym => @@ -946,7 +958,7 @@ llvmExp2Override_F32 :: (FloatType SingleFloat) llvmExp2Override_F32 = [llvmOvr| float @llvm.exp2.f32( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Exp2) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp2) args) llvmExp2Override_F64 :: IsSymInterface sym => @@ -955,7 +967,7 @@ llvmExp2Override_F64 :: (FloatType DoubleFloat) llvmExp2Override_F64 = [llvmOvr| double @llvm.exp2.f64( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Exp2) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp2) args) llvmLog2Override_F32 :: IsSymInterface sym => @@ -964,7 +976,7 @@ llvmLog2Override_F32 :: (FloatType SingleFloat) llvmLog2Override_F32 = [llvmOvr| float @llvm.log2.f32( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Log2) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log2) args) llvmLog2Override_F64 :: IsSymInterface sym => @@ -973,7 +985,7 @@ llvmLog2Override_F64 :: (FloatType DoubleFloat) llvmLog2Override_F64 = [llvmOvr| double @llvm.log2.f64( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Log2) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log2) args) llvmLog10Override_F32 :: IsSymInterface sym => @@ -982,7 +994,7 @@ llvmLog10Override_F32 :: (FloatType SingleFloat) llvmLog10Override_F32 = [llvmOvr| float @llvm.log10.f32( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Log10) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log10) args) llvmLog10Override_F64 :: IsSymInterface sym => @@ -991,7 +1003,7 @@ llvmLog10Override_F64 :: (FloatType DoubleFloat) llvmLog10Override_F64 = [llvmOvr| double @llvm.log10.f64( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Log10) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log10) args) llvmIsFpclassOverride_F32 :: IsSymInterface sym => @@ -1001,7 +1013,7 @@ llvmIsFpclassOverride_F32 :: (BVType 1) llvmIsFpclassOverride_F32 = [llvmOvr| i1 @llvm.is.fpclass.f32( float, i32 ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callIsFpclass bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment callIsFpclass args) llvmIsFpclassOverride_F64 :: IsSymInterface sym => @@ -1011,7 +1023,7 @@ llvmIsFpclassOverride_F64 :: (BVType 1) llvmIsFpclassOverride_F64 = [llvmOvr| i1 @llvm.is.fpclass.f64( double, i32 ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callIsFpclass bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment callIsFpclass args) llvmFmaOverride_F32 :: forall sym p ext @@ -1023,7 +1035,7 @@ llvmFmaOverride_F32 :: (FloatType SingleFloat) llvmFmaOverride_F32 = [llvmOvr| float @llvm.fma.f32( float, float, float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callFMA bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFMA args) llvmFmaOverride_F64 :: forall sym p ext @@ -1035,7 +1047,7 @@ llvmFmaOverride_F64 :: (FloatType DoubleFloat) llvmFmaOverride_F64 = [llvmOvr| double @llvm.fma.f64( double, double, double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callFMA bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFMA args) llvmFmuladdOverride_F32 :: forall sym p ext @@ -1047,7 +1059,7 @@ llvmFmuladdOverride_F32 :: (FloatType SingleFloat) llvmFmuladdOverride_F32 = [llvmOvr| float @llvm.fmuladd.f32( float, float, float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callFMA bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFMA args) llvmFmuladdOverride_F64 :: forall sym p ext @@ -1059,7 +1071,7 @@ llvmFmuladdOverride_F64 :: (FloatType DoubleFloat) llvmFmuladdOverride_F64 = [llvmOvr| double @llvm.fmuladd.f64( double, double, double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callFMA bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFMA args) llvmX86_pclmulqdq @@ -1072,7 +1084,7 @@ llvmX86_pclmulqdq (VectorType (BVType 64)) llvmX86_pclmulqdq = [llvmOvr| <2 x i64> @llvm.x86.pclmulqdq(<2 x i64>, <2 x i64>, i8) |] - (\memOps bak args -> Ctx.uncurryAssignment (callX86_pclmulqdq bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callX86_pclmulqdq memOps) args) llvmX86_SSE2_storeu_dq @@ -1086,45 +1098,45 @@ llvmX86_SSE2_storeu_dq UnitType llvmX86_SSE2_storeu_dq = [llvmOvr| void @llvm.x86.sse2.storeu.dq( i8*, <16 x i8> ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callStoreudq bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callStoreudq memOps) args) ------------------------------------------------------------------------ -- ** Implementations -callX86_pclmulqdq :: forall p sym bak ext wptr r args ret. - (IsSymBackend sym bak, HasPtrWidth wptr) => - bak -> +callX86_pclmulqdq :: forall p sym ext wptr r args ret. + (IsSymInterface sym, HasPtrWidth wptr) => GlobalVar Mem -> RegEntry sym (VectorType (BVType 64)) -> RegEntry sym (VectorType (BVType 64)) -> RegEntry sym (BVType 8) -> OverrideSim p sym ext r args ret (RegValue sym (VectorType (BVType 64))) -callX86_pclmulqdq bak _mvar +callX86_pclmulqdq _mvar (regValue -> xs) (regValue -> ys) (regValue -> imm) = - do unless (V.length xs == 2) $ - liftIO $ addFailedAssertion bak $ AssertFailureSimError - ("Vector length mismatch in llvm.x86.pclmulqdq intrinsic") - (unwords ["Expected <2 x i64>, but got vector of length", show (V.length xs)]) - unless (V.length ys == 2) $ - liftIO $ addFailedAssertion bak $ AssertFailureSimError - ("Vector length mismatch in llvm.x86.pclmulqdq intrinsic") - (unwords ["Expected <2 x i64>, but got vector of length", show (V.length ys)]) - case BV.asUnsigned <$> asBV imm of - Just byte -> - do let xidx = if byte .&. 0x01 == 0 then 0 else 1 - let yidx = if byte .&. 0x10 == 0 then 0 else 1 - liftIO $ doPcmul (xs V.! xidx) (ys V.! yidx) - _ -> - liftIO $ addFailedAssertion bak $ AssertFailureSimError - ("Illegal selector argument to llvm.x86.pclmulqdq") - (unwords ["Expected concrete value but got", show (printSymExpr imm)]) + ovrWithBackend $ \bak -> do + unless (V.length xs == 2) $ + liftIO $ addFailedAssertion bak $ AssertFailureSimError + ("Vector length mismatch in llvm.x86.pclmulqdq intrinsic") + (unwords ["Expected <2 x i64>, but got vector of length", show (V.length xs)]) + unless (V.length ys == 2) $ + liftIO $ addFailedAssertion bak $ AssertFailureSimError + ("Vector length mismatch in llvm.x86.pclmulqdq intrinsic") + (unwords ["Expected <2 x i64>, but got vector of length", show (V.length ys)]) + case BV.asUnsigned <$> asBV imm of + Just byte -> + do let xidx = if byte .&. 0x01 == 0 then 0 else 1 + let yidx = if byte .&. 0x10 == 0 then 0 else 1 + let sym = backendGetSym bak + liftIO $ doPcmul sym (xs V.! xidx) (ys V.! yidx) + _ -> + liftIO $ addFailedAssertion bak $ AssertFailureSimError + ("Illegal selector argument to llvm.x86.pclmulqdq") + (unwords ["Expected concrete value but got", show (printSymExpr imm)]) where - sym = backendGetSym bak - doPcmul :: SymBV sym 64 -> SymBV sym 64 -> IO (V.Vector (SymBV sym 64)) - doPcmul x y = + doPcmul :: sym -> SymBV sym 64 -> SymBV sym 64 -> IO (V.Vector (SymBV sym 64)) + doPcmul sym x y = do r <- carrylessMultiply sym x y lo <- bvTrunc sym (knownNat @64) r hi <- bvSelect sym (knownNat @64) (knownNat @64) r @@ -1132,32 +1144,32 @@ callX86_pclmulqdq bak _mvar return $ V.fromList [ lo, hi ] callStoreudq - :: ( IsSymBackend sym bak + :: ( IsSymInterface sym , HasLLVMAnn sym , HasPtrWidth wptr , ?memOpts :: MemOptions ) - => bak - -> GlobalVar Mem + => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (VectorType (BVType 8)) -> OverrideSim p sym ext r args ret () -callStoreudq bak mvar +callStoreudq mvar (regValue -> dest) (regValue -> vec) = - do mem <- readGlobal mvar - unless (V.length vec == 16) $ - liftIO $ addFailedAssertion bak $ AssertFailureSimError - ("Vector length mismatch in stored_qu intrinsic.") - (unwords ["Expected <16 x i8>, but got vector of length", show (V.length vec)]) - mem' <- liftIO $ doStore - bak - mem - dest - (VectorRepr (KnownBV @8)) - (arrayType 16 (bitvectorType (Bytes 1))) - noAlignment - vec - writeGlobal mvar mem' + ovrWithBackend $ \bak -> do + mem <- readGlobal mvar + unless (V.length vec == 16) $ + liftIO $ addFailedAssertion bak $ AssertFailureSimError + ("Vector length mismatch in stored_qu intrinsic.") + (unwords ["Expected <16 x i8>, but got vector of length", show (V.length vec)]) + mem' <- liftIO $ doStore + bak + mem + dest + (VectorRepr (KnownBV @8)) + (arrayType 16 (bitvectorType (Bytes 1))) + noAlignment + vec + writeGlobal mvar mem' -- Excerpt from the LLVM documentation: @@ -1180,83 +1192,83 @@ callStoreudq bak mvar -- at compile time, llvm.objectsize returns i32/i64 -1 or 0 (depending -- on the min argument). callObjectsize - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> NatRepr w -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callObjectsize bak _mvar w +callObjectsize _mvar w (regValue -> _ptr) - (regValue -> flag) = liftIO $ do - let sym = backendGetSym bak - -- Ignore the pointer value, and just return the value for unknown, as - -- defined by the documenatation. If an `objectsize` invocation survives - -- through compilation for us to see, that means the compiler could not - -- determine the value. - t <- bvIsNonzero sym flag - z <- bvLit sym w (BV.zero w) - n <- bvNotBits sym z -- NB: -1 is the boolean negation of zero - bvIte sym t z n + (regValue -> flag) = do + sym <- getSymInterface + liftIO $ do + -- Ignore the pointer value, and just return the value for unknown, as + -- defined by the documenatation. If an `objectsize` invocation survives + -- through compilation for us to see, that means the compiler could not + -- determine the value. + t <- bvIsNonzero sym flag + z <- bvLit sym w (BV.zero w) + n <- bvNotBits sym z -- NB: -1 is the boolean negation of zero + bvIte sym t z n callObjectsize_null - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> NatRepr w -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType 1) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callObjectsize_null bak mvar w ptr flag _nullUnknown = callObjectsize bak mvar w ptr flag +callObjectsize_null mvar w ptr flag _nullUnknown = callObjectsize mvar w ptr flag callObjectsize_null_dynamic - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> NatRepr w -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType 1) -> RegEntry sym (BVType 1) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callObjectsize_null_dynamic bak mvar w ptr flag _nullUnknown (regValue -> dynamic) = - do let sym = backendGetSym bak - liftIO $ - do notDynamic <- notPred sym =<< bvIsNonzero sym dynamic - assert bak notDynamic (AssertFailureSimError "llvm.objectsize called with `dynamic` set to `true`" "") - callObjectsize bak mvar w ptr flag +callObjectsize_null_dynamic mvar w ptr flag _nullUnknown (regValue -> dynamic) = + ovrWithBackend $ \bak -> do + let sym = backendGetSym bak + liftIO $ + do notDynamic <- notPred sym =<< bvIsNonzero sym dynamic + assert bak notDynamic (AssertFailureSimError "llvm.objectsize called with `dynamic` set to `true`" "") + callObjectsize mvar w ptr flag callCtlz - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callCtlz bak _mvar +callCtlz _mvar (regValue -> val) - (regValue -> isZeroUndef) = liftIO $ - do let sym = backendGetSym bak - isNonzero <- bvIsNonzero sym val - zeroOK <- notPred sym =<< bvIsNonzero sym isZeroUndef - p <- orPred sym isNonzero zeroOK - assert bak p (AssertFailureSimError "Ctlz called with disallowed zero value" "") - bvCountLeadingZeros sym val + (regValue -> isZeroUndef) = + ovrWithBackend $ \bak -> do + sym <- getSymInterface + liftIO $ do + isNonzero <- bvIsNonzero sym val + zeroOK <- notPred sym =<< bvIsNonzero sym isZeroUndef + p <- orPred sym isNonzero zeroOK + assert bak p (AssertFailureSimError "Ctlz called with disallowed zero value" "") + bvCountLeadingZeros sym val callFshl - :: (1 <= w, IsSymBackend sym bak) - => bak - -> NatRepr w + :: (1 <= w, IsSymInterface sym) + => NatRepr w -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callFshl bak w x y amt = liftIO $ - do LeqProof <- return (dblPosIsPos (leqProof (knownNat @1) w)) - Just LeqProof <- return (testLeq (addNat w (knownNat @1)) (addNat w w)) +callFshl w x y amt = + ovrWithBackend $ \bak -> liftIO $ do let sym = backendGetSym bak + LeqProof <- return (dblPosIsPos (leqProof (knownNat @1) w)) + Just LeqProof <- return (testLeq (addNat w (knownNat @1)) (addNat w w)) -- concatenate the values together xy <- bvConcat sym (regValue x) (regValue y) @@ -1271,204 +1283,207 @@ callFshl bak w x y amt = liftIO $ bvSelect sym w w z callFshr - :: (1 <= w, IsSymBackend sym bak) - => bak - -> NatRepr w + :: (1 <= w, IsSymInterface sym) + => NatRepr w -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callFshr bak w x y amt = liftIO $ - do LeqProof <- return (dblPosIsPos (leqProof (knownNat @1) w)) - LeqProof <- return (addPrefixIsLeq w w) - Just LeqProof <- return (testLeq (addNat w (knownNat @1)) (addNat w w)) - let sym = backendGetSym bak +callFshr w x y amt = + ovrWithBackend $ \bak -> liftIO $ do + LeqProof <- return (dblPosIsPos (leqProof (knownNat @1) w)) + LeqProof <- return (addPrefixIsLeq w w) + Just LeqProof <- return (testLeq (addNat w (knownNat @1)) (addNat w w)) + let sym = backendGetSym bak - -- concatenate the values together - xy <- bvConcat sym (regValue x) (regValue y) + -- concatenate the values together + xy <- bvConcat sym (regValue x) (regValue y) - -- The shift argument is treated as an unsigned amount modulo the element size of the arguments. - m <- bvLit sym w (BV.width w) - mamt <- bvUrem sym (regValue amt) m - mamt' <- bvZext sym (addNat w w) mamt + -- The shift argument is treated as an unsigned amount modulo the element size of the arguments. + m <- bvLit sym w (BV.width w) + mamt <- bvUrem sym (regValue amt) m + mamt' <- bvZext sym (addNat w w) mamt - -- shift right, select low bits - z <- bvLshr sym xy mamt' - bvSelect sym (knownNat @0) w z + -- shift right, select low bits + z <- bvLshr sym xy mamt' + bvSelect sym (knownNat @0) w z callSaddWithOverflow - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType (EmptyCtx ::> BVType w ::> BVType 1))) -callSaddWithOverflow bak _mvar +callSaddWithOverflow _mvar (regValue -> x) - (regValue -> y) = liftIO $ - do let sym = backendGetSym bak - (ov, z) <- addSignedOF sym x y - ov' <- predToBV sym ov (knownNat @1) - return (Empty :> RV z :> RV ov') + (regValue -> y) = + ovrWithBackend $ \bak -> liftIO $ do + let sym = backendGetSym bak + (ov, z) <- addSignedOF sym x y + ov' <- predToBV sym ov (knownNat @1) + return (Empty :> RV z :> RV ov') callUaddWithOverflow - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType (EmptyCtx ::> BVType w ::> BVType 1))) -callUaddWithOverflow bak _mvar +callUaddWithOverflow _mvar (regValue -> x) - (regValue -> y) = liftIO $ - do let sym = backendGetSym bak + (regValue -> y) = do + sym <- getSymInterface + liftIO $ do (ov, z) <- addUnsignedOF sym x y ov' <- predToBV sym ov (knownNat @1) return (Empty :> RV z :> RV ov') callUsubWithOverflow - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType (EmptyCtx ::> BVType w ::> BVType 1))) -callUsubWithOverflow bak _mvar +callUsubWithOverflow _mvar (regValue -> x) - (regValue -> y) = liftIO $ - do let sym = backendGetSym bak - (ov, z) <- subUnsignedOF sym x y - ov' <- predToBV sym ov (knownNat @1) - return (Empty :> RV z :> RV ov') + (regValue -> y) = do + sym <- getSymInterface + liftIO $ do + (ov, z) <- subUnsignedOF sym x y + ov' <- predToBV sym ov (knownNat @1) + return (Empty :> RV z :> RV ov') callSsubWithOverflow - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType (EmptyCtx ::> BVType w ::> BVType 1))) -callSsubWithOverflow bak _mvar +callSsubWithOverflow _mvar (regValue -> x) - (regValue -> y) = liftIO $ - do let sym = backendGetSym bak - (ov, z) <- subSignedOF sym x y - ov' <- predToBV sym ov (knownNat @1) - return (Empty :> RV z :> RV ov') + (regValue -> y) = do + sym <- getSymInterface + liftIO $ do + (ov, z) <- subSignedOF sym x y + ov' <- predToBV sym ov (knownNat @1) + return (Empty :> RV z :> RV ov') callSmulWithOverflow - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType (EmptyCtx ::> BVType w ::> BVType 1))) -callSmulWithOverflow bak _mvar +callSmulWithOverflow _mvar (regValue -> x) - (regValue -> y) = liftIO $ - do let sym = backendGetSym bak - (ov, z) <- mulSignedOF sym x y - ov' <- predToBV sym ov (knownNat @1) - return (Empty :> RV z :> RV ov') + (regValue -> y) = do + sym <- getSymInterface + liftIO $ do + (ov, z) <- mulSignedOF sym x y + ov' <- predToBV sym ov (knownNat @1) + return (Empty :> RV z :> RV ov') callUmulWithOverflow - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (StructType (EmptyCtx ::> BVType w ::> BVType 1))) -callUmulWithOverflow bak _mvar +callUmulWithOverflow _mvar (regValue -> x) - (regValue -> y) = liftIO $ - do let sym = backendGetSym bak - (ov, z) <- mulUnsignedOF sym x y - ov' <- predToBV sym ov (knownNat @1) - return (Empty :> RV z :> RV ov') + (regValue -> y) = do + sym <- getSymInterface + liftIO $ do + (ov, z) <- mulUnsignedOF sym x y + ov' <- predToBV sym ov (knownNat @1) + return (Empty :> RV z :> RV ov') callUmax - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callUmax bak _mvar (regValue -> x) (regValue -> y) = liftIO $ - do let sym = backendGetSym bak - xGtY <- bvUgt sym x y - bvIte sym xGtY x y +callUmax _mvar (regValue -> x) (regValue -> y) = do + sym <- getSymInterface + liftIO $ do + xGtY <- bvUgt sym x y + bvIte sym xGtY x y callUmin - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callUmin bak _mvar (regValue -> x) (regValue -> y) = liftIO $ - do let sym = backendGetSym bak - xLtY <- bvUlt sym x y - bvIte sym xLtY x y +callUmin _mvar (regValue -> x) (regValue -> y) = do + sym <- getSymInterface + liftIO $ do + xLtY <- bvUlt sym x y + bvIte sym xLtY x y callSmax - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callSmax bak _mvar (regValue -> x) (regValue -> y) = liftIO $ - do let sym = backendGetSym bak - xGtY <- bvSgt sym x y - bvIte sym xGtY x y +callSmax _mvar (regValue -> x) (regValue -> y) = do + sym <- getSymInterface + liftIO $ do + xGtY <- bvSgt sym x y + bvIte sym xGtY x y callSmin - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callSmin bak _mvar (regValue -> x) (regValue -> y) = liftIO $ - do let sym = backendGetSym bak - xLtY <- bvSlt sym x y - bvIte sym xLtY x y +callSmin _mvar (regValue -> x) (regValue -> y) = do + sym <- getSymInterface + liftIO $ do + xLtY <- bvSlt sym x y + bvIte sym xLtY x y callCttz - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callCttz bak _mvar +callCttz _mvar (regValue -> val) - (regValue -> isZeroUndef) = liftIO $ - do let sym = backendGetSym bak - isNonzero <- bvIsNonzero sym val - zeroOK <- notPred sym =<< bvIsNonzero sym isZeroUndef - p <- orPred sym isNonzero zeroOK - assert bak p (AssertFailureSimError "Cttz called with disallowed zero value" "") - bvCountTrailingZeros sym val + (regValue -> isZeroUndef) = + ovrWithBackend $ \bak -> do + let sym = backendGetSym bak + liftIO $ do + isNonzero <- bvIsNonzero sym val + zeroOK <- notPred sym =<< bvIsNonzero sym isZeroUndef + p <- orPred sym isNonzero zeroOK + assert bak p (AssertFailureSimError "Cttz called with disallowed zero value" "") + bvCountTrailingZeros sym val callCtpop - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callCtpop bak _mvar - (regValue -> val) = liftIO $ bvPopcount (backendGetSym bak) val +callCtpop _mvar + (regValue -> val) = do + sym <- getSymInterface + liftIO $ bvPopcount sym val callBitreverse - :: (1 <= w, IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: (1 <= w, IsSymInterface sym) + => GlobalVar Mem -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callBitreverse bak _mvar - (regValue -> val) = liftIO $ bvBitreverse (backendGetSym bak) val +callBitreverse _mvar + (regValue -> val) = do + sym <- getSymInterface + liftIO $ bvBitreverse sym val -- | Strictly speaking, this doesn't quite conform to the C99 description of -- @copysign@, since @copysign(NaN, -1.0)@ should return @NaN@ with a negative @@ -1476,21 +1491,21 @@ callBitreverse bak _mvar -- with different sign bits, however, so @copysign@ will always turn a @NaN@ -- argument into a positive, \"quiet\" @NaN@. callCopysign :: - forall fi p sym bak ext r args ret. - (IsSymBackend sym bak) => - bak -> + forall fi p sym ext r args ret. + IsSymInterface sym => RegEntry sym (FloatType fi) -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) -callCopysign bak +callCopysign (regValue -> x) - (regValue -> y) = liftIO $ do - let sym = backendGetSym bak - xIsNeg <- iFloatIsNeg @_ @fi sym x - yIsNeg <- iFloatIsNeg @_ @fi sym y - signsSame <- eqPred sym xIsNeg yIsNeg - xNegated <- iFloatNeg @_ @fi sym x - iFloatIte @_ @fi sym signsSame x xNegated + (regValue -> y) = do + sym <- getSymInterface + liftIO $ do + xIsNeg <- iFloatIsNeg @_ @fi sym x + yIsNeg <- iFloatIsNeg @_ @fi sym y + signsSame <- eqPred sym xIsNeg yIsNeg + xNegated <- iFloatNeg @_ @fi sym x + iFloatIte @_ @fi sym signsSame x xNegated -- | An implementation of the @llvm.is.fpclass@ intrinsic. This essentially -- combines several different floating-point checks (checking for @NaN@, @@ -1505,13 +1520,14 @@ callCopysign bak -- @NaN@ checks will always return true in this implementation, regardless of -- whether they are signaling or quiet @NaN@s. callIsFpclass :: - forall fi p sym bak ext r args ret. - IsSymBackend sym bak => - bak -> + forall fi p sym ext r args ret. + IsSymInterface sym => RegEntry sym (FloatType fi) -> RegEntry sym (BVType 32) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 1)) -callIsFpclass bak regOp@(regValue -> op) (regValue -> test) = do +callIsFpclass regOp@(regValue -> op) (regValue -> test) = do + sym <- getSymInterface + let w1 = knownNat @1 bvOne <- liftIO $ bvLit sym w1 (BV.one w1) bvZero <- liftIO $ bvLit sym w1 (BV.zero w1) @@ -1545,7 +1561,7 @@ callIsFpclass bak regOp@(regValue -> op) (regValue -> test) = do is0 <- iFloatIsZero @_ @fi sym x bvIte sym is0 bvOne bvZero - isNan <- Libc.callIsnan bak w1 regOp + isNan <- Libc.callIsnan w1 regOp (isInfN, isInfP) <- negAndPos $ callIsInf op (isNormN, isNormP) <- negAndPos $ callIsNormal op (isSubnormN, isSubnormP) <- negAndPos $ callIsSubnormal op @@ -1568,6 +1584,3 @@ callIsFpclass bak regOp@(regValue -> op) (regValue -> test) = do , (8, isNormP) -- Positive normal , (9, isInfP) -- Positive infinity ] - where - sym = backendGetSym bak - w1 = knownNat @1 diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs index 7e0d11c97..95aab3a4f 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs @@ -85,9 +85,10 @@ llvmMemcpyOverride (LLVMPointerType wptr) llvmMemcpyOverride = [llvmOvr| i8* @memcpy( i8*, i8*, size_t ) |] - (\memOps bak args -> - do volatile <- liftIO $ RegEntry knownRepr <$> bvLit (backendGetSym bak) knownNat (BV.zero knownNat) - Ctx.uncurryAssignment (callMemcpy bak memOps) + (\memOps _bak args -> + do sym <- getSymInterface + volatile <- liftIO $ RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat) + Ctx.uncurryAssignment (callMemcpy memOps) (args :> volatile) return $ regValue $ args^._1 -- return first argument ) @@ -104,10 +105,11 @@ llvmMemcpyChkOverride (LLVMPointerType wptr) llvmMemcpyChkOverride = [llvmOvr| i8* @__memcpy_chk ( i8*, i8*, size_t, size_t ) |] - (\memOps bak args -> + (\memOps _bak args -> do let args' = Empty :> (args^._1) :> (args^._2) :> (args^._3) - volatile <- liftIO $ RegEntry knownRepr <$> bvLit (backendGetSym bak) knownNat (BV.zero knownNat) - Ctx.uncurryAssignment (callMemcpy bak memOps) + sym <- getSymInterface + volatile <- liftIO $ RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat) + Ctx.uncurryAssignment (callMemcpy memOps) (args' :> volatile) return $ regValue $ args^._1 -- return first argument ) @@ -122,9 +124,10 @@ llvmMemmoveOverride (LLVMPointerType wptr) llvmMemmoveOverride = [llvmOvr| i8* @memmove( i8*, i8*, size_t ) |] - (\memOps bak args -> - do volatile <- liftIO (RegEntry knownRepr <$> bvLit (backendGetSym bak) knownNat (BV.zero knownNat)) - Ctx.uncurryAssignment (callMemmove bak memOps) + (\memOps _bak args -> + do sym <- getSymInterface + volatile <- liftIO (RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat)) + Ctx.uncurryAssignment (callMemmove memOps) (args :> volatile) return $ regValue $ args^._1 -- return first argument ) @@ -138,15 +141,15 @@ llvmMemsetOverride :: forall p sym ext wptr. (LLVMPointerType wptr) llvmMemsetOverride = [llvmOvr| i8* @memset( i8*, i32, size_t ) |] - (\memOps bak args -> - do let sym = backendGetSym bak + (\memOps _bak args -> + do sym <- getSymInterface LeqProof <- return (leqTrans @9 @16 @wptr LeqProof LeqProof) let dest = args^._1 val <- liftIO (RegEntry knownRepr <$> bvTrunc sym (knownNat @8) (regValue (args^._2))) let len = args^._3 volatile <- liftIO (RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat)) - callMemset bak memOps dest val len volatile + callMemset memOps dest val len volatile return (regValue dest) ) @@ -160,15 +163,15 @@ llvmMemsetChkOverride (LLVMPointerType wptr) llvmMemsetChkOverride = [llvmOvr| i8* @__memset_chk( i8*, i32, size_t, size_t ) |] - (\memOps bak args -> - do let sym = backendGetSym bak + (\memOps _bak args -> + do sym <- getSymInterface let dest = args^._1 val <- liftIO (RegEntry knownRepr <$> bvTrunc sym knownNat (regValue (args^._2))) let len = args^._3 volatile <- liftIO (RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat)) - callMemset bak memOps dest val len volatile + callMemset memOps dest val len volatile return (regValue dest) ) @@ -184,7 +187,7 @@ llvmCallocOverride llvmCallocOverride = let alignment = maxAlignment (llvmDataLayout ?lc) in [llvmOvr| i8* @calloc( size_t, size_t ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callCalloc bak memOps alignment) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callCalloc memOps alignment) args) llvmReallocOverride @@ -196,7 +199,7 @@ llvmReallocOverride llvmReallocOverride = let alignment = maxAlignment (llvmDataLayout ?lc) in [llvmOvr| i8* @realloc( i8*, size_t ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callRealloc bak memOps alignment) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callRealloc memOps alignment) args) llvmMallocOverride :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -207,7 +210,7 @@ llvmMallocOverride llvmMallocOverride = let alignment = maxAlignment (llvmDataLayout ?lc) in [llvmOvr| i8* @malloc( size_t ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callMalloc bak memOps alignment) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callMalloc memOps alignment) args) posixMemalignOverride :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -219,7 +222,7 @@ posixMemalignOverride :: (BVType 32) posixMemalignOverride = [llvmOvr| i32 @posix_memalign( i8**, size_t, size_t ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callPosixMemalign bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callPosixMemalign memOps) args) llvmFreeOverride @@ -229,7 +232,7 @@ llvmFreeOverride UnitType llvmFreeOverride = [llvmOvr| void @free( i8* ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callFree bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callFree memOps) args) ------------------------------------------------------------------------ -- *** Strings and I/O @@ -243,7 +246,7 @@ llvmPrintfOverride (BVType 32) llvmPrintfOverride = [llvmOvr| i32 @printf( i8*, ... ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callPrintf bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callPrintf memOps) args) llvmPrintfChkOverride :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -255,7 +258,7 @@ llvmPrintfChkOverride (BVType 32) llvmPrintfChkOverride = [llvmOvr| i32 @__printf_chk( i32, i8*, ... ) |] - (\memOps bak args -> Ctx.uncurryAssignment (\_flg -> callPrintf bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (\_flg -> callPrintf memOps) args) llvmPutCharOverride @@ -263,7 +266,7 @@ llvmPutCharOverride => LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32) llvmPutCharOverride = [llvmOvr| i32 @putchar( i32 ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callPutChar bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callPutChar memOps) args) llvmPutsOverride @@ -272,7 +275,7 @@ llvmPutsOverride => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType 32) llvmPutsOverride = [llvmOvr| i32 @puts( i8* ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callPuts bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callPuts memOps) args) llvmStrlenOverride :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -280,7 +283,7 @@ llvmStrlenOverride => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType wptr) llvmStrlenOverride = [llvmOvr| size_t @strlen( i8* ) |] - (\memOps bak args -> Ctx.uncurryAssignment (callStrlen bak memOps) args) + (\memOps _bak args -> Ctx.uncurryAssignment (callStrlen memOps) args) ------------------------------------------------------------------------ -- ** Implementations @@ -289,189 +292,188 @@ llvmStrlenOverride = -- *** Allocation callRealloc - :: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym + :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym , ?memOpts :: MemOptions ) - => bak - -> GlobalVar Mem + => GlobalVar Mem -> Alignment -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) -callRealloc bak mvar alignment (regValue -> ptr) (regValue -> sz) = - do let sym = backendGetSym bak - szZero <- liftIO (notPred sym =<< bvIsNonzero sym sz) - ptrNull <- liftIO (ptrIsNull sym PtrWidth ptr) - loc <- liftIO (plSourceLoc <$> getCurrentProgramLoc sym) - let displayString = " " ++ show loc - - symbolicBranches emptyRegMap - -- If the pointer is null, behave like malloc - [ ( ptrNull - , modifyGlobal mvar $ \mem -> liftIO $ doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment - , Nothing - ) - - -- If the size is zero, behave like malloc (of zero bytes) then free - , (szZero - , modifyGlobal mvar $ \mem -> liftIO $ - do (newp, mem1) <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment - mem2 <- doFree bak mem1 ptr - return (newp, mem2) - , Nothing - ) - - -- Otherwise, allocate a new region, memcopy `sz` bytes and free the old pointer - , (truePred sym - , modifyGlobal mvar $ \mem -> liftIO $ - do (newp, mem1) <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment - mem2 <- uncheckedMemcpy sym mem1 newp ptr sz - mem3 <- doFree bak mem2 ptr - return (newp, mem3) - , Nothing) - ] +callRealloc mvar alignment (regValue -> ptr) (regValue -> sz) = + ovrWithBackend $ \bak -> do + let sym = backendGetSym bak + szZero <- liftIO (notPred sym =<< bvIsNonzero sym sz) + ptrNull <- liftIO (ptrIsNull sym PtrWidth ptr) + loc <- liftIO (plSourceLoc <$> getCurrentProgramLoc sym) + let displayString = " " ++ show loc + + symbolicBranches emptyRegMap + -- If the pointer is null, behave like malloc + [ ( ptrNull + , modifyGlobal mvar $ \mem -> liftIO $ doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment + , Nothing + ) + + -- If the size is zero, behave like malloc (of zero bytes) then free + , (szZero + , modifyGlobal mvar $ \mem -> liftIO $ + do (newp, mem1) <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment + mem2 <- doFree bak mem1 ptr + return (newp, mem2) + , Nothing + ) + + -- Otherwise, allocate a new region, memcopy `sz` bytes and free the old pointer + , (truePred sym + , modifyGlobal mvar $ \mem -> liftIO $ + do (newp, mem1) <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment + mem2 <- uncheckedMemcpy sym mem1 newp ptr sz + mem3 <- doFree bak mem2 ptr + return (newp, mem3) + , Nothing) + ] callPosixMemalign - :: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr + :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr , ?lc :: TypeContext, ?memOpts :: MemOptions ) - => bak - -> GlobalVar Mem + => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) -callPosixMemalign bak mvar (regValue -> outPtr) (regValue -> align) (regValue -> sz) = - let sym = backendGetSym bak in - case asBV align of - Nothing -> fail $ unwords ["posix_memalign: alignment value must be concrete:", show (printSymExpr align)] - Just concrete_align -> - case toAlignment (toBytes (BV.asUnsigned concrete_align)) of - Nothing -> fail $ unwords ["posix_memalign: invalid alignment value:", show concrete_align] - Just a -> - let dl = llvmDataLayout ?lc in - modifyGlobal mvar $ \mem -> liftIO $ - do loc <- plSourceLoc <$> getCurrentProgramLoc sym - let displayString = " " ++ show loc - (p, mem') <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz a - mem'' <- storeRaw bak mem' outPtr (bitvectorType (dl^.ptrSize)) (dl^.ptrAlign) (ptrToPtrVal p) - z <- bvLit sym knownNat (BV.zero knownNat) - return (z, mem'') +callPosixMemalign mvar (regValue -> outPtr) (regValue -> align) (regValue -> sz) = + ovrWithBackend $ \bak -> + let sym = backendGetSym bak in + case asBV align of + Nothing -> fail $ unwords ["posix_memalign: alignment value must be concrete:", show (printSymExpr align)] + Just concrete_align -> + case toAlignment (toBytes (BV.asUnsigned concrete_align)) of + Nothing -> fail $ unwords ["posix_memalign: invalid alignment value:", show concrete_align] + Just a -> + let dl = llvmDataLayout ?lc in + modifyGlobal mvar $ \mem -> liftIO $ + do loc <- plSourceLoc <$> getCurrentProgramLoc sym + let displayString = " " ++ show loc + (p, mem') <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz a + mem'' <- storeRaw bak mem' outPtr (bitvectorType (dl^.ptrSize)) (dl^.ptrAlign) (ptrToPtrVal p) + z <- bvLit sym knownNat (BV.zero knownNat) + return (z, mem'') callMalloc - :: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr + :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr , ?memOpts :: MemOptions ) - => bak - -> GlobalVar Mem + => GlobalVar Mem -> Alignment -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) -callMalloc bak mvar alignment (regValue -> sz) = - modifyGlobal mvar $ \mem -> liftIO $ - do loc <- plSourceLoc <$> getCurrentProgramLoc (backendGetSym bak) - let displayString = " " ++ show loc - doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment +callMalloc mvar alignment (regValue -> sz) = + ovrWithBackend $ \bak -> + modifyGlobal mvar $ \mem -> liftIO $ + do loc <- plSourceLoc <$> getCurrentProgramLoc (backendGetSym bak) + let displayString = " " ++ show loc + doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment callCalloc - :: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr + :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr , ?memOpts :: MemOptions ) - => bak - -> GlobalVar Mem + => GlobalVar Mem -> Alignment -> RegEntry sym (BVType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) -callCalloc bak mvar alignment +callCalloc mvar alignment (regValue -> sz) (regValue -> num) = - modifyGlobal mvar $ \mem -> liftIO $ - doCalloc bak mem sz num alignment + ovrWithBackend $ \bak -> + modifyGlobal mvar $ \mem -> liftIO $ + doCalloc bak mem sz num alignment callFree - :: (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr) - => bak - -> GlobalVar Mem + :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) + => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret () -callFree bak mvar +callFree mvar (regValue -> ptr) = - modifyGlobal mvar $ \mem -> liftIO $ - do mem' <- doFree bak mem ptr - return ((), mem') + ovrWithBackend $ \bak -> + modifyGlobal mvar $ \mem -> liftIO $ + do mem' <- doFree bak mem ptr + return ((), mem') ------------------------------------------------------------------------ -- *** Memory manipulation callMemcpy - :: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr + :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr , ?memOpts :: MemOptions ) - => bak - -> GlobalVar Mem + => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret () -callMemcpy bak mvar +callMemcpy mvar (regValue -> dest) (regValue -> src) (RegEntry (BVRepr w) len) _volatile = - modifyGlobal mvar $ \mem -> liftIO $ - do mem' <- doMemcpy bak w mem True dest src len - return ((), mem') + ovrWithBackend $ \bak -> + modifyGlobal mvar $ \mem -> liftIO $ + do mem' <- doMemcpy bak w mem True dest src len + return ((), mem') -- NB the only difference between memcpy and memove -- is that memmove does not assert that the memory -- ranges are disjoint. The underlying operation -- works correctly in both cases. callMemmove - :: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr + :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr , ?memOpts :: MemOptions ) - => bak - -> GlobalVar Mem + => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret () -callMemmove bak mvar +callMemmove mvar (regValue -> dest) (regValue -> src) (RegEntry (BVRepr w) len) _volatile = -- FIXME? add assertions about alignment - modifyGlobal mvar $ \mem -> liftIO $ - do mem' <- doMemcpy bak w mem False dest src len - return ((), mem') + ovrWithBackend $ \bak -> + modifyGlobal mvar $ \mem -> liftIO $ + do mem' <- doMemcpy bak w mem False dest src len + return ((), mem') callMemset - :: (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr) - => bak - -> GlobalVar Mem + :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) + => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType 8) -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret () -callMemset bak mvar +callMemset mvar (regValue -> dest) (regValue -> val) (RegEntry (BVRepr w) len) _volatile = - modifyGlobal mvar $ \mem -> liftIO $ - do mem' <- doMemset bak w mem dest val len - return ((), mem') + ovrWithBackend $ \bak -> + modifyGlobal mvar $ \mem -> liftIO $ + do mem' <- doMemset bak w mem dest val len + return ((), mem') ------------------------------------------------------------------------ -- *** Strings and I/O callPutChar - :: (IsSymBackend sym bak) - => bak - -> GlobalVar Mem + :: IsSymInterface sym + => GlobalVar Mem -> RegEntry sym (BVType 32) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) -callPutChar _bak _mvar +callPutChar _mvar (regValue -> ch) = do h <- printHandle <$> getContext let chval = maybe '?' (toEnum . fromInteger) (BV.asUnsigned <$> asBV ch) @@ -479,31 +481,31 @@ callPutChar _bak _mvar return ch callPuts - :: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym + :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym , ?memOpts :: MemOptions ) - => bak - -> GlobalVar Mem + => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) -callPuts bak mvar - (regValue -> strPtr) = do - mem <- readGlobal mvar - str <- liftIO $ loadString bak mem strPtr Nothing - h <- printHandle <$> getContext - liftIO $ hPutStrLn h (UTF8.toString str) - -- return non-negative value on success - liftIO $ bvLit (backendGetSym bak) knownNat (BV.one knownNat) +callPuts mvar + (regValue -> strPtr) = + ovrWithBackend $ \bak -> do + mem <- readGlobal mvar + str <- liftIO $ loadString bak mem strPtr Nothing + h <- printHandle <$> getContext + liftIO $ hPutStrLn h (UTF8.toString str) + -- return non-negative value on success + liftIO $ bvLit (backendGetSym bak) knownNat (BV.one knownNat) callStrlen - :: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym + :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym , ?memOpts :: MemOptions ) - => bak - -> GlobalVar Mem + => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)) -callStrlen bak mvar (regValue -> strPtr) = do - mem <- readGlobal mvar - liftIO $ strLen bak mem strPtr +callStrlen mvar (regValue -> strPtr) = + ovrWithBackend $ \bak -> do + mem <- readGlobal mvar + liftIO $ strLen bak mem strPtr callAssert :: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym @@ -548,26 +550,26 @@ callExit bak ec = liftIO $ abortExecBecause $ EarlyExit loc callPrintf - :: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym + :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym , ?memOpts :: MemOptions ) - => bak - -> GlobalVar Mem + => GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (VectorType AnyType) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) -callPrintf bak mvar +callPrintf mvar (regValue -> strPtr) - (regValue -> valist) = do - mem <- readGlobal mvar - formatStr <- liftIO $ loadString bak mem strPtr Nothing - case parseDirectives formatStr of - Left err -> overrideError $ AssertFailureSimError "Format string parsing failed" err - Right ds -> do - ((str, n), mem') <- liftIO $ runStateT (executeDirectives (printfOps bak valist) ds) mem - writeGlobal mvar mem' - h <- printHandle <$> getContext - liftIO $ BS.hPutStr h str - liftIO $ bvLit (backendGetSym bak) knownNat (BV.mkBV knownNat (toInteger n)) + (regValue -> valist) = + ovrWithBackend $ \bak -> do + mem <- readGlobal mvar + formatStr <- liftIO $ loadString bak mem strPtr Nothing + case parseDirectives formatStr of + Left err -> overrideError $ AssertFailureSimError "Format string parsing failed" err + Right ds -> do + ((str, n), mem') <- liftIO $ runStateT (executeDirectives (printfOps bak valist) ds) mem + writeGlobal mvar mem' + h <- printHandle <$> getContext + liftIO $ BS.hPutStr h str + liftIO $ bvLit (backendGetSym bak) knownNat (BV.mkBV knownNat (toInteger n)) printfOps :: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr , ?memOpts :: MemOptions ) @@ -703,7 +705,7 @@ llvmCeilOverride :: (FloatType DoubleFloat) llvmCeilOverride = [llvmOvr| double @ceil( double ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callCeil sym) args) + (\_memOps _bak args -> Ctx.uncurryAssignment callCeil args) llvmCeilfOverride :: IsSymInterface sym => @@ -712,7 +714,7 @@ llvmCeilfOverride :: (FloatType SingleFloat) llvmCeilfOverride = [llvmOvr| float @ceilf( float ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callCeil sym) args) + (\_memOps _bak args -> Ctx.uncurryAssignment callCeil args) llvmFloorOverride :: @@ -722,7 +724,7 @@ llvmFloorOverride :: (FloatType DoubleFloat) llvmFloorOverride = [llvmOvr| double @floor( double ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callFloor sym) args) + (\_memOps _bak args -> Ctx.uncurryAssignment callFloor args) llvmFloorfOverride :: IsSymInterface sym => @@ -731,7 +733,7 @@ llvmFloorfOverride :: (FloatType SingleFloat) llvmFloorfOverride = [llvmOvr| float @floorf( float ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callFloor sym) args) + (\_memOps _bak args -> Ctx.uncurryAssignment callFloor args) llvmFmafOverride :: forall sym p ext @@ -743,7 +745,7 @@ llvmFmafOverride :: (FloatType SingleFloat) llvmFmafOverride = [llvmOvr| float @fmaf( float, float, float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callFMA bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment callFMA args) llvmFmaOverride :: forall sym p ext @@ -755,7 +757,7 @@ llvmFmaOverride :: (FloatType DoubleFloat) llvmFmaOverride = [llvmOvr| double @fma( double, double, double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callFMA bak) args) + (\_memOps _bak args -> Ctx.uncurryAssignment callFMA args) -- math.h defines isinf() and isnan() as macros, so you might think it unusual @@ -776,7 +778,7 @@ llvmIsinfOverride :: (BVType 32) llvmIsinfOverride = [llvmOvr| i32 @isinf( double ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callIsinf sym (knownNat @32)) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args) -- __isinf and __isinff are like the isinf macro, except their arguments are -- known to be double or float, respectively. They are not mentioned in the @@ -790,7 +792,7 @@ llvm__isinfOverride :: (BVType 32) llvm__isinfOverride = [llvmOvr| i32 @__isinf( double ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callIsinf sym (knownNat @32)) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args) llvm__isinffOverride :: IsSymInterface sym => @@ -799,7 +801,7 @@ llvm__isinffOverride :: (BVType 32) llvm__isinffOverride = [llvmOvr| i32 @__isinff( float ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callIsinf sym (knownNat @32)) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args) llvmIsnanOverride :: IsSymInterface sym => @@ -808,7 +810,7 @@ llvmIsnanOverride :: (BVType 32) llvmIsnanOverride = [llvmOvr| i32 @isnan( double ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (knownNat @32)) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) -- __isnan and __isnanf are like the isnan macro, except their arguments are -- known to be double or float, respectively. They are not mentioned in the @@ -822,7 +824,7 @@ llvm__isnanOverride :: (BVType 32) llvm__isnanOverride = [llvmOvr| i32 @__isnan( double ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (knownNat @32)) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) llvm__isnanfOverride :: IsSymInterface sym => @@ -831,7 +833,7 @@ llvm__isnanfOverride :: (BVType 32) llvm__isnanfOverride = [llvmOvr| i32 @__isnanf( float ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (knownNat @32)) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) -- macOS compiles isnan() to __isnand() when the argument is a double. llvm__isnandOverride :: @@ -841,7 +843,7 @@ llvm__isnandOverride :: (BVType 32) llvm__isnandOverride = [llvmOvr| i32 @__isnand( double ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (knownNat @32)) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) llvmSqrtOverride :: IsSymInterface sym => @@ -850,7 +852,7 @@ llvmSqrtOverride :: (FloatType DoubleFloat) llvmSqrtOverride = [llvmOvr| double @sqrt( double ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callSqrt sym) args) + (\_memOps _bak args -> Ctx.uncurryAssignment callSqrt args) llvmSqrtfOverride :: IsSymInterface sym => @@ -859,103 +861,106 @@ llvmSqrtfOverride :: (FloatType SingleFloat) llvmSqrtfOverride = [llvmOvr| float @sqrtf( float ) |] - (\_memOps sym args -> Ctx.uncurryAssignment (callSqrt sym) args) + (\_memOps _bak args -> Ctx.uncurryAssignment callSqrt args) callSpecialFunction1 :: - forall fi p sym bak ext r args ret. - (IsSymBackend sym bak, KnownRepr FloatInfoRepr fi) => - bak -> + forall fi p sym ext r args ret. + (IsSymInterface sym, KnownRepr FloatInfoRepr fi) => W4.SpecialFunction (EmptyCtx ::> W4.R) -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) -callSpecialFunction1 bak fn (regValue -> x) = liftIO $ - iFloatSpecialFunction1 (backendGetSym bak) (knownRepr :: FloatInfoRepr fi) fn x +callSpecialFunction1 fn (regValue -> x) = do + sym <- getSymInterface + liftIO $ iFloatSpecialFunction1 sym (knownRepr :: FloatInfoRepr fi) fn x callSpecialFunction2 :: - forall fi p sym bak ext r args ret. - (IsSymBackend sym bak, KnownRepr FloatInfoRepr fi) => - bak -> + forall fi p sym ext r args ret. + (IsSymInterface sym, KnownRepr FloatInfoRepr fi) => W4.SpecialFunction (EmptyCtx ::> W4.R ::> W4.R) -> RegEntry sym (FloatType fi) -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) -callSpecialFunction2 bak fn (regValue -> x) (regValue -> y) = liftIO $ - iFloatSpecialFunction2 (backendGetSym bak) (knownRepr :: FloatInfoRepr fi) fn x y +callSpecialFunction2 fn (regValue -> x) (regValue -> y) = do + sym <- getSymInterface + liftIO $ iFloatSpecialFunction2 sym (knownRepr :: FloatInfoRepr fi) fn x y callCeil :: - forall fi p sym bak ext r args ret. - (IsSymBackend sym bak) => - bak -> + forall fi p sym ext r args ret. + IsSymInterface sym => RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) -callCeil bak (regValue -> x) = liftIO $ iFloatRound @_ @fi (backendGetSym bak) RTP x +callCeil (regValue -> x) = do + sym <- getSymInterface + liftIO $ iFloatRound @_ @fi sym RTP x callFloor :: - forall fi p sym bak ext r args ret. - (IsSymBackend sym bak) => - bak -> + forall fi p sym ext r args ret. + IsSymInterface sym => RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) -callFloor bak (regValue -> x) = liftIO $ iFloatRound @_ @fi (backendGetSym bak) RTN x +callFloor (regValue -> x) = do + sym <- getSymInterface + liftIO $ iFloatRound @_ @fi sym RTN x -- | An implementation of @libc@'s @fma@ function. callFMA :: - forall fi p sym bak ext r args ret - . IsSymBackend sym bak - => bak - -> RegEntry sym (FloatType fi) + forall fi p sym ext r args ret + . IsSymInterface sym + => RegEntry sym (FloatType fi) -> RegEntry sym (FloatType fi) -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) -callFMA bak (regValue -> x) (regValue -> y) (regValue -> z) = liftIO $ - iFloatFMA @_ @fi (backendGetSym bak) defaultRM x y z +callFMA (regValue -> x) (regValue -> y) (regValue -> z) = do + sym <- getSymInterface + liftIO $ iFloatFMA @_ @fi sym defaultRM x y z -- | An implementation of @libc@'s @isinf@ macro. This returns @1@ when the -- argument is positive infinity, @-1@ when the argument is negative infinity, -- and zero otherwise. callIsinf :: - forall fi w p sym bak ext r args ret. - (IsSymBackend sym bak, 1 <= w) => - bak -> + forall fi w p sym ext r args ret. + (IsSymInterface sym, 1 <= w) => NatRepr w -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callIsinf bak w (regValue -> x) = liftIO $ do - let sym = backendGetSym bak - isInf <- iFloatIsInf @_ @fi sym x - isNeg <- iFloatIsNeg @_ @fi sym x - isPos <- iFloatIsPos @_ @fi sym x - isInfN <- andPred sym isInf isNeg - isInfP <- andPred sym isInf isPos - bvOne <- bvLit sym w (BV.one w) - bvNegOne <- bvNeg sym bvOne - bvZero <- bvLit sym w (BV.zero w) - res0 <- bvIte sym isInfP bvOne bvZero - bvIte sym isInfN bvNegOne res0 +callIsinf w (regValue -> x) = do + sym <- getSymInterface + liftIO $ do + isInf <- iFloatIsInf @_ @fi sym x + isNeg <- iFloatIsNeg @_ @fi sym x + isPos <- iFloatIsPos @_ @fi sym x + isInfN <- andPred sym isInf isNeg + isInfP <- andPred sym isInf isPos + bvOne <- bvLit sym w (BV.one w) + bvNegOne <- bvNeg sym bvOne + bvZero <- bvLit sym w (BV.zero w) + res0 <- bvIte sym isInfP bvOne bvZero + bvIte sym isInfN bvNegOne res0 callIsnan :: - forall fi w p sym bak ext r args ret. - (IsSymBackend sym bak, 1 <= w) => - bak -> + forall fi w p sym ext r args ret. + (IsSymInterface sym, 1 <= w) => NatRepr w -> RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callIsnan bak w (regValue -> x) = liftIO $ do - let sym = backendGetSym bak - isnan <- iFloatIsNaN @_ @fi sym x - bvOne <- bvLit sym w (BV.one w) - bvZero <- bvLit sym w (BV.zero w) - -- isnan() is allowed to return any nonzero value if the argument is NaN, and - -- out of all the possible nonzero values, `1` is certainly one of them. - bvIte sym isnan bvOne bvZero +callIsnan w (regValue -> x) = do + sym <- getSymInterface + liftIO $ do + isnan <- iFloatIsNaN @_ @fi sym x + bvOne <- bvLit sym w (BV.one w) + bvZero <- bvLit sym w (BV.zero w) + -- isnan() is allowed to return any nonzero value if the argument is NaN, and + -- out of all the possible nonzero values, `1` is certainly one of them. + bvIte sym isnan bvOne bvZero callSqrt :: - forall fi p sym bak ext r args ret. - (IsSymBackend sym bak) => - bak -> + forall fi p sym ext r args ret. + IsSymInterface sym => RegEntry sym (FloatType fi) -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi)) -callSqrt bak (regValue -> x) = liftIO $ iFloatSqrt @_ @fi (backendGetSym bak) defaultRM x +callSqrt (regValue -> x) = do + sym <- getSymInterface + liftIO $ iFloatSqrt @_ @fi sym defaultRM x ------------------------------------------------------------------------ -- **** Circular trigonometry functions @@ -969,7 +974,7 @@ llvmSinOverride :: (FloatType DoubleFloat) llvmSinOverride = [llvmOvr| double @sin( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Sin) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args) llvmSinfOverride :: IsSymInterface sym => @@ -978,7 +983,7 @@ llvmSinfOverride :: (FloatType SingleFloat) llvmSinfOverride = [llvmOvr| float @sinf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Sin) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args) -- cos(f) @@ -989,7 +994,7 @@ llvmCosOverride :: (FloatType DoubleFloat) llvmCosOverride = [llvmOvr| double @cos( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Cos) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args) llvmCosfOverride :: IsSymInterface sym => @@ -998,7 +1003,7 @@ llvmCosfOverride :: (FloatType SingleFloat) llvmCosfOverride = [llvmOvr| float @cosf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Cos) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args) -- tan(f) @@ -1009,7 +1014,7 @@ llvmTanOverride :: (FloatType DoubleFloat) llvmTanOverride = [llvmOvr| double @tan( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Tan) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args) llvmTanfOverride :: IsSymInterface sym => @@ -1018,7 +1023,7 @@ llvmTanfOverride :: (FloatType SingleFloat) llvmTanfOverride = [llvmOvr| float @tanf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Tan) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args) -- asin(f) @@ -1029,7 +1034,7 @@ llvmAsinOverride :: (FloatType DoubleFloat) llvmAsinOverride = [llvmOvr| double @asin( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arcsin) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args) llvmAsinfOverride :: IsSymInterface sym => @@ -1038,7 +1043,7 @@ llvmAsinfOverride :: (FloatType SingleFloat) llvmAsinfOverride = [llvmOvr| float @asinf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arcsin) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args) -- acos(f) @@ -1049,7 +1054,7 @@ llvmAcosOverride :: (FloatType DoubleFloat) llvmAcosOverride = [llvmOvr| double @acos( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arccos) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args) llvmAcosfOverride :: IsSymInterface sym => @@ -1058,7 +1063,7 @@ llvmAcosfOverride :: (FloatType SingleFloat) llvmAcosfOverride = [llvmOvr| float @acosf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arccos) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args) -- atan(f) @@ -1069,7 +1074,7 @@ llvmAtanOverride :: (FloatType DoubleFloat) llvmAtanOverride = [llvmOvr| double @atan( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arctan) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args) llvmAtanfOverride :: IsSymInterface sym => @@ -1078,7 +1083,7 @@ llvmAtanfOverride :: (FloatType SingleFloat) llvmAtanfOverride = [llvmOvr| float @atanf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arctan) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args) ------------------------------------------------------------------------ -- **** Hyperbolic trigonometry functions @@ -1092,7 +1097,7 @@ llvmSinhOverride :: (FloatType DoubleFloat) llvmSinhOverride = [llvmOvr| double @sinh( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Sinh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args) llvmSinhfOverride :: IsSymInterface sym => @@ -1101,7 +1106,7 @@ llvmSinhfOverride :: (FloatType SingleFloat) llvmSinhfOverride = [llvmOvr| float @sinhf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Sinh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args) -- cosh(f) @@ -1112,7 +1117,7 @@ llvmCoshOverride :: (FloatType DoubleFloat) llvmCoshOverride = [llvmOvr| double @cosh( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Cosh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args) llvmCoshfOverride :: IsSymInterface sym => @@ -1121,7 +1126,7 @@ llvmCoshfOverride :: (FloatType SingleFloat) llvmCoshfOverride = [llvmOvr| float @coshf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Cosh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args) -- tanh(f) @@ -1132,7 +1137,7 @@ llvmTanhOverride :: (FloatType DoubleFloat) llvmTanhOverride = [llvmOvr| double @tanh( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Tanh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args) llvmTanhfOverride :: IsSymInterface sym => @@ -1141,7 +1146,7 @@ llvmTanhfOverride :: (FloatType SingleFloat) llvmTanhfOverride = [llvmOvr| float @tanhf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Tanh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args) -- asinh(f) @@ -1152,7 +1157,7 @@ llvmAsinhOverride :: (FloatType DoubleFloat) llvmAsinhOverride = [llvmOvr| double @asinh( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arcsinh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args) llvmAsinhfOverride :: IsSymInterface sym => @@ -1161,7 +1166,7 @@ llvmAsinhfOverride :: (FloatType SingleFloat) llvmAsinhfOverride = [llvmOvr| float @asinhf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arcsinh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args) -- acosh(f) @@ -1172,7 +1177,7 @@ llvmAcoshOverride :: (FloatType DoubleFloat) llvmAcoshOverride = [llvmOvr| double @acosh( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arccosh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args) llvmAcoshfOverride :: IsSymInterface sym => @@ -1181,7 +1186,7 @@ llvmAcoshfOverride :: (FloatType SingleFloat) llvmAcoshfOverride = [llvmOvr| float @acoshf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arccosh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args) -- atanh(f) @@ -1192,7 +1197,7 @@ llvmAtanhOverride :: (FloatType DoubleFloat) llvmAtanhOverride = [llvmOvr| double @atanh( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arctanh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args) llvmAtanhfOverride :: IsSymInterface sym => @@ -1201,7 +1206,7 @@ llvmAtanhfOverride :: (FloatType SingleFloat) llvmAtanhfOverride = [llvmOvr| float @atanhf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arctanh) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args) ------------------------------------------------------------------------ -- **** Rectangular to polar coordinate conversion @@ -1215,7 +1220,7 @@ llvmHypotOverride :: (FloatType DoubleFloat) llvmHypotOverride = [llvmOvr| double @hypot( double, double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Hypot) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args) llvmHypotfOverride :: IsSymInterface sym => @@ -1224,7 +1229,7 @@ llvmHypotfOverride :: (FloatType SingleFloat) llvmHypotfOverride = [llvmOvr| float @hypotf( float, float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Hypot) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args) -- atan2(f) @@ -1235,7 +1240,7 @@ llvmAtan2Override :: (FloatType DoubleFloat) llvmAtan2Override = [llvmOvr| double @atan2( double, double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Arctan2) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args) llvmAtan2fOverride :: IsSymInterface sym => @@ -1244,7 +1249,7 @@ llvmAtan2fOverride :: (FloatType SingleFloat) llvmAtan2fOverride = [llvmOvr| float @atan2f( float, float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Arctan2) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args) ------------------------------------------------------------------------ -- **** Exponential and logarithm functions @@ -1258,7 +1263,7 @@ llvmPowfOverride :: (FloatType SingleFloat) llvmPowfOverride = [llvmOvr| float @powf( float, float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Pow) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args) llvmPowOverride :: IsSymInterface sym => @@ -1267,7 +1272,7 @@ llvmPowOverride :: (FloatType DoubleFloat) llvmPowOverride = [llvmOvr| double @pow( double, double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Pow) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args) -- exp(f) @@ -1278,7 +1283,7 @@ llvmExpOverride :: (FloatType DoubleFloat) llvmExpOverride = [llvmOvr| double @exp( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args) llvmExpfOverride :: IsSymInterface sym => @@ -1287,7 +1292,7 @@ llvmExpfOverride :: (FloatType SingleFloat) llvmExpfOverride = [llvmOvr| float @expf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args) -- log(f) @@ -1298,7 +1303,7 @@ llvmLogOverride :: (FloatType DoubleFloat) llvmLogOverride = [llvmOvr| double @log( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args) llvmLogfOverride :: IsSymInterface sym => @@ -1307,7 +1312,7 @@ llvmLogfOverride :: (FloatType SingleFloat) llvmLogfOverride = [llvmOvr| float @logf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args) -- expm1(f) @@ -1318,7 +1323,7 @@ llvmExpm1Override :: (FloatType DoubleFloat) llvmExpm1Override = [llvmOvr| double @expm1( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Expm1) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args) llvmExpm1fOverride :: IsSymInterface sym => @@ -1327,7 +1332,7 @@ llvmExpm1fOverride :: (FloatType SingleFloat) llvmExpm1fOverride = [llvmOvr| float @expm1f( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Expm1) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args) -- log1p(f) @@ -1338,7 +1343,7 @@ llvmLog1pOverride :: (FloatType DoubleFloat) llvmLog1pOverride = [llvmOvr| double @log1p( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log1p) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args) llvmLog1pfOverride :: IsSymInterface sym => @@ -1347,7 +1352,7 @@ llvmLog1pfOverride :: (FloatType SingleFloat) llvmLog1pfOverride = [llvmOvr| float @log1pf( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log1p) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args) ------------------------------------------------------------------------ -- **** Base 2 exponential and logarithm @@ -1361,7 +1366,7 @@ llvmExp2Override :: (FloatType DoubleFloat) llvmExp2Override = [llvmOvr| double @exp2( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp2) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args) llvmExp2fOverride :: IsSymInterface sym => @@ -1370,7 +1375,7 @@ llvmExp2fOverride :: (FloatType SingleFloat) llvmExp2fOverride = [llvmOvr| float @exp2f( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp2) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args) -- log2(f) @@ -1381,7 +1386,7 @@ llvmLog2Override :: (FloatType DoubleFloat) llvmLog2Override = [llvmOvr| double @log2( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log2) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args) llvmLog2fOverride :: IsSymInterface sym => @@ -1390,7 +1395,7 @@ llvmLog2fOverride :: (FloatType SingleFloat) llvmLog2fOverride = [llvmOvr| float @log2f( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log2) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args) ------------------------------------------------------------------------ -- **** Base 10 exponential and logarithm @@ -1404,7 +1409,7 @@ llvmExp10Override :: (FloatType DoubleFloat) llvmExp10Override = [llvmOvr| double @exp10( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp10) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) llvmExp10fOverride :: IsSymInterface sym => @@ -1413,7 +1418,7 @@ llvmExp10fOverride :: (FloatType SingleFloat) llvmExp10fOverride = [llvmOvr| float @exp10f( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp10) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) -- macOS uses __exp10(f) instead of exp10(f). @@ -1424,7 +1429,7 @@ llvm__exp10Override :: (FloatType DoubleFloat) llvm__exp10Override = [llvmOvr| double @__exp10( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp10) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) llvm__exp10fOverride :: IsSymInterface sym => @@ -1433,7 +1438,7 @@ llvm__exp10fOverride :: (FloatType SingleFloat) llvm__exp10fOverride = [llvmOvr| float @__exp10f( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp10) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) -- log10(f) @@ -1444,7 +1449,7 @@ llvmLog10Override :: (FloatType DoubleFloat) llvmLog10Override = [llvmOvr| double @log10( double ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log10) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args) llvmLog10fOverride :: IsSymInterface sym => @@ -1453,7 +1458,7 @@ llvmLog10fOverride :: (FloatType SingleFloat) llvmLog10fOverride = [llvmOvr| float @log10f( float ) |] - (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log10) args) + (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args) ------------------------------------------------------------------------ -- *** Other @@ -1529,7 +1534,7 @@ llvmHtonlOverride :: (BVType 32) llvmHtonlOverride = [llvmOvr| i32 @htonl( i32 ) |] - (\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @4)) args) + (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args) llvmHtonsOverride :: (IsSymInterface sym, ?lc :: TypeContext) => @@ -1538,7 +1543,7 @@ llvmHtonsOverride :: (BVType 16) llvmHtonsOverride = [llvmOvr| i16 @htons( i16 ) |] - (\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @2)) args) + (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args) llvmNtohlOverride :: (IsSymInterface sym, ?lc :: TypeContext) => @@ -1547,7 +1552,7 @@ llvmNtohlOverride :: (BVType 32) llvmNtohlOverride = [llvmOvr| i32 @ntohl( i32 ) |] - (\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @4)) args) + (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args) llvmNtohsOverride :: (IsSymInterface sym, ?lc :: TypeContext) => @@ -1556,7 +1561,7 @@ llvmNtohsOverride :: (BVType 16) llvmNtohsOverride = [llvmOvr| i16 @ntohs( i16 ) |] - (\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @2)) args) + (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args) llvmAbsOverride :: (IsSymInterface sym, HasLLVMAnn sym) => @@ -1565,9 +1570,9 @@ llvmAbsOverride :: (BVType 32) llvmAbsOverride = [llvmOvr| i32 @abs( i32 ) |] - (\mvar bak args -> + (\mvar _bak args -> do callStack <- callStackFromMemVar' mvar - Ctx.uncurryAssignment (callLibcAbs bak callStack (knownNat @32)) args) + Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args) -- @labs@ uses `long` as its argument and result type, so we need two overrides -- for @labs@. See Note [Overrides involving (unsigned) long] in @@ -1579,9 +1584,9 @@ llvmLAbsOverride_32 :: (BVType 32) llvmLAbsOverride_32 = [llvmOvr| i32 @labs( i32 ) |] - (\mvar bak args -> + (\mvar _bak args -> do callStack <- callStackFromMemVar' mvar - Ctx.uncurryAssignment (callLibcAbs bak callStack (knownNat @32)) args) + Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args) llvmLAbsOverride_64 :: (IsSymInterface sym, HasLLVMAnn sym) => @@ -1590,9 +1595,9 @@ llvmLAbsOverride_64 :: (BVType 64) llvmLAbsOverride_64 = [llvmOvr| i64 @labs( i64 ) |] - (\mvar bak args -> + (\mvar _bak args -> do callStack <- callStackFromMemVar' mvar - Ctx.uncurryAssignment (callLibcAbs bak callStack (knownNat @64)) args) + Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) args) llvmLLAbsOverride :: (IsSymInterface sym, HasLLVMAnn sym) => @@ -1601,18 +1606,18 @@ llvmLLAbsOverride :: (BVType 64) llvmLLAbsOverride = [llvmOvr| i64 @llabs( i64 ) |] - (\mvar bak args -> + (\mvar _bak args -> do callStack <- callStackFromMemVar' mvar - Ctx.uncurryAssignment (callLibcAbs bak callStack (knownNat @64)) args) + Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) args) callBSwap :: - (1 <= width, IsSymBackend sym bak) => - bak -> + (1 <= width, IsSymInterface sym) => NatRepr width -> RegEntry sym (BVType (width * 8)) -> OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8))) -callBSwap bak widthRepr (regValue -> vec) = - liftIO $ bvSwap (backendGetSym bak) widthRepr vec +callBSwap widthRepr (regValue -> vec) = do + sym <- getSymInterface + liftIO $ bvSwap sym widthRepr vec -- | This determines under what circumstances @callAbs@ should check if its -- argument is equal to the smallest signed integer of a particular size @@ -1631,60 +1636,58 @@ data CheckAbsIntMin -- | The workhorse for the @abs@, @labs@, and @llabs@ functions, as well as the -- @llvm.abs.*@ family of overloaded intrinsics. callAbs :: - forall w p sym bak ext r args ret. - (1 <= w, IsSymBackend sym bak, HasLLVMAnn sym) => - bak -> + forall w p sym ext r args ret. + (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> CheckAbsIntMin -> NatRepr w -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callAbs bak callStack checkIntMin widthRepr (regValue -> src) = liftIO $ do - let sym = backendGetSym bak - bvIntMin <- bvLit sym widthRepr (BV.minSigned widthRepr) - isNotIntMin <- notPred sym =<< bvEq sym src bvIntMin - - when shouldCheckIntMin $ do - isNotIntMinUB <- annotateUB sym callStack ub isNotIntMin - let err = AssertFailureSimError "Undefined behavior encountered" $ - show $ UB.explain ub - assert bak isNotIntMinUB err - - isSrcNegative <- bvIsNeg sym src - srcNegated <- bvNeg sym src - bvIte sym isSrcNegative srcNegated src - where - shouldCheckIntMin :: Bool - shouldCheckIntMin = - case checkIntMin of - LibcAbsIntMinUB -> True - LLVMAbsIntMinPoison shouldCheck -> shouldCheck - - ub :: UB.UndefinedBehavior (RegValue' sym) - ub = case checkIntMin of - LibcAbsIntMinUB -> - UB.AbsIntMin $ RV src - LLVMAbsIntMinPoison{} -> - UB.PoisonValueCreated $ Poison.LLVMAbsIntMin $ RV src +callAbs callStack checkIntMin widthRepr (regValue -> src) = do + sym <- getSymInterface + ovrWithBackend $ \bak -> liftIO $ do + bvIntMin <- bvLit sym widthRepr (BV.minSigned widthRepr) + isNotIntMin <- notPred sym =<< bvEq sym src bvIntMin + + when shouldCheckIntMin $ do + isNotIntMinUB <- annotateUB sym callStack ub isNotIntMin + let err = AssertFailureSimError "Undefined behavior encountered" $ + show $ UB.explain ub + assert bak isNotIntMinUB err + + isSrcNegative <- bvIsNeg sym src + srcNegated <- bvNeg sym src + bvIte sym isSrcNegative srcNegated src + where + shouldCheckIntMin :: Bool + shouldCheckIntMin = + case checkIntMin of + LibcAbsIntMinUB -> True + LLVMAbsIntMinPoison shouldCheck -> shouldCheck + + ub :: UB.UndefinedBehavior (RegValue' sym) + ub = case checkIntMin of + LibcAbsIntMinUB -> + UB.AbsIntMin $ RV src + LLVMAbsIntMinPoison{} -> + UB.PoisonValueCreated $ Poison.LLVMAbsIntMin $ RV src callLibcAbs :: - (1 <= w, IsSymBackend sym bak, HasLLVMAnn sym) => - bak -> + (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> NatRepr w -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callLibcAbs bak callStack = callAbs bak callStack LibcAbsIntMinUB +callLibcAbs callStack = callAbs callStack LibcAbsIntMinUB callLLVMAbs :: - (1 <= w, IsSymBackend sym bak, HasLLVMAnn sym) => - bak -> + (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => CallStack -> NatRepr w -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callLLVMAbs bak callStack widthRepr src (regValue -> isIntMinPoison) = do +callLLVMAbs callStack widthRepr src (regValue -> isIntMinPoison) = do shouldCheckIntMin <- liftIO $ -- Per https://releases.llvm.org/12.0.0/docs/LangRef.html#id451, the second -- argument must be a constant. @@ -1693,21 +1696,20 @@ callLLVMAbs bak callStack widthRepr src (regValue -> isIntMinPoison) = do Nothing -> malformedLLVMModule "Call to llvm.abs.* with non-constant second argument" [printSymExpr isIntMinPoison] - callAbs bak callStack (LLVMAbsIntMinPoison shouldCheckIntMin) widthRepr src + callAbs callStack (LLVMAbsIntMinPoison shouldCheckIntMin) widthRepr src -- | If the data layout is little-endian, run 'callBSwap' on the input. -- Otherwise, return the input unchanged. This is the workhorse for the -- @hton{s,l}@ and @ntoh{s,l}@ overrides. callBSwapIfLittleEndian :: - (1 <= width, IsSymBackend sym bak, ?lc :: TypeContext) => - bak -> + (1 <= width, IsSymInterface sym, ?lc :: TypeContext) => NatRepr width -> RegEntry sym (BVType (width * 8)) -> OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8))) -callBSwapIfLittleEndian bak widthRepr vec = +callBSwapIfLittleEndian widthRepr vec = case (llvmDataLayout ?lc)^.intLayout of BigEndian -> pure (regValue vec) - LittleEndian -> callBSwap bak widthRepr vec + LittleEndian -> callBSwap widthRepr vec ---------------------------------------------------------------------------- -- atexit stuff From c05d84dc28fd69fd5afa157e628b6333043138fa Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 22 Mar 2024 15:45:37 -0400 Subject: [PATCH 2/3] crucible-llvm: Remove `bak` parameter from `LLVMOverride` definition This simplifies a bunch of signatures, allows for only retrieving the backend where it's needed via `ovrWithBackend`, and brings `LLVMOverride` closer to the more general `TypedOverride`. --- .../Lang/Crucible/LLVM/Intrinsics/Common.hs | 20 +- .../src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs | 194 +++++++------- .../src/Lang/Crucible/LLVM/Intrinsics/Libc.hs | 245 +++++++++--------- .../Lang/Crucible/LLVM/Intrinsics/Libcxx.hs | 12 +- crucible-llvm/src/Lang/Crucible/LLVM/SymIO.hs | 52 ++-- crux-llvm/src/Crux/LLVM/Overrides.hs | 217 ++++++++-------- .../src/UCCrux/LLVM/Overrides/Check.hs | 35 +-- .../src/UCCrux/LLVM/Overrides/Skip.hs | 4 +- .../src/UCCrux/LLVM/Overrides/Spec.hs | 2 +- .../src/UCCrux/LLVM/Overrides/Unsound.hs | 26 +- 10 files changed, 402 insertions(+), 405 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs index 3b53bd9cd..48858f501 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs @@ -93,13 +93,11 @@ data LLVMOverride p sym ext args ret = , llvmOverride_args :: CtxRepr args -- ^ A representation of the argument types , llvmOverride_ret :: TypeRepr ret -- ^ A representation of the return type , llvmOverride_def :: - forall bak. - IsSymBackend sym bak => - GlobalVar Mem -> - bak -> - Ctx.Assignment (RegEntry sym) args -> - forall rtp args' ret'. - OverrideSim p sym ext rtp args' ret' (RegValue sym ret) + IsSymInterface sym => + GlobalVar Mem -> + Ctx.Assignment (RegEntry sym) args -> + forall rtp args' ret'. + OverrideSim p sym ext rtp args' ret' (RegValue sym ret) -- ^ The implementation of the intrinsic in the simulator monad -- (@OverrideSim@). } @@ -279,8 +277,7 @@ build_llvm_override :: TypeRepr ret -> CtxRepr args' -> TypeRepr ret' -> - (forall bak rtp' l' a'. IsSymBackend sym bak => - bak -> + (forall rtp' l' a'. IsSymInterface sym => Ctx.Assignment (RegEntry sym) args -> OverrideSim p sym LLVM rtp' l' a' (RegValue sym ret)) -> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret') @@ -290,8 +287,7 @@ build_llvm_override fnm args ret args' ret' llvmOverride = fret <- transformLLVMRet fnm bak ret ret' return $ mkOverride' fnm ret' $ do RegMap xs <- getOverrideArgs - ovrWithBackend $ \bak' -> - applyValTransformer fret =<< llvmOverride bak' =<< applyArgTransformer fargs xs + applyValTransformer fret =<< llvmOverride =<< applyArgTransformer fargs xs polymorphic1_llvm_override :: forall p sym arch wptr l a rtp. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => @@ -452,7 +448,7 @@ do_register_llvm_override llvmctx llvmOverride = do llvmDeclToFunHandleRepr' decl $ \args ret -> do o <- build_llvm_override fnm overrideArgs overrideRet args ret - (\bak asgn -> llvmOverride_def llvmOverride mvar bak asgn) + (\asgn -> llvmOverride_def llvmOverride mvar asgn) bind_llvm_func llvmctx (L.decName decl) args ret (UseOverride o) -- | Create an allocation for an override and register it. diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs index 6fe9f5190..67eeb61e7 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs @@ -81,7 +81,7 @@ llvmLifetimeStartOverride => LLVMOverride p sym ext (EmptyCtx ::> BVType 64 ::> LLVMPointerType wptr) UnitType llvmLifetimeStartOverride = [llvmOvr| void @llvm.lifetime.start( i64, i8* ) |] - (\_ops _bak _args -> return ()) + (\_ops _args -> return ()) -- | See comment on 'llvmLifetimeStartOverride' -- @@ -91,7 +91,7 @@ llvmLifetimeEndOverride => LLVMOverride p sym ext (EmptyCtx ::> BVType 64 ::> LLVMPointerType wptr) UnitType llvmLifetimeEndOverride = [llvmOvr| void @llvm.lifetime.end( i64, i8* ) |] - (\_ops _bak _args -> return ()) + (\_ops _args -> return ()) -- | This is a no-op. -- @@ -108,7 +108,7 @@ llvmLifetimeOverrideOverload llvmLifetimeOverrideOverload startOrEnd w = let nm = L.Symbol ("llvm.lifetime." ++ startOrEnd ++ ".p0i" ++ show (widthVal w)) in [llvmOvr| void $nm ( i64, #w * ) |] - (\_ops _bak _args -> return ()) + (\_ops _args -> return ()) -- | Like 'llvmLifetimeOverrideOverload', but with an opaque pointer type. llvmLifetimeOverrideOverload_opaque @@ -121,7 +121,7 @@ llvmLifetimeOverrideOverload_opaque llvmLifetimeOverrideOverload_opaque startOrEnd = let nm = L.Symbol ("llvm.lifetime." ++ startOrEnd ++ ".p0") in [llvmOvr| void $nm ( i64, ptr ) |] - (\_ops _bak _args -> return ()) + (\_ops _args -> return ()) -- | This intrinsic is currently a no-op. -- @@ -138,7 +138,7 @@ llvmInvariantStartOverride llvmInvariantStartOverride w = let nm = L.Symbol ("llvm.invariant.start.p0i" ++ show (widthVal w)) in [llvmOvr| {}* $nm ( i64, #w * ) |] - (\_ops _bak _args -> mkNull) + (\_ops _args -> mkNull) -- | Like 'llvmInvariantStartOverride', but with an opaque pointer type. llvmInvariantStartOverride_opaque @@ -149,7 +149,7 @@ llvmInvariantStartOverride_opaque llvmInvariantStartOverride_opaque = let nm = L.Symbol "llvm.invariant.start.p0" in [llvmOvr| {}* $nm ( i64, ptr ) |] - (\_ops _bak _args -> mkNull) + (\_ops _args -> mkNull) -- | See comment on 'llvmInvariantStartOverride'. llvmInvariantEndOverride @@ -161,7 +161,7 @@ llvmInvariantEndOverride llvmInvariantEndOverride w = let nm = L.Symbol ("llvm.invariant.end.p0i" ++ show (widthVal w)) in [llvmOvr| void $nm ( {}*, i64, #w * ) |] - (\_ops _bak _args -> return ()) + (\_ops _args -> return ()) -- | See comment on 'llvmInvariantStartOverride_opaque'. llvmInvariantEndOverride_opaque @@ -172,7 +172,7 @@ llvmInvariantEndOverride_opaque llvmInvariantEndOverride_opaque = let nm = L.Symbol "llvm.invariant.end.p0" in [llvmOvr| void $nm ( {}*, i64, ptr ) |] - (\_ops _bak _args -> return ()) + (\_ops _args -> return ()) -- | This instruction is a hint to optimizers, it isn't really useful for us. -- @@ -187,7 +187,7 @@ llvmExpectOverride llvmExpectOverride w = let nm = L.Symbol ("llvm.expect.i" ++ show (widthVal w)) in [llvmOvr| #w $nm ( #w, #w ) |] - (\_ops _bak args -> + (\_ops args -> Ctx.uncurryAssignment (\val _ -> pure (regValue val)) args) -- | This intrinsic asserts that its argument is equal to 1. @@ -199,7 +199,7 @@ llvmAssumeOverride => LLVMOverride p sym ext (EmptyCtx ::> BVType 1) UnitType llvmAssumeOverride = [llvmOvr| void @llvm.assume ( i1 ) |] - (\_ops _bak _args -> return ()) + (\_ops _args -> return ()) -- | This intrinsic is sometimes inserted by clang, and we interpret it -- as an assertion failure, similar to calling @abort()@. @@ -208,7 +208,9 @@ llvmTrapOverride => LLVMOverride p sym ext EmptyCtx UnitType llvmTrapOverride = [llvmOvr| void @llvm.trap() |] - (\_ops bak _args -> liftIO $ addFailedAssertion bak $ AssertFailureSimError "llvm.trap() called" "") + (\_ops _args -> + ovrWithBackend $ \bak -> + liftIO $ addFailedAssertion bak $ AssertFailureSimError "llvm.trap() called" "") -- | This is like @llvm.trap()@, but with an argument indicating which sort of -- undefined behavior was trapped. The argument acts as an index into @@ -219,21 +221,23 @@ llvmUBSanTrapOverride :: LLVMOverride p sym ext (EmptyCtx ::> BVType 8) UnitType llvmUBSanTrapOverride = [llvmOvr| void @llvm.ubsantrap( i8 ) |] - (\_ops bak _args -> liftIO $ addFailedAssertion bak $ AssertFailureSimError "llvm.ubsantrap() called" "") + (\_ops _args -> + ovrWithBackend $ \bak -> + liftIO $ addFailedAssertion bak $ AssertFailureSimError "llvm.ubsantrap() called" "") llvmStacksave :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext EmptyCtx (LLVMPointerType wptr) llvmStacksave = [llvmOvr| i8* @llvm.stacksave() |] - (\_memOps _bak _args -> mkNull) + (\_memOps _args -> mkNull) llvmStackrestore :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType llvmStackrestore = [llvmOvr| void @llvm.stackrestore( i8* ) |] - (\_memOps _bak _args -> return ()) + (\_memOps _args -> return ()) llvmMemmoveOverride_8_8_32 :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -244,7 +248,7 @@ llvmMemmoveOverride_8_8_32 UnitType llvmMemmoveOverride_8_8_32 = [llvmOvr| void @llvm.memmove.p0i8.p0i8.i32( i8*, i8*, i32, i32, i1 ) |] - (\memOps _bak args -> + (\memOps args -> Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemmove memOps dst src len v) args) llvmMemmoveOverride_8_8_32_noalign @@ -256,7 +260,7 @@ llvmMemmoveOverride_8_8_32_noalign UnitType llvmMemmoveOverride_8_8_32_noalign = [llvmOvr| void @llvm.memmove.p0i8.p0i8.i32( i8*, i8*, i32, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemmove memOps) args) + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemmove memOps) args) llvmMemmoveOverride_8_8_32_noalign_opaque :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -267,7 +271,7 @@ llvmMemmoveOverride_8_8_32_noalign_opaque UnitType llvmMemmoveOverride_8_8_32_noalign_opaque = [llvmOvr| void @llvm.memmove.p0.p0.i32( ptr, ptr, i32, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemmove memOps) args) + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemmove memOps) args) llvmMemmoveOverride_8_8_64 @@ -279,7 +283,7 @@ llvmMemmoveOverride_8_8_64 UnitType llvmMemmoveOverride_8_8_64 = [llvmOvr| void @llvm.memmove.p0i8.p0i8.i64( i8*, i8*, i64, i32, i1 ) |] - (\memOps _bak args -> + (\memOps args -> Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemmove memOps dst src len v) args) llvmMemmoveOverride_8_8_64_noalign @@ -291,7 +295,7 @@ llvmMemmoveOverride_8_8_64_noalign UnitType llvmMemmoveOverride_8_8_64_noalign = [llvmOvr| void @llvm.memmove.p0i8.p0i8.i64( i8*, i8*, i64, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemmove memOps) args) + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemmove memOps) args) llvmMemmoveOverride_8_8_64_noalign_opaque :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -302,7 +306,7 @@ llvmMemmoveOverride_8_8_64_noalign_opaque UnitType llvmMemmoveOverride_8_8_64_noalign_opaque = [llvmOvr| void @llvm.memmove.p0.p0.i64( ptr, ptr, i64, i1 ) |] - (\memOps _bak args -> + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemmove memOps) args) @@ -317,7 +321,7 @@ llvmMemsetOverride_8_64 UnitType llvmMemsetOverride_8_64 = [llvmOvr| void @llvm.memset.p0i8.i64( i8*, i8, i64, i32, i1 ) |] - (\memOps _bak args -> + (\memOps args -> Ctx.uncurryAssignment (\dst val len _align v -> Libc.callMemset memOps dst val len v) args) llvmMemsetOverride_8_64_noalign @@ -330,7 +334,7 @@ llvmMemsetOverride_8_64_noalign UnitType llvmMemsetOverride_8_64_noalign = [llvmOvr| void @llvm.memset.p0i8.i64( i8*, i8, i64, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) llvmMemsetOverride_8_64_noalign_opaque :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) @@ -342,7 +346,7 @@ llvmMemsetOverride_8_64_noalign_opaque UnitType llvmMemsetOverride_8_64_noalign_opaque = [llvmOvr| void @llvm.memset.p0.i64( ptr, i8, i64, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) llvmMemsetOverride_8_32 @@ -356,7 +360,7 @@ llvmMemsetOverride_8_32 UnitType llvmMemsetOverride_8_32 = [llvmOvr| void @llvm.memset.p0i8.i32( i8*, i8, i32, i32, i1 ) |] - (\memOps _bak args -> + (\memOps args -> Ctx.uncurryAssignment (\dst val len _align v -> Libc.callMemset memOps dst val len v) args) llvmMemsetOverride_8_32_noalign @@ -369,7 +373,7 @@ llvmMemsetOverride_8_32_noalign UnitType llvmMemsetOverride_8_32_noalign = [llvmOvr| void @llvm.memset.p0i8.i32( i8*, i8, i32, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) llvmMemsetOverride_8_32_noalign_opaque :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) @@ -381,7 +385,7 @@ llvmMemsetOverride_8_32_noalign_opaque UnitType llvmMemsetOverride_8_32_noalign_opaque = [llvmOvr| void @llvm.memset.p0.i32( ptr, i8, i32, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemset memOps) args) llvmMemcpyOverride_8_8_32 @@ -393,7 +397,7 @@ llvmMemcpyOverride_8_8_32 UnitType llvmMemcpyOverride_8_8_32 = [llvmOvr| void @llvm.memcpy.p0i8.p0i8.i32( i8*, i8*, i32, i32, i1 ) |] - (\memOps _bak args -> + (\memOps args -> Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemcpy memOps dst src len v) args) llvmMemcpyOverride_8_8_32_noalign @@ -405,7 +409,7 @@ llvmMemcpyOverride_8_8_32_noalign UnitType llvmMemcpyOverride_8_8_32_noalign = [llvmOvr| void @llvm.memcpy.p0i8.p0i8.i32( i8*, i8*, i32, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) llvmMemcpyOverride_8_8_32_noalign_opaque :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -416,7 +420,7 @@ llvmMemcpyOverride_8_8_32_noalign_opaque UnitType llvmMemcpyOverride_8_8_32_noalign_opaque = [llvmOvr| void @llvm.memcpy.p0.p0.i32( ptr, ptr, i32, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) llvmMemcpyOverride_8_8_64 @@ -428,7 +432,7 @@ llvmMemcpyOverride_8_8_64 UnitType llvmMemcpyOverride_8_8_64 = [llvmOvr| void @llvm.memcpy.p0i8.p0i8.i64( i8*, i8*, i64, i32, i1 ) |] - (\memOps _bak args -> + (\memOps args -> Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemcpy memOps dst src len v) args) llvmMemcpyOverride_8_8_64_noalign @@ -440,7 +444,7 @@ llvmMemcpyOverride_8_8_64_noalign UnitType llvmMemcpyOverride_8_8_64_noalign = [llvmOvr| void @llvm.memcpy.p0i8.p0i8.i64( i8*, i8*, i64, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) llvmMemcpyOverride_8_8_64_noalign_opaque :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -451,7 +455,7 @@ llvmMemcpyOverride_8_8_64_noalign_opaque UnitType llvmMemcpyOverride_8_8_64_noalign_opaque = [llvmOvr| void @llvm.memcpy.p0.p0.i64( ptr, ptr, i64, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) + (\memOps args -> Ctx.uncurryAssignment (Libc.callMemcpy memOps) args) llvmObjectsizeOverride_32 @@ -459,56 +463,56 @@ llvmObjectsizeOverride_32 => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1) (BVType 32) llvmObjectsizeOverride_32 = [llvmOvr| i32 @llvm.objectsize.i32.p0i8( i8*, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize memOps knownNat) args) + (\memOps args -> Ctx.uncurryAssignment (callObjectsize memOps knownNat) args) llvmObjectsizeOverride_32_null :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1) (BVType 32) llvmObjectsizeOverride_32_null = [llvmOvr| i32 @llvm.objectsize.i32.p0i8( i8*, i1, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null memOps knownNat) args) + (\memOps args -> Ctx.uncurryAssignment (callObjectsize_null memOps knownNat) args) llvmObjectsizeOverride_32_null_dynamic :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1 ::> BVType 1) (BVType 32) llvmObjectsizeOverride_32_null_dynamic = [llvmOvr| i32 @llvm.objectsize.i32.p0i8( i8*, i1, i1, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) + (\memOps args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) llvmObjectsizeOverride_32_null_dynamic_opaque :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1 ::> BVType 1) (BVType 32) llvmObjectsizeOverride_32_null_dynamic_opaque = [llvmOvr| i32 @llvm.objectsize.i32.p0( ptr, i1, i1, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) + (\memOps args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) llvmObjectsizeOverride_64 :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1) (BVType 64) llvmObjectsizeOverride_64 = [llvmOvr| i64 @llvm.objectsize.i64.p0i8( i8*, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize memOps knownNat) args) + (\memOps args -> Ctx.uncurryAssignment (callObjectsize memOps knownNat) args) llvmObjectsizeOverride_64_null :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1) (BVType 64) llvmObjectsizeOverride_64_null = [llvmOvr| i64 @llvm.objectsize.i64.p0i8( i8*, i1, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null memOps knownNat) args) + (\memOps args -> Ctx.uncurryAssignment (callObjectsize_null memOps knownNat) args) llvmObjectsizeOverride_64_null_dynamic :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1 ::> BVType 1) (BVType 64) llvmObjectsizeOverride_64_null_dynamic = [llvmOvr| i64 @llvm.objectsize.i64.p0i8( i8*, i1, i1, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) + (\memOps args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) llvmObjectsizeOverride_64_null_dynamic_opaque :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType 1 ::> BVType 1 ::> BVType 1) (BVType 64) llvmObjectsizeOverride_64_null_dynamic_opaque = [llvmOvr| i64 @llvm.objectsize.i64.p0( ptr, i1, i1, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) + (\memOps args -> Ctx.uncurryAssignment (callObjectsize_null_dynamic memOps knownNat) args) -- | This instruction is a hint to code generators, which means that it is a -- no-op for us. @@ -521,7 +525,7 @@ llvmPrefetchOverride :: UnitType llvmPrefetchOverride = [llvmOvr| void @llvm.prefetch.p0i8( i8*, i32, i32, i32 ) |] - (\_memOps _bak _args -> pure ()) + (\_memOps _args -> pure ()) -- | Like 'llvmPrefetchOverride', but with an opaque pointer type. llvmPrefetchOverride_opaque :: @@ -531,7 +535,7 @@ llvmPrefetchOverride_opaque :: UnitType llvmPrefetchOverride_opaque = [llvmOvr| void @llvm.prefetch.p0( ptr, i32, i32, i32 ) |] - (\_memOps _bak _args -> pure ()) + (\_memOps _args -> pure ()) -- | This instruction is a hint to code generators, which means that it is a -- no-op for us. @@ -548,7 +552,7 @@ llvmPrefetchOverride_preLLVM10 :: UnitType llvmPrefetchOverride_preLLVM10 = [llvmOvr| void @llvm.prefetch( i8*, i32, i32, i32 ) |] - (\_memOps _bak _args -> pure ()) + (\_memOps _args -> pure ()) llvmFshl :: (1 <= w, IsSymInterface sym) => @@ -559,7 +563,7 @@ llvmFshl :: llvmFshl w = let nm = L.Symbol ("llvm.fshl.i" ++ show (natValue w)) in [llvmOvr| #w $nm ( #w, #w, #w ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callFshl w) args) + (\_memOps args -> Ctx.uncurryAssignment (callFshl w) args) llvmFshr :: (1 <= w, IsSymInterface sym) => @@ -570,7 +574,7 @@ llvmFshr :: llvmFshr w = let nm = L.Symbol ("llvm.fshr.i" ++ show (natValue w)) in [llvmOvr| #w $nm ( #w, #w, #w ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callFshr w) args) + (\_memOps args -> Ctx.uncurryAssignment (callFshr w) args) llvmSaddWithOverflow :: (1 <= w, IsSymInterface sym) @@ -581,7 +585,7 @@ llvmSaddWithOverflow llvmSaddWithOverflow w = let nm = L.Symbol ("llvm.sadd.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callSaddWithOverflow memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callSaddWithOverflow memOps) args) llvmUaddWithOverflow :: (1 <= w, IsSymInterface sym) @@ -592,7 +596,7 @@ llvmUaddWithOverflow llvmUaddWithOverflow w = let nm = L.Symbol ("llvm.uadd.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callUaddWithOverflow memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callUaddWithOverflow memOps) args) llvmSsubWithOverflow @@ -604,7 +608,7 @@ llvmSsubWithOverflow llvmSsubWithOverflow w = let nm = L.Symbol ("llvm.ssub.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callSsubWithOverflow memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callSsubWithOverflow memOps) args) llvmUsubWithOverflow @@ -616,7 +620,7 @@ llvmUsubWithOverflow llvmUsubWithOverflow w = let nm = L.Symbol ("llvm.usub.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callUsubWithOverflow memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callUsubWithOverflow memOps) args) llvmSmulWithOverflow :: (1 <= w, IsSymInterface sym) @@ -627,7 +631,7 @@ llvmSmulWithOverflow llvmSmulWithOverflow w = let nm = L.Symbol ("llvm.smul.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callSmulWithOverflow memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callSmulWithOverflow memOps) args) llvmUmulWithOverflow :: (1 <= w, IsSymInterface sym) @@ -638,7 +642,7 @@ llvmUmulWithOverflow llvmUmulWithOverflow w = let nm = L.Symbol ("llvm.umul.with.overflow.i" ++ show (natValue w)) in [llvmOvr| { #w, i1 } $nm ( #w, #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callUmulWithOverflow memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callUmulWithOverflow memOps) args) llvmUmax :: (1 <= w, IsSymInterface sym) => @@ -649,7 +653,7 @@ llvmUmax :: llvmUmax w = let nm = L.Symbol ("llvm.umax.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callUmax memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callUmax memOps) args) llvmUmin :: (1 <= w, IsSymInterface sym) => @@ -660,7 +664,7 @@ llvmUmin :: llvmUmin w = let nm = L.Symbol ("llvm.umin.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callUmin memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callUmin memOps) args) llvmSmax :: (1 <= w, IsSymInterface sym) => @@ -671,7 +675,7 @@ llvmSmax :: llvmSmax w = let nm = L.Symbol ("llvm.smax.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callSmax memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callSmax memOps) args) llvmSmin :: (1 <= w, IsSymInterface sym) => @@ -682,7 +686,7 @@ llvmSmin :: llvmSmin w = let nm = L.Symbol ("llvm.smin.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callSmin memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callSmin memOps) args) llvmCtlz :: (1 <= w, IsSymInterface sym) @@ -693,7 +697,7 @@ llvmCtlz llvmCtlz w = let nm = L.Symbol ("llvm.ctlz.i" ++ show (natValue w)) in [llvmOvr| #w $nm ( #w, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callCtlz memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callCtlz memOps) args) llvmCttz :: (1 <= w, IsSymInterface sym) @@ -704,7 +708,7 @@ llvmCttz llvmCttz w = let nm = L.Symbol ("llvm.cttz.i" ++ show (natValue w)) in [llvmOvr| #w $nm ( #w, i1 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callCttz memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callCttz memOps) args) llvmCtpop :: (1 <= w, IsSymInterface sym) @@ -715,7 +719,7 @@ llvmCtpop llvmCtpop w = let nm = L.Symbol ("llvm.ctpop.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callCtpop memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callCtpop memOps) args) llvmBitreverse :: (1 <= w, IsSymInterface sym) @@ -726,7 +730,7 @@ llvmBitreverse llvmBitreverse w = let nm = L.Symbol ("llvm.bitreverse.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callBitreverse memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callBitreverse memOps) args) -- | llvmBSwapOverride @@ -747,7 +751,7 @@ llvmBSwapOverride widthRepr = -- From the LLVM docs: -- declare i16 @llvm.bswap.i16(i16 ) [llvmOvr| #width8 $nm( #width8 ) |] - (\_ _bak args -> Ctx.uncurryAssignment (Libc.callBSwap widthRepr) args) + (\_ args -> Ctx.uncurryAssignment (Libc.callBSwap widthRepr) args) }}} llvmAbsOverride :: @@ -759,7 +763,7 @@ llvmAbsOverride :: llvmAbsOverride w = let nm = L.Symbol ("llvm.abs.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, i1 ) |] - (\mvar _bak args -> + (\mvar args -> do callStack <- callStackFromMemVar' mvar Ctx.uncurryAssignment (Libc.callLLVMAbs callStack w) args) @@ -770,7 +774,7 @@ llvmCopysignOverride_F32 :: (FloatType SingleFloat) llvmCopysignOverride_F32 = [llvmOvr| float @llvm.copysign.f32( float, float ) |] - (\_memOpts _bak args -> Ctx.uncurryAssignment callCopysign args) + (\_memOps args -> Ctx.uncurryAssignment callCopysign args) llvmCopysignOverride_F64 :: IsSymInterface sym => @@ -779,7 +783,7 @@ llvmCopysignOverride_F64 :: (FloatType DoubleFloat) llvmCopysignOverride_F64 = [llvmOvr| double @llvm.copysign.f64( double, double ) |] - (\_memOpts _bak args -> Ctx.uncurryAssignment callCopysign args) + (\_memOps args -> Ctx.uncurryAssignment callCopysign args) llvmFabsF32 @@ -790,7 +794,7 @@ llvmFabsF32 (FloatType SingleFloat) llvmFabsF32 = [llvmOvr| float @llvm.fabs.f32( float ) |] - (\_memOps _bak (Empty :> (regValue -> x)) -> do + (\_memOps (Empty :> (regValue -> x)) -> do sym <- getSymInterface liftIO (iFloatAbs @_ @SingleFloat sym x)) @@ -803,7 +807,7 @@ llvmFabsF64 (FloatType DoubleFloat) llvmFabsF64 = [llvmOvr| double @llvm.fabs.f64( double ) |] - (\_memOps _bak (Empty :> (regValue -> x)) -> do + (\_memOps (Empty :> (regValue -> x)) -> do sym <- getSymInterface liftIO (iFloatAbs @_ @DoubleFloat sym x)) @@ -814,7 +818,7 @@ llvmCeilOverride_F32 :: (FloatType SingleFloat) llvmCeilOverride_F32 = [llvmOvr| float @llvm.ceil.f32( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callCeil args) + (\_memOps args -> Ctx.uncurryAssignment Libc.callCeil args) llvmCeilOverride_F64 :: IsSymInterface sym => @@ -823,7 +827,7 @@ llvmCeilOverride_F64 :: (FloatType DoubleFloat) llvmCeilOverride_F64 = [llvmOvr| double @llvm.ceil.f64( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callCeil args) + (\_memOps args -> Ctx.uncurryAssignment Libc.callCeil args) llvmFloorOverride_F32 :: IsSymInterface sym => @@ -832,7 +836,7 @@ llvmFloorOverride_F32 :: (FloatType SingleFloat) llvmFloorOverride_F32 = [llvmOvr| float @llvm.floor.f32( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFloor args) + (\_memOps args -> Ctx.uncurryAssignment Libc.callFloor args) llvmFloorOverride_F64 :: IsSymInterface sym => @@ -841,7 +845,7 @@ llvmFloorOverride_F64 :: (FloatType DoubleFloat) llvmFloorOverride_F64 = [llvmOvr| double @llvm.floor.f64( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFloor args) + (\_memOps args -> Ctx.uncurryAssignment Libc.callFloor args) llvmSqrtOverride_F32 :: IsSymInterface sym => @@ -850,7 +854,7 @@ llvmSqrtOverride_F32 :: (FloatType SingleFloat) llvmSqrtOverride_F32 = [llvmOvr| float @llvm.sqrt.f32( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callSqrt args) + (\_memOps args -> Ctx.uncurryAssignment Libc.callSqrt args) llvmSqrtOverride_F64 :: IsSymInterface sym => @@ -859,7 +863,7 @@ llvmSqrtOverride_F64 :: (FloatType DoubleFloat) llvmSqrtOverride_F64 = [llvmOvr| double @llvm.sqrt.f64( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callSqrt args) + (\_memOps args -> Ctx.uncurryAssignment Libc.callSqrt args) llvmSinOverride_F32 :: IsSymInterface sym => @@ -868,7 +872,7 @@ llvmSinOverride_F32 :: (FloatType SingleFloat) llvmSinOverride_F32 = [llvmOvr| float @llvm.sin.f32( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sin) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sin) args) llvmSinOverride_F64 :: IsSymInterface sym => @@ -877,7 +881,7 @@ llvmSinOverride_F64 :: (FloatType DoubleFloat) llvmSinOverride_F64 = [llvmOvr| double @llvm.sin.f64( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sin) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sin) args) llvmCosOverride_F32 :: IsSymInterface sym => @@ -886,7 +890,7 @@ llvmCosOverride_F32 :: (FloatType SingleFloat) llvmCosOverride_F32 = [llvmOvr| float @llvm.cos.f32( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cos) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cos) args) llvmCosOverride_F64 :: IsSymInterface sym => @@ -895,7 +899,7 @@ llvmCosOverride_F64 :: (FloatType DoubleFloat) llvmCosOverride_F64 = [llvmOvr| double @llvm.cos.f64( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cos) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cos) args) llvmPowOverride_F32 :: IsSymInterface sym => @@ -904,7 +908,7 @@ llvmPowOverride_F32 :: (FloatType SingleFloat) llvmPowOverride_F32 = [llvmOvr| float @llvm.pow.f32( float, float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Pow) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Pow) args) llvmPowOverride_F64 :: IsSymInterface sym => @@ -913,7 +917,7 @@ llvmPowOverride_F64 :: (FloatType DoubleFloat) llvmPowOverride_F64 = [llvmOvr| double @llvm.pow.f64( double, double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Pow) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Pow) args) llvmExpOverride_F32 :: IsSymInterface sym => @@ -922,7 +926,7 @@ llvmExpOverride_F32 :: (FloatType SingleFloat) llvmExpOverride_F32 = [llvmOvr| float @llvm.exp.f32( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp) args) llvmExpOverride_F64 :: IsSymInterface sym => @@ -931,7 +935,7 @@ llvmExpOverride_F64 :: (FloatType DoubleFloat) llvmExpOverride_F64 = [llvmOvr| double @llvm.exp.f64( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp) args) llvmLogOverride_F32 :: IsSymInterface sym => @@ -940,7 +944,7 @@ llvmLogOverride_F32 :: (FloatType SingleFloat) llvmLogOverride_F32 = [llvmOvr| float @llvm.log.f32( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log) args) llvmLogOverride_F64 :: IsSymInterface sym => @@ -949,7 +953,7 @@ llvmLogOverride_F64 :: (FloatType DoubleFloat) llvmLogOverride_F64 = [llvmOvr| double @llvm.log.f64( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log) args) llvmExp2Override_F32 :: IsSymInterface sym => @@ -958,7 +962,7 @@ llvmExp2Override_F32 :: (FloatType SingleFloat) llvmExp2Override_F32 = [llvmOvr| float @llvm.exp2.f32( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp2) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp2) args) llvmExp2Override_F64 :: IsSymInterface sym => @@ -967,7 +971,7 @@ llvmExp2Override_F64 :: (FloatType DoubleFloat) llvmExp2Override_F64 = [llvmOvr| double @llvm.exp2.f64( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp2) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Exp2) args) llvmLog2Override_F32 :: IsSymInterface sym => @@ -976,7 +980,7 @@ llvmLog2Override_F32 :: (FloatType SingleFloat) llvmLog2Override_F32 = [llvmOvr| float @llvm.log2.f32( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log2) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log2) args) llvmLog2Override_F64 :: IsSymInterface sym => @@ -985,7 +989,7 @@ llvmLog2Override_F64 :: (FloatType DoubleFloat) llvmLog2Override_F64 = [llvmOvr| double @llvm.log2.f64( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log2) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log2) args) llvmLog10Override_F32 :: IsSymInterface sym => @@ -994,7 +998,7 @@ llvmLog10Override_F32 :: (FloatType SingleFloat) llvmLog10Override_F32 = [llvmOvr| float @llvm.log10.f32( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log10) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log10) args) llvmLog10Override_F64 :: IsSymInterface sym => @@ -1003,7 +1007,7 @@ llvmLog10Override_F64 :: (FloatType DoubleFloat) llvmLog10Override_F64 = [llvmOvr| double @llvm.log10.f64( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log10) args) + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Log10) args) llvmIsFpclassOverride_F32 :: IsSymInterface sym => @@ -1013,7 +1017,7 @@ llvmIsFpclassOverride_F32 :: (BVType 1) llvmIsFpclassOverride_F32 = [llvmOvr| i1 @llvm.is.fpclass.f32( float, i32 ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment callIsFpclass args) + (\_memOps args -> Ctx.uncurryAssignment callIsFpclass args) llvmIsFpclassOverride_F64 :: IsSymInterface sym => @@ -1023,7 +1027,7 @@ llvmIsFpclassOverride_F64 :: (BVType 1) llvmIsFpclassOverride_F64 = [llvmOvr| i1 @llvm.is.fpclass.f64( double, i32 ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment callIsFpclass args) + (\_memOps args -> Ctx.uncurryAssignment callIsFpclass args) llvmFmaOverride_F32 :: forall sym p ext @@ -1035,7 +1039,7 @@ llvmFmaOverride_F32 :: (FloatType SingleFloat) llvmFmaOverride_F32 = [llvmOvr| float @llvm.fma.f32( float, float, float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFMA args) + (\_memOps args -> Ctx.uncurryAssignment Libc.callFMA args) llvmFmaOverride_F64 :: forall sym p ext @@ -1047,7 +1051,7 @@ llvmFmaOverride_F64 :: (FloatType DoubleFloat) llvmFmaOverride_F64 = [llvmOvr| double @llvm.fma.f64( double, double, double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFMA args) + (\_memOps args -> Ctx.uncurryAssignment Libc.callFMA args) llvmFmuladdOverride_F32 :: forall sym p ext @@ -1059,7 +1063,7 @@ llvmFmuladdOverride_F32 :: (FloatType SingleFloat) llvmFmuladdOverride_F32 = [llvmOvr| float @llvm.fmuladd.f32( float, float, float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFMA args) + (\_memOps args -> Ctx.uncurryAssignment Libc.callFMA args) llvmFmuladdOverride_F64 :: forall sym p ext @@ -1071,7 +1075,7 @@ llvmFmuladdOverride_F64 :: (FloatType DoubleFloat) llvmFmuladdOverride_F64 = [llvmOvr| double @llvm.fmuladd.f64( double, double, double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment Libc.callFMA args) + (\_memOps args -> Ctx.uncurryAssignment Libc.callFMA args) llvmX86_pclmulqdq @@ -1084,7 +1088,7 @@ llvmX86_pclmulqdq (VectorType (BVType 64)) llvmX86_pclmulqdq = [llvmOvr| <2 x i64> @llvm.x86.pclmulqdq(<2 x i64>, <2 x i64>, i8) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callX86_pclmulqdq memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callX86_pclmulqdq memOps) args) llvmX86_SSE2_storeu_dq @@ -1098,7 +1102,7 @@ llvmX86_SSE2_storeu_dq UnitType llvmX86_SSE2_storeu_dq = [llvmOvr| void @llvm.x86.sse2.storeu.dq( i8*, <16 x i8> ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callStoreudq memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callStoreudq memOps) args) ------------------------------------------------------------------------ -- ** Implementations diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs index 95aab3a4f..bb61bb327 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs @@ -85,7 +85,7 @@ llvmMemcpyOverride (LLVMPointerType wptr) llvmMemcpyOverride = [llvmOvr| i8* @memcpy( i8*, i8*, size_t ) |] - (\memOps _bak args -> + (\memOps args -> do sym <- getSymInterface volatile <- liftIO $ RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat) Ctx.uncurryAssignment (callMemcpy memOps) @@ -105,7 +105,7 @@ llvmMemcpyChkOverride (LLVMPointerType wptr) llvmMemcpyChkOverride = [llvmOvr| i8* @__memcpy_chk ( i8*, i8*, size_t, size_t ) |] - (\memOps _bak args -> + (\memOps args -> do let args' = Empty :> (args^._1) :> (args^._2) :> (args^._3) sym <- getSymInterface volatile <- liftIO $ RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat) @@ -124,7 +124,7 @@ llvmMemmoveOverride (LLVMPointerType wptr) llvmMemmoveOverride = [llvmOvr| i8* @memmove( i8*, i8*, size_t ) |] - (\memOps _bak args -> + (\memOps args -> do sym <- getSymInterface volatile <- liftIO (RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat)) Ctx.uncurryAssignment (callMemmove memOps) @@ -141,7 +141,7 @@ llvmMemsetOverride :: forall p sym ext wptr. (LLVMPointerType wptr) llvmMemsetOverride = [llvmOvr| i8* @memset( i8*, i32, size_t ) |] - (\memOps _bak args -> + (\memOps args -> do sym <- getSymInterface LeqProof <- return (leqTrans @9 @16 @wptr LeqProof LeqProof) let dest = args^._1 @@ -163,7 +163,7 @@ llvmMemsetChkOverride (LLVMPointerType wptr) llvmMemsetChkOverride = [llvmOvr| i8* @__memset_chk( i8*, i32, size_t, size_t ) |] - (\memOps _bak args -> + (\memOps args -> do sym <- getSymInterface let dest = args^._1 val <- liftIO @@ -187,7 +187,7 @@ llvmCallocOverride llvmCallocOverride = let alignment = maxAlignment (llvmDataLayout ?lc) in [llvmOvr| i8* @calloc( size_t, size_t ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callCalloc memOps alignment) args) + (\memOps args -> Ctx.uncurryAssignment (callCalloc memOps alignment) args) llvmReallocOverride @@ -199,7 +199,7 @@ llvmReallocOverride llvmReallocOverride = let alignment = maxAlignment (llvmDataLayout ?lc) in [llvmOvr| i8* @realloc( i8*, size_t ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callRealloc memOps alignment) args) + (\memOps args -> Ctx.uncurryAssignment (callRealloc memOps alignment) args) llvmMallocOverride :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -210,7 +210,7 @@ llvmMallocOverride llvmMallocOverride = let alignment = maxAlignment (llvmDataLayout ?lc) in [llvmOvr| i8* @malloc( size_t ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callMalloc memOps alignment) args) + (\memOps args -> Ctx.uncurryAssignment (callMalloc memOps alignment) args) posixMemalignOverride :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -222,7 +222,7 @@ posixMemalignOverride :: (BVType 32) posixMemalignOverride = [llvmOvr| i32 @posix_memalign( i8**, size_t, size_t ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callPosixMemalign memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callPosixMemalign memOps) args) llvmFreeOverride @@ -232,7 +232,7 @@ llvmFreeOverride UnitType llvmFreeOverride = [llvmOvr| void @free( i8* ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callFree memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callFree memOps) args) ------------------------------------------------------------------------ -- *** Strings and I/O @@ -246,7 +246,7 @@ llvmPrintfOverride (BVType 32) llvmPrintfOverride = [llvmOvr| i32 @printf( i8*, ... ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callPrintf memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callPrintf memOps) args) llvmPrintfChkOverride :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -258,7 +258,7 @@ llvmPrintfChkOverride (BVType 32) llvmPrintfChkOverride = [llvmOvr| i32 @__printf_chk( i32, i8*, ... ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (\_flg -> callPrintf memOps) args) + (\memOps args -> Ctx.uncurryAssignment (\_flg -> callPrintf memOps) args) llvmPutCharOverride @@ -266,7 +266,7 @@ llvmPutCharOverride => LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32) llvmPutCharOverride = [llvmOvr| i32 @putchar( i32 ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callPutChar memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callPutChar memOps) args) llvmPutsOverride @@ -275,7 +275,7 @@ llvmPutsOverride => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType 32) llvmPutsOverride = [llvmOvr| i32 @puts( i8* ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callPuts memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callPuts memOps) args) llvmStrlenOverride :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr @@ -283,7 +283,7 @@ llvmStrlenOverride => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType wptr) llvmStrlenOverride = [llvmOvr| size_t @strlen( i8* ) |] - (\memOps _bak args -> Ctx.uncurryAssignment (callStrlen memOps) args) + (\memOps args -> Ctx.uncurryAssignment (callStrlen memOps) args) ------------------------------------------------------------------------ -- ** Implementations @@ -508,10 +508,9 @@ callStrlen mvar (regValue -> strPtr) = liftIO $ strLen bak mem strPtr callAssert - :: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym + :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) => GlobalVar Mem - -> bak -> Ctx.Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr @@ -519,35 +518,36 @@ callAssert ::> LLVMPointerType wptr) -> forall r args reg. OverrideSim p sym ext r args reg (RegValue sym UnitType) -callAssert mvar bak (Empty :> _pfn :> _pfile :> _pline :> ptxt ) = - do let sym = backendGetSym bak - when failUponExit $ - do mem <- readGlobal mvar - txt <- liftIO $ loadString bak mem (regValue ptxt) Nothing - let err = AssertFailureSimError "Call to assert()" (UTF8.toString txt) - liftIO $ addFailedAssertion bak err - liftIO $ - do loc <- liftIO $ getCurrentProgramLoc sym - abortExecBecause $ EarlyExit loc +callAssert mvar (Empty :> _pfn :> _pfile :> _pline :> ptxt ) = + ovrWithBackend $ \bak -> do + let sym = backendGetSym bak + when failUponExit $ + do mem <- readGlobal mvar + txt <- liftIO $ loadString bak mem (regValue ptxt) Nothing + let err = AssertFailureSimError "Call to assert()" (UTF8.toString txt) + liftIO $ addFailedAssertion bak err + liftIO $ + do loc <- liftIO $ getCurrentProgramLoc sym + abortExecBecause $ EarlyExit loc where failUponExit :: Bool failUponExit = abnormalExitBehavior ?intrinsicsOpts `elem` [AlwaysFail, OnlyAssertFail] -callExit :: ( IsSymBackend sym bak +callExit :: ( IsSymInterface sym , ?intrinsicsOpts :: IntrinsicsOptions ) - => bak - -> RegEntry sym (BVType 32) + => RegEntry sym (BVType 32) -> OverrideSim p sym ext r args ret (RegValue sym UnitType) -callExit bak ec = liftIO $ - do let sym = backendGetSym bak - when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $ - do cond <- bvEq sym (regValue ec) =<< bvLit sym knownNat (BV.zero knownNat) - -- If the argument is non-zero, throw an assertion failure. Otherwise, - -- simply stop the current thread of execution. - assert bak cond "Call to exit() with non-zero argument" - loc <- getCurrentProgramLoc sym - abortExecBecause $ EarlyExit loc +callExit ec = + ovrWithBackend $ \bak -> liftIO $ do + let sym = backendGetSym bak + when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $ + do cond <- bvEq sym (regValue ec) =<< bvLit sym knownNat (BV.zero knownNat) + -- If the argument is non-zero, throw an assertion failure. Otherwise, + -- simply stop the current thread of execution. + assert bak cond "Call to exit() with non-zero argument" + loc <- getCurrentProgramLoc sym + abortExecBecause $ EarlyExit loc callPrintf :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym @@ -705,7 +705,7 @@ llvmCeilOverride :: (FloatType DoubleFloat) llvmCeilOverride = [llvmOvr| double @ceil( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment callCeil args) + (\_memOps args -> Ctx.uncurryAssignment callCeil args) llvmCeilfOverride :: IsSymInterface sym => @@ -714,7 +714,7 @@ llvmCeilfOverride :: (FloatType SingleFloat) llvmCeilfOverride = [llvmOvr| float @ceilf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment callCeil args) + (\_memOps args -> Ctx.uncurryAssignment callCeil args) llvmFloorOverride :: @@ -724,7 +724,7 @@ llvmFloorOverride :: (FloatType DoubleFloat) llvmFloorOverride = [llvmOvr| double @floor( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment callFloor args) + (\_memOps args -> Ctx.uncurryAssignment callFloor args) llvmFloorfOverride :: IsSymInterface sym => @@ -733,7 +733,7 @@ llvmFloorfOverride :: (FloatType SingleFloat) llvmFloorfOverride = [llvmOvr| float @floorf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment callFloor args) + (\_memOps args -> Ctx.uncurryAssignment callFloor args) llvmFmafOverride :: forall sym p ext @@ -745,7 +745,7 @@ llvmFmafOverride :: (FloatType SingleFloat) llvmFmafOverride = [llvmOvr| float @fmaf( float, float, float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment callFMA args) + (\_memOps args -> Ctx.uncurryAssignment callFMA args) llvmFmaOverride :: forall sym p ext @@ -757,7 +757,7 @@ llvmFmaOverride :: (FloatType DoubleFloat) llvmFmaOverride = [llvmOvr| double @fma( double, double, double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment callFMA args) + (\_memOps args -> Ctx.uncurryAssignment callFMA args) -- math.h defines isinf() and isnan() as macros, so you might think it unusual @@ -778,7 +778,7 @@ llvmIsinfOverride :: (BVType 32) llvmIsinfOverride = [llvmOvr| i32 @isinf( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args) + (\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args) -- __isinf and __isinff are like the isinf macro, except their arguments are -- known to be double or float, respectively. They are not mentioned in the @@ -792,7 +792,7 @@ llvm__isinfOverride :: (BVType 32) llvm__isinfOverride = [llvmOvr| i32 @__isinf( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args) + (\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args) llvm__isinffOverride :: IsSymInterface sym => @@ -801,7 +801,7 @@ llvm__isinffOverride :: (BVType 32) llvm__isinffOverride = [llvmOvr| i32 @__isinff( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args) + (\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args) llvmIsnanOverride :: IsSymInterface sym => @@ -810,7 +810,7 @@ llvmIsnanOverride :: (BVType 32) llvmIsnanOverride = [llvmOvr| i32 @isnan( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) + (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) -- __isnan and __isnanf are like the isnan macro, except their arguments are -- known to be double or float, respectively. They are not mentioned in the @@ -824,7 +824,7 @@ llvm__isnanOverride :: (BVType 32) llvm__isnanOverride = [llvmOvr| i32 @__isnan( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) + (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) llvm__isnanfOverride :: IsSymInterface sym => @@ -833,7 +833,7 @@ llvm__isnanfOverride :: (BVType 32) llvm__isnanfOverride = [llvmOvr| i32 @__isnanf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) + (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) -- macOS compiles isnan() to __isnand() when the argument is a double. llvm__isnandOverride :: @@ -843,7 +843,7 @@ llvm__isnandOverride :: (BVType 32) llvm__isnandOverride = [llvmOvr| i32 @__isnand( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) + (\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args) llvmSqrtOverride :: IsSymInterface sym => @@ -852,7 +852,7 @@ llvmSqrtOverride :: (FloatType DoubleFloat) llvmSqrtOverride = [llvmOvr| double @sqrt( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment callSqrt args) + (\_memOps args -> Ctx.uncurryAssignment callSqrt args) llvmSqrtfOverride :: IsSymInterface sym => @@ -861,7 +861,7 @@ llvmSqrtfOverride :: (FloatType SingleFloat) llvmSqrtfOverride = [llvmOvr| float @sqrtf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment callSqrt args) + (\_memOps args -> Ctx.uncurryAssignment callSqrt args) callSpecialFunction1 :: forall fi p sym ext r args ret. @@ -974,7 +974,7 @@ llvmSinOverride :: (FloatType DoubleFloat) llvmSinOverride = [llvmOvr| double @sin( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args) llvmSinfOverride :: IsSymInterface sym => @@ -983,7 +983,7 @@ llvmSinfOverride :: (FloatType SingleFloat) llvmSinfOverride = [llvmOvr| float @sinf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args) -- cos(f) @@ -994,7 +994,7 @@ llvmCosOverride :: (FloatType DoubleFloat) llvmCosOverride = [llvmOvr| double @cos( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args) llvmCosfOverride :: IsSymInterface sym => @@ -1003,7 +1003,7 @@ llvmCosfOverride :: (FloatType SingleFloat) llvmCosfOverride = [llvmOvr| float @cosf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args) -- tan(f) @@ -1014,7 +1014,7 @@ llvmTanOverride :: (FloatType DoubleFloat) llvmTanOverride = [llvmOvr| double @tan( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args) llvmTanfOverride :: IsSymInterface sym => @@ -1023,7 +1023,7 @@ llvmTanfOverride :: (FloatType SingleFloat) llvmTanfOverride = [llvmOvr| float @tanf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args) -- asin(f) @@ -1034,7 +1034,7 @@ llvmAsinOverride :: (FloatType DoubleFloat) llvmAsinOverride = [llvmOvr| double @asin( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args) llvmAsinfOverride :: IsSymInterface sym => @@ -1043,7 +1043,7 @@ llvmAsinfOverride :: (FloatType SingleFloat) llvmAsinfOverride = [llvmOvr| float @asinf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args) -- acos(f) @@ -1054,7 +1054,7 @@ llvmAcosOverride :: (FloatType DoubleFloat) llvmAcosOverride = [llvmOvr| double @acos( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args) llvmAcosfOverride :: IsSymInterface sym => @@ -1063,7 +1063,7 @@ llvmAcosfOverride :: (FloatType SingleFloat) llvmAcosfOverride = [llvmOvr| float @acosf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args) -- atan(f) @@ -1074,7 +1074,7 @@ llvmAtanOverride :: (FloatType DoubleFloat) llvmAtanOverride = [llvmOvr| double @atan( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args) llvmAtanfOverride :: IsSymInterface sym => @@ -1083,7 +1083,7 @@ llvmAtanfOverride :: (FloatType SingleFloat) llvmAtanfOverride = [llvmOvr| float @atanf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args) ------------------------------------------------------------------------ -- **** Hyperbolic trigonometry functions @@ -1097,7 +1097,7 @@ llvmSinhOverride :: (FloatType DoubleFloat) llvmSinhOverride = [llvmOvr| double @sinh( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args) llvmSinhfOverride :: IsSymInterface sym => @@ -1106,7 +1106,7 @@ llvmSinhfOverride :: (FloatType SingleFloat) llvmSinhfOverride = [llvmOvr| float @sinhf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args) -- cosh(f) @@ -1117,7 +1117,7 @@ llvmCoshOverride :: (FloatType DoubleFloat) llvmCoshOverride = [llvmOvr| double @cosh( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args) llvmCoshfOverride :: IsSymInterface sym => @@ -1126,7 +1126,7 @@ llvmCoshfOverride :: (FloatType SingleFloat) llvmCoshfOverride = [llvmOvr| float @coshf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args) -- tanh(f) @@ -1137,7 +1137,7 @@ llvmTanhOverride :: (FloatType DoubleFloat) llvmTanhOverride = [llvmOvr| double @tanh( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args) llvmTanhfOverride :: IsSymInterface sym => @@ -1146,7 +1146,7 @@ llvmTanhfOverride :: (FloatType SingleFloat) llvmTanhfOverride = [llvmOvr| float @tanhf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args) -- asinh(f) @@ -1157,7 +1157,7 @@ llvmAsinhOverride :: (FloatType DoubleFloat) llvmAsinhOverride = [llvmOvr| double @asinh( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args) llvmAsinhfOverride :: IsSymInterface sym => @@ -1166,7 +1166,7 @@ llvmAsinhfOverride :: (FloatType SingleFloat) llvmAsinhfOverride = [llvmOvr| float @asinhf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args) -- acosh(f) @@ -1177,7 +1177,7 @@ llvmAcoshOverride :: (FloatType DoubleFloat) llvmAcoshOverride = [llvmOvr| double @acosh( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args) llvmAcoshfOverride :: IsSymInterface sym => @@ -1186,7 +1186,7 @@ llvmAcoshfOverride :: (FloatType SingleFloat) llvmAcoshfOverride = [llvmOvr| float @acoshf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args) -- atanh(f) @@ -1197,7 +1197,7 @@ llvmAtanhOverride :: (FloatType DoubleFloat) llvmAtanhOverride = [llvmOvr| double @atanh( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args) llvmAtanhfOverride :: IsSymInterface sym => @@ -1206,7 +1206,7 @@ llvmAtanhfOverride :: (FloatType SingleFloat) llvmAtanhfOverride = [llvmOvr| float @atanhf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args) ------------------------------------------------------------------------ -- **** Rectangular to polar coordinate conversion @@ -1220,7 +1220,7 @@ llvmHypotOverride :: (FloatType DoubleFloat) llvmHypotOverride = [llvmOvr| double @hypot( double, double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args) llvmHypotfOverride :: IsSymInterface sym => @@ -1229,7 +1229,7 @@ llvmHypotfOverride :: (FloatType SingleFloat) llvmHypotfOverride = [llvmOvr| float @hypotf( float, float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args) -- atan2(f) @@ -1240,7 +1240,7 @@ llvmAtan2Override :: (FloatType DoubleFloat) llvmAtan2Override = [llvmOvr| double @atan2( double, double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args) llvmAtan2fOverride :: IsSymInterface sym => @@ -1249,7 +1249,7 @@ llvmAtan2fOverride :: (FloatType SingleFloat) llvmAtan2fOverride = [llvmOvr| float @atan2f( float, float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args) ------------------------------------------------------------------------ -- **** Exponential and logarithm functions @@ -1263,7 +1263,7 @@ llvmPowfOverride :: (FloatType SingleFloat) llvmPowfOverride = [llvmOvr| float @powf( float, float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args) llvmPowOverride :: IsSymInterface sym => @@ -1272,7 +1272,7 @@ llvmPowOverride :: (FloatType DoubleFloat) llvmPowOverride = [llvmOvr| double @pow( double, double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args) -- exp(f) @@ -1283,7 +1283,7 @@ llvmExpOverride :: (FloatType DoubleFloat) llvmExpOverride = [llvmOvr| double @exp( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args) llvmExpfOverride :: IsSymInterface sym => @@ -1292,7 +1292,7 @@ llvmExpfOverride :: (FloatType SingleFloat) llvmExpfOverride = [llvmOvr| float @expf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args) -- log(f) @@ -1303,7 +1303,7 @@ llvmLogOverride :: (FloatType DoubleFloat) llvmLogOverride = [llvmOvr| double @log( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args) llvmLogfOverride :: IsSymInterface sym => @@ -1312,7 +1312,7 @@ llvmLogfOverride :: (FloatType SingleFloat) llvmLogfOverride = [llvmOvr| float @logf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args) -- expm1(f) @@ -1323,7 +1323,7 @@ llvmExpm1Override :: (FloatType DoubleFloat) llvmExpm1Override = [llvmOvr| double @expm1( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args) llvmExpm1fOverride :: IsSymInterface sym => @@ -1332,7 +1332,7 @@ llvmExpm1fOverride :: (FloatType SingleFloat) llvmExpm1fOverride = [llvmOvr| float @expm1f( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args) -- log1p(f) @@ -1343,7 +1343,7 @@ llvmLog1pOverride :: (FloatType DoubleFloat) llvmLog1pOverride = [llvmOvr| double @log1p( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args) llvmLog1pfOverride :: IsSymInterface sym => @@ -1352,7 +1352,7 @@ llvmLog1pfOverride :: (FloatType SingleFloat) llvmLog1pfOverride = [llvmOvr| float @log1pf( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args) ------------------------------------------------------------------------ -- **** Base 2 exponential and logarithm @@ -1366,7 +1366,7 @@ llvmExp2Override :: (FloatType DoubleFloat) llvmExp2Override = [llvmOvr| double @exp2( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args) llvmExp2fOverride :: IsSymInterface sym => @@ -1375,7 +1375,7 @@ llvmExp2fOverride :: (FloatType SingleFloat) llvmExp2fOverride = [llvmOvr| float @exp2f( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args) -- log2(f) @@ -1386,7 +1386,7 @@ llvmLog2Override :: (FloatType DoubleFloat) llvmLog2Override = [llvmOvr| double @log2( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args) llvmLog2fOverride :: IsSymInterface sym => @@ -1395,7 +1395,7 @@ llvmLog2fOverride :: (FloatType SingleFloat) llvmLog2fOverride = [llvmOvr| float @log2f( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args) ------------------------------------------------------------------------ -- **** Base 10 exponential and logarithm @@ -1409,7 +1409,7 @@ llvmExp10Override :: (FloatType DoubleFloat) llvmExp10Override = [llvmOvr| double @exp10( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) llvmExp10fOverride :: IsSymInterface sym => @@ -1418,7 +1418,7 @@ llvmExp10fOverride :: (FloatType SingleFloat) llvmExp10fOverride = [llvmOvr| float @exp10f( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) -- macOS uses __exp10(f) instead of exp10(f). @@ -1429,7 +1429,7 @@ llvm__exp10Override :: (FloatType DoubleFloat) llvm__exp10Override = [llvmOvr| double @__exp10( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) llvm__exp10fOverride :: IsSymInterface sym => @@ -1438,7 +1438,7 @@ llvm__exp10fOverride :: (FloatType SingleFloat) llvm__exp10fOverride = [llvmOvr| float @__exp10f( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args) -- log10(f) @@ -1449,7 +1449,7 @@ llvmLog10Override :: (FloatType DoubleFloat) llvmLog10Override = [llvmOvr| double @log10( double ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args) llvmLog10fOverride :: IsSymInterface sym => @@ -1458,7 +1458,7 @@ llvmLog10fOverride :: (FloatType SingleFloat) llvmLog10fOverride = [llvmOvr| float @log10f( float ) |] - (\_memOps _bak args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args) + (\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args) ------------------------------------------------------------------------ -- *** Other @@ -1498,13 +1498,14 @@ llvmAbortOverride => LLVMOverride p sym ext EmptyCtx UnitType llvmAbortOverride = [llvmOvr| void @abort() |] - (\_ bak _args -> liftIO $ - do let sym = backendGetSym bak - when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $ - let err = AssertFailureSimError "Call to abort" "" in - assert bak (falsePred sym) err - loc <- getCurrentProgramLoc sym - abortExecBecause $ EarlyExit loc + (\_ _args -> + ovrWithBackend $ \bak -> liftIO $ do + let sym = backendGetSym bak + when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $ + let err = AssertFailureSimError "Call to abort" "" in + assert bak (falsePred sym) err + loc <- getCurrentProgramLoc sym + abortExecBecause $ EarlyExit loc ) llvmExitOverride @@ -1516,7 +1517,7 @@ llvmExitOverride UnitType llvmExitOverride = [llvmOvr| void @exit( i32 ) |] - (\_ bak args -> Ctx.uncurryAssignment (callExit bak) args) + (\_ args -> Ctx.uncurryAssignment callExit args) llvmGetenvOverride :: (IsSymInterface sym, HasPtrWidth wptr) @@ -1525,7 +1526,9 @@ llvmGetenvOverride (LLVMPointerType wptr) llvmGetenvOverride = [llvmOvr| i8* @getenv( i8* ) |] - (\_ bak _args -> liftIO $ mkNullPointer (backendGetSym bak) PtrWidth) + (\_ _args -> do + sym <- getSymInterface + liftIO $ mkNullPointer sym PtrWidth) llvmHtonlOverride :: (IsSymInterface sym, ?lc :: TypeContext) => @@ -1534,7 +1537,7 @@ llvmHtonlOverride :: (BVType 32) llvmHtonlOverride = [llvmOvr| i32 @htonl( i32 ) |] - (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args) + (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args) llvmHtonsOverride :: (IsSymInterface sym, ?lc :: TypeContext) => @@ -1543,7 +1546,7 @@ llvmHtonsOverride :: (BVType 16) llvmHtonsOverride = [llvmOvr| i16 @htons( i16 ) |] - (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args) + (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args) llvmNtohlOverride :: (IsSymInterface sym, ?lc :: TypeContext) => @@ -1552,7 +1555,7 @@ llvmNtohlOverride :: (BVType 32) llvmNtohlOverride = [llvmOvr| i32 @ntohl( i32 ) |] - (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args) + (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args) llvmNtohsOverride :: (IsSymInterface sym, ?lc :: TypeContext) => @@ -1561,7 +1564,7 @@ llvmNtohsOverride :: (BVType 16) llvmNtohsOverride = [llvmOvr| i16 @ntohs( i16 ) |] - (\_ _bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args) + (\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args) llvmAbsOverride :: (IsSymInterface sym, HasLLVMAnn sym) => @@ -1570,7 +1573,7 @@ llvmAbsOverride :: (BVType 32) llvmAbsOverride = [llvmOvr| i32 @abs( i32 ) |] - (\mvar _bak args -> + (\mvar args -> do callStack <- callStackFromMemVar' mvar Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args) @@ -1584,7 +1587,7 @@ llvmLAbsOverride_32 :: (BVType 32) llvmLAbsOverride_32 = [llvmOvr| i32 @labs( i32 ) |] - (\mvar _bak args -> + (\mvar args -> do callStack <- callStackFromMemVar' mvar Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args) @@ -1595,7 +1598,7 @@ llvmLAbsOverride_64 :: (BVType 64) llvmLAbsOverride_64 = [llvmOvr| i64 @labs( i64 ) |] - (\mvar _bak args -> + (\mvar args -> do callStack <- callStackFromMemVar' mvar Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) args) @@ -1606,7 +1609,7 @@ llvmLLAbsOverride :: (BVType 64) llvmLLAbsOverride = [llvmOvr| i64 @llabs( i64 ) |] - (\mvar _bak args -> + (\mvar args -> do callStack <- callStackFromMemVar' mvar Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) args) @@ -1721,7 +1724,9 @@ cxa_atexitOverride (BVType 32) cxa_atexitOverride = [llvmOvr| i32 @__cxa_atexit( void (i8*)*, i8*, i8* ) |] - (\_ bak _args -> liftIO $ bvLit (backendGetSym bak) knownNat (BV.zero knownNat)) + (\_ _args -> do + sym <- getSymInterface + liftIO $ bvLit sym knownNat (BV.zero knownNat)) ---------------------------------------------------------------------------- diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libcxx.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libcxx.hs index 44e1fdf5e..f5a644a9b 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libcxx.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libcxx.hs @@ -50,6 +50,7 @@ import What4.Interface (bvLit, natLit) import Lang.Crucible.Backend import Lang.Crucible.CFG.Common (GlobalVar) +import Lang.Crucible.Simulator.OverrideSim (getSymInterface) import Lang.Crucible.Simulator.RegMap (RegValue, regValue) import Lang.Crucible.Panic (panic) import Lang.Crucible.Types (TypeRepr(UnitRepr), CtxRepr) @@ -147,7 +148,7 @@ voidOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) voidOverride substrings = mkOverride substrings $ \decl argTys retTy -> Just $ case retTy of - UnitRepr -> SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \_mem _sym _args -> pure () + UnitRepr -> SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \_mem _args -> pure () _ -> panic_ "voidOverride" decl argTys retTy -- | Make an override for a function of (LLVM) type @a -> a@, for any @a@. @@ -162,7 +163,7 @@ identityOverride substrings = case argTys of (Ctx.Empty Ctx.:> argTy) | Just Refl <- testEquality argTy retTy -> - SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \_mem _sym args -> + SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \_mem args -> -- Just return the input pure (Ctx.uncurryAssignment regValue args) @@ -180,7 +181,7 @@ constOverride substrings = case argTys of (Ctx.Empty Ctx.:> fstTy Ctx.:> _) | Just Refl <- testEquality fstTy retTy -> - SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \_mem _sym args -> + SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \_mem args -> pure (Ctx.uncurryAssignment (const . regValue) args) _ -> panic_ "constOverride" decl argTys retTy @@ -196,8 +197,9 @@ fixedOverride ty regval substrings = mkOverride substrings $ \decl argTys retTy -> Just $ case testEquality retTy ty of Just Refl -> - SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \mem bak _args -> - liftIO (regval mem (backendGetSym bak)) + SomeLLVMOverride $ LLVMOverride decl argTys retTy $ \mem _args -> do + sym <- getSymInterface + liftIO (regval mem sym) _ -> panic_ "fixedOverride" decl argTys retTy diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SymIO.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SymIO.hs index 73a2a30bb..e7bdbbdbc 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/SymIO.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SymIO.hs @@ -408,17 +408,16 @@ openFile openFile fsVars = [llvmOvr| i32 @open( i8*, i32 ) |] -- TODO add mode support by making this a varargs function - (\memOps bak args -> uncurryAssignment (callOpenFile bak memOps fsVars) args) + (\memOps args -> uncurryAssignment (callOpenFile memOps fsVars) args) callOpenFile :: - (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => - bak -> + (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> LLVMFileSystem wptr -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType 32) -> OverrideSim p sym ext rtp args ret (RegValue sym (BVType 32)) -callOpenFile _bak memOps fsVars filename_ptr _flags = +callOpenFile memOps fsVars filename_ptr _flags = do fileIdent <- loadFileIdent memOps (regValue filename_ptr) SymIO.openFile (llvmFileSystem fsVars) fileIdent $ \case Left SymIO.FileNotFound -> returnIOError32 @@ -432,17 +431,16 @@ closeFile (BVType 32) closeFile fsVars = [llvmOvr| i32 @close( i32 ) |] - (\memOps bak args -> uncurryAssignment (callCloseFile bak memOps fsVars) args) + (\memOps args -> uncurryAssignment (callCloseFile memOps fsVars) args) callCloseFile :: - (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr) => - bak -> + (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => GlobalVar Mem -> LLVMFileSystem wptr -> RegEntry sym (BVType 32) -> OverrideSim p sym ext rtp args ret (RegValue sym (BVType 32)) -callCloseFile bak _memOps fsVars filedesc = - do let sym = backendGetSym bak +callCloseFile _memOps fsVars filedesc = + do sym <- getSymInterface lookupFileHandle fsVars (regValue filedesc) emptyRegMap $ \case Just fileHandle -> \_ -> SymIO.closeFileHandle (llvmFileSystem fsVars) fileHandle $ \case @@ -460,29 +458,29 @@ readFileHandle (BVType wptr) readFileHandle fsVars = [llvmOvr| ssize_t @read( i32, i8*, size_t ) |] - (\memOps bak args -> uncurryAssignment (callReadFileHandle bak memOps fsVars) args) + (\memOps args -> uncurryAssignment (callReadFileHandle memOps fsVars) args) callReadFileHandle :: - (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr) => - bak -> + (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => GlobalVar Mem -> LLVMFileSystem wptr -> RegEntry sym (BVType 32) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr)) -callReadFileHandle bak memOps fsVars filedesc buf count = - do let sym = backendGetSym bak +callReadFileHandle memOps fsVars filedesc buf count = + do sym <- getSymInterface let args = Empty :> filedesc :> buf :> count lookupFileHandle fsVars (regValue filedesc) (RegMap args) $ \case Just fileHandle -> \(RegMap (Empty :> _ :> buffer_ptr :> size)) -> SymIO.readChunk (llvmFileSystem fsVars) fileHandle (regValue size) $ \case Left SymIO.FileHandleClosed -> returnIOError Right (chunk, bytesRead) -> do - modifyGlobal memOps $ \mem -> liftIO $ do - chunkArray <- SymIO.chunkToArray sym (W4.BaseBVRepr PtrWidth) chunk - mem' <- doArrayStore bak mem (regValue buffer_ptr) noAlignment chunkArray bytesRead - return (bytesRead, mem') + ovrWithBackend $ \bak -> + modifyGlobal memOps $ \mem -> liftIO $ do + chunkArray <- SymIO.chunkToArray sym (W4.BaseBVRepr PtrWidth) chunk + mem' <- doArrayStore bak mem (regValue buffer_ptr) noAlignment chunkArray bytesRead + return (bytesRead, mem') Nothing -> \_ -> returnIOError -- | If the write is to a concrete FD for which we have an associated 'IO.Handle', mirror the write to that Handle @@ -530,27 +528,27 @@ writeFileHandle (BVType wptr) writeFileHandle fsVars = [llvmOvr| ssize_t @write( i32, i8*, size_t ) |] - (\memOps bak args -> uncurryAssignment (callWriteFileHandle bak memOps fsVars) args) + (\memOps args -> uncurryAssignment (callWriteFileHandle memOps fsVars) args) callWriteFileHandle :: - (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => - bak -> + (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> LLVMFileSystem wptr -> RegEntry sym (BVType 32) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr)) -callWriteFileHandle bak memOps fsVars filedesc buf count = +callWriteFileHandle memOps fsVars filedesc buf count = do let args = Empty :> filedesc :> buf :> count lookupFileHandle fsVars (regValue filedesc) (RegMap args) $ \case Just fileHandle -> \(RegMap (Empty :> _ :> buffer_ptr :> size)) -> do mem <- readGlobal memOps - chunk <- liftIO $ chunkFromMemory bak mem (regValue buffer_ptr) - doConcreteWrite (llvmFilePointerRepr fsVars) (llvmHandles fsVars) (regValue filedesc) chunk size - SymIO.writeChunk (llvmFileSystem fsVars) fileHandle chunk (regValue size) $ \case - Left SymIO.FileHandleClosed -> returnIOError - Right bytesWritten -> return bytesWritten + ovrWithBackend $ \bak -> do + chunk <- liftIO $ chunkFromMemory bak mem (regValue buffer_ptr) + doConcreteWrite (llvmFilePointerRepr fsVars) (llvmHandles fsVars) (regValue filedesc) chunk size + SymIO.writeChunk (llvmFileSystem fsVars) fileHandle chunk (regValue size) $ \case + Left SymIO.FileHandleClosed -> returnIOError + Right bytesWritten -> return bytesWritten Nothing -> \_ -> returnIOError -- | The file handling overrides diff --git a/crux-llvm/src/Crux/LLVM/Overrides.hs b/crux-llvm/src/Crux/LLVM/Overrides.hs index f7f65317c..19e68a395 100644 --- a/crux-llvm/src/Crux/LLVM/Overrides.hs +++ b/crux-llvm/src/Crux/LLVM/Overrides.hs @@ -43,13 +43,14 @@ import Lang.Crucible.Simulator.RegMap(regValue,RegValue,RegEntry) import Lang.Crucible.Simulator.ExecutionTree( printHandle ) import Lang.Crucible.Simulator.OverrideSim ( getContext + , getSymInterface , readGlobal , writeGlobal , ovrWithBackend ) import Lang.Crucible.Simulator.SimError (SimErrorReason(..),SimError(..)) import Lang.Crucible.Backend - ( IsSymInterface, IsSymBackend, addDurableAssertion + ( IsSymInterface, addDurableAssertion , addAssumption, LabeledPred(..), CrucibleAssumption(..) , backendGetSym ) @@ -146,7 +147,7 @@ cruxLLVMOverrides arch = , basic_llvm_override $ [llvmOvr| void @crucible_dump_memory( ) |] - (\mvar _sym _args -> + (\mvar _args -> do mem <- readGlobal mvar h <- printHandle <$> getContext liftIO (doDumpMem h mem)) @@ -363,208 +364,200 @@ lookupString _ mvar ptr = return (BS8.unpack (BS.pack bytes)) sv_comp_fresh_bits :: - (IsSymBackend sym bak, 1 <= w) => + (IsSymInterface sym, 1 <= w) => NatRepr w -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) EmptyCtx -> OverM personality sym ext (RegValue sym (BVType w)) -sv_comp_fresh_bits w _mvar _bak Empty = Crux.mkFresh (safeSymbol "X") (BaseBVRepr w) +sv_comp_fresh_bits w _mvar Empty = Crux.mkFresh (safeSymbol "X") (BaseBVRepr w) sv_comp_fresh_float :: - (IsSymBackend sym bak) => + IsSymInterface sym => FloatInfoRepr fi -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) EmptyCtx -> OverM personality sym ext (RegValue sym (FloatType fi)) -sv_comp_fresh_float fi _mvar _bak Empty = Crux.mkFreshFloat (safeSymbol "X") fi +sv_comp_fresh_float fi _mvar Empty = Crux.mkFreshFloat (safeSymbol "X") fi fresh_bits :: - ( ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w + ( ArchOk arch, IsSymInterface sym, HasLLVMAnn sym, 1 <= w , ?memOpts :: MemOptions ) => Proxy# arch -> NatRepr w -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch) -> OverM personality sym ext (RegValue sym (BVType w)) -fresh_bits arch w mvar _ (Empty :> pName) = +fresh_bits arch w mvar (Empty :> pName) = do name <- lookupString arch mvar pName Crux.mkFresh (safeSymbol name) (BaseBVRepr w) fresh_float :: - ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym + ( ArchOk arch, IsSymInterface sym, HasLLVMAnn sym , ?memOpts :: MemOptions ) => Proxy# arch -> FloatInfoRepr fi -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch) -> OverM personality sym ext (RegValue sym (FloatType fi)) -fresh_float arch fi mvar _ (Empty :> pName) = +fresh_float arch fi mvar (Empty :> pName) = do name <- lookupString arch mvar pName Crux.mkFreshFloat (safeSymbol name) fi fresh_str :: - ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym + ( ArchOk arch, HasLLVMAnn sym , ?memOpts :: MemOptions ) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> BVType (ArchWidth arch)) -> OverM personality sym ext (RegValue sym (TPtr arch)) -fresh_str arch mvar bak (Empty :> pName :> maxLen) = - do let sym = backendGetSym bak - name <- lookupString arch mvar pName - - -- Compute the allocation length, which is the requested length plus one - -- to hold the NUL terminator - one <- liftIO $ bvLit sym ?ptrWidth (BV.one ?ptrWidth) - -- maxLenBV <- liftIO $ projectLLVM_bv sym (regValue maxLen) - len <- liftIO $ bvAdd sym (regValue maxLen) one - mem0 <- readGlobal mvar - - -- Allocate memory to hold the string - (ptr, mem1) <- liftIO $ doMalloc bak HeapAlloc Mutable name mem0 len noAlignment - - -- Allocate contents for the string - we want to make each byte symbolic, - -- so we allocate a fresh array (which has unbounded length) with symbolic - -- contents and write it into our allocation. This write does not cover - -- the NUL terminator. - contentsName <- case userSymbol (name ++ "_contents") of - Left err -> fail (show err) - Right nm -> return nm - let arrayRep = BaseArrayRepr (Empty :> BaseBVRepr ?ptrWidth) (BaseBVRepr (knownNat @8)) - initContents <- liftIO $ freshConstant sym contentsName arrayRep - zeroByte <- liftIO $ bvLit sym (knownNat @8) (BV.zero knownNat) - -- Put the NUL terminator in place - initContentsZ <- liftIO $ arrayUpdate sym initContents (singleton (regValue maxLen)) zeroByte - mem2 <- liftIO $ doArrayConstStore bak mem1 ptr noAlignment initContentsZ len - - writeGlobal mvar mem2 - return ptr +fresh_str arch mvar (Empty :> pName :> maxLen) = + ovrWithBackend $ \bak -> do + let sym = backendGetSym bak + name <- lookupString arch mvar pName + + -- Compute the allocation length, which is the requested length plus one + -- to hold the NUL terminator + one <- liftIO $ bvLit sym ?ptrWidth (BV.one ?ptrWidth) + -- maxLenBV <- liftIO $ projectLLVM_bv sym (regValue maxLen) + len <- liftIO $ bvAdd sym (regValue maxLen) one + mem0 <- readGlobal mvar + + -- Allocate memory to hold the string + (ptr, mem1) <- liftIO $ doMalloc bak HeapAlloc Mutable name mem0 len noAlignment + + -- Allocate contents for the string - we want to make each byte symbolic, + -- so we allocate a fresh array (which has unbounded length) with symbolic + -- contents and write it into our allocation. This write does not cover + -- the NUL terminator. + contentsName <- case userSymbol (name ++ "_contents") of + Left err -> fail (show err) + Right nm -> return nm + let arrayRep = BaseArrayRepr (Empty :> BaseBVRepr ?ptrWidth) (BaseBVRepr (knownNat @8)) + initContents <- liftIO $ freshConstant sym contentsName arrayRep + zeroByte <- liftIO $ bvLit sym (knownNat @8) (BV.zero knownNat) + -- Put the NUL terminator in place + initContentsZ <- liftIO $ arrayUpdate sym initContents (singleton (regValue maxLen)) zeroByte + mem2 <- liftIO $ doArrayConstStore bak mem1 ptr noAlignment initContentsZ len + + writeGlobal mvar mem2 + return ptr do_assume :: - ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym + ( ArchOk arch, HasLLVMAnn sym , ?memOpts :: MemOptions ) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TBits 8 ::> TPtr arch ::> TBits 32) -> OverM personality sym ext (RegValue sym UnitType) -do_assume arch mvar bak (Empty :> p :> pFile :> line) = - do let sym = backendGetSym bak - cond <- liftIO $ bvIsNonzero sym (regValue p) - file <- lookupString arch mvar pFile - l <- case asBV (regValue line) of - Just (BV.BV l) -> return (fromInteger l) - Nothing -> return 0 - let pos = SourcePos (T.pack file) l 0 - loc <- liftIO $ getCurrentProgramLoc sym - let loc' = loc{ plSourceLoc = pos } - liftIO $ addAssumption bak (GenericAssumption loc' "crucible_assume" cond) +do_assume arch mvar (Empty :> p :> pFile :> line) = + ovrWithBackend $ \bak -> do + let sym = backendGetSym bak + cond <- liftIO $ bvIsNonzero sym (regValue p) + file <- lookupString arch mvar pFile + l <- case asBV (regValue line) of + Just (BV.BV l) -> return (fromInteger l) + Nothing -> return 0 + let pos = SourcePos (T.pack file) l 0 + loc <- liftIO $ getCurrentProgramLoc sym + let loc' = loc{ plSourceLoc = pos } + liftIO $ addAssumption bak (GenericAssumption loc' "crucible_assume" cond) do_assert :: - ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym + ( ArchOk arch, HasLLVMAnn sym , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TBits 8 ::> TPtr arch ::> TBits 32) -> OverM personality sym ext (RegValue sym UnitType) -do_assert arch mvar bak (Empty :> p :> pFile :> line) = +do_assert arch mvar (Empty :> p :> pFile :> line) = when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $ - do let sym = backendGetSym bak - cond <- liftIO $ bvIsNonzero sym (regValue p) - file <- lookupString arch mvar pFile - l <- case asBV (regValue line) of - Just (BV.BV l) -> return (fromInteger l) - Nothing -> return 0 - let pos = SourcePos (T.pack file) l 0 - loc <- liftIO $ getCurrentProgramLoc sym - let loc' = loc{ plSourceLoc = pos } - let msg = GenericSimError "crucible_assert" - liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc' msg)) - -do_print_uint32 :: - (IsSymBackend sym bak) => + ovrWithBackend $ \bak -> do + let sym = backendGetSym bak + cond <- liftIO $ bvIsNonzero sym (regValue p) + file <- lookupString arch mvar pFile + l <- case asBV (regValue line) of + Just (BV.BV l) -> return (fromInteger l) + Nothing -> return 0 + let pos = SourcePos (T.pack file) l 0 + loc <- liftIO $ getCurrentProgramLoc sym + let loc' = loc{ plSourceLoc = pos } + let msg = GenericSimError "crucible_assert" + liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc' msg)) + +do_print_uint32 :: + IsSymInterface sym => GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TBits 32) -> OverM personality sym ext (RegValue sym UnitType) -do_print_uint32 _mvar _bak (Empty :> x) = +do_print_uint32 _mvar (Empty :> x) = do h <- printHandle <$> getContext liftIO $ hPutStrLn h (show (printSymExpr (regValue x))) do_havoc_memory :: - (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) => + (ArchOk arch, IsSymInterface sym, HasLLVMAnn sym) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> TBits (ArchWidth arch)) -> OverM personality sym ext (RegValue sym UnitType) -do_havoc_memory _ mvar bak (Empty :> ptr :> len) = - do let sym = backendGetSym bak - let tp = BaseArrayRepr (Empty :> BaseBVRepr ?ptrWidth) (BaseBVRepr (knownNat @8)) - mem <- readGlobal mvar - mem' <- liftIO $ do - arr <- freshConstant sym emptySymbol tp - doArrayStore bak mem (regValue ptr) noAlignment arr (regValue len) - writeGlobal mvar mem' +do_havoc_memory _ mvar (Empty :> ptr :> len) = + ovrWithBackend $ \bak -> + do let sym = backendGetSym bak + let tp = BaseArrayRepr (Empty :> BaseBVRepr ?ptrWidth) (BaseBVRepr (knownNat @8)) + mem <- readGlobal mvar + mem' <- liftIO $ do + arr <- freshConstant sym emptySymbol tp + doArrayStore bak mem (regValue ptr) noAlignment arr (regValue len) + writeGlobal mvar mem' cprover_assume :: - (IsSymBackend sym bak) => GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TBits 32) -> OverM personality sym ext (RegValue sym UnitType) -cprover_assume _mvar bak (Empty :> p) = liftIO $ - do let sym = backendGetSym bak - cond <- bvIsNonzero sym (regValue p) - loc <- getCurrentProgramLoc sym - addAssumption bak (GenericAssumption loc "__CPROVER_assume" cond) +cprover_assume _mvar (Empty :> p) = + ovrWithBackend $ \bak -> liftIO $ do + let sym = backendGetSym bak + cond <- bvIsNonzero sym (regValue p) + loc <- getCurrentProgramLoc sym + addAssumption bak (GenericAssumption loc "__CPROVER_assume" cond) cprover_assert :: - ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym + ( ArchOk arch, HasLLVMAnn sym , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TBits 32 ::> TPtr arch) -> OverM personality sym ext (RegValue sym UnitType) -cprover_assert arch mvar bak (Empty :> p :> pMsg) = +cprover_assert arch mvar (Empty :> p :> pMsg) = when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $ - do let sym = backendGetSym bak - cond <- liftIO $ bvIsNonzero sym (regValue p) - str <- lookupString arch mvar pMsg - loc <- liftIO $ getCurrentProgramLoc sym - let msg = AssertFailureSimError "__CPROVER_assert" str - liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc msg)) + ovrWithBackend $ \bak -> + do let sym = backendGetSym bak + cond <- liftIO $ bvIsNonzero sym (regValue p) + str <- lookupString arch mvar pMsg + loc <- liftIO $ getCurrentProgramLoc sym + let msg = AssertFailureSimError "__CPROVER_assert" str + liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc msg)) cprover_r_ok :: - (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) => + (ArchOk arch, IsSymInterface sym, HasLLVMAnn sym) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> BVType (ArchWidth arch)) -> OverM personality sym ext (RegValue sym (BVType 1)) -cprover_r_ok _ mvar bak (Empty :> (regValue -> p) :> (regValue -> sz)) = - do let sym = backendGetSym bak +cprover_r_ok _ mvar (Empty :> (regValue -> p) :> (regValue -> sz)) = + do sym <- getSymInterface mem <- readGlobal mvar x <- liftIO $ isAllocatedAlignedPointer sym PtrWidth noAlignment Immutable p (Just sz) mem liftIO $ predToBV sym x knownNat cprover_w_ok :: - (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) => + (ArchOk arch, IsSymInterface sym, HasLLVMAnn sym) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> BVType (ArchWidth arch)) -> OverM personality sym ext (RegValue sym (BVType 1)) -cprover_w_ok _ mvar bak (Empty :> (regValue -> p) :> (regValue -> sz)) = - do let sym = backendGetSym bak +cprover_w_ok _ mvar (Empty :> (regValue -> p) :> (regValue -> sz)) = + do sym <- getSymInterface mem <- readGlobal mvar x <- liftIO $ isAllocatedAlignedPointer sym PtrWidth noAlignment Mutable p (Just sz) mem liftIO $ predToBV sym x knownNat diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Check.hs b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Check.hs index f33fdbf08..67dea83ba 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Check.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Check.hs @@ -168,23 +168,24 @@ createCheckOverride appCtx modCtx usedRef argFTys constraints cfg funcSym = llvmOverride_args = Crucible.cfgArgTypes cfg, llvmOverride_ret = Crucible.cfgReturnType cfg, llvmOverride_def = - \mvar bak args -> - Override.modifyGlobal mvar $ \mem -> - do - let sym = backendGetSym bak - liftIO $ (appCtx ^. log) Hi $ "Checking preconditions of " <> name - let pp = PP.renderStrict . PP.layoutPretty PP.defaultLayoutOptions - liftIO $ (appCtx ^. log) Hi "Preconditions:" - liftIO $ (appCtx ^. log) Hi $ pp (ppPreconds constraints) - stack <- collectStack - argCs <- liftIO $ getArgPreconds sym mem args - globCs <- liftIO $ getGlobalPreconds bak mem - let cs = argCs <> globCs - let args' = fmapFC (Crucible.RV . Crucible.regValue) args - liftIO $ - modifyIORef usedRef (CheckedCall stack args' cs:) - retEntry <- Crucible.callCFG cfg (Crucible.RegMap args) - return (Crucible.regValue retEntry, mem) + \mvar args -> + Override.ovrWithBackend $ \bak -> + Override.modifyGlobal mvar $ \mem -> + do + let sym = backendGetSym bak + liftIO $ (appCtx ^. log) Hi $ "Checking preconditions of " <> name + let pp = PP.renderStrict . PP.layoutPretty PP.defaultLayoutOptions + liftIO $ (appCtx ^. log) Hi "Preconditions:" + liftIO $ (appCtx ^. log) Hi $ pp (ppPreconds constraints) + stack <- collectStack + argCs <- liftIO $ getArgPreconds sym mem args + globCs <- liftIO $ getGlobalPreconds bak mem + let cs = argCs <> globCs + let args' = fmapFC (Crucible.RV . Crucible.regValue) args + liftIO $ + modifyIORef usedRef (CheckedCall stack args' cs:) + retEntry <- Crucible.callCFG cfg (Crucible.RegMap args) + return (Crucible.regValue retEntry, mem) } where getArgPreconds :: diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs index e5dda00fb..2074f3675 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs @@ -181,7 +181,7 @@ mkOverride modCtx _proxy funcSymb impl = llvmOverride_args = argTys Ctx.:> CTy.VectorRepr CTy.AnyRepr, llvmOverride_ret = toCrucibleReturnType modCtx retTy, llvmOverride_def = - \mvar _sym (args Ctx.:> _) -> + \mvar (args Ctx.:> _) -> Override.modifyGlobal mvar (\mem -> liftIO (impl fs mem args)) } Some fs@(FuncSigRepr VA.NotVarArgsRepr argFTys retTy) -> @@ -194,7 +194,7 @@ mkOverride modCtx _proxy funcSymb impl = llvmOverride_args = argTys, llvmOverride_ret = toCrucibleReturnType modCtx retTy, llvmOverride_def = - \mvar _sym args -> + \mvar args -> Override.modifyGlobal mvar (\mem -> liftIO (impl fs mem args)) } where decl = modCtx ^. moduleDecls . funcSymbol funcSymb diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs index 5f04adfed..f3c1db08a 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs @@ -142,7 +142,7 @@ mkOverride modCtx _proxy funcSymb (FuncSigRepr _ argFTys retTy) impl = llvmOverride_args = argTys, llvmOverride_ret = toCrucibleReturnType modCtx retTy, llvmOverride_def = - \mvar _sym args -> impl mvar args + \mvar args -> impl mvar args } where decl = modCtx ^. moduleDecls . funcSymbol funcSymb diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Unsound.hs b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Unsound.hs index 7d6b0b739..93a4b5c08 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Unsound.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Unsound.hs @@ -37,9 +37,9 @@ import Data.Parameterized.NatRepr (knownNat) import qualified What4.Interface as What4 -- crucible -import Lang.Crucible.Backend (IsSymBackend, backendGetSym) +import Lang.Crucible.Backend (IsSymInterface, backendGetSym) import Lang.Crucible.CFG.Common (GlobalVar) -import Lang.Crucible.Simulator.OverrideSim (OverrideSim) +import Lang.Crucible.Simulator.OverrideSim (OverrideSim, ovrWithBackend) import qualified Lang.Crucible.Simulator.OverrideSim as Override import Lang.Crucible.Simulator.RegMap (RegEntry, emptyRegMap, regValue) import Lang.Crucible.Simulator.RegValue (RegValue) @@ -85,18 +85,18 @@ unsoundOverrides usedRef = makePolymorphicLLVMOverride $ basic_llvm_override $ [llvmOvr| i32 @gethostname( i8* , size_t ) |] - ( \memOps bak args -> + ( \memOps args -> liftIO (used "gethostname") - >> Ctx.uncurryAssignment (callGetHostName arch bak memOps) args + >> Ctx.uncurryAssignment (callGetHostName arch memOps) args ), makeForAllSymArch $ \arch -> makePolymorphicLLVMOverride $ basic_llvm_override $ [llvmOvr| i8* @getenv( i8* ) |] - ( \memOps bak args -> + ( \memOps args -> liftIO (used "getenv") - >> Ctx.uncurryAssignment (callGetEnv arch bak memOps) args + >> Ctx.uncurryAssignment (callGetEnv arch memOps) args ) ] where @@ -108,7 +108,7 @@ unsoundOverrides usedRef = -- ** Implementations callGetHostName :: - ( IsSymBackend sym bak, + ( IsSymInterface sym, HasLLVMAnn sym, wptr ~ ArchWidth arch, ArchOk arch, @@ -116,13 +116,12 @@ callGetHostName :: ?memOpts :: MemOptions ) => proxy arch -> - bak -> GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)) -callGetHostName _proxy bak mvar (regValue -> ptr) (regValue -> len) = - do +callGetHostName _proxy mvar (regValue -> ptr) (regValue -> len) = + ovrWithBackend $ \bak -> do let sym = backendGetSym bak let hostname = "hostname" let lenLt bv = liftIO (What4.bvSlt sym len =<< What4.bvLit sym ?ptrWidth bv) @@ -165,7 +164,7 @@ callGetHostName _proxy bak mvar (regValue -> ptr) (regValue -> len) = -- that the variable name be concrete and then have a map from names to -- allocations holding values. callGetEnv :: - ( IsSymBackend sym bak, + ( IsSymInterface sym, HasLLVMAnn sym, wptr ~ ArchWidth arch, ArchOk arch, @@ -173,12 +172,11 @@ callGetEnv :: ?memOpts :: LLVMMem.MemOptions ) => proxy arch -> - bak -> GlobalVar Mem -> RegEntry sym (LLVMPointerType wptr) -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) -callGetEnv _proxy bak mvar _ptr = - do +callGetEnv _proxy mvar _ptr = + ovrWithBackend $ \bak -> do let value = "" Override.modifyGlobal mvar $ \mem -> liftIO $ From f3d828a3972dc38c880995ed21af0d500ab094a9 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 22 Mar 2024 16:29:16 -0400 Subject: [PATCH 3/3] crucible-llvm: Note `LLVMOverride` removal of `bak` in CHANGELOG --- crucible-llvm/CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md index 8b246d34a..59578cfd7 100644 --- a/crucible-llvm/CHANGELOG.md +++ b/crucible-llvm/CHANGELOG.md @@ -2,6 +2,9 @@ * `LLVMOverride` now has an additional `ext` type parameter. See the Haddocks for `LLVMOverride` for details and motivation. +* The `llvmOverride_def` field of `LLVMOverride` no longer takes a `bak` + argument. To retrieve the current symbolic backend, use + `Lang.Crucible.Simulator.OverrideSim.ovrWithBackend`. # 0.6 -- 2024-02-05