Merge pull request #1082 from GaloisInc/remote-llvm_points_to

saw-remote-api: Support more llvm_points_to features

saw-remote-api/docs/SAW.rst

@@ -208,12 +208,26 @@ these specifications are represented by a JSON object with the following fields:
 
 ``pre points to``
   A list of 'points-to' relationships in the initial state section of the specification. These
-  relationships are captured in a JSON object containing two fields:
+  relationships are captured in a JSON object containing four fields, two of which are optional:
 
 .. _points-to:
 
   - ``pointer``: A :ref:`Crucible Setup value<setup-values>` representing the pointer.
   - ``points to``: A :ref:`Crucible Setup value<setup-values>` representing the referent of ``pointer``.
+  - ``check points to type``: An optional description of a type to check the ``points to`` value against.
+    If the description is ``null``, then this has no effect. The description is represented as a JSON
+    object containing a tag named ``check against``, with any further fields determined by this tag.
+    These tag values can be:
+
+    + ``pointer type``: Check the type of the ``points to`` value against the type that the ``pointer``
+      value's type points to.
+    + ``casted type``: Check the type of the ``points to`` value against the provided type. There is
+      an additional field ``type``, which contains the :ref:`LLVM<llvm-types>` or :ref:`JVM<jvm-types>`
+      type to check against.
+
+  - ``condition``: An optional condition, represented as a :ref:`Cryptol term<cryptol-json-expression>`.
+    If the ``condition`` is not ``null``, then the ``pointer`` value will only point to the ``points to``
+    value if the ``condition`` holds.
 
 ``argument vals``
   A list of :ref:`Crucible Setup values<setup-values>` representing the arguments to the function being verified.

saw-remote-api/src/SAWServer.hs

@@ -46,6 +46,7 @@ import Verifier.SAW.TypedTerm (TypedTerm, CryptolModule)
 
 
 import qualified SAWScript.Crucible.Common.MethodSpec as CMS (CrucibleMethodSpecIR)
+import SAWScript.Crucible.LLVM.Builtins (CheckPointsToType)
 import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (SomeLLVM, LLVMModule)
 import SAWScript.JavaExpr (JavaType(..))
 import SAWScript.Options (defaultOptions)
@@ -94,10 +95,16 @@ data SetupStep ty
   = SetupReturn (CrucibleSetupVal CryptolAST) -- ^ The return value
   | SetupFresh ServerName Text ty -- ^ Server name to save in, debug name, fresh variable type
   | SetupAlloc ServerName ty Bool (Maybe Int) -- ^ Server name to save in, type of allocation, mutability, alignment
-  | SetupPointsTo (CrucibleSetupVal CryptolAST) (CrucibleSetupVal CryptolAST) -- ^ Source, target
+  | SetupPointsTo (CrucibleSetupVal CryptolAST)
+                  (CrucibleSetupVal CryptolAST)
+                  (Maybe (CheckPointsToType ty))
+                  (Maybe CryptolAST)
+                  -- ^ The source, the target, the type to check the target,
+                  --   and the condition that must hold in order for the source to point to the target
   | SetupExecuteFunction [CrucibleSetupVal CryptolAST] -- ^ Function's arguments
   | SetupPrecond CryptolAST -- ^ Function's precondition
   | SetupPostcond CryptolAST -- ^ Function's postcondition
+  deriving stock (Foldable, Functor, Traversable)
 
 instance Show (SetupStep ty) where
   show _ = "⟨SetupStep⟩" -- TODO

saw-remote-api/src/SAWServer/Data/Contract.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 module SAWServer.Data.Contract
   ( ContractMode(..)
@@ -11,8 +12,11 @@ module SAWServer.Data.Contract
   , PointsTo(..)
   ) where
 
-import Data.Aeson (FromJSON(..), withObject, (.:))
-import Data.Text
+import Control.Applicative
+import Data.Aeson (FromJSON(..), withObject, withText, (.:))
+import Data.Text (Text)
+
+import SAWScript.Crucible.LLVM.Builtins (CheckPointsToType(..))
 
 import SAWServer
 import SAWServer.Data.SetupValue ()
@@ -27,12 +31,12 @@ data Contract ty cryptolExpr =
     { preVars       :: [ContractVar ty]
     , preConds      :: [cryptolExpr]
     , preAllocated  :: [Allocated ty]
-    , prePointsTos  :: [PointsTo cryptolExpr]
+    , prePointsTos  :: [PointsTo ty cryptolExpr]
     , argumentVals  :: [CrucibleSetupVal cryptolExpr]
     , postVars      :: [ContractVar ty]
     , postConds     :: [cryptolExpr]
     , postAllocated :: [Allocated ty]
-    , postPointsTos :: [PointsTo cryptolExpr]
+    , postPointsTos :: [PointsTo ty cryptolExpr]
     , returnVal     :: Maybe (CrucibleSetupVal cryptolExpr)
     }
     deriving stock (Functor, Foldable, Traversable)
@@ -52,17 +56,25 @@ data Allocated ty =
     , allocatedAlignment  :: Maybe Int
     }
 
-data PointsTo cryptolExpr =
+data PointsTo ty cryptolExpr =
   PointsTo
-    { pointer  :: CrucibleSetupVal cryptolExpr
-    , pointsTo :: CrucibleSetupVal cryptolExpr
+    { pointer           :: CrucibleSetupVal cryptolExpr
+    , pointsTo          :: CrucibleSetupVal cryptolExpr
+    , checkPointsToType :: Maybe (CheckPointsToType ty)
+    , condition         :: Maybe cryptolExpr
     } deriving stock (Functor, Foldable, Traversable)
 
-instance FromJSON cryptolExpr => FromJSON (PointsTo cryptolExpr) where
+data CheckAgainstTag
+  = TagCheckAgainstPointerType
+  | TagCheckAgainstCastedType
+
+instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (PointsTo ty cryptolExpr) where
   parseJSON =
     withObject "Points-to relationship" $ \o ->
       PointsTo <$> o .: "pointer"
                <*> o .: "points to"
+               <*> o .: "check points to type"
+               <*> o .: "condition"
 
 instance FromJSON ty => FromJSON (Allocated ty) where
   parseJSON =
@@ -92,3 +104,19 @@ instance (FromJSON ty, FromJSON e) => FromJSON (Contract ty e) where
              <*> o .: "post allocated"
              <*> o .: "post points tos"
              <*> o .: "return val"
+
+instance FromJSON CheckAgainstTag where
+  parseJSON =
+    withText "`check points to type` tag" $
+    \case
+      "pointer type" -> pure TagCheckAgainstPointerType
+      "casted type"  -> pure TagCheckAgainstCastedType
+      _ -> empty
+
+instance FromJSON ty => FromJSON (CheckPointsToType ty) where
+  parseJSON =
+    withObject "check points to type" $ \o ->
+      o .: "check against" >>=
+      \case
+        TagCheckAgainstPointerType -> pure CheckAgainstPointerType
+        TagCheckAgainstCastedType  -> CheckAgainstCastedType <$> o .: "type"

saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs

@@ -82,12 +82,12 @@ compileJVMContract fileReader bic cenv c = interpretJVMSetup fileReader bic cenv
       map setupFresh (preVars c) ++
       map SetupPrecond (preConds c) ++
       map setupAlloc (preAllocated c) ++
-      map (\(PointsTo p v) -> SetupPointsTo p v) (prePointsTos c) ++
+      map (\(PointsTo p v chkV cond) -> SetupPointsTo p v chkV cond) (prePointsTos c) ++
       [ SetupExecuteFunction (argumentVals c) ] ++
       map setupFresh (postVars c) ++
       map SetupPostcond (postConds c) ++
       map setupAlloc (postAllocated c) ++
-      map (\(PointsTo p v) -> SetupPointsTo p v) (postPointsTos c) ++
+      map (\(PointsTo p v chkV cond) -> SetupPointsTo p v chkV cond) (postPointsTos c) ++
       [ SetupReturn v | v <- maybeToList (returnVal c) ]
 
 interpretJVMSetup ::
@@ -113,7 +113,7 @@ interpretJVMSetup fileReader bic cenv0 ss = runStateT (traverse_ go ss) (mempty,
       lift (jvm_alloc_object c) >>= save name . Val
     go (SetupAlloc _ ty _ Nothing) =
       error $ "cannot allocate type: " ++ show ty
-    go (SetupPointsTo src tgt) = get >>= \env -> lift $
+    go (SetupPointsTo src tgt _chkTgt _cond) = get >>= \env -> lift $
       do _ptr <- getSetupVal env src
          _tgt' <- getSetupVal env tgt
          error "nyi: points-to"

saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs

@@ -41,7 +41,7 @@ import SAWScript.Crucible.LLVM.Builtins
     , llvm_alloc_readonly_aligned
     , llvm_execute_func
     , llvm_fresh_var
-    , llvm_points_to
+    , llvm_points_to_internal
     , llvm_return
     , llvm_precond
     , llvm_postcond )
@@ -53,7 +53,7 @@ import Verifier.SAW.TypedTerm (TypedTerm)
 
 import Argo
 import qualified Argo.Doc as Doc
-import SAWServer
+import SAWServer as Server
 import SAWServer.Data.Contract
 import SAWServer.Data.LLVMType (JSONLLVMType, llvmType)
 import SAWServer.Data.SetupValue ()
@@ -93,12 +93,12 @@ compileLLVMContract fileReader bic cenv c =
       map setupFresh (preVars c) ++
       map SetupPrecond (preConds c) ++
       map setupAlloc (preAllocated c) ++
-      map (\(PointsTo p v) -> SetupPointsTo p v) (prePointsTos c) ++
+      map (\(PointsTo p v chkV cond) -> SetupPointsTo p v (fmap (fmap llvmType) chkV) cond) (prePointsTos c) ++
       [ SetupExecuteFunction (argumentVals c) ] ++
       map setupFresh (postVars c) ++
       map SetupPostcond (postConds c) ++
       map setupAlloc (postAllocated c) ++
-      map (\(PointsTo p v) -> SetupPointsTo p v) (postPointsTos c) ++
+      map (\(PointsTo p v chkV cond) -> SetupPointsTo p v (fmap (fmap llvmType) chkV) cond) (postPointsTos c) ++
       [ SetupReturn v | v <- maybeToList (returnVal c) ]
 
 interpretLLVMSetup ::
@@ -125,10 +125,11 @@ interpretLLVMSetup fileReader bic cenv0 ss =
       lift (llvm_alloc_aligned align ty) >>= save name . Val
     go (SetupAlloc name ty False (Just align)) =
       lift (llvm_alloc_readonly_aligned align ty) >>= save name . Val
-    go (SetupPointsTo src tgt) = get >>= \env -> lift $
+    go (SetupPointsTo src tgt chkTgt cond) = get >>= \env -> lift $
       do ptr <- getSetupVal env src
          tgt' <- getSetupVal env tgt
-         llvm_points_to True ptr tgt'
+         cond' <- traverse (getTypedTerm env) cond
+         llvm_points_to_internal chkTgt cond' ptr tgt'
     go (SetupExecuteFunction args) =
       get >>= \env ->
       lift $ traverse (getSetupVal env) args >>= llvm_execute_func

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -11,6 +11,7 @@ Stability   : provisional
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ParallelListComp #-}
@@ -40,10 +41,12 @@ module SAWScript.Crucible.LLVM.Builtins
     , llvm_ghost_value
     , llvm_declare_ghost_state
     , llvm_equal
+    , CheckPointsToType(..)
     , llvm_points_to
     , llvm_conditional_points_to
     , llvm_points_to_at_type
     , llvm_conditional_points_to_at_type
+    , llvm_points_to_internal
     , llvm_points_to_array_prefix
     , llvm_fresh_pointer
     , llvm_unsafe_assume_spec
@@ -1989,7 +1992,7 @@ llvm_points_to ::
   AllLLVM SetupValue     ->
   LLVMCrucibleSetupM ()
 llvm_points_to typed =
-  llvm_points_to_internal typed Nothing Nothing
+  llvm_points_to_internal (shouldCheckAgainstPointerType typed) Nothing
 
 llvm_conditional_points_to ::
   Bool {- ^ whether to check type compatibility -} ->
@@ -1998,15 +2001,15 @@ llvm_conditional_points_to ::
   AllLLVM SetupValue ->
   LLVMCrucibleSetupM ()
 llvm_conditional_points_to typed cond =
-  llvm_points_to_internal typed Nothing (Just cond)
+  llvm_points_to_internal (shouldCheckAgainstPointerType typed) (Just cond)
 
 llvm_points_to_at_type ::
   AllLLVM SetupValue ->
   L.Type             ->
   AllLLVM SetupValue ->
   LLVMCrucibleSetupM ()
 llvm_points_to_at_type ptr ty val =
-  llvm_points_to_internal False (Just ty) Nothing ptr val
+  llvm_points_to_internal (Just (CheckAgainstCastedType ty)) Nothing ptr val
 
 llvm_conditional_points_to_at_type ::
   TypedTerm ->
@@ -2015,16 +2018,35 @@ llvm_conditional_points_to_at_type ::
   AllLLVM SetupValue ->
   LLVMCrucibleSetupM ()
 llvm_conditional_points_to_at_type cond ptr ty val =
-  llvm_points_to_internal False (Just ty) (Just cond) ptr val
+  llvm_points_to_internal (Just (CheckAgainstCastedType ty)) (Just cond) ptr val
+
+-- | When invoking @llvm_points_to@ and friends, against what should SAW check
+-- the type of the RHS value?
+data CheckPointsToType ty
+  = CheckAgainstPointerType
+    -- ^ Check the type of the RHS value against the type that the LHS points to.
+    --   Used for @llvm_{conditional_}points_to@.
+  | CheckAgainstCastedType ty
+    -- ^ Check the type of the RHS value against the provided @ty@, which
+    --   the LHS pointer is casted to.
+    --   Used for @llvm_{conditional_}points_to_at_type@.
+  deriving (Functor, Foldable, Traversable)
+
+-- | If the argument is @True@, check the type of the RHS value against the
+-- type that the LHS points to (i.e., @'Just' 'CheckAgainstPointerType'@).
+-- Otherwise, don't check the type of the RHS value at all (i.e., 'Nothing').
+shouldCheckAgainstPointerType :: Bool -> Maybe (CheckPointsToType ty)
+shouldCheckAgainstPointerType b = if b then Just CheckAgainstPointerType else Nothing
 
 llvm_points_to_internal ::
-  Bool {- ^ whether to check type compatibility -} ->
-  Maybe L.Type {- ^ optional type constraint for rhs -} ->
+  Maybe (CheckPointsToType L.Type) {- ^ If 'Just', check the type of the RHS value.
+                                        If 'Nothing', don't check the type of the
+                                        RHS value at all. -} ->
   Maybe TypedTerm ->
   AllLLVM SetupValue {- ^ lhs pointer -} ->
   AllLLVM SetupValue {- ^ rhs value -} ->
   LLVMCrucibleSetupM ()
-llvm_points_to_internal typed rhsTy cond (getAllLLVM -> ptr) (getAllLLVM -> val) =
+llvm_points_to_internal mbCheckType cond (getAllLLVM -> ptr) (getAllLLVM -> val) =
   LLVMCrucibleSetupM $
   do cc <- getLLVMCrucibleContext
      loc <- getW4Position "llvm_points_to"
@@ -2051,13 +2073,13 @@ llvm_points_to_internal typed rhsTy cond (getAllLLVM -> ptr) (getAllLLVM -> val)
             _ -> throwCrucibleSetup loc $ "lhs not a pointer type: " ++ show ptrTy
 
           valTy <- typeOfSetupValue cc env nameEnv val
-          case rhsTy of
-            Nothing -> pure ()
-            Just ty ->
-              do ty' <- memTypeForLLVMType loc ty
-                 checkMemTypeCompatibility loc ty' valTy
+          case mbCheckType of
+            Nothing                          -> pure ()
+            Just CheckAgainstPointerType     -> checkMemTypeCompatibility loc lhsTy valTy
+            Just (CheckAgainstCastedType ty) -> do
+              ty' <- memTypeForLLVMType loc ty
+              checkMemTypeCompatibility loc ty' valTy
 
-          when typed (checkMemTypeCompatibility loc lhsTy valTy)
           Setup.addPointsTo (LLVMPointsTo loc cond ptr $ ConcreteSizeValue val)
 
 llvm_points_to_array_prefix ::