uc-crux-llvm: New type for function postconditions

The Postcondition module declares a type that approximates a specification of a function's postconditions. This is used in Classify to infer such postconditions on return values, in the future it may be used to infer information about clobbered memory. This module supersedes the "Clobber" specs that were part of the Skip override machinery. These weren't amenable to use-cases such as inference. Also implement some additional pretty-printing machinery.
GaloisInc · May 12, 2022 · c970b60 · c970b60
1 parent 108a6e2
commit c970b60
Show file tree

Hide file tree

Showing 18 changed files with 979 additions and 480 deletions.
diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Classify.hs b/uc-crux-llvm/src/UCCrux/LLVM/Classify.hs
@@ -84,12 +84,12 @@ import           UCCrux.LLVM.Module (makeFuncSymbol, makeGlobalSymbol, globalSym
 import           UCCrux.LLVM.Newtypes.PreSimulationMem (PreSimulationMem, getPreSimulationMem)
 import           UCCrux.LLVM.Overrides.Skip (SkipOverrideName)
 import           UCCrux.LLVM.PP (ppProgramLoc)
-import           UCCrux.LLVM.Precondition (NewConstraint(..))
 import           UCCrux.LLVM.Setup (SymValue)
 import           UCCrux.LLVM.Setup.Monad (TypedSelector(..), mallocLocation)
 import           UCCrux.LLVM.Shape (Shape)
 import qualified UCCrux.LLVM.Shape as Shape
 import           UCCrux.LLVM.Errors.Panic (panic)
+import qualified UCCrux.LLVM.Precondition as Pre
 import           UCCrux.LLVM.Errors.Unimplemented (unimplemented)
 import qualified UCCrux.LLVM.Errors.Unimplemented as Unimplemented
 {- ORMOLU_ENABLE -}
@@ -699,11 +699,11 @@ doClassifyBadBehavior appCtx modCtx funCtx sym memImpl skipped simError (Crucibl
     argName :: Ctx.Index argTypes tp -> String
     argName idx = funCtx ^. argumentNames . ixF' idx . to getConst . to (maybe "<top>" Text.unpack)
 
-    oneConstraint selector constraint =
-      [NewConstraint (SomeInSelector selector) constraint]
+    oneConstraint selector pre =
+      [Pre.NewConstraint (SomeInSelector selector) pre]
 
-    oneShapeConstraint selector shapeConstraint =
-      [NewShapeConstraint (SomeInSelector selector) shapeConstraint]
+    oneShapeConstraint selector shapePre =
+      [Pre.NewShapeConstraint (SomeInSelector selector) shapePre]
 
     getConcretePointerBlock :: LLVMPtr.LLVMPtr sym w -> IO (Maybe Natural)
     getConcretePointerBlock ptr =

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Constraints.hs b/uc-crux-llvm/src/UCCrux/LLVM/Constraints.hs
@@ -28,6 +28,7 @@ module UCCrux.LLVM.Constraints
     -- * 'ConstrainedShape'
     ConstrainedShape (..),
     minimalConstrainedShape,
+    ppConstrainedShape,
   )
 where
 
@@ -36,6 +37,7 @@ import           Data.BitVector.Sized (BV)
 import qualified Data.BitVector.Sized as BV
 import           Data.Functor.Compose (Compose(..))
 import           Data.Kind (Type)
+import           Data.Void (Void)
 import           Prettyprinter (Doc)
 import qualified Prettyprinter as PP
 
@@ -175,3 +177,7 @@ minimalConstrainedShape =
 instance Eq (ConstrainedShape m ft) where
   ConstrainedShape shape1 == ConstrainedShape shape2 =
     Shape.eqShape (\(Compose c1) (Compose c2) -> c1 == c2) shape1 shape2
+
+ppConstrainedShape :: ConstrainedShape m ft -> Doc Void
+ppConstrainedShape =
+  Shape.ppShape (PP.vsep . map ppConstraint . getCompose) . getConstrainedShape
diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Errors/Unimplemented.hs b/uc-crux-llvm/src/UCCrux/LLVM/Errors/Unimplemented.hs
@@ -38,8 +38,7 @@ data Unimplemented
   | CastIntegerToPointer
   | CheckPrecondsPtrArray
   | CheckPrecondsStruct
-  | SometimesClobber
-  | ClobberConstraints
+  | ClobberPreconds
   | ClobberGlobal
   | SeekOffset
   deriving (Eq, Ord)
@@ -58,8 +57,7 @@ ppUnimplemented =
     CastIntegerToPointer -> "Value of integer type treated as/cast to a pointer"
     CheckPrecondsPtrArray -> "Checking inferred precondition on an array"
     CheckPrecondsStruct -> "Checking inferred precondition on a struct"
-    SometimesClobber -> "Selective clobbering"
-    ClobberConstraints -> "Constraints on clobbered values"
+    ClobberPreconds -> "Preconditions on clobbered values"
     ClobberGlobal -> "Clobbering global variables"
     SeekOffset -> "Seeking a pointer at a non-zero offset"
 

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/FullType/CrucibleType.hs b/uc-crux-llvm/src/UCCrux/LLVM/FullType/CrucibleType.hs
@@ -18,6 +18,9 @@ Stability        : provisional
 
 module UCCrux.LLVM.FullType.CrucibleType
   ( toCrucibleType,
+    toCrucibleReturnType,
+
+    opaquePointersToCrucibleCompat,
 
     -- * Assignments
     SomeIndex (..),
@@ -30,17 +33,20 @@ module UCCrux.LLVM.FullType.CrucibleType
     translateIndex,
     generateM,
     generate,
+    CrucibleTypeCompat(..),
+    zip
   )
 where
 
 {- ORMOLU_DISABLE -}
-import           Prelude hiding (unzip)
+import           Prelude hiding (unzip, zip, zipWith)
 
 import           Data.Coerce (coerce)
 import           Data.Functor ((<&>))
 import           Data.Functor.Const (Const(Const))
 import           Data.Functor.Identity (Identity(Identity, runIdentity))
 import           Data.Functor.Product (Product(Pair))
+import           Unsafe.Coerce (unsafeCoerce)
 
 import qualified Data.Parameterized.Context as Ctx
 import           Data.Parameterized.NatRepr
@@ -78,6 +84,16 @@ toCrucibleType proxy =
       case assignmentToCrucibleType proxy typeReprs of
         SomeAssign' ctReprs Refl _ -> CrucibleTypes.StructRepr ctReprs
 
+toCrucibleReturnType ::
+  ArchOk arch =>
+  proxy arch ->
+  ReturnTypeRepr m mft ->
+  CrucibleTypes.TypeRepr (ReturnTypeToCrucibleType arch mft)
+toCrucibleReturnType proxy =
+  \case
+    VoidRepr -> CrucibleTypes.UnitRepr
+    NonVoidRepr ftRepr -> toCrucibleType proxy ftRepr
+
 data SomeAssign' arch m fullTypes f = forall crucibleTypes.
   SomeAssign'
   { saCrucibleTypes :: Ctx.Assignment CrucibleTypes.TypeRepr crucibleTypes,
@@ -139,6 +155,95 @@ assignmentToCrucibleType proxy fullTypes =
   runIdentity
     (assignmentToCrucibleTypeA proxy (\_ _ -> Identity (Const ())) fullTypes)
 
+-- | See 'opaquePointersToCrucibleCompat'
+-- to Crucible types.
+mapOpaquePointersToCrucibleCompat ::
+  ArchOk arch =>
+  (MapOpaquePointers ctx ~ MapOpaquePointers ctx') =>
+  proxy arch ->
+  Ctx.Assignment (FullTypeRepr m) ctx ->
+  Ctx.Assignment (FullTypeRepr m) ctx' ->
+  MapToCrucibleType arch ctx :~: MapToCrucibleType arch ctx'
+mapOpaquePointersToCrucibleCompat proxy a a' =
+  case (Ctx.viewAssign a, Ctx.viewAssign a') of
+    (Ctx.AssignEmpty, Ctx.AssignEmpty) -> Refl
+    (Ctx.AssignExtend rest hd, Ctx.AssignExtend rest' hd') ->
+      case (opaquePointersToCrucibleCompat proxy hd hd', mapOpaquePointersToCrucibleCompat proxy rest rest') of
+        (Refl, Refl) -> Refl
+
+-- | Despite being unused, DO NOT REMOVE. See comment on
+-- 'opaquePointersToCrucibleCompat'.
+_opaquePointersToCrucibleCompat ::
+  ArchOk arch =>
+  (OpaquePointers ft ~ OpaquePointers ft') =>
+  proxy arch ->
+  FullTypeRepr m ft ->
+  FullTypeRepr m ft' ->
+  (ToCrucibleType arch ft :~: ToCrucibleType arch ft')
+_opaquePointersToCrucibleCompat proxy ft ft' =
+  case (ft, ft') of
+    (FTIntRepr {}, FTIntRepr {}) -> Refl
+    (FTPtrRepr{}, FTPtrRepr{}) -> Refl
+    (FTPtrRepr{}, FTOpaquePtrRepr{}) -> Refl
+    (FTPtrRepr{}, FTVoidFuncPtrRepr{}) -> Refl
+    (FTPtrRepr{}, FTNonVoidFuncPtrRepr{}) -> Refl
+    (FTFloatRepr{}, FTFloatRepr{}) -> Refl
+    (FTVoidFuncPtrRepr{}, FTVoidFuncPtrRepr{}) -> Refl
+    (FTVoidFuncPtrRepr{}, FTPtrRepr{}) -> Refl
+    (FTVoidFuncPtrRepr{}, FTOpaquePtrRepr{}) -> Refl
+    (FTVoidFuncPtrRepr{}, FTNonVoidFuncPtrRepr{}) -> Refl
+    (FTNonVoidFuncPtrRepr{}, FTNonVoidFuncPtrRepr{}) -> Refl
+    (FTNonVoidFuncPtrRepr{}, FTPtrRepr{}) -> Refl
+    (FTNonVoidFuncPtrRepr{}, FTOpaquePtrRepr{}) -> Refl
+    (FTNonVoidFuncPtrRepr{}, FTVoidFuncPtrRepr{}) -> Refl
+    (FTOpaquePtrRepr{}, FTOpaquePtrRepr{}) -> Refl
+    (FTOpaquePtrRepr{}, FTPtrRepr{}) -> Refl
+    (FTOpaquePtrRepr{}, FTVoidFuncPtrRepr{}) -> Refl
+    (FTOpaquePtrRepr{}, FTNonVoidFuncPtrRepr{}) -> Refl
+    (FTUnboundedArrayRepr elems, FTUnboundedArrayRepr elems') ->
+      case opaquePointersToCrucibleCompat proxy elems elems' of
+        Refl -> Refl
+    (FTArrayRepr _ elems, FTArrayRepr _ elems') ->
+      case opaquePointersToCrucibleCompat proxy elems elems' of
+        Refl -> Refl
+    (FTStructRepr _ fields, FTStructRepr _ fields') ->
+      case mapOpaquePointersToCrucibleCompat proxy fields fields' of
+        Refl -> Refl
+
+-- | Two types that are identical up to pointer types also have the same mapping
+-- to Crucible types.
+--
+-- This function is implemented using 'unsafeCoerce'. The safety of this use is
+-- justified by the above implementation of @_opaquePointersToCrucibleCompat@,
+-- which takes two 'FullTypeRepr's and proves that
+-- @'OpaquePointers' ft1 ~ 'OpaquePointers' ft2@ implies
+-- @'ToCrucibleType' arch ft1 ~ ToCrucibleType arch ft2@.
+-- Since 'FullTypeRepr' is a singleton type and every
+-- 'UCCrux.LLVM.FullType.Type.FullType' is represented by some 'FullTypeRepr',
+-- we can conclude that the reasoning holds even when 'FullTypeRepr's aren't
+-- available.
+--
+-- There are two reasons to implement this unsafely:
+--
+-- * It's faster; the unsafe version is /O(1)/ whereas the safe version is
+--   /O(n)/.
+-- * It can be used even when a 'FullTypeRepr' for each type isn't available.
+opaquePointersToCrucibleCompat ::
+  forall proxy proxy' proxy'' arch ft ft'.
+  ArchOk arch =>
+  (OpaquePointers ft ~ OpaquePointers ft') =>
+  proxy arch ->
+  proxy' ft ->
+  proxy'' ft' ->
+  (ToCrucibleType arch ft :~: ToCrucibleType arch ft')
+opaquePointersToCrucibleCompat _ _ _ =
+  -- Explicitly type the unsafeCoerce to avoid accidentally treating it as a
+  -- function type.
+  unsafeCoerce (Refl :: () :~: ()) :: ToCrucibleType arch ft :~: ToCrucibleType arch ft'
+{-# NOINLINE opaquePointersToCrucibleCompat #-}
+-- ^ NOINLINE to work around GHC issues, see
+-- https://github.com/GaloisInc/parameterized-utils/blob/4b6562fdf334849d63435442bbcd2a6d9bce34a7/src/Data/Parameterized/Axiom.hs#L32
+
 testCompatibility ::
   forall proxy arch m ft tp.
   ArchOk arch =>
@@ -251,3 +356,27 @@ generate ::
   ) ->
   Ctx.Assignment f (MapToCrucibleType arch fullTypes)
 generate proxy sz f = coerce (generateM proxy sz (\i1 i2 refl -> Identity (f i1 i2 refl)))
+
+newtype CrucibleTypeCompat arch f ft =
+  CrucibleTypeCompat (f (ToCrucibleType arch ft))
+
+zipWith ::
+  ArchOk arch =>
+  proxy arch ->
+  (forall ft. f ft -> g (ToCrucibleType arch ft) -> h ft) ->
+  Ctx.Assignment f ctx ->
+  Ctx.Assignment g (MapToCrucibleType arch ctx) ->
+  Ctx.Assignment h ctx
+zipWith proxy fun ftAssign ctAssign =
+  case (Ctx.viewAssign ftAssign, Ctx.viewAssign ctAssign) of
+    (Ctx.AssignEmpty, Ctx.AssignEmpty) -> Ctx.empty
+    (Ctx.AssignExtend ftRest ftHead, Ctx.AssignExtend ctRest ctHead) ->
+      Ctx.extend (zipWith proxy fun ftRest ctRest) (fun ftHead ctHead)
+
+zip ::
+  ArchOk arch =>
+  proxy arch ->
+  Ctx.Assignment f ctx ->
+  Ctx.Assignment g (MapToCrucibleType arch ctx) ->
+  Ctx.Assignment (Product f (CrucibleTypeCompat arch g)) ctx
+zip proxy = zipWith proxy (\ft ct -> Pair ft (CrucibleTypeCompat ct))
diff --git a/uc-crux-llvm/src/UCCrux/LLVM/FullType/FuncSig.hs b/uc-crux-llvm/src/UCCrux/LLVM/FullType/FuncSig.hs
@@ -23,23 +23,30 @@ module UCCrux.LLVM.FullType.FuncSig
     ReturnTypeToCrucibleType,
     ReturnTypeRepr (..),
     mkReturnTypeRepr,
+    ppReturnTypeRepr,
     -- * Function signatures
-    FuncSig,
+    type FuncSig(..),
     FuncSigRepr(..),
+    ppFuncSigRepr,
   )
 where
 
 {- ORMOLU_DISABLE -}
 import           Data.Kind (Type)
 
+import           Prettyprinter (Doc)
+import qualified Prettyprinter as PP
+
 import           Data.Parameterized.Classes (OrdF(compareF))
 import qualified Data.Parameterized.Context as Ctx
 import           Data.Parameterized.Some (Some(Some))
 import qualified Data.Parameterized.TH.GADT as U
+import           Data.Parameterized.TraversableFC (toListFC)
 import           Data.Type.Equality (TestEquality(testEquality))
 
 import qualified Lang.Crucible.Types as CrucibleTypes hiding ((::>))
 
+import           UCCrux.LLVM.FullType.PP (ppFullTypeRepr)
 import           UCCrux.LLVM.FullType.Type
 import           UCCrux.LLVM.FullType.VarArgs
 {- ORMOLU_ENABLE -}
@@ -63,6 +70,12 @@ mkReturnTypeRepr =
     Nothing -> Some VoidRepr
     Just (Some ftRepr) -> Some (NonVoidRepr ftRepr)
 
+ppReturnTypeRepr :: ReturnTypeRepr m mft -> Doc ann
+ppReturnTypeRepr =
+  \case
+    VoidRepr -> PP.pretty "void"
+    NonVoidRepr ft -> ppFullTypeRepr ft
+
 -- | Type-level only
 data FuncSig m where
   FuncSig ::
@@ -73,11 +86,21 @@ data FuncSig m where
 
 data FuncSigRepr m (fs :: FuncSig m) where
   FuncSigRepr ::
-    VarArgsRepr varArgs ->
-    Ctx.Assignment (FullTypeRepr m) args ->
-    ReturnTypeRepr m ret ->
+    { fsVarArgs :: VarArgsRepr varArgs,
+      fsArgTypes :: Ctx.Assignment (FullTypeRepr m) args,
+      fsRetType :: ReturnTypeRepr m ret
+    } ->
     FuncSigRepr m ('FuncSig varArgs ret args)
 
+ppFuncSigRepr :: FuncSigRepr m mft -> Doc ann
+ppFuncSigRepr (FuncSigRepr va args ret) =
+  PP.hsep
+    [ PP.hsep (PP.punctuate (PP.pretty " ->") (toListFC ppFullTypeRepr args))
+        <> if varArgsReprToBool va then PP.pretty "..." else mempty
+    , PP.pretty "->"
+    , ppReturnTypeRepr ret
+    ]
+
 -- ------------------------------------------------------------------------------
 -- Instances
 

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/FullType/MemType.hs b/uc-crux-llvm/src/UCCrux/LLVM/FullType/MemType.hs
@@ -1,6 +1,6 @@
 {-
 Module           : UCCrux.LLVM.FullType.MemType
-Description      : Interop between 'FullType' and 'MemType'
+Description      : Interop between 'FullType' and 'MemType' and 'SymType'
 Copyright        : (c) Galois, Inc 2021
 License          : BSD3
 Maintainer       : Langston Barrett <langston@galois.com>
@@ -14,6 +14,7 @@ Stability        : provisional
 
 module UCCrux.LLVM.FullType.MemType
   ( toMemType,
+    toSymType
   )
 where
 
@@ -27,7 +28,7 @@ import qualified What4.InterpretedFloatingPoint as W4IFP
 import           Lang.Crucible.LLVM.MemType (MemType(..), SymType(..), FunDecl(..))
 
 import           UCCrux.LLVM.Errors.Panic (panic)
-import           UCCrux.LLVM.FullType.Type (FullTypeRepr(..), aliasOrFullType)
+import           UCCrux.LLVM.FullType.Type (FullTypeRepr(..), PartTypeRepr, aliasOrFullType)
 import           UCCrux.LLVM.FullType.VarArgs (varArgsReprToBool)
 {- ORMOLU_ENABLE -}
 
@@ -38,10 +39,7 @@ toMemType :: FullTypeRepr m ft -> MemType
 toMemType =
   \case
     FTIntRepr natRepr -> IntType (natValue natRepr)
-    FTPtrRepr ptRepr ->
-      case aliasOrFullType ptRepr of
-        Left ident -> PtrType (Alias ident)
-        Right ftRepr -> PtrType (MemType (toMemType ftRepr))
+    FTPtrRepr ptRepr -> PtrType (toSymType ptRepr)
     FTFloatRepr W4IFP.SingleFloatRepr -> FloatType
     FTFloatRepr W4IFP.DoubleFloatRepr -> DoubleType
     FTFloatRepr W4IFP.X86_80FloatRepr -> X86_FP80Type
@@ -65,3 +63,9 @@ toMemType =
                 isVarArgs
             )
         )
+
+toSymType :: PartTypeRepr m ft -> SymType
+toSymType ptRepr =
+  case aliasOrFullType ptRepr of
+    Left ident -> Alias ident
+    Right ftRepr -> MemType (toMemType ftRepr)
diff --git a/uc-crux-llvm/src/UCCrux/LLVM/FullType/PP.hs b/uc-crux-llvm/src/UCCrux/LLVM/FullType/PP.hs
@@ -0,0 +1,27 @@
+{-
+Module           : UCCrux.LLVM.FullType.PP
+Description      : Pretty-printing 'FullTypeRepr'
+Copyright        : (c) Galois, Inc 2022
+License          : BSD3
+Maintainer       : Langston Barrett <langston@galois.com>
+Stability        : provisional
+-}
+
+module UCCrux.LLVM.FullType.PP
+  ( ppFullTypeRepr,
+    ppPartTypeRepr
+  )
+where
+
+import           Prettyprinter (Doc)
+
+import           Lang.Crucible.LLVM.MemType (ppMemType, ppSymType)
+
+import           UCCrux.LLVM.FullType.MemType (toMemType, toSymType)
+import           UCCrux.LLVM.FullType.Type (FullTypeRepr, PartTypeRepr)
+
+ppFullTypeRepr :: FullTypeRepr m ft -> Doc ann
+ppFullTypeRepr = ppMemType . toMemType
+
+ppPartTypeRepr :: PartTypeRepr m ft -> Doc ann
+ppPartTypeRepr = ppSymType . toSymType