diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py index f17ae1057d..ea4c28ce0b 100644 --- a/saw-remote-api/python/saw_client/crucible.py +++ b/saw-remote-api/python/saw_client/crucible.py @@ -334,6 +334,7 @@ class Contract: __state : ContractState = 'pre' + __mutable_globals : List[str] __pre_state : State __post_state : State @@ -347,6 +348,7 @@ class Contract: __cached_json : Optional[Any] def __init__(self) -> None: + self.__mutable_globals = [] self.__pre_state = State(self) self.__post_state = State(self) self.__used_names = set() @@ -423,6 +425,12 @@ def alloc(self, type : Union['LLVMType', 'JVMType'], *, read_only : bool = False return a + def alloc_global(self, name: str) -> None: + """Declare that memory for the named mutable global should be allocated. + This is done implicitly for immutable globals. A pointer to the + allocated memory may be obtained using `global_var`.""" + self.__mutable_globals.append(name) + def points_to(self, pointer : SetupVal, target : SetupVal, *, check_target_type : Union[PointerType, 'LLVMType', 'JVMType', None] = PointerType(), condition : Optional[Condition] = None) -> None: @@ -546,7 +554,8 @@ def to_json(self) -> Any: raise Exception("forgot return") self.__cached_json = \ - {'pre vars': [v.to_init_json() for v in self.__pre_state.fresh], + {'mutable globals': self.__mutable_globals, + 'pre vars': [v.to_init_json() for v in self.__pre_state.fresh], 'pre conds': [c.to_json() for c in self.__pre_state.conditions], 'pre allocated': [a.to_init_json() for a in self.__pre_state.allocated], 'pre ghost values': [g.to_json() for g in self.__pre_state.ghost_values], diff --git a/saw-remote-api/python/tests/saw/test-files/global.bc b/saw-remote-api/python/tests/saw/test-files/global.bc new file mode 100644 index 0000000000..e410f41c69 Binary files /dev/null and b/saw-remote-api/python/tests/saw/test-files/global.bc differ diff --git a/saw-remote-api/python/tests/saw/test-files/global.c b/saw-remote-api/python/tests/saw/test-files/global.c new file mode 100644 index 0000000000..31a5334971 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/global.c @@ -0,0 +1,15 @@ +#include + +uint32_t g; + +void clear() { + g = 0; +} + +void set(uint32_t x) { + g = x; +} + +uint32_t get() { + return g; +} diff --git a/saw-remote-api/python/tests/saw/test_llvm_global_mutable.py b/saw-remote-api/python/tests/saw/test_llvm_global_mutable.py new file mode 100644 index 0000000000..a7653c36e9 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_llvm_global_mutable.py @@ -0,0 +1,40 @@ +from pathlib import Path +import unittest +from saw_client import * +from saw_client.llvm import Contract, cryptol, global_var, void, i32 + + +class ClearContract(Contract): + def specification(self): + self.alloc_global("g") + + self.execute_func() + + self.points_to(global_var("g"), cryptol("0 : [32]")) + self.returns(void) + +class SetContract(Contract): + def specification(self): + self.alloc_global("g") + x = self.fresh_var(i32, "x") + + self.execute_func(x) + + self.points_to(global_var("g"), x) + self.returns(void) + +class LLVMGlobalTest(unittest.TestCase): + def test_llvm_global(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults()) + bcname = str(Path('tests','saw','test-files', 'global.bc')) + mod = llvm_load_module(bcname) + + result = llvm_verify(mod, 'set', SetContract()) + self.assertIs(result.is_success(), True) + result = llvm_verify(mod, 'clear', ClearContract()) + self.assertIs(result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/python/tests/saw_low_level/test_llvm_assume.py b/saw-remote-api/python/tests/saw_low_level/test_llvm_assume.py index ff4c27a1e9..105bde0fb9 100644 --- a/saw-remote-api/python/tests/saw_low_level/test_llvm_assume.py +++ b/saw-remote-api/python/tests/saw_low_level/test_llvm_assume.py @@ -15,6 +15,7 @@ def test_llvm_assume(self): c.llvm_load_module('m', assume_bc).result() seven_contract = { + "mutable globals": [], "pre vars": [], "pre conds": [], "pre allocated": [], @@ -28,6 +29,7 @@ def test_llvm_assume(self): } addone_contract = { + "mutable globals": [], "pre vars": [], "pre conds": [], "pre allocated": [], diff --git a/saw-remote-api/python/tests/saw_low_level/test_salsa20_low_level.py b/saw-remote-api/python/tests/saw_low_level/test_salsa20_low_level.py index 60fec5d933..a22e8e2993 100755 --- a/saw-remote-api/python/tests/saw_low_level/test_salsa20_low_level.py +++ b/saw-remote-api/python/tests/saw_low_level/test_salsa20_low_level.py @@ -50,6 +50,7 @@ def test_salsa20(self): crypt_res = {"setup value": "Cryptol", "expression" : "Salsa20_encrypt (k, v, m)" } rotl_contract = { + "mutable globals": [], "pre vars": [ {"server name": "value", "name": "value", "type": i32.to_json()}, {"server name": "shift", "name": "shift", "type": i32.to_json()} @@ -66,6 +67,7 @@ def test_salsa20(self): } qr_contract = { + "mutable globals": [], "pre vars": [ {"server name": "y0", "name": "y0", "type": i32.to_json()}, {"server name": "y1", "name": "y1", "type": i32.to_json()}, @@ -108,6 +110,7 @@ def test_salsa20(self): def oneptr_update_contract(ty, res): return { + "mutable globals": [], "pre vars": [ {"server name": "y", "name": "y", "type": ty.to_json()} ], @@ -140,6 +143,7 @@ def oneptr_update_contract(ty, res): zero = {"setup value": "Cryptol", "expression" : "0 : [32]" } expand_contract = { + "mutable globals": [], "pre vars": [ {"server name": "k", "name": "k", "type": LLVMArrayType(i8, 32).to_json()}, {"server name": "n", "name": "n", "type": LLVMArrayType(i8, 16).to_json()} @@ -175,6 +179,7 @@ def oneptr_update_contract(ty, res): m = {"setup value": "Cryptol", "expression" : "m" } def crypt_contract(size : int): return { + "mutable globals": [], "pre vars": [ {"server name": "k", "name": "k", "type": LLVMArrayType(i8, 32).to_json()}, {"server name": "v", "name": "v", "type": LLVMArrayType(i8, 8).to_json()}, diff --git a/saw-remote-api/python/tests/saw_low_level/test_seven.py b/saw-remote-api/python/tests/saw_low_level/test_seven.py index 041ffd66b4..951138babd 100644 --- a/saw-remote-api/python/tests/saw_low_level/test_seven.py +++ b/saw-remote-api/python/tests/saw_low_level/test_seven.py @@ -13,6 +13,7 @@ def test_seven(self): c.llvm_load_module('m', seven_bc).result() contract = { + "mutable globals": [], "pre vars": [], "pre conds": [], "pre allocated": [], diff --git a/saw-remote-api/python/tests/saw_low_level/test_swap_low_level.py b/saw-remote-api/python/tests/saw_low_level/test_swap_low_level.py index 6c0891425f..474a5c7048 100644 --- a/saw-remote-api/python/tests/saw_low_level/test_swap_low_level.py +++ b/saw-remote-api/python/tests/saw_low_level/test_swap_low_level.py @@ -26,6 +26,7 @@ def test_swap(self): y = {"setup value": "Cryptol", "expression": "x" } contract = { + "mutable globals": [], "pre vars": [ {"server name": "x", "name": "x", "type": i32}, {"server name": "y", "name": "y", "type": i32} diff --git a/saw-remote-api/python/tests/saw_low_level/test_trivial.py b/saw-remote-api/python/tests/saw_low_level/test_trivial.py index 335b121041..d72e6322b3 100644 --- a/saw-remote-api/python/tests/saw_low_level/test_trivial.py +++ b/saw-remote-api/python/tests/saw_low_level/test_trivial.py @@ -18,6 +18,7 @@ def test_trivial(self): c.llvm_load_module('m', null_bc).result() contract = { + "mutable globals": [], "pre vars": [], "pre conds": [], "pre allocated": [], diff --git a/saw-remote-api/src/SAWServer/Data/Contract.hs b/saw-remote-api/src/SAWServer/Data/Contract.hs index d3647de328..e0418b865c 100644 --- a/saw-remote-api/src/SAWServer/Data/Contract.hs +++ b/saw-remote-api/src/SAWServer/Data/Contract.hs @@ -29,7 +29,8 @@ data ContractMode data Contract ty cryptolExpr = Contract - { preVars :: [ContractVar ty] + { mutableGlobals :: [Text] + , preVars :: [ContractVar ty] , preConds :: [cryptolExpr] , preAllocated :: [Allocated ty] , preGhostValues :: [GhostValue cryptolExpr] @@ -110,7 +111,8 @@ instance FromJSON ty => FromJSON (ContractVar ty) where instance (FromJSON ty, FromJSON e) => FromJSON (Contract ty e) where parseJSON = withObject "contract" $ \o -> - Contract <$> o .: "pre vars" + Contract <$> o .: "mutable globals" + <*> o .: "pre vars" <*> o .: "pre conds" <*> o .: "pre allocated" <*> o .:? "pre ghost values" .!= [] diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs index 893663d790..0161c8bc4e 100644 --- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs @@ -26,6 +26,7 @@ import Data.Aeson (FromJSON(..), withObject, (.:)) import Data.ByteString (ByteString) import Data.Map (Map) import qualified Data.Map as Map +import qualified Data.Text as T import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) @@ -34,6 +35,7 @@ import qualified SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) import SAWScript.Crucible.LLVM.Builtins ( llvm_alloc , llvm_alloc_aligned + , llvm_alloc_global , llvm_alloc_readonly , llvm_alloc_readonly_aligned , llvm_execute_func @@ -89,7 +91,8 @@ compileLLVMContract :: Contract JSONLLVMType (P.Expr P.PName) -> LLVMCrucibleSetupM () compileLLVMContract fileReader bic ghostEnv cenv0 c = - do allocsPre <- mapM setupAlloc (preAllocated c) + do mapM_ (llvm_alloc_global . T.unpack) (mutableGlobals c) + allocsPre <- mapM setupAlloc (preAllocated c) (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) mapM_ (\p -> getTypedTerm cenvPre p >>= llvm_precond) (preConds c) mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c)