Checksafety: soundly handle ArrayInit

CHANGELOG.md

@@ -59,8 +59,9 @@
   ([PR #313](https://github.com/jasmin-lang/jasmin/pull/313);
   fixes [#310](https://github.com/jasmin-lang/jasmin/issues/310)).
 
-- Fix to the safety checker
-  ([PR #315](https://github.com/jasmin-lang/jasmin/pull/315);
+- Fixes to the safety checker
+  ([PR #315](https://github.com/jasmin-lang/jasmin/pull/315),
+  ([PR #343](https://github.com/jasmin-lang/jasmin/pull/343);
   fixes [#314](https://github.com/jasmin-lang/jasmin/issues/314)).
 
 - Safety checker better handles integer shift operators

compiler/safety/fail/array_init.jazz

@@ -0,0 +1,10 @@
+export
+fn bad_read() -> reg u64 {
+  stack u64[2] t;
+  reg u64 r;
+  t[0] = 42;
+  t[1] = 33;
+  ArrayInit(t);
+  r = t[0];
+  return r;
+}

compiler/safety/success/parr_init.jazz

@@ -0,0 +1,47 @@
+export
+fn reg_arr_init() -> reg u64 {
+  reg u64 r;
+  reg u64[1] a;
+  ArrayInit(a);
+  a[0] = 1;
+  r = a[0];
+  return r;
+}
+
+export
+fn stack_arr_init() -> reg u64 {
+  reg u64 r;
+  stack u64[1] a;
+  ArrayInit(a);
+  a[0] = 1;
+  r = a[0];
+  return r;
+}
+
+export
+fn slice_arr_init() -> reg u64 {
+  reg u64 r;
+  stack u64[2] a;
+  reg ptr u64[1] s;
+  a[1] = 1;
+  s = a[0:1];
+  ArrayInit(s);
+  r = a[1];
+  return r;
+}
+
+export
+fn slices_arr_init(reg u64 b) -> reg u64 {
+  reg u64 r;
+  stack u64[4] a;
+  reg ptr u64[1] s;
+  if b >s 0 {
+    s = a[0:1];
+  } else {
+    s = a[1:1];
+  }
+  ArrayInit(s);
+  a[0] = 1;
+  r = a[0];
+  return r;
+}

compiler/src/safety/safetyAbsExpr.ml

@@ -1128,6 +1128,27 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
           (u8_blast_var ~blast_arrays:true eiv)
       ) a vevs  
 
+  (* The variables representing the contents of an array *)
+  let array_contents lhs_arr =
+    lhs_arr |> arr_full_range |> List.map (fun y -> Mlocal y)
+
+  (* The variables representing the contents of a slice *)
+  let slice_contents x ws n =
+    List.init (size_of_ws ws) (fun i -> Mlocal (AarraySlice (x, U8, n + i)))
+
+  let remove_array_contents_mv abs =
+    function
+    | Mlocal (Aarray x) -> array_contents x |> AbsDom.remove_vars abs
+    | Mlocal (AarraySlice (x, ws, n)) -> slice_contents x ws n |> AbsDom.remove_vars abs
+    | _ -> assert false
+
+  let abs_forget_array_contents abs mi lv =
+    match mvar_of_lvar abs mi lv with
+    | MLnone -> abs
+    | MLvar(_, mv) -> remove_array_contents_mv abs mv
+    | MLvars(_, mvs) -> List.fold_left remove_array_contents_mv abs mvs
+    | MLasub(_, _ms) -> failwith "Not implemented (explicit array init of a slice)"
+
   (* Array slice assignment. Does the numerical assignments.
      Remark: array elements do not need to be tracked in the point-to
      abstraction. *)
@@ -1139,12 +1160,7 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
       assign_slice_aux abs lhs rhs
 
     (* If any offset is unknown, we need to forget the array content. *)
-    | _, _ ->
-      let lhs_arr = lhs.ms_v in
-      let mvs = arr_full_range lhs_arr
-                |> List.map (fun y -> Mlocal y) in
-      AbsDom.forget_list abs mvs
-
+    | _, _ -> array_contents lhs.ms_v |> AbsDom.forget_list abs
 
   let omvar_is_offset = function
     | MLvar (_, MvarOffset _) -> true

compiler/src/safety/safetyAbsExpr.mli

@@ -74,7 +74,9 @@ module AbsExpr (AbsDom : SafetyInterfaces.AbsNumBoolType) : sig
     AbsDom.t -> 'a gty -> mvar -> minfo option -> expr -> AbsDom.t
 
   val a_init_mlv_no_array : mlvar -> AbsDom.t -> AbsDom.t
-
+
+  val abs_forget_array_contents : AbsDom.t -> minfo -> lval -> AbsDom.t
+
   val abs_assign : AbsDom.t -> ty -> mlvar -> expr -> AbsDom.t
 
   val abs_assign_opn :

compiler/src/safety/safetyInterpreter.ml

@@ -1600,6 +1600,10 @@ end = struct
         let cr = { ginstr with i_desc = Cassgn (lv, tag, Bty (U sz), er) } in
         aeval_if asmOp ginstr c [cl] [cr] state
 
+      | Cassgn (lv, _, _, Parr_init _) ->
+        let abs = AbsExpr.abs_forget_array_contents state.abs ginstr.i_info lv in
+        { state with abs }
+
       | Copn ([ lv ], _, Ocopy _, [ e ])
       | Cassgn (lv, _, _, e) ->
         let abs = AbsExpr.abs_assign