crucible-llvm: Annotate errors with call stacks

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

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
 

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

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 ->

crucible-llvm/src/Lang/Crucible/LLVM/Eval.hs

@@ -4,50 +4,79 @@
 {-# 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
 
 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 ->

crucible-llvm/src/Lang/Crucible/LLVM/Extension/Syntax.hs

@@ -70,9 +70,12 @@ instance TraversableF LLVMSideCondition where
 
 data LLVMExtensionExpr :: (CrucibleType -> Type) -> (CrucibleType -> Type) where
 
-  X86Expr :: !(X86.ExtX86 f t) -> LLVMExtensionExpr f t
+  X86Expr ::
+    !(X86.ExtX86 f t) ->
+    LLVMExtensionExpr f t
 
   LLVM_SideConditions ::
+    !(GlobalVar Mem) {- Memory global variable -} ->
     !(TypeRepr tp) ->
     !(NonEmpty (LLVMSideCondition f)) ->
     !(f tp) ->
@@ -235,7 +238,7 @@ data LLVMStmt (f :: CrucibleType -> Type) :: CrucibleType -> Type where
 -- | Debug statement variants - these have no semantic meaning
 data LLVM_Dbg f c where
   -- | Annotates a value pointed to by a pointer with local-variable debug information
-  -- 
+  --
   -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-addr>
   LLVM_Dbg_Addr ::
     HasPtrWidth wptr =>
@@ -245,7 +248,7 @@ data LLVM_Dbg f c where
     LLVM_Dbg f (LLVMPointerType wptr)
 
   -- | Annotates a value pointed to by a pointer with local-variable debug information
-  -- 
+  --
   -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-declare>
   LLVM_Dbg_Declare ::
     HasPtrWidth wptr =>
@@ -270,7 +273,7 @@ instance TypeApp LLVMExtensionExpr where
   appType e =
     case e of
       X86Expr ex             -> appType ex
-      LLVM_SideConditions tpr _ _ -> tpr
+      LLVM_SideConditions _ tpr _ _ -> tpr
       LLVM_PointerExpr w _ _ -> LLVMPointerRepr w
       LLVM_PointerBlock _ _  -> NatRepr
       LLVM_PointerOffset w _ -> BVRepr w
@@ -280,7 +283,7 @@ instance PrettyApp LLVMExtensionExpr where
   ppApp pp e =
     case e of
       X86Expr ex -> ppApp pp ex
-      LLVM_SideConditions _ _conds ex ->
+      LLVM_SideConditions _ _ _conds ex ->
         pretty "sideConditions" <+> pp ex -- TODO? Print the conditions?
       LLVM_PointerExpr _ blk off ->
         pretty "pointerExpr" <+> pp blk <+> pp off
@@ -297,6 +300,7 @@ instance TestEqualityFC LLVMExtensionExpr where
        [ (U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])
        , (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
        , (U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
+       , (U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|testEquality|])
        , (U.ConType [t|X86.ExtX86|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|testEqualityFC testSubterm|])
        , (U.ConType [t|NonEmpty|] `U.TypeApp` (U.ConType [t|LLVMSideCondition|] `U.TypeApp` U.AnyType)
          , [| \x y -> if liftEq (testEqualityC testSubterm) x y then Just Refl else Nothing |]
@@ -309,6 +313,7 @@ instance OrdFC LLVMExtensionExpr where
        [ (U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])
        , (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
        , (U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
+       , (U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|compareF|])
        , (U.ConType [t|X86.ExtX86|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|compareFC testSubterm|])
        , (U.ConType [t|NonEmpty|] `U.TypeApp` (U.ConType [t|LLVMSideCondition|] `U.TypeApp` U.AnyType)
          , [| \x y -> fromOrdering (liftCompare (compareC testSubterm) x y) |]

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
 

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 =>