WIP check

uc-crux-llvm/src/UCCrux/LLVM/Check.hs

@@ -0,0 +1,245 @@
+{-
+Module       : UCCrux.LLVM.Check
+Description  : Check whether constraints hold
+Copyright    : (c) Galois, Inc 2022
+License      : BSD3
+Maintainer   : Langston Barrett <langston@galois.com>
+Stability    : provisional
+
+Create predicates that represent whether or not a set of constraints
+('ConstrainedShape') hold of some Crucible value ('Crucible.RegValue') in some
+LLVM memory ('LLVMMem.MemImpl'). These predicates are used in "check overrides"
+("UCCrux.LLVM.Overrides.Check"), and when applying function specs
+("UCCrux.LLVM.Specs.Apply").
+-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module UCCrux.LLVM.Check
+  ( CheckedConstraint(..),
+    SomeCheckedConstraint(..),
+    SomeCheckedConstraint'(..),
+    checkConstrainedShape,
+  )
+where
+
+{- ORMOLU_DISABLE -}
+import           Prelude hiding (log)
+import           Control.Lens ((^.), (%~), to)
+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
+
+-- what4
+import           What4.Interface (Pred)
+
+-- crucible
+import qualified Lang.Crucible.CFG.Core as Crucible
+import           Lang.Crucible.Backend (IsSymInterface, IsSymBackend, backendGetSym)
+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.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 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 -}
+
+
+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
+
+ifoldMapMFC ::
+  FoldableFCWithIndex t =>
+  Monoid m =>
+  Monad g =>
+  (forall x. IndexF (t f z) x -> f x -> g m) ->
+  t f z ->
+  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
+-- 'ConstrainedShape'.
+checkConstrainedShape ::
+  forall arch m sym argTypes inTy atTy.
+  IsSymInterface sym =>
+  HasLLVMAnn sym =>
+  ArchOk arch =>
+  (?memOpts :: LLVMMem.MemOptions) =>
+  ModuleContext m arch ->
+  sym ->
+  LLVMMem.MemImpl sym ->
+  -- | Selector for provenance information
+  Selector m argTypes inTy atTy ->
+  ConstrainedShape m atTy ->
+  FullTypeRepr m atTy ->
+  Crucible.RegValue sym (ToCrucibleType arch atTy) ->
+  IO (Seq (Some (CheckedConstraint m sym argTypes inTy)))
+checkConstrainedShape modCtx sym mem selector cShape fullTypeRepr val =
+  case getConstrainedShape cShape of
+    Shape.ShapeInt (Compose cs) ->
+      constraintsToSomePreds fullTypeRepr selector cs val
+    Shape.ShapeFloat (Compose cs) ->
+      constraintsToSomePreds fullTypeRepr selector cs val
+    Shape.ShapePtr (Compose cs) Shape.ShapeUnallocated ->
+      constraintsToSomePreds fullTypeRepr selector cs val
+    Shape.ShapePtr (Compose cs) Shape.ShapeAllocated{} ->
+      -- TODO: How to actually tell if the pointer points to something of the
+      -- right size? Might be something in MemModel.* that could help?
+      constraintsToSomePreds fullTypeRepr selector cs val
+    Shape.ShapePtr (Compose cs) (Shape.ShapeInitialized subShapes) ->
+      do -- TODO: Is there code from Setup that helps with the other addresses?
+         -- (Look at 'pointerRange'?)
+         unless (Seq.length subShapes == 1) $
+           Unimplemented.unimplemented
+             "checkPreconds"
+             Unimplemented.CheckPrecondsPtrArray
+         let mts = modCtx ^. moduleTypes
+         (ptdToPred, mbPtdToVal) <- Mem.loadRaw' modCtx sym mem mts val fullTypeRepr
+         let shape = ConstrainedShape (subShapes `Seq.index` 0)
+         let ptdToRepr = pointedToType (modCtx ^. moduleTypes) fullTypeRepr
+         let ptdToSelector = selector & selectorCursor %~ Cursor.deepenPtr mts
+         subs <-
+           case mbPtdToVal of
+             Nothing -> pure Seq.empty
+             Just ptdToVal ->
+               checkPreconds modCtx sym mem ptdToSelector shape ptdToRepr ptdToVal
+         here <- constraintsToSomePreds fullTypeRepr selector cs val
+         let ptdToConstraint =
+               CheckedConstraint
+                 { checkedConstraint =
+                     Left (Initialized (Seq.length subShapes)),
+                   checkedSelector = selector,
+                   checkedPred = ptdToPred
+                 }
+         return (Some ptdToConstraint Seq.<| here <> subs)
+    Shape.ShapeFuncPtr (Compose cs) ->
+      constraintsToSomePreds fullTypeRepr selector cs val
+    Shape.ShapeOpaquePtr (Compose cs) ->
+      constraintsToSomePreds fullTypeRepr selector cs val
+    Shape.ShapeArray (Compose cs) _ subShapes ->
+      (<>)
+      <$> constraintsToSomePreds fullTypeRepr selector cs val
+      <*> ifoldMapM
+            (\i shape ->
+               checkPreconds
+                 modCtx
+                 sym
+                 mem
+                 (selector &
+                  selectorCursor %~
+                  (\c ->
+                    Fin.viewFin
+                      (\i' -> Cursor.deepenArray i' (PVec.length subShapes) c)
+                      i))
+                 (ConstrainedShape shape)
+                 (arrayElementType fullTypeRepr)
+                 (val Vec.! fromIntegral (Fin.finToNat i)))
+            subShapes
+    Shape.ShapeUnboundedArray (Compose cs) subShapes ->
+      (<>)
+      <$> constraintsToSomePreds fullTypeRepr selector cs val
+      <*> ifoldMapM
+            (\i shape ->
+               checkPreconds
+                 modCtx
+                 sym
+                 mem
+                 (Unimplemented.unimplemented
+                    "checkPreconds"
+                    Unimplemented.NonEmptyUnboundedSizeArrays)
+                 (ConstrainedShape shape)
+                 (arrayElementType fullTypeRepr)
+                 (val Vec.! i))
+            subShapes
+    Shape.ShapeStruct (Compose cs) _ ->
+      (<>)
+      <$> constraintsToSomePreds fullTypeRepr selector cs val
+      <*> Unimplemented.unimplemented
+            "checkPreconds"
+            Unimplemented.CheckPrecondsStruct
+
+  where
+    foldMapM :: forall t f m' a. Foldable t => Monoid m' => Monad f => (a -> f m') -> t a -> f m'
+    foldMapM f = foldM (\acc -> fmap (<> acc) . f) mempty
+
+    constraintsToSomePreds ::
+      forall atTy'.
+      FullTypeRepr m atTy' ->
+      Selector m argTypes inTy atTy' ->
+      [Constraint m atTy'] ->
+      Crucible.RegValue sym (ToCrucibleType arch atTy') ->
+      IO (Seq (Some (CheckedConstraint m sym argTypes inTy)))
+    constraintsToSomePreds ftRepr selector_ cs v =
+      fmap (fmap Some) (constraintsToPreds ftRepr selector_ cs v)
+
+    constraintsToPreds ::
+      forall atTy'.
+      FullTypeRepr m atTy' ->
+      Selector m argTypes inTy atTy' ->
+      [Constraint m atTy'] ->
+      Crucible.RegValue sym (ToCrucibleType arch atTy') ->
+      IO (Seq (CheckedConstraint m sym argTypes inTy atTy'))
+    constraintsToPreds ftRepr selector_ cs v =
+      foldMapM
+        (\c ->
+          Seq.singleton . CheckedConstraint (Right c) selector_ <$>
+            constraintToPred modCtx sym c ftRepr v)
+        cs