packages feed

crucible-llvm 0.7.1 → 0.9

raw patch · 32 files changed

Files

CHANGELOG.md view
@@ -1,3 +1,66 @@+# 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 `loadProvablyNullTerminatedString`.+* Add a new "low-level" API for loading strings to+  `Lang.Crucible.LLVM.MemModel.Strings`: `ByteLoader`, `ByteChecker`, and+  `loadBytes`.+* Support simulating LLVM bitcode files whose data layout strings specify+  function pointer alignment.+* Fix a bug that would cause the simuator to compute incorrect results for the+  `llvm.is.fpclass` intrinsic. (Among other things, this is used to power the+  `isnan` function in Clang 17 or later.)+* Support vectorized versions of the `llvm.u{min,max}` and `llvm.s{min,max}`+  intrinsics.+ # 0.7.1 -- 2025-03-21  * Fix a bug in which the memory model would panic when attempting to unpack@@ -52,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
crucible-llvm.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crucible-llvm-Version:       0.7.1+Version:       0.9 Author:        Galois Inc. Copyright:     (c) Galois, Inc 2014-2022 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com@@ -29,22 +29,112 @@   ghc-prof-options: -O2 -fprof-auto-exported   default-language: Haskell2010 +common warns+  -- Specifying -Wall and -Werror can cause the project to fail to build on+  -- newer versions of GHC simply due to new warnings being added to -Wall. To+  -- prevent this from happening we manually list which warnings should be+  -- considered errors. We also list some warnings that are not in -Wall, though+  -- try to avoid "opinionated" warnings (though this judgement is clearly+  -- subjective).+  --+  -- Warnings are grouped by the GHC version that introduced them, and then+  -- alphabetically.+  --+  -- A list of warnings and the GHC version in which they were introduced is+  -- available here:+  -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html +  -- Since GHC 9.6 or earlier:+  ghc-options:+    -Wall+    -Werror=ambiguous-fields+    -Werror=compat-unqualified-imports+    -Werror=deferred-type-errors+    -Werror=deprecated-flags+    -Werror=deprecations+    -Werror=deriving-defaults+    -Werror=deriving-typeable+    -Werror=dodgy-foreign-imports+    -Werror=duplicate-exports+    -Werror=empty-enumerations+    -Werror=gadt-mono-local-binds+    -Werror=identities+    -Werror=inaccessible-code+    -Werror=incomplete-patterns+    -Werror=incomplete-record-updates+    -Werror=incomplete-uni-patterns+    -Werror=inline-rule-shadowing+    -Werror=misplaced-pragmas+    -Werror=missed-extra-shared-lib+    -Werror=missing-exported-signatures+    -Werror=missing-fields+    -Werror=missing-home-modules+    -Werror=missing-methods+    -Werror=missing-pattern-synonym-signatures+    -Werror=missing-signatures+    -Werror=name-shadowing+    -Werror=noncanonical-monad-instances+    -Werror=noncanonical-monoid-instances+    -Werror=operator-whitespace+    -Werror=operator-whitespace-ext-conflict+    -Werror=orphans+    -Werror=overflowed-literals+    -Werror=overlapping-patterns+    -Werror=partial-fields+    -Werror=partial-type-signatures+    -Werror=redundant-bang-patterns+    -Werror=redundant-record-wildcards+    -Werror=redundant-strictness-flags+    -Werror=simplifiable-class-constraints+    -Werror=star-binder+    -Werror=star-is-type+    -Werror=tabs+    -Werror=type-defaults+    -Werror=typed-holes+    -Werror=type-equality-out-of-scope+    -Werror=type-equality-requires-operators+    -Werror=unicode-bidirectional-format-characters+    -Werror=unrecognised-pragmas+    -Werror=unrecognised-warning-flags+    -Werror=unsupported-calling-conventions+    -Werror=unsupported-llvm-version+    -Werror=unused-do-bind+    -Werror=unused-imports+    -Werror=unused-record-wildcards+    -Werror=warnings-deprecations+    -Werror=wrong-do-bind++  if impl(ghc < 9.8)+    ghc-options:+      -Werror=forall-identifier++  if impl(ghc >= 9.8)+    ghc-options:+      -Werror=incomplete-export-warnings+      -Werror=inconsistent-flags++  if impl(ghc >= 9.10)+    ghc-options:+      -Werror=badly-staged-types+      -Werror=data-kinds-tc+      -Werror=deprecated-type-abstractions+      -Werror=incomplete-record-selectors+ library   import: bldflags   build-depends:-    base >= 4.13 && < 4.20,+    base >= 4.13 && < 4.21,     attoparsec,     bv-sized >= 1.0.0,     bytestring,     containers >= 0.5.8.0,     crucible >= 0.5,     crucible-symio,-    what4 >= 0.4.1,+    what4 >= 0.5,     extra,     lens,     itanium-abi >= 0.1.1.1 && < 0.2,-    llvm-pretty >= 0.12.1 && < 0.14,+    llvm-pretty >= 0.12.1 && < 0.15,     mtl,     parameterized-utils >= 2.1.5 && < 2.2,     pretty,@@ -73,6 +163,7 @@     Lang.Crucible.LLVM.Extension     Lang.Crucible.LLVM.Functions     Lang.Crucible.LLVM.Globals+    Lang.Crucible.LLVM.Internal     Lang.Crucible.LLVM.Intrinsics     Lang.Crucible.LLVM.Intrinsics.Cast     Lang.Crucible.LLVM.Intrinsics.Libc@@ -85,6 +176,7 @@     Lang.Crucible.LLVM.MemModel.MemLog     Lang.Crucible.LLVM.MemModel.Partial     Lang.Crucible.LLVM.MemModel.Pointer+    Lang.Crucible.LLVM.MemModel.Strings     Lang.Crucible.LLVM.MemType     Lang.Crucible.LLVM.PrettyPrint     Lang.Crucible.LLVM.Printf@@ -124,6 +216,7 @@  test-suite crucible-llvm-tests   import: bldflags+  import: warns   type: exitcode-stdio-1.0   main-is: Tests.hs   hs-source-dirs: test
src/Lang/Crucible/LLVM/DataLayout.hs view
@@ -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@@ -164,12 +158,13 @@ data DataLayout    = 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]         }@@ -184,6 +179,14 @@ stackAlignment :: Lens' DataLayout Alignment stackAlignment = lens _stackAlignment (\s v -> s { _stackAlignment = v}) +functionPtrAlignment :: Lens' DataLayout Alignment+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})@@ -201,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})@@ -238,12 +237,13 @@ defaultDataLayout = execState defaults dl   where dl = DL { _intLayout = BigEndian                 , _stackAlignment = noAlignment+                , _functionPtrAlignment = noAlignment                 , _ptrSize  = 8 -- 64 bit pointers = 8 bytes                 , _ptrAlign = Alignment 3 -- 64 bit alignment: 2^3=8 byte boundaries+                , _aggregateAlignment = noAlignment -- Aggregates are 1-byte aligned.                 , _integerInfo = emptyAlignInfo                 , _floatInfo   = emptyAlignInfo                 , _vectorInfo  = emptyAlignInfo-                , _aggInfo     = emptyAlignInfo                 , _stackInfo   = emptyAlignInfo                 , _layoutWarnings = []                 }@@ -262,18 +262,17 @@           -- 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 maxAlignment dl =   maximum [ dl^.stackAlignment+          , dl^.functionPtrAlignment           , dl^.ptrAlign+          , dl^.aggregateAlignment           , maxAlignmentInTree (dl^.integerInfo)           , maxAlignmentInTree (dl^.vectorInfo)           , maxAlignmentInTree (dl^.floatInfo)-          , maxAlignmentInTree (dl^.aggInfo)           , maxAlignmentInTree (dl^.stackInfo)           ] @@ -282,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:)@@ -302,27 +301,46 @@     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+      -- us whether the function pointer alignment is related to the alignment+      -- of functions, but llvm-pretty currently does not track the alignment of+      -- individual functions, so we have no use for this info just yet. When+      -- https://github.com/GaloisInc/llvm-pretty/issues/164 is implemented, we+      -- should revisit this.+      L.FunctionPointerAlign _ a -> setBits functionPtrAlignment ls a       L.Mangling _      -> return ()+      -- 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
src/Lang/Crucible/LLVM/Errors/MemoryError.hs view
@@ -6,6 +6,7 @@ -- Maintainer       : Langston Barrett <lbarrett@galois.com> -- Stability        : provisional --+-- See @crucible-llvm-cli/test-data/ub@ for tests demonstrating some of these. --------------------------------------------------------------------------  {-# LANGUAGE DataKinds #-}@@ -37,7 +38,6 @@  import           Data.Text (Text) import qualified Text.LLVM.AST as L-import           Type.Reflection (SomeTypeRep(SomeTypeRep)) import           Prettyprinter  import           What4.Interface@@ -99,7 +99,6 @@   = SymbolicPointer   | RawBitvector   | NoOverride-  | Uncallable SomeTypeRep   deriving (Eq, Ord)  ppFuncLookupError :: FuncLookupError -> Doc ann@@ -108,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
src/Lang/Crucible/LLVM/Errors/Poison.hs view
@@ -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   -- -----------------------------------------------------------------------
src/Lang/Crucible/LLVM/Errors/Standards.hs view
@@ -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
src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs view
@@ -20,6 +20,8 @@ -- code essentially have an additional hypothesis: that the LLVM -- compiler/hardware platform behave identically to Crucible's simulator when -- encountering such behavior.+--+-- See @crucible-llvm-cli/test-data/ub@ for tests demonstrating some of these. --------------------------------------------------------------------------  {-# LANGUAGE DataKinds #-}
src/Lang/Crucible/LLVM/Eval.hs view
@@ -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+        ]
src/Lang/Crucible/LLVM/Extension/Syntax.hs view
@@ -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|] [])
src/Lang/Crucible/LLVM/Globals.hs view
@@ -46,7 +46,8 @@ import           Control.Monad.IO.Class (MonadIO(..)) import           Control.Monad.Except (MonadError(..)) import           Control.Lens hiding (op, (:>) )-import           Data.List (foldl', genericLength, isPrefixOf)+import qualified Data.Foldable as Foldable+import           Data.List (genericLength, isPrefixOf) import           Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import qualified Data.Set as Set@@ -107,7 +108,7 @@               => LLVMContext arch               -> L.Module               -> GlobalInitializerMap-makeGlobalMap ctx m = foldl' addAliases globalMap1 (Map.toList (llvmGlobalAliases ctx))+makeGlobalMap ctx m = Foldable.foldl' addAliases globalMap1 (Map.toList (llvmGlobalAliases ctx))    where    addAliases mp (glob, aliases) =@@ -433,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])@@ -482,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
+ src/Lang/Crucible/LLVM/Internal.hs view
@@ -0,0 +1,25 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeApplications #-}++-- | Items in this module should /not/ be considered part of Crucible-LLVM's+-- API, they are exported only for the sake of the test suite.+module Lang.Crucible.LLVM.Internal+  ( assertionsEnabled+  ) where++import qualified Control.Exception as X+import           Data.Functor ((<&>))++-- | Check if assertions are enabled.+--+-- Note [Asserts]: When optimizations are enabled, GHC compiles 'X.assert' to+-- a no-op. However, Cabal enables @-O1@ by default. Therefore, if we want our+-- assertions to be checked by our test suite, we must carefully ensure that we+-- pass the correct flags to GHC for the @lib:crucible-llvm@ target. We verify+-- that we have done so by asserting as much in the test suite.+assertionsEnabled :: IO Bool+assertionsEnabled = do+  X.try @X.AssertionFailed (X.assert False (pure ())) <&>+    \case+      Left _ -> True+      Right () -> False
src/Lang/Crucible/LLVM/Intrinsics.hs view
@@ -26,6 +26,7 @@ , register_llvm_overrides , register_llvm_overrides_ , llvmDeclToFunHandleRepr+, declare_overrides  , module Lang.Crucible.LLVM.Intrinsics.Common , module Lang.Crucible.LLVM.Intrinsics.Options
src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs view
@@ -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@@ -307,6 +325,23 @@     , Poly1VecLLVMOverride $ \vecSz intSz ->         SomeLLVMOverride (llvmVectorReduceUmin vecSz intSz)     )++  , ("llvm.smax"+    , Poly1VecLLVMOverride $ \vecSz intSz ->+        SomeLLVMOverride (llvmSmaxVector vecSz intSz)+    )+  , ("llvm.smin"+    , Poly1VecLLVMOverride $ \vecSz intSz ->+        SomeLLVMOverride (llvmSminVector vecSz intSz)+    )+  , ("llvm.umax"+    , Poly1VecLLVMOverride $ \vecSz intSz ->+        SomeLLVMOverride (llvmUmaxVector vecSz intSz)+    )+  , ("llvm.umin"+    , Poly1VecLLVMOverride $ \vecSz intSz ->+        SomeLLVMOverride (llvmUminVector vecSz intSz)+    )   ]  ------------------------------------------------------------------------@@ -467,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 ()) @@ -1159,6 +1224,150 @@   [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 =>   LLVMOverride p sym ext@@ -1469,6 +1678,67 @@         (BVType intSz) llvmVectorReduceUmin = llvmVectorReduce "umin" callVectorReduceUmin +-- | Build an 'LLVMOverride' for a vector map intrinsic.+llvmVectorMap ::+  (1 <= intSz) =>+  -- | The name of the operation to map (@umin@, @smin@, etc.).+  String ->+  -- | The semantics of the override.+  (forall r args ret.+    IsSymInterface sym =>+    RegEntry sym (VectorType (BVType intSz)) ->+    RegEntry sym (VectorType (BVType intSz)) ->+    OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))) ->+  -- | The size of the vector type.+  NatRepr vecSz ->+  -- | The size of the integer type.+  NatRepr intSz ->+  LLVMOverride p sym ext+    (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))+    (VectorType (BVType intSz))+llvmVectorMap opName callMap vecSz intSz =+  let nm = L.Symbol ("llvm." ++ opName +++                     ".v" ++ show (natValue vecSz) +++                     "i" ++ show (natValue intSz)) in+    [llvmOvr| <#vecSz x #intSz> $nm( <#vecSz x #intSz>, <#vecSz x #intSz> ) |]+    (\_memOps args -> Ctx.uncurryAssignment callMap args)++llvmSmaxVector ::+  (1 <= intSz) =>+  NatRepr vecSz ->+  NatRepr intSz ->+  LLVMOverride p sym ext+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))+     (VectorType (BVType intSz))+llvmSmaxVector = llvmVectorMap "smax" callVectorMapSmax++llvmSminVector ::+  (1 <= intSz) =>+  NatRepr vecSz ->+  NatRepr intSz ->+  LLVMOverride p sym ext+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))+     (VectorType (BVType intSz))+llvmSminVector = llvmVectorMap "smin" callVectorMapSmin++llvmUmaxVector ::+  (1 <= intSz) =>+  NatRepr vecSz ->+  NatRepr intSz ->+  LLVMOverride p sym ext+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))+     (VectorType (BVType intSz))+llvmUmaxVector = llvmVectorMap "umax" callVectorMapUmax++llvmUminVector ::+  (1 <= intSz) =>+  NatRepr vecSz ->+  NatRepr intSz ->+  LLVMOverride p sym ext+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))+     (VectorType (BVType intSz))+llvmUminVector = llvmVectorMap "umin" callVectorMapUmin+ ------------------------------------------------------------------------ -- ** Implementations @@ -1933,8 +2203,8 @@ callIsFpclass regOp@(regValue -> op) (regValue -> test) = do   sym <- getSymInterface   let w1 = knownNat @1-  bv1 <- liftIO $ bvZero sym w1-  bv0 <- liftIO $ bvOne sym w1+  bv1 <- liftIO $ bvOne sym w1+  bv0 <- liftIO $ bvZero sym w1    let negative bit = liftIO $ do         isNeg <- iFloatIsNeg @_ @fi sym op@@ -2140,3 +2410,52 @@   sym <- getSymInterface   umax <- liftIO $ maxUnsignedBV sym intSz   callVectorReduce (bvUmin sym) umax vec++-- | The semantics of an LLVM vector map intrinsic.+callVectorMap ::+  -- | The operation to apply when mapping (e.g., @umin@, @smin@, etc.)+  (RegValue sym tp -> RegValue sym tp -> IO (RegValue sym tp)) ->+  -- | The first vector to map over.+  RegEntry sym (VectorType tp) ->+  -- | The second vector to map over.+  RegEntry sym (VectorType tp) ->+  -- | The result of mapping over the vectors.+  OverrideSim p sym ext r args ret (V.Vector (RegValue sym tp))+callVectorMap mapOp (regValue -> vec1) (regValue -> vec2) =+  liftIO $ V.zipWithM mapOp vec1 vec2++callVectorMapSmax ::+  (IsSymInterface sym, 1 <= intSz) =>+  RegEntry sym (VectorType (BVType intSz)) ->+  RegEntry sym (VectorType (BVType intSz)) ->+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))+callVectorMapSmax vec1 vec2 = do+  sym <- getSymInterface+  callVectorMap (bvSmax sym) vec1 vec2++callVectorMapSmin ::+  (IsSymInterface sym, 1 <= intSz) =>+  RegEntry sym (VectorType (BVType intSz)) ->+  RegEntry sym (VectorType (BVType intSz)) ->+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))+callVectorMapSmin vec1 vec2 = do+  sym <- getSymInterface+  callVectorMap (bvSmin sym) vec1 vec2++callVectorMapUmax ::+  (IsSymInterface sym, 1 <= intSz) =>+  RegEntry sym (VectorType (BVType intSz)) ->+  RegEntry sym (VectorType (BVType intSz)) ->+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))+callVectorMapUmax vec1 vec2 = do+  sym <- getSymInterface+  callVectorMap (bvUmax sym) vec1 vec2++callVectorMapUmin ::+  (IsSymInterface sym, 1 <= intSz) =>+  RegEntry sym (VectorType (BVType intSz)) ->+  RegEntry sym (VectorType (BVType intSz)) ->+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))+callVectorMapUmin vec1 vec2 = do+  sym <- getSymInterface+  callVectorMap (bvUmin sym) vec1 vec2
src/Lang/Crucible/LLVM/Intrinsics/Libc.hs view
@@ -65,6 +65,7 @@ import qualified Lang.Crucible.LLVM.MemModel.Generic as G import           Lang.Crucible.LLVM.MemModel.Partial import qualified Lang.Crucible.LLVM.MemModel.Pointer as Ptr+import           Lang.Crucible.LLVM.MemModel.Strings as CStr import           Lang.Crucible.LLVM.Printf import           Lang.Crucible.LLVM.QQ( llvmOvr ) import           Lang.Crucible.LLVM.TypeContext@@ -94,6 +95,10 @@   , SomeLLVMOverride llvmFreeOverride   , SomeLLVMOverride llvmReallocOverride   , SomeLLVMOverride llvmStrlenOverride+  , SomeLLVMOverride llvmStrnlenOverride+  , SomeLLVMOverride llvmStrcpyOverride+  , SomeLLVMOverride llvmStrdupOverride+  , SomeLLVMOverride llvmStrndupOverride   , SomeLLVMOverride llvmPrintfOverride   , SomeLLVMOverride llvmPrintfChkOverride   , SomeLLVMOverride llvmPutsOverride@@ -391,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 @@ -596,7 +633,7 @@   (regValue -> strPtr) =     ovrWithBackend $ \bak -> do       mem <- readGlobal mvar-      str <- liftIO $ loadString bak mem strPtr Nothing+      str <- liftIO $ CStr.loadString bak mem strPtr Nothing       h <- printHandle <$> getContext       liftIO $ hPutStrLn h (UTF8.toString str)       -- return non-negative value on success@@ -613,6 +650,66 @@     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      , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )@@ -629,7 +726,7 @@     let sym = backendGetSym bak     when failUponExit $       do mem <- readGlobal mvar-         txt <- liftIO $ loadString bak mem (regValue ptxt) Nothing+         txt <- liftIO $ CStr.loadString bak mem (regValue ptxt) Nothing          let err = AssertFailureSimError "Call to assert()" (UTF8.toString txt)          liftIO $ addFailedAssertion bak err     liftIO $@@ -667,7 +764,7 @@   (regValue -> valist) =     ovrWithBackend $ \bak -> do       mem <- readGlobal mvar-      formatStr <- liftIO $ loadString bak mem strPtr Nothing+      formatStr <- liftIO $ CStr.loadString bak mem strPtr Nothing       case parseDirectives formatStr of         Left err -> overrideError $ AssertFailureSimError "Format string parsing failed" err         Right ds -> do@@ -731,7 +828,7 @@      case valist V.!? (i-1) of        Just (AnyValue PtrRepr ptr) ->            do mem <- get-              liftIO $ loadString bak mem ptr numchars+              liftIO $ CStr.loadString bak mem ptr numchars        Just (AnyValue tpr _) ->          lift $ addFailedAssertion bak               $ AssertFailureSimError
src/Lang/Crucible/LLVM/MemModel.hs view
@@ -46,6 +46,8 @@   , IndeterminateLoadBehavior(..)   , defaultMemOptions   , laxPointerMemOptions+  , ppLLVMMemIntrinsicType+  , ppLLVMIntrinsicTypes    -- * Pointers   , LLVMPointerType@@ -83,9 +85,15 @@   , doArrayStoreUnbounded   , doArrayConstStore   , doArrayConstStoreUnbounded-  , loadString-  , loadMaybeString-  , strLen+  -- TODO(#1308): When GHC 9.6 support is dropped, deprecate these imports+  -- TOOD(#1406): After they have been deprecated for a while, move the+  -- implementations to `Strings` and remove these exports.+  , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-}+    loadString+  , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-}+    loadMaybeString+  , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-}+    strLen   , uncheckedMemcpy      -- * \"Raw\" operations with LLVMVal@@ -194,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@@ -203,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@@ -270,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   } @@ -353,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 ::@@ -527,9 +563,7 @@     do mem <- getMem mvar        liftIO $ doPtrSubtract bak mem x y -  eval LLVM_Debug{} = pure () - mkMemVar :: Text          -> HandleAllocator          -> IO (GlobalVar Mem)@@ -713,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"@@ -732,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@@ -746,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. --@@ -1558,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"@@ -1770,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
src/Lang/Crucible/LLVM/MemModel/Common.hs view
@@ -467,8 +467,10 @@         let d = lo - so         -- Store is before load.         valueLoad lo ltp lo (SelectSuffixBV d (sw - d) v)-      | otherwise -> assert (lo == so && lw < sw) $+      | otherwise ->+        -- TODO(#1560): This assertion can fail.         -- Load ends before store ends.+        -- assert (lo == so && lw < sw) $         valueLoad lo ltp so (SelectPrefixBV lw (sw - lw) v)     Float -> valueLoad lo ltp so (FloatToBV v)     Double -> valueLoad lo ltp so (DoubleToBV v)@@ -511,8 +513,10 @@   ValueView {- ^ view of stored value -} ->   ValueCtor (ValueLoad Addr) valueLoad lo ltp so v-  | le <= so = ValueCtorVar (OldMemory lo ltp) -- Load ends before store-  | se <= lo = ValueCtorVar (OldMemory lo ltp) -- Store ends before load+  -- The non-zero test ensures that 0-byte loads are always overlapping+  -- with the most recent store so that they're not spuriously rejected.+  | le <= so && nonZeroLoad = ValueCtorVar (OldMemory lo ltp) -- Load ends before store+  | se <= lo && nonZeroLoad = ValueCtorVar (OldMemory lo ltp) -- Store ends before load     -- Load is before store.   | lo < so  = splitTypeValue ltp (so - lo) (\o tp -> valueLoad (lo+o) tp so v)     -- Load ends after store ends.@@ -534,6 +538,7 @@  where stp = fromMaybe (error ("Coerce value given bad view " ++ show v)) (viewType v)        le = typeEnd lo ltp        se = so + storageTypeSize stp+       nonZeroLoad = le - lo > 0  -- | @LinearLoadStoreOffsetDiff stride delta@ represents the fact that --   the difference between the load offset and the store offset is
src/Lang/Crucible/LLVM/MemModel/Generic.hs view
@@ -76,6 +76,7 @@  import           Prelude hiding (pred) +import qualified Control.Exception as X import           Control.Lens import           Control.Monad import           Control.Monad.State.Strict@@ -91,6 +92,7 @@ import           Numeric.Natural import           Prettyprinter import           Lang.Crucible.Panic (panic)+import qualified Data.Vector as V  import           Data.BitVector.Sized (BV) import qualified Data.BitVector.Sized as BV@@ -695,6 +697,21 @@       | otherwise       = liftIO (Partial.partErr sym mop $ Invalidated msg) +-- | Construct a value of a type that has no in-memory representation at all+buildEmptyVal :: StorageType -> Maybe (LLVMVal sym)+buildEmptyVal t =+  case storageTypeF t of+    Struct fields   -> LLVMValStruct <$> traverse emptyStorageField fields+    Array n eltTy+      | n == 0      -> Just (LLVMValArray eltTy V.empty)+      | otherwise   -> LLVMValArray eltTy . V.replicate (fromIntegral n) <$> buildEmptyVal eltTy+    X86_FP80        -> Nothing+    Float           -> Nothing+    Double          -> Nothing+    Bitvector {}    -> Nothing -- Bitvectors can't be empty; they have a non-zero size invariant+  where+    emptyStorageField field = (,) field <$> buildEmptyVal (field ^. fieldVal)+ -- | Read a value from memory. readMem :: forall sym w.   ( 1 <= w, IsSymInterface sym, HasLLVMAnn sym@@ -707,6 +724,12 @@   Alignment ->   Mem sym ->   IO (PartLLVMVal sym)+readMem sym _ _ _ tp _ _+  -- no actual memory read happens when reading a value with+  -- no memory representation. This check comes up in+  -- particular when evaluating llvm_points_to statements+  -- in SAW script.+  | Just v <- buildEmptyVal tp = pure (Partial.totalLLVMVal sym v) readMem sym w gsym l tp alignment m = do   sz         <- bvLit sym w (bytesToBV w (typeEnd 0 tp))   p1         <- isAllocated sym w alignment l (Just sz) m@@ -1584,21 +1607,43 @@     isHeapMutable (AllocInfo HeapAlloc _ Mutable _ _) = pure (truePred sym)     isHeapMutable _ = pure (falsePred sym) +-- | Prepare memory so that it can later be merged via 'mergeMem'.+--+-- This is primarily intended for use in the implementation of+-- 'Lang.Crucible.Simulator.Intrinsics.pushBranchIntrinsic' for LLVM memory.+-- It would be nice to remove this someday, see #890.+--+-- For more information about branching and merging, see the comment on 'Mem'. branchMem :: Mem sym -> Mem sym branchMem = memState %~ \s ->   BranchFrame (memStateAllocCount s) (memStateWriteCount s) emptyChanges s +-- | Remove the top 'BranchFrame', adding changes to the underlying memory.+--+-- This is primarily intended for use in the implementation of+-- 'Lang.Crucible.Simulator.Intrinsics.abortBranchIntrinsic' for LLVM memory. branchAbortMem :: Mem sym -> Mem sym branchAbortMem = memState %~ popf   where popf (BranchFrame _ _ c s) = s & memStateAddChanges c         popf _ = error "branchAbortMem given unexpected memory" +-- | Merge memory that was previously prepared via 'branchMem'.+--+-- This is primarily intended for use in the implementation of+-- 'Lang.Crucible.Simulator.Intrinsics.muxIntrinsic' for LLVM memory.+--+-- For more information about branching and merging, see the comment on 'Mem'. mergeMem :: IsExpr (SymExpr sym) => Pred sym -> Mem sym -> Mem sym -> Mem sym mergeMem c x y =   case (x^.memState, y^.memState) of-    (BranchFrame _ _ a s, BranchFrame _ _ b _) ->-      let s' = s & memStateAddChanges (muxChanges c a b)-      in x & memState .~ s'+    (BranchFrame _ _ a s, BranchFrame _ _ b s') ->+      -- The memories to be merged must have originated from the same memory,+      -- and in particular, should have matching alloc/write counts.+      let allocsEq = memStateAllocCount s == memStateAllocCount s' in+      let writesEq = memStateWriteCount s == memStateWriteCount s' in+      X.assert (allocsEq && writesEq) $+        let s' = s & memStateAddChanges (muxChanges c a b)+        in x & memState .~ s'     _ -> error "mergeMem given unexpected memories"  --------------------------------------------------------------------------------
src/Lang/Crucible/LLVM/MemModel/MemLog.hs view
@@ -344,8 +344,12 @@     -- of the list.   | StackFrame !Int !Int Text (MemChanges sym) (MemState sym)     -- | Represents a push of a branch frame, and changes since that branch.+    --     -- Changes are stored in order, with more recent changes closer to the head     -- of the list.+    --+    -- For more information about branching and merging, see the comment on+    -- 'Mem'.   | BranchFrame !Int !Int (MemChanges sym) (MemState sym)  type MemChanges sym = (MemAllocs sym, MemWrites sym)@@ -672,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 ::
src/Lang/Crucible/LLVM/MemModel/Partial.hs view
@@ -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 =
src/Lang/Crucible/LLVM/MemModel/Pointer.hs view
@@ -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. --
+ src/Lang/Crucible/LLVM/MemModel/Strings.hs view
@@ -0,0 +1,866 @@+-- TODO(#1406): Move the definitions of the deprecated imports into this module,+-- and remove the exports from MemModel.+{-# OPTIONS_GHC -Wno-warnings-deprecations #-}++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++-- | Manipulating C-style null-terminated strings+module Lang.Crucible.LLVM.MemModel.Strings+  ( storeString+  -- * Loading strings+  , Mem.loadString+  , Mem.loadMaybeString+  , loadConcretelyNullTerminatedString+  , 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+  , provablyNullTerminatedString+  -- *** For string length+  , fullyConcreteNullTerminatedStringLength+  , concretelyNullTerminatedStringLength+  , provablyNullTerminatedStringLength+  -- ** 'ByteLoader'+  , ByteLoader(..)+  , llvmByteLoader+  -- ** 'loadBytes'+  , loadBytes+  ) where++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+import           Data.Word (Word8)+import qualified Data.Vector as Vec+import qualified GHC.Stack as GHC+import qualified Lang.Crucible.Backend as LCB+import qualified Lang.Crucible.Backend.Online as LCBO+import qualified Lang.Crucible.Simulator as LCS+import qualified Lang.Crucible.LLVM.DataLayout as CLD+import qualified Lang.Crucible.LLVM.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+-- characters is provided, no more than that number of characters will be read.+-- In either case, 'loadConcretelyNullTerminatedString' will stop reading if it+-- encounters a (concretely) null terminator.+--+-- Note that the loaded string may actually be smaller than the returned list if+-- any of the symbolic bytes are equal to 0.+loadConcretelyNullTerminatedString ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  -- | Maximum number of characters to read+  Maybe Int ->+  IO [WI.SymBV sym 8]+loadConcretelyNullTerminatedString bak mem ptr limit =+  let loader = llvmByteLoader mem in+  case limit of+    Nothing -> loadBytes bak mem id ptr loader concretelyNullTerminatedString+    Just l ->+      let byteChecker = withMaxChars l (\f -> pure (f [])) concretelyNullTerminatedString in+      loadBytes bak mem (id, 0) ptr loader byteChecker++-- | Load a null-terminated string from memory.+--+-- Consults an SMT solver to check if any of the loaded bytes are known+-- to be null (0). If a maximum number of characters is provided, no+-- more than that number of charcters will be read. In either case,+-- '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.+loadProvablyNullTerminatedString ::+  ( LCB.IsSymBackend sym bak+  , sym ~ WEB.ExprBuilder scope st fs+  , bak ~ LCBO.OnlineBackend solver scope st fs+  , WPO.OnlineSolver solver+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  Mem.MemImpl sym ->+  Mem.LLVMPtr sym wptr ->+  -- | Maximum number of characters to read+  Maybe Int ->+  IO [WI.SymBV sym 8]+loadProvablyNullTerminatedString bak mem ptr limit =+  let loader = llvmByteLoader mem in+  case limit of+    Nothing -> loadBytes bak mem id ptr loader provablyNullTerminatedString+    Just l ->+      let byteChecker = withMaxChars l (\f -> pure (f [])) provablyNullTerminatedString in+      loadBytes bak mem (id, 0) ptr loader byteChecker++---------------------------------------------------------------------+-- * String length++-- | Implementation of libc @strnlen@.+strnlen ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  ) =>+  bak ->+  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) ->+  -- | 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+  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++---------------------------------------------------------------------+-- ** 'ByteChecker'++-- | Whether to stop or keep going+--+-- Like Rust's @std::ops::ControlFlow@.+data ControlFlow a b+  = Continue a+  | Break b+  deriving Functor++-- NB: 'first' is used in this module+instance Bifunctor ControlFlow where+  bimap l r =+    \case+      Continue x -> Continue (l x)+      Break x -> Break (r x)++-- | Compute a result from a symbolic byte, and check if the load should+-- continue to the next byte.+--+-- Used to:+--+-- * Check if the byte is concrete ('fullyConcreteNullTerminatedString')+-- * Check if the byte is concretely a null terminator+--   ('concretelyNullTerminatedString')+-- * Check if a byte is known by a solver to be a null terminator ('nullTerminatedString')+-- * Check if we have surpassed a length limit ('withMaxChars')+--+-- Note that it is relatively common for @a@ to be a function @[b] -> [b]@. This+-- is used to build up a snoc-list.+newtype ByteChecker m sym bak a b+  = ByteChecker { runByteChecker :: bak -> a -> Mem.LLVMPtr sym 8 -> m (ControlFlow a b) }++-- Helper, not exported+ptrToBv8 ::+  LCB.IsSymBackend sym bak =>+  bak ->+  Mem.LLVMPtr sym 8 ->+  IO (WI.SymBV sym 8)+ptrToBv8 bak bytePtr = do+  let err = LCS.AssertFailureSimError "Found pointer instead of byte when loading string" ""+  Partial.ptrToBv bak err bytePtr++-- | 'ByteChecker' for 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+-- 'Lang.Crucible.LLVM.MemModel.loadString'. In fact, it would be good to define+-- that function in terms of this one. However, this is blocked on TODO(#1406).+fullyConcreteNullTerminatedString ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  ByteChecker m sym bak ([Word8] -> [Word8]) [Word8]+fullyConcreteNullTerminatedString =+  ByteChecker $ \bak acc bytePtr -> do+    byte <- liftIO (ptrToBv8 bak bytePtr)+    case BV.asUnsigned <$> WI.asBV byte of+      Just 0 -> pure (Break (acc []))+      Just c -> do+        let c' = toEnum @Word8 (fromInteger c)+        pure (Continue (\l -> acc (c' : l)))+      Nothing -> do+        let msg = "Symbolic value encountered when loading a string"+        liftIO (LCB.addFailedAssertion bak (LCS.Unsupported GHC.callStack msg))++-- | 'ByteChecker' for loading symbolic strings with a concrete null terminator.+--+-- Used in 'loadConcretelyNullTerminatedString'.+concretelyNullTerminatedString ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  ByteChecker m sym bak ([WI.SymBV sym 8] -> [WI.SymBV sym 8]) [WI.SymBV sym 8]+concretelyNullTerminatedString =+  ByteChecker $ \bak acc bytePtr -> do+    byte <- liftIO (ptrToBv8 bak bytePtr)+    if isConcreteNullTerminator byte+    then pure (Break (acc []))+    else  pure (Continue (\l -> acc (byte : l)))+  where+    isConcreteNullTerminator symByte =+      case BV.asUnsigned <$> WI.asBV symByte of+        Just 0 -> True+        _ -> False++-- | 'ByteChecker' for loading symbolic strings with a provably-null terminator.+--+-- Used in 'loadSymbolicString'.+provablyNullTerminatedString ::+  MonadIO m =>+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  sym ~ WEB.ExprBuilder scope st fs =>+  bak ~ LCBO.OnlineBackend solver scope st fs =>+  WPO.OnlineSolver solver =>+  ByteChecker m sym bak ([WI.SymBV sym 8] -> [WI.SymBV sym 8]) [WI.SymBV sym 8]+provablyNullTerminatedString =+  ByteChecker $ \bak acc bytePtr -> liftIO $ do+    byte <- ptrToBv8 bak bytePtr+    let sym = LCB.backendGetSym bak+    isNullTerm <- isProvablyNullTerminator bak sym byte+    if isNullTerm+    then pure (Break (acc []))+    else  pure (Continue (\l -> acc (byte : l)))++-- Helper, not exported+isProvablyNullTerminator ::+  GHC.HasCallStack =>+  LCB.IsSymBackend sym bak =>+  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'++-- | Load a byte from memory.+--+-- The only 'ByteLoader' defined here is 'llvmByteLoader', but Macaw users will+-- most often want one based on @doReadMemModel@.+newtype ByteLoader m sym bak wptr+  = ByteLoader { runByteLoader :: bak -> Mem.LLVMPtr sym wptr -> m (Mem.LLVMPtr sym 8) }++-- | A 'ByteLoader' for LLVM memory based on 'Mem.doLoad'.+llvmByteLoader ::+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  , MonadIO m+  ) =>+  Mem.MemImpl sym ->+  ByteLoader m sym bak wptr+llvmByteLoader mem =+  ByteLoader $ \bak ptr -> do+    let i1 = Mem.bitvectorType 1+    let p8 = Mem.LLVMPointerRepr (DPN.knownNat @8)+    liftIO (Mem.doLoad bak mem ptr i1 p8 CLD.noAlignment)++---------------------------------------------------------------------+-- * 'loadBytes'++-- | Load a sequence of bytes, one at a time.+--+-- Used to implement 'loadConcretelyNullTerminatedString' and+-- 'loadSymbolicString'. Highly customizable via 'ByteLoader' and 'ByteChecker'.+loadBytes ::+  forall m a b sym bak wptr.+  ( LCB.IsSymBackend sym bak+  , Mem.HasPtrWidth wptr+  , Mem.HasLLVMAnn sym+  , ?memOpts :: Mem.MemOptions+  , GHC.HasCallStack+  , MonadIO m+  ) =>+  bak ->+  Mem.MemImpl sym ->+  -- | Initial accumulator+  a ->+  -- | Pointer to load from+  Mem.LLVMPtr sym wptr ->+  -- | How to load a byte from memory+  ByteLoader m sym bak wptr ->+  -- | How to check if we should continue loading the next byte+  ByteChecker m sym bak a b ->+  m b+loadBytes bak mem = go+ where+  sym = LCB.backendGetSym bak+  go ::+    a ->+    Mem.LLVMPtr sym wptr ->+    ByteLoader m sym bak wptr ->+    ByteChecker m sym bak a b ->+    m b+  go acc ptr loader checker = do+    byte <- runByteLoader loader bak ptr+    runByteChecker checker bak acc byte >>=+      \case+        Break result -> pure result+        Continue acc' -> do+          -- It is important that safety assertions for later loads can use+          -- the assumption that earlier bytes were nonzero, see #1463 or+          -- `crucible-llvm-cli/test-data/T1463-read-bytes.cbl` for details.+          prevByteWasNonNull <-+            liftIO (WI.notPred sym =<< Mem.ptrIsNull sym (WI.knownNat @8) byte)+          loc <- liftIO (WI.getCurrentProgramLoc sym)+          let assump = LCB.BranchCondition loc Nothing prevByteWasNonNull+          liftIO (LCB.addAssumption bak assump)++          ptr' <- liftIO (Mem.doPtrAddOffset bak mem ptr =<< WI.bvOne sym Mem.PtrWidth)+          go acc' ptr' loader checker
src/Lang/Crucible/LLVM/MemModel/Value.hs view
@@ -107,8 +107,11 @@   -- | 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 :: IsExprBuilder sym => LLVMVal sym -> StorageType++llvmValStorableType :: IsExpr (SymExpr sym) => LLVMVal sym -> StorageType llvmValStorableType v =   case v of     LLVMValInt _ bv -> bitvectorType (bitsToBytes (natValue (bvWidth bv)))@@ -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)
src/Lang/Crucible/LLVM/MemType.hs view
@@ -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
src/Lang/Crucible/LLVM/SymIO.hs view
@@ -102,6 +102,7 @@  import           Lang.Crucible.LLVM.Bytes (toBytes) import           Lang.Crucible.LLVM.MemModel+import qualified Lang.Crucible.LLVM.MemModel.Strings as CStr import           Lang.Crucible.LLVM.Extension ( ArchWidth ) import           Lang.Crucible.LLVM.DataLayout ( noAlignment ) import           Lang.Crucible.LLVM.Intrinsics@@ -380,7 +381,7 @@ loadFileIdent memOps filename_ptr =   ovrWithBackend $ \bak ->    do mem <- readGlobal memOps-      filename_bytes <- liftIO $ loadString bak mem filename_ptr Nothing+      filename_bytes <- liftIO $ CStr.loadString bak mem filename_ptr Nothing       liftIO $ W4.stringLit (backendGetSym bak) (W4.Char8Literal (BS.pack filename_bytes))  returnIOError32
src/Lang/Crucible/LLVM/Translation.hs view
@@ -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
src/Lang/Crucible/LLVM/Translation/BlockInfo.hs view
@@ -25,7 +25,7 @@   ) where  import Data.Foldable (toList)-import Data.List (foldl')+import qualified Data.Foldable as Foldable import Data.Maybe import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map@@ -131,7 +131,7 @@  -- | Compute predecessor sets from the successor sets already computed in @buildBlockInfo@ updatePredSets :: LLVMBlockInfoMap s -> LLVMBlockInfoMap s-updatePredSets bim0 = foldl' upd bim0 predEdges+updatePredSets bim0 = Foldable.foldl' upd bim0 predEdges   where    upd bim (to,from) = Map.adjust (\bi -> bi{ block_pred_set = Set.insert from (block_pred_set bi) }) to bim @@ -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)
src/Lang/Crucible/LLVM/Translation/Constant.hs view
@@ -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'
src/Lang/Crucible/LLVM/Translation/Expr.hs view
@@ -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
src/Lang/Crucible/LLVM/Translation/Instruction.hs view
@@ -51,8 +51,6 @@ 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@@ -81,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@@ -159,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))@@ -171,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) ->@@ -237,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)@@ -293,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 @@ -357,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@@ -390,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@@ -533,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@@ -575,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' ->@@ -599,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@@ -638,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@@ -699,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@@ -1269,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'@@ -1296,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@@ -1512,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 -} ->@@ -1521,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@@ -1589,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))@@ -1669,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@@ -1690,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 @@ -1732,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 @@ -1801,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)))@@ -2004,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 -} ->@@ -2012,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"@@ -2078,33 +2106,6 @@       | otherwise = callOrdinaryFunction (Just instr) tailCall_ fnTy fn args assign_f --- | Match the arguments used by @dbg.addr@, @dbg.declare@, and @dbg.value@.-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 =-    case args of-      [valArg, lvArg, diArg] ->-        case valArg of-          L.Typed _ (L.ValMd (L.ValMdValue val)) ->-            case lvArg of-              L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoLocalVariable lv))) ->-                case diArg of-                  L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoExpression di))) ->-                    let unusableIdents = Set.difference (useTypedVal val) defSet-                    in if Set.null unusableIdents then-                         do v <- transTypedValue val-                            pure (Right (v, lv, di))-                       else-                         do let msg = unwords (["dbg intrinsic def/use violation for:"] ++-                                       map (show . LPP.ppIdent) (Set.toList unusableIdents))-                            pure (Left msg)-                  _ -> pure (Left ("dbg: argument 3 expected DIExpression, got: " ++ show diArg))-              _ -> pure (Left ("dbg: argument 2 expected local variable metadata, got: " ++ show lvArg))-          _ -> pure (Left ("dbg: argument 1 expected value metadata, got: " ++ show valArg))-      _ -> pure (Left ("dbg: expected 3 arguments, got: " ++ show (length args)))- typedValueAsCrucibleValue ::   L.Typed L.Value ->   LLVMGenerator s arch ret (Some (Value s))@@ -2213,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 ->
test/TestFunctions.hs view
@@ -60,7 +60,8 @@                           (L.PtrTo                             (L.Alias (L.Ident "class.std::cls"))) Nothing (Just 8))                         []-                      , L.Effect L.RetVoid []+                        []+                      , L.Effect L.RetVoid [] []                       ]                   }                 ]
test/TestMemory.hs view
@@ -592,8 +592,8 @@                checkField bak' expectedBV actualPtrRV = do                  actualSymBV <- projectLLVM_bv bak' $ CS.unRV actualPtrRV                  Just expectedBV @=? What4.asBV actualSymBV-           checkField bak struct_bv1 (struct_val'^._1)-           checkField bak struct_bv2 (struct_val'^._2)+           checkField bak struct_bv1 (struct_val' ^. _1)+           checkField bak struct_bv2 (struct_val' ^. _2)       testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = False })      testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = True
test/Tests.hs view
@@ -9,12 +9,13 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} -module Main where+module Main (main) where  -- Crucible 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@@ -46,7 +49,11 @@ import qualified System.IO as IO import qualified System.Process as Proc ++import qualified What4.Internal as WInt+ -- Modules being tested+import           Lang.Crucible.LLVM.Internal (assertionsEnabled) import           Lang.Crucible.LLVM.MemModel ( mkMemVar ) import           Lang.Crucible.LLVM.MemType import           Lang.Crucible.LLVM.Translation@@ -157,7 +164,15 @@         defaultMainWithIngredients llvmTestIngredients $          testGroup "Tests"-         [ functionTests+         [ -- See Note [Asserts] in crucible-llvm+           testCase "assertions enabled" $ do+             assertsEnabled <- assertionsEnabled+             assertBool "assertions should be enabled" assertsEnabled+         , -- See Note [Asserts] in what4+           testCase "What4 assertions enabled" $ do+             assertsEnabled <- WInt.assertionsEnabled+             assertBool "What4 assertions should be enabled" assertsEnabled+         , functionTests          , globalTests          , memoryTests          , translationTests@@ -252,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