crucible-llvm 0.8.0.0 → 0.9

raw patch · 26 files changed

+1625/−484 lines, 26 filesdep ~llvm-prettyPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: llvm-pretty

API changes (from Hackage documentation)

Files

• CHANGELOG.md +47/−2
• crucible-llvm.cabal +2/−2
• src/Lang/Crucible/LLVM/DataLayout.hs +33/−29
• src/Lang/Crucible/LLVM/Errors/MemoryError.hs +0/−6
• src/Lang/Crucible/LLVM/Errors/Poison.hs +54/−2
• src/Lang/Crucible/LLVM/Errors/Standards.hs +9/−0
• src/Lang/Crucible/LLVM/Eval.hs +12/−0
• src/Lang/Crucible/LLVM/Extension/Syntax.hs +20/−70
• src/Lang/Crucible/LLVM/Globals.hs +4/−3
• src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs +192/−0
• src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +96/−0
• src/Lang/Crucible/LLVM/MemModel.hs +48/−14
• src/Lang/Crucible/LLVM/MemModel/MemLog.hs +3/−1
• src/Lang/Crucible/LLVM/MemModel/Partial.hs +18/−0
• src/Lang/Crucible/LLVM/MemModel/Pointer.hs +35/−2
• src/Lang/Crucible/LLVM/MemModel/Strings.hs +568/−69
• src/Lang/Crucible/LLVM/MemModel/Value.hs +21/−6
• src/Lang/Crucible/LLVM/MemType.hs +1/−1
• src/Lang/Crucible/LLVM/Translation.hs +79/−39
• src/Lang/Crucible/LLVM/Translation/BlockInfo.hs +4/−4
• src/Lang/Crucible/LLVM/Translation/Constant.hs +38/−38
• src/Lang/Crucible/LLVM/Translation/Expr.hs +117/−25
• src/Lang/Crucible/LLVM/Translation/Instruction.hs +107/−152
• src/Lang/Crucible/LLVM/Translation/Monad.hs +0/−8
• test/TestFunctions.hs +2/−1
• test/Tests.hs +115/−10

@@ -1,10 +1,55 @@+# 0.9 -- 2026-01-29++* The `LLVM_Debug` data constructor for `LLVMStmt`, as well as the related+  `LLVM_Dbg` data type, have been removed.+* Remove `aggInfo` in favor of `aggregateAlignment`, a lens that retrieves an+  `Alignment` instead of a full `AlignInfo`. In practice, `aggInfo` would only+  ever contain a single size (`0`) in its `AlignInfo`, and the concept of+  "size" doesn't really apply to aggregate alignments in data layout strings,+  so this was simplified to just be an `Alignment` instead.+* Support simulating bitcode that uses features from LLVM 19, including+  [debug records](https://llvm.org/docs/RemoveDIsDebugInfo.html) and+  [`getelementptr`+  attributes](https://releases.llvm.org/19.1.0/docs/LangRef.html#id237).+* Support the `nneg` flag in `zext` and `uitofp` instructions. If `nneg` is+  set, then converting a negative argument will yield a poisoned result.+* Support the `nuw` and `nsw` flags in `trunc` instructions. If `nuw` or `nsw`+  is set, then performing a truncation that would result in unsigned or signed+  integer overflow, respectively, will yield a poisoned result.+* Support the `samesign` flag in `icmp` instructions. If `samesign` is set, then+  comparing two integers of different signs will yield a poisoned result.+* Support the `llvm.tan`, `llvm.a{sin,cos,tan}`, `llvm.{sin,cos,tan}h`, and+  `llvm.atan2` floating-point intrinsics.+* Add extremely limited support for representing `poison` constants. For more+  details on the extent to which `crucible-llvm` can reason about `poison`, see+  `doc/limitations.md`.++  As part of these changes:++  * `LLVMVal` now features an additional `LLVMValPoison` data constructor.+  * `LLVMExpr` now features an additional `PoisonExpr` data constructor.+  * `LLVMConst` now features an addition `PoisonConst` data constructor.+  * `LLVMExtensionExpr` now features `LLVM_Poison{BV,Float}` data constructors,+    which represent primitive `poison` values.+* Remove the `Eq LLVMConst` instance. This instance was inherently unreliable+  because it cannot easily compute a simple `True`-or-`False` answer in the+  presence of `undef` or `poison` values.+* Replace `Data.Dynamic.Dynamic` with `SomeFnHandle` in+  `MemModel.{doInstallHandle,doLookupHandle}`.+* Add pretty-printing functions for use with `Lang.Crucible.Types.ppTypeRepr`+  * `Lang.Crucible.LLVM.MemModel.ppLLVMIntrinsicTypes`+  * `Lang.Crucible.LLVM.MemModel.ppLLVMMemIntrinsicType`+  * `Lang.Crucible.LLVM.MemModel.Pointer.ppLLVMPointerIntrinsicType`+* Overrides for `strnlen`, `strcpy`, `strdup`, and `strndup` supported by new+  APIs in `Lang.Crucible.LLVM.MemModel.Strings`.+ # 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`.+  `loadConcretelyNullTerminatedString` and `loadProvablyNullTerminatedString`. * Add a new "low-level" API for loading strings to   `Lang.Crucible.LLVM.MemModel.Strings`: `ByteLoader`, `ByteChecker`, and   `loadBytes`.@@ -70,7 +115,7 @@   * `Lang.Crucible.LLVM.Globals`: `populateGlobal`   * `Lang.Crucible.LLVM.MemModel.Generic`: `writeMem` and `writeConstMem` * `Lang.Crucible.LLVM`: `registerModuleFn` has changed type to-  accomodate lazy loading of Crucible IR.+  accommodate lazy loading of Crucible IR. * `Lang.Crucible.LLVM.Translation` : The `ModuleTranslation` record is   now opaque, the `cfgMap` is no longer exported and `globalInitMap`   and `modTransNonce` have become lens-style getters instead of record

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crucible-llvm-Version:       0.8.0.0+Version:       0.9 Author:        Galois Inc. Copyright:     (c) Galois, Inc 2014-2022 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com@@ -134,7 +134,7 @@     extra,     lens,     itanium-abi >= 0.1.1.1 && < 0.2,-    llvm-pretty >= 0.12.1 && < 0.14,+    llvm-pretty >= 0.12.1 && < 0.15,     mtl,     parameterized-utils >= 2.1.5 && < 2.2,     pretty,

@@ -42,7 +42,6 @@ import Control.Monad.State.Strict import Data.Map (Map) import qualified Data.Map as Map-import Data.Maybe (fromMaybe) import Data.Word (Word32) import qualified Text.LLVM as L import Numeric.Natural@@ -131,11 +130,6 @@ floatAlignment dl w = Map.lookup w t   where AT t = dl^.floatInfo --- | Get the basic alignment for aggregate types.-aggregateAlignment :: DataLayout -> Alignment-aggregateAlignment dl =-  fromMaybe noAlignment (findExact 0 (dl^.aggInfo))- -- | Return maximum alignment constraint stored in tree. maxAlignmentInTree :: AlignInfo -> Alignment maxAlignmentInTree (AT t) = foldrOf folded max noAlignment t@@ -165,12 +159,12 @@    = DL { _intLayout :: EndianForm         , _stackAlignment :: !Alignment         , _functionPtrAlignment :: !Alignment+        , _aggregateAlignment :: !Alignment         , _ptrSize     :: !Bytes         , _ptrAlign    :: !Alignment         , _integerInfo :: !AlignInfo         , _vectorInfo  :: !AlignInfo         , _floatInfo   :: !AlignInfo-        , _aggInfo     :: !AlignInfo         , _stackInfo   :: !AlignInfo         , _layoutWarnings :: [L.LayoutSpec]         }@@ -189,6 +183,10 @@ functionPtrAlignment =   lens _functionPtrAlignment (\s v -> s { _functionPtrAlignment = v}) +aggregateAlignment :: Lens' DataLayout Alignment+aggregateAlignment =+  lens _aggregateAlignment (\s v -> s { _aggregateAlignment = v})+ -- | Size of pointers in bytes. ptrSize :: Lens' DataLayout Bytes ptrSize = lens _ptrSize (\s v -> s { _ptrSize = v})@@ -206,10 +204,6 @@ floatInfo :: Lens' DataLayout AlignInfo floatInfo = lens _floatInfo (\s v -> s { _floatInfo = v}) --- | Information about aggregate size.-aggInfo :: Lens' DataLayout AlignInfo-aggInfo = lens _aggInfo (\s v -> s { _aggInfo = v})- -- | Layout constraints on a stack object with the given size. stackInfo :: Lens' DataLayout AlignInfo stackInfo = lens _stackInfo (\s v -> s { _stackInfo = v})@@ -246,10 +240,10 @@                 , _functionPtrAlignment = noAlignment                 , _ptrSize  = 8 -- 64 bit pointers = 8 bytes                 , _ptrAlign = Alignment 3 -- 64 bit alignment: 2^3=8 byte boundaries+                , _aggregateAlignment = noAlignment -- Aggregates are 1-byte aligned.                 , _integerInfo = emptyAlignInfo                 , _floatInfo   = emptyAlignInfo                 , _vectorInfo  = emptyAlignInfo-                , _aggInfo     = emptyAlignInfo                 , _stackInfo   = emptyAlignInfo                 , _layoutWarnings = []                 }@@ -268,8 +262,6 @@           -- Default vector alignments.           setAt vectorInfo  64 (Alignment 3) -- 64-bit vector is 8 byte aligned.           setAt vectorInfo 128 (Alignment 4) -- 128-bit vector is 16 byte aligned.-          -- Default aggregate alignments.-          setAt aggInfo  0 noAlignment  -- Aggregates are 1-byte aligned.  -- | Maximum alignment for any type (used by malloc). maxAlignment :: DataLayout -> Alignment@@ -277,10 +269,10 @@   maximum [ dl^.stackAlignment           , dl^.functionPtrAlignment           , dl^.ptrAlign+          , dl^.aggregateAlignment           , maxAlignmentInTree (dl^.integerInfo)           , maxAlignmentInTree (dl^.vectorInfo)           , maxAlignmentInTree (dl^.floatInfo)-          , maxAlignmentInTree (dl^.aggInfo)           , maxAlignmentInTree (dl^.stackInfo)           ] @@ -289,14 +281,14 @@            | otherwise = fromIntegral i  -- | Insert alignment into spec.-setAtBits :: Lens' DataLayout AlignInfo -> L.LayoutSpec -> Int -> Int -> State DataLayout ()-setAtBits f spec sz a =-  case fromBits a of+setAtBits :: Lens' DataLayout AlignInfo -> L.LayoutSpec -> L.Storage -> State DataLayout ()+setAtBits f spec st =+  case fromBits (L.alignABI (L.storageAlignment st)) of     Left{} -> layoutWarnings %= (spec:)-    Right w -> f . at (fromSize sz) .= Just w+    Right w -> f . at (fromSize (L.storageSize st)) .= Just w  -- | Insert alignment into spec.-setBits :: Lens' DataLayout Alignment -> L.LayoutSpec -> Int -> State DataLayout ()+setBits :: Lens' DataLayout Alignment -> L.LayoutSpec -> L.NumBits -> State DataLayout () setBits f spec a =   case fromBits a of     Left{} -> layoutWarnings %= (spec:)@@ -309,24 +301,25 @@     case ls of       L.BigEndian    -> intLayout .= BigEndian       L.LittleEndian -> intLayout .= LittleEndian-      L.PointerSize n sz a _+      L.PointerSize ps            -- Currently, we assume that only default address space (0) is used.            -- We use that address space as the sole arbiter of what pointer            -- size to use, and we ignore all other PointerSize layout specs.            -- See doc/limitations.md for more discussion.-        |  n == 0-        -> case fromBits a of+        |  L.ptrAddrSpace ps == 0+        -> case fromBits (L.alignABI (L.storageAlignment st)) of              Right a' | r == 0 -> do ptrSize .= fromIntegral w                                      ptrAlign .= a'              _ -> layoutWarnings %= (ls:)         |  otherwise         -> return ()-       where (w,r) = sz `divMod` 8-      L.IntegerSize    sz a _ -> setAtBits integerInfo ls sz a-      L.VectorSize     sz a _ -> setAtBits vectorInfo  ls sz a-      L.FloatSize      sz a _ -> setAtBits floatInfo   ls sz a-      L.AggregateSize  sz a _ -> setAtBits aggInfo     ls sz a-      L.StackObjSize   sz a _ -> setAtBits stackInfo   ls sz a+       where st = L.ptrStorage ps+             (w,r) = L.storageSize st `divMod` 8+      L.IntegerSize st -> setStorageAlignInfo integerInfo st+      L.VectorSize st -> setStorageAlignInfo vectorInfo st+      L.FloatSize st -> setStorageAlignInfo floatInfo st+      L.StackObjSize st -> setStorageAlignInfo stackInfo st+      L.AggregateSize _ a -> setBits aggregateAlignment ls (L.alignABI a)       L.NativeIntSize _ -> return ()       L.StackAlign a    -> setBits stackAlignment ls a       -- TODO: For now, we ignore the FunctionPointerAlignType field. This tells@@ -337,6 +330,17 @@       -- should revisit this.       L.FunctionPointerAlign _ a -> setBits functionPtrAlignment ls a       L.Mangling _      -> return ()+      -- Currently, we assume that only the default address space (0) is used,+      -- and we ignore all other address space-related layout specs.+      -- See doc/limitations.md for more discussion.+      L.ProgramAddrSpace {} -> return ()+      L.GlobalAddrSpace {} -> return ()+      L.AllocaAddrSpace {} -> return ()+      L.NonIntegralPointerSpaces {} -> return ()+  where+    setStorageAlignInfo ::+      Lens' DataLayout AlignInfo -> L.Storage -> State DataLayout ()+    setStorageAlignInfo info st = setAtBits info ls st  -- | Create parsed data layout from layout spec AST. parseDataLayout :: L.DataLayout -> DataLayout

@@ -38,7 +38,6 @@  import           Data.Text (Text) import qualified Text.LLVM.AST as L-import           Type.Reflection (SomeTypeRep(SomeTypeRep)) import           Prettyprinter  import           What4.Interface@@ -100,7 +99,6 @@   = SymbolicPointer   | RawBitvector   | NoOverride-  | Uncallable SomeTypeRep   deriving (Eq, Ord)  ppFuncLookupError :: FuncLookupError -> Doc ann@@ -109,10 +107,6 @@     SymbolicPointer -> "Cannot resolve a symbolic pointer to a function handle"     RawBitvector -> "Cannot treat raw bitvector as function pointer"     NoOverride -> "No implementation or override found for pointer"-    Uncallable (SomeTypeRep typeRep) ->-      vsep [ "Data associated with the pointer found, but was not a callable function:"-           , hang 2 (viaShow typeRep)-           ]  type MemErrContext sym w = MemoryOp sym w 

@@ -130,6 +130,22 @@   GEPOutOfBounds      :: (1 <= w, 1 <= wptr) => e (LLVMPointerType wptr)                       -> e (BVType w)                       -> Poison e+  ZExtNonNegative     :: (1 <= w)+                      => e (BVType w)+                      -> Poison e+  UiToFpNonNegative   :: (1 <= w)+                      => e (BVType w)+                      -> Poison e+  TruncNoUnsignedWrap :: (1 <= w)+                      => e (BVType w)+                      -> Poison e+  TruncNoSignedWrap   :: (1 <= w)+                      => e (BVType w)+                      -> Poison e+  ICmpSameSign        :: (1 <= w)+                      => e (BVType w)+                      -> e (BVType w)+                      -> Poison e   deriving (Typeable)  standard :: Poison e -> Standard@@ -154,6 +170,11 @@     InsertElementIndex _    -> LLVMRef LLVM8     LLVMAbsIntMin _         -> LLVMRef LLVM12     GEPOutOfBounds _ _      -> LLVMRef LLVM8+    ZExtNonNegative _       -> LLVMRef LLVM18+    UiToFpNonNegative _     -> LLVMRef LLVM19+    TruncNoUnsignedWrap _   -> LLVMRef LLVM20+    TruncNoSignedWrap _     -> LLVMRef LLVM20+    ICmpSameSign _ _        -> LLVMRef LLVM20  -- | Which section(s) of the document state that this is poison? cite :: Poison e -> Doc ann@@ -178,6 +199,11 @@     InsertElementIndex _    -> "‘insertelement’ Instruction (Semantics)"     LLVMAbsIntMin _         -> "‘llvm.abs.*’ Intrinsic (Semantics)"     GEPOutOfBounds _ _      -> "‘getelementptr’ Instruction (Semantics)"+    ZExtNonNegative _       -> "‘zext’ Instruction (Semantics)"+    UiToFpNonNegative _     -> "‘uitofp’ Instruction (Semantics)"+    TruncNoUnsignedWrap _   -> "‘trunc’ Instruction (Semantics)"+    TruncNoSignedWrap _     -> "‘trunc’ Instruction (Semantics)"+    ICmpSameSign _ _        -> "‘icmp’ Instruction (Semantics)"  explain :: Poison e -> Doc ann explain =@@ -226,13 +252,24 @@       ]      -- The following explanation is a bit unsatisfactory, because it is specific-    -- to how we treat this instruction in Crucible.+    -- to how we treat this instruction in Crucible. (See also #1605.)     GEPOutOfBounds _ _ -> cat $       [ "Calling `getelementptr` resulted in an index that was out of bounds for the"       , "given allocation (likely due to arithmetic overflow), but Crucible currently"-      , "treats all GEP instructions as if they had the `inbounds` flag set."+      , "treats all GEP instructions as if they had the `inbounds` attribute set."       ] +    ZExtNonNegative _ ->+      "A negative integer was zero-extended even though the `nneg` flag was set"+    UiToFpNonNegative _ ->+      "A negative integer was converted to a floating-point value even though the `nneg` flag was set"+    TruncNoUnsignedWrap _ ->+      "Unsigned truncation caused wrapping even though the `nuw` flag was set"+    TruncNoSignedWrap _ ->+      "Signed truncation caused wrapping even though the `nsw` flag was set"+    ICmpSameSign _ _ ->+      "Two integers with different signs were compared even though the `samesign` flag was set"+ details :: forall sym ann.   W4I.IsExpr (W4I.SymExpr sym) => Poison (RegValue' sym) -> [Doc ann] details =@@ -259,6 +296,11 @@       [ "Pointer:" <+> ppPtr ptr       , "Bitvector:" <+> W4I.printSymExpr bv       ]+    ZExtNonNegative v -> args [v]+    UiToFpNonNegative v -> args [v]+    TruncNoUnsignedWrap v -> args [v]+    TruncNoSignedWrap v -> args [v]+    ICmpSameSign v1 v2 -> args [v1, v2]   where  args :: forall w. [RegValue' sym (BVType w)] -> [Doc ann]@@ -334,6 +376,16 @@       GEPOutOfBounds <$> concPtr' sym conc p <*> bv v     LLVMAbsIntMin v ->       LLVMAbsIntMin <$> bv v+    ZExtNonNegative v ->+      ZExtNonNegative <$> bv v+    UiToFpNonNegative v ->+      UiToFpNonNegative <$> bv v+    TruncNoUnsignedWrap v ->+      TruncNoUnsignedWrap <$> bv v+    TruncNoSignedWrap v ->+      TruncNoSignedWrap <$> bv v+    ICmpSameSign v1 v2 ->+      ICmpSameSign <$> bv v1 <*> bv v2   -- -----------------------------------------------------------------------

@@ -69,6 +69,9 @@   | LLVM7   | LLVM8   | LLVM12+  | LLVM18+  | LLVM19+  | LLVM20   deriving (Data, Eq, Enum, Generic, Ord, Read, Show, Typeable)  ppLLVMRefVer :: LLVMRefVer -> Text@@ -79,6 +82,9 @@ ppLLVMRefVer LLVM7  = "7" ppLLVMRefVer LLVM8  = "8" ppLLVMRefVer LLVM12 = "12"+ppLLVMRefVer LLVM18 = "18"+ppLLVMRefVer LLVM19 = "19"+ppLLVMRefVer LLVM20 = "20"  stdURL :: Standard -> Maybe Text stdURL (CStd   C11)     = Just "http://www.iso-9899.info/n1570.html"@@ -90,6 +96,9 @@ stdURL (LLVMRef LLVM7)  = Just "https://releases.llvm.org/7.0.0/docs/LangRef.html" stdURL (LLVMRef LLVM8)  = Just "https://releases.llvm.org/8.0.0/docs/LangRef.html" stdURL (LLVMRef LLVM12) = Just "https://releases.llvm.org/12.0.0/docs/LangRef.html"+stdURL (LLVMRef LLVM18) = Just "https://releases.llvm.org/18.1.0/docs/LangRef.html"+stdURL (LLVMRef LLVM19) = Just "https://releases.llvm.org/19.1.0/docs/LangRef.html"+stdURL (LLVMRef LLVM20) = Just "https://releases.llvm.org/20.1.0/docs/LangRef.html" stdURL _                = Nothing  ppStd :: Standard -> Text

@@ -23,6 +23,7 @@ import           Lang.Crucible.Simulator.Evaluation import           Lang.Crucible.Simulator.RegValue import           Lang.Crucible.Simulator.SimError+import           Lang.Crucible.Types (TypeRepr(..)) import           Lang.Crucible.Panic (panic)  import qualified Lang.Crucible.LLVM.Arch.X86 as X86@@ -99,3 +100,14 @@          blk <- natIte sym cond xblk yblk          off <- bvIte sym cond xoff yoff          return (LLVMPointer blk off)++    -- These are not necessarily considered correct, see crucible#366+    LLVM_PoisonBV w -> poisonPanic (BVRepr w)+    LLVM_PoisonFloat fi -> poisonPanic (FloatRepr fi)+  where+    poisonPanic tpr =+      panic+        "llvmExtensionEval"+        [ "Attempting to evaluate poison value"+        , "Type: " ++ show tpr+        ]

@@ -98,7 +98,18 @@     !(f BoolType) -> !(f (LLVMPointerType w)) -> !(f (LLVMPointerType w)) ->     LLVMExtensionExpr f (LLVMPointerType w) +  -- | A @poison@ bitvector value. The semantics of this construct are still+  -- under discussion, see crucible#366.+  LLVM_PoisonBV ::+    (1 <= w) => !(NatRepr w) ->+    LLVMExtensionExpr f (BVType w) +  -- | A @poison@ float value. The semantics of this construct are still under+  -- discussion, see crucible#366.+  LLVM_PoisonFloat ::+    !(FloatInfoRepr fi) ->+    LLVMExtensionExpr f (FloatType fi)+ -- | Extension statements for LLVM.  These statements represent the operations --   necessary to interact with the LLVM memory model. data LLVMStmt (f :: CrucibleType -> Type) :: CrucibleType -> Type where@@ -230,43 +241,6 @@      !(f (LLVMPointerType wptr)) {- Second pointer -} ->      LLVMStmt f (BVType wptr) -  -- | Debug information-  LLVM_Debug ::-    !(LLVM_Dbg f c)              {- Debug variant -} ->-    LLVMStmt f UnitType---- | 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 =>-    !(f (LLVMPointerType wptr))  {- Pointer to local variable -} ->-    L.DILocalVariable            {- Local variable information -} ->-    L.DIExpression               {- Complex expression -} ->-    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 =>-    !(f (LLVMPointerType wptr))  {- Pointer to local variable -} ->-    L.DILocalVariable            {- Local variable information -} ->-    L.DIExpression               {- Complex expression -} ->-    LLVM_Dbg f (LLVMPointerType wptr)--  -- | Annotates a value with local-variable debug information-  ---  -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-value>-  LLVM_Dbg_Value ::-    !(TypeRepr c)                {- Type of local variable -} ->-    !(f c)                       {- Value of local variable -} ->-    L.DILocalVariable            {- Local variable information -} ->-    L.DIExpression               {- Complex expression -} ->-    LLVM_Dbg f c- $(return [])  instance TypeApp LLVMExtensionExpr where@@ -278,6 +252,8 @@       LLVM_PointerBlock _ _  -> NatRepr       LLVM_PointerOffset w _ -> BVRepr w       LLVM_PointerIte w _ _ _ -> LLVMPointerRepr w+      LLVM_PoisonBV w -> BVRepr w+      LLVM_PoisonFloat fi -> FloatRepr fi  instance PrettyApp LLVMExtensionExpr where   ppApp pp e =@@ -293,11 +269,16 @@         pretty "pointerOffset" <+> pp ptr       LLVM_PointerIte _ cond x y ->         pretty "pointerIte" <+> pp cond <+> pp x <+> pp y+      LLVM_PoisonBV _ ->+        pretty "poisonBV"+      LLVM_PoisonFloat _ ->+        pretty "poisonFloat"  instance TestEqualityFC LLVMExtensionExpr where   testEqualityFC testSubterm =     $(U.structuralTypeEquality [t|LLVMExtensionExpr|]        [ (U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])+       , (U.ConType [t|FloatInfoRepr|] `U.TypeApp` U.AnyType, [|testEquality|])        , (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|])@@ -311,6 +292,7 @@   compareFC testSubterm =     $(U.structuralTypeOrd [t|LLVMExtensionExpr|]        [ (U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])+       , (U.ConType [t|FloatInfoRepr|] `U.TypeApp` U.AnyType, [|compareF|])        , (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|])@@ -357,7 +339,6 @@     LLVM_PtrLe{} -> knownRepr     LLVM_PtrAddOffset w _ _ _ -> LLVMPointerRepr w     LLVM_PtrSubtract w _ _ _ -> BVRepr w-    LLVM_Debug{} -> knownRepr  instance PrettyApp LLVMStmt where   ppApp pp = \case@@ -385,14 +366,7 @@        pretty "ptrAddOffset" <+> ppGlobalVar mvar <+> pp x <+> pp y     LLVM_PtrSubtract _ mvar x y ->        pretty "ptrSubtract" <+> ppGlobalVar mvar <+> pp x <+> pp y-    LLVM_Debug dbg -> ppApp pp dbg -instance PrettyApp LLVM_Dbg where-  ppApp pp = \case-    LLVM_Dbg_Addr    x _ _ -> pretty "dbg.addr"    <+> pp x-    LLVM_Dbg_Declare x _ _ -> pretty "dbg.declare" <+> pp x-    LLVM_Dbg_Value _ x _ _ -> pretty "dbg.value"   <+> pp x- -- TODO: move to a Pretty instance ppGlobalVar :: GlobalVar Mem -> Doc ann ppGlobalVar = viaShow@@ -401,26 +375,6 @@ ppAlignment :: Alignment -> Doc ann ppAlignment = viaShow -instance TestEqualityFC LLVM_Dbg where-  testEqualityFC testSubterm = $(U.structuralTypeEquality [t|LLVM_Dbg|]-    [(U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])-    ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])-    ])--instance OrdFC LLVM_Dbg where-  compareFC compareSubterm = $(U.structuralTypeOrd [t|LLVM_Dbg|]-    [(U.DataArg 0 `U.TypeApp` U.AnyType, [|compareSubterm|])-    ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])-    ])--instance FoldableFC LLVM_Dbg where-  foldMapFC = foldMapFCDefault-instance FunctorFC LLVM_Dbg where-  fmapFC = fmapFCDefault--instance TraversableFC LLVM_Dbg where-  traverseFC = $(U.structuralTraversal [t|LLVM_Dbg|] [])- instance TestEqualityFC LLVMStmt where   testEqualityFC testSubterm =     $(U.structuralTypeEquality [t|LLVMStmt|]@@ -429,7 +383,6 @@        ,(U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|testEquality|])        ,(U.ConType [t|CtxRepr|] `U.TypeApp` U.AnyType, [|testEquality|])        ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])-       ,(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|testEqualityFC testSubterm|])        ])  instance OrdFC LLVMStmt where@@ -440,7 +393,6 @@        ,(U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|compareF|])        ,(U.ConType [t|CtxRepr|] `U.TypeApp` U.AnyType, [|compareF|])        ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])-       ,(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|compareFC compareSubterm|])        ])  instance FunctorFC LLVMStmt where@@ -451,6 +403,4 @@  instance TraversableFC LLVMStmt where   traverseFC =-    $(U.structuralTraversal [t|LLVMStmt|]-      [(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|traverseFC|])-      ])+    $(U.structuralTraversal [t|LLVMStmt|] [])

@@ -434,8 +434,8 @@     basicBlockConstInits bb = foldMap stmtConstInits (L.bbStmts bb)      stmtConstInits :: L.Stmt -> LoadRelConstInitMap-    stmtConstInits (L.Result _ instr _) = instrConstInits instr-    stmtConstInits (L.Effect instr _)   = instrConstInits instr+    stmtConstInits (L.Result _ instr _ _) = instrConstInits instr+    stmtConstInits (L.Effect instr _ _)   = instrConstInits instr      instrConstInits :: L.Instr -> LoadRelConstInitMap     instrConstInits (L.Call _ _ (L.ValSymbol fun) [ptr, _offset])@@ -483,7 +483,8 @@     foldLoadRelConstInitElem :: L.Global -> L.Value -> Maybe L.Value     foldLoadRelConstInitElem global constInitElem       | L.ValConstExpr-          (L.ConstConv L.Trunc+          (L.ConstConv+            (L.Trunc False False)             (L.Typed { L.typedValue =               L.ValConstExpr                 (L.ConstArith

@@ -134,7 +134,9 @@   , SomeLLVMOverride llvmPrefetchOverride_preLLVM10    , SomeLLVMOverride llvmStacksave+  , SomeLLVMOverride llvmStacksave_preLLVM18   , SomeLLVMOverride llvmStackrestore+  , SomeLLVMOverride llvmStackrestore_preLLVM18    , SomeLLVMOverride (llvmBSwapOverride (knownNat @2))  -- 16 = 2 * 8   , SomeLLVMOverride (llvmBSwapOverride (knownNat @4))  -- 32 = 4 * 8@@ -160,6 +162,22 @@   , SomeLLVMOverride llvmSinOverride_F64   , SomeLLVMOverride llvmCosOverride_F32   , SomeLLVMOverride llvmCosOverride_F64+  , SomeLLVMOverride llvmTanOverride_F32+  , SomeLLVMOverride llvmTanOverride_F64+  , SomeLLVMOverride llvmAsinOverride_F32+  , SomeLLVMOverride llvmAsinOverride_F64+  , SomeLLVMOverride llvmAcosOverride_F32+  , SomeLLVMOverride llvmAcosOverride_F64+  , SomeLLVMOverride llvmAtanOverride_F32+  , SomeLLVMOverride llvmAtanOverride_F64+  , SomeLLVMOverride llvmAtan2Override_F32+  , SomeLLVMOverride llvmAtan2Override_F64+  , SomeLLVMOverride llvmSinhOverride_F32+  , SomeLLVMOverride llvmSinhOverride_F64+  , SomeLLVMOverride llvmCoshOverride_F32+  , SomeLLVMOverride llvmCoshOverride_F64+  , SomeLLVMOverride llvmTanhOverride_F32+  , SomeLLVMOverride llvmTanhOverride_F64   , SomeLLVMOverride llvmPowOverride_F32   , SomeLLVMOverride llvmPowOverride_F64   , SomeLLVMOverride llvmExpOverride_F32@@ -484,17 +502,47 @@     ovrWithBackend $ \bak ->       liftIO $ addFailedAssertion bak $ AssertFailureSimError "llvm.ubsantrap() called" "") +-- | TODO(#130): This override ought to impose proof obligations related to+-- proper block scoping. llvmStacksave   :: (IsSymInterface sym, HasPtrWidth wptr)   => LLVMOverride p sym ext EmptyCtx (LLVMPointerType wptr) llvmStacksave =+  [llvmOvr| i8* @llvm.stacksave.p0() |]+  (\_memOps _args -> mkNull)++-- | TODO(#130): This override ought to impose proof obligations related to+-- proper block scoping.+--+-- See also 'llvmStacksave'. This version exists for compatibility with+-- pre-18 versions of LLVM, where @llvm.stacksave@ always assumed that the+-- returned pointer value resides in address space 0.+llvmStacksave_preLLVM18+  :: (IsSymInterface sym, HasPtrWidth wptr)+  => LLVMOverride p sym ext EmptyCtx (LLVMPointerType wptr)+llvmStacksave_preLLVM18 =   [llvmOvr| i8* @llvm.stacksave() |]   (\_memOps _args -> mkNull) +-- | TODO(#130): This override ought to impose proof obligations related to+-- proper block scoping. llvmStackrestore   :: (IsSymInterface sym, HasPtrWidth wptr)   => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType llvmStackrestore =+  [llvmOvr| void @llvm.stackrestore.p0( i8* ) |]+  (\_memOps _args -> return ())++-- | TODO(#130): This override ought to impose proof obligations related to+-- proper block scoping.+--+-- See also 'llvmStackrestore'. This version exists for compatibility with+-- pre-18 versions of LLVM, where @llvm.stackrestore@ always assumed that the+-- pointer argument resides in address space 0.+llvmStackrestore_preLLVM18+  :: (IsSymInterface sym, HasPtrWidth wptr)+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType+llvmStackrestore_preLLVM18 =   [llvmOvr| void @llvm.stackrestore( i8* ) |]   (\_memOps _args -> return ()) @@ -1175,6 +1223,150 @@ llvmCosOverride_F64 =   [llvmOvr| double @llvm.cos.f64( double ) |]   (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cos) args)++llvmTanOverride_F32 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmTanOverride_F32 =+  [llvmOvr| float @llvm.tan.f32( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tan) args)++llvmTanOverride_F64 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmTanOverride_F64 =+  [llvmOvr| double @llvm.tan.f64( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tan) args)++llvmAsinOverride_F32 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmAsinOverride_F32 =+  [llvmOvr| float @llvm.asin.f32( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arcsin) args)++llvmAsinOverride_F64 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmAsinOverride_F64 =+  [llvmOvr| double @llvm.asin.f64( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arcsin) args)++llvmAcosOverride_F32 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmAcosOverride_F32 =+  [llvmOvr| float @llvm.acos.f32( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arccos) args)++llvmAcosOverride_F64 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmAcosOverride_F64 =+  [llvmOvr| double @llvm.acos.f64( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arccos) args)++llvmAtanOverride_F32 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmAtanOverride_F32 =+  [llvmOvr| float @llvm.atan.f32( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arctan) args)++llvmAtanOverride_F64 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmAtanOverride_F64 =+  [llvmOvr| double @llvm.atan.f64( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arctan) args)++llvmSinhOverride_F32 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmSinhOverride_F32 =+  [llvmOvr| float @llvm.sinh.f32( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sinh) args)++llvmSinhOverride_F64 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmSinhOverride_F64 =+  [llvmOvr| double @llvm.sinh.f64( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sinh) args)++llvmCoshOverride_F32 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmCoshOverride_F32 =+  [llvmOvr| float @llvm.cosh.f32( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cosh) args)++llvmCoshOverride_F64 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmCoshOverride_F64 =+  [llvmOvr| double @llvm.cosh.f64( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cosh) args)++llvmTanhOverride_F32 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmTanhOverride_F32 =+  [llvmOvr| float @llvm.tanh.f32( float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tanh) args)++llvmTanhOverride_F64 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmTanhOverride_F64 =+  [llvmOvr| double @llvm.tanh.f64( double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tanh) args)++llvmAtan2Override_F32 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)+     (FloatType SingleFloat)+llvmAtan2Override_F32 =+  [llvmOvr| float @llvm.atan2.f32( float, float ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Arctan2) args)++llvmAtan2Override_F64 ::+  IsSymInterface sym =>+  LLVMOverride p sym ext+     (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)+     (FloatType DoubleFloat)+llvmAtan2Override_F64 =+  [llvmOvr| double @llvm.atan2.f64( double, double ) |]+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Arctan2) args)  llvmPowOverride_F32 ::   IsSymInterface sym =>

@@ -95,6 +95,10 @@   , SomeLLVMOverride llvmFreeOverride   , SomeLLVMOverride llvmReallocOverride   , SomeLLVMOverride llvmStrlenOverride+  , SomeLLVMOverride llvmStrnlenOverride+  , SomeLLVMOverride llvmStrcpyOverride+  , SomeLLVMOverride llvmStrdupOverride+  , SomeLLVMOverride llvmStrndupOverride   , SomeLLVMOverride llvmPrintfOverride   , SomeLLVMOverride llvmPrintfChkOverride   , SomeLLVMOverride llvmPutsOverride@@ -392,6 +396,38 @@   [llvmOvr| size_t @strlen( i8* ) |]   (\memOps args -> Ctx.uncurryAssignment (callStrlen memOps) args) +llvmStrnlenOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (BVType wptr)+llvmStrnlenOverride =+  [llvmOvr| size_t @strnlen( i8*, size_t ) |]+  (\memOps args -> Ctx.uncurryAssignment (callStrnlen memOps) args)++llvmStrcpyOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr) (LLVMPointerType wptr)+llvmStrcpyOverride =+  [llvmOvr| i8* @strcpy( i8*, i8* ) |]+  (\memOps args -> Ctx.uncurryAssignment (callStrcpy memOps) args)++llvmStrdupOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (LLVMPointerType wptr)+llvmStrdupOverride =+  [llvmOvr| i8* @strdup( i8* ) |]+  (\memOps args -> Ctx.uncurryAssignment (callStrdup memOps) args)++llvmStrndupOverride+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr+     , ?memOpts :: MemOptions )+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (LLVMPointerType wptr)+llvmStrndupOverride =+  [llvmOvr| i8* @strndup( i8*, size_t ) |]+  (\memOps args -> Ctx.uncurryAssignment (callStrndup memOps) args)+ ------------------------------------------------------------------------ -- ** Implementations @@ -613,6 +649,66 @@   ovrWithBackend $ \bak -> do     mem <- readGlobal mvar     liftIO $ strLen bak mem strPtr++callStrnlen+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (BVType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))+callStrnlen mvar (regValue -> strPtr) (regValue -> bound) =+  ovrWithBackend $ \bak -> do+    mem <- readGlobal mvar+    liftIO $ CStr.strnlen bak mem strPtr bound++callStrcpy+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (LLVMPointerType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))+callStrcpy mvar (regValue -> dst) (regValue -> src) =+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> do+      mem' <- liftIO $ CStr.copyConcretelyNullTerminatedString bak mem dst src Nothing+      pure (dst, mem')++callStrdup+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))+callStrdup mvar (regValue -> src) =+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> liftIO $ do+      let sym = backendGetSym bak+      loc <- plSourceLoc <$> getCurrentProgramLoc sym+      let loc' = "<strdup> " ++ show loc+      CStr.dupConcretelyNullTerminatedString bak mem src Nothing loc' noAlignment++callStrndup+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym+     , ?memOpts :: MemOptions )+  => GlobalVar Mem+  -> RegEntry sym (LLVMPointerType wptr)+  -> RegEntry sym (BVType wptr)+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))+callStrndup mvar (regValue -> src) (regValue -> bound) =+  ovrWithBackend $ \bak ->+    modifyGlobal mvar $ \mem -> liftIO $ do+      let sym = backendGetSym bak+      loc <- plSourceLoc <$> getCurrentProgramLoc sym+      let loc' = "<strndup> " ++ show loc+      case BV.asUnsigned <$> asBV bound of+        Nothing -> do+          let err = AssertFailureSimError "`strndup` called with symbolic max length" ""+          addFailedAssertion bak err+        Just b ->+          let bound' = Just (fromIntegral b) in+          CStr.dupConcretelyNullTerminatedString bak mem src bound' loc' noAlignment  callAssert   :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym

@@ -46,6 +46,8 @@   , IndeterminateLoadBehavior(..)   , defaultMemOptions   , laxPointerMemOptions+  , ppLLVMMemIntrinsicType+  , ppLLVMIntrinsicTypes    -- * Pointers   , LLVMPointerType@@ -200,7 +202,6 @@ import           Control.Monad.IO.Class import           Control.Monad.Trans (lift) import           Control.Monad.Trans.State-import           Data.Dynamic import           Data.IORef import           Data.Map (Map) import qualified Data.Map as Map@@ -209,6 +210,7 @@ import           Data.Word import qualified GHC.Stack as GHC import           Numeric.Natural (Natural)+import qualified Prettyprinter as PP import           System.IO (Handle, hPutStrLn)  import qualified Data.BitVector.Sized as BV@@ -276,7 +278,7 @@   { memImplBlockSource :: BlockSource   , memImplGlobalMap   :: GlobalMap sym   , memImplSymbolMap   :: Map Natural L.Symbol -- inverse mapping to 'memImplGlobalMap'-  , memImplHandleMap   :: Map Natural Dynamic+  , memImplHandleMap   :: Map Natural SomeFnHandle   , memImplHeap        :: G.Mem sym   } @@ -359,6 +361,34 @@         --putStrLn "MEM ABORT BRANCH"         return $ MemImpl nxt gMap sMap hMap $ G.branchAbortMem m +-- | An intrinsic-printing function for 'MemImpl' for use with+-- 'Lang.Crucible.Types.ppTypeRepr'.+ppLLVMMemIntrinsicType ::+  Applicative f =>+  -- | Fallback for other instrinsics, can be+  -- 'Lang.Crucible.Types.ppIntrinsicDefault'.+  (forall s ctx'. SymbolRepr s -> CtxRepr ctx' -> f (PP.Doc ann)) ->+  SymbolRepr symb ->+  CtxRepr ctx ->+  f (PP.Doc ann)+ppLLVMMemIntrinsicType fallback symbRepr tyCtx =+  case testEquality symbRepr (knownSymbol @"LLVM_memory") of+    Nothing -> fallback symbRepr tyCtx+    Just Refl -> pure "LLVMMemory"++-- | An intrinsic-printing function for the LLVM intrinsic types for use with+-- 'Lang.Crucible.Types.ppTypeRepr'.+ppLLVMIntrinsicTypes ::+  Applicative f =>+  -- | Fallback for other instrinsics, can be+  -- 'Lang.Crucible.Types.ppIntrinsicDefault'.+  (forall s ctx'. SymbolRepr s -> CtxRepr ctx' -> f (PP.Doc ann)) ->+  SymbolRepr symb ->+  CtxRepr ctx ->+  f (PP.Doc ann)+ppLLVMIntrinsicTypes fallback =+  ppLLVMMemIntrinsicType (ppLLVMPointerIntrinsicType fallback)+ -- | Top-level evaluation function for LLVM extension statements. --   LLVM extension statements are used to implement the memory model operations. llvmStatementExec ::@@ -533,9 +563,7 @@     do mem <- getMem mvar        liftIO $ doPtrSubtract bak mem x y -  eval LLVM_Debug{} = pure () - mkMemVar :: Text          -> HandleAllocator          -> IO (GlobalVar Mem)@@ -719,16 +747,16 @@ -- -- See also "Lang.Crucible.LLVM.Functions". doInstallHandle-  :: (Typeable a, IsSymBackend sym bak)+  :: IsSymBackend sym bak   => bak   -> LLVMPtr sym wptr-  -> a {- ^ handle -}+  -> SomeFnHandle   -> MemImpl sym   -> IO (MemImpl sym)-doInstallHandle _bak ptr x mem =+doInstallHandle _bak ptr hdl mem =   case asNat (llvmPointerBlock ptr) of     Just blkNum ->-      do let hMap' = Map.insert blkNum (toDyn x) (memImplHandleMap mem)+      do let hMap' = Map.insert blkNum hdl (memImplHandleMap mem)          return mem{ memImplHandleMap = hMap' }     Nothing ->       panic "MemModel.doInstallHandle"@@ -738,11 +766,11 @@  -- | Look up the handle associated with the given pointer, if any. doLookupHandle-  :: (Typeable a, IsSymInterface sym)+  :: IsSymInterface sym   => sym   -> MemImpl sym   -> LLVMPtr sym wptr-  -> IO (Either ME.FuncLookupError a)+  -> IO (Either ME.FuncLookupError SomeFnHandle) doLookupHandle _sym mem ptr = do   let LLVMPointer blk _ = ptr   case asNat blk of@@ -752,10 +780,7 @@       | otherwise ->           case Map.lookup i (memImplHandleMap mem) of             Nothing -> return (Left ME.NoOverride)-            Just x ->-              case fromDynamic x of-                Nothing -> return (Left (ME.Uncallable (dynTypeRep x)))-                Just a  -> return (Right a)+            Just hdl -> return (Right hdl)  -- | Free the memory region pointed to by the given pointer. --@@ -1564,6 +1589,13 @@     , "*** Undef value: " ++ show v     ] +unpackMemValue _ tpr v@(LLVMValPoison _) =+  panic "MemModel.unpackMemValue"+    [ "Cannot unpack a `poison` value"+    , "*** Crucible type: " ++ show tpr+    , "*** Poison value: " ++ show v+    ]+ unpackMemValue _ tpr v =   panic "MemModel.unpackMemValue"     [ "Crucible type mismatch when unpacking LLVM value"@@ -1776,6 +1808,8 @@   LLVMValZero <$> toStorableType memty constToLLVMValP _sym _look (UndefConst memty) = liftIO $   LLVMValUndef <$> toStorableType memty+constToLLVMValP _sym _look (PoisonConst memty) = liftIO $+  LLVMValPoison <$> toStorableType memty   -- | Translate a constant into an LLVM runtime value. Assumes all necessary

@@ -676,7 +676,9 @@ concLLVMVal _ _ v@LLVMValString{} = pure v concLLVMVal _ _ v@LLVMValZero{} = pure v concLLVMVal _ _ (LLVMValUndef st) =-  pure (LLVMValZero st) -- ??? does it make sense to turn Undef into Zero?+  pure (LLVMValUndef st)+concLLVMVal _ _ (LLVMValPoison st) =+  pure (LLVMValPoison st)   concWriteSource ::

@@ -381,6 +381,9 @@ floatToBV _ _ (NoErr p (LLVMValUndef (StorageType Float _))) =   return (NoErr p (LLVMValUndef (Type.bitvectorType 4))) +floatToBV _ _ (NoErr p (LLVMValPoison (StorageType Float _))) =+  return (NoErr p (LLVMValPoison (Type.bitvectorType 4)))+ floatToBV sym _ (NoErr p (LLVMValZero (StorageType Float _))) =   do nz <- W4I.natLit sym 0      iz <- W4I.bvZero sym (knownNat @32)@@ -407,6 +410,9 @@ doubleToBV _ _ (NoErr p (LLVMValUndef (StorageType Double _))) =   return (NoErr p (LLVMValUndef (Type.bitvectorType 8))) +doubleToBV _ _ (NoErr p (LLVMValPoison (StorageType Double _))) =+  return (NoErr p (LLVMValPoison (Type.bitvectorType 8)))+ doubleToBV sym _ (NoErr p (LLVMValZero (StorageType Double _))) =   do nz <- W4I.natLit sym 0      iz <- W4I.bvZero sym (knownNat @64)@@ -433,6 +439,9 @@ fp80ToBV _ _ (NoErr p (LLVMValUndef (StorageType X86_FP80 _))) =   return (NoErr p (LLVMValUndef (Type.bitvectorType 10))) +fp80ToBV _ _ (NoErr p (LLVMValPoison (StorageType X86_FP80 _))) =+  return (NoErr p (LLVMValPoison (Type.bitvectorType 10)))+ fp80ToBV sym _ (NoErr p (LLVMValZero (StorageType X86_FP80 _))) =   do nz <- W4I.natLit sym 0      iz <- W4I.bvLit sym (knownNat @80) (BV.zero knownNat)@@ -937,6 +946,12 @@                                           , "Undef type: " ++ show tpu                                           ] +      LLVMValPoison tpp ->+        -- TODO: Is this the right behavior?+        panic "Cannot mux zero and poison" [ "Zero type: " ++ show tpz+                                           , "Poison type: " ++ show tpp+                                           ]+       LLVMValString bs -> muxzero cond tpz =<< Value.explodeStringValue sym bs        LLVMValInt base off ->@@ -1007,6 +1022,9 @@           LLVMValArray tp1 <$> V.zipWithM (muxval cond) v1 v2      muxval _ v1@(LLVMValUndef tp1) (LLVMValUndef tp2)+      | tp1 == tp2 = pure v1++    muxval _ v1@(LLVMValPoison tp1) (LLVMValPoison tp2)       | tp1 == tp2 = pure v1      muxval _ v1 v2 =

@@ -78,6 +78,7 @@      -- * Pretty printing   , ppPtr+  , ppLLVMPointerIntrinsicType      -- * Annotation   , annotatePointerBlock@@ -89,6 +90,7 @@ import qualified Data.Map as Map (lookup) import           Numeric.Natural import           Prettyprinter+import qualified Prettyprinter as PP  import           GHC.TypeLits (TypeError, ErrorMessage(..)) import           GHC.TypeNats@@ -250,10 +252,14 @@        panic "LLVM.MemModel.Pointer.concPtrFn"          [ "Impossible: LLVMPointerType ill-formed context" ] +-- | Helper, not exported+ptrSymb :: SymbolRepr "LLVM_pointer"+ptrSymb = knownSymbol+ -- | A singleton map suitable for use in a 'Conc.ConcCtx' if LLVM pointers are -- the only intrinsic type in use concPtrFnMap :: MapF.MapF SymbolRepr (Conc.IntrinsicConcFn t)-concPtrFnMap = MapF.singleton (knownSymbol @"LLVM_pointer") concPtrFn+concPtrFnMap = MapF.singleton ptrSymb concPtrFn  -- | A 'Conc.IntrinsicConcToSymFn' for LLVM pointers concToSymPtrFn :: Conc.IntrinsicConcToSymFn "LLVM_pointer"@@ -272,7 +278,7 @@ -- | A singleton map suitable for use in 'Crucible.Concretize.concToSym' if LLVM -- pointers are the only intrinsic type in use concToSymPtrFnMap :: MapF.MapF SymbolRepr Conc.IntrinsicConcToSymFn-concToSymPtrFnMap = MapF.singleton (knownSymbol @"LLVM_pointer") concToSymPtrFn+concToSymPtrFnMap = MapF.singleton ptrSymb concToSymPtrFn  -- | Mux function specialized to LLVM pointer values. muxLLVMPtr ::@@ -424,6 +430,33 @@      let blk_doc = printSymNat blk          off_doc = printSymExpr bv       in pretty "(" <> blk_doc <> pretty "," <+> off_doc <> pretty ")"++-- | An intrinsic-printing function for use with+-- 'Lang.Crucible.Types.ppTypeRepr'.+ppLLVMPointerIntrinsicType ::+  Applicative f =>+  -- | Fallback for other instrinsics, can be+  -- 'Lang.Crucible.Types.ppIntrinsicDefault'.+  (forall s ctx'. SymbolRepr s -> CtxRepr ctx' -> f (PP.Doc ann)) ->+  SymbolRepr symb ->+  CtxRepr ctx ->+  f (PP.Doc ann)+ppLLVMPointerIntrinsicType fallback symbRepr tyCtx =+  case testEquality symbRepr ptrSymb of+    Nothing -> fallback symbRepr tyCtx+    Just Refl ->+      case Ctx.viewAssign tyCtx of+        Ctx.AssignExtend (Ctx.viewAssign -> Ctx.AssignEmpty) (BVRepr w) ->+          pure (PP.pretty "(Ptr" PP.<+> PP.viaShow w <> PP.pretty ")")+        -- These are impossible by the definition of LLVMPointerImpl+        Ctx.AssignEmpty ->+          panic+          "ppLLVMPointerIntrinsicType"+          ["Impossible: LLVMPointerType empty context"]+        Ctx.AssignExtend _ _ ->+          panic+          "ppLLVMPointerIntrinsicType"+          ["Impossible: LLVMPointerType ill-formed context"]  -- | Look up a pointer in the 'memImplGlobalMap' to see if it's a global. --

@@ -15,20 +15,39 @@  -- | Manipulating C-style null-terminated strings module Lang.Crucible.LLVM.MemModel.Strings-  ( Mem.loadString+  ( storeString+  -- * Loading strings+  , Mem.loadString   , Mem.loadMaybeString-  , Mem.strLen   , loadConcretelyNullTerminatedString-  , loadSymbolicString-  , storeString+  , loadProvablyNullTerminatedString+  -- * String length+  , Mem.strLen+  , strnlen+  , strlenConcreteString+  , strlenConcretelyNullTerminatedString+  , strlenProvablyNullTerminatedString+  -- * String copying+  , copyConcreteString+  , copyConcretelyNullTerminatedString+  , copyProvablyNullTerminatedString+  -- * String duplication+  , dupConcreteString+  , dupConcretelyNullTerminatedString+  , dupProvablyNullTerminatedString   -- * Low-level string loading primitives   -- ** 'ByteChecker'   , ControlFlow(..)   , ByteChecker(..)+  , withMaxChars+  -- *** For loading strings   , fullyConcreteNullTerminatedString   , concretelyNullTerminatedString-  , nullTerminatedString-  , withMaxChars+  , provablyNullTerminatedString+  -- *** For string length+  , fullyConcreteNullTerminatedStringLength+  , concretelyNullTerminatedStringLength+  , provablyNullTerminatedStringLength   -- ** 'ByteLoader'   , ByteLoader(..)   , llvmByteLoader@@ -36,8 +55,10 @@   , loadBytes   ) where -import           Data.Bifunctor (Bifunctor(bimap, first))+import           Control.Lens ((^.), to)+import           Data.Bifunctor (Bifunctor(bimap)) import           Control.Monad.IO.Class (MonadIO, liftIO)+import qualified Control.Monad.State.Strict as State import qualified Data.BitVector.Sized as BV import           Data.Functor ((<&>)) import qualified Data.Parameterized.NatRepr as DPN@@ -48,14 +69,65 @@ 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.Errors.MemoryError as MemErr import qualified Lang.Crucible.LLVM.MemModel as LCLM import qualified Lang.Crucible.LLVM.MemModel as Mem+import qualified Lang.Crucible.LLVM.MemModel.Generic as Mem.G 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 +-- | Store a null-terminated string to memory.+storeNullTerminatedString ::+  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 included)+  Vec.Vector (WI.SymBV sym 8) ->+  IO (LCLM.MemImpl sym)+storeNullTerminatedString bak mem ptr bytesBvs = do+  let sym = LCB.backendGetSym bak+  zeroNat <- WI.natLit sym 0+  let bytes = Vec.map (Mem.LLVMValInt zeroNat) bytesBvs+  let val = Mem.LLVMValArray (Mem.bitvectorType 1) bytes+  let storTy = Mem.llvmValStorableType @sym val+  Mem.storeRaw bak mem ptr storTy CLD.noAlignment val++-- | 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+  zeroByte <- WI.bvZero sym (DPN.knownNat @8)+  let nullTerminatedBytes = Vec.snoc bytesBvs zeroByte+  storeNullTerminatedString bak mem ptr nullTerminatedBytes++---------------------------------------------------------------------+-- * Loading strings+ -- | 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@@ -88,14 +160,15 @@  -- | 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.+-- 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,+-- 'loadProvablyNullTerminatedString' 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 ::+loadProvablyNullTerminatedString ::   ( LCB.IsSymBackend sym bak   , sym ~ WEB.ExprBuilder scope st fs   , bak ~ LCBO.OnlineBackend solver scope st fs@@ -111,41 +184,370 @@   -- | Maximum number of characters to read   Maybe Int ->   IO [WI.SymBV sym 8]-loadSymbolicString bak mem ptr limit =+loadProvablyNullTerminatedString bak mem ptr limit =   let loader = llvmByteLoader mem in   case limit of-    Nothing -> loadBytes bak mem id ptr loader nullTerminatedString+    Nothing -> loadBytes bak mem id ptr loader provablyNullTerminatedString     Just l ->-      let byteChecker = withMaxChars l (\f -> pure (f [])) nullTerminatedString in+      let byteChecker = withMaxChars l (\f -> pure (f [])) provablyNullTerminatedString 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.+---------------------------------------------------------------------+-- * String length++-- | Implementation of libc @strnlen@.+strnlen ::   ( LCB.IsSymBackend sym bak-  , WI.IsExpr (WI.SymExpr sym)-  , LCLM.HasPtrWidth w-  , LCLM.HasLLVMAnn sym-  , ?memOpts :: LCLM.MemOptions+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack   ) =>   bak ->-  LCLM.MemImpl sym ->-  -- | Pointer to write string to-  LCLM.LLVMPtr sym w ->-  -- | The bytes of the string to write (null terminator not included)+  Mem.MemImpl sym ->+  -- | Pointer to null-terminated string+  Mem.LLVMPtr sym wptr ->+  -- | Size+  --+  -- If this is not concrete, this will generate an assertion failure.+  WI.SymBV sym wptr ->+  IO (WI.SymBV sym wptr)+strnlen bak mem ptr bound = do+  case BV.asUnsigned <$> WI.asBV bound of+    Nothing ->+      let err = LCS.AssertFailureSimError "`strnlen` called with symbolic max length" "" in+      LCB.addFailedAssertion bak err+    Just b ->+      let bound' = Just (fromIntegral b) in+      strlenConcretelyNullTerminatedString bak mem ptr bound'+ +-- | @strlen@ of a concrete string.+--+-- If any symbolic bytes are encountered, an assertion failure will be+-- generated. If a maximum number of characters is provided, no more than that+-- number of characters will be read. In either case, 'strlenConcreteString'+-- will stop reading if it encounters a null terminator.+strlenConcreteString ::+  ( 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 Int+strlenConcreteString bak mem ptr limit = do+  let loader = llvmByteLoader mem+  case limit of+    Nothing -> loadBytes bak mem 0 ptr loader fullyConcreteNullTerminatedStringLength+    Just 0 -> pure 0+    Just l -> do+      let byteChecker = withMaxChars l pure fullyConcreteNullTerminatedStringLength+      loadBytes bak mem (0, 0) ptr loader byteChecker+ +-- | @strlen@ of a null-terminated string (with a concrete null terminator).+--+-- 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, 'strlenConcretelyNullTerminatedString' will stop reading if+-- it encounters a (concretely) null terminator.+--+-- This has the same behavior as 'Lang.Crucible.LLVM.MemModel.strLen', except+-- that it supports a maximum length.+strlenConcretelyNullTerminatedString ::+  ( 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 wptr)+strlenConcretelyNullTerminatedString bak mem ptr limit = do+  let loader = llvmByteLoader mem+  let sym = LCB.backendGetSym bak+  z <- WI.bvZero sym ?ptrWidth+  flip State.evalStateT (WI.truePred sym) $+    case limit of+      Nothing -> loadBytes bak mem z ptr loader concretelyNullTerminatedStringLength+      Just 0 -> liftIO (WI.bvZero (LCB.backendGetSym bak) ?ptrWidth)+      Just l -> do+        let byteChecker = withMaxChars l pure concretelyNullTerminatedStringLength+        loadBytes bak mem (z, 0) ptr loader byteChecker++-- | @strlen@ of a provably null-terminated string.+--+-- 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,+-- 'strlenProvablyNullTerminatedString' will stop reading if it encounters a+-- (provably) null terminator.+strlenProvablyNullTerminatedString ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  , sym ~ WEB.ExprBuilder scope st fs+  , bak ~ LCBO.OnlineBackend solver scope st fs+  , WPO.OnlineSolver solver+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  -- | Maximum number of characters to read+  Maybe Int ->+  IO (WI.SymBV sym wptr)+strlenProvablyNullTerminatedString bak mem ptr limit = do+  let loader = llvmByteLoader mem+  let sym = LCB.backendGetSym bak+  z <- WI.bvZero sym ?ptrWidth+  flip State.evalStateT (WI.truePred sym) $+    case limit of+      Nothing -> loadBytes bak mem z ptr loader provablyNullTerminatedStringLength+      Just 0 -> liftIO (WI.bvZero (LCB.backendGetSym bak) ?ptrWidth)+      Just l -> do+        let byteChecker = withMaxChars l pure provablyNullTerminatedStringLength+        loadBytes bak mem (z, 0) ptr loader byteChecker++---------------------------------------------------------------------+-- * String copying++-- | Helper, not exported+strcpyAssertDisjoint ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  -- | Loaded bytes   Vec.Vector (WI.SymBV sym 8) ->-  IO (LCLM.MemImpl sym)-storeString bak mem ptr bytesBvs = do+  -- | Destination pointer+  Mem.LLVMPtr sym wptr ->+  -- | Source pointer+  Mem.LLVMPtr sym wptr ->+  IO ()+strcpyAssertDisjoint bak mem bytes dst src = 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+  let len = fromIntegral (Vec.length bytes)+  sz <- WI.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth len)+  let heap = mem ^. to Mem.memImplHeap+  let memOp =+        MemErr.MemCopyOp (Just "strcpy dst", dst) (Just "strcpy src", src) sz heap+  Mem.assertDisjointRegions bak memOp ?ptrWidth dst sz src sz +-- | @strcpy@ of a concrete string.+--+-- Uses 'Mem.loadString' to load the string, see that function for details.+--+-- Asserts that the regions are disjoint.+copyConcreteString ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  -- | Destination pointer+  Mem.LLVMPtr sym wptr ->+  -- | Source pointer+  Mem.LLVMPtr sym wptr ->+  IO (Mem.MemImpl sym)+copyConcreteString bak mem dst src = do+  bytes <- Mem.loadString bak mem src Nothing+  let sym = LCB.backendGetSym bak+  symBytes <- mapM (WI.bvLit sym WI.knownRepr . BV.word8) bytes+  let bytesVec = Vec.fromList symBytes+  strcpyAssertDisjoint bak mem bytesVec dst src+  storeString bak mem dst (Vec.fromList symBytes)++-- | @strcpy@ of a concretely null-terminated string.+--+-- Uses 'loadConcretelyNullTerminatedString' to load the string, see that+-- function for details.+--+-- Asserts that the regions are disjoint.+copyConcretelyNullTerminatedString ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  -- | Destination pointer+  Mem.LLVMPtr sym wptr ->+  -- | Source pointer+  Mem.LLVMPtr sym wptr ->+  -- | Maximum number of characters to read+  Maybe Int ->+  IO (Mem.MemImpl sym)+copyConcretelyNullTerminatedString bak mem dst src bounds = do+  bytes <- loadConcretelyNullTerminatedString bak mem src bounds+  let bytesVec = Vec.fromList bytes+  strcpyAssertDisjoint bak mem bytesVec dst src+  storeString bak mem dst bytesVec++-- | @strcpy@ of a concrete string.+--+-- Uses 'loadProvablyNullTerminatedString' to load the string, see that+-- function for details.+--+-- Asserts that the regions are disjoint.+copyProvablyNullTerminatedString ::+  ( 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 ->+  -- | Destination pointer+  Mem.LLVMPtr sym wptr ->+  -- | Source pointer+  Mem.LLVMPtr sym wptr ->+  -- | Maximum number of characters to read+  Maybe Int ->+  IO (Mem.MemImpl sym)+copyProvablyNullTerminatedString bak mem dst src bounds = do+  bytes <- loadProvablyNullTerminatedString bak mem src bounds+  let bytesVec = Vec.fromList bytes+  strcpyAssertDisjoint bak mem bytesVec dst src+  storeString bak mem dst bytesVec+ ---------------------------------------------------------------------+-- * String duplication++-- | Helper function: allocate memory and store bytes for string duplication.+--+-- Takes a vector of bytes (NOT including null terminator) and:+-- 1. Allocates memory of the appropriate size (length + 1 for null terminator)+-- 2. Stores the bytes with null terminator to the allocated memory+-- 3. Returns the new pointer and updated memory+dupFromLoadedBytes ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Vec.Vector (WI.SymBV sym 8) ->+  String ->+  CLD.Alignment ->+  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)+dupFromLoadedBytes bak mem bytesVec displayString alignment = do+  let len = fromIntegral (Vec.length bytesVec) + 1  -- +1 for null terminator+  let sym = LCB.backendGetSym bak+  sz <- WI.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth len)+  (dst, mem') <- Mem.doMalloc bak Mem.G.HeapAlloc Mem.G.Mutable displayString mem sz alignment+  mem'' <- storeString bak mem' dst bytesVec+  pure (dst, mem'')++-- | @strdup@ of a concrete string.+--+-- Uses 'Mem.loadString' to load the string, see that function for details.+--+-- Allocates memory and copies the string to it, returning the new pointer.+dupConcreteString ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  -- | Source pointer+  Mem.LLVMPtr sym wptr ->+  -- | Display string for allocation+  String ->+  -- | Alignment+  CLD.Alignment ->+  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)+dupConcreteString bak mem src displayString alignment = do+  bytes <- Mem.loadString bak mem src Nothing+  let sym = LCB.backendGetSym bak+  symBytes <- mapM (WI.bvLit sym WI.knownRepr . BV.word8) bytes+  dupFromLoadedBytes bak mem (Vec.fromList symBytes) displayString alignment++-- | @strdup@ of a concretely null-terminated string.+--+-- Uses 'loadConcretelyNullTerminatedString' to load the string, see that+-- function for details.+--+-- Allocates memory and copies the string to it, returning the new pointer.+dupConcretelyNullTerminatedString ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  -- | Source pointer+  Mem.LLVMPtr sym wptr ->+  -- | Maximum number of characters to read+  Maybe Int ->+  -- | Display string for allocation+  String ->+  CLD.Alignment ->+  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)+dupConcretelyNullTerminatedString bak mem src bounds displayString alignment = do+  bytes <- loadConcretelyNullTerminatedString bak mem src bounds+  dupFromLoadedBytes bak mem (Vec.fromList bytes) displayString alignment++-- | @strdup@ of a provably null-terminated string.+--+-- Uses 'loadProvablyNullTerminatedString' to load the string, see that+-- function for details.+--+-- Allocates memory and copies the string to it, returning the new pointer.+dupProvablyNullTerminatedString ::+  ( 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 ->+  -- | Source pointer+  Mem.LLVMPtr sym wptr ->+  -- | Maximum number of characters to read+  Maybe Int ->+  -- | Display string for allocation+  String ->+  CLD.Alignment ->+  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)+dupProvablyNullTerminatedString bak mem src bounds displayString alignment = do+  bytes <- loadProvablyNullTerminatedString bak mem src bounds+  dupFromLoadedBytes bak mem (Vec.fromList bytes) displayString alignment++--------------------------------------------------------------------- -- * Low-level string loading primitives  ---------------------------------------------------------------------@@ -192,6 +594,31 @@   let err = LCS.AssertFailureSimError "Found pointer instead of byte when loading string" ""   Partial.ptrToBv bak err bytePtr +-- | 'ByteChecker' for adding a maximum character length.+withMaxChars ::+  MonadIO m =>+  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 ->+    runByteChecker checker bak acc bytePtr >>=+      \case+        Break r -> pure (Break r)+        Continue r ->+          if i + 1 >= limit+          then Break <$> done r+          else pure (Continue (r, i + 1))++---------------------------------------------------------------------+-- *** For loading strings+ -- | 'ByteChecker' for loading concrete strings. -- -- Currently unused internally, but analogous with@@ -234,10 +661,10 @@         Just 0 -> True         _ -> False --- | 'ByteChecker' for loading symbolic strings with a null terminator.+-- | 'ByteChecker' for loading symbolic strings with a provably-null terminator. -- -- Used in 'loadSymbolicString'.-nullTerminatedString ::+provablyNullTerminatedString ::   MonadIO m =>   GHC.HasCallStack =>   LCB.IsSymBackend sym bak =>@@ -245,45 +672,117 @@   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)+provablyNullTerminatedString =+  ByteChecker $ \bak acc bytePtr -> liftIO $ do+    byte <- ptrToBv8 bak bytePtr     let sym = LCB.backendGetSym bak-    isNullTerm <- liftIO (isNullTerminator bak sym byte)+    isNullTerm <- isProvablyNullTerminator 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 ::+-- Helper, not exported+isProvablyNullTerminator ::   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+  sym ~ WEB.ExprBuilder scope st fs =>+  bak ~ LCBO.OnlineBackend solver scope st fs =>+  WPO.OnlineSolver solver =>+  bak ->+  sym ->+  WI.SymBV sym 8 ->+  IO Bool+isProvablyNullTerminator 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 "isProvablyNullTerminator" p <&>+          \case+            WS.Unsat () -> True+            WS.Sat () -> False+            WS.Unknown -> False++---------------------------------------------------------------------+-- *** For string length++-- | 'ByteChecker' for @strlen@ of concrete strings.+fullyConcreteNullTerminatedStringLength ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  ByteChecker m sym bak Int Int+fullyConcreteNullTerminatedStringLength =+  ByteChecker $ \bak acc bytePtr -> do+    byte <- liftIO (ptrToBv8 bak bytePtr)+    case BV.asUnsigned <$> WI.asBV byte of+      Just 0 -> pure (Break acc)+      Just _ -> pure (Continue $! acc + 1)+      Nothing -> do+        let msg = "Symbolic value encountered when loading a string"+        liftIO (LCB.addFailedAssertion bak (LCS.Unsupported GHC.callStack msg))++-- Helper, not exported+symStringLength ::+  MonadIO m =>+  State.MonadState (WI.Pred sym) m =>+  GHC.HasCallStack =>+  Mem.HasPtrWidth wptr =>+  LCB.IsSymBackend sym bak =>+  -- | How to check if a predicate is false+  (bak -> WI.Pred sym -> m Bool) ->+  ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr)+symStringLength predIsFalse =+  ByteChecker $ \bak len bytePtr -> do+    byte <- liftIO (ptrToBv8 bak bytePtr)+    keepGoing <- State.get+    let sym = LCB.backendGetSym bak+    byteWasNonNull <- liftIO (WI.bvIsNonzero sym byte)+    keepGoing' <- liftIO (WI.andPred sym keepGoing byteWasNonNull)+    stopHere <- predIsFalse bak keepGoing'+    if stopHere+    then pure (Break len)+    else do+      State.put keepGoing'+      lenPlusOne <- liftIO (WI.bvAdd sym len =<< WI.bvOne sym ?ptrWidth)+      Continue <$> liftIO (WI.bvIte sym keepGoing' lenPlusOne len)++-- | 'ByteChecker' for @strlen@ of strings with a concrete null terminator.+concretelyNullTerminatedStringLength ::+  MonadIO m =>+  State.MonadState (WI.Pred sym) m =>+  GHC.HasCallStack =>+  Mem.HasPtrWidth wptr =>+  LCB.IsSymBackend sym bak =>+  ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr)+concretelyNullTerminatedStringLength =+  symStringLength (\_bak p -> pure (WI.asConstantPred p == Just False))++-- | 'ByteChecker' for @strlen@ for strings with a provably-null terminator.+provablyNullTerminatedStringLength ::+  MonadIO m =>+  State.MonadState (WI.Pred sym) m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  Mem.HasPtrWidth wptr =>+  sym ~ WEB.ExprBuilder scope st fs =>+  bak ~ LCBO.OnlineBackend solver scope st fs =>+  WPO.OnlineSolver solver =>+  ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr)+provablyNullTerminatedStringLength =+  symStringLength $ \bak p ->+    case WI.asConstantPred p of+      Just b -> pure b+      _ ->+        liftIO $ LCBO.withSolverProcess bak (pure False) $ \proc -> do+          WPO.checkSatisfiable proc "provablyNullTerminatedStringLength" p <&>+            \case+              WS.Unsat () -> True+              WS.Sat () -> False+              WS.Unknown -> False  --------------------------------------------------------------------- -- ** 'ByteLoader'

@@ -107,7 +107,10 @@   -- | The @undef@ value exists at all storage types.   LLVMValUndef :: StorageType -> LLVMVal sym +  -- | The @poison@ value exists at all storage types.+  LLVMValPoison :: StorageType -> LLVMVal sym + llvmValStorableType :: IsExpr (SymExpr sym) => LLVMVal sym -> StorageType llvmValStorableType v =   case v of@@ -120,6 +123,7 @@     LLVMValString bs -> arrayType (fromIntegral (BS.length bs)) (bitvectorType (Bytes 1))     LLVMValZero tp -> tp     LLVMValUndef tp -> tp+    LLVMValPoison tp -> tp  -- | Create a fresh 'LLVMVal' of the given type. freshLLVMVal :: IsSymInterface sym =>@@ -145,6 +149,7 @@   case t of     LLVMValZero _tp -> pretty "0"     LLVMValUndef tp -> pretty "<undef : " <> viaShow tp <> pretty ">"+    LLVMValPoison tp -> pretty "<poison : " <> viaShow tp <> pretty ">"     LLVMValString bs -> viaShow bs     LLVMValInt base off -> ppPtr @sym (LLVMPointer base off)     LLVMValFloat _ v -> printSymExpr v@@ -191,6 +196,7 @@     \case       (LLVMValZero tp) -> pure $ angles (typed "zero" tp)       (LLVMValUndef tp) -> pure $ angles (typed "undef" tp)+      (LLVMValPoison tp) -> pure $ angles (typed "poison" tp)       (LLVMValString bs) -> pure $ viaShow bs       (LLVMValInt blk w) -> fromMaybe otherDoc <$> ppInt blk w         where@@ -257,6 +263,7 @@ instance IsExpr (SymExpr sym) => Show (LLVMVal sym) where   show (LLVMValZero _tp) = "0"   show (LLVMValUndef tp) = "<undef : " ++ show tp ++ ">"+  show (LLVMValPoison tp) = "<poison : " ++ show tp ++ ">"   show (LLVMValString  _) = "<string>"   show (LLVMValInt blk w)     | Just 0 <- asNat blk = "<int" ++ show (bvWidth w) ++ ">"@@ -333,9 +340,9 @@ -- -- Should be faster than using 'testEqual' with 'zeroExpandLLVMVal' for compound -- values, because we 'traverse' subcomponents of vectors and structs, quitting--- early on a constantly false answer or 'LLVMValUndef'.+-- early on a constantly false answer or 'LLVMValUndef' or 'LLVMValPoison'. ----- Returns 'Nothing' for 'LLVMValUndef'.+-- Returns 'Nothing' for 'LLVMValUndef' or 'LLVMValPoison'. isZero :: forall sym. (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym)        => sym -> LLVMVal sym -> IO (Maybe (Pred sym)) isZero sym v =@@ -345,9 +352,9 @@     LLVMValString bs  -> pure $ Just $ backendPred sym $ not $ isJust $ BS.find (/= 0) bs     LLVMValZero _     -> pure (Just $ truePred sym)     LLVMValUndef _    -> pure Nothing-    _                 ->-      -- For atomic types, we simply expand and compare.-      testEqual sym v =<< zeroExpandLLVMVal sym (llvmValStorableType v)+    LLVMValPoison _   -> pure Nothing+    LLVMValInt {}     -> compareToZeroExpansion+    LLVMValFloat {}   -> compareToZeroExpansion   where     areZero :: Traversable t => t (LLVMVal sym) -> IO (Maybe (t (Pred sym)))     areZero = fmap sequence . traverse (isZero sym)@@ -356,9 +363,15 @@       -- This could probably be simplified with a well-placed =<<...       join $ fmap commuteMaybe $ fmap (fmap (allOf sym . toList)) $ areZero vs +    -- Check if a value is equal to itself after zero-expansion. This is+    -- suitable for checking atomic types (e.g., integers and floats).+    compareToZeroExpansion =+      testEqual sym v =<< zeroExpandLLVMVal sym (llvmValStorableType v)+ -- | A predicate denoting the equality of two LLVMVals. ----- Returns 'Nothing' in the event that one of the values contains 'LLVMValUndef'.+-- Returns 'Nothing' in the event that one of the values contains 'LLVMValUndef'+-- or 'LLVMValPoison'. testEqual :: forall sym. (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym)           => sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym)) testEqual sym v1 v2 =@@ -394,6 +407,8 @@     (other, LLVMValZero tp) -> compareZero tp other     (LLVMValUndef _, _) -> pure Nothing     (_, LLVMValUndef _) -> pure Nothing+    (LLVMValPoison _, _) -> pure Nothing+    (_, LLVMValPoison _) -> pure Nothing     (_, _) -> false -- type mismatch    where true = pure (Just $ truePred sym)

@@ -313,7 +313,7 @@              -> StructInfo mkStructInfo dl packed tps0 = go [] 0 a0 tps0   where a0 | packed    = noAlignment-           | otherwise = nextAlign noAlignment tps0 `max` aggregateAlignment dl+           | otherwise = nextAlign noAlignment tps0 `max` (dl ^. aggregateAlignment)         -- Padding after each field depends on the alignment of the         -- type of the next field, if there is one. Padding after the         -- last field depends on the alignment of the whole struct

@@ -97,7 +97,6 @@ import           Data.IORef (IORef, newIORef, readIORef, modifyIORef) import           Data.Map.Strict (Map) import qualified Data.Map.Strict as Map-import           Data.Set (Set) import qualified Data.Set as Set import           Data.Maybe import           Data.String@@ -206,8 +205,8 @@           , fromString msg           ] -    stmt m (L.Effect _ _) = return m-    stmt m (L.Result ident instr _) = do+    stmt m (L.Effect _ _ _) = return m+    stmt m (L.Result ident instr _ _) = do          ty <- either (err instr) return $ instrResultType instr          ex <- typeToRegExpr ty          case Map.lookup ident m of@@ -223,26 +222,25 @@ generateStmts :: (?transOpts :: TranslationOptions)         => TypeRepr ret         -> L.BlockLabel-        -> Set L.Ident {- ^ Set of usable identifiers -}         -> [L.Stmt]         -> LLVMGenerator s arch ret a-generateStmts retType lab defSet0 stmts = go defSet0 (processDbgDeclare stmts)- where go _ [] = fail "LLVM basic block ended without a terminating instruction"-       go defSet (x:xs) =+generateStmts retType lab stmts = go (processDbgDeclare stmts)+ where go [] = fail "LLVM basic block ended without a terminating instruction"+       go (x:xs) =          case x of            -- a result statement assigns the result of the instruction into a register-           L.Result ident instr md ->-              do setLocation md-                 generateInstr retType lab defSet instr+           L.Result ident instr dr md ->+              do setLocation md dr+                 generateInstr retType lab instr                    (assignLLVMReg ident)-                   (go (Set.insert ident defSet) xs)+                   (go xs)             -- an effect statement simply executes the instruction for its effects and discards the result-           L.Effect instr md ->-              do setLocation md-                 generateInstr retType lab defSet instr+           L.Effect instr dr md ->+              do setLocation md dr+                 generateInstr retType lab instr                    (\_ -> return ())-                   (go defSet xs)+                   (go xs)  -- | Search for calls to intrinsic 'llvm.dbg.declare' and copy the -- metadata onto the corresponding 'alloca' statement.  Also copy@@ -255,18 +253,18 @@     go (stmt : stmts) =       let (m, stmts') = go stmts in       case stmt of-        L.Result x instr@L.Alloca{} md ->+        L.Result x instr@L.Alloca{} dr md ->           case Map.lookup x m of-            Just md' -> (m, L.Result x instr (md' ++ md) : stmts')+            Just md' -> (m, L.Result x instr dr (md' ++ md) : stmts')             Nothing -> (m, stmt : stmts')               --error $ "Identifier not found: " ++ show x ++ "\nPossible identifiers: " ++ show (Map.keys m) -        L.Result x (L.Conv L.BitCast (L.Typed _ (L.ValIdent y)) _) md ->+        L.Result x (L.Conv L.BitCast (L.Typed _ (L.ValIdent y)) _) _dr md ->           let md' = md ++ fromMaybe [] (Map.lookup x m)               m'  = Map.alter (Just . maybe md' (md'++)) y m            in (m', stmt:stmts) -        L.Effect (L.Call _ _ (L.ValSymbol "llvm.dbg.declare") (L.Typed _ (L.ValMd (L.ValMdValue (L.Typed _ (L.ValIdent x)))) : _)) md ->+        L.Effect (L.Call _ _ (L.ValSymbol "llvm.dbg.declare") (L.Typed _ (L.ValMd (L.ValMdValue (L.Typed _ (L.ValIdent x)))) : _)) _dr md ->           (Map.insert x md m, stmt : stmts')          -- This is needlessly fragile. Let's just ignore debug declarations we don't understand.@@ -275,25 +273,67 @@          _ -> (m, stmt : stmts') -setLocation-  :: [(String,L.ValMd)]-  -> LLVMGenerator s arch ret ()-setLocation [] = return ()-setLocation (x:xs) =-  case x of-    ("dbg",L.ValMdLoc dl) ->-      let ln   = fromIntegral $ L.dlLine dl-          col  = fromIntegral $ L.dlCol dl-          file = getFile $ L.dlScope dl-       in setPosition (SourcePos file ln col)-    ("dbg",L.ValMdDebugInfo (L.DebugInfoSubprogram subp))-      | Just file' <- L.dispFile subp-      -> let ln = fromIntegral $ L.dispLine subp-             file = getFile file'-          in setPosition (SourcePos file ln 0)-    _ -> setLocation xs-+-- | Search for an instruction's nearest debug location that was attached as a+-- metadata attribute using the @!dbg@ identifier, and then set the+-- `LLVMGenerator`'s position using the location. If such a metadata attribute+-- cannot be found, look at the debug records as a fallback. (In practice, LLVM+-- will usually attach debug locations as metadata attributes, so it makes more+-- sense to look through the metadata attributes first.)+setLocation ::+  forall s arch ret.+  -- | The metadata attributes.+  [(String,L.ValMd)] ->+  -- | The debug records.+  [L.DebugRecord] ->+  LLVMGenerator s arch ret ()+setLocation mds drs = setMetadataLocation mds  where+ setMetadataLocation :: [(String,L.ValMd)] -> LLVMGenerator s arch ret ()+ setMetadataLocation [] =+   -- If we can't find a @!dbg@ metadata location, fall back to searching the+   -- debug records.+   setDebugRecordLocation drs+ setMetadataLocation (x:xs) =+   case x of+     ("dbg",md)+       | Just posn <- valMdPosition md ->+         setPosition posn+     _ -> setMetadataLocation xs++ setDebugRecordLocation :: [L.DebugRecord] -> LLVMGenerator s arch ret ()+ setDebugRecordLocation [] = return ()+ setDebugRecordLocation (x:xs) =+   case x of+     L.DebugRecordValue drv+       | Just posn <- valMdPosition (L.drvLocation drv) ->+         setPosition posn+     L.DebugRecordValueSimple drvs+       | Just posn <- valMdPosition (L.drvsLocation drvs) ->+         setPosition posn+     L.DebugRecordDeclare drd+       | Just posn <- valMdPosition (L.drdLocation drd) ->+         setPosition posn+     L.DebugRecordAssign dra+       | Just posn <- valMdPosition (L.draLocation dra) ->+         setPosition posn+     L.DebugRecordLabel drl+       | Just posn <- valMdPosition (L.drlLocation drl) ->+         setPosition posn+     _ -> setDebugRecordLocation xs++ valMdPosition :: L.ValMd -> Maybe Position+ valMdPosition (L.ValMdLoc dl) =+   let ln   = fromIntegral $ L.dlLine dl+       col  = fromIntegral $ L.dlCol dl+       file = getFile $ L.dlScope dl+    in Just (SourcePos file ln col)+ valMdPosition (L.ValMdDebugInfo (L.DebugInfoSubprogram subp))+   | Just file' <- L.dispFile subp =+     let ln = fromIntegral $ L.dispLine subp+         file = getFile file'+     in Just (SourcePos file ln 0)+ valMdPosition _ = Nothing+  getFile = Text.pack . maybe "" filenm . findFile   -- The typical values available here will be something like:@@ -353,7 +393,7 @@         -> LLVMGenerator s arch ret () defineLLVMBlock retType lm L.BasicBlock{ L.bbLabel = Just lab, L.bbStmts = stmts } = do   case Map.lookup lab lm of-    Just bi -> defineBlock (block_label bi) (generateStmts retType lab (block_use_set bi) stmts)+    Just bi -> defineBlock (block_label bi) (generateStmts retType lab stmts)     Nothing -> fail $ unwords ["LLVM basic block not found in block info map", show lab]  defineLLVMBlock _ _ _ = fail "LLVM basic block has no label!"@@ -375,7 +415,7 @@     ( L.BasicBlock{ L.bbLabel = Just entry_lab } : _ ) -> do       let (L.Symbol nm) = L.defName defn       callPushFrame $ Text.pack nm-      setLocation $ Map.toList (L.defMetadata defn)+      setLocation (Map.toList (L.defMetadata defn)) []        bim <- buildBlockInfoMap defn       blockInfoMap .= bim

@@ -190,7 +190,7 @@   -- to registers: the return values can only be used in the "normal" successor   -- block. -  loop (L.Result nm i _md:ss) =+  loop (L.Result nm i _dr _md:ss) =     case i of       L.Invoke _tp f args l_normal l_unwind ->             -- the use sets from the function value, arguments, and unwind label@@ -214,7 +214,7 @@       -- defined here       _ -> Set.union (instrUse lab i bim) (Set.delete nm (loop ss)) -  loop (L.Effect i _md:ss) = Set.union (instrUse lab i bim) (loop ss)+  loop (L.Effect i _dr _md:ss) = Set.union (instrUse lab i bim) (loop ss)  instrUse :: L.BlockLabel -> L.Instr -> Map L.BlockLabel (LLVMBlockInfo s) -> Set L.Ident instrUse from i bim = Set.unions $ case i of@@ -237,7 +237,7 @@   L.Fence{} -> []   L.CmpXchg _weak _vol p v1 v2 _s _o1 _o2 -> map useTypedVal [p,v1,v2]   L.AtomicRW _vol _op p v _s _o -> [useTypedVal p, useTypedVal v]-  L.ICmp _op x y -> [useTypedVal x, useVal y]+  L.ICmp _samesign _op x y -> [useTypedVal x, useVal y]   L.FCmp _op x y -> [useTypedVal x, useVal y]   L.GEP _ib _tp base args -> useTypedVal base : map useTypedVal args   L.Select c x y -> [ useTypedVal c, useTypedVal x, useVal y ]@@ -312,7 +312,7 @@ -- compute the list of assignments that must be made for each predecessor block. buildPhiMap :: [L.Stmt] -> Map L.BlockLabel (Seq (L.Ident, L.Type, L.Value)) buildPhiMap ss = go ss Map.empty- where go (L.Result ident (L.Phi tp xs) _ : stmts) m = go stmts (go' ident tp xs m)+ where go (L.Result ident (L.Phi tp xs) _ _ : stmts) m = go stmts (go' ident tp xs m)        go _ m = m         f x mseq = Just (fromMaybe Seq.empty mseq Seq.|> x)

@@ -52,6 +52,7 @@   , testBreakpointFunction   ) where +import qualified Control.Exception as X import           Control.Lens( to, (^.) ) import           Control.Monad import           Control.Monad.Except@@ -73,7 +74,6 @@ import qualified Data.BitVector.Sized.Overflow as BV import           Data.Parameterized.NatRepr import           Data.Parameterized.Some-import           Data.Parameterized.DecidableEq (decEq)  import           Lang.Crucible.LLVM.Bytes import           Lang.Crucible.LLVM.DataLayout( intLayout, EndianForm(..) )@@ -152,8 +152,7 @@ -- types, computing vectorization lanes, etc. -- -- As a concrete example, consider a call to--- @'translateGEP' inbounds baseTy basePtr elts@ with the following--- instruction:+-- @'translateGEP' attrs baseTy basePtr elts@ with the following instruction: -- -- @ -- getelementptr [12 x i8], ptr %aptr, i64 0, i32 1@@ -161,8 +160,10 @@ -- -- Here: ----- * @inbounds@ is 'False', as the keyword of the same name is missing from---   the instruction. (Currently, @crucible-llvm@ ignores this information.)+-- * @attrs@ is @[]@, as there are no @inbounds@, @nusw@, @nuw@, or @inrange@+--   attributes used in the instruction. (Currently, @crucible-llvm@ ignores+--   attribute information. See+--   <https://github.com/GaloisInc/crucible/issues/1605>.) -- -- * @baseTy@ is @[12 x i8]@. This is the type used as the basis for --   subsequent calculations.@@ -175,7 +176,7 @@ --   which of the elements of the aggregate object are indexed. translateGEP :: forall wptr m.   (?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>-  Bool              {- ^ inbounds flag -} ->+  [L.GEPAttr]       {- ^ attributes -} ->   L.Type            {- ^ base type for calculations -} ->   L.Typed L.Value   {- ^ base pointer expression -} ->   [L.Typed L.Value] {- ^ index arguments -} ->@@ -184,7 +185,7 @@ translateGEP _ _ _ [] =   throwError "getelementpointer must have at least one index" -translateGEP inbounds baseTy basePtr elts =+translateGEP attrs baseTy basePtr elts =   do baseMemType <- liftMemType baseTy      mt <- liftMemType (L.typedType basePtr)      -- Input value to a GEP must have a pointer type (or be a vector of pointer@@ -209,7 +210,7 @@          -> badGEP  where  badGEP :: m a- badGEP = throwError $ unlines [ "Invalid GEP", showInstr (L.GEP inbounds baseTy basePtr elts) ]+ badGEP = throwError $ unlines [ "Invalid GEP", showInstr (L.GEP attrs baseTy basePtr elts) ]   -- This auxilary function builds up the intermediate GEP mini-instructions that compute  -- the overall GEP, as well as the resulting memory type of the final pointers and the@@ -337,6 +338,9 @@   -- | The @undef@ value is quite strange. See: The LLVM Language Reference,   -- § Undefined Values.   UndefConst    :: !MemType -> LLVMConst+  -- | The @poison@ value is quite strange. See: The LLVM Language Reference,+  -- § Poison Values.+  PoisonConst   :: !MemType -> LLVMConst   -- | This also can't be derived, but is completely uninteresting.@@ -353,29 +357,9 @@       (StructConst si a)  -> ["StructConst", show si, show a]       (SymbolConst s x)   -> ["SymbolConst", show s, show x]       (UndefConst mem)    -> ["UndefConst", show mem]+      (PoisonConst mem)   -> ["PoisonConst", show mem]       (StringConst bs)    -> ["StringConst", show bs] --- | The interesting cases here are:---  * @IntConst@: GHC can't derive this because @IntConst@ existentially---    quantifies the integer's width. We say that two integers are equal when---    they have the same width *and* the same value.---  * @UndefConst@: Two @undef@ values aren't necessarily the same...-instance Eq LLVMConst where-  (ZeroConst mem1)      == (ZeroConst mem2)      = mem1 == mem2-  (IntConst w1 x1)      == (IntConst w2 x2)      =-    case decEq w1 w2 of-      Left Refl -> x1 == x2-      Right _   -> False-  (FloatConst f1)       == (FloatConst f2)       = f1 == f2-  (DoubleConst d1)      == (DoubleConst d2)      = d1 == d2-  (LongDoubleConst ld1) == (LongDoubleConst ld2) = ld1 == ld2-  (ArrayConst mem1 a1)  == (ArrayConst mem2 a2)  = mem1 == mem2 && a1 == a2-  (VectorConst mem1 v1) == (VectorConst mem2 v2) = mem1 == mem2 && v1 == v2-  (StructConst si1 a1)  == (StructConst si2 a2)  = si1 == si2   && a1 == a2-  (SymbolConst s1 x1)   == (SymbolConst s2 x2)   = s1 == s2     && x1 == x2-  (UndefConst  _)       == (UndefConst _)        = False-  _                     == _                     = False- -- | Create an LLVM constant value from a boolean. boolConst :: Bool -> LLVMConst boolConst False = IntConst (knownNat @1) (BV.zero knownNat)@@ -423,6 +407,8 @@   m LLVMConst transConstant' tp (L.ValUndef) =   return (UndefConst tp)+transConstant' tp (L.ValPoison) =+  return (PoisonConst tp) transConstant' (IntType n) (L.ValInteger x) =   intConst n x transConstant' (IntType 1) (L.ValBool b) =@@ -805,14 +791,19 @@       , DoubleConst d <- x       -> return $ IntConst w (BV.mkBV w (truncate d)) -    L.UiToFp+    L.UiToFp nneg       | FloatType <- mt       , IntConst _w i <- x-      -> return $ FloatConst (fromInteger (BV.asUnsigned i) :: Float)+      -> -- LLVM does not currently enable the `nneg` flag in constant+         -- expressions, only in instructions. As such, we don't use the flag+         -- below except to assert that it's disabled.+         X.assert (not nneg) $+         return $ FloatConst (fromInteger (BV.asUnsigned i) :: Float)        | DoubleType <- mt       , IntConst _w i <- x-      -> return $ DoubleConst (fromInteger (BV.asUnsigned i) :: Double)+      -> X.assert (not nneg) $+         return $ DoubleConst (fromInteger (BV.asUnsigned i) :: Double)      L.SiToFp       | FloatType <- mt@@ -823,23 +814,32 @@       , IntConst w i <- x       -> return $ DoubleConst (fromInteger (BV.asSigned w i) :: Double) -    L.Trunc+    L.Trunc nuw nsw       | IntType n <- mt       , IntConst w i <- x       , Just (Some w') <- someNat n       , Just LeqProof <- isPosNat w'-      -> case testNatCases w' w of+      -> -- LLVM does not currently enable the `nuw` or `nsw` flags in constant+         -- expressions, only in instructions. As such, we don't use the flags+         -- below except to assert that they're disabled.+         X.assert (not nuw) $+         X.assert (not nsw) $+         case testNatCases w' w of           NatCaseLT LeqProof -> return $ IntConst w' (BV.trunc w' i)           NatCaseEQ -> return x           NatCaseGT LeqProof ->             throwError $ "Attempted to truncate " <> show w <> " bits to " <> show w' -    L.ZExt+    L.ZExt nneg       | IntType n <- mt       , IntConst w i <- x       , Just (Some w') <- someNat n       , Just LeqProof <- isPosNat w'-      -> case testNatCases w w' of+      -> -- LLVM does not currently enable the `nneg` flag in constant+         -- expressions, only in instructions. As such, we don't use the flag+         -- below except to assert that it's disabled.+         X.assert (not nneg) $+         case testNatCases w w' of           NatCaseLT LeqProof -> return $ IntConst w' (BV.zext w' i)           NatCaseEQ -> return x           NatCaseGT LeqProof ->@@ -1085,8 +1085,8 @@   L.ConstExpr ->   m LLVMConst transConstantExpr expr = case expr of-  L.ConstGEP inbounds _inrange baseTy base exps -> -- TODO? pay attention to the inrange flag-    do gep <- translateGEP inbounds baseTy base exps+  L.ConstGEP attrs _inrange baseTy base exps -> -- TODO(#1605)? pay attention to the inrange flag+    do gep <- translateGEP attrs baseTy base exps        gep' <- traverse transConstant gep        snd <$> evalConstGEP gep' 

@@ -35,12 +35,15 @@   , pattern PointerExpr   , pattern BitvectorAsPointerExpr   , pointerAsBitvectorExpr+  , poisonBvExpr+  , poisonFloatExpr    , unpackOne   , unpackVec   , unpackArgs   , zeroExpand   , undefExpand+  , poisonExpand   , explodeVector    , constToLLVMVal@@ -121,6 +124,7 @@    BaseExpr   :: TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch    ZeroExpr   :: MemType -> LLVMExpr s arch    UndefExpr  :: MemType -> LLVMExpr s arch+   PoisonExpr :: MemType -> LLVMExpr s arch    VecExpr    :: MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch    StructExpr :: Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch @@ -128,6 +132,7 @@   show (BaseExpr ty x)  = C.showF x ++ " : " ++ show ty   show (ZeroExpr mt)    = "<zero :" ++ show mt ++ ">"   show (UndefExpr mt)   = "<undef :" ++ show mt ++ ">"+  show (PoisonExpr mt)  = "<poison :" ++ show mt ++ ">"   show (VecExpr _mt xs) = "[" ++ List.intercalate ", " (map show (toList xs)) ++ "]"   show (StructExpr xs)  = "{" ++ List.intercalate ", " (map f (toList xs)) ++ "}"     where f (_mt,x) = show x@@ -150,6 +155,9 @@ asScalar (UndefExpr llvmtp)   = let ?err = error      in undefExpand proxy# llvmtp $ \archProxy tpr ex -> Scalar archProxy tpr ex+asScalar (PoisonExpr llvmtp)+  = let ?err = error+     in poisonExpand proxy# llvmtp $ \archProxy tpr ex -> Scalar archProxy tpr ex asScalar _ = NotScalar  -- | Turn the expression into an explicit vector.@@ -158,6 +166,7 @@   case v of     ZeroExpr (VecType n t)  -> Just (t, Seq.replicate (fromIntegral n) (ZeroExpr t))     UndefExpr (VecType n t) -> Just (t, Seq.replicate (fromIntegral n) (UndefExpr t))+    PoisonExpr (VecType n t) -> Just (t, Seq.replicate (fromIntegral n) (PoisonExpr t))     VecExpr t s             -> Just (t, s)     _                       -> Nothing @@ -198,8 +207,18 @@                 (litExpr "Expected bitvector, but found pointer")      return off +poisonBvExpr ::+  (1 <= w) =>+  NatRepr w ->+  Expr LLVM s (BVType w)+poisonBvExpr w = App (ExtensionApp (LLVM_PoisonBV w)) +poisonFloatExpr ::+  FloatInfoRepr fi ->+  Expr LLVM s (FloatType fi)+poisonFloatExpr fi = App (ExtensionApp (LLVM_PoisonFloat fi)) + -- | Given a list of LLVMExpressions, "unpack" them into an assignment --   of crucible expressions. unpackArgs :: forall s a arch@@ -225,6 +244,7 @@    -> a unpackOne (BaseExpr tyr ex) k = k proxy# tyr ex unpackOne (UndefExpr tp) k = undefExpand proxy# tp k+unpackOne (PoisonExpr tp) k = poisonExpand proxy# tp k unpackOne (ZeroExpr tp) k = zeroExpand proxy# tp k unpackOne (StructExpr vs) k =   unpackArgs (map snd $ toList vs) $ \archProxy struct_ctx struct_asgn ->@@ -284,36 +304,103 @@             -> MemType             -> (forall tp. Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)             -> a-undefExpand _archProxy (IntType w) k =-  case mkNatRepr w of-    Some w' | Just LeqProof <- isPosNat w' ->-      k proxy# (LLVMPointerRepr w') $-         BitvectorAsPointerExpr w' $-         App $ BVUndef w'+undefExpand archProxy t k =+  case t of+    IntType w ->+      case mkNatRepr w of+        Some w' | Just LeqProof <- isPosNat w' ->+          k proxy# (LLVMPointerRepr w') $+             BitvectorAsPointerExpr w' $+             App $ BVUndef w' -    _ -> ?err $ unwords ["illegal integer size", show w]-undefExpand _archProxy (PtrType _tp) k =-   k proxy# PtrRepr $ BitvectorAsPointerExpr PtrWidth $ App $ BVUndef PtrWidth-undefExpand _archProxy PtrOpaqueType k =-   k proxy# PtrRepr $ BitvectorAsPointerExpr PtrWidth $ App $ BVUndef PtrWidth-undefExpand _archProxy (StructType si) k =-   unpackArgs (map UndefExpr tps) $ \archProxy ctx asgn -> k archProxy (StructRepr ctx) (mkStruct ctx asgn)- where tps = map fiType $ toList $ siFields si-undefExpand archProxy (ArrayType n tp) k =-  llvmTypeAsRepr tp $ \tpr -> unpackVec archProxy tpr (replicate (fromIntegral n) (UndefExpr tp)) $ k proxy# (VectorRepr tpr)-undefExpand archProxy (VecType n tp) k =-  llvmTypeAsRepr tp $ \tpr -> unpackVec archProxy tpr (replicate (fromIntegral n) (UndefExpr tp)) $ k proxy# (VectorRepr tpr)-undefExpand _archProxy FloatType k =-  k proxy# (FloatRepr SingleFloatRepr) (App (FloatUndef SingleFloatRepr))-undefExpand _archProxy DoubleType k =-  k proxy# (FloatRepr DoubleFloatRepr) (App (FloatUndef DoubleFloatRepr))-undefExpand _archProxy X86_FP80Type k =-  k proxy# (FloatRepr X86_80FloatRepr) (App (FloatUndef X86_80FloatRepr))-undefExpand _archPrxy tp _ = ?err $ unwords ["cannot undef expand type:", show tp]+        _ -> ?err $ unwords ["illegal integer size", show w]+    PtrType _tp ->+      k proxy# PtrRepr $+        BitvectorAsPointerExpr PtrWidth $ App $ BVUndef PtrWidth+    PtrOpaqueType ->+      k proxy# PtrRepr $+        BitvectorAsPointerExpr PtrWidth $ App $ BVUndef PtrWidth+    StructType si ->+      unpackArgs (map UndefExpr tps) $ \structArchProxy ctx asgn ->+        k structArchProxy (StructRepr ctx) (mkStruct ctx asgn)+      where tps = map fiType $ toList $ siFields si+    ArrayType n tp ->+      llvmTypeAsRepr tp $ \tpr ->+        unpackVec+          archProxy+          tpr+          (replicate (fromIntegral n) (UndefExpr tp))+          (k proxy# (VectorRepr tpr))+    VecType n tp ->+      llvmTypeAsRepr tp $ \tpr ->+        unpackVec+          archProxy+          tpr+          (replicate (fromIntegral n) (UndefExpr tp))+          (k proxy# (VectorRepr tpr))+    FloatType ->+      k proxy# (FloatRepr SingleFloatRepr) (App (FloatUndef SingleFloatRepr))+    DoubleType ->+      k proxy# (FloatRepr DoubleFloatRepr) (App (FloatUndef DoubleFloatRepr))+    X86_FP80Type ->+      k proxy# (FloatRepr X86_80FloatRepr) (App (FloatUndef X86_80FloatRepr))+    MetadataType ->+      ?err $ unwords ["cannot undef expand metadata type"] +poisonExpand :: ( ?err :: String -> a+                , HasPtrWidth (ArchWidth arch)+                )+             => Proxy# arch+             -> MemType+             -> (forall tp. Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)+             -> a+poisonExpand archProxy t k =+  case t of+    IntType w ->+      case mkNatRepr w of+        Some w' | Just LeqProof <- isPosNat w' ->+          k proxy# (LLVMPointerRepr w') $+             BitvectorAsPointerExpr w' $+             poisonBvExpr w' +        _ -> ?err $ unwords ["illegal integer size", show w]+    PtrType _tp ->+      k proxy# PtrRepr $+        BitvectorAsPointerExpr PtrWidth $ poisonBvExpr PtrWidth+    PtrOpaqueType ->+      k proxy# PtrRepr $+        BitvectorAsPointerExpr PtrWidth $ poisonBvExpr PtrWidth+    StructType si ->+      unpackArgs (map PoisonExpr tps) $ \structArchProxy ctx asgn ->+        k structArchProxy (StructRepr ctx) (mkStruct ctx asgn)+      where tps = map fiType $ toList $ siFields si+    ArrayType n tp ->+      llvmTypeAsRepr tp $ \tpr ->+        unpackVec+          archProxy+          tpr+          (replicate (fromIntegral n) (PoisonExpr tp))+          (k proxy# (VectorRepr tpr))+    VecType n tp ->+      llvmTypeAsRepr tp $ \tpr ->+        unpackVec+          archProxy+          tpr+          (replicate (fromIntegral n) (PoisonExpr tp))+          (k proxy# (VectorRepr tpr))+    FloatType ->+      k proxy# (FloatRepr SingleFloatRepr) (poisonFloatExpr SingleFloatRepr)+    DoubleType ->+      k proxy# (FloatRepr DoubleFloatRepr) (poisonFloatExpr DoubleFloatRepr)+    X86_FP80Type ->+      k proxy# (FloatRepr X86_80FloatRepr) (poisonFloatExpr X86_80FloatRepr)+    MetadataType ->+      ?err $ unwords ["cannot poison expand metadata type"]++ explodeVector :: Natural -> LLVMExpr s arch -> Maybe (Seq (LLVMExpr s arch)) explodeVector n (UndefExpr (VecType n' tp)) | n == n' = return (Seq.replicate (fromIntegral n) (UndefExpr tp))+explodeVector n (PoisonExpr (VecType n' tp)) | n == n' = return (Seq.replicate (fromIntegral n) (PoisonExpr tp)) explodeVector n (ZeroExpr (VecType n' tp)) | n == n' = return (Seq.replicate (fromIntegral n) (ZeroExpr tp)) explodeVector n (VecExpr _tp xs)   | n == fromIntegral (length xs) = return xs@@ -335,6 +422,8 @@     return $ ZeroExpr mt   UndefConst mt ->     return $ UndefExpr mt+  PoisonConst mt ->+    return $ PoisonExpr mt   IntConst w i ->     return $ BaseExpr (LLVMPointerRepr w) (BitvectorAsPointerExpr w (App (BVLit w i)))   FloatConst f ->@@ -395,6 +484,9 @@  transValue ty L.ValUndef =   return $ UndefExpr ty++transValue ty L.ValPoison =+  return $ PoisonExpr ty  transValue ty L.ValZeroInit =   return $ ZeroExpr ty

@@ -41,20 +41,16 @@ import           Control.Lens hiding (op, (:>) ) import           Control.Monad (MonadPlus(..), forM, unless) import           Control.Monad.Except (MonadError(..), runExceptT)-import           Control.Monad.State.Strict (MonadState(..), gets)+import           Control.Monad.State.Strict (MonadState(..)) 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 import           Data.Maybe-import           Data.Set (Set)-import qualified Data.Set as Set import           Data.Sequence (Seq) import qualified Data.Sequence as Seq import           Data.String@@ -83,7 +79,6 @@ import           Lang.Crucible.LLVM.Extension import           Lang.Crucible.LLVM.MemModel import           Lang.Crucible.LLVM.MemType-import qualified Lang.Crucible.LLVM.PrettyPrint as LPP import           Lang.Crucible.LLVM.Translation.Constant import           Lang.Crucible.LLVM.Translation.Expr import           Lang.Crucible.LLVM.Translation.Monad@@ -161,7 +156,7 @@     L.CallBr ty _ _ _ _ -> throwError $ unwords ["unexpected non-function type in callbr:", show ty]     L.Alloca ty _ _ -> liftMemType (L.PtrTo ty)     L.Load tp _ _ _ -> liftMemType tp-    L.ICmp _op tv _ -> do+    L.ICmp _samesign _op tv _ -> do       inpType <- liftMemType (L.typedType tv)       case inpType of         VecType len _ -> return (VecType len (IntType 1))@@ -173,8 +168,8 @@         _ -> return (IntType 1)     L.Phi tp _   -> liftMemType tp -    L.GEP inbounds baseTy basePtr elts ->-       do gepRes <- runExceptT (translateGEP inbounds baseTy basePtr elts)+    L.GEP attrs baseTy basePtr elts ->+       do gepRes <- runExceptT (translateGEP attrs baseTy basePtr elts)           case gepRes of             Left err -> throwError err             Right (GEPResult lanes tp _gep) ->@@ -239,10 +234,14 @@     -> LLVMGenerator s arch ret (LLVMExpr s arch) extractElt _instr ty _n (UndefExpr _) _i =    return $ UndefExpr ty+extractElt _instr ty _n (PoisonExpr _) _i =+   return $ PoisonExpr ty extractElt _instr ty _n (ZeroExpr _) _i =    return $ ZeroExpr ty extractElt _ ty _ _ (UndefExpr _) =    return $ UndefExpr ty+extractElt _ ty _ _ (PoisonExpr _) =+   return $ PoisonExpr ty extractElt instr ty n v (ZeroExpr zty) =    let ?err = fail in    zeroExpand (proxy# :: Proxy# arch) zty $ \_archProxy tyr ex -> extractElt instr ty n v (BaseExpr tyr ex)@@ -295,12 +294,16 @@     -> LLVMGenerator s arch ret (LLVMExpr s arch) insertElt _ ty _ _ _ (UndefExpr _) = do    return $ UndefExpr ty+insertElt _ ty _ _ _ (PoisonExpr _) = do+   return $ PoisonExpr ty insertElt instr ty n v a (ZeroExpr zty) = do    let ?err = fail    zeroExpand (proxy# :: Proxy# arch) zty $ \_archProxy tyr ex -> insertElt instr ty n v a (BaseExpr tyr ex)  insertElt instr ty n (UndefExpr _) a i  = do   insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (UndefExpr ty))) a i+insertElt instr ty n (PoisonExpr _) a i  = do+  insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (PoisonExpr ty))) a i insertElt instr ty n (ZeroExpr _) a i   = do   insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (ZeroExpr ty))) a i @@ -359,6 +362,11 @@  where tps = map fiType $ toList $ siFields si extractValue (UndefExpr (ArrayType n tp)) is =    extractValue (VecExpr tp $ Seq.replicate (fromIntegral n) (UndefExpr tp)) is+extractValue (PoisonExpr (StructType si)) is =+   extractValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, PoisonExpr tp)) tps) is+ where tps = map fiType $ toList $ siFields si+extractValue (PoisonExpr (ArrayType n tp)) is =+   extractValue (VecExpr tp $ Seq.replicate (fromIntegral n) (PoisonExpr tp)) is extractValue (ZeroExpr (StructType si)) is =    extractValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, ZeroExpr tp)) tps) is  where tps = map fiType $ toList $ siFields si@@ -392,6 +400,11 @@  where tps = map fiType $ toList $ siFields si insertValue (UndefExpr (ArrayType n tp)) v is =    insertValue (VecExpr tp $ Seq.replicate (fromIntegral n) (UndefExpr tp)) v is+insertValue (PoisonExpr (StructType si)) v is =+   insertValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, PoisonExpr tp)) tps) v is+ where tps = map fiType $ toList $ siFields si+insertValue (PoisonExpr (ArrayType n tp)) v is =+   insertValue (VecExpr tp $ Seq.replicate (fromIntegral n) (PoisonExpr tp)) v is insertValue (ZeroExpr (StructType si)) v is =    insertValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, ZeroExpr tp)) tps) v is  where tps = map fiType $ toList $ siFields si@@ -535,8 +548,8 @@              in                -- Multiplication overflow will result in a pointer which is not "in                -- bounds" for the given allocation. We translate all GEP-               -- instructions as if they had the `inbounds` flag set, so the-               -- result would be a poison value.+               -- instructions as if they had the `inbounds` attribute set, so+               -- the result would be a poison value.                poisonSideCondition mvar (BVRepr PtrWidth) poison off0 cond       -- Perform the pointer offset arithmetic@@ -577,8 +590,10 @@   | n == m = VecExpr outty <$> traverse (\x -> translateConversion instr op inty x outty) xs  -- Otherwise, assume scalar values and do the basic conversions-translateConversion instr op _inty x outty =- let showI = showInstr instr in+translateConversion instr op _inty x outty = do+ mvar <- getMemVar+ let showI = showInstr instr+ let noLaxArith = not (laxArith ?transOpts)  case op of     L.IntToPtr -> do        llvmTypeAsRepr outty $ \outty' ->@@ -601,26 +616,46 @@               , Just Refl <- testEquality w' PtrWidth -> return x            _ -> fail (unlines ["pointer-to-integer conversion failed", showI]) -    L.Trunc -> do+    L.Trunc nuw nsw -> do        llvmTypeAsRepr outty $ \outty' ->          case (asScalar x, outty') of            (Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w'))              | Just LeqProof <- isPosNat w'              , Just LeqProof <- testLeq (incNat w') w ->                  do x_bv <- pointerAsBitvectorExpr w x'-                    let bv' = App (BVTrunc w' w x_bv)-                    return (BaseExpr outty' (BitvectorAsPointerExpr w' bv'))+                    bv' <- AtomExpr <$> mkAtom (App (BVTrunc w' w x_bv))+                    result <- sideConditionsA mvar (BVRepr w') bv'+                      [ ( nuw && noLaxArith+                        , fmap (App . BVEq w x_bv . AtomExpr)+                               (mkAtom (App (BVZext w w' bv')))+                        , UB.PoisonValueCreated $ Poison.TruncNoUnsignedWrap x_bv+                        )+                      , ( nsw && noLaxArith+                        , fmap (App . BVEq w x_bv . AtomExpr)+                               (mkAtom (App (BVSext w w' bv')))+                        , UB.PoisonValueCreated $ Poison.TruncNoSignedWrap x_bv+                        )+                      ]+                    return (BaseExpr outty' (BitvectorAsPointerExpr w' result))            _ -> fail (unlines [unwords ["invalid truncation:", show x, show outty], showI]) -    L.ZExt -> do+    L.ZExt nneg -> do        llvmTypeAsRepr outty $ \outty' ->          case (asScalar x, outty') of            (Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w'))              | Just LeqProof <- isPosNat w              , Just LeqProof <- testLeq (incNat w) w' ->                  do x_bv <- pointerAsBitvectorExpr w x'-                    let bv' = App (BVZext w' w x_bv)-                    return (BaseExpr outty' (BitvectorAsPointerExpr w' bv'))+                    bv' <- AtomExpr <$> mkAtom (App (BVZext w' w x_bv))+                    let z = App $ BVLit w $ BV.zero w+                    result <-+                      sideConditionsA mvar (BVRepr w') bv'+                        [ ( nneg+                          , pure $ App $ BVSle w z x_bv+                          , UB.PoisonValueCreated $ Poison.ZExtNonNegative x_bv+                          )+                        ]+                    return (BaseExpr outty' (BitvectorAsPointerExpr w' result))            _ -> fail (unlines [unwords ["invalid zero extension:", show x, show outty], showI])      L.SExt -> do@@ -640,12 +675,21 @@     L.BitCast -> bitCast _inty x outty #endif -    L.UiToFp -> do+    L.UiToFp nneg -> do        llvmTypeAsRepr outty $ \outty' ->          case (asScalar x, outty') of            (Scalar _archProxy (LLVMPointerRepr w) x', FloatRepr fi) -> do              bv <- pointerAsBitvectorExpr w x'-             return $ BaseExpr (FloatRepr fi) $ App $ FloatFromBV fi RNE bv+             bvFp <- AtomExpr <$> mkAtom (App (FloatFromBV fi RNE bv))+             let z = App $ BVLit w $ BV.zero w+             result <-+               sideConditionsA mvar outty' bvFp+                 [ ( nneg+                   , pure $ App $ BVSle w z bv+                   , UB.PoisonValueCreated $ Poison.UiToFpNonNegative bv+                   )+                 ]+             return $ BaseExpr (FloatRepr fi) result            _ -> fail (unlines [unwords ["Invalid uitofp:", show op, show x, show outty], showI])      L.SiToFp -> do@@ -701,6 +745,8 @@  bitCast _ (UndefExpr _) tgtT = return (UndefExpr tgtT) +bitCast _ (PoisonExpr _) tgtT = return (PoisonExpr tgtT)+ -- pointer casts always succeed bitCast (PtrType _) expr (PtrType _) = return expr bitCast (PtrType _) expr PtrOpaqueType = return expr@@ -1271,25 +1317,30 @@   integerCompare ::+  -- ^ If 'True', require that the arguments have the same sign.+  Bool ->   L.ICmpOp ->   MemType ->   LLVMExpr s arch ->   LLVMExpr s arch ->   LLVMGenerator s arch ret (LLVMExpr s arch)-integerCompare op (VecType n tp) (explodeVector n -> Just xs) (explodeVector n -> Just ys) =-  VecExpr (IntType 1) <$> sequence (Seq.zipWith (\x y -> integerCompare op tp x y) xs ys)+integerCompare samesign op (VecType n tp) (explodeVector n -> Just xs) (explodeVector n -> Just ys) =+  VecExpr (IntType 1) <$> sequence (Seq.zipWith (\x y -> integerCompare samesign op tp x y) xs ys) -integerCompare op _ x y = do-  b <- scalarIntegerCompare op x y+integerCompare samesign op _ x y = do+  b <- scalarIntegerCompare samesign op x y   return (BaseExpr (LLVMPointerRepr (knownNat :: NatRepr 1))                    (BitvectorAsPointerExpr knownNat (App (BoolToBV knownNat b))))  scalarIntegerCompare ::+  -- ^ If 'True', require that the arguments have the same sign.+  Bool ->   L.ICmpOp ->   LLVMExpr s arch ->   LLVMExpr s arch ->   LLVMGenerator s arch ret (Expr LLVM s BoolType)-scalarIntegerCompare op x y =+scalarIntegerCompare samesign op x y = do+  mvar <- getMemVar   case (asScalar x, asScalar y) of     (Scalar _archProxy (LLVMPointerRepr w) x'', Scalar _archProxy' (LLVMPointerRepr w') y'')        | Just Refl <- testEquality w w'@@ -1298,7 +1349,14 @@        | Just Refl <- testEquality w w'        -> do xbv <- pointerAsBitvectorExpr w x''              ybv <- pointerAsBitvectorExpr w y''-             return (intcmp w op xbv ybv)+             result <- AtomExpr <$> mkAtom (intcmp w op xbv ybv)+             let z = App $ BVLit w $ BV.zero w+             sideConditionsA mvar BoolRepr result+               [ ( samesign+                 , pure $ App $ BoolEq (App (BVSlt w xbv z)) (App (BVSlt w ybv z))+                 , UB.PoisonValueCreated $ Poison.ICmpSameSign xbv ybv+                 )+               ]     _ -> fail $ unlines [ "arithmetic comparison on incompatible values"                         , "Comparison: " ++ show op                         , "Value 1: " ++ show x@@ -1514,7 +1572,6 @@    (?transOpts :: TranslationOptions) =>    TypeRepr ret   {- ^ Type of the function return value -} ->    L.BlockLabel   {- ^ The label of the current LLVM basic block -} ->-   Set L.Ident {- ^ Set of usable identifiers -} ->    L.Instr        {- ^ The instruction to translate -} ->    (LLVMExpr s arch -> LLVMGenerator s arch ret ())      {- ^ A continuation to assign the produced value of this instruction to a register -} ->@@ -1523,7 +1580,7 @@           Straightline instructions should enter this continuation,           but block-terminating instructions should not. -} ->    LLVMGenerator s arch ret a-generateInstr retType lab defSet instr assign_f k =+generateInstr retType lab instr assign_f k =   case instr of     -- skip phi instructions, they are handled in definePhiBlock     L.Phi _ _ -> k@@ -1591,6 +1648,7 @@                  do let getV x =                           case x of                             UndefExpr _ -> return $ UndefExpr elTy+                            PoisonExpr _ -> return $ PoisonExpr elTy                             ZeroExpr _  -> return $ Seq.index v1 0                             BaseExpr (LLVMPointerRepr _) (BitvectorAsPointerExpr _ (App (BVLit _ i)))                               | BV.asUnsigned i < inL -> return $ Seq.index v1 (fromIntegral (BV.asUnsigned i))@@ -1671,11 +1729,14 @@       callStore vTp ptr' v' align'       k -    -- NB We treat every GEP as though it has the "inbounds" flag set;+    -- NB We treat every GEP as though it has the "inbounds" attribute set;     --    thus, the calculation of out-of-bounds pointers results in     --    a runtime error.-    L.GEP inbounds baseTy basePtr elts -> do-      runExceptT (translateGEP inbounds baseTy basePtr elts) >>= \case+    --+    --    TODO(#1605): Don't error immediately if the "inbounds" attribute isn't+    --    set.+    L.GEP attrs baseTy basePtr elts -> do+      runExceptT (translateGEP attrs baseTy basePtr elts) >>= \case         Left err -> reportError $ fromString $ unlines ["Error translating GEP", err]         Right gep ->           do gep' <- traverse (\v -> transTypedValue v) gep@@ -1692,14 +1753,14 @@          k      L.Call tailcall fnTy fn args ->-      callFunction defSet instr tailcall fnTy fn args assign_f >> k+      callFunction instr tailcall fnTy fn args assign_f >> k      L.Invoke fnTy fn args normLabel _unwindLabel -> do-      do callFunction defSet instr False fnTy fn args assign_f+      do callFunction instr False fnTy fn args assign_f          definePhiBlock lab normLabel      L.CallBr fnTy fn args normLabel otherLabels -> do-      do callFunction defSet instr False fnTy fn args assign_f+      do callFunction instr False fnTy fn args assign_f          for_ otherLabels $ \lab' -> void (definePhiBlock lab lab')          definePhiBlock lab normLabel @@ -1734,11 +1795,11 @@            assign_f cmp            k -    L.ICmp op x y -> do+    L.ICmp samesign op x y -> do            tp <- liftMemType' (L.typedType x)            x' <- transTypedValue x            y' <- transTypedValue (L.Typed (L.typedType x) y)-           cmp <- integerCompare op tp x' y'+           cmp <- integerCompare samesign op tp x' y'            assign_f cmp            k @@ -1803,7 +1864,7 @@                let a0 = memTypeAlign (llvmDataLayout ?lc) resTy               oldVal <- callLoad resTy expectTy ptr' a0-              cmp <- scalarIntegerCompare L.Ieq oldVal cmpVal+              cmp <- scalarIntegerCompare False L.Ieq oldVal cmpVal               let flag = BaseExpr (LLVMPointerRepr (knownNat @1))                                   (BitvectorAsPointerExpr knownNat                                      (App (BoolToBV knownNat cmp)))@@ -2006,7 +2067,6 @@ -- for debugging intrinsics and breakpoint functions. callFunction :: forall s arch ret.    (?transOpts :: TranslationOptions) =>-   Set L.Ident {- ^ Set of usable identifiers -} ->    L.Instr {- ^ Source instruction of the call -} ->    Bool    {- ^ Is the function a tail call? -} ->    L.Type  {- ^ type of the function to call -} ->@@ -2014,42 +2074,8 @@    [L.Typed L.Value] {- ^ argument list -} ->    (LLVMExpr s arch -> LLVMGenerator s arch ret ()) {- ^ assignment continuation for return value -} ->    LLVMGenerator s arch ret ()-callFunction defSet instr tailCall_ fnTy fn args assign_f--     -- Supports LLVM 4-12-     | L.ValSymbol "llvm.dbg.declare" <- fn-     , debugIntrinsics ?transOpts =-       do mbArgs <- dbgArgs defSet args-          case mbArgs of-            Right (asScalar -> Scalar _ PtrRepr ptr, lv, di) ->-              do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Declare ptr lv di))-                 return ()-            Left msg -> addWarning (Text.pack msg)-            _ -> addWarning "Unexpected argument in llvm.dbg.declare"--     -- Supports LLVM 6-12-     | L.ValSymbol "llvm.dbg.addr" <- fn-     , debugIntrinsics ?transOpts =-       do mbArgs <- dbgArgs defSet args-          case mbArgs of-            Right (asScalar -> Scalar _ PtrRepr ptr, lv, di) ->-              do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Addr ptr lv di))-                 return ()-            Left msg -> addWarning (Text.pack msg)-            _ -> addWarning "Unexpected argument in llvm.dbg.addr"--     -- Supports LLVM 6-12 (earlier versions had an extra argument)-     | L.ValSymbol "llvm.dbg.value" <- fn-     , debugIntrinsics ?transOpts =-       do mbArgs <- dbgArgs defSet args-          case mbArgs of-            Right (asScalar -> Scalar _ repr val, lv, di) ->-              do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Value repr val lv di))-                 return ()-            Left msg -> addWarning (Text.pack msg)-            _ -> addWarning "Unexpected argument in llvm.dbg.value"--     -- Skip calls to other debugging intrinsics.+callFunction instr tailCall_ fnTy fn args assign_f+     -- Skip calls to debugging intrinsics.      | L.ValSymbol nm <- fn      , nm `elem` [ "llvm.dbg.label"                  , "llvm.dbg.declare"@@ -2080,83 +2106,6 @@       | 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 = do-    unnamedMd <- gets (llvmUnnamedMd . llvmContext)-    case args of-      [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 ->   LLVMGenerator s arch ret (Some (Value s))@@ -2265,6 +2214,12 @@     case testEquality (typeOfReg r) tpr of       Just Refl -> assignReg r ex       Nothing -> reportError $ fromString $ "type mismatch when assigning undef value"+doAssign (Some r) (PoisonExpr tp) = do+  let ?err = fail+  poisonExpand (proxy# :: Proxy# arch) tp $ \_archProxy (tpr :: TypeRepr t) (ex :: Expr LLVM s t) ->+    case testEquality (typeOfReg r) tpr of+      Just Refl -> assignReg r ex+      Nothing -> reportError $ fromString $ "type mismatch when assigning poison value" doAssign (Some r) (VecExpr tp vs) = do   let ?err = fail   llvmTypeAsRepr tp $ \tpr ->

@@ -53,8 +53,6 @@ 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)@@ -97,9 +95,6 @@      -- | 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@@ -113,8 +108,6 @@   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 ->@@ -130,7 +123,6 @@                      , _llvmTypeCtx = typeCtx                      , llvmGlobalAliases = mempty   -- these are computed later                      , llvmFunctionAliases = mempty -- these are computed later-                     , llvmUnnamedMd = unnamedMd                      }            return (Some ctx)     _ ->

@@ -60,7 +60,8 @@                           (L.PtrTo                             (L.Alias (L.Ident "class.std::cls"))) Nothing (Just 8))                         []-                      , L.Effect L.RetVoid []+                        []+                      , L.Effect L.RetVoid [] []                       ]                   }                 ]

@@ -15,6 +15,7 @@ import           Lang.Crucible.FunctionHandle ( newHandleAllocator )  import qualified Data.BitVector.Sized as BV+import           Data.Parameterized.DecidableEq ( decEq ) import           Data.Parameterized.Some import           Data.Parameterized.NatRepr import           Data.Parameterized.SymbolRepr ( SomeSym(SomeSym) )@@ -35,6 +36,8 @@ import           Control.Lens (view) import           Control.Monad import           Data.Either ( fromRight )+import           Data.Functor.Classes ( Eq1(liftEq) )+import           Data.Functor.Identity ( Identity(..) ) import           Data.Maybe ( catMaybes ) import           GHC.TypeLits import qualified Data.Map.Strict as Map@@ -264,31 +267,133 @@   "extern_int" ->     testCase "valid global extern variable reference" $ do     Some t <- getTrans-    Map.singleton (L.Symbol "extern_int") (Right (i32, Nothing)) @=?-      Map.map snd (view globalInitMap t)+    case snd <$> Map.lookup (L.Symbol "extern_int") (view globalInitMap t) of+      Just (Right (actualTy, actualMbConst)) -> do+        let expectedTy = i32+        let expectedMbConst = Nothing+        expectedTy @=? actualTy+        assertLiftEq llvmConstSyntacticEq expectedMbConst actualMbConst+      _ -> assertFailure "Could not look up extern_int"    "x=42" ->     testCase "valid global integer symbol reference" $ do     Some t <- getTrans-    Map.singleton (L.Symbol "x") (Right $ (i32, Just $ IntConst (knownNat @32) (BV.mkBV knownNat 42))) @=?-      Map.map snd (view globalInitMap t)+    case snd <$> Map.lookup (L.Symbol "x") (view globalInitMap t) of+      Just (Right (actualTy, actualMbConst)) -> do+        let expectedTy = i32+        let expectedMbConst = Just $ IntConst (knownNat @32) (BV.mkBV knownNat 42)+        expectedTy @=? actualTy+        assertLiftEq llvmConstSyntacticEq expectedMbConst actualMbConst+      _ -> assertFailure "Could not look up x"    "z.xx=17" ->     testCase "valid global struct field symbol reference" $ do     Some t <- getTrans-    IntConst (knownNat @32) (BV.mkBV knownNat 17) @=?-      case snd <$> Map.lookup (L.Symbol "z") (view globalInitMap t) of-        Just (Right (_, Just (StructConst _ (x : _)))) -> x-        _ -> IntConst (knownNat @1) (BV.zero knownNat)+    case snd <$> Map.lookup (L.Symbol "z") (view globalInitMap t) of+      Just (Right (_, actualMbConst)) ->+        case actualMbConst of+          Just (StructConst _ (actualXField : _)) -> do+            let expectedXField = IntConst (knownNat @32) (BV.mkBV knownNat 17)+            assertLiftEq+              llvmConstSyntacticEq+              (Identity expectedXField)+              (Identity actualXField)+          _ -> assertFailure $+            "Expected x to be a struct with at least one field, " +++            "but it was actually " ++ show actualMbConst+      _ -> assertFailure "Could not look up z"    "x uninitialized" ->     testCase "valid global unitialized variable reference" $ do     Some t <- getTrans-    Map.singleton (L.Symbol "x") (Right $ (i32, Just $ ZeroConst i32)) @=?-      Map.map snd (view globalInitMap t)+    case snd <$> Map.lookup (L.Symbol "x") (view globalInitMap t) of+      Just (Right (actualTy, actualMbConst)) -> do+        let expectedTy = i32+        let expectedMbConst = Just $ ZeroConst i32+        expectedTy @=? actualTy+        assertLiftEq llvmConstSyntacticEq expectedMbConst actualMbConst+      _ -> assertFailure "Could not look up x"    -- We're really just checking that the translation succeeds without   -- exceptions.   "" -> testCase "no additional checks" $ return ()    other -> testCase other $ assertFailure $ "Unknown check: " <> other++-- | Helper, not exported+--+-- Compare two 'LLVMConst's for syntactic equality. This should not be confused+-- with the semantic notion of equality that LLVM typically uses. For instance,+-- this function considers two 'UndefConst's values to be syntactically equal,+-- but LLVM's semantic equality could deem two @undef@ values to be not equal.+llvmConstSyntacticEq :: LLVMConst -> LLVMConst -> Bool+llvmConstSyntacticEq (ZeroConst mem1) (ZeroConst mem2) =+  mem1 == mem2+llvmConstSyntacticEq (IntConst w1 x1) (IntConst w2 x2) =+  case decEq w1 w2 of+    Left Refl -> x1 == x2+    Right _   -> False+llvmConstSyntacticEq (FloatConst f1) (FloatConst f2) =+  f1 == f2+llvmConstSyntacticEq (DoubleConst d1) (DoubleConst d2) =+  d1 == d2+llvmConstSyntacticEq (LongDoubleConst ld1) (LongDoubleConst ld2) =+  ld1 == ld2+llvmConstSyntacticEq (StringConst s1) (StringConst s2) =+  s1 == s2+llvmConstSyntacticEq (ArrayConst mem1 a1) (ArrayConst mem2 a2) =+  mem1 == mem2 && liftEq llvmConstSyntacticEq a1 a2+llvmConstSyntacticEq (VectorConst mem1 v1) (VectorConst mem2 v2) =+  mem1 == mem2 && liftEq llvmConstSyntacticEq v1 v2+llvmConstSyntacticEq (StructConst si1 a1) (StructConst si2 a2) =+  si1 == si2 && liftEq llvmConstSyntacticEq a1 a2+llvmConstSyntacticEq (SymbolConst s1 x1) (SymbolConst s2 x2) =+  s1 == s2 && x1 == x2+llvmConstSyntacticEq (UndefConst tp1) (UndefConst tp2) =+  tp1 == tp2+llvmConstSyntacticEq (PoisonConst tp1) (PoisonConst tp2) =+  tp1 == tp2++llvmConstSyntacticEq (ZeroConst {}) _ =+  False+llvmConstSyntacticEq (IntConst {}) _ =+  False+llvmConstSyntacticEq (FloatConst {}) _ =+  False+llvmConstSyntacticEq (DoubleConst {}) _ =+  False+llvmConstSyntacticEq (LongDoubleConst {}) _ =+  False+llvmConstSyntacticEq (StringConst {}) _ =+  False+llvmConstSyntacticEq (ArrayConst {}) _ =+  False+llvmConstSyntacticEq (VectorConst {}) _ =+  False+llvmConstSyntacticEq (StructConst {}) _ =+  False+llvmConstSyntacticEq (SymbolConst {}) _ =+  False+llvmConstSyntacticEq (UndefConst {}) _ =+  False+llvmConstSyntacticEq (PoisonConst {}) _ =+  False++-- | Helper, not exported+--+-- Like 'assertEqual', but lifted to work over an 'Eq1' instance instead of an+-- 'Eq' instance. In addition, this allows the user to customize how to check+-- the underlying values (of type @expected@ and @actual@) for equality.+assertLiftEq ::+  (Eq1 f, Show (f expected), Show (f actual), HasCallStack) =>+  -- | How to check the underlying values for equality+  (expected -> actual -> Bool) ->+  -- | The expected value+  f expected ->+  -- | The actual value+  f actual ->+  Assertion+assertLiftEq eq expected actual =+  unless (liftEq eq expected actual) (assertFailure msg)+  where+    msg = "expected: " ++ show expected ++ "\n but got: " ++ show actual