Merge pull request #1925 from GaloisInc/T1859-mir_array_value

`mir_array_value`

crucible-mir-comp/src/Mir/Compositional/Builder.hs

@@ -685,14 +685,14 @@ regToSetup bak p eval shp rv = go shp rv
             msbPrePost p . seVars %= Set.insert (Some var)
         liftIO $ MS.SetupTerm <$> eval btpr expr
     go (TupleShape _ _ flds) rvs = MS.SetupStruct () <$> goFields flds rvs
-    go (ArrayShape _ _ shp) vec = do
+    go (ArrayShape _ elemTy shp) vec = do
         svs <- case vec of
             MirVector_Vector v -> mapM (go shp) (toList v)
             MirVector_PartialVector v -> forM (toList v) $ \p -> do
                 rv <- liftIO $ readMaybeType sym "vector element" (shapeType shp) p
                 go shp rv
             MirVector_Array _ -> error $ "regToSetup: MirVector_Array NYI"
-        return $ MS.SetupArray () svs
+        return $ MS.SetupArray elemTy svs
     go (StructShape _ _ flds) (AnyValue tpr rvs)
       | Just Refl <- testEquality tpr shpTpr =
         MS.SetupStruct () <$> goFields flds rvs

crucible-mir-comp/src/Mir/Compositional/Override.hs

@@ -391,7 +391,7 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
                             show (W4.printSymExpr val))
                         ""
     go (TupleShape _ _ flds) rvs (MS.SetupStruct () svs) = goFields flds rvs svs
-    go (ArrayShape _ _ shp) vec (MS.SetupArray () svs) = case vec of
+    go (ArrayShape _ _ shp) vec (MS.SetupArray _ svs) = case vec of
         MirVector_Vector v -> zipWithM_ (\x y -> go shp x y) (toList v) svs
         MirVector_PartialVector pv -> forM_ (zip (toList pv) svs) $ \(p, sv) -> do
             rv <- liftIO $ readMaybeType sym "vector element" (shapeType shp) p

doc/manual/manual.md

@@ -2621,6 +2621,13 @@ the value of an array element.
 * `jvm_field_is : JVMValue -> String -> JVMValue -> JVMSetup ()`
 specifies the name of an object field.
 
+In the experimental MIR verification implementation, the following functions
+construct compound values:
+
+* `mir_array_value : MIRType -> [SetupValue] -> SetupValue` constructs an array
+  of the given type whose elements consist of the given values. Supplying the
+  element type is necessary to support length-0 arrays.
+
 ### Bitfields
 
 SAW has experimental support for specifying `struct`s with bitfields, such as

intTests/test_mir_verify_arrays/Makefile

@@ -0,0 +1,13 @@
+all: test.linked-mir.json
+
+test.linked-mir.json: test.rs
+	saw-rustc $<
+	$(MAKE) remove-unused-build-artifacts
+
+.PHONY: remove-unused-build-artifacts
+remove-unused-build-artifacts:
+	rm -f test libtest.mir libtest.rlib
+
+.PHONY: clean
+clean: remove-unused-build-artifacts
+	rm -f test.linked-mir.json

intTests/test_mir_verify_arrays/test.rs

@@ -0,0 +1,16 @@
+pub fn f(x: [&u32; 2]) -> u32 {
+    x[0].wrapping_add(*x[1])
+}
+
+pub fn g(x: [&mut u32; 2]) {
+    *x[0] = 42;
+    *x[1] = x[1].wrapping_add(1);
+}
+
+pub fn h() -> [&'static u32; 2] {
+    [&27, &42]
+}
+
+pub fn i(_x: [u32; 0]) -> [u64; 0] {
+    []
+}

intTests/test_mir_verify_arrays/test.saw

@@ -0,0 +1,80 @@
+enable_experimental;
+
+let f_spec = do {
+  x0_ref <- mir_alloc mir_u32;
+  x0 <- mir_fresh_var "x0" mir_u32;
+  mir_points_to x0_ref (mir_term x0);
+
+  x1_ref <- mir_alloc mir_u32;
+  x1 <- mir_fresh_var "x1" mir_u32;
+  mir_points_to x1_ref (mir_term x1);
+
+  let x = mir_array_value (mir_ref mir_u32) [x0_ref, x1_ref];
+
+  mir_execute_func [x];
+
+  mir_return (mir_term {{ x0 + x1 }});
+};
+
+let g_spec = do {
+  x0_ref <- mir_alloc_mut mir_u32;
+
+  x1_ref <- mir_alloc_mut mir_u32;
+  x1 <- mir_fresh_var "x1" mir_u32;
+  mir_points_to x1_ref (mir_term x1);
+
+  let x = mir_array_value (mir_ref_mut mir_u32) [x0_ref, x1_ref];
+
+  mir_execute_func [x];
+
+  mir_points_to x0_ref (mir_term {{ 42 : [32] }});
+  mir_points_to x1_ref (mir_term {{ x1 + 1 }});
+};
+
+let h_spec = do {
+  mir_execute_func [];
+
+  x0_ref <- mir_alloc mir_u32;
+  mir_points_to x0_ref (mir_term {{ 27 : [32] }});
+
+  x1_ref <- mir_alloc mir_u32;
+  mir_points_to x1_ref (mir_term {{ 42 : [32] }});
+
+  let x = mir_array_value (mir_ref mir_u32) [x0_ref, x1_ref];
+  mir_return x;
+};
+
+let i_spec = do {
+  let x = mir_term {{ [] : [0][32] }};
+  mir_execute_func [x];
+
+  mir_return (mir_array_value mir_u64 []);
+};
+
+let i_spec_bad1 = do {
+  let x = mir_term {{ [42] : [1][32] }};
+  mir_execute_func [x];
+
+  mir_return (mir_array_value mir_u64 []);
+};
+
+let i_spec_bad2 = do {
+  let x = mir_term {{ [] : [0][32] }};
+  mir_execute_func [x];
+
+  mir_return (mir_array_value mir_u64 [mir_term {{ 42 : [64] }}]);
+};
+
+m <- mir_load_module "test.linked-mir.json";
+
+mir_verify m "test::f" [] false f_spec z3;
+mir_verify m "test::g" [] false g_spec z3;
+mir_verify m "test::h" [] false h_spec z3;
+mir_verify m "test::i" [] false i_spec z3;
+
+fails (
+  mir_verify m "test::i" [] false i_spec_bad1 z3
+);
+fails (
+  mir_verify m "test::i" [] false i_spec_bad2 z3
+);

intTests/test_mir_verify_arrays/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

saw-remote-api/CHANGELOG.md

@@ -13,6 +13,10 @@
   how SAW's MIR verification support works in general, see the `mir_*` commands
   documented in the [SAW
   manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md).
+* The API for `"array"` `setup value`s now has an `"element type"` field. For
+  LLVM verification, this field is optional. For MIR verification, this field
+  is required if the `"elements"` value is empty and optional if the
+  `"elements"` value is non-empty.
 
 ## 1.0.0 -- 2023-06-26
 

saw-remote-api/python/CHANGELOG.md

@@ -12,6 +12,9 @@
   For more information about how SAW's MIR verification support works in
   general, see the `mir_*` commands documented in the [SAW
   manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md).
+* The `array()` function now takes an additional `element_type` argument, which
+  defaults to `None`. If constructing a MIR array with no elements, then the
+  `element_type` must be specified. Otherwise, this argument is optional.
 
 ## 1.0.1 -- YYYY-MM-DD
 

saw-remote-api/python/saw_client/crucible.py

@@ -197,13 +197,23 @@ def to_json(self) -> JSON:
         return {'setup value': 'null'}
 
 class ArrayVal(SetupVal):
+    element_type : Union['LLVMType', 'JVMType', 'MIRType', None]
     elements : List[SetupVal]
 
-    def __init__(self, elements : List[SetupVal]) -> None:
+    def __init__(self,
+                 element_type : Union['LLVMType', 'JVMType', 'MIRType', None],
+                 elements : List[SetupVal]) -> None:
+        self.element_type = element_type
         self.elements = elements
 
     def to_json(self) -> JSON:
+        element_type_json: Optional[Any]
+        if self.element_type is None:
+            element_type_json = None
+        else:
+            element_type_json = self.element_type.to_json()
         return {'setup value': 'array',
+                'element type' : element_type_json,
                 'elements': [element.to_json() for element in self.elements]}
 
 name_regexp = re.compile('^(?P<prefix>.*[^0-9])?(?P<number>[0-9]+)?$')
@@ -668,16 +678,18 @@ def cry_f(s : str) -> CryptolTerm:
     """
     return CryptolTerm(to_cryptol_str_customf(s, frames=1))
 
-def array(*elements: SetupVal) -> SetupVal:
+def array(*elements: SetupVal, element_type: Union['LLVMType', 'JVMType', 'MIRType', None] = None) -> SetupVal:
     """Returns an array with the provided ``elements`` (i.e., an ``ArrayVal``).
+    If returning an empty MIR array, you are required to explicitly supply
+    an ``element_type``; otherwise, the ``element_type`` argument is optional.
 
-    N.B., one or more ``elements`` must be provided.""" # FIXME why? document this here when we figure it out.
-    if len(elements) == 0:
-        raise ValueError('An array must be constructed with one or more elements')
+    If returning an LLVM array, then one or more ``elements`` must be provided.""" # FIXME why? document this here when we figure it out.
+    if isinstance(element_type, LLVMType) and len(elements) == 0:
+        raise ValueError('An LLVM array must be constructed with one or more elements')
     for e in elements:
         if not isinstance(e, SetupVal):
             raise ValueError('array expected a SetupVal, but got {e!r}')
-    return ArrayVal(list(elements))
+    return ArrayVal(element_type, list(elements))
 
 def elem(base: SetupVal, index: int) -> SetupVal:
     """Returns the value of the array element at position ``index`` in ``base`` (i.e., an ``ElemVal``).

saw-remote-api/python/tests/saw/test-files/mir_arrays.rs

@@ -0,0 +1,16 @@
+pub fn f(x: [&u32; 2]) -> u32 {
+    x[0].wrapping_add(*x[1])
+}
+
+pub fn g(x: [&mut u32; 2]) {
+    *x[0] = 42;
+    *x[1] = x[1].wrapping_add(1);
+}
+
+pub fn h() -> [&'static u32; 2] {
+    [&27, &42]
+}
+
+pub fn i(_x: [u32; 0]) -> [u64; 0] {
+    []
+}

saw-remote-api/python/tests/saw/test_mir_arrays.py

@@ -0,0 +1,82 @@
+import unittest
+from pathlib import Path
+
+from saw_client import *
+from saw_client.crucible import array, cry, cry_f
+from saw_client.mir import Contract, FreshVar, MIRType, SetupVal, u32, u64, void
+
+
+def ref_to_fresh(c : Contract, ty : MIRType, name : Optional[str] = None,
+                 read_only : bool = False) -> Tuple[FreshVar, SetupVal]:
+    """Add to ``Contract`` ``c`` an allocation of a reference of type ``ty`` initialized to an unknown fresh value.
+    If ``read_only == True`` then the allocated memory is immutable.
+
+    :returns A fresh variable bound to the reference's initial value and the newly allocated reference. (The fresh
+             variable will be assigned ``name`` if provided/available.)"""
+    var = c.fresh_var(ty, name)
+    ptr = c.alloc(ty, points_to = var, read_only = read_only)
+    return (var, ptr)
+
+
+class FContract(Contract):
+    def specification(self) -> None:
+        (x0, x0_p) = ref_to_fresh(self, u32, "x0", read_only = True)
+        (x1, x1_p) = ref_to_fresh(self, u32, "x1", read_only = True)
+        x = array(x0_p, x1_p)
+
+        self.execute_func(x)
+
+        self.returns_f('{x0} + {x1}')
+
+
+class GContract(Contract):
+    def specification(self) -> None:
+        x0_p = self.alloc(u32)
+        (x1, x1_p) = ref_to_fresh(self, u32, "x1")
+        x = array(x0_p, x1_p)
+
+        self.execute_func(x)
+
+        self.points_to(x0_p, cry_f('42 : [32]'))
+        self.points_to(x1_p, cry_f('{x1} + 1'))
+        self.returns(void)
+
+
+class HContract(Contract):
+    def specification(self) -> None:
+        self.execute_func()
+
+        x0_ptr = self.alloc(u32, points_to = cry_f('27 : [32]'), read_only = True)
+        x1_ptr = self.alloc(u32, points_to = cry_f('42 : [32]'), read_only = True)
+        self.returns(array(x0_ptr, x1_ptr))
+
+
+class IContract(Contract):
+    def specification(self) -> None:
+        self.execute_func(cry_f('[] : [0][32]'))
+
+        self.returns(array(element_type = u64))
+
+
+class MIRArraysTest(unittest.TestCase):
+    def test_mir_points_to(self):
+        connect(reset_server=True)
+        if __name__ == "__main__": view(LogResults())
+        json_name = str(Path('tests', 'saw', 'test-files', 'mir_arrays.linked-mir.json'))
+        mod = mir_load_module(json_name)
+
+        f_result = mir_verify(mod, 'mir_arrays::f', FContract())
+        self.assertIs(f_result.is_success(), True)
+
+        g_result = mir_verify(mod, 'mir_arrays::g', GContract())
+        self.assertIs(g_result.is_success(), True)
+
+        h_result = mir_verify(mod, 'mir_arrays::h', HContract())
+        self.assertIs(h_result.is_success(), True)
+
+        i_result = mir_verify(mod, 'mir_arrays::i', IContract())
+        self.assertIs(i_result.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()

saw-remote-api/src/SAWServer.hs

@@ -106,7 +106,7 @@ instance Show SAWTask where
 
 data CrucibleSetupVal ty e
   = NullValue
-  | ArrayValue [CrucibleSetupVal ty e]
+  | ArrayValue (Maybe ty) [CrucibleSetupVal ty e]
   | TupleValue [CrucibleSetupVal ty e]
   -- | RecordValue [(String, CrucibleSetupVal e)]
   | FieldLValue (CrucibleSetupVal ty e) String

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

@@ -4,7 +4,7 @@
 module SAWServer.Data.SetupValue (CrucibleSetupVal) where
 
 import Control.Applicative
-import Data.Aeson (FromJSON(..), withObject, withText, (.:))
+import Data.Aeson (FromJSON(..), withObject, withText, (.:), (.:?))
 
 import SAWServer
 
@@ -47,7 +47,7 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cr
           TagNamedValue -> NamedValue <$> o .: "name"
           TagNullValue -> pure NullValue
           TagCryptol -> CryptolExpr <$> o .: "expression"
-          TagArrayValue -> ArrayValue <$> o .: "elements"
+          TagArrayValue -> ArrayValue <$> o .:? "element type" <*> o .: "elements"
           TagTupleValue -> TupleValue <$> o .: "elements"
           TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field"
           TagCastLValue -> CastLValue <$> o .: "base" <*> o .: "type"

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

@@ -180,7 +180,7 @@ compileJVMContract fileReader bic cenv0 c =
       resolve env n >>= \case Val x -> return x
     getSetupVal (_, cenv) (CryptolExpr expr) =
       MS.SetupTerm <$> getTypedTerm cenv expr
-    getSetupVal _ (ArrayValue _) =
+    getSetupVal _ (ArrayValue _ _) =
       JVMSetupM $ fail "Array setup values unsupported in JVM API."
     getSetupVal _ (TupleValue _) =
       JVMSetupM $ fail "Tuple setup values unsupported in JVM API."

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

@@ -176,7 +176,7 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
       CrucibleSetupVal JSONLLVMType (P.Expr P.PName) ->
       LLVMCrucibleSetupM (CMS.AllLLVM MS.SetupValue)
     getSetupVal _ NullValue = LLVMCrucibleSetupM $ return CMS.anySetupNull
-    getSetupVal env (ArrayValue elts) =
+    getSetupVal env (ArrayValue _ elts) =
       do elts' <- mapM (getSetupVal env) elts
          LLVMCrucibleSetupM $ return $ CMS.anySetupArray elts'
     getSetupVal env (TupleValue elts) =