Merge pull request #933 from GaloisInc/lb/skip-clobber

uc-crux-llvm: Configure how external functions clobber/havoc their arguments

uc-crux-llvm/.hlint.yaml

@@ -65,7 +65,7 @@
     within: ["UCCrux.LLVM.Config"]
 - ignore:  # No need for this in the test suite
     name: "Use panic"
-    within: ["Check", "Main", "Utils"]
+    within: ["Check", "Clobber", "Main", "Utils"]
 - ignore:  # Guide to further implementation
     name: "Redundant if"
     within: ["UCCrux.LLVM.Classify.Poison"]

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

@@ -82,6 +82,7 @@ import           Lang.Crucible.LLVM.DataLayout (Alignment, fromAlignment)
 
 import           UCCrux.LLVM.Context.Module (ModuleContext, funcTypes, globalTypes, moduleTypes)
 import           UCCrux.LLVM.Cursor (Cursor, Selector(..), SomeInSelector(SomeInSelector), seekType, checkCompatibility)
+import           UCCrux.LLVM.Errors.Unimplemented (unimplemented, Unimplemented(ClobberConstraints))
 import           UCCrux.LLVM.Shape (Shape, ShapeSeekError)
 import qualified UCCrux.LLVM.Shape as Shape
 import           UCCrux.LLVM.FullType.Translation (ftRetType)
@@ -193,8 +194,8 @@ data RelationalConstraint m (argTypes :: Ctx (FullType m))
 
 data ConstrainedTypedValue m = forall ft.
   ConstrainedTypedValue
-  { constrainedValue :: FullTypeRepr m ft,
-    constrainedType :: ConstrainedShape m ft
+  { constrainedType :: FullTypeRepr m ft,
+    constrainedValue :: ConstrainedShape m ft
   }
 
 -- | A collection of constraints on the state of a program. These are used to
@@ -483,6 +484,10 @@ addConstraint modCtx argTypes constraints =
             )
     NewRelationalConstraint relationalConstraint ->
       Right $ constraints & relationalConstraints %~ (relationalConstraint :)
+    NewConstraint (SomeInSelector SelectClobbered {}) _ ->
+      unimplemented "addConstraint" ClobberConstraints
+    NewShapeConstraint (SomeInSelector SelectClobbered {}) _ ->
+      unimplemented "addConstraint" ClobberConstraints
   where
     addOneConstraint ::
       Constraint m atTy ->

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

@@ -43,6 +43,7 @@ where
 
 {- ORMOLU_DISABLE -}
 import           Control.Lens (Lens, lens, (^.))
+import           Data.Maybe (isJust)
 import           Data.Semigroupoid (Semigroupoid(o))
 import           Data.Type.Equality
 import           Prettyprinter (Doc)
@@ -92,6 +93,9 @@ data Cursor m (inTy :: FullType m) (atTy :: FullType m) where
     Cursor m inTy atTy ->
     Cursor m ('FTStruct fields) atTy
 
+instance Eq (Cursor m inTy atTy) where
+  c1 == c2 = isJust (testEquality c1 c2)
+
 instance Semigroupoid (Cursor m) where
   o cursor1 cursor2 =
     case (cursor1, cursor2) of
@@ -227,21 +231,38 @@ ppCursor top =
 -- | A 'Selector' points to a spot inside
 --
 -- * an argument,
--- * a global variable, or
--- * the manufactured return value from a \"skipped\" function
+-- * a global variable,
+-- * the manufactured return value from a \"skipped\" function, or
+-- * the manufactured value used to clobber something from a \"skipped\"
+--   function.
 --
 -- For documentation of the type parameters, see the comment on 'Cursor'.
 data Selector m (argTypes :: Ctx (FullType m)) inTy atTy
   = SelectArgument !(Ctx.Index argTypes inTy) (Cursor m inTy atTy)
   | SelectGlobal !(GlobalSymbol m) (Cursor m inTy atTy)
+    -- TODO(lb): This doesn't really have enough information - it should contain
+    --
+    -- (1) which function was called,
+    -- (2) which call it was - maybe a callstack plus a counter that gets
+    --     incremented at each call
   | SelectReturn !(FuncSymbol m) (Cursor m inTy atTy)
+    -- TODO(lb): This doesn't really have enough information - it should contain
+    --
+    -- (1) which function was called,
+    -- (2) which call it was - maybe a callstack plus a counter that gets
+    --     incremented at each call
+    -- (3) what got clobbered, i.e., a 'ClobberSelector'
+  | SelectClobbered !(FuncSymbol m) (Cursor m inTy atTy)
+  deriving Eq
 
 -- | A non-parameterized summary of a 'Selector'
 data Where
   = Arg !Int
   | Global !String
   | -- | Name of the skipped function
     ReturnValue !String
+    -- | Name of the skipped function
+  | ClobberedValue !String
   deriving (Eq, Ord)
 
 selectWhere :: Selector m argTypes inTy atTy -> Where
@@ -254,6 +275,9 @@ selectWhere =
     SelectReturn fSymb _ ->
       let L.Symbol f = getFuncSymbol fSymb
        in ReturnValue f
+    SelectClobbered fSymb _ ->
+      let L.Symbol f = getFuncSymbol fSymb
+       in ClobberedValue f
 
 ppWhere :: Where -> PP.Doc ann
 ppWhere =
@@ -262,6 +286,8 @@ ppWhere =
     Global g -> PP.pretty "in global" PP.<+> PP.pretty g
     ReturnValue f ->
       PP.pretty "in return value of skipped function" PP.<+> PP.pretty f
+    ClobberedValue f ->
+      PP.pretty "in value clobbered by skipped function" PP.<+> PP.pretty f
 
 ppSelector :: Selector m argTypes inTy atTy -> PP.Doc ann
 ppSelector selector =
@@ -296,12 +322,14 @@ selectorCursor =
         SelectArgument _ cursor -> cursor
         SelectGlobal _ cursor -> cursor
         SelectReturn _ cursor -> cursor
+        SelectClobbered _ cursor -> cursor
     )
     ( \s v ->
         case s of
           SelectArgument arg _ -> SelectArgument arg v
           SelectGlobal glob _ -> SelectGlobal glob v
           SelectReturn func _ -> SelectReturn func v
+          SelectClobbered func _ -> SelectClobbered func v
     )
 
 $(return [])

uc-crux-llvm/src/UCCrux/LLVM/Errors/Unimplemented.hs

@@ -38,7 +38,10 @@ data Unimplemented
   | CastIntegerToPointer
   | CheckConstraintsPtrArray
   | CheckConstraintsStruct
-  | CheckConstraintsGlobal
+  | SometimesClobber
+  | ClobberConstraints
+  | ClobberGlobal
+  | SeekOffset
   deriving (Eq, Ord)
 
 ppUnimplemented :: Unimplemented -> String
@@ -55,7 +58,10 @@ ppUnimplemented =
     CastIntegerToPointer -> "Value of integer type treated as/cast to a pointer"
     CheckConstraintsPtrArray -> "Checking inferred precondition on an array"
     CheckConstraintsStruct -> "Checking inferred precondition on a struct"
-    CheckConstraintsGlobal -> "Checking inferred precondition on a global"
+    SometimesClobber -> "Selective clobbering"
+    ClobberConstraints -> "Constraints on clobbered values"
+    ClobberGlobal -> "Clobbering global variables"
+    SeekOffset -> "Seeking a pointer at a non-zero offset"
 
 instance PanicComponent Unimplemented where
   panicComponentName _ = "uc-crux-llvm"

uc-crux-llvm/src/UCCrux/LLVM/FullType/Type.hs

@@ -83,6 +83,7 @@ import           Data.Kind (Type)
 import           Data.Functor.Const (Const(Const))
 import           Data.Map (Map)
 import qualified Data.Map as Map
+import           Data.Maybe (isJust)
 import           Data.Type.Equality (TestEquality(testEquality), (:~:)(Refl))
 import qualified Data.Vector as Vec
 import           Unsafe.Coerce (unsafeCoerce)
@@ -210,6 +211,9 @@ data FullTypeRepr (m :: Type) (ft :: FullType m) where
   -- TODO(lb): This could have a symbol repr for the name
   FTOpaquePtrRepr :: L.Ident -> FullTypeRepr m 'FTOpaquePtr
 
+instance Eq (FullTypeRepr m ft) where
+  ft1 == ft2 = isJust (testEquality ft1 ft2)
+
 -- | This functions similarly to 'MemType.SymType'
 data PartTypeRepr (m :: Type) (ft :: FullType m) where
   PTFullRepr :: FullTypeRepr m ft -> PartTypeRepr m ft