diff --git a/crucible-go/src/Lang/Crucible/Go/Simulate.hs b/crucible-go/src/Lang/Crucible/Go/Simulate.hs index 7e7c1b96b..15f6cb7fc 100644 --- a/crucible-go/src/Lang/Crucible/Go/Simulate.hs +++ b/crucible-go/src/Lang/Crucible/Go/Simulate.hs @@ -72,10 +72,22 @@ setSimulatorVerbosity verbosity sym = do _ <- W4.setOpt verbSetting (toInteger verbosity) return () +goExtensionEval :: + forall sym p ext rtp blocks r ctx. + (IsSymInterface sym) => + sym -> + C.IntrinsicTypes sym -> + (Int -> String -> IO ()) -> + EvalAppFunc sym (ExprExtension Go) +goExtensionEval _sym _iTypes _logFn _f x = case x of + -- | No syntax extensions. goExtensionImpl :: C.ExtensionImpl p sym Go goExtensionImpl = - C.ExtensionImpl (\_sym _iTypes _logFn _f x -> case x of) (\x -> case x of) + C.ExtensionImpl + (\sym iTypes logFn _ f -> + goExtensionEval sym iTypes logFn f) + (\x -> case x of) failIfNotEqual :: forall k f m a (b :: k). (MonadFail m, Show (f a), Show (f b), TestEquality f) @@ -127,7 +139,7 @@ doAppGo :: IsSymInterface sym -> IO (C.RegValue sym tp) doAppGo sym = evalApp sym goIntrinsicTypes out - (C.extensionEval goExtensionImpl sym goIntrinsicTypes out) $ + (goExtensionEval sym goIntrinsicTypes out) $ flip asApp $ doAppGo sym where out = const putStrLn diff --git a/crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs b/crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs index c57dd6c9f..d9a8e44e8 100644 --- a/crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs +++ b/crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs @@ -69,7 +69,7 @@ import Lang.Crucible.Utils.MonadVerbosity import qualified Lang.Crucible.Utils.MuxTree as C (toMuxTree) import qualified Lang.Crucible.Simulator as C -import qualified Lang.Crucible.Simulator.Evaluation as C (evalApp) +import qualified Lang.Crucible.Simulator.Evaluation as C (EvalAppFunc, evalApp) import qualified Lang.Crucible.Simulator.GlobalState as C import qualified Lang.Crucible.Analysis.Postdom as C import qualified Lang.Crucible.Simulator.CallFrame as C @@ -439,8 +439,21 @@ mkDelayedBindings ctx verbosity = jvmIntrinsicTypes :: C.IntrinsicTypes sym jvmIntrinsicTypes = C.emptyIntrinsicTypes +jvmExtensionEval :: + forall sym. + (IsSymInterface sym) => + sym -> + C.IntrinsicTypes sym -> + (Int -> String -> IO ()) -> + C.EvalAppFunc sym (ExprExtension JVM) +jvmExtensionEval _sym _iTypes _logFn _f x = case x of + jvmExtensionImpl :: C.ExtensionImpl p sym JVM -jvmExtensionImpl = C.ExtensionImpl (\_sym _iTypes _logFn _f x -> case x of) (\x -> case x of) +jvmExtensionImpl = + C.ExtensionImpl + (\sym iTypes logFn _ f -> + jvmExtensionEval sym iTypes logFn f) + (\x -> case x of) -- | Create a new 'C.SimContext' containing the bindings from the given 'JVMContext'. jvmSimContext :: @@ -808,7 +821,7 @@ doAppJVM :: sym -> App JVM (C.RegValue' sym) tp -> IO (C.RegValue sym tp) doAppJVM sym = C.evalApp sym jvmIntrinsicTypes out - (C.extensionEval jvmExtensionImpl sym jvmIntrinsicTypes out) (return . C.unRV) + (jvmExtensionEval sym jvmIntrinsicTypes out) (return . C.unRV) where out _verbosity _msg = return () --putStrLn diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal index 2e6b774c5..9e644121e 100644 --- a/crucible-llvm/crucible-llvm.cabal +++ b/crucible-llvm/crucible-llvm.cabal @@ -75,6 +75,7 @@ library Lang.Crucible.LLVM.Intrinsics Lang.Crucible.LLVM.MalformedLLVMModule Lang.Crucible.LLVM.MemModel + Lang.Crucible.LLVM.MemModel.CallStack Lang.Crucible.LLVM.MemModel.Generic Lang.Crucible.LLVM.MemModel.Partial Lang.Crucible.LLVM.MemModel.Pointer diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs index 09dbb2f91..becb84bfa 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs @@ -22,6 +22,7 @@ module Lang.Crucible.LLVM.Errors.MemoryError , details , ppMemoryError , MemoryOp(..) +, memOpMem , ppMemoryOp , MemoryErrorReason(..) , ppMemoryErrorReason @@ -61,6 +62,16 @@ data MemoryOp sym w | forall wlen. (1 <= wlen) => MemInvalidateOp Text (Maybe String) (LLVMPtr sym w) (SymBV sym wlen) (Mem sym) +memOpMem :: MemoryOp sym w -> Mem sym +memOpMem = + \case + MemLoadOp _ _ _ mem -> mem + MemStoreOp _ _ _ mem -> mem + MemStoreBytesOp _ _ _ mem -> mem + MemCopyOp _ _ _ mem -> mem + MemLoadHandleOp _ _ _ mem -> mem + MemInvalidateOp _ _ _ _ mem -> mem + data MemoryError sym where MemoryError :: (1 <= w) => MemoryOp sym w -> diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Eval.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Eval.hs index e6acbb0c7..9e67ec9f8 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Eval.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Eval.hs @@ -4,8 +4,10 @@ {-# LANGUAGE TypeApplications #-} module Lang.Crucible.LLVM.Eval ( llvmExtensionEval + , callStackFromMemVar ) where +import Control.Lens ((^.), view) import Control.Monad (forM_) import qualified Data.List.NonEmpty as NE import Data.Parameterized.TraversableF @@ -13,41 +15,68 @@ import Data.Parameterized.TraversableF import What4.Interface import Lang.Crucible.Backend +import Lang.Crucible.CFG.Common (GlobalVar) +import Lang.Crucible.Simulator.ExecutionTree (SimState, CrucibleState) +import Lang.Crucible.Simulator.ExecutionTree (stateGlobals) +import Lang.Crucible.Simulator.GlobalState (lookupGlobal) import Lang.Crucible.Simulator.Intrinsics import Lang.Crucible.Simulator.Evaluation import Lang.Crucible.Simulator.RegValue import Lang.Crucible.Simulator.SimError +import Lang.Crucible.Panic (panic) import qualified Lang.Crucible.LLVM.Arch.X86 as X86 import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB import Lang.Crucible.LLVM.Extension -import Lang.Crucible.LLVM.MemModel.Pointer +import Lang.Crucible.LLVM.MemModel (memImplHeap) +import Lang.Crucible.LLVM.MemModel.CallStack (CallStack, getCallStack) +import Lang.Crucible.LLVM.MemModel.MemLog (memState) import Lang.Crucible.LLVM.MemModel.Partial +import Lang.Crucible.LLVM.MemModel.Pointer +import Lang.Crucible.LLVM.Types (Mem) + +callStackFromMemVar :: + SimState p sym ext rtp lang args -> + GlobalVar Mem -> + CallStack +callStackFromMemVar state mvar = + getCallStack . view memState . memImplHeap $ + case lookupGlobal mvar (state ^. stateGlobals) of + Just v -> v + Nothing -> + panic "callStackFromMemVar" + [ "Global heap value not initialized." + , "*** Global heap variable: " ++ show mvar + ] assertSideCondition :: (HasLLVMAnn sym, IsSymInterface sym) => sym -> + CallStack -> LLVMSideCondition (RegValue' sym) -> IO () -assertSideCondition sym (LLVMSideCondition (RV p) ub) = - do p' <- annotateUB sym ub p +assertSideCondition sym callStack (LLVMSideCondition (RV p) ub) = + do p' <- annotateUB sym callStack ub p let err = AssertFailureSimError "Undefined behavior encountered" (show (UB.explain ub)) assert sym p' err -llvmExtensionEval :: forall sym. +llvmExtensionEval :: + forall sym p ext rtp blocks r ctx. (HasLLVMAnn sym, IsSymInterface sym) => sym -> IntrinsicTypes sym -> (Int -> String -> IO ()) -> + CrucibleState p sym ext rtp blocks r ctx -> EvalAppFunc sym LLVMExtensionExpr -llvmExtensionEval sym _iTypes _logFn eval e = +llvmExtensionEval sym _iTypes _logFn state eval e = case e of X86Expr ex -> X86.eval sym eval ex - LLVM_SideConditions _ _tp conds val -> - do conds' <- traverse (traverseF (\x -> RV @sym <$> eval x)) (NE.toList conds) - forM_ conds' (assertSideCondition sym) + LLVM_SideConditions mvar _tp conds val -> + do let callStack = callStackFromMemVar state mvar + conds' <- traverse (traverseF (\x -> RV @sym <$> eval x)) (NE.toList conds) + forM_ conds' (assertSideCondition sym callStack) eval val LLVM_PointerExpr _w blk off -> diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs index 4aa1c951f..e6d8cb6f6 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs @@ -25,6 +25,7 @@ module Lang.Crucible.LLVM.Intrinsics.Common , llvmSSizeT , OverrideTemplate(..) , TemplateMatcher(..) + , callStackFromMemVar' -- ** register_llvm_override , basic_llvm_override , polymorphic1_llvm_override @@ -65,7 +66,9 @@ import Lang.Crucible.Types import What4.FunctionName import Lang.Crucible.LLVM.Extension +import Lang.Crucible.LLVM.Eval (callStackFromMemVar) import Lang.Crucible.LLVM.MemModel +import Lang.Crucible.LLVM.MemModel.CallStack (CallStack) import Lang.Crucible.LLVM.Translation.Monad import Lang.Crucible.LLVM.Translation.Types @@ -114,6 +117,11 @@ type RegOverrideM p sym arch rtp l a = ReaderT (L.Declare, Maybe ABI.DecodedName, LLVMContext arch) (MaybeT (OverrideSim p sym LLVM rtp l a)) +callStackFromMemVar' :: + GlobalVar Mem -> + OverrideSim p sym ext r args ret CallStack +callStackFromMemVar' mvar = use (to (flip callStackFromMemVar mvar)) + ------------------------------------------------------------------------ -- ** register_llvm_override diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs index c6a1d3fbd..ee162ed1d 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs @@ -573,7 +573,9 @@ llvmAbsOverride :: llvmAbsOverride w = let nm = L.Symbol ("llvm.abs.i" ++ show (natValue w)) in [llvmOvr| #w $nm( #w, i1 ) |] - (\_memOpts sym args -> Ctx.uncurryAssignment (Libc.callLLVMAbs sym w) args) + (\mvar sym args -> + do callStack <- callStackFromMemVar' mvar + Ctx.uncurryAssignment (Libc.callLLVMAbs sym callStack w) args) llvmCopysignOverride_F32 :: IsSymInterface sym => diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs index 1b2f30c3e..0e8fde1a6 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs @@ -57,6 +57,7 @@ import qualified Lang.Crucible.LLVM.Errors.Poison as Poison import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB import Lang.Crucible.LLVM.MalformedLLVMModule import Lang.Crucible.LLVM.MemModel +import Lang.Crucible.LLVM.MemModel.CallStack (CallStack) import qualified Lang.Crucible.LLVM.MemModel.Type as G import qualified Lang.Crucible.LLVM.MemModel.Generic as G import Lang.Crucible.LLVM.MemModel.Partial @@ -1367,7 +1368,9 @@ llvmAbsOverride :: (BVType 32) llvmAbsOverride = [llvmOvr| i32 @abs( i32 ) |] - (\_ sym args -> Ctx.uncurryAssignment (callLibcAbs sym (knownNat @32)) args) + (\mvar sym args -> + do callStack <- callStackFromMemVar' mvar + Ctx.uncurryAssignment (callLibcAbs sym 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 @@ -1379,7 +1382,9 @@ llvmLAbsOverride_32 :: (BVType 32) llvmLAbsOverride_32 = [llvmOvr| i32 @labs( i32 ) |] - (\_ sym args -> Ctx.uncurryAssignment (callLibcAbs sym (knownNat @32)) args) + (\mvar sym args -> + do callStack <- callStackFromMemVar' mvar + Ctx.uncurryAssignment (callLibcAbs sym callStack (knownNat @32)) args) llvmLAbsOverride_64 :: (IsSymInterface sym, HasLLVMAnn sym) => @@ -1388,7 +1393,9 @@ llvmLAbsOverride_64 :: (BVType 64) llvmLAbsOverride_64 = [llvmOvr| i64 @labs( i64 ) |] - (\_ sym args -> Ctx.uncurryAssignment (callLibcAbs sym (knownNat @64)) args) + (\mvar sym args -> + do callStack <- callStackFromMemVar' mvar + Ctx.uncurryAssignment (callLibcAbs sym callStack (knownNat @64)) args) llvmLLAbsOverride :: (IsSymInterface sym, HasLLVMAnn sym) => @@ -1397,7 +1404,9 @@ llvmLLAbsOverride :: (BVType 64) llvmLLAbsOverride = [llvmOvr| i64 @llabs( i64 ) |] - (\_ sym args -> Ctx.uncurryAssignment (callLibcAbs sym (knownNat @64)) args) + (\mvar sym args -> + do callStack <- callStackFromMemVar' mvar + Ctx.uncurryAssignment (callLibcAbs sym callStack (knownNat @64)) args) callBSwap :: (1 <= width, IsSymInterface sym) => @@ -1427,16 +1436,17 @@ callAbs :: forall w p sym ext r args ret. (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => sym -> + CallStack -> CheckAbsIntMin -> NatRepr w -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callAbs sym checkIntMin widthRepr (regValue -> src) = liftIO $ do +callAbs sym callStack checkIntMin widthRepr (regValue -> src) = liftIO $ do bvIntMin <- bvLit sym widthRepr (BV.minSigned widthRepr) isNotIntMin <- notPred sym =<< bvEq sym src bvIntMin when shouldCheckIntMin $ do - isNotIntMinUB <- annotateUB sym ub isNotIntMin + isNotIntMinUB <- annotateUB sym callStack ub isNotIntMin let err = AssertFailureSimError "Undefined behavior encountered" $ show $ UB.explain ub assert sym isNotIntMinUB err @@ -1461,19 +1471,21 @@ callAbs sym checkIntMin widthRepr (regValue -> src) = liftIO $ do callLibcAbs :: (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => sym -> + CallStack -> NatRepr w -> RegEntry sym (BVType w) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callLibcAbs sym = callAbs sym LibcAbsIntMinUB +callLibcAbs sym callStack = callAbs sym callStack LibcAbsIntMinUB callLLVMAbs :: (1 <= w, IsSymInterface sym, HasLLVMAnn sym) => sym -> + CallStack -> NatRepr w -> RegEntry sym (BVType w) -> RegEntry sym (BVType 1) -> OverrideSim p sym ext r args ret (RegValue sym (BVType w)) -callLLVMAbs sym widthRepr src (regValue -> isIntMinPoison) = do +callLLVMAbs sym 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. @@ -1482,7 +1494,7 @@ callLLVMAbs sym widthRepr src (regValue -> isIntMinPoison) = do Nothing -> malformedLLVMModule "Call to llvm.abs.* with non-constant second argument" [printSymExpr isIntMinPoison] - callAbs sym (LLVMAbsIntMinPoison shouldCheckIntMin) widthRepr src + callAbs sym 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 diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs index e7aaad231..344b5c47b 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs @@ -237,6 +237,7 @@ import Lang.Crucible.LLVM.Errors.MemoryError import qualified Lang.Crucible.LLVM.Errors.MemoryError as ME import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB import Lang.Crucible.LLVM.MemType +import Lang.Crucible.LLVM.MemModel.CallStack (CallStack, getCallStack) import qualified Lang.Crucible.LLVM.MemModel.MemLog as ML import Lang.Crucible.LLVM.MemModel.Type import qualified Lang.Crucible.LLVM.MemModel.Partial as Partial @@ -250,7 +251,7 @@ import Lang.Crucible.LLVM.Utils import Lang.Crucible.Panic (panic) -import GHC.Stack +import GHC.Stack (HasCallStack) ---------------------------------------------------------------------- -- The MemImpl type @@ -305,11 +306,12 @@ doDumpMem h mem = do assertUndefined :: (IsSymInterface sym, Partial.HasLLVMAnn sym) => -- HasPtrWidth wptr) sym -> + CallStack -> Pred sym -> (UB.UndefinedBehavior (RegValue' sym)) {- ^ The undesirable behavior -} -> IO () -assertUndefined sym p ub = - do p' <- Partial.annotateUB sym ub p +assertUndefined sym callStack p ub = + do p' <- Partial.annotateUB sym callStack ub p assert sym p' $ AssertFailureSimError "Undefined behavior encountered" (show (UB.explain ub)) @@ -474,9 +476,10 @@ evalStmt sym = eval v2 <- isValidPointer sym y mem v3 <- G.notAliasable sym x y (memImplHeap mem) - assertUndefined sym v1 $ + let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) + assertUndefined sym callStack v1 $ UB.CompareInvalidPointer UB.Eq (RV x) (RV y) - assertUndefined sym v2 $ + assertUndefined sym callStack v2 $ UB.CompareInvalidPointer UB.Eq (RV x) (RV y) unless (laxConstantEquality ?memOpts) $ @@ -498,13 +501,15 @@ evalStmt sym = eval liftIO $ do v1 <- isValidPointer sym x mem v2 <- isValidPointer sym y mem - assertUndefined sym v1 + + let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) + assertUndefined sym callStack v1 (UB.CompareInvalidPointer UB.Leq (RV x) (RV y)) - assertUndefined sym v2 + assertUndefined sym callStack v2 (UB.CompareInvalidPointer UB.Leq (RV x) (RV y)) (le, valid) <- ptrLe sym PtrWidth x y - assertUndefined sym valid + assertUndefined sym callStack valid (UB.CompareDifferentAllocs (RV x) (RV y)) pure le @@ -791,9 +796,10 @@ doFree sym mem ptr = do p1' <- orPred sym p1 isNull p2' <- orPred sym p2 isNull notFreed' <- orPred sym notFreed isNull - assertUndefined sym p1' (UB.FreeBadOffset (RV ptr)) - assertUndefined sym p2' (UB.FreeUnallocated (RV ptr)) - assertUndefined sym notFreed' (UB.DoubleFree (RV ptr)) + let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) + assertUndefined sym callStack p1' (UB.FreeBadOffset (RV ptr)) + assertUndefined sym callStack p2' (UB.FreeUnallocated (RV ptr)) + assertUndefined sym callStack notFreed' (UB.DoubleFree (RV ptr)) return mem{ memImplHeap = heap', memImplHandleMap = hMap' } @@ -814,7 +820,8 @@ doMemset sym w mem dest val len = do (heap', p) <- G.setMem sym PtrWidth dest val len' (memImplHeap mem) - assertUndefined sym p $ + let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) + assertUndefined sym callStack p $ UB.MemsetInvalidRegion (RV dest) (RV val) (RV len) return mem{ memImplHeap = heap' } @@ -885,7 +892,8 @@ doArrayStoreSize len sym mem ptr alignment arr = do let mop = MemStoreBytesOp gsym ptr len (memImplHeap mem) assertStoreError sym mop UnwritableRegion p1 - assertUndefined sym p2 (UB.WriteBadAlignment (RV ptr) alignment) + let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) + assertUndefined sym callStack p2 (UB.WriteBadAlignment (RV ptr) alignment) return mem { memImplHeap = heap' } @@ -910,7 +918,8 @@ doArrayConstStore sym mem ptr alignment arr len = do let mop = MemStoreBytesOp gsym ptr (Just len) (memImplHeap mem) assertStoreError sym mop UnwritableRegion p1 - assertUndefined sym p2 (UB.WriteBadAlignment (RV ptr) alignment) + let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) + assertUndefined sym callStack p2 (UB.WriteBadAlignment (RV ptr) alignment) return mem { memImplHeap = heap' } @@ -975,9 +984,10 @@ doPtrSubtract :: LLVMPtr sym wptr -> LLVMPtr sym wptr -> IO (SymBV sym wptr) -doPtrSubtract sym _m x y = do +doPtrSubtract sym mem x y = do (diff, valid) <- ptrDiff sym PtrWidth x y - assertUndefined sym valid $ + let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) + assertUndefined sym callStack valid $ UB.PtrSubDifferentAllocs (RV x) (RV y) pure diff @@ -997,7 +1007,8 @@ doPtrAddOffset sym m x@(LLVMPointer blk _) off = do Just True -> return isBV _ -> orPred sym isBV =<< G.isValidPointer sym PtrWidth x' (memImplHeap m) unless (laxLoadsAndStores ?memOpts) $ - assertUndefined sym v (UB.PtrAddOffsetOutOfBounds (RV x) (RV off)) + let callStack = getCallStack (m ^. to memImplHeap . ML.memState) + in assertUndefined sym callStack v (UB.PtrAddOffsetOutOfBounds (RV x) (RV off)) return x' -- | This predicate tests if the pointer is a valid, live pointer @@ -1176,7 +1187,8 @@ storeRaw sym mem ptr valType alignment val = do let mop = MemStoreOp valType gsym ptr (memImplHeap mem) assertStoreError sym mop UnwritableRegion p1 - assertUndefined sym p2 (UB.WriteBadAlignment (RV ptr) alignment) + let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) + assertUndefined sym callStack p2 (UB.WriteBadAlignment (RV ptr) alignment) return mem{ memImplHeap = heap' } @@ -1256,7 +1268,8 @@ condStoreRaw sym mem cond ptr valType alignment val = do assertStoreError sym mop UnwritableRegion condIsAllocated -- Assert is aligned if write executes do condIsAligned <- impliesPred sym cond isAligned - assertUndefined sym condIsAligned (UB.WriteBadAlignment (RV ptr) alignment) + let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) + assertUndefined sym callStack condIsAligned (UB.WriteBadAlignment (RV ptr) alignment) -- Merge the write heap and non-write heap let mergedHeap = G.mergeMem cond postWriteHeap postBranchHeap -- Return new memory @@ -1280,7 +1293,8 @@ storeConstRaw sym mem ptr valType alignment val = do let mop = MemStoreOp valType gsym ptr (memImplHeap mem) assertStoreError sym mop UnwritableRegion p1 - assertUndefined sym p2 (UB.WriteBadAlignment (RV ptr) alignment) + let callStack = getCallStack (mem ^. to memImplHeap . ML.memState) + assertUndefined sym callStack p2 (UB.WriteBadAlignment (RV ptr) alignment) return mem{ memImplHeap = heap' } diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/CallStack.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/CallStack.hs new file mode 100644 index 000000000..db64f4219 --- /dev/null +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/CallStack.hs @@ -0,0 +1,49 @@ +------------------------------------------------------------------------ +-- | +-- Module : Lang.Crucible.LLVM.MemModel.CallStack +-- Description : Call stacks from the LLVM memory model +-- Copyright : (c) Galois, Inc 2021 +-- License : BSD3 +-- Maintainer : Rob Dockins +-- Stability : provisional +------------------------------------------------------------------------ + +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} + +module Lang.Crucible.LLVM.MemModel.CallStack + ( CallStack + , getCallStack + , ppCallStack + ) where + +import Data.Foldable (toList) +import Data.Sequence (Seq) +import qualified Data.Sequence as Seq +import Data.Text (Text) +import qualified Prettyprinter as PP + +import Lang.Crucible.LLVM.MemModel.MemLog (MemState(..)) + +newtype FunctionName = + FunctionName { getFunctionName :: Text } + deriving (Eq, Monoid, Ord, Semigroup) + +newtype CallStack = + CallStack { runCallStack :: Seq FunctionName } + deriving (Eq, Monoid, Ord, Semigroup) + +cons :: FunctionName -> CallStack -> CallStack +cons top (CallStack rest) = CallStack (top Seq.<| rest) + +getCallStack :: MemState sym -> CallStack +getCallStack = + \case + EmptyMem{} -> CallStack mempty + StackFrame _ _ nm _ rest -> cons (FunctionName nm) (getCallStack rest) + BranchFrame _ _ _ rest -> getCallStack rest + +ppCallStack :: CallStack -> PP.Doc ann +ppCallStack = + PP.vsep . toList . fmap (PP.pretty . getFunctionName) . runCallStack diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs index f041d616c..ef25a2d6d 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -103,6 +103,7 @@ import Lang.Crucible.LLVM.Bytes import Lang.Crucible.LLVM.DataLayout import Lang.Crucible.LLVM.Errors.MemoryError (MemErrContext, MemoryErrorReason(..), MemoryOp(..)) import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB +import Lang.Crucible.LLVM.MemModel.CallStack (getCallStack) import Lang.Crucible.LLVM.MemModel.Common import Lang.Crucible.LLVM.MemModel.Options import Lang.Crucible.LLVM.MemModel.MemLog @@ -719,8 +720,9 @@ readMem sym w gsym l tp alignment m = do -- Otherwise, fall back to the less-optimized read case _ -> readMem' sym w (memEndianForm m) gsym l m tp alignment (memWrites m) + let stack = getCallStack (m ^. memState) part_val' <- applyUnless (laxLoadsAndStores ?memOpts) - (Partial.attachSideCondition sym p2 (UB.ReadBadAlignment (RV l) alignment)) + (Partial.attachSideCondition sym stack p2 (UB.ReadBadAlignment (RV l) alignment)) part_val applyUnless (laxLoadsAndStores ?memOpts) (Partial.attachMemoryError sym p1 mop UnreadableRegion) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs index 977f2cb14..68e591fe0 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs @@ -88,6 +88,8 @@ import Lang.Crucible.Simulator.SimError import Lang.Crucible.Simulator.RegValue (RegValue'(..)) import Lang.Crucible.LLVM.Bytes (Bytes) import qualified Lang.Crucible.LLVM.Bytes as Bytes +import Lang.Crucible.LLVM.MemModel.MemLog (memState) +import Lang.Crucible.LLVM.MemModel.CallStack (CallStack, getCallStack) import Lang.Crucible.LLVM.MemModel.Pointer ( pattern LLVMPointer, LLVMPtr ) import Lang.Crucible.LLVM.MemModel.Type (StorageType(..), StorageTypeF(..), Field(..)) import qualified Lang.Crucible.LLVM.MemModel.Type as Type @@ -95,7 +97,7 @@ import Lang.Crucible.LLVM.MemModel.Value (LLVMVal(..)) import qualified Lang.Crucible.LLVM.MemModel.Value as Value import Lang.Crucible.LLVM.Errors import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB -import Lang.Crucible.LLVM.Errors.MemoryError (MemoryError(..), MemoryErrorReason(..), MemoryOp(..)) +import Lang.Crucible.LLVM.Errors.MemoryError (MemoryError(..), MemoryErrorReason(..), MemoryOp(..), memOpMem) import Lang.Crucible.Panic (panic) import What4.Expr @@ -113,12 +115,12 @@ instance IsSymInterface sym => Eq (BoolAnn sym) where instance IsSymInterface sym => Ord (BoolAnn sym) where compare (BoolAnn x) (BoolAnn y) = toOrdering $ compareF x y -type LLVMAnnMap sym = Map (BoolAnn sym) (BadBehavior sym) -type HasLLVMAnn sym = (?recordLLVMAnnotation :: BoolAnn sym -> BadBehavior sym -> IO ()) +type LLVMAnnMap sym = Map (BoolAnn sym) (CallStack, BadBehavior sym) +type HasLLVMAnn sym = (?recordLLVMAnnotation :: CallStack -> BoolAnn sym -> BadBehavior sym -> IO ()) data CexExplanation sym (tp :: BaseType) where NoExplanation :: CexExplanation sym tp - DisjOfFailures :: [ BadBehavior sym ] -> CexExplanation sym BaseBoolType + DisjOfFailures :: [ (CallStack, BadBehavior sym) ] -> CexExplanation sym BaseBoolType instance Semigroup (CexExplanation sym BaseBoolType) where NoExplanation <> y = y @@ -148,11 +150,11 @@ explainCex sym bbMap evalFn = (asNonceApp -> Just (Annotation BaseBoolRepr annId e')) -> case Map.lookup (BoolAnn annId) bbMap of Nothing -> evalPos posCache negCache e' - Just bb -> + Just (callStack, bb) -> do bb' <- case evalFn of Just f -> concBadBehavior sym (groundEval f) bb Nothing -> pure bb - pure (DisjOfFailures [ bb' ]) + pure (DisjOfFailures [ (callStack, bb') ]) (asApp -> Just (BaseIte BaseBoolRepr _ c x y)) | Just f <- evalFn -> @@ -233,14 +235,18 @@ explainCex sym bbMap evalFn = annotateUB :: (IsSymInterface sym, HasLLVMAnn sym) => sym -> + CallStack -> UB.UndefinedBehavior (RegValue' sym) -> Pred sym -> IO (Pred sym) -annotateUB sym ub p = +annotateUB sym callStack ub p = do (n, p') <- annotateTerm sym p - ?recordLLVMAnnotation (BoolAnn n) (BBUndefinedBehavior ub) + ?recordLLVMAnnotation callStack (BoolAnn n) (BBUndefinedBehavior ub) return p' +memOpCallStack :: MemoryOp sym w -> CallStack +memOpCallStack = getCallStack . view memState . memOpMem + annotateME :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => sym -> MemoryOp sym w -> @@ -249,7 +255,10 @@ annotateME :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => IO (Pred sym) annotateME sym mop rsn p = do (n, p') <- annotateTerm sym p - ?recordLLVMAnnotation (BoolAnn n) (BBMemoryError (MemoryError mop rsn)) + ?recordLLVMAnnotation + (memOpCallStack mop) + (BoolAnn n) + (BBMemoryError (MemoryError mop rsn)) return p' -- | Assert that the given LLVM pointer value is actually a raw bitvector and extract its value. @@ -270,8 +279,12 @@ data PartLLVMVal sym where Err :: Pred sym -> PartLLVMVal sym NoErr :: Pred sym -> LLVMVal sym -> PartLLVMVal sym -partErr :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => - sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym) +partErr :: + (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) => + sym -> + MemoryOp sym w -> + MemoryErrorReason -> + IO (PartLLVMVal sym) partErr sym errCtx rsn = do p <- annotateME sym errCtx rsn (falsePred sym) pure (Err p) @@ -279,15 +292,16 @@ partErr sym errCtx rsn = attachSideCondition :: (IsSymInterface sym, HasLLVMAnn sym) => sym -> + CallStack -> Pred sym -> UB.UndefinedBehavior (RegValue' sym) -> PartLLVMVal sym -> IO (PartLLVMVal sym) -attachSideCondition sym pnew ub pv = +attachSideCondition sym callStack pnew ub pv = case pv of Err p -> pure (Err p) NoErr p v -> - do p' <- andPred sym p =<< annotateUB sym ub pnew + do p' <- andPred sym p =<< annotateUB sym callStack ub pnew return $ NoErr p' v attachMemoryError :: @@ -334,7 +348,6 @@ assertSafe sym (Err p) = do addProofObligation sym (LabeledPred p err) abortExecBecause (AssertionFailure err) - ------------------------------------------------------------------------ -- ** PartLLVMVal interface -- @@ -429,11 +442,11 @@ bvToFloat sym _ (NoErr p (LLVMValZero (StorageType (Bitvector 4) _))) = (W4IFP.iFloatFromBinary sym W4IFP.SingleFloatRepr =<< W4I.bvLit sym (knownNat @32) (BV.zero knownNat)) -bvToFloat sym _ (NoErr p (LLVMValInt blk off)) +bvToFloat sym errCtx (NoErr p (LLVMValInt blk off)) | Just Refl <- testEquality (bvWidth off) (knownNat @32) = do pz <- natEq sym blk =<< natLit sym 0 let ub = UB.PointerFloatCast (RV (LLVMPointer blk off)) Type.floatType - p' <- andPred sym p =<< annotateUB sym ub pz + p' <- andPred sym p =<< annotateUB sym (memOpCallStack errCtx) ub pz NoErr p' . LLVMValFloat Value.SingleSize <$> W4IFP.iFloatFromBinary sym W4IFP.SingleFloatRepr off @@ -457,11 +470,11 @@ bvToDouble sym _ (NoErr p (LLVMValZero (StorageType (Bitvector 8) _))) = (W4IFP.iFloatFromBinary sym W4IFP.DoubleFloatRepr =<< W4I.bvLit sym (knownNat @64) (BV.zero knownNat)) -bvToDouble sym _ (NoErr p (LLVMValInt blk off)) +bvToDouble sym errCtx (NoErr p (LLVMValInt blk off)) | Just Refl <- testEquality (bvWidth off) (knownNat @64) = do pz <- natEq sym blk =<< natLit sym 0 let ub = UB.PointerFloatCast (RV (LLVMPointer blk off)) Type.doubleType - p' <- andPred sym p =<< annotateUB sym ub pz + p' <- andPred sym p =<< annotateUB sym (memOpCallStack errCtx) ub pz NoErr p' . LLVMValFloat Value.DoubleSize <$> W4IFP.iFloatFromBinary sym W4IFP.DoubleFloatRepr off @@ -486,11 +499,11 @@ bvToX86_FP80 sym _ (NoErr p (LLVMValZero (StorageType (Bitvector 10) _))) = (W4IFP.iFloatFromBinary sym W4IFP.X86_80FloatRepr =<< W4I.bvLit sym (knownNat @80) (BV.zero knownNat)) -bvToX86_FP80 sym _ (NoErr p (LLVMValInt blk off)) +bvToX86_FP80 sym errCtx (NoErr p (LLVMValInt blk off)) | Just Refl <- testEquality (bvWidth off) (knownNat @80) = do pz <- natEq sym blk =<< natLit sym 0 let ub = UB.PointerFloatCast (RV (LLVMPointer blk off)) Type.x86_fp80Type - p' <- andPred sym p =<< annotateUB sym ub pz + p' <- andPred sym p =<< annotateUB sym (memOpCallStack errCtx) ub pz NoErr p' . LLVMValFloat Value.X86_FP80Size <$> W4IFP.iFloatFromBinary sym W4IFP.X86_80FloatRepr off @@ -546,8 +559,9 @@ bvConcat sym errCtx (NoErr p1 v1) (NoErr p2 v2) = Just LeqProof <- return $ isPosNat (addNat high_w' low_w') let ub1 = UB.PointerIntCast (RV (LLVMPointer blk_low low)) low_tp ub2 = UB.PointerIntCast (RV (LLVMPointer blk_high high)) high_tp - predLow <- annotateUB sym ub1 =<< natEq sym blk_low blk0 - predHigh <- annotateUB sym ub2 =<< natEq sym blk_high blk0 + annUB = annotateUB sym (memOpCallStack errCtx) + predLow <- annUB ub1 =<< natEq sym blk_low blk0 + predHigh <- annUB ub2 =<< natEq sym blk_high blk0 bv <- W4I.bvConcat sym high low p' <- andPred sym p1 =<< andPred sym p2 =<< andPred sym predLow predHigh @@ -732,7 +746,7 @@ selectLowBv _sym _ low hi (NoErr p (LLVMValZero (StorageType (Bitvector bytes) _ | low + hi == bytes = return $ NoErr p $ LLVMValZero (Type.bitvectorType low) -selectLowBv sym _ low hi (NoErr p (LLVMValInt blk bv)) +selectLowBv sym errCtx low hi (NoErr p (LLVMValInt blk bv)) | Just (Some (low_w)) <- someNat (Bytes.bytesToBits low) , Just (Some (hi_w)) <- someNat (Bytes.bytesToBits hi) , Just LeqProof <- isPosNat low_w @@ -741,7 +755,7 @@ selectLowBv sym _ low hi (NoErr p (LLVMValInt blk bv)) do pz <- natEq sym blk =<< natLit sym 0 bv' <- bvSelect sym (knownNat :: NatRepr 0) low_w bv let ub = UB.PointerIntCast (RV (LLVMPointer blk bv)) tp - p' <- andPred sym p =<< annotateUB sym ub pz + p' <- andPred sym p =<< annotateUB sym (memOpCallStack errCtx) ub pz return $ NoErr p' $ LLVMValInt blk bv' where w = bvWidth bv tp = Type.bitvectorType (Bytes.bitsToBytes (natValue w)) @@ -768,7 +782,7 @@ selectHighBv _sym _ low hi (NoErr p (LLVMValZero (StorageType (Bitvector bytes) | low + hi == bytes = return $ NoErr p $ LLVMValZero (Type.bitvectorType hi) -selectHighBv sym _ low hi (NoErr p (LLVMValInt blk bv)) +selectHighBv sym errCtx low hi (NoErr p (LLVMValInt blk bv)) | Just (Some (low_w)) <- someNat (Bytes.bytesToBits low) , Just (Some (hi_w)) <- someNat (Bytes.bytesToBits hi) , Just LeqProof <- isPosNat hi_w @@ -776,7 +790,7 @@ selectHighBv sym _ low hi (NoErr p (LLVMValInt blk bv)) do pz <- natEq sym blk =<< natLit sym 0 bv' <- bvSelect sym low_w hi_w bv let ub = UB.PointerIntCast (RV (LLVMPointer blk bv)) tp - p' <- andPred sym p =<< annotateUB sym ub pz + p' <- andPred sym p =<< annotateUB sym (memOpCallStack errCtx) ub pz return $ NoErr p' $ LLVMValInt blk bv' where w = bvWidth bv tp = Type.bitvectorType (Bytes.bitsToBytes (natValue w)) diff --git a/crucible-llvm/test/TestMemory.hs b/crucible-llvm/test/TestMemory.hs index 78b43e663..934fc8079 100644 --- a/crucible-llvm/test/TestMemory.hs +++ b/crucible-llvm/test/TestMemory.hs @@ -66,7 +66,7 @@ withMem :: withMem endianess action = withIONonceGenerator $ \nonce_gen -> CBO.withZ3OnlineBackend W4B.FloatIEEERepr nonce_gen CBO.NoUnsatFeatures noFeatures $ \sym -> do let ?ptrWidth = knownNat @64 - let ?recordLLVMAnnotation = \_ _ -> pure () + let ?recordLLVMAnnotation = \_ _ _ -> pure () let ?memOpts = LLVMMem.defaultMemOptions mem <- LLVMMem.emptyMem endianess action sym mem diff --git a/crucible-mc/exe/Main.hs b/crucible-mc/exe/Main.hs index 60cf1bc2e..8c5f8e32f 100644 --- a/crucible-mc/exe/Main.hs +++ b/crucible-mc/exe/Main.hs @@ -47,7 +47,7 @@ main = Just (AnyCFG cfg) -> case (cfgArgTypes cfg, cfgReturnType cfg) of (Empty, UnitRepr) -> - let ?recordLLVMAnnotation = \_ _ -> pure () in + let ?recordLLVMAnnotation = \_ _ _ -> pure () in pure Setup { cruxOutput = stdout , cruxBackend = sym diff --git a/crucible-wasm/src/Lang/Crucible/Wasm/Extension.hs b/crucible-wasm/src/Lang/Crucible/Wasm/Extension.hs index d419142bf..ce9dec1cc 100644 --- a/crucible-wasm/src/Lang/Crucible/Wasm/Extension.hs +++ b/crucible-wasm/src/Lang/Crucible/Wasm/Extension.hs @@ -139,7 +139,7 @@ extImpl mo = let ?memOpts = mo in ExtensionImpl { -- There are no interesting extension expression formers - extensionEval = \_ _ _ _ -> \case{} + extensionEval = \_ _ _ _ _ -> \case{} , extensionExec = evalWasmExt } diff --git a/crucible-wasm/tool/Main.hs b/crucible-wasm/tool/Main.hs index 25f643be2..8e15e44f2 100644 --- a/crucible-wasm/tool/Main.hs +++ b/crucible-wasm/tool/Main.hs @@ -41,7 +41,7 @@ setupWasmState :: IsSymInterface sym => setupWasmState sym memOptions s = do halloc <- newHandleAllocator - let ?recordLLVMAnnotation = \_ _ -> pure () + let ?recordLLVMAnnotation = \_ _ _ -> pure () let ?memOpts = memOptions let globals = emptyGlobals let bindings = emptyHandleMap diff --git a/crux-llvm/src/Crux/LLVM/Simulate.hs b/crux-llvm/src/Crux/LLVM/Simulate.hs index 3d074011b..8c3eb83af 100644 --- a/crux-llvm/src/Crux/LLVM/Simulate.hs +++ b/crux-llvm/src/Crux/LLVM/Simulate.hs @@ -70,6 +70,7 @@ import Lang.Crucible.LLVM.MemModel , pattern LLVMPointer, pattern LLVMPointerRepr, LLVMPointerType , pattern PtrRepr, pattern PtrWidth ) +import Lang.Crucible.LLVM.MemModel.CallStack (ppCallStack) import Lang.Crucible.LLVM.MemType (MemType(..), SymType(..), i8, memTypeAlign, memTypeSize) import Lang.Crucible.LLVM.Translation ( translateModule, ModuleTranslation, globalInitMap @@ -158,7 +159,9 @@ simulateLLVMFile :: simulateLLVMFile llvm_file llvmOpts = Crux.SimulatorCallbacks $ do bbMapRef <- newIORef (Map.empty :: LLVMAnnMap sym) - let ?recordLLVMAnnotation = \an bb -> modifyIORef bbMapRef (Map.insert an bb) + let ?recordLLVMAnnotation = + \callStack an bb -> + modifyIORef bbMapRef (Map.insert an (callStack, bb)) return $ Crux.SimulatorHooks { Crux.setupHook = @@ -382,7 +385,7 @@ explainFailure sym bbMapRef evalFn gl = case ex of NoExplanation -> mempty DisjOfFailures xs -> - case ppBB <$> xs of + case ppBBPair <$> xs of [] -> mempty [x] -> indent 2 x xs' -> @@ -397,3 +400,8 @@ explainFailure sym bbMapRef evalFn gl = else "Total failed conditions:" <+> pretty xs'l in nest 2 $ vcat $ msg1 : xs'' <> [msg2] return $ vcat [ ppSimError (gl^. labeledPredMsg), details ] + where ppBBPair (callStack, bb) = + vsep [ ppBB bb + , "in context:" + , indent 2 (ppCallStack callStack) + ] diff --git a/crux-llvm/test-data/golden/golden/T847-fail1.good b/crux-llvm/test-data/golden/golden/T847-fail1.good index b7e15eb2b..74f3038f0 100644 --- a/crux-llvm/test-data/golden/golden/T847-fail1.good +++ b/crux-llvm/test-data/golden/golden/T847-fail1.good @@ -8,6 +8,8 @@ [Crux] The C language standard, version C11 [Crux] §7.22.6 Integer arithmetic functions, ¶1 [Crux] Document URL: http://www.iso-9899.info/n1570.html +[Crux] in context: +[Crux] main [Crux] Found counterexample for verification goal [Crux] internal: error: in main [Crux] Undefined behavior encountered @@ -18,6 +20,8 @@ [Crux] The C language standard, version C11 [Crux] §7.22.6 Integer arithmetic functions, ¶1 [Crux] Document URL: http://www.iso-9899.info/n1570.html +[Crux] in context: +[Crux] main [Crux] Found counterexample for verification goal [Crux] internal: error: in main [Crux] Undefined behavior encountered @@ -28,4 +32,6 @@ [Crux] The C language standard, version C11 [Crux] §7.22.6 Integer arithmetic functions, ¶1 [Crux] Document URL: http://www.iso-9899.info/n1570.html +[Crux] in context: +[Crux] main [Crux] Overall status: Invalid. diff --git a/crux-llvm/test-data/golden/golden/double_free.good b/crux-llvm/test-data/golden/golden/double_free.good index 3ff8e9fc8..daabfeb46 100644 --- a/crux-llvm/test-data/golden/golden/double_free.good +++ b/crux-llvm/test-data/golden/golden/double_free.good @@ -9,4 +9,6 @@ [Crux] The C language standard, version C11 [Crux] §7.22.3.3 The free function, ¶2 [Crux] Document URL: http://www.iso-9899.info/n1570.html +[Crux] in context: +[Crux] main [Crux] Overall status: Invalid. diff --git a/crux-llvm/test-data/golden/golden/invoke-test.good b/crux-llvm/test-data/golden/golden/invoke-test.good index b7f6691b2..902d7f1c7 100644 --- a/crux-llvm/test-data/golden/golden/invoke-test.good +++ b/crux-llvm/test-data/golden/golden/invoke-test.good @@ -74,4 +74,7 @@ [Crux] ,base+32 = (10, 0x0:[64]) [Crux] ,base+40 = (11, 0x0:[64])} [Crux] 46 |-> *(46, 0x0:[64]) := {base+0 = "\n"} +[Crux] in context: +[Crux] _ZN3std2rt10lang_start17h4f32aa1279b9079fE +[Crux] main [Crux] Overall status: Invalid. diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs index 08fdd9aaa..6eaa4a82d 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs @@ -57,6 +57,9 @@ import Data.Void (Void) import GHC.Exts (proxy#) +import Prettyprinter as PP +import qualified Prettyprinter.Render.Text as PP + import qualified Text.LLVM.AST as L import Data.Parameterized.Ctx (Ctx) @@ -79,6 +82,7 @@ import qualified Lang.Crucible.Types as CrucibleTypes import Lang.Crucible.LLVM (llvmGlobalsToCtx, registerModuleFn) import qualified Lang.Crucible.LLVM.Errors as LLVMErrors import qualified Lang.Crucible.LLVM.Intrinsics as LLVMIntrinsics +import Lang.Crucible.LLVM.MemModel.CallStack (ppCallStack) import Lang.Crucible.LLVM.MemModel (HasLLVMAnn, LLVMAnnMap, MemImpl, MemOptions) import Lang.Crucible.LLVM.Translation (transContext, llvmMemVar, llvmTypeCtx, cfgMap, allModuleDeclares) import Lang.Crucible.LLVM.TypeContext (TypeContext) @@ -309,7 +313,8 @@ mkCallbacks appCtx modCtx funCtx halloc callbacks constraints cfg llvmOpts = -- Hooks let ?recordLLVMAnnotation = - \an bb -> IORef.modifyIORef bbMapRef (Map.insert an bb) + \callStack an bb -> + IORef.modifyIORef bbMapRef (Map.insert an (callStack, bb)) SimulatorHooks overrides resHook <- getSimulatorCallbacks callbacks @@ -495,13 +500,17 @@ mkCallbacks appCtx modCtx funCtx halloc callbacks constraints cfg llvmOpts = Located loc (ExUncertain (UMissingAnnotation (gl ^. Crucible.labeledPredMsg))) - Just badBehavior -> + Just (callStack, badBehavior) -> do -- Helpful for debugging: -- putStrLn "~~~~~~~~~~~" -- putStrLn (show (LLVMErrors.ppBB badBehavior)) liftIO $ (appCtx ^. log) Hi ("Explaining error: " <> Text.pack (show (LLVMErrors.explainBB badBehavior))) + let render = PP.renderStrict . PP.layoutPretty PP.defaultLayoutOptions + + liftIO $ (appCtx ^. log) Hi "Error call stack:" + liftIO $ (appCtx ^. log) Hi (render (ppCallStack callStack)) skipped <- IORef.readIORef skipOverrideRef retAnns <- IORef.readIORef skipReturnValueAnnotations classifyBadBehavior