diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,21 @@ +# 0.8.0 -- 2025-11-09 + +* `Lang.Crucible.LLVM.MemModel.{loadString,loadMaybeString,strLen}` + should now be imported from `Lang.Crucible.LLVM.MemModel.Strings`. +* Two new functions for loading C-style null-terminated strings from + LLVM memory were added to `Lang.Crucible.LLVM.MemModel.Strings`: + `loadConcretelyNullTerminatedString` and `loadSymbolicString`. +* Add a new "low-level" API for loading strings to + `Lang.Crucible.LLVM.MemModel.Strings`: `ByteLoader`, `ByteChecker`, and + `loadBytes`. +* Support simulating LLVM bitcode files whose data layout strings specify + function pointer alignment. +* Fix a bug that would cause the simuator to compute incorrect results for the + `llvm.is.fpclass` intrinsic. (Among other things, this is used to power the + `isnan` function in Clang 17 or later.) +* Support vectorized versions of the `llvm.u{min,max}` and `llvm.s{min,max}` + intrinsics. + # 0.7.1 -- 2025-03-21 * Fix a bug in which the memory model would panic when attempting to unpack diff --git a/crucible-llvm.cabal b/crucible-llvm.cabal --- a/crucible-llvm.cabal +++ b/crucible-llvm.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: crucible-llvm -Version: 0.7.1 +Version: 0.8.0.0 Author: Galois Inc. Copyright: (c) Galois, Inc 2014-2022 Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com @@ -29,18 +29,108 @@ ghc-prof-options: -O2 -fprof-auto-exported default-language: Haskell2010 +common warns + -- Specifying -Wall and -Werror can cause the project to fail to build on + -- newer versions of GHC simply due to new warnings being added to -Wall. To + -- prevent this from happening we manually list which warnings should be + -- considered errors. We also list some warnings that are not in -Wall, though + -- try to avoid "opinionated" warnings (though this judgement is clearly + -- subjective). + -- + -- Warnings are grouped by the GHC version that introduced them, and then + -- alphabetically. + -- + -- A list of warnings and the GHC version in which they were introduced is + -- available here: + -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html + -- Since GHC 9.6 or earlier: + ghc-options: + -Wall + -Werror=ambiguous-fields + -Werror=compat-unqualified-imports + -Werror=deferred-type-errors + -Werror=deprecated-flags + -Werror=deprecations + -Werror=deriving-defaults + -Werror=deriving-typeable + -Werror=dodgy-foreign-imports + -Werror=duplicate-exports + -Werror=empty-enumerations + -Werror=gadt-mono-local-binds + -Werror=identities + -Werror=inaccessible-code + -Werror=incomplete-patterns + -Werror=incomplete-record-updates + -Werror=incomplete-uni-patterns + -Werror=inline-rule-shadowing + -Werror=misplaced-pragmas + -Werror=missed-extra-shared-lib + -Werror=missing-exported-signatures + -Werror=missing-fields + -Werror=missing-home-modules + -Werror=missing-methods + -Werror=missing-pattern-synonym-signatures + -Werror=missing-signatures + -Werror=name-shadowing + -Werror=noncanonical-monad-instances + -Werror=noncanonical-monoid-instances + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=orphans + -Werror=overflowed-literals + -Werror=overlapping-patterns + -Werror=partial-fields + -Werror=partial-type-signatures + -Werror=redundant-bang-patterns + -Werror=redundant-record-wildcards + -Werror=redundant-strictness-flags + -Werror=simplifiable-class-constraints + -Werror=star-binder + -Werror=star-is-type + -Werror=tabs + -Werror=type-defaults + -Werror=typed-holes + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + -Werror=unicode-bidirectional-format-characters + -Werror=unrecognised-pragmas + -Werror=unrecognised-warning-flags + -Werror=unsupported-calling-conventions + -Werror=unsupported-llvm-version + -Werror=unused-do-bind + -Werror=unused-imports + -Werror=unused-record-wildcards + -Werror=warnings-deprecations + -Werror=wrong-do-bind + + if impl(ghc < 9.8) + ghc-options: + -Werror=forall-identifier + + if impl(ghc >= 9.8) + ghc-options: + -Werror=incomplete-export-warnings + -Werror=inconsistent-flags + + if impl(ghc >= 9.10) + ghc-options: + -Werror=badly-staged-types + -Werror=data-kinds-tc + -Werror=deprecated-type-abstractions + -Werror=incomplete-record-selectors + library import: bldflags build-depends: - base >= 4.13 && < 4.20, + base >= 4.13 && < 4.21, attoparsec, bv-sized >= 1.0.0, bytestring, containers >= 0.5.8.0, crucible >= 0.5, crucible-symio, - what4 >= 0.4.1, + what4 >= 0.5, extra, lens, itanium-abi >= 0.1.1.1 && < 0.2, @@ -73,6 +163,7 @@ Lang.Crucible.LLVM.Extension Lang.Crucible.LLVM.Functions Lang.Crucible.LLVM.Globals + Lang.Crucible.LLVM.Internal Lang.Crucible.LLVM.Intrinsics Lang.Crucible.LLVM.Intrinsics.Cast Lang.Crucible.LLVM.Intrinsics.Libc @@ -85,6 +176,7 @@ Lang.Crucible.LLVM.MemModel.MemLog Lang.Crucible.LLVM.MemModel.Partial Lang.Crucible.LLVM.MemModel.Pointer + Lang.Crucible.LLVM.MemModel.Strings Lang.Crucible.LLVM.MemType Lang.Crucible.LLVM.PrettyPrint Lang.Crucible.LLVM.Printf @@ -124,6 +216,7 @@ test-suite crucible-llvm-tests import: bldflags + import: warns type: exitcode-stdio-1.0 main-is: Tests.hs hs-source-dirs: test diff --git a/src/Lang/Crucible/LLVM/DataLayout.hs b/src/Lang/Crucible/LLVM/DataLayout.hs --- a/src/Lang/Crucible/LLVM/DataLayout.hs +++ b/src/Lang/Crucible/LLVM/DataLayout.hs @@ -164,6 +164,7 @@ data DataLayout = DL { _intLayout :: EndianForm , _stackAlignment :: !Alignment + , _functionPtrAlignment :: !Alignment , _ptrSize :: !Bytes , _ptrAlign :: !Alignment , _integerInfo :: !AlignInfo @@ -184,6 +185,10 @@ stackAlignment :: Lens' DataLayout Alignment stackAlignment = lens _stackAlignment (\s v -> s { _stackAlignment = v}) +functionPtrAlignment :: Lens' DataLayout Alignment +functionPtrAlignment = + lens _functionPtrAlignment (\s v -> s { _functionPtrAlignment = v}) + -- | Size of pointers in bytes. ptrSize :: Lens' DataLayout Bytes ptrSize = lens _ptrSize (\s v -> s { _ptrSize = v}) @@ -238,6 +243,7 @@ defaultDataLayout = execState defaults dl where dl = DL { _intLayout = BigEndian , _stackAlignment = noAlignment + , _functionPtrAlignment = noAlignment , _ptrSize = 8 -- 64 bit pointers = 8 bytes , _ptrAlign = Alignment 3 -- 64 bit alignment: 2^3=8 byte boundaries , _integerInfo = emptyAlignInfo @@ -269,6 +275,7 @@ maxAlignment :: DataLayout -> Alignment maxAlignment dl = maximum [ dl^.stackAlignment + , dl^.functionPtrAlignment , dl^.ptrAlign , maxAlignmentInTree (dl^.integerInfo) , maxAlignmentInTree (dl^.vectorInfo) @@ -322,6 +329,13 @@ L.StackObjSize sz a _ -> setAtBits stackInfo ls sz a L.NativeIntSize _ -> return () L.StackAlign a -> setBits stackAlignment ls a + -- TODO: For now, we ignore the FunctionPointerAlignType field. This tells + -- us whether the function pointer alignment is related to the alignment + -- of functions, but llvm-pretty currently does not track the alignment of + -- individual functions, so we have no use for this info just yet. When + -- https://github.com/GaloisInc/llvm-pretty/issues/164 is implemented, we + -- should revisit this. + L.FunctionPointerAlign _ a -> setBits functionPtrAlignment ls a L.Mangling _ -> return () -- | Create parsed data layout from layout spec AST. diff --git a/src/Lang/Crucible/LLVM/Errors/MemoryError.hs b/src/Lang/Crucible/LLVM/Errors/MemoryError.hs --- a/src/Lang/Crucible/LLVM/Errors/MemoryError.hs +++ b/src/Lang/Crucible/LLVM/Errors/MemoryError.hs @@ -6,6 +6,7 @@ -- Maintainer : Langston Barrett -- Stability : provisional -- +-- See @crucible-llvm-cli/test-data/ub@ for tests demonstrating some of these. -------------------------------------------------------------------------- {-# LANGUAGE DataKinds #-} diff --git a/src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs b/src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs --- a/src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs +++ b/src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs @@ -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 #-} diff --git a/src/Lang/Crucible/LLVM/Globals.hs b/src/Lang/Crucible/LLVM/Globals.hs --- a/src/Lang/Crucible/LLVM/Globals.hs +++ b/src/Lang/Crucible/LLVM/Globals.hs @@ -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) = diff --git a/src/Lang/Crucible/LLVM/Internal.hs b/src/Lang/Crucible/LLVM/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/LLVM/Internal.hs @@ -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 diff --git a/src/Lang/Crucible/LLVM/Intrinsics.hs b/src/Lang/Crucible/LLVM/Intrinsics.hs --- a/src/Lang/Crucible/LLVM/Intrinsics.hs +++ b/src/Lang/Crucible/LLVM/Intrinsics.hs @@ -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 diff --git a/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs b/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs --- a/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs +++ b/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs @@ -307,6 +307,23 @@ , Poly1VecLLVMOverride $ \vecSz intSz -> SomeLLVMOverride (llvmVectorReduceUmin vecSz intSz) ) + + , ("llvm.smax" + , Poly1VecLLVMOverride $ \vecSz intSz -> + SomeLLVMOverride (llvmSmaxVector vecSz intSz) + ) + , ("llvm.smin" + , Poly1VecLLVMOverride $ \vecSz intSz -> + SomeLLVMOverride (llvmSminVector vecSz intSz) + ) + , ("llvm.umax" + , Poly1VecLLVMOverride $ \vecSz intSz -> + SomeLLVMOverride (llvmUmaxVector vecSz intSz) + ) + , ("llvm.umin" + , Poly1VecLLVMOverride $ \vecSz intSz -> + SomeLLVMOverride (llvmUminVector vecSz intSz) + ) ] ------------------------------------------------------------------------ @@ -1469,6 +1486,67 @@ (BVType intSz) llvmVectorReduceUmin = llvmVectorReduce "umin" callVectorReduceUmin +-- | Build an 'LLVMOverride' for a vector map intrinsic. +llvmVectorMap :: + (1 <= intSz) => + -- | The name of the operation to map (@umin@, @smin@, etc.). + String -> + -- | The semantics of the override. + (forall r args ret. + IsSymInterface sym => + RegEntry sym (VectorType (BVType intSz)) -> + RegEntry sym (VectorType (BVType intSz)) -> + OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))) -> + -- | The size of the vector type. + NatRepr vecSz -> + -- | The size of the integer type. + NatRepr intSz -> + LLVMOverride p sym ext + (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz)) + (VectorType (BVType intSz)) +llvmVectorMap opName callMap vecSz intSz = + let nm = L.Symbol ("llvm." ++ opName ++ + ".v" ++ show (natValue vecSz) ++ + "i" ++ show (natValue intSz)) in + [llvmOvr| <#vecSz x #intSz> $nm( <#vecSz x #intSz>, <#vecSz x #intSz> ) |] + (\_memOps args -> Ctx.uncurryAssignment callMap args) + +llvmSmaxVector :: + (1 <= intSz) => + NatRepr vecSz -> + NatRepr intSz -> + LLVMOverride p sym ext + (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz)) + (VectorType (BVType intSz)) +llvmSmaxVector = llvmVectorMap "smax" callVectorMapSmax + +llvmSminVector :: + (1 <= intSz) => + NatRepr vecSz -> + NatRepr intSz -> + LLVMOverride p sym ext + (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz)) + (VectorType (BVType intSz)) +llvmSminVector = llvmVectorMap "smin" callVectorMapSmin + +llvmUmaxVector :: + (1 <= intSz) => + NatRepr vecSz -> + NatRepr intSz -> + LLVMOverride p sym ext + (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz)) + (VectorType (BVType intSz)) +llvmUmaxVector = llvmVectorMap "umax" callVectorMapUmax + +llvmUminVector :: + (1 <= intSz) => + NatRepr vecSz -> + NatRepr intSz -> + LLVMOverride p sym ext + (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz)) + (VectorType (BVType intSz)) +llvmUminVector = llvmVectorMap "umin" callVectorMapUmin + ------------------------------------------------------------------------ -- ** Implementations @@ -1933,8 +2011,8 @@ callIsFpclass regOp@(regValue -> op) (regValue -> test) = do sym <- getSymInterface let w1 = knownNat @1 - bv1 <- liftIO $ bvZero sym w1 - bv0 <- liftIO $ bvOne sym w1 + bv1 <- liftIO $ bvOne sym w1 + bv0 <- liftIO $ bvZero sym w1 let negative bit = liftIO $ do isNeg <- iFloatIsNeg @_ @fi sym op @@ -2140,3 +2218,52 @@ sym <- getSymInterface umax <- liftIO $ maxUnsignedBV sym intSz callVectorReduce (bvUmin sym) umax vec + +-- | The semantics of an LLVM vector map intrinsic. +callVectorMap :: + -- | The operation to apply when mapping (e.g., @umin@, @smin@, etc.) + (RegValue sym tp -> RegValue sym tp -> IO (RegValue sym tp)) -> + -- | The first vector to map over. + RegEntry sym (VectorType tp) -> + -- | The second vector to map over. + RegEntry sym (VectorType tp) -> + -- | The result of mapping over the vectors. + OverrideSim p sym ext r args ret (V.Vector (RegValue sym tp)) +callVectorMap mapOp (regValue -> vec1) (regValue -> vec2) = + liftIO $ V.zipWithM mapOp vec1 vec2 + +callVectorMapSmax :: + (IsSymInterface sym, 1 <= intSz) => + RegEntry sym (VectorType (BVType intSz)) -> + RegEntry sym (VectorType (BVType intSz)) -> + OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz)) +callVectorMapSmax vec1 vec2 = do + sym <- getSymInterface + callVectorMap (bvSmax sym) vec1 vec2 + +callVectorMapSmin :: + (IsSymInterface sym, 1 <= intSz) => + RegEntry sym (VectorType (BVType intSz)) -> + RegEntry sym (VectorType (BVType intSz)) -> + OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz)) +callVectorMapSmin vec1 vec2 = do + sym <- getSymInterface + callVectorMap (bvSmin sym) vec1 vec2 + +callVectorMapUmax :: + (IsSymInterface sym, 1 <= intSz) => + RegEntry sym (VectorType (BVType intSz)) -> + RegEntry sym (VectorType (BVType intSz)) -> + OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz)) +callVectorMapUmax vec1 vec2 = do + sym <- getSymInterface + callVectorMap (bvUmax sym) vec1 vec2 + +callVectorMapUmin :: + (IsSymInterface sym, 1 <= intSz) => + RegEntry sym (VectorType (BVType intSz)) -> + RegEntry sym (VectorType (BVType intSz)) -> + OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz)) +callVectorMapUmin vec1 vec2 = do + sym <- getSymInterface + callVectorMap (bvUmin sym) vec1 vec2 diff --git a/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs b/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs --- a/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +++ b/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs @@ -65,6 +65,7 @@ import qualified Lang.Crucible.LLVM.MemModel.Generic as G import Lang.Crucible.LLVM.MemModel.Partial import qualified Lang.Crucible.LLVM.MemModel.Pointer as Ptr +import Lang.Crucible.LLVM.MemModel.Strings as CStr import Lang.Crucible.LLVM.Printf import Lang.Crucible.LLVM.QQ( llvmOvr ) import Lang.Crucible.LLVM.TypeContext @@ -596,7 +597,7 @@ (regValue -> strPtr) = ovrWithBackend $ \bak -> do mem <- readGlobal mvar - str <- liftIO $ loadString bak mem strPtr Nothing + str <- liftIO $ CStr.loadString bak mem strPtr Nothing h <- printHandle <$> getContext liftIO $ hPutStrLn h (UTF8.toString str) -- return non-negative value on success @@ -629,7 +630,7 @@ let sym = backendGetSym bak when failUponExit $ do mem <- readGlobal mvar - txt <- liftIO $ loadString bak mem (regValue ptxt) Nothing + txt <- liftIO $ CStr.loadString bak mem (regValue ptxt) Nothing let err = AssertFailureSimError "Call to assert()" (UTF8.toString txt) liftIO $ addFailedAssertion bak err liftIO $ @@ -667,7 +668,7 @@ (regValue -> valist) = ovrWithBackend $ \bak -> do mem <- readGlobal mvar - formatStr <- liftIO $ loadString bak mem strPtr Nothing + formatStr <- liftIO $ CStr.loadString bak mem strPtr Nothing case parseDirectives formatStr of Left err -> overrideError $ AssertFailureSimError "Format string parsing failed" err Right ds -> do @@ -731,7 +732,7 @@ case valist V.!? (i-1) of Just (AnyValue PtrRepr ptr) -> do mem <- get - liftIO $ loadString bak mem ptr numchars + liftIO $ CStr.loadString bak mem ptr numchars Just (AnyValue tpr _) -> lift $ addFailedAssertion bak $ AssertFailureSimError diff --git a/src/Lang/Crucible/LLVM/MemModel.hs b/src/Lang/Crucible/LLVM/MemModel.hs --- a/src/Lang/Crucible/LLVM/MemModel.hs +++ b/src/Lang/Crucible/LLVM/MemModel.hs @@ -83,9 +83,15 @@ , doArrayStoreUnbounded , doArrayConstStore , doArrayConstStoreUnbounded - , loadString - , loadMaybeString - , strLen + -- TODO(#1308): When GHC 9.6 support is dropped, deprecate these imports + -- TOOD(#1406): After they have been deprecated for a while, move the + -- implementations to `Strings` and remove these exports. + , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-} + loadString + , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-} + loadMaybeString + , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-} + strLen , uncheckedMemcpy -- * \"Raw\" operations with LLVMVal diff --git a/src/Lang/Crucible/LLVM/MemModel/Common.hs b/src/Lang/Crucible/LLVM/MemModel/Common.hs --- a/src/Lang/Crucible/LLVM/MemModel/Common.hs +++ b/src/Lang/Crucible/LLVM/MemModel/Common.hs @@ -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 diff --git a/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/src/Lang/Crucible/LLVM/MemModel/Generic.hs --- a/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -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" -------------------------------------------------------------------------------- diff --git a/src/Lang/Crucible/LLVM/MemModel/MemLog.hs b/src/Lang/Crucible/LLVM/MemModel/MemLog.hs --- a/src/Lang/Crucible/LLVM/MemModel/MemLog.hs +++ b/src/Lang/Crucible/LLVM/MemModel/MemLog.hs @@ -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) diff --git a/src/Lang/Crucible/LLVM/MemModel/Strings.hs b/src/Lang/Crucible/LLVM/MemModel/Strings.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/LLVM/MemModel/Strings.hs @@ -0,0 +1,367 @@ +-- TODO(#1406): Move the definitions of the deprecated imports into this module, +-- and remove the exports from MemModel. +{-# OPTIONS_GHC -Wno-warnings-deprecations #-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +-- | Manipulating C-style null-terminated strings +module Lang.Crucible.LLVM.MemModel.Strings + ( Mem.loadString + , Mem.loadMaybeString + , Mem.strLen + , loadConcretelyNullTerminatedString + , loadSymbolicString + , storeString + -- * Low-level string loading primitives + -- ** 'ByteChecker' + , ControlFlow(..) + , ByteChecker(..) + , fullyConcreteNullTerminatedString + , concretelyNullTerminatedString + , nullTerminatedString + , withMaxChars + -- ** 'ByteLoader' + , ByteLoader(..) + , llvmByteLoader + -- ** 'loadBytes' + , loadBytes + ) where + +import Data.Bifunctor (Bifunctor(bimap, first)) +import Control.Monad.IO.Class (MonadIO, liftIO) +import qualified Data.BitVector.Sized as BV +import Data.Functor ((<&>)) +import qualified Data.Parameterized.NatRepr as DPN +import Data.Word (Word8) +import qualified Data.Vector as Vec +import qualified GHC.Stack as GHC +import qualified Lang.Crucible.Backend as LCB +import qualified Lang.Crucible.Backend.Online as LCBO +import qualified Lang.Crucible.Simulator as LCS +import qualified Lang.Crucible.LLVM.DataLayout as CLD +import qualified Lang.Crucible.LLVM.MemModel as LCLM +import qualified Lang.Crucible.LLVM.MemModel as Mem +import qualified Lang.Crucible.LLVM.MemModel.Partial as Partial +import qualified What4.Expr.Builder as WEB +import qualified What4.Interface as WI +import qualified What4.Protocol.Online as WPO +import qualified What4.SatResult as WS + +-- | Load a null-terminated string (with a concrete null terminator) from memory. +-- +-- The string must contain a concrete null terminator. If a maximum number of +-- characters is provided, no more than that number of characters will be read. +-- In either case, 'loadConcretelyNullTerminatedString' will stop reading if it +-- encounters a (concretely) null terminator. +-- +-- Note that the loaded string may actually be smaller than the returned list if +-- any of the symbolic bytes are equal to 0. +loadConcretelyNullTerminatedString :: + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + Mem.LLVMPtr sym wptr -> + -- | Maximum number of characters to read + Maybe Int -> + IO [WI.SymBV sym 8] +loadConcretelyNullTerminatedString bak mem ptr limit = + let loader = llvmByteLoader mem in + case limit of + Nothing -> loadBytes bak mem id ptr loader concretelyNullTerminatedString + Just l -> + let byteChecker = withMaxChars l (\f -> pure (f [])) concretelyNullTerminatedString in + loadBytes bak mem (id, 0) ptr loader byteChecker + +-- | Load a null-terminated string from memory. +-- +-- Consults an SMT solver to check if any of the loaded bytes are known to be +-- null (0). If a maximum number of characters is provided, no more than that +-- number of charcters will be read. In either case, 'loadSymbolicString' will +-- stop reading if it encounters a null terminator. +-- +-- Note that the loaded string may actually be smaller than the returned list if +-- any of the symbolic bytes are equal to 0. +loadSymbolicString :: + ( LCB.IsSymBackend sym bak + , sym ~ WEB.ExprBuilder scope st fs + , bak ~ LCBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + Mem.LLVMPtr sym wptr -> + -- | Maximum number of characters to read + Maybe Int -> + IO [WI.SymBV sym 8] +loadSymbolicString bak mem ptr limit = + let loader = llvmByteLoader mem in + case limit of + Nothing -> loadBytes bak mem id ptr loader nullTerminatedString + Just l -> + let byteChecker = withMaxChars l (\f -> pure (f [])) nullTerminatedString in + loadBytes bak mem (id, 0) ptr loader byteChecker + +-- | Store a string to memory, adding a null terminator at the end. +storeString :: + forall sym bak w. + ( LCB.IsSymBackend sym bak + , WI.IsExpr (WI.SymExpr sym) + , LCLM.HasPtrWidth w + , LCLM.HasLLVMAnn sym + , ?memOpts :: LCLM.MemOptions + ) => + bak -> + LCLM.MemImpl sym -> + -- | Pointer to write string to + LCLM.LLVMPtr sym w -> + -- | The bytes of the string to write (null terminator not included) + Vec.Vector (WI.SymBV sym 8) -> + IO (LCLM.MemImpl sym) +storeString bak mem ptr bytesBvs = do + let sym = LCB.backendGetSym bak + zeroNat <- WI.natLit sym 0 + let bytes = Vec.map (Mem.LLVMValInt zeroNat) bytesBvs + zeroByte <- Mem.LLVMValInt zeroNat <$> WI.bvZero sym (DPN.knownNat @8) + let nullTerminatedBytes = Vec.snoc bytes zeroByte + let val = Mem.LLVMValArray (Mem.bitvectorType 1) nullTerminatedBytes + let storTy = Mem.llvmValStorableType @sym val + Mem.storeRaw bak mem ptr storTy CLD.noAlignment val + +--------------------------------------------------------------------- +-- * Low-level string loading primitives + +--------------------------------------------------------------------- +-- ** 'ByteChecker' + +-- | Whether to stop or keep going +-- +-- Like Rust's @std::ops::ControlFlow@. +data ControlFlow a b + = Continue a + | Break b + deriving Functor + +-- NB: 'first' is used in this module +instance Bifunctor ControlFlow where + bimap l r = + \case + Continue x -> Continue (l x) + Break x -> Break (r x) + +-- | Compute a result from a symbolic byte, and check if the load should +-- continue to the next byte. +-- +-- Used to: +-- +-- * Check if the byte is concrete ('fullyConcreteNullTerminatedString') +-- * Check if the byte is concretely a null terminator +-- ('concretelyNullTerminatedString') +-- * Check if a byte is known by a solver to be a null terminator ('nullTerminatedString') +-- * Check if we have surpassed a length limit ('withMaxChars') +-- +-- Note that it is relatively common for @a@ to be a function @[b] -> [b]@. This +-- is used to build up a snoc-list. +newtype ByteChecker m sym bak a b + = ByteChecker { runByteChecker :: bak -> a -> Mem.LLVMPtr sym 8 -> m (ControlFlow a b) } + +-- Helper, not exported +ptrToBv8 :: + LCB.IsSymBackend sym bak => + bak -> + Mem.LLVMPtr sym 8 -> + IO (WI.SymBV sym 8) +ptrToBv8 bak bytePtr = do + let err = LCS.AssertFailureSimError "Found pointer instead of byte when loading string" "" + Partial.ptrToBv bak err bytePtr + +-- | 'ByteChecker' for loading concrete strings. +-- +-- Currently unused internally, but analogous with +-- 'Lang.Crucible.LLVM.MemModel.loadString'. In fact, it would be good to define +-- that function in terms of this one. However, this is blocked on TODO(#1406). +fullyConcreteNullTerminatedString :: + MonadIO m => + GHC.HasCallStack => + LCB.IsSymBackend sym bak => + ByteChecker m sym bak ([Word8] -> [Word8]) [Word8] +fullyConcreteNullTerminatedString = + ByteChecker $ \bak acc bytePtr -> do + byte <- liftIO (ptrToBv8 bak bytePtr) + case BV.asUnsigned <$> WI.asBV byte of + Just 0 -> pure (Break (acc [])) + Just c -> do + let c' = toEnum @Word8 (fromInteger c) + pure (Continue (\l -> acc (c' : l))) + Nothing -> do + let msg = "Symbolic value encountered when loading a string" + liftIO (LCB.addFailedAssertion bak (LCS.Unsupported GHC.callStack msg)) + +-- | 'ByteChecker' for loading symbolic strings with a concrete null terminator. +-- +-- Used in 'loadConcretelyNullTerminatedString'. +concretelyNullTerminatedString :: + MonadIO m => + GHC.HasCallStack => + LCB.IsSymBackend sym bak => + ByteChecker m sym bak ([WI.SymBV sym 8] -> [WI.SymBV sym 8]) [WI.SymBV sym 8] +concretelyNullTerminatedString = + ByteChecker $ \bak acc bytePtr -> do + byte <- liftIO (ptrToBv8 bak bytePtr) + if isConcreteNullTerminator byte + then pure (Break (acc [])) + else pure (Continue (\l -> acc (byte : l))) + where + isConcreteNullTerminator symByte = + case BV.asUnsigned <$> WI.asBV symByte of + Just 0 -> True + _ -> False + +-- | 'ByteChecker' for loading symbolic strings with a null terminator. +-- +-- Used in 'loadSymbolicString'. +nullTerminatedString :: + MonadIO m => + GHC.HasCallStack => + LCB.IsSymBackend sym bak => + sym ~ WEB.ExprBuilder scope st fs => + bak ~ LCBO.OnlineBackend solver scope st fs => + WPO.OnlineSolver solver => + ByteChecker m sym bak ([WI.SymBV sym 8] -> [WI.SymBV sym 8]) [WI.SymBV sym 8] +nullTerminatedString = + ByteChecker $ \bak acc bytePtr -> do + byte <- liftIO (ptrToBv8 bak bytePtr) + let sym = LCB.backendGetSym bak + isNullTerm <- liftIO (isNullTerminator bak sym byte) + if isNullTerm + then pure (Break (acc [])) + else pure (Continue (\l -> acc (byte : l))) + where + isNullTerminator bak sym symByte = + case BV.asUnsigned <$> WI.asBV symByte of + Just 0 -> pure True + Just _ -> pure False + _ -> + LCBO.withSolverProcess bak (pure False) $ \proc -> do + z <- WI.bvZero sym (WI.knownNat @8) + p <- WI.notPred sym =<< WI.bvEq sym z symByte + WPO.checkSatisfiable proc "nullTerminatedString" p <&> + \case + WS.Unsat () -> True + WS.Sat () -> False + WS.Unknown -> False + +-- | 'ByteChecker' for adding a maximum character length. +withMaxChars :: + GHC.HasCallStack => + LCB.IsSymBackend sym bak => + Functor m => + -- | Maximum number of bytes to load + Int -> + -- | What to do when the maximum is reached + (a -> m b) -> + ByteChecker m sym bak a b -> + ByteChecker m sym bak (a, Int) b +withMaxChars limit done checker = + ByteChecker $ \bak (acc, i) bytePtr -> + if i > limit + then Break <$> done acc + else first (, i + 1) <$> runByteChecker checker bak acc bytePtr + +--------------------------------------------------------------------- +-- ** 'ByteLoader' + +-- | Load a byte from memory. +-- +-- The only 'ByteLoader' defined here is 'llvmByteLoader', but Macaw users will +-- most often want one based on @doReadMemModel@. +newtype ByteLoader m sym bak wptr + = ByteLoader { runByteLoader :: bak -> Mem.LLVMPtr sym wptr -> m (Mem.LLVMPtr sym 8) } + +-- | A 'ByteLoader' for LLVM memory based on 'Mem.doLoad'. +llvmByteLoader :: + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + , MonadIO m + ) => + Mem.MemImpl sym -> + ByteLoader m sym bak wptr +llvmByteLoader mem = + ByteLoader $ \bak ptr -> do + let i1 = Mem.bitvectorType 1 + let p8 = Mem.LLVMPointerRepr (DPN.knownNat @8) + liftIO (Mem.doLoad bak mem ptr i1 p8 CLD.noAlignment) + +--------------------------------------------------------------------- +-- * 'loadBytes' + +-- | Load a sequence of bytes, one at a time. +-- +-- Used to implement 'loadConcretelyNullTerminatedString' and +-- 'loadSymbolicString'. Highly customizable via 'ByteLoader' and 'ByteChecker'. +loadBytes :: + forall m a b sym bak wptr. + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + , MonadIO m + ) => + bak -> + Mem.MemImpl sym -> + -- | Initial accumulator + a -> + -- | Pointer to load from + Mem.LLVMPtr sym wptr -> + -- | How to load a byte from memory + ByteLoader m sym bak wptr -> + -- | How to check if we should continue loading the next byte + ByteChecker m sym bak a b -> + m b +loadBytes bak mem = go + where + sym = LCB.backendGetSym bak + go :: + a -> + Mem.LLVMPtr sym wptr -> + ByteLoader m sym bak wptr -> + ByteChecker m sym bak a b -> + m b + go acc ptr loader checker = do + byte <- runByteLoader loader bak ptr + runByteChecker checker bak acc byte >>= + \case + Break result -> pure result + Continue acc' -> do + -- It is important that safety assertions for later loads can use + -- the assumption that earlier bytes were nonzero, see #1463 or + -- `crucible-llvm-cli/test-data/T1463-read-bytes.cbl` for details. + prevByteWasNonNull <- + liftIO (WI.notPred sym =<< Mem.ptrIsNull sym (WI.knownNat @8) byte) + loc <- liftIO (WI.getCurrentProgramLoc sym) + let assump = LCB.BranchCondition loc Nothing prevByteWasNonNull + liftIO (LCB.addAssumption bak assump) + + ptr' <- liftIO (Mem.doPtrAddOffset bak mem ptr =<< WI.bvOne sym Mem.PtrWidth) + go acc' ptr' loader checker diff --git a/src/Lang/Crucible/LLVM/MemModel/Value.hs b/src/Lang/Crucible/LLVM/MemModel/Value.hs --- a/src/Lang/Crucible/LLVM/MemModel/Value.hs +++ b/src/Lang/Crucible/LLVM/MemModel/Value.hs @@ -108,7 +108,7 @@ LLVMValUndef :: StorageType -> LLVMVal sym -llvmValStorableType :: IsExprBuilder sym => LLVMVal sym -> StorageType +llvmValStorableType :: IsExpr (SymExpr sym) => LLVMVal sym -> StorageType llvmValStorableType v = case v of LLVMValInt _ bv -> bitvectorType (bitsToBytes (natValue (bvWidth bv))) diff --git a/src/Lang/Crucible/LLVM/SymIO.hs b/src/Lang/Crucible/LLVM/SymIO.hs --- a/src/Lang/Crucible/LLVM/SymIO.hs +++ b/src/Lang/Crucible/LLVM/SymIO.hs @@ -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 diff --git a/src/Lang/Crucible/LLVM/Translation/BlockInfo.hs b/src/Lang/Crucible/LLVM/Translation/BlockInfo.hs --- a/src/Lang/Crucible/LLVM/Translation/BlockInfo.hs +++ b/src/Lang/Crucible/LLVM/Translation/BlockInfo.hs @@ -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 diff --git a/src/Lang/Crucible/LLVM/Translation/Instruction.hs b/src/Lang/Crucible/LLVM/Translation/Instruction.hs --- a/src/Lang/Crucible/LLVM/Translation/Instruction.hs +++ b/src/Lang/Crucible/LLVM/Translation/Instruction.hs @@ -41,12 +41,14 @@ import Control.Lens hiding (op, (:>) ) import Control.Monad (MonadPlus(..), forM, unless) import Control.Monad.Except (MonadError(..), runExceptT) -import Control.Monad.State.Strict (MonadState(..)) +import Control.Monad.State.Strict (MonadState(..), gets) import Control.Monad.Trans.Class (MonadTrans(..)) import Control.Monad.Trans.Maybe import Data.Foldable (for_, toList) import Data.Functor (void) import Data.Int +import Data.IntMap.Strict (IntMap) +import qualified Data.IntMap.Strict as IntMap import qualified Data.List as List import Data.List.NonEmpty (NonEmpty((:|))) import qualified Data.Map.Strict as Map @@ -2079,31 +2081,81 @@ | otherwise = callOrdinaryFunction (Just instr) tailCall_ fnTy fn args assign_f -- | Match the arguments used by @dbg.addr@, @dbg.declare@, and @dbg.value@. +-- For more information on how these work, see +-- . + +-- This function assumes that each argument should either be a particular kind +-- of metadata value or a reference that resolves to a particular kind of +-- metadata value (see @resolveArg{1,2,3}@ below). If we encounter other types +-- of LLVM metadata that breaks this assumption, then we will need to update +-- this function's implementation accordingly. dbgArgs :: Set L.Ident {- ^ Set of usable identifiers -} -> [L.Typed L.Value] {- ^ debug call arguments -} -> LLVMGenerator s arch ret (Either String (LLVMExpr s arch, L.DILocalVariable, L.DIExpression)) -dbgArgs defSet args = +dbgArgs defSet args = do + unnamedMd <- gets (llvmUnnamedMd . llvmContext) case args of - [valArg, lvArg, diArg] -> - case valArg of - L.Typed _ (L.ValMd (L.ValMdValue val)) -> - case lvArg of - L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoLocalVariable lv))) -> - case diArg of - L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoExpression di))) -> - let unusableIdents = Set.difference (useTypedVal val) defSet - in if Set.null unusableIdents then - do v <- transTypedValue val - pure (Right (v, lv, di)) - else - do let msg = unwords (["dbg intrinsic def/use violation for:"] ++ - map (show . LPP.ppIdent) (Set.toList unusableIdents)) - pure (Left msg) - _ -> pure (Left ("dbg: argument 3 expected DIExpression, got: " ++ show diArg)) - _ -> pure (Left ("dbg: argument 2 expected local variable metadata, got: " ++ show lvArg)) - _ -> pure (Left ("dbg: argument 1 expected value metadata, got: " ++ show valArg)) + [valArg, lvArg, diArg] -> do + let resolveRes = do -- Either String + val <- resolveArg1 unnamedMd $ L.typedValue valArg + lv <- resolveArg2 unnamedMd $ L.typedValue lvArg + di <- resolveArg3 unnamedMd $ L.typedValue diArg + Right (val, lv, di) + case resolveRes of + Left err -> pure (Left err) + Right (val, lv, di) -> + let unusableIdents = Set.difference (useTypedVal val) defSet + in if Set.null unusableIdents then + do v <- transTypedValue val + pure (Right (v, lv, di)) + else + do let msg = unwords (["dbg intrinsic def/use violation for:"] ++ + map (show . LPP.ppIdent) (Set.toList unusableIdents)) + pure (Left msg) _ -> pure (Left ("dbg: expected 3 arguments, got: " ++ show (length args))) + where + resolveArg1 :: + IntMap L.ValMd -> + L.Value -> + Either String (L.Typed L.Value) + resolveArg1 unnamedMd = go + where + go (L.ValMd (L.ValMdRef ref)) + | Just valMd <- IntMap.lookup ref unnamedMd + = go (L.ValMd valMd) + go (L.ValMd (L.ValMdValue val)) = + Right val + go valArg = + Left ("dbg: argument 1 expected value metadata, got: " ++ show valArg) + + resolveArg2 :: + IntMap L.ValMd -> + L.Value -> + Either String L.DILocalVariable + resolveArg2 unnamedMd = go + where + go (L.ValMd (L.ValMdRef ref)) + | Just valMd <- IntMap.lookup ref unnamedMd + = go (L.ValMd valMd) + go (L.ValMd (L.ValMdDebugInfo (L.DebugInfoLocalVariable lv))) = + Right lv + go lvArg = + Left ("dbg: argument 2 expected local variable metadata, got: " ++ show lvArg) + + resolveArg3 :: + IntMap L.ValMd -> + L.Value -> + Either String L.DIExpression + resolveArg3 unnamedMd = go + where + go (L.ValMd (L.ValMdRef ref)) + | Just valMd <- IntMap.lookup ref unnamedMd + = go (L.ValMd valMd) + go (L.ValMd (L.ValMdDebugInfo (L.DebugInfoExpression di))) = + Right di + go diArg = + Left ("dbg: argument 3 expected DIExpression, got: " ++ show diArg) typedValueAsCrucibleValue :: L.Typed L.Value -> diff --git a/src/Lang/Crucible/LLVM/Translation/Monad.hs b/src/Lang/Crucible/LLVM/Translation/Monad.hs --- a/src/Lang/Crucible/LLVM/Translation/Monad.hs +++ b/src/Lang/Crucible/LLVM/Translation/Monad.hs @@ -53,6 +53,8 @@ import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.State.Strict (MonadState(..)) import Data.IORef (IORef, modifyIORef) +import Data.IntMap.Strict (IntMap) +import qualified Data.IntMap.Strict as IntMap import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Set (Set) @@ -95,6 +97,9 @@ -- | For each function symbol, compute the set of -- aliases to that symbol , llvmFunctionAliases :: Map L.Symbol (Set L.GlobalAlias) + -- | Map the index of each piece of unnamed LLVM metadata to its value. + -- This information is used to resolve the arguments to debug intrinsics. + , llvmUnnamedMd :: IntMap L.ValMd } llvmTypeCtx :: Simple Lens (LLVMContext arch) TypeContext @@ -108,6 +113,8 @@ unless (null errs) $ malformedLLVMModule "Failed to construct LLVM type context" errs let dl = llvmDataLayout typeCtx + let unnamedMd = + IntMap.fromList [(L.umIndex um, L.umValues um) | um <- L.modUnnamedMd m] case mkNatRepr (ptrBitwidth dl) of Some (wptr :: NatRepr wptr) | Just LeqProof <- testLeq (knownNat @16) wptr -> @@ -123,6 +130,7 @@ , _llvmTypeCtx = typeCtx , llvmGlobalAliases = mempty -- these are computed later , llvmFunctionAliases = mempty -- these are computed later + , llvmUnnamedMd = unnamedMd } return (Some ctx) _ -> diff --git a/test/TestMemory.hs b/test/TestMemory.hs --- a/test/TestMemory.hs +++ b/test/TestMemory.hs @@ -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 diff --git a/test/Tests.hs b/test/Tests.hs --- a/test/Tests.hs +++ b/test/Tests.hs @@ -9,7 +9,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} -module Main where +module Main (main) where -- Crucible import Lang.Crucible.FunctionHandle ( newHandleAllocator ) @@ -46,7 +46,11 @@ import qualified System.IO as IO import qualified System.Process as Proc + +import qualified What4.Internal as WInt + -- Modules being tested +import Lang.Crucible.LLVM.Internal (assertionsEnabled) import Lang.Crucible.LLVM.MemModel ( mkMemVar ) import Lang.Crucible.LLVM.MemType import Lang.Crucible.LLVM.Translation @@ -157,7 +161,15 @@ defaultMainWithIngredients llvmTestIngredients $ testGroup "Tests" - [ functionTests + [ -- See Note [Asserts] in crucible-llvm + testCase "assertions enabled" $ do + assertsEnabled <- assertionsEnabled + assertBool "assertions should be enabled" assertsEnabled + , -- See Note [Asserts] in what4 + testCase "What4 assertions enabled" $ do + assertsEnabled <- WInt.assertionsEnabled + assertBool "What4 assertions should be enabled" assertsEnabled + , functionTests , globalTests , memoryTests , translationTests