feat(rpc): python llvm_alloc_global equiv (alloc_global)

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],

saw-remote-api/python/tests/saw/test-files/global.c

@@ -0,0 +1,15 @@
+#include <stdint.h>
+
+uint32_t g;
+
+void clear() {
+    g = 0;
+}
+
+void set(uint32_t x) {
+    g = x;
+}
+
+uint32_t get() {
+    return g;
+}

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()

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": [],

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()},

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": [],

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}

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": [],

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" .!= []

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)