uc-crux-llvm: Factor out constraint-checking code into its own module

This functionality will be useful for implementing #982.
GaloisInc · Jun 16, 2022 · dbc0bfe · dbc0bfe
1 parent d916a8f
commit dbc0bfe
Show file tree

Hide file tree

Showing 4 changed files with 98 additions and 107 deletions.
diff --git 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
@@ -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