Merge pull request #981 from GaloisInc/lb/postcond

uc-crux-llvm: Specify function postconditions

uc-crux-llvm/.hlint.yaml

@@ -55,6 +55,7 @@
 - ignore: {name: "Eta reduce"}  # Can be more clear with explicit binding
 - ignore: {name: "Parse error"}  # we trust the compiler over HLint
 - ignore: {name: "Reduce duplication"}  # Too heuristic
+- ignore: {name: "Use const"}  # Naming parameters helps
 - ignore: {name: "Use section"}  # Too opinionated
 - ignore:  # "AppContext" should be extensible with more fields
     name: "Use newtype instead of data"

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

@@ -81,12 +81,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 -}
@@ -695,11 +695,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 =

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

@@ -28,6 +28,7 @@ module UCCrux.LLVM.Constraints
     -- * 'ConstrainedShape'
     ConstrainedShape (..),
     minimalConstrainedShape,
+    ppConstrainedShape,
   )
 where
 
@@ -175,3 +176,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 ann
+ppConstrainedShape =
+  Shape.ppShape (PP.vsep . map ppConstraint . getCompose) . getConstrainedShape

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"
 

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

@@ -18,6 +18,7 @@ Stability        : provisional
 
 module UCCrux.LLVM.FullType.CrucibleType
   ( toCrucibleType,
+    toCrucibleReturnType,
 
     -- * Assignments
     SomeIndex (..),
@@ -30,11 +31,24 @@ module UCCrux.LLVM.FullType.CrucibleType
     translateIndex,
     generateM,
     generate,
+    CrucibleTypeCompat(..),
+    zip,
+
+    -- * SameCrucibleType
+    SameCrucibleType,
+    sameCrucibleType,
+    makeSameCrucibleType,
+    sameCrucibleTypeRefl,
+    MapSameCrucibleType,
+    mapSameCrucibleType,
+    mapSameCrucibleTypeRefl,
+    testSameCrucibleType,
+    testMapSameCrucibleType,
   )
 where
 
 {- ORMOLU_DISABLE -}
-import           Prelude hiding (unzip)
+import           Prelude hiding (unzip, zip, zipWith)
 
 import           Data.Coerce (coerce)
 import           Data.Functor ((<&>))
@@ -78,6 +92,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,
@@ -251,3 +275,136 @@ generate ::
   ) ->
   Ctx.Assignment f (MapToCrucibleType arch fullTypes)
 generate proxy sz f = coerce (generateM proxy sz (\i1 i2 refl -> Identity (f i1 i2 refl)))
+
+-- | Re-index a type that is indexed by Crucible types to be indexed by
+-- 'FullType' instead. Useful when you want to maintain information about the
+-- compatibility between data over Crucible types and 'FullType', see 'zip'.
+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 an assignment over 'FullType' with a compatible assignment over
+-- Crucible types, maintaining the type-level correspondence via
+-- 'CrucibleTypeCompat'.
+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))
+
+-- ------------------------------------------------------------------------------
+-- SameCrucibleType
+
+-- | A proof that two 'FullType's map to the same Crucible type, in any
+-- architecture.
+newtype SameCrucibleType ft ft' =
+  SameCrucibleType
+    { getSameCrucibleType ::
+      forall proxy arch.
+      proxy arch ->
+      ToCrucibleType arch ft :~: ToCrucibleType arch ft'
+    }
+
+sameCrucibleType ::
+  SameCrucibleType ft ft' ->
+  proxy arch ->
+  ToCrucibleType arch ft :~: ToCrucibleType arch ft'
+sameCrucibleType (SameCrucibleType prf) arch = prf arch
+
+makeSameCrucibleType ::
+  (forall proxy arch. proxy arch -> ToCrucibleType arch ft :~: ToCrucibleType arch ft') ->
+  SameCrucibleType ft ft'
+makeSameCrucibleType = SameCrucibleType
+
+sameCrucibleTypeRefl :: SameCrucibleType ft ft
+sameCrucibleTypeRefl = SameCrucibleType (\_arch -> Refl)
+
+-- | A proof that two contexts of 'FullType's map to the same contexts of
+-- Crucible types, in any architecture.
+newtype MapSameCrucibleType ctx ctx' =
+  MapSameCrucibleType
+    { getMapSameCrucibleType ::
+      forall proxy arch.
+      proxy arch ->
+      MapToCrucibleType arch ctx :~: MapToCrucibleType arch ctx'
+    }
+
+mapSameCrucibleType ::
+  MapSameCrucibleType ctx ctx' ->
+  proxy arch ->
+  MapToCrucibleType arch ctx :~: MapToCrucibleType arch ctx'
+mapSameCrucibleType (MapSameCrucibleType prf) arch = prf arch
+
+mapSameCrucibleTypeRefl :: MapSameCrucibleType ctx ctx
+mapSameCrucibleTypeRefl = MapSameCrucibleType (\_arch -> Refl)
+
+testMapSameCrucibleType ::
+  Ctx.Assignment (FullTypeRepr m) ctx ->
+  Ctx.Assignment (FullTypeRepr m) ctx' ->
+  Maybe (MapSameCrucibleType ctx ctx')
+testMapSameCrucibleType a a' =
+  case (Ctx.viewAssign a, Ctx.viewAssign a') of
+    (Ctx.AssignEmpty, Ctx.AssignEmpty) ->
+      Just (MapSameCrucibleType (\_arch -> Refl))
+    (Ctx.AssignExtend rest hd, Ctx.AssignExtend rest' hd') ->
+      case (testSameCrucibleType hd hd', testMapSameCrucibleType rest rest') of
+        (Just prf1, Just prf2) ->
+          Just $ MapSameCrucibleType $ \arch ->
+            case (sameCrucibleType prf1 arch, mapSameCrucibleType prf2 arch) of
+              (Refl, Refl) -> Refl
+        _ -> Nothing
+    _ -> Nothing
+
+-- | Check if two 'FullTypeRepr's are the same up to pointers.
+testSameCrucibleType ::
+  FullTypeRepr m ft ->
+  FullTypeRepr m ft' ->
+  Maybe (SameCrucibleType ft ft')
+testSameCrucibleType ft ft' =
+  case (ft, ft') of
+    (FTIntRepr natRepr, FTIntRepr natRepr') ->
+      do Refl <- testEquality natRepr natRepr'
+         return (SameCrucibleType (\_arch -> Refl))
+    (FTPtrRepr{}, FTPtrRepr{}) -> Just (SameCrucibleType (\_arch -> Refl))
+    (FTFloatRepr fi, FTFloatRepr fi') ->
+      do Refl <- testEquality fi fi'
+         return (SameCrucibleType (\_arch -> Refl))
+    (FTVoidFuncPtrRepr{}, FTVoidFuncPtrRepr{}) ->
+      Just (SameCrucibleType (\_arch -> Refl))
+    (FTNonVoidFuncPtrRepr{}, FTNonVoidFuncPtrRepr{}) ->
+      Just (SameCrucibleType (\_arch -> Refl))
+    (FTOpaquePtrRepr nm, FTOpaquePtrRepr nm') ->
+      do Refl <- testEquality nm nm'
+         return (SameCrucibleType (\_arch -> Refl))
+    (FTArrayRepr natRepr itemRepr, FTArrayRepr natRepr' itemRepr') ->
+      do Refl <- testEquality natRepr natRepr'
+         subPrf <- testSameCrucibleType itemRepr itemRepr'
+         return $ SameCrucibleType $ \arch ->
+           case sameCrucibleType subPrf arch of
+             Refl -> Refl
+    (FTUnboundedArrayRepr itemRepr, FTUnboundedArrayRepr itemRepr') ->
+      do subPrf <- testSameCrucibleType itemRepr itemRepr'
+         return $ SameCrucibleType $ \arch ->
+           case sameCrucibleType subPrf arch of
+             Refl -> Refl
+    (FTStructRepr sp fields, FTStructRepr sp' fields') ->
+      do subPrf <- testMapSameCrucibleType fields fields'
+         Refl <- testEquality sp sp'
+         return $ SameCrucibleType $ \arch ->
+           case mapSameCrucibleType subPrf arch of
+             Refl -> Refl
+    _ -> Nothing

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
 

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

@@ -1,10 +1,15 @@
 {-
 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>
 Stability        : provisional
+
+These functions are in their own module (instead of in
+"UCCrux.LLVM.FullType.PP.Type") to ensure only a small amount of code has access
+to the constructors of 'PartTypeRepr', which can be used to violate its
+invariant.
 -}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -15,6 +20,7 @@ Stability        : provisional
 
 module UCCrux.LLVM.FullType.MemType
   ( toMemType,
+    toSymType
   )
 where
 
@@ -28,7 +34,7 @@ import qualified What4.InterpretedFloatingPoint as W4IFP
 import           Lang.Crucible.LLVM.MemType (MemType(..), SymType(..), FunDecl(..), mkStructInfo)
 
 import           UCCrux.LLVM.Errors.Panic (panic)
-import           UCCrux.LLVM.FullType.Type (FullTypeRepr(..), aliasOrFullType, DataLayout, crucibleDataLayout, structPackedReprToBool)
+import           UCCrux.LLVM.FullType.Type (FullTypeRepr(..), PartTypeRepr, aliasOrFullType, DataLayout, crucibleDataLayout, structPackedReprToBool)
 import           UCCrux.LLVM.FullType.VarArgs (varArgsReprToBool)
 {- ORMOLU_ENABLE -}
 
@@ -39,10 +45,7 @@ toMemType :: forall m ft. DataLayout m -> FullTypeRepr m ft -> MemType
 toMemType dl =
   \case
     FTIntRepr natRepr -> IntType (natValue natRepr)
-    FTPtrRepr ptRepr ->
-      case aliasOrFullType ptRepr of
-        Left ident -> PtrType (Alias ident)
-        Right ftRepr -> PtrType (MemType (toMemType dl ftRepr))
+    FTPtrRepr ptRepr -> PtrType (toSymType dl ptRepr)
     FTFloatRepr W4IFP.SingleFloatRepr -> FloatType
     FTFloatRepr W4IFP.DoubleFloatRepr -> DoubleType
     FTFloatRepr W4IFP.X86_80FloatRepr -> X86_FP80Type
@@ -74,3 +77,9 @@ toMemType dl =
                 isVarArgs
             )
         )
+
+toSymType :: DataLayout m -> PartTypeRepr m ft -> SymType
+toSymType dl ptRepr =
+  case aliasOrFullType ptRepr of
+    Left ident -> Alias ident
+    Right ftRepr -> MemType (toMemType dl ftRepr)