crucible-llvm 0.7.1 → 0.8.0.0

raw patch · 22 files changed

+831/−48 lines, 22 filesdep ~basedep ~llvm-prettydep ~what4new-uploaderPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, llvm-pretty, what4

API changes (from Hackage documentation)

Files

• CHANGELOG.md +18/−0
• crucible-llvm.cabal +96/−3
• src/Lang/Crucible/LLVM/DataLayout.hs +14/−0
• src/Lang/Crucible/LLVM/Errors/MemoryError.hs +1/−0
• src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs +2/−0
• src/Lang/Crucible/LLVM/Globals.hs +3/−2
• src/Lang/Crucible/LLVM/Internal.hs +25/−0
• src/Lang/Crucible/LLVM/Intrinsics.hs +1/−0
• src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs +129/−2
• src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +5/−4
• src/Lang/Crucible/LLVM/MemModel.hs +9/−3
• src/Lang/Crucible/LLVM/MemModel/Common.hs +8/−3
• src/Lang/Crucible/LLVM/MemModel/Generic.hs +48/−3
• src/Lang/Crucible/LLVM/MemModel/MemLog.hs +4/−0
• src/Lang/Crucible/LLVM/MemModel/Strings.hs +367/−0
• src/Lang/Crucible/LLVM/MemModel/Value.hs +1/−1
• src/Lang/Crucible/LLVM/SymIO.hs +2/−1
• src/Lang/Crucible/LLVM/Translation/BlockInfo.hs +2/−2
• src/Lang/Crucible/LLVM/Translation/Instruction.hs +72/−20
• src/Lang/Crucible/LLVM/Translation/Monad.hs +8/−0
• test/TestMemory.hs +2/−2
• test/Tests.hs +14/−2

@@ -1,3 +1,21 @@+# 0.8.0 -- 2025-11-09++* `Lang.Crucible.LLVM.MemModel.{loadString,loadMaybeString,strLen}`+  should now be imported from `Lang.Crucible.LLVM.MemModel.Strings`.+* Two new functions for loading C-style null-terminated strings from+  LLVM memory were added to `Lang.Crucible.LLVM.MemModel.Strings`:+  `loadConcretelyNullTerminatedString` and `loadSymbolicString`.+* Add a new "low-level" API for loading strings to+  `Lang.Crucible.LLVM.MemModel.Strings`: `ByteLoader`, `ByteChecker`, and+  `loadBytes`.+* Support simulating LLVM bitcode files whose data layout strings specify+  function pointer alignment.+* Fix a bug that would cause the simuator to compute incorrect results for the+  `llvm.is.fpclass` intrinsic. (Among other things, this is used to power the+  `isnan` function in Clang 17 or later.)+* Support vectorized versions of the `llvm.u{min,max}` and `llvm.s{min,max}`+  intrinsics.+ # 0.7.1 -- 2025-03-21  * Fix a bug in which the memory model would panic when attempting to unpack

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crucible-llvm-Version:       0.7.1+Version:       0.8.0.0 Author:        Galois Inc. Copyright:     (c) Galois, Inc 2014-2022 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com@@ -29,18 +29,108 @@   ghc-prof-options: -O2 -fprof-auto-exported   default-language: Haskell2010 +common warns+  -- Specifying -Wall and -Werror can cause the project to fail to build on+  -- newer versions of GHC simply due to new warnings being added to -Wall. To+  -- prevent this from happening we manually list which warnings should be+  -- considered errors. We also list some warnings that are not in -Wall, though+  -- try to avoid "opinionated" warnings (though this judgement is clearly+  -- subjective).+  --+  -- Warnings are grouped by the GHC version that introduced them, and then+  -- alphabetically.+  --+  -- A list of warnings and the GHC version in which they were introduced is+  -- available here:+  -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html +  -- Since GHC 9.6 or earlier:+  ghc-options:+    -Wall+    -Werror=ambiguous-fields+    -Werror=compat-unqualified-imports+    -Werror=deferred-type-errors+    -Werror=deprecated-flags+    -Werror=deprecations+    -Werror=deriving-defaults+    -Werror=deriving-typeable+    -Werror=dodgy-foreign-imports+    -Werror=duplicate-exports+    -Werror=empty-enumerations+    -Werror=gadt-mono-local-binds+    -Werror=identities+    -Werror=inaccessible-code+    -Werror=incomplete-patterns+    -Werror=incomplete-record-updates+    -Werror=incomplete-uni-patterns+    -Werror=inline-rule-shadowing+    -Werror=misplaced-pragmas+    -Werror=missed-extra-shared-lib+    -Werror=missing-exported-signatures+    -Werror=missing-fields+    -Werror=missing-home-modules+    -Werror=missing-methods+    -Werror=missing-pattern-synonym-signatures+    -Werror=missing-signatures+    -Werror=name-shadowing+    -Werror=noncanonical-monad-instances+    -Werror=noncanonical-monoid-instances+    -Werror=operator-whitespace+    -Werror=operator-whitespace-ext-conflict+    -Werror=orphans+    -Werror=overflowed-literals+    -Werror=overlapping-patterns+    -Werror=partial-fields+    -Werror=partial-type-signatures+    -Werror=redundant-bang-patterns+    -Werror=redundant-record-wildcards+    -Werror=redundant-strictness-flags+    -Werror=simplifiable-class-constraints+    -Werror=star-binder+    -Werror=star-is-type+    -Werror=tabs+    -Werror=type-defaults+    -Werror=typed-holes+    -Werror=type-equality-out-of-scope+    -Werror=type-equality-requires-operators+    -Werror=unicode-bidirectional-format-characters+    -Werror=unrecognised-pragmas+    -Werror=unrecognised-warning-flags+    -Werror=unsupported-calling-conventions+    -Werror=unsupported-llvm-version+    -Werror=unused-do-bind+    -Werror=unused-imports+    -Werror=unused-record-wildcards+    -Werror=warnings-deprecations+    -Werror=wrong-do-bind++  if impl(ghc < 9.8)+    ghc-options:+      -Werror=forall-identifier++  if impl(ghc >= 9.8)+    ghc-options:+      -Werror=incomplete-export-warnings+      -Werror=inconsistent-flags++  if impl(ghc >= 9.10)+    ghc-options:+      -Werror=badly-staged-types+      -Werror=data-kinds-tc+      -Werror=deprecated-type-abstractions+      -Werror=incomplete-record-selectors+ library   import: bldflags   build-depends:-    base >= 4.13 && < 4.20,+    base >= 4.13 && < 4.21,     attoparsec,     bv-sized >= 1.0.0,     bytestring,     containers >= 0.5.8.0,     crucible >= 0.5,     crucible-symio,-    what4 >= 0.4.1,+    what4 >= 0.5,     extra,     lens,     itanium-abi >= 0.1.1.1 && < 0.2,@@ -73,6 +163,7 @@     Lang.Crucible.LLVM.Extension     Lang.Crucible.LLVM.Functions     Lang.Crucible.LLVM.Globals+    Lang.Crucible.LLVM.Internal     Lang.Crucible.LLVM.Intrinsics     Lang.Crucible.LLVM.Intrinsics.Cast     Lang.Crucible.LLVM.Intrinsics.Libc@@ -85,6 +176,7 @@     Lang.Crucible.LLVM.MemModel.MemLog     Lang.Crucible.LLVM.MemModel.Partial     Lang.Crucible.LLVM.MemModel.Pointer+    Lang.Crucible.LLVM.MemModel.Strings     Lang.Crucible.LLVM.MemType     Lang.Crucible.LLVM.PrettyPrint     Lang.Crucible.LLVM.Printf@@ -124,6 +216,7 @@  test-suite crucible-llvm-tests   import: bldflags+  import: warns   type: exitcode-stdio-1.0   main-is: Tests.hs   hs-source-dirs: test

@@ -164,6 +164,7 @@ data DataLayout    = DL { _intLayout :: EndianForm         , _stackAlignment :: !Alignment+        , _functionPtrAlignment :: !Alignment         , _ptrSize     :: !Bytes         , _ptrAlign    :: !Alignment         , _integerInfo :: !AlignInfo@@ -184,6 +185,10 @@ stackAlignment :: Lens' DataLayout Alignment stackAlignment = lens _stackAlignment (\s v -> s { _stackAlignment = v}) +functionPtrAlignment :: Lens' DataLayout Alignment+functionPtrAlignment =+  lens _functionPtrAlignment (\s v -> s { _functionPtrAlignment = v})+ -- | Size of pointers in bytes. ptrSize :: Lens' DataLayout Bytes ptrSize = lens _ptrSize (\s v -> s { _ptrSize = v})@@ -238,6 +243,7 @@ defaultDataLayout = execState defaults dl   where dl = DL { _intLayout = BigEndian                 , _stackAlignment = noAlignment+                , _functionPtrAlignment = noAlignment                 , _ptrSize  = 8 -- 64 bit pointers = 8 bytes                 , _ptrAlign = Alignment 3 -- 64 bit alignment: 2^3=8 byte boundaries                 , _integerInfo = emptyAlignInfo@@ -269,6 +275,7 @@ maxAlignment :: DataLayout -> Alignment maxAlignment dl =   maximum [ dl^.stackAlignment+          , dl^.functionPtrAlignment           , dl^.ptrAlign           , maxAlignmentInTree (dl^.integerInfo)           , maxAlignmentInTree (dl^.vectorInfo)@@ -322,6 +329,13 @@       L.StackObjSize   sz a _ -> setAtBits stackInfo   ls sz a       L.NativeIntSize _ -> return ()       L.StackAlign a    -> setBits stackAlignment ls a+      -- TODO: For now, we ignore the FunctionPointerAlignType field. This tells+      -- us whether the function pointer alignment is related to the alignment+      -- of functions, but llvm-pretty currently does not track the alignment of+      -- individual functions, so we have no use for this info just yet. When+      -- https://github.com/GaloisInc/llvm-pretty/issues/164 is implemented, we+      -- should revisit this.+      L.FunctionPointerAlign _ a -> setBits functionPtrAlignment ls a       L.Mangling _      -> return ()  -- | Create parsed data layout from layout spec AST.

@@ -6,6 +6,7 @@ -- Maintainer       : Langston Barrett <lbarrett@galois.com> -- Stability        : provisional --+-- See @crucible-llvm-cli/test-data/ub@ for tests demonstrating some of these. --------------------------------------------------------------------------  {-# LANGUAGE DataKinds #-}

@@ -20,6 +20,8 @@ -- code essentially have an additional hypothesis: that the LLVM -- compiler/hardware platform behave identically to Crucible's simulator when -- encountering such behavior.+--+-- See @crucible-llvm-cli/test-data/ub@ for tests demonstrating some of these. --------------------------------------------------------------------------  {-# LANGUAGE DataKinds #-}

@@ -46,7 +46,8 @@ import           Control.Monad.IO.Class (MonadIO(..)) import           Control.Monad.Except (MonadError(..)) import           Control.Lens hiding (op, (:>) )-import           Data.List (foldl', genericLength, isPrefixOf)+import qualified Data.Foldable as Foldable+import           Data.List (genericLength, isPrefixOf) import           Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import qualified Data.Set as Set@@ -107,7 +108,7 @@               => LLVMContext arch               -> L.Module               -> GlobalInitializerMap-makeGlobalMap ctx m = foldl' addAliases globalMap1 (Map.toList (llvmGlobalAliases ctx))+makeGlobalMap ctx m = Foldable.foldl' addAliases globalMap1 (Map.toList (llvmGlobalAliases ctx))    where    addAliases mp (glob, aliases) =

@@ -0,0 +1,25 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeApplications #-}++-- | Items in this module should /not/ be considered part of Crucible-LLVM's+-- API, they are exported only for the sake of the test suite.+module Lang.Crucible.LLVM.Internal+  ( assertionsEnabled+  ) where++import qualified Control.Exception as X+import           Data.Functor ((<&>))++-- | Check if assertions are enabled.+--+-- Note [Asserts]: When optimizations are enabled, GHC compiles 'X.assert' to+-- a no-op. However, Cabal enables @-O1@ by default. Therefore, if we want our+-- assertions to be checked by our test suite, we must carefully ensure that we+-- pass the correct flags to GHC for the @lib:crucible-llvm@ target. We verify+-- that we have done so by asserting as much in the test suite.+assertionsEnabled :: IO Bool+assertionsEnabled = do+  X.try @X.AssertionFailed (X.assert False (pure ())) <&>+    \case+      Left _ -> True+      Right () -> False

@@ -26,6 +26,7 @@ , register_llvm_overrides , register_llvm_overrides_ , llvmDeclToFunHandleRepr+, declare_overrides  , module Lang.Crucible.LLVM.Intrinsics.Common , module Lang.Crucible.LLVM.Intrinsics.Options

@@ -307,6 +307,23 @@     , Poly1VecLLVMOverride $ \vecSz intSz ->         SomeLLVMOverride (llvmVectorReduceUmin vecSz intSz)     )++  , ("llvm.smax"+    , Poly1VecLLVMOverride $ \vecSz intSz ->+        SomeLLVMOverride (llvmSmaxVector vecSz intSz)+    )+  , ("llvm.smin"+    , Poly1VecLLVMOverride $ \vecSz intSz ->+        SomeLLVMOverride (llvmSminVector vecSz intSz)+    )+  , ("llvm.umax"+    , Poly1VecLLVMOverride $ \vecSz intSz ->+        SomeLLVMOverride (llvmUmaxVector vecSz intSz)+    )+  , ("llvm.umin"+    , Poly1VecLLVMOverride $ \vecSz intSz ->+        SomeLLVMOverride (llvmUminVector vecSz intSz)+    )   ]  ------------------------------------------------------------------------@@ -1469,6 +1486,67 @@         (BVType intSz) llvmVectorReduceUmin = llvmVectorReduce "umin" callVectorReduceUmin +-- | Build an 'LLVMOverride' for a vector map intrinsic.+llvmVectorMap ::+  (1 <= intSz) =>+  -- | The name of the operation to map (@umin@, @smin@, etc.).+  String ->+  -- | The semantics of the override.+  (forall r args ret.+    IsSymInterface sym =>+    RegEntry sym (VectorType (BVType intSz)) ->+    RegEntry sym (VectorType (BVType intSz)) ->+    OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))) ->+  -- | The size of the vector type.+  NatRepr vecSz ->+  -- | The size of the integer type.+  NatRepr intSz ->+  LLVMOverride p sym ext+    (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))+    (VectorType (BVType intSz))+llvmVectorMap opName callMap vecSz intSz =+  let nm = L.Symbol ("llvm." ++ opName +++                     ".v" ++ show (natValue vecSz) +++                     "i" ++ show (natValue intSz)) in+    [llvmOvr| <#vecSz x #intSz> $nm( <#vecSz x #intSz>, <#vecSz x #intSz> ) |]+    (\_memOps args -> Ctx.uncurryAssignment callMap args)++llvmSmaxVector ::+  (1 <= intSz) =>+  NatRepr vecSz ->+  NatRepr intSz ->+  LLVMOverride p sym ext+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))+     (VectorType (BVType intSz))+llvmSmaxVector = llvmVectorMap "smax" callVectorMapSmax++llvmSminVector ::+  (1 <= intSz) =>+  NatRepr vecSz ->+  NatRepr intSz ->+  LLVMOverride p sym ext+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))+     (VectorType (BVType intSz))+llvmSminVector = llvmVectorMap "smin" callVectorMapSmin++llvmUmaxVector ::+  (1 <= intSz) =>+  NatRepr vecSz ->+  NatRepr intSz ->+  LLVMOverride p sym ext+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))+     (VectorType (BVType intSz))+llvmUmaxVector = llvmVectorMap "umax" callVectorMapUmax++llvmUminVector ::+  (1 <= intSz) =>+  NatRepr vecSz ->+  NatRepr intSz ->+  LLVMOverride p sym ext+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))+     (VectorType (BVType intSz))+llvmUminVector = llvmVectorMap "umin" callVectorMapUmin+ ------------------------------------------------------------------------ -- ** Implementations @@ -1933,8 +2011,8 @@ callIsFpclass regOp@(regValue -> op) (regValue -> test) = do   sym <- getSymInterface   let w1 = knownNat @1-  bv1 <- liftIO $ bvZero sym w1-  bv0 <- liftIO $ bvOne sym w1+  bv1 <- liftIO $ bvOne sym w1+  bv0 <- liftIO $ bvZero sym w1    let negative bit = liftIO $ do         isNeg <- iFloatIsNeg @_ @fi sym op@@ -2140,3 +2218,52 @@   sym <- getSymInterface   umax <- liftIO $ maxUnsignedBV sym intSz   callVectorReduce (bvUmin sym) umax vec++-- | The semantics of an LLVM vector map intrinsic.+callVectorMap ::+  -- | The operation to apply when mapping (e.g., @umin@, @smin@, etc.)+  (RegValue sym tp -> RegValue sym tp -> IO (RegValue sym tp)) ->+  -- | The first vector to map over.+  RegEntry sym (VectorType tp) ->+  -- | The second vector to map over.+  RegEntry sym (VectorType tp) ->+  -- | The result of mapping over the vectors.+  OverrideSim p sym ext r args ret (V.Vector (RegValue sym tp))+callVectorMap mapOp (regValue -> vec1) (regValue -> vec2) =+  liftIO $ V.zipWithM mapOp vec1 vec2++callVectorMapSmax ::+  (IsSymInterface sym, 1 <= intSz) =>+  RegEntry sym (VectorType (BVType intSz)) ->+  RegEntry sym (VectorType (BVType intSz)) ->+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))+callVectorMapSmax vec1 vec2 = do+  sym <- getSymInterface+  callVectorMap (bvSmax sym) vec1 vec2++callVectorMapSmin ::+  (IsSymInterface sym, 1 <= intSz) =>+  RegEntry sym (VectorType (BVType intSz)) ->+  RegEntry sym (VectorType (BVType intSz)) ->+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))+callVectorMapSmin vec1 vec2 = do+  sym <- getSymInterface+  callVectorMap (bvSmin sym) vec1 vec2++callVectorMapUmax ::+  (IsSymInterface sym, 1 <= intSz) =>+  RegEntry sym (VectorType (BVType intSz)) ->+  RegEntry sym (VectorType (BVType intSz)) ->+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))+callVectorMapUmax vec1 vec2 = do+  sym <- getSymInterface+  callVectorMap (bvUmax sym) vec1 vec2++callVectorMapUmin ::+  (IsSymInterface sym, 1 <= intSz) =>+  RegEntry sym (VectorType (BVType intSz)) ->+  RegEntry sym (VectorType (BVType intSz)) ->+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))+callVectorMapUmin vec1 vec2 = do+  sym <- getSymInterface+  callVectorMap (bvUmin sym) vec1 vec2

@@ -65,6 +65,7 @@ import qualified Lang.Crucible.LLVM.MemModel.Generic as G import           Lang.Crucible.LLVM.MemModel.Partial import qualified Lang.Crucible.LLVM.MemModel.Pointer as Ptr+import           Lang.Crucible.LLVM.MemModel.Strings as CStr import           Lang.Crucible.LLVM.Printf import           Lang.Crucible.LLVM.QQ( llvmOvr ) import           Lang.Crucible.LLVM.TypeContext@@ -596,7 +597,7 @@   (regValue -> strPtr) =     ovrWithBackend $ \bak -> do       mem <- readGlobal mvar-      str <- liftIO $ loadString bak mem strPtr Nothing+      str <- liftIO $ CStr.loadString bak mem strPtr Nothing       h <- printHandle <$> getContext       liftIO $ hPutStrLn h (UTF8.toString str)       -- return non-negative value on success@@ -629,7 +630,7 @@     let sym = backendGetSym bak     when failUponExit $       do mem <- readGlobal mvar-         txt <- liftIO $ loadString bak mem (regValue ptxt) Nothing+         txt <- liftIO $ CStr.loadString bak mem (regValue ptxt) Nothing          let err = AssertFailureSimError "Call to assert()" (UTF8.toString txt)          liftIO $ addFailedAssertion bak err     liftIO $@@ -667,7 +668,7 @@   (regValue -> valist) =     ovrWithBackend $ \bak -> do       mem <- readGlobal mvar-      formatStr <- liftIO $ loadString bak mem strPtr Nothing+      formatStr <- liftIO $ CStr.loadString bak mem strPtr Nothing       case parseDirectives formatStr of         Left err -> overrideError $ AssertFailureSimError "Format string parsing failed" err         Right ds -> do@@ -731,7 +732,7 @@      case valist V.!? (i-1) of        Just (AnyValue PtrRepr ptr) ->            do mem <- get-              liftIO $ loadString bak mem ptr numchars+              liftIO $ CStr.loadString bak mem ptr numchars        Just (AnyValue tpr _) ->          lift $ addFailedAssertion bak               $ AssertFailureSimError

@@ -83,9 +83,15 @@   , doArrayStoreUnbounded   , doArrayConstStore   , doArrayConstStoreUnbounded-  , loadString-  , loadMaybeString-  , strLen+  -- TODO(#1308): When GHC 9.6 support is dropped, deprecate these imports+  -- TOOD(#1406): After they have been deprecated for a while, move the+  -- implementations to `Strings` and remove these exports.+  , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-}+    loadString+  , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-}+    loadMaybeString+  , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-}+    strLen   , uncheckedMemcpy      -- * \"Raw\" operations with LLVMVal

@@ -467,8 +467,10 @@         let d = lo - so         -- Store is before load.         valueLoad lo ltp lo (SelectSuffixBV d (sw - d) v)-      | otherwise -> assert (lo == so && lw < sw) $+      | otherwise ->+        -- TODO(#1560): This assertion can fail.         -- Load ends before store ends.+        -- assert (lo == so && lw < sw) $         valueLoad lo ltp so (SelectPrefixBV lw (sw - lw) v)     Float -> valueLoad lo ltp so (FloatToBV v)     Double -> valueLoad lo ltp so (DoubleToBV v)@@ -511,8 +513,10 @@   ValueView {- ^ view of stored value -} ->   ValueCtor (ValueLoad Addr) valueLoad lo ltp so v-  | le <= so = ValueCtorVar (OldMemory lo ltp) -- Load ends before store-  | se <= lo = ValueCtorVar (OldMemory lo ltp) -- Store ends before load+  -- The non-zero test ensures that 0-byte loads are always overlapping+  -- with the most recent store so that they're not spuriously rejected.+  | le <= so && nonZeroLoad = ValueCtorVar (OldMemory lo ltp) -- Load ends before store+  | se <= lo && nonZeroLoad = ValueCtorVar (OldMemory lo ltp) -- Store ends before load     -- Load is before store.   | lo < so  = splitTypeValue ltp (so - lo) (\o tp -> valueLoad (lo+o) tp so v)     -- Load ends after store ends.@@ -534,6 +538,7 @@  where stp = fromMaybe (error ("Coerce value given bad view " ++ show v)) (viewType v)        le = typeEnd lo ltp        se = so + storageTypeSize stp+       nonZeroLoad = le - lo > 0  -- | @LinearLoadStoreOffsetDiff stride delta@ represents the fact that --   the difference between the load offset and the store offset is

@@ -76,6 +76,7 @@  import           Prelude hiding (pred) +import qualified Control.Exception as X import           Control.Lens import           Control.Monad import           Control.Monad.State.Strict@@ -91,6 +92,7 @@ import           Numeric.Natural import           Prettyprinter import           Lang.Crucible.Panic (panic)+import qualified Data.Vector as V  import           Data.BitVector.Sized (BV) import qualified Data.BitVector.Sized as BV@@ -695,6 +697,21 @@       | otherwise       = liftIO (Partial.partErr sym mop $ Invalidated msg) +-- | Construct a value of a type that has no in-memory representation at all+buildEmptyVal :: StorageType -> Maybe (LLVMVal sym)+buildEmptyVal t =+  case storageTypeF t of+    Struct fields   -> LLVMValStruct <$> traverse emptyStorageField fields+    Array n eltTy+      | n == 0      -> Just (LLVMValArray eltTy V.empty)+      | otherwise   -> LLVMValArray eltTy . V.replicate (fromIntegral n) <$> buildEmptyVal eltTy+    X86_FP80        -> Nothing+    Float           -> Nothing+    Double          -> Nothing+    Bitvector {}    -> Nothing -- Bitvectors can't be empty; they have a non-zero size invariant+  where+    emptyStorageField field = (,) field <$> buildEmptyVal (field ^. fieldVal)+ -- | Read a value from memory. readMem :: forall sym w.   ( 1 <= w, IsSymInterface sym, HasLLVMAnn sym@@ -707,6 +724,12 @@   Alignment ->   Mem sym ->   IO (PartLLVMVal sym)+readMem sym _ _ _ tp _ _+  -- no actual memory read happens when reading a value with+  -- no memory representation. This check comes up in+  -- particular when evaluating llvm_points_to statements+  -- in SAW script.+  | Just v <- buildEmptyVal tp = pure (Partial.totalLLVMVal sym v) readMem sym w gsym l tp alignment m = do   sz         <- bvLit sym w (bytesToBV w (typeEnd 0 tp))   p1         <- isAllocated sym w alignment l (Just sz) m@@ -1584,21 +1607,43 @@     isHeapMutable (AllocInfo HeapAlloc _ Mutable _ _) = pure (truePred sym)     isHeapMutable _ = pure (falsePred sym) +-- | Prepare memory so that it can later be merged via 'mergeMem'.+--+-- This is primarily intended for use in the implementation of+-- 'Lang.Crucible.Simulator.Intrinsics.pushBranchIntrinsic' for LLVM memory.+-- It would be nice to remove this someday, see #890.+--+-- For more information about branching and merging, see the comment on 'Mem'. branchMem :: Mem sym -> Mem sym branchMem = memState %~ \s ->   BranchFrame (memStateAllocCount s) (memStateWriteCount s) emptyChanges s +-- | Remove the top 'BranchFrame', adding changes to the underlying memory.+--+-- This is primarily intended for use in the implementation of+-- 'Lang.Crucible.Simulator.Intrinsics.abortBranchIntrinsic' for LLVM memory. branchAbortMem :: Mem sym -> Mem sym branchAbortMem = memState %~ popf   where popf (BranchFrame _ _ c s) = s & memStateAddChanges c         popf _ = error "branchAbortMem given unexpected memory" +-- | Merge memory that was previously prepared via 'branchMem'.+--+-- This is primarily intended for use in the implementation of+-- 'Lang.Crucible.Simulator.Intrinsics.muxIntrinsic' for LLVM memory.+--+-- For more information about branching and merging, see the comment on 'Mem'. mergeMem :: IsExpr (SymExpr sym) => Pred sym -> Mem sym -> Mem sym -> Mem sym mergeMem c x y =   case (x^.memState, y^.memState) of-    (BranchFrame _ _ a s, BranchFrame _ _ b _) ->-      let s' = s & memStateAddChanges (muxChanges c a b)-      in x & memState .~ s'+    (BranchFrame _ _ a s, BranchFrame _ _ b s') ->+      -- The memories to be merged must have originated from the same memory,+      -- and in particular, should have matching alloc/write counts.+      let allocsEq = memStateAllocCount s == memStateAllocCount s' in+      let writesEq = memStateWriteCount s == memStateWriteCount s' in+      X.assert (allocsEq && writesEq) $+        let s' = s & memStateAddChanges (muxChanges c a b)+        in x & memState .~ s'     _ -> error "mergeMem given unexpected memories"  --------------------------------------------------------------------------------

@@ -344,8 +344,12 @@     -- of the list.   | StackFrame !Int !Int Text (MemChanges sym) (MemState sym)     -- | Represents a push of a branch frame, and changes since that branch.+    --     -- Changes are stored in order, with more recent changes closer to the head     -- of the list.+    --+    -- For more information about branching and merging, see the comment on+    -- 'Mem'.   | BranchFrame !Int !Int (MemChanges sym) (MemState sym)  type MemChanges sym = (MemAllocs sym, MemWrites sym)

@@ -0,0 +1,367 @@+-- TODO(#1406): Move the definitions of the deprecated imports into this module,+-- and remove the exports from MemModel.+{-# OPTIONS_GHC -Wno-warnings-deprecations #-}++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++-- | Manipulating C-style null-terminated strings+module Lang.Crucible.LLVM.MemModel.Strings+  ( Mem.loadString+  , Mem.loadMaybeString+  , Mem.strLen+  , loadConcretelyNullTerminatedString+  , loadSymbolicString+  , storeString+  -- * Low-level string loading primitives+  -- ** 'ByteChecker'+  , ControlFlow(..)+  , ByteChecker(..)+  , fullyConcreteNullTerminatedString+  , concretelyNullTerminatedString+  , nullTerminatedString+  , withMaxChars+  -- ** 'ByteLoader'+  , ByteLoader(..)+  , llvmByteLoader+  -- ** 'loadBytes'+  , loadBytes+  ) where++import           Data.Bifunctor (Bifunctor(bimap, first))+import           Control.Monad.IO.Class (MonadIO, liftIO)+import qualified Data.BitVector.Sized as BV+import           Data.Functor ((<&>))+import qualified Data.Parameterized.NatRepr as DPN+import           Data.Word (Word8)+import qualified Data.Vector as Vec+import qualified GHC.Stack as GHC+import qualified Lang.Crucible.Backend as LCB+import qualified Lang.Crucible.Backend.Online as LCBO+import qualified Lang.Crucible.Simulator as LCS+import qualified Lang.Crucible.LLVM.DataLayout as CLD+import qualified Lang.Crucible.LLVM.MemModel as LCLM+import qualified Lang.Crucible.LLVM.MemModel as Mem+import qualified Lang.Crucible.LLVM.MemModel.Partial as Partial+import qualified What4.Expr.Builder as WEB+import qualified What4.Interface as WI+import qualified What4.Protocol.Online as WPO+import qualified What4.SatResult as WS++-- | Load a null-terminated string (with a concrete null terminator) from memory.+--+-- The string must contain a concrete null terminator. If a maximum number of+-- characters is provided, no more than that number of characters will be read.+-- In either case, 'loadConcretelyNullTerminatedString' will stop reading if it+-- encounters a (concretely) null terminator.+--+-- Note that the loaded string may actually be smaller than the returned list if+-- any of the symbolic bytes are equal to 0.+loadConcretelyNullTerminatedString ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  -- | Maximum number of characters to read+  Maybe Int ->+  IO [WI.SymBV sym 8]+loadConcretelyNullTerminatedString bak mem ptr limit =+  let loader = llvmByteLoader mem in+  case limit of+    Nothing -> loadBytes bak mem id ptr loader concretelyNullTerminatedString+    Just l ->+      let byteChecker = withMaxChars l (\f -> pure (f [])) concretelyNullTerminatedString in+      loadBytes bak mem (id, 0) ptr loader byteChecker++-- | Load a null-terminated string from memory.+--+-- Consults an SMT solver to check if any of the loaded bytes are known to be+-- null (0). If a maximum number of characters is provided, no more than that+-- number of charcters will be read. In either case, 'loadSymbolicString' will+-- stop reading if it encounters a null terminator.+--+-- Note that the loaded string may actually be smaller than the returned list if+-- any of the symbolic bytes are equal to 0.+loadSymbolicString ::+  ( LCB.IsSymBackend sym bak+  , sym ~ WEB.ExprBuilder scope st fs+  , bak ~ LCBO.OnlineBackend solver scope st fs+  , WPO.OnlineSolver solver+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  -- | Maximum number of characters to read+  Maybe Int ->+  IO [WI.SymBV sym 8]+loadSymbolicString bak mem ptr limit =+  let loader = llvmByteLoader mem in+  case limit of+    Nothing -> loadBytes bak mem id ptr loader nullTerminatedString+    Just l ->+      let byteChecker = withMaxChars l (\f -> pure (f [])) nullTerminatedString in+      loadBytes bak mem (id, 0) ptr loader byteChecker++-- | Store a string to memory, adding a null terminator at the end.+storeString ::+  forall sym bak w.+  ( LCB.IsSymBackend sym bak+  , WI.IsExpr (WI.SymExpr sym)+  , LCLM.HasPtrWidth w+  , LCLM.HasLLVMAnn sym+  , ?memOpts :: LCLM.MemOptions+  ) =>+  bak ->+  LCLM.MemImpl sym ->+  -- | Pointer to write string to+  LCLM.LLVMPtr sym w ->+  -- | The bytes of the string to write (null terminator not included)+  Vec.Vector (WI.SymBV sym 8) ->+  IO (LCLM.MemImpl sym)+storeString bak mem ptr bytesBvs = do+  let sym = LCB.backendGetSym bak+  zeroNat <- WI.natLit sym 0+  let bytes = Vec.map (Mem.LLVMValInt zeroNat) bytesBvs+  zeroByte <- Mem.LLVMValInt zeroNat <$> WI.bvZero sym (DPN.knownNat @8)+  let nullTerminatedBytes = Vec.snoc bytes zeroByte+  let val = Mem.LLVMValArray (Mem.bitvectorType 1) nullTerminatedBytes+  let storTy = Mem.llvmValStorableType @sym val+  Mem.storeRaw bak mem ptr storTy CLD.noAlignment val++---------------------------------------------------------------------+-- * Low-level string loading primitives++---------------------------------------------------------------------+-- ** 'ByteChecker'++-- | Whether to stop or keep going+--+-- Like Rust's @std::ops::ControlFlow@.+data ControlFlow a b+  = Continue a+  | Break b+  deriving Functor++-- NB: 'first' is used in this module+instance Bifunctor ControlFlow where+  bimap l r =+    \case+      Continue x -> Continue (l x)+      Break x -> Break (r x)++-- | Compute a result from a symbolic byte, and check if the load should+-- continue to the next byte.+--+-- Used to:+--+-- * Check if the byte is concrete ('fullyConcreteNullTerminatedString')+-- * Check if the byte is concretely a null terminator+--   ('concretelyNullTerminatedString')+-- * Check if a byte is known by a solver to be a null terminator ('nullTerminatedString')+-- * Check if we have surpassed a length limit ('withMaxChars')+--+-- Note that it is relatively common for @a@ to be a function @[b] -> [b]@. This+-- is used to build up a snoc-list.+newtype ByteChecker m sym bak a b+  = ByteChecker { runByteChecker :: bak -> a -> Mem.LLVMPtr sym 8 -> m (ControlFlow a b) }++-- Helper, not exported+ptrToBv8 ::+  LCB.IsSymBackend sym bak =>+  bak ->+  Mem.LLVMPtr sym 8 ->+  IO (WI.SymBV sym 8)+ptrToBv8 bak bytePtr = do+  let err = LCS.AssertFailureSimError "Found pointer instead of byte when loading string" ""+  Partial.ptrToBv bak err bytePtr++-- | 'ByteChecker' for loading concrete strings.+--+-- Currently unused internally, but analogous with+-- 'Lang.Crucible.LLVM.MemModel.loadString'. In fact, it would be good to define+-- that function in terms of this one. However, this is blocked on TODO(#1406).+fullyConcreteNullTerminatedString ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  ByteChecker m sym bak ([Word8] -> [Word8]) [Word8]+fullyConcreteNullTerminatedString =+  ByteChecker $ \bak acc bytePtr -> do+    byte <- liftIO (ptrToBv8 bak bytePtr)+    case BV.asUnsigned <$> WI.asBV byte of+      Just 0 -> pure (Break (acc []))+      Just c -> do+        let c' = toEnum @Word8 (fromInteger c)+        pure (Continue (\l -> acc (c' : l)))+      Nothing -> do+        let msg = "Symbolic value encountered when loading a string"+        liftIO (LCB.addFailedAssertion bak (LCS.Unsupported GHC.callStack msg))++-- | 'ByteChecker' for loading symbolic strings with a concrete null terminator.+--+-- Used in 'loadConcretelyNullTerminatedString'.+concretelyNullTerminatedString ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  ByteChecker m sym bak ([WI.SymBV sym 8] -> [WI.SymBV sym 8]) [WI.SymBV sym 8]+concretelyNullTerminatedString =+  ByteChecker $ \bak acc bytePtr -> do+    byte <- liftIO (ptrToBv8 bak bytePtr)+    if isConcreteNullTerminator byte+    then pure (Break (acc []))+    else  pure (Continue (\l -> acc (byte : l)))+  where+    isConcreteNullTerminator symByte =+      case BV.asUnsigned <$> WI.asBV symByte of+        Just 0 -> True+        _ -> False++-- | 'ByteChecker' for loading symbolic strings with a null terminator.+--+-- Used in 'loadSymbolicString'.+nullTerminatedString ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  sym ~ WEB.ExprBuilder scope st fs =>+  bak ~ LCBO.OnlineBackend solver scope st fs =>+  WPO.OnlineSolver solver =>+  ByteChecker m sym bak ([WI.SymBV sym 8] -> [WI.SymBV sym 8]) [WI.SymBV sym 8]+nullTerminatedString =+  ByteChecker $ \bak acc bytePtr -> do+    byte <- liftIO (ptrToBv8 bak bytePtr)+    let sym = LCB.backendGetSym bak+    isNullTerm <- liftIO (isNullTerminator bak sym byte)+    if isNullTerm+    then pure (Break (acc []))+    else  pure (Continue (\l -> acc (byte : l)))+  where+    isNullTerminator bak sym symByte =+      case BV.asUnsigned <$> WI.asBV symByte of+        Just 0 -> pure True+        Just _ -> pure False+        _ ->+          LCBO.withSolverProcess bak (pure False) $ \proc -> do+            z <- WI.bvZero sym (WI.knownNat @8)+            p <- WI.notPred sym =<< WI.bvEq sym z symByte+            WPO.checkSatisfiable proc "nullTerminatedString" p <&>+              \case+                WS.Unsat () -> True+                WS.Sat () -> False+                WS.Unknown -> False++-- | 'ByteChecker' for adding a maximum character length.+withMaxChars ::+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  Functor m =>+  -- | Maximum number of bytes to load+  Int ->+  -- | What to do when the maximum is reached+  (a -> m b) ->+  ByteChecker m sym bak a b ->+  ByteChecker m sym bak (a, Int) b+withMaxChars limit done checker =+  ByteChecker $ \bak (acc, i) bytePtr ->+    if i > limit+    then Break <$> done acc+    else first (, i + 1) <$> runByteChecker checker bak acc bytePtr++---------------------------------------------------------------------+-- ** 'ByteLoader'++-- | Load a byte from memory.+--+-- The only 'ByteLoader' defined here is 'llvmByteLoader', but Macaw users will+-- most often want one based on @doReadMemModel@.+newtype ByteLoader m sym bak wptr+  = ByteLoader { runByteLoader :: bak -> Mem.LLVMPtr sym wptr -> m (Mem.LLVMPtr sym 8) }++-- | A 'ByteLoader' for LLVM memory based on 'Mem.doLoad'.+llvmByteLoader ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  , MonadIO m+  ) =>+  Mem.MemImpl sym ->+  ByteLoader m sym bak wptr+llvmByteLoader mem =+  ByteLoader $ \bak ptr -> do+    let i1 = Mem.bitvectorType 1+    let p8 = Mem.LLVMPointerRepr (DPN.knownNat @8)+    liftIO (Mem.doLoad bak mem ptr i1 p8 CLD.noAlignment)++---------------------------------------------------------------------+-- * 'loadBytes'++-- | Load a sequence of bytes, one at a time.+--+-- Used to implement 'loadConcretelyNullTerminatedString' and+-- 'loadSymbolicString'. Highly customizable via 'ByteLoader' and 'ByteChecker'.+loadBytes ::+  forall m a b sym bak wptr.+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  , MonadIO m+  ) =>+  bak ->+  Mem.MemImpl sym ->+  -- | Initial accumulator+  a ->+  -- | Pointer to load from+  Mem.LLVMPtr sym wptr ->+  -- | How to load a byte from memory+  ByteLoader m sym bak wptr ->+  -- | How to check if we should continue loading the next byte+  ByteChecker m sym bak a b ->+  m b+loadBytes bak mem = go+ where+  sym = LCB.backendGetSym bak+  go ::+    a ->+    Mem.LLVMPtr sym wptr ->+    ByteLoader m sym bak wptr ->+    ByteChecker m sym bak a b ->+    m b+  go acc ptr loader checker = do+    byte <- runByteLoader loader bak ptr+    runByteChecker checker bak acc byte >>=+      \case+        Break result -> pure result+        Continue acc' -> do+          -- It is important that safety assertions for later loads can use+          -- the assumption that earlier bytes were nonzero, see #1463 or+          -- `crucible-llvm-cli/test-data/T1463-read-bytes.cbl` for details.+          prevByteWasNonNull <-+            liftIO (WI.notPred sym =<< Mem.ptrIsNull sym (WI.knownNat @8) byte)+          loc <- liftIO (WI.getCurrentProgramLoc sym)+          let assump = LCB.BranchCondition loc Nothing prevByteWasNonNull+          liftIO (LCB.addAssumption bak assump)++          ptr' <- liftIO (Mem.doPtrAddOffset bak mem ptr =<< WI.bvOne sym Mem.PtrWidth)+          go acc' ptr' loader checker 

@@ -108,7 +108,7 @@   LLVMValUndef :: StorageType -> LLVMVal sym  -llvmValStorableType :: IsExprBuilder sym => LLVMVal sym -> StorageType+llvmValStorableType :: IsExpr (SymExpr sym) => LLVMVal sym -> StorageType llvmValStorableType v =   case v of     LLVMValInt _ bv -> bitvectorType (bitsToBytes (natValue (bvWidth bv)))

@@ -102,6 +102,7 @@  import           Lang.Crucible.LLVM.Bytes (toBytes) import           Lang.Crucible.LLVM.MemModel+import qualified Lang.Crucible.LLVM.MemModel.Strings as CStr import           Lang.Crucible.LLVM.Extension ( ArchWidth ) import           Lang.Crucible.LLVM.DataLayout ( noAlignment ) import           Lang.Crucible.LLVM.Intrinsics@@ -380,7 +381,7 @@ loadFileIdent memOps filename_ptr =   ovrWithBackend $ \bak ->    do mem <- readGlobal memOps-      filename_bytes <- liftIO $ loadString bak mem filename_ptr Nothing+      filename_bytes <- liftIO $ CStr.loadString bak mem filename_ptr Nothing       liftIO $ W4.stringLit (backendGetSym bak) (W4.Char8Literal (BS.pack filename_bytes))  returnIOError32

@@ -25,7 +25,7 @@   ) where  import Data.Foldable (toList)-import Data.List (foldl')+import qualified Data.Foldable as Foldable import Data.Maybe import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map@@ -131,7 +131,7 @@  -- | Compute predecessor sets from the successor sets already computed in @buildBlockInfo@ updatePredSets :: LLVMBlockInfoMap s -> LLVMBlockInfoMap s-updatePredSets bim0 = foldl' upd bim0 predEdges+updatePredSets bim0 = Foldable.foldl' upd bim0 predEdges   where    upd bim (to,from) = Map.adjust (\bi -> bi{ block_pred_set = Set.insert from (block_pred_set bi) }) to bim 

@@ -41,12 +41,14 @@ import           Control.Lens hiding (op, (:>) ) import           Control.Monad (MonadPlus(..), forM, unless) import           Control.Monad.Except (MonadError(..), runExceptT)-import           Control.Monad.State.Strict (MonadState(..))+import           Control.Monad.State.Strict (MonadState(..), gets) import           Control.Monad.Trans.Class (MonadTrans(..)) import           Control.Monad.Trans.Maybe import           Data.Foldable (for_, toList) import           Data.Functor (void) import           Data.Int+import           Data.IntMap.Strict (IntMap)+import qualified Data.IntMap.Strict as IntMap import qualified Data.List as List import           Data.List.NonEmpty (NonEmpty((:|))) import qualified Data.Map.Strict as Map@@ -2079,31 +2081,81 @@      | otherwise = callOrdinaryFunction (Just instr) tailCall_ fnTy fn args assign_f  -- | Match the arguments used by @dbg.addr@, @dbg.declare@, and @dbg.value@.+-- For more information on how these work, see+-- <https://llvm.org/docs/SourceLevelDebugging.html>.++-- This function assumes that each argument should either be a particular kind+-- of metadata value or a reference that resolves to a particular kind of+-- metadata value (see @resolveArg{1,2,3}@ below). If we encounter other types+-- of LLVM metadata that breaks this assumption, then we will need to update+-- this function's implementation accordingly. dbgArgs ::   Set L.Ident {- ^ Set of usable identifiers -} ->   [L.Typed L.Value] {- ^ debug call arguments -} ->   LLVMGenerator s arch ret (Either String (LLVMExpr s arch, L.DILocalVariable, L.DIExpression))-dbgArgs defSet args =+dbgArgs defSet args = do+    unnamedMd <- gets (llvmUnnamedMd . llvmContext)     case args of-      [valArg, lvArg, diArg] ->-        case valArg of-          L.Typed _ (L.ValMd (L.ValMdValue val)) ->-            case lvArg of-              L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoLocalVariable lv))) ->-                case diArg of-                  L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoExpression di))) ->-                    let unusableIdents = Set.difference (useTypedVal val) defSet-                    in if Set.null unusableIdents then-                         do v <- transTypedValue val-                            pure (Right (v, lv, di))-                       else-                         do let msg = unwords (["dbg intrinsic def/use violation for:"] ++-                                       map (show . LPP.ppIdent) (Set.toList unusableIdents))-                            pure (Left msg)-                  _ -> pure (Left ("dbg: argument 3 expected DIExpression, got: " ++ show diArg))-              _ -> pure (Left ("dbg: argument 2 expected local variable metadata, got: " ++ show lvArg))-          _ -> pure (Left ("dbg: argument 1 expected value metadata, got: " ++ show valArg))+      [valArg, lvArg, diArg] -> do+        let resolveRes = do -- Either String+              val <- resolveArg1 unnamedMd $ L.typedValue valArg+              lv <- resolveArg2 unnamedMd $ L.typedValue lvArg+              di <- resolveArg3 unnamedMd $ L.typedValue diArg+              Right (val, lv, di)+        case resolveRes of+          Left err -> pure (Left err)+          Right (val, lv, di) ->+            let unusableIdents = Set.difference (useTypedVal val) defSet+            in if Set.null unusableIdents then+                 do v <- transTypedValue val+                    pure (Right (v, lv, di))+               else+                 do let msg = unwords (["dbg intrinsic def/use violation for:"] +++                               map (show . LPP.ppIdent) (Set.toList unusableIdents))+                    pure (Left msg)       _ -> pure (Left ("dbg: expected 3 arguments, got: " ++ show (length args)))+  where+    resolveArg1 ::+      IntMap L.ValMd ->+      L.Value ->+      Either String (L.Typed L.Value)+    resolveArg1 unnamedMd = go+      where+        go (L.ValMd (L.ValMdRef ref))+          | Just valMd <- IntMap.lookup ref unnamedMd+          = go (L.ValMd valMd)+        go (L.ValMd (L.ValMdValue val)) =+          Right val+        go valArg =+          Left ("dbg: argument 1 expected value metadata, got: " ++ show valArg)++    resolveArg2 ::+      IntMap L.ValMd ->+      L.Value ->+      Either String L.DILocalVariable+    resolveArg2 unnamedMd = go+      where+        go (L.ValMd (L.ValMdRef ref))+          | Just valMd <- IntMap.lookup ref unnamedMd+          = go (L.ValMd valMd)+        go (L.ValMd (L.ValMdDebugInfo (L.DebugInfoLocalVariable lv))) =+          Right lv+        go lvArg =+          Left ("dbg: argument 2 expected local variable metadata, got: " ++ show lvArg)++    resolveArg3 ::+      IntMap L.ValMd ->+      L.Value ->+      Either String L.DIExpression+    resolveArg3 unnamedMd = go+      where+        go (L.ValMd (L.ValMdRef ref))+          | Just valMd <- IntMap.lookup ref unnamedMd+          = go (L.ValMd valMd)+        go (L.ValMd (L.ValMdDebugInfo (L.DebugInfoExpression di))) =+          Right di+        go diArg =+          Left ("dbg: argument 3 expected DIExpression, got: " ++ show diArg)  typedValueAsCrucibleValue ::   L.Typed L.Value ->

@@ -53,6 +53,8 @@ import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.State.Strict (MonadState(..)) import Data.IORef (IORef, modifyIORef)+import Data.IntMap.Strict (IntMap)+import qualified Data.IntMap.Strict as IntMap import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Set (Set)@@ -95,6 +97,9 @@      -- | For each function symbol, compute the set of      --   aliases to that symbol    , llvmFunctionAliases :: Map L.Symbol (Set L.GlobalAlias)+     -- | Map the index of each piece of unnamed LLVM metadata to its value.+     -- This information is used to resolve the arguments to debug intrinsics.+   , llvmUnnamedMd :: IntMap L.ValMd    }  llvmTypeCtx :: Simple Lens (LLVMContext arch) TypeContext@@ -108,6 +113,8 @@   unless (null errs) $     malformedLLVMModule "Failed to construct LLVM type context" errs   let dl = llvmDataLayout typeCtx+  let unnamedMd =+        IntMap.fromList [(L.umIndex um, L.umValues um) | um <- L.modUnnamedMd m]    case mkNatRepr (ptrBitwidth dl) of     Some (wptr :: NatRepr wptr) | Just LeqProof <- testLeq (knownNat @16) wptr ->@@ -123,6 +130,7 @@                      , _llvmTypeCtx = typeCtx                      , llvmGlobalAliases = mempty   -- these are computed later                      , llvmFunctionAliases = mempty -- these are computed later+                     , llvmUnnamedMd = unnamedMd                      }            return (Some ctx)     _ ->

@@ -592,8 +592,8 @@                checkField bak' expectedBV actualPtrRV = do                  actualSymBV <- projectLLVM_bv bak' $ CS.unRV actualPtrRV                  Just expectedBV @=? What4.asBV actualSymBV-           checkField bak struct_bv1 (struct_val'^._1)-           checkField bak struct_bv2 (struct_val'^._2)+           checkField bak struct_bv1 (struct_val' ^. _1)+           checkField bak struct_bv2 (struct_val' ^. _2)       testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = False })      testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = True

@@ -9,7 +9,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} -module Main where+module Main (main) where  -- Crucible import           Lang.Crucible.FunctionHandle ( newHandleAllocator )@@ -46,7 +46,11 @@ import qualified System.IO as IO import qualified System.Process as Proc ++import qualified What4.Internal as WInt+ -- Modules being tested+import           Lang.Crucible.LLVM.Internal (assertionsEnabled) import           Lang.Crucible.LLVM.MemModel ( mkMemVar ) import           Lang.Crucible.LLVM.MemType import           Lang.Crucible.LLVM.Translation@@ -157,7 +161,15 @@         defaultMainWithIngredients llvmTestIngredients $          testGroup "Tests"-         [ functionTests+         [ -- See Note [Asserts] in crucible-llvm+           testCase "assertions enabled" $ do+             assertsEnabled <- assertionsEnabled+             assertBool "assertions should be enabled" assertsEnabled+         , -- See Note [Asserts] in what4+           testCase "What4 assertions enabled" $ do+             assertsEnabled <- WInt.assertionsEnabled+             assertBool "What4 assertions should be enabled" assertsEnabled+         , functionTests          , globalTests          , memoryTests          , translationTests