diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,10 +1,55 @@ +# 0.9 -- 2026-01-29 + +* The `LLVM_Debug` data constructor for `LLVMStmt`, as well as the related + `LLVM_Dbg` data type, have been removed. +* Remove `aggInfo` in favor of `aggregateAlignment`, a lens that retrieves an + `Alignment` instead of a full `AlignInfo`. In practice, `aggInfo` would only + ever contain a single size (`0`) in its `AlignInfo`, and the concept of + "size" doesn't really apply to aggregate alignments in data layout strings, + so this was simplified to just be an `Alignment` instead. +* Support simulating bitcode that uses features from LLVM 19, including + [debug records](https://llvm.org/docs/RemoveDIsDebugInfo.html) and + [`getelementptr` + attributes](https://releases.llvm.org/19.1.0/docs/LangRef.html#id237). +* Support the `nneg` flag in `zext` and `uitofp` instructions. If `nneg` is + set, then converting a negative argument will yield a poisoned result. +* Support the `nuw` and `nsw` flags in `trunc` instructions. If `nuw` or `nsw` + is set, then performing a truncation that would result in unsigned or signed + integer overflow, respectively, will yield a poisoned result. +* Support the `samesign` flag in `icmp` instructions. If `samesign` is set, then + comparing two integers of different signs will yield a poisoned result. +* Support the `llvm.tan`, `llvm.a{sin,cos,tan}`, `llvm.{sin,cos,tan}h`, and + `llvm.atan2` floating-point intrinsics. +* Add extremely limited support for representing `poison` constants. For more + details on the extent to which `crucible-llvm` can reason about `poison`, see + `doc/limitations.md`. + + As part of these changes: + + * `LLVMVal` now features an additional `LLVMValPoison` data constructor. + * `LLVMExpr` now features an additional `PoisonExpr` data constructor. + * `LLVMConst` now features an addition `PoisonConst` data constructor. + * `LLVMExtensionExpr` now features `LLVM_Poison{BV,Float}` data constructors, + which represent primitive `poison` values. +* Remove the `Eq LLVMConst` instance. This instance was inherently unreliable + because it cannot easily compute a simple `True`-or-`False` answer in the + presence of `undef` or `poison` values. +* Replace `Data.Dynamic.Dynamic` with `SomeFnHandle` in + `MemModel.{doInstallHandle,doLookupHandle}`. +* Add pretty-printing functions for use with `Lang.Crucible.Types.ppTypeRepr` + * `Lang.Crucible.LLVM.MemModel.ppLLVMIntrinsicTypes` + * `Lang.Crucible.LLVM.MemModel.ppLLVMMemIntrinsicType` + * `Lang.Crucible.LLVM.MemModel.Pointer.ppLLVMPointerIntrinsicType` +* Overrides for `strnlen`, `strcpy`, `strdup`, and `strndup` supported by new + APIs in `Lang.Crucible.LLVM.MemModel.Strings`. + # 0.8.0 -- 2025-11-09 * `Lang.Crucible.LLVM.MemModel.{loadString,loadMaybeString,strLen}` should now be imported from `Lang.Crucible.LLVM.MemModel.Strings`. * Two new functions for loading C-style null-terminated strings from LLVM memory were added to `Lang.Crucible.LLVM.MemModel.Strings`: - `loadConcretelyNullTerminatedString` and `loadSymbolicString`. + `loadConcretelyNullTerminatedString` and `loadProvablyNullTerminatedString`. * Add a new "low-level" API for loading strings to `Lang.Crucible.LLVM.MemModel.Strings`: `ByteLoader`, `ByteChecker`, and `loadBytes`. @@ -70,7 +115,7 @@ * `Lang.Crucible.LLVM.Globals`: `populateGlobal` * `Lang.Crucible.LLVM.MemModel.Generic`: `writeMem` and `writeConstMem` * `Lang.Crucible.LLVM`: `registerModuleFn` has changed type to - accomodate lazy loading of Crucible IR. + accommodate lazy loading of Crucible IR. * `Lang.Crucible.LLVM.Translation` : The `ModuleTranslation` record is now opaque, the `cfgMap` is no longer exported and `globalInitMap` and `modTransNonce` have become lens-style getters instead of record 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.8.0.0 +Version: 0.9 Author: Galois Inc. Copyright: (c) Galois, Inc 2014-2022 Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com @@ -134,7 +134,7 @@ extra, lens, itanium-abi >= 0.1.1.1 && < 0.2, - llvm-pretty >= 0.12.1 && < 0.14, + llvm-pretty >= 0.12.1 && < 0.15, mtl, parameterized-utils >= 2.1.5 && < 2.2, pretty, 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 @@ -42,7 +42,6 @@ import Control.Monad.State.Strict import Data.Map (Map) import qualified Data.Map as Map -import Data.Maybe (fromMaybe) import Data.Word (Word32) import qualified Text.LLVM as L import Numeric.Natural @@ -131,11 +130,6 @@ floatAlignment dl w = Map.lookup w t where AT t = dl^.floatInfo --- | Get the basic alignment for aggregate types. -aggregateAlignment :: DataLayout -> Alignment -aggregateAlignment dl = - fromMaybe noAlignment (findExact 0 (dl^.aggInfo)) - -- | Return maximum alignment constraint stored in tree. maxAlignmentInTree :: AlignInfo -> Alignment maxAlignmentInTree (AT t) = foldrOf folded max noAlignment t @@ -165,12 +159,12 @@ = DL { _intLayout :: EndianForm , _stackAlignment :: !Alignment , _functionPtrAlignment :: !Alignment + , _aggregateAlignment :: !Alignment , _ptrSize :: !Bytes , _ptrAlign :: !Alignment , _integerInfo :: !AlignInfo , _vectorInfo :: !AlignInfo , _floatInfo :: !AlignInfo - , _aggInfo :: !AlignInfo , _stackInfo :: !AlignInfo , _layoutWarnings :: [L.LayoutSpec] } @@ -189,6 +183,10 @@ functionPtrAlignment = lens _functionPtrAlignment (\s v -> s { _functionPtrAlignment = v}) +aggregateAlignment :: Lens' DataLayout Alignment +aggregateAlignment = + lens _aggregateAlignment (\s v -> s { _aggregateAlignment = v}) + -- | Size of pointers in bytes. ptrSize :: Lens' DataLayout Bytes ptrSize = lens _ptrSize (\s v -> s { _ptrSize = v}) @@ -206,10 +204,6 @@ floatInfo :: Lens' DataLayout AlignInfo floatInfo = lens _floatInfo (\s v -> s { _floatInfo = v}) --- | Information about aggregate size. -aggInfo :: Lens' DataLayout AlignInfo -aggInfo = lens _aggInfo (\s v -> s { _aggInfo = v}) - -- | Layout constraints on a stack object with the given size. stackInfo :: Lens' DataLayout AlignInfo stackInfo = lens _stackInfo (\s v -> s { _stackInfo = v}) @@ -246,10 +240,10 @@ , _functionPtrAlignment = noAlignment , _ptrSize = 8 -- 64 bit pointers = 8 bytes , _ptrAlign = Alignment 3 -- 64 bit alignment: 2^3=8 byte boundaries + , _aggregateAlignment = noAlignment -- Aggregates are 1-byte aligned. , _integerInfo = emptyAlignInfo , _floatInfo = emptyAlignInfo , _vectorInfo = emptyAlignInfo - , _aggInfo = emptyAlignInfo , _stackInfo = emptyAlignInfo , _layoutWarnings = [] } @@ -268,8 +262,6 @@ -- Default vector alignments. setAt vectorInfo 64 (Alignment 3) -- 64-bit vector is 8 byte aligned. setAt vectorInfo 128 (Alignment 4) -- 128-bit vector is 16 byte aligned. - -- Default aggregate alignments. - setAt aggInfo 0 noAlignment -- Aggregates are 1-byte aligned. -- | Maximum alignment for any type (used by malloc). maxAlignment :: DataLayout -> Alignment @@ -277,10 +269,10 @@ maximum [ dl^.stackAlignment , dl^.functionPtrAlignment , dl^.ptrAlign + , dl^.aggregateAlignment , maxAlignmentInTree (dl^.integerInfo) , maxAlignmentInTree (dl^.vectorInfo) , maxAlignmentInTree (dl^.floatInfo) - , maxAlignmentInTree (dl^.aggInfo) , maxAlignmentInTree (dl^.stackInfo) ] @@ -289,14 +281,14 @@ | otherwise = fromIntegral i -- | Insert alignment into spec. -setAtBits :: Lens' DataLayout AlignInfo -> L.LayoutSpec -> Int -> Int -> State DataLayout () -setAtBits f spec sz a = - case fromBits a of +setAtBits :: Lens' DataLayout AlignInfo -> L.LayoutSpec -> L.Storage -> State DataLayout () +setAtBits f spec st = + case fromBits (L.alignABI (L.storageAlignment st)) of Left{} -> layoutWarnings %= (spec:) - Right w -> f . at (fromSize sz) .= Just w + Right w -> f . at (fromSize (L.storageSize st)) .= Just w -- | Insert alignment into spec. -setBits :: Lens' DataLayout Alignment -> L.LayoutSpec -> Int -> State DataLayout () +setBits :: Lens' DataLayout Alignment -> L.LayoutSpec -> L.NumBits -> State DataLayout () setBits f spec a = case fromBits a of Left{} -> layoutWarnings %= (spec:) @@ -309,24 +301,25 @@ case ls of L.BigEndian -> intLayout .= BigEndian L.LittleEndian -> intLayout .= LittleEndian - L.PointerSize n sz a _ + L.PointerSize ps -- Currently, we assume that only default address space (0) is used. -- We use that address space as the sole arbiter of what pointer -- size to use, and we ignore all other PointerSize layout specs. -- See doc/limitations.md for more discussion. - | n == 0 - -> case fromBits a of + | L.ptrAddrSpace ps == 0 + -> case fromBits (L.alignABI (L.storageAlignment st)) of Right a' | r == 0 -> do ptrSize .= fromIntegral w ptrAlign .= a' _ -> layoutWarnings %= (ls:) | otherwise -> return () - where (w,r) = sz `divMod` 8 - L.IntegerSize sz a _ -> setAtBits integerInfo ls sz a - L.VectorSize sz a _ -> setAtBits vectorInfo ls sz a - L.FloatSize sz a _ -> setAtBits floatInfo ls sz a - L.AggregateSize sz a _ -> setAtBits aggInfo ls sz a - L.StackObjSize sz a _ -> setAtBits stackInfo ls sz a + where st = L.ptrStorage ps + (w,r) = L.storageSize st `divMod` 8 + L.IntegerSize st -> setStorageAlignInfo integerInfo st + L.VectorSize st -> setStorageAlignInfo vectorInfo st + L.FloatSize st -> setStorageAlignInfo floatInfo st + L.StackObjSize st -> setStorageAlignInfo stackInfo st + L.AggregateSize _ a -> setBits aggregateAlignment ls (L.alignABI a) L.NativeIntSize _ -> return () L.StackAlign a -> setBits stackAlignment ls a -- TODO: For now, we ignore the FunctionPointerAlignType field. This tells @@ -337,6 +330,17 @@ -- should revisit this. L.FunctionPointerAlign _ a -> setBits functionPtrAlignment ls a L.Mangling _ -> return () + -- Currently, we assume that only the default address space (0) is used, + -- and we ignore all other address space-related layout specs. + -- See doc/limitations.md for more discussion. + L.ProgramAddrSpace {} -> return () + L.GlobalAddrSpace {} -> return () + L.AllocaAddrSpace {} -> return () + L.NonIntegralPointerSpaces {} -> return () + where + setStorageAlignInfo :: + Lens' DataLayout AlignInfo -> L.Storage -> State DataLayout () + setStorageAlignInfo info st = setAtBits info ls st -- | Create parsed data layout from layout spec AST. parseDataLayout :: L.DataLayout -> DataLayout 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 @@ -38,7 +38,6 @@ import Data.Text (Text) import qualified Text.LLVM.AST as L -import Type.Reflection (SomeTypeRep(SomeTypeRep)) import Prettyprinter import What4.Interface @@ -100,7 +99,6 @@ = SymbolicPointer | RawBitvector | NoOverride - | Uncallable SomeTypeRep deriving (Eq, Ord) ppFuncLookupError :: FuncLookupError -> Doc ann @@ -109,10 +107,6 @@ SymbolicPointer -> "Cannot resolve a symbolic pointer to a function handle" RawBitvector -> "Cannot treat raw bitvector as function pointer" NoOverride -> "No implementation or override found for pointer" - Uncallable (SomeTypeRep typeRep) -> - vsep [ "Data associated with the pointer found, but was not a callable function:" - , hang 2 (viaShow typeRep) - ] type MemErrContext sym w = MemoryOp sym w diff --git a/src/Lang/Crucible/LLVM/Errors/Poison.hs b/src/Lang/Crucible/LLVM/Errors/Poison.hs --- a/src/Lang/Crucible/LLVM/Errors/Poison.hs +++ b/src/Lang/Crucible/LLVM/Errors/Poison.hs @@ -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 -- ----------------------------------------------------------------------- diff --git a/src/Lang/Crucible/LLVM/Errors/Standards.hs b/src/Lang/Crucible/LLVM/Errors/Standards.hs --- a/src/Lang/Crucible/LLVM/Errors/Standards.hs +++ b/src/Lang/Crucible/LLVM/Errors/Standards.hs @@ -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 diff --git a/src/Lang/Crucible/LLVM/Eval.hs b/src/Lang/Crucible/LLVM/Eval.hs --- a/src/Lang/Crucible/LLVM/Eval.hs +++ b/src/Lang/Crucible/LLVM/Eval.hs @@ -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 + ] diff --git a/src/Lang/Crucible/LLVM/Extension/Syntax.hs b/src/Lang/Crucible/LLVM/Extension/Syntax.hs --- a/src/Lang/Crucible/LLVM/Extension/Syntax.hs +++ b/src/Lang/Crucible/LLVM/Extension/Syntax.hs @@ -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 - -- - -- - 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 - -- - -- - 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 - -- - -- - 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|] []) 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 @@ -434,8 +434,8 @@ basicBlockConstInits bb = foldMap stmtConstInits (L.bbStmts bb) stmtConstInits :: L.Stmt -> LoadRelConstInitMap - stmtConstInits (L.Result _ instr _) = instrConstInits instr - stmtConstInits (L.Effect instr _) = instrConstInits instr + stmtConstInits (L.Result _ instr _ _) = instrConstInits instr + stmtConstInits (L.Effect instr _ _) = instrConstInits instr instrConstInits :: L.Instr -> LoadRelConstInitMap instrConstInits (L.Call _ _ (L.ValSymbol fun) [ptr, _offset]) @@ -483,7 +483,8 @@ foldLoadRelConstInitElem :: L.Global -> L.Value -> Maybe L.Value foldLoadRelConstInitElem global constInitElem | L.ValConstExpr - (L.ConstConv L.Trunc + (L.ConstConv + (L.Trunc False False) (L.Typed { L.typedValue = L.ValConstExpr (L.ConstArith 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 @@ -134,7 +134,9 @@ , SomeLLVMOverride llvmPrefetchOverride_preLLVM10 , SomeLLVMOverride llvmStacksave + , SomeLLVMOverride llvmStacksave_preLLVM18 , SomeLLVMOverride llvmStackrestore + , SomeLLVMOverride llvmStackrestore_preLLVM18 , SomeLLVMOverride (llvmBSwapOverride (knownNat @2)) -- 16 = 2 * 8 , SomeLLVMOverride (llvmBSwapOverride (knownNat @4)) -- 32 = 4 * 8 @@ -160,6 +162,22 @@ , SomeLLVMOverride llvmSinOverride_F64 , SomeLLVMOverride llvmCosOverride_F32 , SomeLLVMOverride llvmCosOverride_F64 + , SomeLLVMOverride llvmTanOverride_F32 + , SomeLLVMOverride llvmTanOverride_F64 + , SomeLLVMOverride llvmAsinOverride_F32 + , SomeLLVMOverride llvmAsinOverride_F64 + , SomeLLVMOverride llvmAcosOverride_F32 + , SomeLLVMOverride llvmAcosOverride_F64 + , SomeLLVMOverride llvmAtanOverride_F32 + , SomeLLVMOverride llvmAtanOverride_F64 + , SomeLLVMOverride llvmAtan2Override_F32 + , SomeLLVMOverride llvmAtan2Override_F64 + , SomeLLVMOverride llvmSinhOverride_F32 + , SomeLLVMOverride llvmSinhOverride_F64 + , SomeLLVMOverride llvmCoshOverride_F32 + , SomeLLVMOverride llvmCoshOverride_F64 + , SomeLLVMOverride llvmTanhOverride_F32 + , SomeLLVMOverride llvmTanhOverride_F64 , SomeLLVMOverride llvmPowOverride_F32 , SomeLLVMOverride llvmPowOverride_F64 , SomeLLVMOverride llvmExpOverride_F32 @@ -484,17 +502,47 @@ ovrWithBackend $ \bak -> liftIO $ addFailedAssertion bak $ AssertFailureSimError "llvm.ubsantrap() called" "") +-- | TODO(#130): This override ought to impose proof obligations related to +-- proper block scoping. llvmStacksave :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext EmptyCtx (LLVMPointerType wptr) llvmStacksave = + [llvmOvr| i8* @llvm.stacksave.p0() |] + (\_memOps _args -> mkNull) + +-- | TODO(#130): This override ought to impose proof obligations related to +-- proper block scoping. +-- +-- See also 'llvmStacksave'. This version exists for compatibility with +-- pre-18 versions of LLVM, where @llvm.stacksave@ always assumed that the +-- returned pointer value resides in address space 0. +llvmStacksave_preLLVM18 + :: (IsSymInterface sym, HasPtrWidth wptr) + => LLVMOverride p sym ext EmptyCtx (LLVMPointerType wptr) +llvmStacksave_preLLVM18 = [llvmOvr| i8* @llvm.stacksave() |] (\_memOps _args -> mkNull) +-- | TODO(#130): This override ought to impose proof obligations related to +-- proper block scoping. llvmStackrestore :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType llvmStackrestore = + [llvmOvr| void @llvm.stackrestore.p0( i8* ) |] + (\_memOps _args -> return ()) + +-- | TODO(#130): This override ought to impose proof obligations related to +-- proper block scoping. +-- +-- See also 'llvmStackrestore'. This version exists for compatibility with +-- pre-18 versions of LLVM, where @llvm.stackrestore@ always assumed that the +-- pointer argument resides in address space 0. +llvmStackrestore_preLLVM18 + :: (IsSymInterface sym, HasPtrWidth wptr) + => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType +llvmStackrestore_preLLVM18 = [llvmOvr| void @llvm.stackrestore( i8* ) |] (\_memOps _args -> return ()) @@ -1175,6 +1223,150 @@ llvmCosOverride_F64 = [llvmOvr| double @llvm.cos.f64( double ) |] (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cos) args) + +llvmTanOverride_F32 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType SingleFloat) + (FloatType SingleFloat) +llvmTanOverride_F32 = + [llvmOvr| float @llvm.tan.f32( float ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tan) args) + +llvmTanOverride_F64 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType DoubleFloat) + (FloatType DoubleFloat) +llvmTanOverride_F64 = + [llvmOvr| double @llvm.tan.f64( double ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tan) args) + +llvmAsinOverride_F32 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType SingleFloat) + (FloatType SingleFloat) +llvmAsinOverride_F32 = + [llvmOvr| float @llvm.asin.f32( float ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arcsin) args) + +llvmAsinOverride_F64 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType DoubleFloat) + (FloatType DoubleFloat) +llvmAsinOverride_F64 = + [llvmOvr| double @llvm.asin.f64( double ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arcsin) args) + +llvmAcosOverride_F32 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType SingleFloat) + (FloatType SingleFloat) +llvmAcosOverride_F32 = + [llvmOvr| float @llvm.acos.f32( float ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arccos) args) + +llvmAcosOverride_F64 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType DoubleFloat) + (FloatType DoubleFloat) +llvmAcosOverride_F64 = + [llvmOvr| double @llvm.acos.f64( double ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arccos) args) + +llvmAtanOverride_F32 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType SingleFloat) + (FloatType SingleFloat) +llvmAtanOverride_F32 = + [llvmOvr| float @llvm.atan.f32( float ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arctan) args) + +llvmAtanOverride_F64 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType DoubleFloat) + (FloatType DoubleFloat) +llvmAtanOverride_F64 = + [llvmOvr| double @llvm.atan.f64( double ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arctan) args) + +llvmSinhOverride_F32 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType SingleFloat) + (FloatType SingleFloat) +llvmSinhOverride_F32 = + [llvmOvr| float @llvm.sinh.f32( float ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sinh) args) + +llvmSinhOverride_F64 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType DoubleFloat) + (FloatType DoubleFloat) +llvmSinhOverride_F64 = + [llvmOvr| double @llvm.sinh.f64( double ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sinh) args) + +llvmCoshOverride_F32 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType SingleFloat) + (FloatType SingleFloat) +llvmCoshOverride_F32 = + [llvmOvr| float @llvm.cosh.f32( float ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cosh) args) + +llvmCoshOverride_F64 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType DoubleFloat) + (FloatType DoubleFloat) +llvmCoshOverride_F64 = + [llvmOvr| double @llvm.cosh.f64( double ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cosh) args) + +llvmTanhOverride_F32 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType SingleFloat) + (FloatType SingleFloat) +llvmTanhOverride_F32 = + [llvmOvr| float @llvm.tanh.f32( float ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tanh) args) + +llvmTanhOverride_F64 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType DoubleFloat) + (FloatType DoubleFloat) +llvmTanhOverride_F64 = + [llvmOvr| double @llvm.tanh.f64( double ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tanh) args) + +llvmAtan2Override_F32 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat) + (FloatType SingleFloat) +llvmAtan2Override_F32 = + [llvmOvr| float @llvm.atan2.f32( float, float ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Arctan2) args) + +llvmAtan2Override_F64 :: + IsSymInterface sym => + LLVMOverride p sym ext + (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat) + (FloatType DoubleFloat) +llvmAtan2Override_F64 = + [llvmOvr| double @llvm.atan2.f64( double, double ) |] + (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Arctan2) args) llvmPowOverride_F32 :: IsSymInterface sym => 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 @@ -95,6 +95,10 @@ , SomeLLVMOverride llvmFreeOverride , SomeLLVMOverride llvmReallocOverride , SomeLLVMOverride llvmStrlenOverride + , SomeLLVMOverride llvmStrnlenOverride + , SomeLLVMOverride llvmStrcpyOverride + , SomeLLVMOverride llvmStrdupOverride + , SomeLLVMOverride llvmStrndupOverride , SomeLLVMOverride llvmPrintfOverride , SomeLLVMOverride llvmPrintfChkOverride , SomeLLVMOverride llvmPutsOverride @@ -392,6 +396,38 @@ [llvmOvr| size_t @strlen( i8* ) |] (\memOps args -> Ctx.uncurryAssignment (callStrlen memOps) args) +llvmStrnlenOverride + :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr + , ?memOpts :: MemOptions ) + => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (BVType wptr) +llvmStrnlenOverride = + [llvmOvr| size_t @strnlen( i8*, size_t ) |] + (\memOps args -> Ctx.uncurryAssignment (callStrnlen memOps) args) + +llvmStrcpyOverride + :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr + , ?memOpts :: MemOptions ) + => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr) (LLVMPointerType wptr) +llvmStrcpyOverride = + [llvmOvr| i8* @strcpy( i8*, i8* ) |] + (\memOps args -> Ctx.uncurryAssignment (callStrcpy memOps) args) + +llvmStrdupOverride + :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr + , ?memOpts :: MemOptions ) + => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (LLVMPointerType wptr) +llvmStrdupOverride = + [llvmOvr| i8* @strdup( i8* ) |] + (\memOps args -> Ctx.uncurryAssignment (callStrdup memOps) args) + +llvmStrndupOverride + :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr + , ?memOpts :: MemOptions ) + => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (LLVMPointerType wptr) +llvmStrndupOverride = + [llvmOvr| i8* @strndup( i8*, size_t ) |] + (\memOps args -> Ctx.uncurryAssignment (callStrndup memOps) args) + ------------------------------------------------------------------------ -- ** Implementations @@ -613,6 +649,66 @@ ovrWithBackend $ \bak -> do mem <- readGlobal mvar liftIO $ strLen bak mem strPtr + +callStrnlen + :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym + , ?memOpts :: MemOptions ) + => GlobalVar Mem + -> RegEntry sym (LLVMPointerType wptr) + -> RegEntry sym (BVType wptr) + -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr)) +callStrnlen mvar (regValue -> strPtr) (regValue -> bound) = + ovrWithBackend $ \bak -> do + mem <- readGlobal mvar + liftIO $ CStr.strnlen bak mem strPtr bound + +callStrcpy + :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym + , ?memOpts :: MemOptions ) + => GlobalVar Mem + -> RegEntry sym (LLVMPointerType wptr) + -> RegEntry sym (LLVMPointerType wptr) + -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) +callStrcpy mvar (regValue -> dst) (regValue -> src) = + ovrWithBackend $ \bak -> + modifyGlobal mvar $ \mem -> do + mem' <- liftIO $ CStr.copyConcretelyNullTerminatedString bak mem dst src Nothing + pure (dst, mem') + +callStrdup + :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym + , ?memOpts :: MemOptions ) + => GlobalVar Mem + -> RegEntry sym (LLVMPointerType wptr) + -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr)) +callStrdup mvar (regValue -> src) = + ovrWithBackend $ \bak -> + modifyGlobal mvar $ \mem -> liftIO $ do + let sym = backendGetSym bak + loc <- plSourceLoc <$> getCurrentProgramLoc sym + let loc' = " " ++ 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' = " " ++ 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 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 @@ -46,6 +46,8 @@ , IndeterminateLoadBehavior(..) , defaultMemOptions , laxPointerMemOptions + , ppLLVMMemIntrinsicType + , ppLLVMIntrinsicTypes -- * Pointers , LLVMPointerType @@ -200,7 +202,6 @@ import Control.Monad.IO.Class import Control.Monad.Trans (lift) import Control.Monad.Trans.State -import Data.Dynamic import Data.IORef import Data.Map (Map) import qualified Data.Map as Map @@ -209,6 +210,7 @@ import Data.Word import qualified GHC.Stack as GHC import Numeric.Natural (Natural) +import qualified Prettyprinter as PP import System.IO (Handle, hPutStrLn) import qualified Data.BitVector.Sized as BV @@ -276,7 +278,7 @@ { memImplBlockSource :: BlockSource , memImplGlobalMap :: GlobalMap sym , memImplSymbolMap :: Map Natural L.Symbol -- inverse mapping to 'memImplGlobalMap' - , memImplHandleMap :: Map Natural Dynamic + , memImplHandleMap :: Map Natural SomeFnHandle , memImplHeap :: G.Mem sym } @@ -359,6 +361,34 @@ --putStrLn "MEM ABORT BRANCH" return $ MemImpl nxt gMap sMap hMap $ G.branchAbortMem m +-- | An intrinsic-printing function for 'MemImpl' for use with +-- 'Lang.Crucible.Types.ppTypeRepr'. +ppLLVMMemIntrinsicType :: + Applicative f => + -- | Fallback for other instrinsics, can be + -- 'Lang.Crucible.Types.ppIntrinsicDefault'. + (forall s ctx'. SymbolRepr s -> CtxRepr ctx' -> f (PP.Doc ann)) -> + SymbolRepr symb -> + CtxRepr ctx -> + f (PP.Doc ann) +ppLLVMMemIntrinsicType fallback symbRepr tyCtx = + case testEquality symbRepr (knownSymbol @"LLVM_memory") of + Nothing -> fallback symbRepr tyCtx + Just Refl -> pure "LLVMMemory" + +-- | An intrinsic-printing function for the LLVM intrinsic types for use with +-- 'Lang.Crucible.Types.ppTypeRepr'. +ppLLVMIntrinsicTypes :: + Applicative f => + -- | Fallback for other instrinsics, can be + -- 'Lang.Crucible.Types.ppIntrinsicDefault'. + (forall s ctx'. SymbolRepr s -> CtxRepr ctx' -> f (PP.Doc ann)) -> + SymbolRepr symb -> + CtxRepr ctx -> + f (PP.Doc ann) +ppLLVMIntrinsicTypes fallback = + ppLLVMMemIntrinsicType (ppLLVMPointerIntrinsicType fallback) + -- | Top-level evaluation function for LLVM extension statements. -- LLVM extension statements are used to implement the memory model operations. llvmStatementExec :: @@ -533,9 +563,7 @@ do mem <- getMem mvar liftIO $ doPtrSubtract bak mem x y - eval LLVM_Debug{} = pure () - mkMemVar :: Text -> HandleAllocator -> IO (GlobalVar Mem) @@ -719,16 +747,16 @@ -- -- See also "Lang.Crucible.LLVM.Functions". doInstallHandle - :: (Typeable a, IsSymBackend sym bak) + :: IsSymBackend sym bak => bak -> LLVMPtr sym wptr - -> a {- ^ handle -} + -> SomeFnHandle -> MemImpl sym -> IO (MemImpl sym) -doInstallHandle _bak ptr x mem = +doInstallHandle _bak ptr hdl mem = case asNat (llvmPointerBlock ptr) of Just blkNum -> - do let hMap' = Map.insert blkNum (toDyn x) (memImplHandleMap mem) + do let hMap' = Map.insert blkNum hdl (memImplHandleMap mem) return mem{ memImplHandleMap = hMap' } Nothing -> panic "MemModel.doInstallHandle" @@ -738,11 +766,11 @@ -- | Look up the handle associated with the given pointer, if any. doLookupHandle - :: (Typeable a, IsSymInterface sym) + :: IsSymInterface sym => sym -> MemImpl sym -> LLVMPtr sym wptr - -> IO (Either ME.FuncLookupError a) + -> IO (Either ME.FuncLookupError SomeFnHandle) doLookupHandle _sym mem ptr = do let LLVMPointer blk _ = ptr case asNat blk of @@ -752,10 +780,7 @@ | otherwise -> case Map.lookup i (memImplHandleMap mem) of Nothing -> return (Left ME.NoOverride) - Just x -> - case fromDynamic x of - Nothing -> return (Left (ME.Uncallable (dynTypeRep x))) - Just a -> return (Right a) + Just hdl -> return (Right hdl) -- | Free the memory region pointed to by the given pointer. -- @@ -1564,6 +1589,13 @@ , "*** Undef value: " ++ show v ] +unpackMemValue _ tpr v@(LLVMValPoison _) = + panic "MemModel.unpackMemValue" + [ "Cannot unpack a `poison` value" + , "*** Crucible type: " ++ show tpr + , "*** Poison value: " ++ show v + ] + unpackMemValue _ tpr v = panic "MemModel.unpackMemValue" [ "Crucible type mismatch when unpacking LLVM value" @@ -1776,6 +1808,8 @@ LLVMValZero <$> toStorableType memty constToLLVMValP _sym _look (UndefConst memty) = liftIO $ LLVMValUndef <$> toStorableType memty +constToLLVMValP _sym _look (PoisonConst memty) = liftIO $ + LLVMValPoison <$> toStorableType memty -- | Translate a constant into an LLVM runtime value. Assumes all necessary 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 @@ -676,7 +676,9 @@ concLLVMVal _ _ v@LLVMValString{} = pure v concLLVMVal _ _ v@LLVMValZero{} = pure v concLLVMVal _ _ (LLVMValUndef st) = - pure (LLVMValZero st) -- ??? does it make sense to turn Undef into Zero? + pure (LLVMValUndef st) +concLLVMVal _ _ (LLVMValPoison st) = + pure (LLVMValPoison st) concWriteSource :: diff --git a/src/Lang/Crucible/LLVM/MemModel/Partial.hs b/src/Lang/Crucible/LLVM/MemModel/Partial.hs --- a/src/Lang/Crucible/LLVM/MemModel/Partial.hs +++ b/src/Lang/Crucible/LLVM/MemModel/Partial.hs @@ -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 = diff --git a/src/Lang/Crucible/LLVM/MemModel/Pointer.hs b/src/Lang/Crucible/LLVM/MemModel/Pointer.hs --- a/src/Lang/Crucible/LLVM/MemModel/Pointer.hs +++ b/src/Lang/Crucible/LLVM/MemModel/Pointer.hs @@ -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. -- diff --git a/src/Lang/Crucible/LLVM/MemModel/Strings.hs b/src/Lang/Crucible/LLVM/MemModel/Strings.hs --- a/src/Lang/Crucible/LLVM/MemModel/Strings.hs +++ b/src/Lang/Crucible/LLVM/MemModel/Strings.hs @@ -15,20 +15,39 @@ -- | Manipulating C-style null-terminated strings module Lang.Crucible.LLVM.MemModel.Strings - ( Mem.loadString + ( storeString + -- * Loading strings + , Mem.loadString , Mem.loadMaybeString - , Mem.strLen , loadConcretelyNullTerminatedString - , loadSymbolicString - , storeString + , loadProvablyNullTerminatedString + -- * String length + , Mem.strLen + , strnlen + , strlenConcreteString + , strlenConcretelyNullTerminatedString + , strlenProvablyNullTerminatedString + -- * String copying + , copyConcreteString + , copyConcretelyNullTerminatedString + , copyProvablyNullTerminatedString + -- * String duplication + , dupConcreteString + , dupConcretelyNullTerminatedString + , dupProvablyNullTerminatedString -- * Low-level string loading primitives -- ** 'ByteChecker' , ControlFlow(..) , ByteChecker(..) + , withMaxChars + -- *** For loading strings , fullyConcreteNullTerminatedString , concretelyNullTerminatedString - , nullTerminatedString - , withMaxChars + , provablyNullTerminatedString + -- *** For string length + , fullyConcreteNullTerminatedStringLength + , concretelyNullTerminatedStringLength + , provablyNullTerminatedStringLength -- ** 'ByteLoader' , ByteLoader(..) , llvmByteLoader @@ -36,8 +55,10 @@ , loadBytes ) where -import Data.Bifunctor (Bifunctor(bimap, first)) +import Control.Lens ((^.), to) +import Data.Bifunctor (Bifunctor(bimap)) import Control.Monad.IO.Class (MonadIO, liftIO) +import qualified Control.Monad.State.Strict as State import qualified Data.BitVector.Sized as BV import Data.Functor ((<&>)) import qualified Data.Parameterized.NatRepr as DPN @@ -48,14 +69,65 @@ import qualified Lang.Crucible.Backend.Online as LCBO import qualified Lang.Crucible.Simulator as LCS import qualified Lang.Crucible.LLVM.DataLayout as CLD +import qualified Lang.Crucible.LLVM.Errors.MemoryError as MemErr import qualified Lang.Crucible.LLVM.MemModel as LCLM import qualified Lang.Crucible.LLVM.MemModel as Mem +import qualified Lang.Crucible.LLVM.MemModel.Generic as Mem.G import qualified Lang.Crucible.LLVM.MemModel.Partial as Partial import qualified What4.Expr.Builder as WEB import qualified What4.Interface as WI import qualified What4.Protocol.Online as WPO import qualified What4.SatResult as WS +-- | Store a null-terminated string to memory. +storeNullTerminatedString :: + forall sym bak w. + ( LCB.IsSymBackend sym bak + , WI.IsExpr (WI.SymExpr sym) + , LCLM.HasPtrWidth w + , LCLM.HasLLVMAnn sym + , ?memOpts :: LCLM.MemOptions + ) => + bak -> + LCLM.MemImpl sym -> + -- | Pointer to write string to + LCLM.LLVMPtr sym w -> + -- | The bytes of the string to write (null terminator included) + Vec.Vector (WI.SymBV sym 8) -> + IO (LCLM.MemImpl sym) +storeNullTerminatedString bak mem ptr bytesBvs = do + let sym = LCB.backendGetSym bak + zeroNat <- WI.natLit sym 0 + let bytes = Vec.map (Mem.LLVMValInt zeroNat) bytesBvs + let val = Mem.LLVMValArray (Mem.bitvectorType 1) bytes + let storTy = Mem.llvmValStorableType @sym val + Mem.storeRaw bak mem ptr storTy CLD.noAlignment val + +-- | Store a string to memory, adding a null terminator at the end. +storeString :: + forall sym bak w. + ( LCB.IsSymBackend sym bak + , WI.IsExpr (WI.SymExpr sym) + , LCLM.HasPtrWidth w + , LCLM.HasLLVMAnn sym + , ?memOpts :: LCLM.MemOptions + ) => + bak -> + LCLM.MemImpl sym -> + -- | Pointer to write string to + LCLM.LLVMPtr sym w -> + -- | The bytes of the string to write (null terminator not included) + Vec.Vector (WI.SymBV sym 8) -> + IO (LCLM.MemImpl sym) +storeString bak mem ptr bytesBvs = do + let sym = LCB.backendGetSym bak + zeroByte <- WI.bvZero sym (DPN.knownNat @8) + let nullTerminatedBytes = Vec.snoc bytesBvs zeroByte + storeNullTerminatedString bak mem ptr nullTerminatedBytes + +--------------------------------------------------------------------- +-- * Loading strings + -- | Load a null-terminated string (with a concrete null terminator) from memory. -- -- The string must contain a concrete null terminator. If a maximum number of @@ -88,14 +160,15 @@ -- | Load a null-terminated string from memory. -- --- Consults an SMT solver to check if any of the loaded bytes are known to be --- null (0). If a maximum number of characters is provided, no more than that --- number of charcters will be read. In either case, 'loadSymbolicString' will --- stop reading if it encounters a null terminator. +-- Consults an SMT solver to check if any of the loaded bytes are known +-- to be null (0). If a maximum number of characters is provided, no +-- more than that number of charcters will be read. In either case, +-- 'loadProvablyNullTerminatedString' will stop reading if it encounters a null +-- terminator. -- -- Note that the loaded string may actually be smaller than the returned list if -- any of the symbolic bytes are equal to 0. -loadSymbolicString :: +loadProvablyNullTerminatedString :: ( LCB.IsSymBackend sym bak , sym ~ WEB.ExprBuilder scope st fs , bak ~ LCBO.OnlineBackend solver scope st fs @@ -111,41 +184,370 @@ -- | Maximum number of characters to read Maybe Int -> IO [WI.SymBV sym 8] -loadSymbolicString bak mem ptr limit = +loadProvablyNullTerminatedString bak mem ptr limit = let loader = llvmByteLoader mem in case limit of - Nothing -> loadBytes bak mem id ptr loader nullTerminatedString + Nothing -> loadBytes bak mem id ptr loader provablyNullTerminatedString Just l -> - let byteChecker = withMaxChars l (\f -> pure (f [])) nullTerminatedString in + let byteChecker = withMaxChars l (\f -> pure (f [])) provablyNullTerminatedString in loadBytes bak mem (id, 0) ptr loader byteChecker --- | Store a string to memory, adding a null terminator at the end. -storeString :: - forall sym bak w. +--------------------------------------------------------------------- +-- * String length + +-- | Implementation of libc @strnlen@. +strnlen :: ( LCB.IsSymBackend sym bak - , WI.IsExpr (WI.SymExpr sym) - , LCLM.HasPtrWidth w - , LCLM.HasLLVMAnn sym - , ?memOpts :: LCLM.MemOptions + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack ) => bak -> - LCLM.MemImpl sym -> - -- | Pointer to write string to - LCLM.LLVMPtr sym w -> - -- | The bytes of the string to write (null terminator not included) + Mem.MemImpl sym -> + -- | Pointer to null-terminated string + Mem.LLVMPtr sym wptr -> + -- | Size + -- + -- If this is not concrete, this will generate an assertion failure. + WI.SymBV sym wptr -> + IO (WI.SymBV sym wptr) +strnlen bak mem ptr bound = do + case BV.asUnsigned <$> WI.asBV bound of + Nothing -> + let err = LCS.AssertFailureSimError "`strnlen` called with symbolic max length" "" in + LCB.addFailedAssertion bak err + Just b -> + let bound' = Just (fromIntegral b) in + strlenConcretelyNullTerminatedString bak mem ptr bound' + +-- | @strlen@ of a concrete string. +-- +-- If any symbolic bytes are encountered, an assertion failure will be +-- generated. If a maximum number of characters is provided, no more than that +-- number of characters will be read. In either case, 'strlenConcreteString' +-- will stop reading if it encounters a null terminator. +strlenConcreteString :: + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + Mem.LLVMPtr sym wptr -> + -- | Maximum number of characters to read + Maybe Int -> + IO Int +strlenConcreteString bak mem ptr limit = do + let loader = llvmByteLoader mem + case limit of + Nothing -> loadBytes bak mem 0 ptr loader fullyConcreteNullTerminatedStringLength + Just 0 -> pure 0 + Just l -> do + let byteChecker = withMaxChars l pure fullyConcreteNullTerminatedStringLength + loadBytes bak mem (0, 0) ptr loader byteChecker + +-- | @strlen@ of a null-terminated string (with a concrete null terminator). +-- +-- The string must contain a concrete null terminator. If a maximum number of +-- characters is provided, no more than that number of characters will be read. +-- In either case, 'strlenConcretelyNullTerminatedString' will stop reading if +-- it encounters a (concretely) null terminator. +-- +-- This has the same behavior as 'Lang.Crucible.LLVM.MemModel.strLen', except +-- that it supports a maximum length. +strlenConcretelyNullTerminatedString :: + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + Mem.LLVMPtr sym wptr -> + -- | Maximum number of characters to read + Maybe Int -> + IO (WI.SymBV sym wptr) +strlenConcretelyNullTerminatedString bak mem ptr limit = do + let loader = llvmByteLoader mem + let sym = LCB.backendGetSym bak + z <- WI.bvZero sym ?ptrWidth + flip State.evalStateT (WI.truePred sym) $ + case limit of + Nothing -> loadBytes bak mem z ptr loader concretelyNullTerminatedStringLength + Just 0 -> liftIO (WI.bvZero (LCB.backendGetSym bak) ?ptrWidth) + Just l -> do + let byteChecker = withMaxChars l pure concretelyNullTerminatedStringLength + loadBytes bak mem (z, 0) ptr loader byteChecker + +-- | @strlen@ of a provably null-terminated string. +-- +-- Consults an SMT solver to check if any of the loaded bytes are known +-- to be null (0). If a maximum number of characters is provided, no +-- more than that number of charcters will be read. In either case, +-- 'strlenProvablyNullTerminatedString' will stop reading if it encounters a +-- (provably) null terminator. +strlenProvablyNullTerminatedString :: + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + , sym ~ WEB.ExprBuilder scope st fs + , bak ~ LCBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + ) => + bak -> + Mem.MemImpl sym -> + Mem.LLVMPtr sym wptr -> + -- | Maximum number of characters to read + Maybe Int -> + IO (WI.SymBV sym wptr) +strlenProvablyNullTerminatedString bak mem ptr limit = do + let loader = llvmByteLoader mem + let sym = LCB.backendGetSym bak + z <- WI.bvZero sym ?ptrWidth + flip State.evalStateT (WI.truePred sym) $ + case limit of + Nothing -> loadBytes bak mem z ptr loader provablyNullTerminatedStringLength + Just 0 -> liftIO (WI.bvZero (LCB.backendGetSym bak) ?ptrWidth) + Just l -> do + let byteChecker = withMaxChars l pure provablyNullTerminatedStringLength + loadBytes bak mem (z, 0) ptr loader byteChecker + +--------------------------------------------------------------------- +-- * String copying + +-- | Helper, not exported +strcpyAssertDisjoint :: + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + -- | Loaded bytes Vec.Vector (WI.SymBV sym 8) -> - IO (LCLM.MemImpl sym) -storeString bak mem ptr bytesBvs = do + -- | Destination pointer + Mem.LLVMPtr sym wptr -> + -- | Source pointer + Mem.LLVMPtr sym wptr -> + IO () +strcpyAssertDisjoint bak mem bytes dst src = do let sym = LCB.backendGetSym bak - zeroNat <- WI.natLit sym 0 - let bytes = Vec.map (Mem.LLVMValInt zeroNat) bytesBvs - zeroByte <- Mem.LLVMValInt zeroNat <$> WI.bvZero sym (DPN.knownNat @8) - let nullTerminatedBytes = Vec.snoc bytes zeroByte - let val = Mem.LLVMValArray (Mem.bitvectorType 1) nullTerminatedBytes - let storTy = Mem.llvmValStorableType @sym val - Mem.storeRaw bak mem ptr storTy CLD.noAlignment val + let len = fromIntegral (Vec.length bytes) + sz <- WI.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth len) + let heap = mem ^. to Mem.memImplHeap + let memOp = + MemErr.MemCopyOp (Just "strcpy dst", dst) (Just "strcpy src", src) sz heap + Mem.assertDisjointRegions bak memOp ?ptrWidth dst sz src sz +-- | @strcpy@ of a concrete string. +-- +-- Uses 'Mem.loadString' to load the string, see that function for details. +-- +-- Asserts that the regions are disjoint. +copyConcreteString :: + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + -- | Destination pointer + Mem.LLVMPtr sym wptr -> + -- | Source pointer + Mem.LLVMPtr sym wptr -> + IO (Mem.MemImpl sym) +copyConcreteString bak mem dst src = do + bytes <- Mem.loadString bak mem src Nothing + let sym = LCB.backendGetSym bak + symBytes <- mapM (WI.bvLit sym WI.knownRepr . BV.word8) bytes + let bytesVec = Vec.fromList symBytes + strcpyAssertDisjoint bak mem bytesVec dst src + storeString bak mem dst (Vec.fromList symBytes) + +-- | @strcpy@ of a concretely null-terminated string. +-- +-- Uses 'loadConcretelyNullTerminatedString' to load the string, see that +-- function for details. +-- +-- Asserts that the regions are disjoint. +copyConcretelyNullTerminatedString :: + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + -- | Destination pointer + Mem.LLVMPtr sym wptr -> + -- | Source pointer + Mem.LLVMPtr sym wptr -> + -- | Maximum number of characters to read + Maybe Int -> + IO (Mem.MemImpl sym) +copyConcretelyNullTerminatedString bak mem dst src bounds = do + bytes <- loadConcretelyNullTerminatedString bak mem src bounds + let bytesVec = Vec.fromList bytes + strcpyAssertDisjoint bak mem bytesVec dst src + storeString bak mem dst bytesVec + +-- | @strcpy@ of a concrete string. +-- +-- Uses 'loadProvablyNullTerminatedString' to load the string, see that +-- function for details. +-- +-- Asserts that the regions are disjoint. +copyProvablyNullTerminatedString :: + ( LCB.IsSymBackend sym bak + , sym ~ WEB.ExprBuilder scope st fs + , bak ~ LCBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + -- | Destination pointer + Mem.LLVMPtr sym wptr -> + -- | Source pointer + Mem.LLVMPtr sym wptr -> + -- | Maximum number of characters to read + Maybe Int -> + IO (Mem.MemImpl sym) +copyProvablyNullTerminatedString bak mem dst src bounds = do + bytes <- loadProvablyNullTerminatedString bak mem src bounds + let bytesVec = Vec.fromList bytes + strcpyAssertDisjoint bak mem bytesVec dst src + storeString bak mem dst bytesVec + --------------------------------------------------------------------- +-- * String duplication + +-- | Helper function: allocate memory and store bytes for string duplication. +-- +-- Takes a vector of bytes (NOT including null terminator) and: +-- 1. Allocates memory of the appropriate size (length + 1 for null terminator) +-- 2. Stores the bytes with null terminator to the allocated memory +-- 3. Returns the new pointer and updated memory +dupFromLoadedBytes :: + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + Vec.Vector (WI.SymBV sym 8) -> + String -> + CLD.Alignment -> + IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym) +dupFromLoadedBytes bak mem bytesVec displayString alignment = do + let len = fromIntegral (Vec.length bytesVec) + 1 -- +1 for null terminator + let sym = LCB.backendGetSym bak + sz <- WI.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth len) + (dst, mem') <- Mem.doMalloc bak Mem.G.HeapAlloc Mem.G.Mutable displayString mem sz alignment + mem'' <- storeString bak mem' dst bytesVec + pure (dst, mem'') + +-- | @strdup@ of a concrete string. +-- +-- Uses 'Mem.loadString' to load the string, see that function for details. +-- +-- Allocates memory and copies the string to it, returning the new pointer. +dupConcreteString :: + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + -- | Source pointer + Mem.LLVMPtr sym wptr -> + -- | Display string for allocation + String -> + -- | Alignment + CLD.Alignment -> + IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym) +dupConcreteString bak mem src displayString alignment = do + bytes <- Mem.loadString bak mem src Nothing + let sym = LCB.backendGetSym bak + symBytes <- mapM (WI.bvLit sym WI.knownRepr . BV.word8) bytes + dupFromLoadedBytes bak mem (Vec.fromList symBytes) displayString alignment + +-- | @strdup@ of a concretely null-terminated string. +-- +-- Uses 'loadConcretelyNullTerminatedString' to load the string, see that +-- function for details. +-- +-- Allocates memory and copies the string to it, returning the new pointer. +dupConcretelyNullTerminatedString :: + ( LCB.IsSymBackend sym bak + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + -- | Source pointer + Mem.LLVMPtr sym wptr -> + -- | Maximum number of characters to read + Maybe Int -> + -- | Display string for allocation + String -> + CLD.Alignment -> + IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym) +dupConcretelyNullTerminatedString bak mem src bounds displayString alignment = do + bytes <- loadConcretelyNullTerminatedString bak mem src bounds + dupFromLoadedBytes bak mem (Vec.fromList bytes) displayString alignment + +-- | @strdup@ of a provably null-terminated string. +-- +-- Uses 'loadProvablyNullTerminatedString' to load the string, see that +-- function for details. +-- +-- Allocates memory and copies the string to it, returning the new pointer. +dupProvablyNullTerminatedString :: + ( LCB.IsSymBackend sym bak + , sym ~ WEB.ExprBuilder scope st fs + , bak ~ LCBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + , Mem.HasPtrWidth wptr + , Mem.HasLLVMAnn sym + , ?memOpts :: Mem.MemOptions + , GHC.HasCallStack + ) => + bak -> + Mem.MemImpl sym -> + -- | Source pointer + Mem.LLVMPtr sym wptr -> + -- | Maximum number of characters to read + Maybe Int -> + -- | Display string for allocation + String -> + CLD.Alignment -> + IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym) +dupProvablyNullTerminatedString bak mem src bounds displayString alignment = do + bytes <- loadProvablyNullTerminatedString bak mem src bounds + dupFromLoadedBytes bak mem (Vec.fromList bytes) displayString alignment + +--------------------------------------------------------------------- -- * Low-level string loading primitives --------------------------------------------------------------------- @@ -192,6 +594,31 @@ let err = LCS.AssertFailureSimError "Found pointer instead of byte when loading string" "" Partial.ptrToBv bak err bytePtr +-- | 'ByteChecker' for adding a maximum character length. +withMaxChars :: + MonadIO m => + GHC.HasCallStack => + LCB.IsSymBackend sym bak => + Functor m => + -- | Maximum number of bytes to load + Int -> + -- | What to do when the maximum is reached + (a -> m b) -> + ByteChecker m sym bak a b -> + ByteChecker m sym bak (a, Int) b +withMaxChars limit done checker = + ByteChecker $ \bak (acc, i) bytePtr -> + runByteChecker checker bak acc bytePtr >>= + \case + Break r -> pure (Break r) + Continue r -> + if i + 1 >= limit + then Break <$> done r + else pure (Continue (r, i + 1)) + +--------------------------------------------------------------------- +-- *** For loading strings + -- | 'ByteChecker' for loading concrete strings. -- -- Currently unused internally, but analogous with @@ -234,10 +661,10 @@ Just 0 -> True _ -> False --- | 'ByteChecker' for loading symbolic strings with a null terminator. +-- | 'ByteChecker' for loading symbolic strings with a provably-null terminator. -- -- Used in 'loadSymbolicString'. -nullTerminatedString :: +provablyNullTerminatedString :: MonadIO m => GHC.HasCallStack => LCB.IsSymBackend sym bak => @@ -245,45 +672,117 @@ bak ~ LCBO.OnlineBackend solver scope st fs => WPO.OnlineSolver solver => ByteChecker m sym bak ([WI.SymBV sym 8] -> [WI.SymBV sym 8]) [WI.SymBV sym 8] -nullTerminatedString = - ByteChecker $ \bak acc bytePtr -> do - byte <- liftIO (ptrToBv8 bak bytePtr) +provablyNullTerminatedString = + ByteChecker $ \bak acc bytePtr -> liftIO $ do + byte <- ptrToBv8 bak bytePtr let sym = LCB.backendGetSym bak - isNullTerm <- liftIO (isNullTerminator bak sym byte) + isNullTerm <- isProvablyNullTerminator bak sym byte if isNullTerm then pure (Break (acc [])) else pure (Continue (\l -> acc (byte : l))) - where - isNullTerminator bak sym symByte = - case BV.asUnsigned <$> WI.asBV symByte of - Just 0 -> pure True - Just _ -> pure False - _ -> - LCBO.withSolverProcess bak (pure False) $ \proc -> do - z <- WI.bvZero sym (WI.knownNat @8) - p <- WI.notPred sym =<< WI.bvEq sym z symByte - WPO.checkSatisfiable proc "nullTerminatedString" p <&> - \case - WS.Unsat () -> True - WS.Sat () -> False - WS.Unknown -> False --- | 'ByteChecker' for adding a maximum character length. -withMaxChars :: +-- Helper, not exported +isProvablyNullTerminator :: GHC.HasCallStack => LCB.IsSymBackend sym bak => - Functor m => - -- | Maximum number of bytes to load - Int -> - -- | What to do when the maximum is reached - (a -> m b) -> - ByteChecker m sym bak a b -> - ByteChecker m sym bak (a, Int) b -withMaxChars limit done checker = - ByteChecker $ \bak (acc, i) bytePtr -> - if i > limit - then Break <$> done acc - else first (, i + 1) <$> runByteChecker checker bak acc bytePtr + sym ~ WEB.ExprBuilder scope st fs => + bak ~ LCBO.OnlineBackend solver scope st fs => + WPO.OnlineSolver solver => + bak -> + sym -> + WI.SymBV sym 8 -> + IO Bool +isProvablyNullTerminator bak sym symByte = + case BV.asUnsigned <$> WI.asBV symByte of + Just 0 -> pure True + Just _ -> pure False + _ -> + LCBO.withSolverProcess bak (pure False) $ \proc -> do + z <- WI.bvZero sym (WI.knownNat @8) + p <- WI.notPred sym =<< WI.bvEq sym z symByte + WPO.checkSatisfiable proc "isProvablyNullTerminator" p <&> + \case + WS.Unsat () -> True + WS.Sat () -> False + WS.Unknown -> False + +--------------------------------------------------------------------- +-- *** For string length + +-- | 'ByteChecker' for @strlen@ of concrete strings. +fullyConcreteNullTerminatedStringLength :: + MonadIO m => + GHC.HasCallStack => + LCB.IsSymBackend sym bak => + ByteChecker m sym bak Int Int +fullyConcreteNullTerminatedStringLength = + ByteChecker $ \bak acc bytePtr -> do + byte <- liftIO (ptrToBv8 bak bytePtr) + case BV.asUnsigned <$> WI.asBV byte of + Just 0 -> pure (Break acc) + Just _ -> pure (Continue $! acc + 1) + Nothing -> do + let msg = "Symbolic value encountered when loading a string" + liftIO (LCB.addFailedAssertion bak (LCS.Unsupported GHC.callStack msg)) + +-- Helper, not exported +symStringLength :: + MonadIO m => + State.MonadState (WI.Pred sym) m => + GHC.HasCallStack => + Mem.HasPtrWidth wptr => + LCB.IsSymBackend sym bak => + -- | How to check if a predicate is false + (bak -> WI.Pred sym -> m Bool) -> + ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr) +symStringLength predIsFalse = + ByteChecker $ \bak len bytePtr -> do + byte <- liftIO (ptrToBv8 bak bytePtr) + keepGoing <- State.get + let sym = LCB.backendGetSym bak + byteWasNonNull <- liftIO (WI.bvIsNonzero sym byte) + keepGoing' <- liftIO (WI.andPred sym keepGoing byteWasNonNull) + stopHere <- predIsFalse bak keepGoing' + if stopHere + then pure (Break len) + else do + State.put keepGoing' + lenPlusOne <- liftIO (WI.bvAdd sym len =<< WI.bvOne sym ?ptrWidth) + Continue <$> liftIO (WI.bvIte sym keepGoing' lenPlusOne len) + +-- | 'ByteChecker' for @strlen@ of strings with a concrete null terminator. +concretelyNullTerminatedStringLength :: + MonadIO m => + State.MonadState (WI.Pred sym) m => + GHC.HasCallStack => + Mem.HasPtrWidth wptr => + LCB.IsSymBackend sym bak => + ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr) +concretelyNullTerminatedStringLength = + symStringLength (\_bak p -> pure (WI.asConstantPred p == Just False)) + +-- | 'ByteChecker' for @strlen@ for strings with a provably-null terminator. +provablyNullTerminatedStringLength :: + MonadIO m => + State.MonadState (WI.Pred sym) m => + GHC.HasCallStack => + LCB.IsSymBackend sym bak => + Mem.HasPtrWidth wptr => + sym ~ WEB.ExprBuilder scope st fs => + bak ~ LCBO.OnlineBackend solver scope st fs => + WPO.OnlineSolver solver => + ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr) +provablyNullTerminatedStringLength = + symStringLength $ \bak p -> + case WI.asConstantPred p of + Just b -> pure b + _ -> + liftIO $ LCBO.withSolverProcess bak (pure False) $ \proc -> do + WPO.checkSatisfiable proc "provablyNullTerminatedStringLength" p <&> + \case + WS.Unsat () -> True + WS.Sat () -> False + WS.Unknown -> False --------------------------------------------------------------------- -- ** 'ByteLoader' 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 @@ -107,7 +107,10 @@ -- | The @undef@ value exists at all storage types. LLVMValUndef :: StorageType -> LLVMVal sym + -- | The @poison@ value exists at all storage types. + LLVMValPoison :: StorageType -> LLVMVal sym + llvmValStorableType :: IsExpr (SymExpr sym) => LLVMVal sym -> StorageType llvmValStorableType v = case v of @@ -120,6 +123,7 @@ LLVMValString bs -> arrayType (fromIntegral (BS.length bs)) (bitvectorType (Bytes 1)) LLVMValZero tp -> tp LLVMValUndef tp -> tp + LLVMValPoison tp -> tp -- | Create a fresh 'LLVMVal' of the given type. freshLLVMVal :: IsSymInterface sym => @@ -145,6 +149,7 @@ case t of LLVMValZero _tp -> pretty "0" LLVMValUndef tp -> pretty " viaShow tp <> pretty ">" + LLVMValPoison tp -> pretty " 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) = "" + show (LLVMValPoison tp) = "" show (LLVMValString _) = "" show (LLVMValInt blk w) | Just 0 <- asNat blk = "" @@ -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) diff --git a/src/Lang/Crucible/LLVM/MemType.hs b/src/Lang/Crucible/LLVM/MemType.hs --- a/src/Lang/Crucible/LLVM/MemType.hs +++ b/src/Lang/Crucible/LLVM/MemType.hs @@ -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 diff --git a/src/Lang/Crucible/LLVM/Translation.hs b/src/Lang/Crucible/LLVM/Translation.hs --- a/src/Lang/Crucible/LLVM/Translation.hs +++ b/src/Lang/Crucible/LLVM/Translation.hs @@ -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 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 @@ -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) diff --git a/src/Lang/Crucible/LLVM/Translation/Constant.hs b/src/Lang/Crucible/LLVM/Translation/Constant.hs --- a/src/Lang/Crucible/LLVM/Translation/Constant.hs +++ b/src/Lang/Crucible/LLVM/Translation/Constant.hs @@ -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 +-- .) -- -- * @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' diff --git a/src/Lang/Crucible/LLVM/Translation/Expr.hs b/src/Lang/Crucible/LLVM/Translation/Expr.hs --- a/src/Lang/Crucible/LLVM/Translation/Expr.hs +++ b/src/Lang/Crucible/LLVM/Translation/Expr.hs @@ -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) = "" show (UndefExpr mt) = "" + show (PoisonExpr 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 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,20 +41,16 @@ import Control.Lens hiding (op, (:>) ) import Control.Monad (MonadPlus(..), forM, unless) import Control.Monad.Except (MonadError(..), runExceptT) -import Control.Monad.State.Strict (MonadState(..), gets) +import Control.Monad.State.Strict (MonadState(..)) import Control.Monad.Trans.Class (MonadTrans(..)) import Control.Monad.Trans.Maybe import Data.Foldable (for_, toList) import Data.Functor (void) import Data.Int -import Data.IntMap.Strict (IntMap) -import qualified Data.IntMap.Strict as IntMap import qualified Data.List as List import Data.List.NonEmpty (NonEmpty((:|))) import qualified Data.Map.Strict as Map import Data.Maybe -import Data.Set (Set) -import qualified Data.Set as Set import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Data.String @@ -83,7 +79,6 @@ import Lang.Crucible.LLVM.Extension import Lang.Crucible.LLVM.MemModel import Lang.Crucible.LLVM.MemType -import qualified Lang.Crucible.LLVM.PrettyPrint as LPP import Lang.Crucible.LLVM.Translation.Constant import Lang.Crucible.LLVM.Translation.Expr import Lang.Crucible.LLVM.Translation.Monad @@ -161,7 +156,7 @@ L.CallBr ty _ _ _ _ -> throwError $ unwords ["unexpected non-function type in callbr:", show ty] L.Alloca ty _ _ -> liftMemType (L.PtrTo ty) L.Load tp _ _ _ -> liftMemType tp - L.ICmp _op tv _ -> do + L.ICmp _samesign _op tv _ -> do inpType <- liftMemType (L.typedType tv) case inpType of VecType len _ -> return (VecType len (IntType 1)) @@ -173,8 +168,8 @@ _ -> return (IntType 1) L.Phi tp _ -> liftMemType tp - L.GEP inbounds baseTy basePtr elts -> - do gepRes <- runExceptT (translateGEP inbounds baseTy basePtr elts) + L.GEP attrs baseTy basePtr elts -> + do gepRes <- runExceptT (translateGEP attrs baseTy basePtr elts) case gepRes of Left err -> throwError err Right (GEPResult lanes tp _gep) -> @@ -239,10 +234,14 @@ -> LLVMGenerator s arch ret (LLVMExpr s arch) extractElt _instr ty _n (UndefExpr _) _i = return $ UndefExpr ty +extractElt _instr ty _n (PoisonExpr _) _i = + return $ PoisonExpr ty extractElt _instr ty _n (ZeroExpr _) _i = return $ ZeroExpr ty extractElt _ ty _ _ (UndefExpr _) = return $ UndefExpr ty +extractElt _ ty _ _ (PoisonExpr _) = + return $ PoisonExpr ty extractElt instr ty n v (ZeroExpr zty) = let ?err = fail in zeroExpand (proxy# :: Proxy# arch) zty $ \_archProxy tyr ex -> extractElt instr ty n v (BaseExpr tyr ex) @@ -295,12 +294,16 @@ -> LLVMGenerator s arch ret (LLVMExpr s arch) insertElt _ ty _ _ _ (UndefExpr _) = do return $ UndefExpr ty +insertElt _ ty _ _ _ (PoisonExpr _) = do + return $ PoisonExpr ty insertElt instr ty n v a (ZeroExpr zty) = do let ?err = fail zeroExpand (proxy# :: Proxy# arch) zty $ \_archProxy tyr ex -> insertElt instr ty n v a (BaseExpr tyr ex) insertElt instr ty n (UndefExpr _) a i = do insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (UndefExpr ty))) a i +insertElt instr ty n (PoisonExpr _) a i = do + insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (PoisonExpr ty))) a i insertElt instr ty n (ZeroExpr _) a i = do insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (ZeroExpr ty))) a i @@ -359,6 +362,11 @@ where tps = map fiType $ toList $ siFields si extractValue (UndefExpr (ArrayType n tp)) is = extractValue (VecExpr tp $ Seq.replicate (fromIntegral n) (UndefExpr tp)) is +extractValue (PoisonExpr (StructType si)) is = + extractValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, PoisonExpr tp)) tps) is + where tps = map fiType $ toList $ siFields si +extractValue (PoisonExpr (ArrayType n tp)) is = + extractValue (VecExpr tp $ Seq.replicate (fromIntegral n) (PoisonExpr tp)) is extractValue (ZeroExpr (StructType si)) is = extractValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, ZeroExpr tp)) tps) is where tps = map fiType $ toList $ siFields si @@ -392,6 +400,11 @@ where tps = map fiType $ toList $ siFields si insertValue (UndefExpr (ArrayType n tp)) v is = insertValue (VecExpr tp $ Seq.replicate (fromIntegral n) (UndefExpr tp)) v is +insertValue (PoisonExpr (StructType si)) v is = + insertValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, PoisonExpr tp)) tps) v is + where tps = map fiType $ toList $ siFields si +insertValue (PoisonExpr (ArrayType n tp)) v is = + insertValue (VecExpr tp $ Seq.replicate (fromIntegral n) (PoisonExpr tp)) v is insertValue (ZeroExpr (StructType si)) v is = insertValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, ZeroExpr tp)) tps) v is where tps = map fiType $ toList $ siFields si @@ -535,8 +548,8 @@ in -- Multiplication overflow will result in a pointer which is not "in -- bounds" for the given allocation. We translate all GEP - -- instructions as if they had the `inbounds` flag set, so the - -- result would be a poison value. + -- instructions as if they had the `inbounds` attribute set, so + -- the result would be a poison value. poisonSideCondition mvar (BVRepr PtrWidth) poison off0 cond -- Perform the pointer offset arithmetic @@ -577,8 +590,10 @@ | n == m = VecExpr outty <$> traverse (\x -> translateConversion instr op inty x outty) xs -- Otherwise, assume scalar values and do the basic conversions -translateConversion instr op _inty x outty = - let showI = showInstr instr in +translateConversion instr op _inty x outty = do + mvar <- getMemVar + let showI = showInstr instr + let noLaxArith = not (laxArith ?transOpts) case op of L.IntToPtr -> do llvmTypeAsRepr outty $ \outty' -> @@ -601,26 +616,46 @@ , Just Refl <- testEquality w' PtrWidth -> return x _ -> fail (unlines ["pointer-to-integer conversion failed", showI]) - L.Trunc -> do + L.Trunc nuw nsw -> do llvmTypeAsRepr outty $ \outty' -> case (asScalar x, outty') of (Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w')) | Just LeqProof <- isPosNat w' , Just LeqProof <- testLeq (incNat w') w -> do x_bv <- pointerAsBitvectorExpr w x' - let bv' = App (BVTrunc w' w x_bv) - return (BaseExpr outty' (BitvectorAsPointerExpr w' bv')) + bv' <- AtomExpr <$> mkAtom (App (BVTrunc w' w x_bv)) + result <- sideConditionsA mvar (BVRepr w') bv' + [ ( nuw && noLaxArith + , fmap (App . BVEq w x_bv . AtomExpr) + (mkAtom (App (BVZext w w' bv'))) + , UB.PoisonValueCreated $ Poison.TruncNoUnsignedWrap x_bv + ) + , ( nsw && noLaxArith + , fmap (App . BVEq w x_bv . AtomExpr) + (mkAtom (App (BVSext w w' bv'))) + , UB.PoisonValueCreated $ Poison.TruncNoSignedWrap x_bv + ) + ] + return (BaseExpr outty' (BitvectorAsPointerExpr w' result)) _ -> fail (unlines [unwords ["invalid truncation:", show x, show outty], showI]) - L.ZExt -> do + L.ZExt nneg -> do llvmTypeAsRepr outty $ \outty' -> case (asScalar x, outty') of (Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w')) | Just LeqProof <- isPosNat w , Just LeqProof <- testLeq (incNat w) w' -> do x_bv <- pointerAsBitvectorExpr w x' - let bv' = App (BVZext w' w x_bv) - return (BaseExpr outty' (BitvectorAsPointerExpr w' bv')) + bv' <- AtomExpr <$> mkAtom (App (BVZext w' w x_bv)) + let z = App $ BVLit w $ BV.zero w + result <- + sideConditionsA mvar (BVRepr w') bv' + [ ( nneg + , pure $ App $ BVSle w z x_bv + , UB.PoisonValueCreated $ Poison.ZExtNonNegative x_bv + ) + ] + return (BaseExpr outty' (BitvectorAsPointerExpr w' result)) _ -> fail (unlines [unwords ["invalid zero extension:", show x, show outty], showI]) L.SExt -> do @@ -640,12 +675,21 @@ L.BitCast -> bitCast _inty x outty #endif - L.UiToFp -> do + L.UiToFp nneg -> do llvmTypeAsRepr outty $ \outty' -> case (asScalar x, outty') of (Scalar _archProxy (LLVMPointerRepr w) x', FloatRepr fi) -> do bv <- pointerAsBitvectorExpr w x' - return $ BaseExpr (FloatRepr fi) $ App $ FloatFromBV fi RNE bv + bvFp <- AtomExpr <$> mkAtom (App (FloatFromBV fi RNE bv)) + let z = App $ BVLit w $ BV.zero w + result <- + sideConditionsA mvar outty' bvFp + [ ( nneg + , pure $ App $ BVSle w z bv + , UB.PoisonValueCreated $ Poison.UiToFpNonNegative bv + ) + ] + return $ BaseExpr (FloatRepr fi) result _ -> fail (unlines [unwords ["Invalid uitofp:", show op, show x, show outty], showI]) L.SiToFp -> do @@ -701,6 +745,8 @@ bitCast _ (UndefExpr _) tgtT = return (UndefExpr tgtT) +bitCast _ (PoisonExpr _) tgtT = return (PoisonExpr tgtT) + -- pointer casts always succeed bitCast (PtrType _) expr (PtrType _) = return expr bitCast (PtrType _) expr PtrOpaqueType = return expr @@ -1271,25 +1317,30 @@ integerCompare :: + -- ^ If 'True', require that the arguments have the same sign. + Bool -> L.ICmpOp -> MemType -> LLVMExpr s arch -> LLVMExpr s arch -> LLVMGenerator s arch ret (LLVMExpr s arch) -integerCompare op (VecType n tp) (explodeVector n -> Just xs) (explodeVector n -> Just ys) = - VecExpr (IntType 1) <$> sequence (Seq.zipWith (\x y -> integerCompare op tp x y) xs ys) +integerCompare samesign op (VecType n tp) (explodeVector n -> Just xs) (explodeVector n -> Just ys) = + VecExpr (IntType 1) <$> sequence (Seq.zipWith (\x y -> integerCompare samesign op tp x y) xs ys) -integerCompare op _ x y = do - b <- scalarIntegerCompare op x y +integerCompare samesign op _ x y = do + b <- scalarIntegerCompare samesign op x y return (BaseExpr (LLVMPointerRepr (knownNat :: NatRepr 1)) (BitvectorAsPointerExpr knownNat (App (BoolToBV knownNat b)))) scalarIntegerCompare :: + -- ^ If 'True', require that the arguments have the same sign. + Bool -> L.ICmpOp -> LLVMExpr s arch -> LLVMExpr s arch -> LLVMGenerator s arch ret (Expr LLVM s BoolType) -scalarIntegerCompare op x y = +scalarIntegerCompare samesign op x y = do + mvar <- getMemVar case (asScalar x, asScalar y) of (Scalar _archProxy (LLVMPointerRepr w) x'', Scalar _archProxy' (LLVMPointerRepr w') y'') | Just Refl <- testEquality w w' @@ -1298,7 +1349,14 @@ | Just Refl <- testEquality w w' -> do xbv <- pointerAsBitvectorExpr w x'' ybv <- pointerAsBitvectorExpr w y'' - return (intcmp w op xbv ybv) + result <- AtomExpr <$> mkAtom (intcmp w op xbv ybv) + let z = App $ BVLit w $ BV.zero w + sideConditionsA mvar BoolRepr result + [ ( samesign + , pure $ App $ BoolEq (App (BVSlt w xbv z)) (App (BVSlt w ybv z)) + , UB.PoisonValueCreated $ Poison.ICmpSameSign xbv ybv + ) + ] _ -> fail $ unlines [ "arithmetic comparison on incompatible values" , "Comparison: " ++ show op , "Value 1: " ++ show x @@ -1514,7 +1572,6 @@ (?transOpts :: TranslationOptions) => TypeRepr ret {- ^ Type of the function return value -} -> L.BlockLabel {- ^ The label of the current LLVM basic block -} -> - Set L.Ident {- ^ Set of usable identifiers -} -> L.Instr {- ^ The instruction to translate -} -> (LLVMExpr s arch -> LLVMGenerator s arch ret ()) {- ^ A continuation to assign the produced value of this instruction to a register -} -> @@ -1523,7 +1580,7 @@ Straightline instructions should enter this continuation, but block-terminating instructions should not. -} -> LLVMGenerator s arch ret a -generateInstr retType lab defSet instr assign_f k = +generateInstr retType lab instr assign_f k = case instr of -- skip phi instructions, they are handled in definePhiBlock L.Phi _ _ -> k @@ -1591,6 +1648,7 @@ do let getV x = case x of UndefExpr _ -> return $ UndefExpr elTy + PoisonExpr _ -> return $ PoisonExpr elTy ZeroExpr _ -> return $ Seq.index v1 0 BaseExpr (LLVMPointerRepr _) (BitvectorAsPointerExpr _ (App (BVLit _ i))) | BV.asUnsigned i < inL -> return $ Seq.index v1 (fromIntegral (BV.asUnsigned i)) @@ -1671,11 +1729,14 @@ callStore vTp ptr' v' align' k - -- NB We treat every GEP as though it has the "inbounds" flag set; + -- NB We treat every GEP as though it has the "inbounds" attribute set; -- thus, the calculation of out-of-bounds pointers results in -- a runtime error. - L.GEP inbounds baseTy basePtr elts -> do - runExceptT (translateGEP inbounds baseTy basePtr elts) >>= \case + -- + -- TODO(#1605): Don't error immediately if the "inbounds" attribute isn't + -- set. + L.GEP attrs baseTy basePtr elts -> do + runExceptT (translateGEP attrs baseTy basePtr elts) >>= \case Left err -> reportError $ fromString $ unlines ["Error translating GEP", err] Right gep -> do gep' <- traverse (\v -> transTypedValue v) gep @@ -1692,14 +1753,14 @@ k L.Call tailcall fnTy fn args -> - callFunction defSet instr tailcall fnTy fn args assign_f >> k + callFunction instr tailcall fnTy fn args assign_f >> k L.Invoke fnTy fn args normLabel _unwindLabel -> do - do callFunction defSet instr False fnTy fn args assign_f + do callFunction instr False fnTy fn args assign_f definePhiBlock lab normLabel L.CallBr fnTy fn args normLabel otherLabels -> do - do callFunction defSet instr False fnTy fn args assign_f + do callFunction instr False fnTy fn args assign_f for_ otherLabels $ \lab' -> void (definePhiBlock lab lab') definePhiBlock lab normLabel @@ -1734,11 +1795,11 @@ assign_f cmp k - L.ICmp op x y -> do + L.ICmp samesign op x y -> do tp <- liftMemType' (L.typedType x) x' <- transTypedValue x y' <- transTypedValue (L.Typed (L.typedType x) y) - cmp <- integerCompare op tp x' y' + cmp <- integerCompare samesign op tp x' y' assign_f cmp k @@ -1803,7 +1864,7 @@ let a0 = memTypeAlign (llvmDataLayout ?lc) resTy oldVal <- callLoad resTy expectTy ptr' a0 - cmp <- scalarIntegerCompare L.Ieq oldVal cmpVal + cmp <- scalarIntegerCompare False L.Ieq oldVal cmpVal let flag = BaseExpr (LLVMPointerRepr (knownNat @1)) (BitvectorAsPointerExpr knownNat (App (BoolToBV knownNat cmp))) @@ -2006,7 +2067,6 @@ -- for debugging intrinsics and breakpoint functions. callFunction :: forall s arch ret. (?transOpts :: TranslationOptions) => - Set L.Ident {- ^ Set of usable identifiers -} -> L.Instr {- ^ Source instruction of the call -} -> Bool {- ^ Is the function a tail call? -} -> L.Type {- ^ type of the function to call -} -> @@ -2014,42 +2074,8 @@ [L.Typed L.Value] {- ^ argument list -} -> (LLVMExpr s arch -> LLVMGenerator s arch ret ()) {- ^ assignment continuation for return value -} -> LLVMGenerator s arch ret () -callFunction defSet instr tailCall_ fnTy fn args assign_f - - -- Supports LLVM 4-12 - | L.ValSymbol "llvm.dbg.declare" <- fn - , debugIntrinsics ?transOpts = - do mbArgs <- dbgArgs defSet args - case mbArgs of - Right (asScalar -> Scalar _ PtrRepr ptr, lv, di) -> - do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Declare ptr lv di)) - return () - Left msg -> addWarning (Text.pack msg) - _ -> addWarning "Unexpected argument in llvm.dbg.declare" - - -- Supports LLVM 6-12 - | L.ValSymbol "llvm.dbg.addr" <- fn - , debugIntrinsics ?transOpts = - do mbArgs <- dbgArgs defSet args - case mbArgs of - Right (asScalar -> Scalar _ PtrRepr ptr, lv, di) -> - do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Addr ptr lv di)) - return () - Left msg -> addWarning (Text.pack msg) - _ -> addWarning "Unexpected argument in llvm.dbg.addr" - - -- Supports LLVM 6-12 (earlier versions had an extra argument) - | L.ValSymbol "llvm.dbg.value" <- fn - , debugIntrinsics ?transOpts = - do mbArgs <- dbgArgs defSet args - case mbArgs of - Right (asScalar -> Scalar _ repr val, lv, di) -> - do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Value repr val lv di)) - return () - Left msg -> addWarning (Text.pack msg) - _ -> addWarning "Unexpected argument in llvm.dbg.value" - - -- Skip calls to other debugging intrinsics. +callFunction instr tailCall_ fnTy fn args assign_f + -- Skip calls to debugging intrinsics. | L.ValSymbol nm <- fn , nm `elem` [ "llvm.dbg.label" , "llvm.dbg.declare" @@ -2080,83 +2106,6 @@ | otherwise = callOrdinaryFunction (Just instr) tailCall_ fnTy fn args assign_f --- | Match the arguments used by @dbg.addr@, @dbg.declare@, and @dbg.value@. --- For more information on how these work, see --- . - --- This function assumes that each argument should either be a particular kind --- of metadata value or a reference that resolves to a particular kind of --- metadata value (see @resolveArg{1,2,3}@ below). If we encounter other types --- of LLVM metadata that breaks this assumption, then we will need to update --- this function's implementation accordingly. -dbgArgs :: - Set L.Ident {- ^ Set of usable identifiers -} -> - [L.Typed L.Value] {- ^ debug call arguments -} -> - LLVMGenerator s arch ret (Either String (LLVMExpr s arch, L.DILocalVariable, L.DIExpression)) -dbgArgs defSet args = do - unnamedMd <- gets (llvmUnnamedMd . llvmContext) - case args of - [valArg, lvArg, diArg] -> do - let resolveRes = do -- Either String - val <- resolveArg1 unnamedMd $ L.typedValue valArg - lv <- resolveArg2 unnamedMd $ L.typedValue lvArg - di <- resolveArg3 unnamedMd $ L.typedValue diArg - Right (val, lv, di) - case resolveRes of - Left err -> pure (Left err) - Right (val, lv, di) -> - let unusableIdents = Set.difference (useTypedVal val) defSet - in if Set.null unusableIdents then - do v <- transTypedValue val - pure (Right (v, lv, di)) - else - do let msg = unwords (["dbg intrinsic def/use violation for:"] ++ - map (show . LPP.ppIdent) (Set.toList unusableIdents)) - pure (Left msg) - _ -> pure (Left ("dbg: expected 3 arguments, got: " ++ show (length args))) - where - resolveArg1 :: - IntMap L.ValMd -> - L.Value -> - Either String (L.Typed L.Value) - resolveArg1 unnamedMd = go - where - go (L.ValMd (L.ValMdRef ref)) - | Just valMd <- IntMap.lookup ref unnamedMd - = go (L.ValMd valMd) - go (L.ValMd (L.ValMdValue val)) = - Right val - go valArg = - Left ("dbg: argument 1 expected value metadata, got: " ++ show valArg) - - resolveArg2 :: - IntMap L.ValMd -> - L.Value -> - Either String L.DILocalVariable - resolveArg2 unnamedMd = go - where - go (L.ValMd (L.ValMdRef ref)) - | Just valMd <- IntMap.lookup ref unnamedMd - = go (L.ValMd valMd) - go (L.ValMd (L.ValMdDebugInfo (L.DebugInfoLocalVariable lv))) = - Right lv - go lvArg = - Left ("dbg: argument 2 expected local variable metadata, got: " ++ show lvArg) - - resolveArg3 :: - IntMap L.ValMd -> - L.Value -> - Either String L.DIExpression - resolveArg3 unnamedMd = go - where - go (L.ValMd (L.ValMdRef ref)) - | Just valMd <- IntMap.lookup ref unnamedMd - = go (L.ValMd valMd) - go (L.ValMd (L.ValMdDebugInfo (L.DebugInfoExpression di))) = - Right di - go diArg = - Left ("dbg: argument 3 expected DIExpression, got: " ++ show diArg) - typedValueAsCrucibleValue :: L.Typed L.Value -> LLVMGenerator s arch ret (Some (Value s)) @@ -2265,6 +2214,12 @@ case testEquality (typeOfReg r) tpr of Just Refl -> assignReg r ex Nothing -> reportError $ fromString $ "type mismatch when assigning undef value" +doAssign (Some r) (PoisonExpr tp) = do + let ?err = fail + poisonExpand (proxy# :: Proxy# arch) tp $ \_archProxy (tpr :: TypeRepr t) (ex :: Expr LLVM s t) -> + case testEquality (typeOfReg r) tpr of + Just Refl -> assignReg r ex + Nothing -> reportError $ fromString $ "type mismatch when assigning poison value" doAssign (Some r) (VecExpr tp vs) = do let ?err = fail llvmTypeAsRepr tp $ \tpr -> 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,8 +53,6 @@ import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.State.Strict (MonadState(..)) import Data.IORef (IORef, modifyIORef) -import Data.IntMap.Strict (IntMap) -import qualified Data.IntMap.Strict as IntMap import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Set (Set) @@ -97,9 +95,6 @@ -- | For each function symbol, compute the set of -- aliases to that symbol , llvmFunctionAliases :: Map L.Symbol (Set L.GlobalAlias) - -- | Map the index of each piece of unnamed LLVM metadata to its value. - -- This information is used to resolve the arguments to debug intrinsics. - , llvmUnnamedMd :: IntMap L.ValMd } llvmTypeCtx :: Simple Lens (LLVMContext arch) TypeContext @@ -113,8 +108,6 @@ unless (null errs) $ malformedLLVMModule "Failed to construct LLVM type context" errs let dl = llvmDataLayout typeCtx - let unnamedMd = - IntMap.fromList [(L.umIndex um, L.umValues um) | um <- L.modUnnamedMd m] case mkNatRepr (ptrBitwidth dl) of Some (wptr :: NatRepr wptr) | Just LeqProof <- testLeq (knownNat @16) wptr -> @@ -130,7 +123,6 @@ , _llvmTypeCtx = typeCtx , llvmGlobalAliases = mempty -- these are computed later , llvmFunctionAliases = mempty -- these are computed later - , llvmUnnamedMd = unnamedMd } return (Some ctx) _ -> diff --git a/test/TestFunctions.hs b/test/TestFunctions.hs --- a/test/TestFunctions.hs +++ b/test/TestFunctions.hs @@ -60,7 +60,8 @@ (L.PtrTo (L.Alias (L.Ident "class.std::cls"))) Nothing (Just 8)) [] - , L.Effect L.RetVoid [] + [] + , L.Effect L.RetVoid [] [] ] } ] diff --git a/test/Tests.hs b/test/Tests.hs --- a/test/Tests.hs +++ b/test/Tests.hs @@ -15,6 +15,7 @@ import Lang.Crucible.FunctionHandle ( newHandleAllocator ) import qualified Data.BitVector.Sized as BV +import Data.Parameterized.DecidableEq ( decEq ) import Data.Parameterized.Some import Data.Parameterized.NatRepr import Data.Parameterized.SymbolRepr ( SomeSym(SomeSym) ) @@ -35,6 +36,8 @@ import Control.Lens (view) import Control.Monad import Data.Either ( fromRight ) +import Data.Functor.Classes ( Eq1(liftEq) ) +import Data.Functor.Identity ( Identity(..) ) import Data.Maybe ( catMaybes ) import GHC.TypeLits import qualified Data.Map.Strict as Map @@ -264,31 +267,133 @@ "extern_int" -> testCase "valid global extern variable reference" $ do Some t <- getTrans - Map.singleton (L.Symbol "extern_int") (Right (i32, Nothing)) @=? - Map.map snd (view globalInitMap t) + case snd <$> Map.lookup (L.Symbol "extern_int") (view globalInitMap t) of + Just (Right (actualTy, actualMbConst)) -> do + let expectedTy = i32 + let expectedMbConst = Nothing + expectedTy @=? actualTy + assertLiftEq llvmConstSyntacticEq expectedMbConst actualMbConst + _ -> assertFailure "Could not look up extern_int" "x=42" -> testCase "valid global integer symbol reference" $ do Some t <- getTrans - Map.singleton (L.Symbol "x") (Right $ (i32, Just $ IntConst (knownNat @32) (BV.mkBV knownNat 42))) @=? - Map.map snd (view globalInitMap t) + case snd <$> Map.lookup (L.Symbol "x") (view globalInitMap t) of + Just (Right (actualTy, actualMbConst)) -> do + let expectedTy = i32 + let expectedMbConst = Just $ IntConst (knownNat @32) (BV.mkBV knownNat 42) + expectedTy @=? actualTy + assertLiftEq llvmConstSyntacticEq expectedMbConst actualMbConst + _ -> assertFailure "Could not look up x" "z.xx=17" -> testCase "valid global struct field symbol reference" $ do Some t <- getTrans - IntConst (knownNat @32) (BV.mkBV knownNat 17) @=? - case snd <$> Map.lookup (L.Symbol "z") (view globalInitMap t) of - Just (Right (_, Just (StructConst _ (x : _)))) -> x - _ -> IntConst (knownNat @1) (BV.zero knownNat) + case snd <$> Map.lookup (L.Symbol "z") (view globalInitMap t) of + Just (Right (_, actualMbConst)) -> + case actualMbConst of + Just (StructConst _ (actualXField : _)) -> do + let expectedXField = IntConst (knownNat @32) (BV.mkBV knownNat 17) + assertLiftEq + llvmConstSyntacticEq + (Identity expectedXField) + (Identity actualXField) + _ -> assertFailure $ + "Expected x to be a struct with at least one field, " ++ + "but it was actually " ++ show actualMbConst + _ -> assertFailure "Could not look up z" "x uninitialized" -> testCase "valid global unitialized variable reference" $ do Some t <- getTrans - Map.singleton (L.Symbol "x") (Right $ (i32, Just $ ZeroConst i32)) @=? - Map.map snd (view globalInitMap t) + case snd <$> Map.lookup (L.Symbol "x") (view globalInitMap t) of + Just (Right (actualTy, actualMbConst)) -> do + let expectedTy = i32 + let expectedMbConst = Just $ ZeroConst i32 + expectedTy @=? actualTy + assertLiftEq llvmConstSyntacticEq expectedMbConst actualMbConst + _ -> assertFailure "Could not look up x" -- We're really just checking that the translation succeeds without -- exceptions. "" -> testCase "no additional checks" $ return () other -> testCase other $ assertFailure $ "Unknown check: " <> other + +-- | Helper, not exported +-- +-- Compare two 'LLVMConst's for syntactic equality. This should not be confused +-- with the semantic notion of equality that LLVM typically uses. For instance, +-- this function considers two 'UndefConst's values to be syntactically equal, +-- but LLVM's semantic equality could deem two @undef@ values to be not equal. +llvmConstSyntacticEq :: LLVMConst -> LLVMConst -> Bool +llvmConstSyntacticEq (ZeroConst mem1) (ZeroConst mem2) = + mem1 == mem2 +llvmConstSyntacticEq (IntConst w1 x1) (IntConst w2 x2) = + case decEq w1 w2 of + Left Refl -> x1 == x2 + Right _ -> False +llvmConstSyntacticEq (FloatConst f1) (FloatConst f2) = + f1 == f2 +llvmConstSyntacticEq (DoubleConst d1) (DoubleConst d2) = + d1 == d2 +llvmConstSyntacticEq (LongDoubleConst ld1) (LongDoubleConst ld2) = + ld1 == ld2 +llvmConstSyntacticEq (StringConst s1) (StringConst s2) = + s1 == s2 +llvmConstSyntacticEq (ArrayConst mem1 a1) (ArrayConst mem2 a2) = + mem1 == mem2 && liftEq llvmConstSyntacticEq a1 a2 +llvmConstSyntacticEq (VectorConst mem1 v1) (VectorConst mem2 v2) = + mem1 == mem2 && liftEq llvmConstSyntacticEq v1 v2 +llvmConstSyntacticEq (StructConst si1 a1) (StructConst si2 a2) = + si1 == si2 && liftEq llvmConstSyntacticEq a1 a2 +llvmConstSyntacticEq (SymbolConst s1 x1) (SymbolConst s2 x2) = + s1 == s2 && x1 == x2 +llvmConstSyntacticEq (UndefConst tp1) (UndefConst tp2) = + tp1 == tp2 +llvmConstSyntacticEq (PoisonConst tp1) (PoisonConst tp2) = + tp1 == tp2 + +llvmConstSyntacticEq (ZeroConst {}) _ = + False +llvmConstSyntacticEq (IntConst {}) _ = + False +llvmConstSyntacticEq (FloatConst {}) _ = + False +llvmConstSyntacticEq (DoubleConst {}) _ = + False +llvmConstSyntacticEq (LongDoubleConst {}) _ = + False +llvmConstSyntacticEq (StringConst {}) _ = + False +llvmConstSyntacticEq (ArrayConst {}) _ = + False +llvmConstSyntacticEq (VectorConst {}) _ = + False +llvmConstSyntacticEq (StructConst {}) _ = + False +llvmConstSyntacticEq (SymbolConst {}) _ = + False +llvmConstSyntacticEq (UndefConst {}) _ = + False +llvmConstSyntacticEq (PoisonConst {}) _ = + False + +-- | Helper, not exported +-- +-- Like 'assertEqual', but lifted to work over an 'Eq1' instance instead of an +-- 'Eq' instance. In addition, this allows the user to customize how to check +-- the underlying values (of type @expected@ and @actual@) for equality. +assertLiftEq :: + (Eq1 f, Show (f expected), Show (f actual), HasCallStack) => + -- | How to check the underlying values for equality + (expected -> actual -> Bool) -> + -- | The expected value + f expected -> + -- | The actual value + f actual -> + Assertion +assertLiftEq eq expected actual = + unless (liftEq eq expected actual) (assertFailure msg) + where + msg = "expected: " ++ show expected ++ "\n but got: " ++ show actual