diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Check.hs b/uc-crux-llvm/src/UCCrux/LLVM/Check.hs index 6a0970f50..57eb1cba1 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Check.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Check.hs @@ -25,35 +25,26 @@ module UCCrux.LLVM.Check SomeCheckedConstraint(..), SomeCheckedConstraint'(..), checkConstrainedShape, + checkConstrainedShapes, ) where {- ORMOLU_DISABLE -} import Prelude hiding (log) -import Control.Lens ((^.), (%~), to) +import Control.Lens ((^.), (%~)) import Control.Monad (foldM, unless) -import Control.Monad.IO.Class (liftIO) import Data.Function ((&)) import Data.Foldable.WithIndex (FoldableWithIndex, ifoldrM) import Data.Functor.Compose (Compose(Compose)) -import Data.IORef (IORef, modifyIORef) import Data.Sequence (Seq) import qualified Data.Sequence as Seq -import Data.Text (Text) -import qualified Data.Text as Text import Data.Type.Equality ((:~:)(Refl)) import qualified Data.Vector as Vec -import qualified Prettyprinter as PP -import qualified Prettyprinter.Render.Text as PP - -import qualified Text.LLVM.AST as L - import Data.Parameterized.Classes (IndexF) import Data.Parameterized.Ctx (Ctx) import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.Fin as Fin -import Data.Parameterized.TraversableFC (fmapFC) import Data.Parameterized.TraversableFC.WithIndex (FoldableFCWithIndex, ifoldrMFC) import Data.Parameterized.Some (Some(Some), viewSome) import qualified Data.Parameterized.Vector as PVec @@ -62,41 +53,58 @@ import qualified Data.Parameterized.Vector as PVec import What4.Interface (Pred) -- crucible -import qualified Lang.Crucible.CFG.Core as Crucible -import Lang.Crucible.Backend (IsSymInterface, IsSymBackend, backendGetSym) +import Lang.Crucible.Backend (IsSymInterface) import qualified Lang.Crucible.Simulator as Crucible -import qualified Lang.Crucible.Simulator.OverrideSim as Override -- crucible-llvm import Lang.Crucible.LLVM.MemModel (HasLLVMAnn) import qualified Lang.Crucible.LLVM.MemModel as LLVMMem -import Lang.Crucible.LLVM.Intrinsics (LLVM, LLVMOverride(..), basic_llvm_override) -- crux-llvm import Crux.LLVM.Overrides (ArchOk) -- uc-crux-llvm -import UCCrux.LLVM.Constraints (Constraint, ShapeConstraint(Initialized), ConstrainedShape(..), ConstrainedTypedValue(..)) -import UCCrux.LLVM.Context.App (AppContext, log) -import UCCrux.LLVM.Context.Module (ModuleContext, moduleDecls, moduleTypes) +import UCCrux.LLVM.Constraints (Constraint, ShapeConstraint(Initialized), ConstrainedShape(..)) +import UCCrux.LLVM.Context.Module (ModuleContext, moduleTypes) import UCCrux.LLVM.Cursor (Selector, selectorCursor) import qualified UCCrux.LLVM.Cursor as Cursor import qualified UCCrux.LLVM.Errors.Unimplemented as Unimplemented import UCCrux.LLVM.FullType.CrucibleType (SomeIndex(SomeIndex), translateIndex) -import UCCrux.LLVM.FullType.Type (FullType, FullTypeRepr, MapToCrucibleType, ToCrucibleType, pointedToType, arrayElementType, dataLayout) -import UCCrux.LLVM.Logging (Verbosity(Hi)) +import UCCrux.LLVM.FullType.Type (FullType, FullTypeRepr, MapToCrucibleType, ToCrucibleType, pointedToType, arrayElementType) import qualified UCCrux.LLVM.Mem as Mem -import UCCrux.LLVM.Module (FuncSymbol, funcSymbol, getGlobalSymbol) -import UCCrux.LLVM.Overrides.Polymorphic (PolymorphicLLVMOverride, makePolymorphicLLVMOverride) -import UCCrux.LLVM.Overrides.Stack (Stack, collectStack) -import UCCrux.LLVM.Precondition (Preconds, argPreconds, globalPreconds, ppPreconds) -import UCCrux.LLVM.Run.Result (BugfindingResult) -import qualified UCCrux.LLVM.Run.Result as Result import qualified UCCrux.LLVM.Shape as Shape import UCCrux.LLVM.Setup.Constraints (constraintToPred) {- ORMOLU_ENABLE -} +-- | A constraint, together with where it was applied and the resulting 'Pred' +-- it was \"compiled\" to. +-- +-- NOTE(lb): The explicit kind signature here is necessary for GHC 8.8 +-- compatibility. +data CheckedConstraint m sym (argTypes :: Ctx (FullType m)) inTy atTy + = CheckedConstraint + { -- | The 'Constraint' that was applied at this 'Selector' to yield this + -- 'Pred' + checkedConstraint :: Either (ShapeConstraint m atTy) (Constraint m atTy), + -- | The location in an argument or global variable where this + -- 'Constraint' was applied + checkedSelector :: Selector m argTypes inTy atTy, + -- | The \"compiled\"/applied form of the 'Constraint' + checkedPred :: Pred sym + } + +-- NOTE(lb): The explicit kind signature here is necessary for GHC 8.8 +-- compatibility. +data SomeCheckedConstraint m sym (argTypes :: Ctx (FullType m)) = + forall inTy atTy. + SomeCheckedConstraint (CheckedConstraint m sym argTypes inTy atTy) + +data SomeCheckedConstraint' m = + forall sym argTypes inTy atTy. + SomeCheckedConstraint' (CheckedConstraint m sym argTypes inTy atTy) + +-- | Helper, not exported ifoldMapM :: FoldableWithIndex i t => Monoid m => @@ -106,6 +114,7 @@ ifoldMapM :: f m ifoldMapM f = ifoldrM (\i x acc -> fmap (<> acc) (f i x)) mempty +-- | Helper, not exported ifoldMapMFC :: FoldableFCWithIndex t => Monoid m => @@ -115,7 +124,7 @@ ifoldMapMFC :: g m ifoldMapMFC f = ifoldrMFC (\i x acc -> fmap (<> acc) (f i x)) mempty --- | Create a predicate that checks that a Crucible(-LLVM) value conforms to the +-- | Create predicates that check that a Crucible(-LLVM) value conforms to the -- 'ConstrainedShape'. checkConstrainedShape :: forall arch m sym argTypes inTy atTy. @@ -149,7 +158,7 @@ checkConstrainedShape modCtx sym mem selector cShape fullTypeRepr val = -- (Look at 'pointerRange'?) unless (Seq.length subShapes == 1) $ Unimplemented.unimplemented - "checkPreconds" + "checkConstrainedShape" Unimplemented.CheckPrecondsPtrArray let mts = modCtx ^. moduleTypes (ptdToPred, mbPtdToVal) <- Mem.loadRaw' modCtx sym mem mts val fullTypeRepr @@ -160,7 +169,7 @@ checkConstrainedShape modCtx sym mem selector cShape fullTypeRepr val = case mbPtdToVal of Nothing -> pure Seq.empty Just ptdToVal -> - checkPreconds modCtx sym mem ptdToSelector shape ptdToRepr ptdToVal + checkConstrainedShape modCtx sym mem ptdToSelector shape ptdToRepr ptdToVal here <- constraintsToSomePreds fullTypeRepr selector cs val let ptdToConstraint = CheckedConstraint @@ -179,7 +188,7 @@ checkConstrainedShape modCtx sym mem selector cShape fullTypeRepr val = <$> constraintsToSomePreds fullTypeRepr selector cs val <*> ifoldMapM (\i shape -> - checkPreconds + checkConstrainedShape modCtx sym mem @@ -198,12 +207,12 @@ checkConstrainedShape modCtx sym mem selector cShape fullTypeRepr val = <$> constraintsToSomePreds fullTypeRepr selector cs val <*> ifoldMapM (\i shape -> - checkPreconds + checkConstrainedShape modCtx sym mem (Unimplemented.unimplemented - "checkPreconds" + "checkConstrainedShape" Unimplemented.NonEmptyUnboundedSizeArrays) (ConstrainedShape shape) (arrayElementType fullTypeRepr) @@ -213,7 +222,7 @@ checkConstrainedShape modCtx sym mem selector cShape fullTypeRepr val = (<>) <$> constraintsToSomePreds fullTypeRepr selector cs val <*> Unimplemented.unimplemented - "checkPreconds" + "checkConstrainedShape" Unimplemented.CheckPrecondsStruct where @@ -243,3 +252,37 @@ checkConstrainedShape modCtx sym mem selector cShape fullTypeRepr val = Seq.singleton . CheckedConstraint (Right c) selector_ <$> constraintToPred modCtx sym c ftRepr v) cs + +-- | Create predicates that check that an list of Crucible(-LLVM) values conform +-- to a list of 'ConstrainedShape's. +checkConstrainedShapes :: + IsSymInterface sym => + HasLLVMAnn sym => + ArchOk arch => + (?memOpts :: LLVMMem.MemOptions) => + ModuleContext m arch -> + sym -> + LLVMMem.MemImpl sym -> + Ctx.Assignment (FullTypeRepr m) argTypes -> + Ctx.Assignment (ConstrainedShape m) argTypes -> + Ctx.Assignment (Crucible.RegEntry sym) (MapToCrucibleType arch argTypes) -> + IO (Seq (SomeCheckedConstraint m sym argTypes)) +checkConstrainedShapes modCtx sym mem argFTys constraints args = + ifoldMapMFC + (\idx constraint -> + do SomeIndex idx' Refl <- + pure $ + let sz = Ctx.size constraints + in translateIndex modCtx sz idx + let arg = args Ctx.! idx' + let fTy = argFTys Ctx.! idx + fmap (viewSome SomeCheckedConstraint) <$> + checkConstrainedShape + modCtx + sym + mem + (Cursor.SelectArgument idx (Cursor.Here fTy)) + constraint + fTy + (Crucible.regValue arg)) + constraints diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Check.hs b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Check.hs index 57035288c..50786d1f5 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Check.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Check.hs @@ -34,9 +34,6 @@ module UCCrux.LLVM.Overrides.Check ( CheckOverrideName (..), createCheckOverride, checkOverrideFromResult, - CheckedConstraint(..), - SomeCheckedConstraint(..), - SomeCheckedConstraint'(..), CheckedCall, checkedCallContext, checkedCallArgs, @@ -46,36 +43,23 @@ where {- ORMOLU_DISABLE -} import Prelude hiding (log) -import Control.Lens ((^.), (%~), to) -import Control.Monad (foldM, unless) +import Control.Lens ((^.), to) import Control.Monad.IO.Class (liftIO) -import Data.Function ((&)) import Data.Foldable.WithIndex (FoldableWithIndex, ifoldrM) -import Data.Functor.Compose (Compose(Compose)) import Data.IORef (IORef, modifyIORef) import Data.Sequence (Seq) -import qualified Data.Sequence as Seq import Data.Text (Text) import qualified Data.Text as Text -import Data.Type.Equality ((:~:)(Refl)) -import qualified Data.Vector as Vec import qualified Prettyprinter as PP import qualified Prettyprinter.Render.Text as PP import qualified Text.LLVM.AST as L -import Data.Parameterized.Classes (IndexF) import Data.Parameterized.Ctx (Ctx) import qualified Data.Parameterized.Context as Ctx -import qualified Data.Parameterized.Fin as Fin import Data.Parameterized.TraversableFC (fmapFC) -import Data.Parameterized.TraversableFC.WithIndex (FoldableFCWithIndex, ifoldrMFC) -import Data.Parameterized.Some (Some(Some), viewSome) -import qualified Data.Parameterized.Vector as PVec - --- what4 -import What4.Interface (Pred) +import Data.Parameterized.Some (viewSome) -- crucible import qualified Lang.Crucible.CFG.Core as Crucible @@ -92,15 +76,12 @@ import Lang.Crucible.LLVM.Intrinsics (LLVM, LLVMOverride(..), basic_ll import Crux.LLVM.Overrides (ArchOk) -- uc-crux-llvm -import UCCrux.LLVM.Check (checkPreconds) -import UCCrux.LLVM.Constraints (Constraint, ShapeConstraint(Initialized), ConstrainedShape(..), ConstrainedTypedValue(..)) +import UCCrux.LLVM.Check (SomeCheckedConstraint(..), checkConstrainedShape, checkConstrainedShapes) +import UCCrux.LLVM.Constraints (ConstrainedTypedValue(..)) import UCCrux.LLVM.Context.App (AppContext, log) import UCCrux.LLVM.Context.Module (ModuleContext, moduleDecls, moduleTypes) -import UCCrux.LLVM.Cursor (Selector, selectorCursor) import qualified UCCrux.LLVM.Cursor as Cursor -import qualified UCCrux.LLVM.Errors.Unimplemented as Unimplemented -import UCCrux.LLVM.FullType.CrucibleType (SomeIndex(SomeIndex), translateIndex) -import UCCrux.LLVM.FullType.Type (FullType, FullTypeRepr, MapToCrucibleType, ToCrucibleType, pointedToType, arrayElementType, dataLayout) +import UCCrux.LLVM.FullType.Type (FullType, FullTypeRepr, MapToCrucibleType, dataLayout) import UCCrux.LLVM.Logging (Verbosity(Hi)) import qualified UCCrux.LLVM.Mem as Mem import UCCrux.LLVM.Module (FuncSymbol, funcSymbol, getGlobalSymbol) @@ -109,8 +90,6 @@ import UCCrux.LLVM.Overrides.Stack (Stack, collectStack) import UCCrux.LLVM.Precondition (Preconds, argPreconds, globalPreconds, ppPreconds) import UCCrux.LLVM.Run.Result (BugfindingResult) import qualified UCCrux.LLVM.Run.Result as Result -import qualified UCCrux.LLVM.Shape as Shape -import UCCrux.LLVM.Setup.Constraints (constraintToPred) {- ORMOLU_ENABLE -} newtype CheckOverrideName = CheckOverrideName {getCheckOverrideName :: Text} @@ -121,33 +100,6 @@ declName decl = let L.Symbol name = L.decName decl in Text.pack name --- | A constraint, together with where it was applied and the resulting 'Pred' --- it was \"compiled\" to. --- --- NOTE(lb): The explicit kind signature here is necessary for GHC 8.8 --- compatibility. -data CheckedConstraint m sym (argTypes :: Ctx (FullType m)) inTy atTy - = CheckedConstraint - { -- | The 'Constraint' that was applied at this 'Selector' to yield this - -- 'Pred' - checkedConstraint :: Either (ShapeConstraint m atTy) (Constraint m atTy), - -- | The location in an argument or global variable where this - -- 'Constraint' was applied - checkedSelector :: Selector m argTypes inTy atTy, - -- | The \"compiled\"/applied form of the 'Constraint' - checkedPred :: Pred sym - } - --- NOTE(lb): The explicit kind signature here is necessary for GHC 8.8 --- compatibility. -data SomeCheckedConstraint m sym (argTypes :: Ctx (FullType m)) = - forall inTy atTy. - SomeCheckedConstraint (CheckedConstraint m sym argTypes inTy atTy) - -data SomeCheckedConstraint' m = - forall sym argTypes inTy atTy. - SomeCheckedConstraint' (CheckedConstraint m sym argTypes inTy atTy) - -- | This is what a check override (see 'createCheckOverride') records when it -- is called during execution, consisting of the calling context, the arguments, -- and the results of checking all of the constraints on arguments and global @@ -167,6 +119,16 @@ data CheckedCall m sym arch (argTypes :: Ctx (FullType m)) = checkedCallPreconds :: Seq (SomeCheckedConstraint m sym argTypes) } +-- | Helper, not exported +ifoldMapM :: + FoldableWithIndex i t => + Monoid m => + Monad f => + (i -> a -> f m) -> + t a -> + f m +ifoldMapM f = ifoldrM (\i x acc -> fmap (<> acc) (f i x)) mempty + -- TODO: Split out the part that simply wraps a call to an existing LLVM CFG -- with additional Override actions before and after into its own module. @@ -230,24 +192,7 @@ createCheckOverride appCtx modCtx usedRef argFTys constraints cfg funcSym = Ctx.Assignment (Crucible.RegEntry sym) (MapToCrucibleType arch argTypes) -> IO (Seq (SomeCheckedConstraint m sym argTypes)) getArgPreconds sym mem args = - ifoldMapMFC - (\idx constraint -> - do SomeIndex idx' Refl <- - pure $ - let sz = Ctx.size (constraints ^. argPreconds) - in translateIndex modCtx sz idx - let arg = args Ctx.! idx' - let fTy = argFTys Ctx.! idx - fmap (viewSome SomeCheckedConstraint) <$> - checkPreconds - modCtx - sym - mem - (Cursor.SelectArgument idx (Cursor.Here fTy)) - constraint - fTy - (Crucible.regValue arg)) - (constraints ^. argPreconds) + checkConstrainedShapes modCtx sym mem argFTys (constraints ^. argPreconds) args getGlobalPreconds :: IsSymBackend sym bak => @@ -264,7 +209,7 @@ createCheckOverride appCtx modCtx usedRef argFTys constraints cfg funcSym = let dl = modCtx ^. moduleTypes . to dataLayout glob <- Mem.loadGlobal modCtx dl bak mem globTy (getGlobalSymbol gSymb) fmap (viewSome SomeCheckedConstraint) <$> - checkPreconds + checkConstrainedShape modCtx sym mem diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs index 5c3c05bfb..b37fb7290 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs @@ -68,6 +68,8 @@ import qualified Crux.LLVM.Config as CruxLLVM import Crux.LLVM.Overrides (ArchOk) -- local +import UCCrux.LLVM.Check (SomeCheckedConstraint(..)) +import qualified UCCrux.LLVM.Check as Check import UCCrux.LLVM.Cursor (ppSelector) import UCCrux.LLVM.Context.App (AppContext) import UCCrux.LLVM.Context.Module (ModuleContext, CFGWithTypes(..), findFun) @@ -387,9 +389,9 @@ ppSomeCheckResult _appCtx entry proxy@(SomeCheckResult _ftReprs (CheckResult k)) forall sym argTypes. IsSymInterface sym => sym -> - Check.SomeCheckedConstraint m sym argTypes -> + SomeCheckedConstraint m sym argTypes -> IO (PP.Doc ann) - ppCheckedConstraint _sym (Check.SomeCheckedConstraint constraint) = + ppCheckedConstraint _sym (SomeCheckedConstraint constraint) = do return $ PP.vsep [ "Constraint:" PP.<+> diff --git a/uc-crux-llvm/test/Check.hs b/uc-crux-llvm/test/Check.hs index f9b8e2d39..ac34fa571 100644 --- a/uc-crux-llvm/test/Check.hs +++ b/uc-crux-llvm/test/Check.hs @@ -29,6 +29,7 @@ import qualified Test.Tasty.HUnit as TH import qualified What4.Interface as What4 +import qualified UCCrux.LLVM.Check as Check import UCCrux.LLVM.Context.Function (makeFunctionContext) import UCCrux.LLVM.Context.Module (ModuleContext, CFGWithTypes(..), defnTypes, findFun, withModulePtrWidth) import UCCrux.LLVM.Module (FuncSymbol(FuncDefnSymbol), DefnSymbol, defnSymbolToString)