mir_array_value

This adds support for a `mir_array_value` function in the MIR backend, which
allows constructing array `SetupValue`s. This largely behaves like
`llvm_array_value`s in the LLVM backend, but with the following differences:

* Unlike in the LLVM backend, MIR arrays can have length 0. To account for this
  possibility, `mir_array_value` has a `MIRType` argument to ensure that SAW
  can always infer the type of the array, even if there are no element values
  from which to infer the type.

  Similarly, the SAW remote API's `array()` function now has an optional
  `element_type` kwarg that can be used to specify the element type in the
  event that there are no element values.
* Because only the MIR backend makes use of the element type, this is encoded
  in the `XSetupArray` extension field.

This checks off one box in #1859.

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

@@ -692,7 +692,7 @@ regToSetup bak p eval shp rv = go shp rv
                 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 (shapeMirTy shp) 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

@@ -2615,6 +2615,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 a `"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 `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) =