Skip to content

Commit a946a91

Browse files
robdockinsrobdockins
committed
Add hooks to the SAW remote API for the new pointer cast operation.
The new form still needs to be piped through the Python client.
1 parent db5baec commit a946a91

File tree

5 files changed

+35
-27
lines changed

5 files changed

+35
-27
lines changed

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

+12-12
Original file line numberDiff line numberDiff line change
@@ -87,40 +87,40 @@ instance Show SAWTask where
8787
show (JVMSetup n) = "(JVMSetup" ++ show n ++ ")"
8888

8989

90-
data CrucibleSetupVal e
90+
data CrucibleSetupVal ty e
9191
= NullValue
92-
| ArrayValue [CrucibleSetupVal e]
93-
| TupleValue [CrucibleSetupVal e]
92+
| ArrayValue [CrucibleSetupVal ty e]
93+
| TupleValue [CrucibleSetupVal ty e]
9494
-- | RecordValue [(String, CrucibleSetupVal e)]
95-
| FieldLValue (CrucibleSetupVal e) String
96-
| ElementLValue (CrucibleSetupVal e) Int
95+
| FieldLValue (CrucibleSetupVal ty e) String
96+
| CastLValue (CrucibleSetupVal ty e) ty
97+
| ElementLValue (CrucibleSetupVal ty e) Int
9798
| GlobalInitializer String
9899
| GlobalLValue String
99100
| NamedValue ServerName
100101
| CryptolExpr e
101102
deriving stock (Foldable, Functor, Traversable)
102103

103104
data SetupStep ty
104-
= SetupReturn (CrucibleSetupVal CryptolAST) -- ^ The return value
105+
= SetupReturn (CrucibleSetupVal ty CryptolAST) -- ^ The return value
105106
| SetupFresh ServerName Text ty -- ^ Server name to save in, debug name, fresh variable type
106107
| SetupAlloc ServerName ty Bool (Maybe Int) -- ^ Server name to save in, type of allocation, mutability, alignment
107108
| SetupGhostValue ServerName Text CryptolAST -- ^ Variable, term
108-
| SetupPointsTo (CrucibleSetupVal CryptolAST)
109-
(CrucibleSetupVal CryptolAST)
109+
| SetupPointsTo (CrucibleSetupVal ty CryptolAST)
110+
(CrucibleSetupVal ty CryptolAST)
110111
(Maybe (CheckPointsToType ty))
111112
(Maybe CryptolAST)
112113
-- ^ The source, the target, the type to check the target,
113114
-- and the condition that must hold in order for the source to point to the target
114-
| SetupPointsToBitfield (CrucibleSetupVal CryptolAST)
115+
| SetupPointsToBitfield (CrucibleSetupVal ty CryptolAST)
115116
Text
116-
(CrucibleSetupVal CryptolAST)
117+
(CrucibleSetupVal ty CryptolAST)
117118
-- ^ The source bitfield,
118119
-- the name of the field within the bitfield,
119120
-- and the target.
120-
| SetupExecuteFunction [CrucibleSetupVal CryptolAST] -- ^ Function's arguments
121+
| SetupExecuteFunction [CrucibleSetupVal ty CryptolAST] -- ^ Function's arguments
121122
| SetupPrecond CryptolAST -- ^ Function's precondition
122123
| SetupPostcond CryptolAST -- ^ Function's postcondition
123-
deriving stock (Foldable, Functor, Traversable)
124124

125125
instance Show (SetupStep ty) where
126126
show _ = "⟨SetupStep⟩" -- TODO

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

+10-10
Original file line numberDiff line numberDiff line change
@@ -35,15 +35,15 @@ data Contract ty cryptolExpr =
3535
, preAllocated :: [Allocated ty]
3636
, preGhostValues :: [GhostValue cryptolExpr]
3737
, prePointsTos :: [PointsTo ty cryptolExpr]
38-
, prePointsToBitfields :: [PointsToBitfield cryptolExpr]
39-
, argumentVals :: [CrucibleSetupVal cryptolExpr]
38+
, prePointsToBitfields :: [PointsToBitfield ty cryptolExpr]
39+
, argumentVals :: [CrucibleSetupVal ty cryptolExpr]
4040
, postVars :: [ContractVar ty]
4141
, postConds :: [cryptolExpr]
4242
, postAllocated :: [Allocated ty]
4343
, postGhostValues :: [GhostValue cryptolExpr]
4444
, postPointsTos :: [PointsTo ty cryptolExpr]
45-
, postPointsToBitfields :: [PointsToBitfield cryptolExpr]
46-
, returnVal :: Maybe (CrucibleSetupVal cryptolExpr)
45+
, postPointsToBitfields :: [PointsToBitfield ty cryptolExpr]
46+
, returnVal :: Maybe (CrucibleSetupVal ty cryptolExpr)
4747
}
4848
deriving stock (Functor, Foldable, Traversable)
4949

@@ -64,17 +64,17 @@ data Allocated ty =
6464

6565
data PointsTo ty cryptolExpr =
6666
PointsTo
67-
{ pointer :: CrucibleSetupVal cryptolExpr
68-
, pointsTo :: CrucibleSetupVal cryptolExpr
67+
{ pointer :: CrucibleSetupVal ty cryptolExpr
68+
, pointsTo :: CrucibleSetupVal ty cryptolExpr
6969
, checkPointsToType :: Maybe (CheckPointsToType ty)
7070
, condition :: Maybe cryptolExpr
7171
} deriving stock (Functor, Foldable, Traversable)
7272

73-
data PointsToBitfield cryptolExpr =
73+
data PointsToBitfield ty cryptolExpr =
7474
PointsToBitfield
75-
{ bfPointer :: CrucibleSetupVal cryptolExpr
75+
{ bfPointer :: CrucibleSetupVal ty cryptolExpr
7676
, bfFieldName :: Text
77-
, bfPointsTo :: CrucibleSetupVal cryptolExpr
77+
, bfPointsTo :: CrucibleSetupVal ty cryptolExpr
7878
} deriving stock (Functor, Foldable, Traversable)
7979

8080
data CheckAgainstTag
@@ -96,7 +96,7 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (PointsTo ty cryptolExp
9696
<*> o .:? "check points to type"
9797
<*> o .:? "condition"
9898

99-
instance FromJSON cryptolExpr => FromJSON (PointsToBitfield cryptolExpr) where
99+
instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (PointsToBitfield ty cryptolExpr) where
100100
parseJSON =
101101
withObject "Points-to-bitfield relationship" $ \o ->
102102
PointsToBitfield <$> o .: "pointer"

‎saw-remote-api/src/SAWServer/Data/SetupValue.hs

+4-1
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ data SetupValTag
1515
| TagArrayValue
1616
| TagTupleValue
1717
| TagFieldLValue
18+
| TagCastLValue
1819
| TagElemLValue
1920
| TagGlobalInit
2021
| TagGlobalLValue
@@ -29,12 +30,13 @@ instance FromJSON SetupValTag where
2930
"array" -> pure TagArrayValue
3031
"tuple" -> pure TagTupleValue
3132
"field" -> pure TagFieldLValue
33+
"cast" -> pure TagCastLValue
3234
"element lvalue" -> pure TagElemLValue
3335
"global initializer" -> pure TagGlobalInit
3436
"global lvalue" -> pure TagGlobalLValue
3537
_ -> empty
3638

37-
instance FromJSON cryptolExpr => FromJSON (CrucibleSetupVal cryptolExpr) where
39+
instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cryptolExpr) where
3840
parseJSON v = fromObject v
3941
where
4042
fromObject = withObject "saved value or Cryptol expression" $ \o ->
@@ -46,6 +48,7 @@ instance FromJSON cryptolExpr => FromJSON (CrucibleSetupVal cryptolExpr) where
4648
TagArrayValue -> ArrayValue <$> o .: "elements"
4749
TagTupleValue -> TupleValue <$> o .: "elements"
4850
TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field"
51+
TagCastLValue -> CastLValue <$> o .: "base" <*> o .: "type"
4952
TagElemLValue -> ElementLValue <$> o .: "base" <*> o .: "index"
5053
TagGlobalInit -> GlobalInitializer <$> o .: "name"
5154
TagGlobalLValue -> GlobalLValue <$> o .: "name"

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

+4-2
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,7 @@ compileJVMContract fileReader bic cenv0 c =
145145
GlobalLValue name -> jvm_static_field_is name sv
146146
_ -> JVMSetupM $ fail "Invalid points-to statement."
147147

148-
setupPointsToBitfields :: PointsToBitfield (P.Expr P.PName) -> JVMSetupM ()
148+
setupPointsToBitfields :: PointsToBitfield JavaType (P.Expr P.PName) -> JVMSetupM ()
149149
setupPointsToBitfields _ =
150150
JVMSetupM $ fail "Points-to-bitfield not supported in JVM API."
151151

@@ -173,7 +173,7 @@ compileJVMContract fileReader bic cenv0 c =
173173

174174
getSetupVal ::
175175
(Map ServerName ServerSetupVal, CryptolEnv) ->
176-
CrucibleSetupVal (P.Expr P.PName) ->
176+
CrucibleSetupVal JavaType (P.Expr P.PName) ->
177177
JVMSetupM (MS.SetupValue CJ.JVM)
178178
getSetupVal _ NullValue = JVMSetupM $ return (MS.SetupNull ())
179179
getSetupVal (env, _) (NamedValue n) =
@@ -186,6 +186,8 @@ compileJVMContract fileReader bic cenv0 c =
186186
JVMSetupM $ fail "Tuple setup values unsupported in JVM API."
187187
getSetupVal _ (FieldLValue _ _) =
188188
JVMSetupM $ fail "Field l-values unsupported in JVM API."
189+
getSetupVal _ (CastLValue _ _) =
190+
JVMSetupM $ fail "Cast l-values unsupported in JVM API."
189191
getSetupVal _ (ElementLValue _ _) =
190192
JVMSetupM $ fail "Element l-values unsupported in JVM API."
191193
getSetupVal _ (GlobalInitializer _) =

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

+5-2
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
138138

139139
setupPointsToBitfield ::
140140
(Map ServerName ServerSetupVal, CryptolEnv) ->
141-
PointsToBitfield (P.Expr P.PName) ->
141+
PointsToBitfield JSONLLVMType (P.Expr P.PName) ->
142142
LLVMCrucibleSetupM ()
143143
setupPointsToBitfield env (PointsToBitfield p fieldName v) =
144144
do ptr <- getSetupVal env p
@@ -173,7 +173,7 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
173173

174174
getSetupVal ::
175175
(Map ServerName ServerSetupVal, CryptolEnv) ->
176-
CrucibleSetupVal (P.Expr P.PName) ->
176+
CrucibleSetupVal JSONLLVMType (P.Expr P.PName) ->
177177
LLVMCrucibleSetupM (CMS.AllLLVM MS.SetupValue)
178178
getSetupVal _ NullValue = LLVMCrucibleSetupM $ return CMS.anySetupNull
179179
getSetupVal env (ArrayValue elts) =
@@ -185,6 +185,9 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
185185
getSetupVal env (FieldLValue base fld) =
186186
do base' <- getSetupVal env base
187187
LLVMCrucibleSetupM $ return $ CMS.anySetupField base' fld
188+
getSetupVal env (CastLValue base ty) =
189+
do base' <- getSetupVal env base
190+
LLVMCrucibleSetupM $ return $ CMS.anySetupCast base' (llvmType ty)
188191
getSetupVal env (ElementLValue base idx) =
189192
do base' <- getSetupVal env base
190193
LLVMCrucibleSetupM $ return $ CMS.anySetupElem base' idx

0 commit comments

Comments
 (0)