checksafety: add support for #randombytes

CHANGELOG.md

@@ -32,8 +32,9 @@
   ([PR #303](https://github.com/jasmin-lang/jasmin/pull/303);
   fixes [#301](https://github.com/jasmin-lang/jasmin/issues/301)).
 
-- Safety checker handles the `#copy` operator
-  ([PR #312](https://github.com/jasmin-lang/jasmin/pull/312);
+- Safety checker handles the `#copy` and `#randombytes` operators
+  ([PR #312](https://github.com/jasmin-lang/jasmin/pull/312),
+  [PR #317](https://github.com/jasmin-lang/jasmin/pull/317);
   fixes [#308](https://github.com/jasmin-lang/jasmin/issues/308)).
 
 ## Other changes

compiler/safety/success/randombytes.jazz

@@ -0,0 +1,15 @@
+export fn test1() -> reg u64 {
+  stack u64[1] r;
+  reg u64 x;
+  r = #randombytes(r);
+  x = r[0];
+  return x;
+}
+
+export fn test2() -> reg u64 {
+  stack u64[2] r;
+  reg u64 x;
+  r[1:1] = #randombytes(r[1:1]);
+  x = r[1];
+  return x;
+}

compiler/src/prog.ml

@@ -512,14 +512,14 @@ let is_var = function
   | Pvar _ -> true
   | _ -> false
 
+let access_offset aa ws i =
+  match aa with
+  | Warray_.AAscale -> size_of_ws ws * i
+  | Warray_.AAdirect -> i
+
 let get_ofs aa ws e =
   match e with
-  | Pconst i ->
-     Some
-       (match aa with
-        | Warray_.AAdirect -> Z.to_int i
-        | Warray_.AAscale -> size_of_ws ws * Z.to_int i
-       )
+  | Pconst i -> Some (access_offset aa ws (Z.to_int i))
   | _ -> None
 
 (* -------------------------------------------------------------------- *)

compiler/src/prog.mli

@@ -300,6 +300,8 @@ val array_kind : ty -> wsize * int
 val ws_of_ty   : 'e gty -> wsize
 val arr_size : wsize -> int -> int
 val size_of  : ty -> int
+val access_offset : Warray_.arr_access -> wsize -> int -> int
+
 (* -------------------------------------------------------------------- *)
 (* Functions on variables                                               *)
 

compiler/src/safety/safetyAbsExpr.ml

@@ -360,10 +360,6 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
       (arr_range x * size_of_ws (arr_size x))
       (fun i -> AarraySlice (x, U8, i))
 
-  let access_offset acc ws i = match acc with
-    | Warray_.AAscale  -> size_of_ws ws * i
-    | Warray_.AAdirect -> i 
-
   (* let abs_arr_range_at abs x acc ws ei = match aeval_cst_int abs ei with
    *   | Some i ->
    *     [AarraySlice (x, ws, access_offset acc ws i)]

compiler/src/safety/safetyInterpreter.ml

@@ -1544,6 +1544,29 @@ end = struct
       fname
       L.pp_iloc ginstr.i_loc
 
+  let cells_of_array x ofs n =
+    let x = L.unloc x in
+    List.init (Conv.int_of_pos n) (fun i -> SafetyVar.AarraySlice (x, U8, ofs + i))
+
+  let aeval_syscall state sc lvs _es =
+    match sc with
+    | Syscall_t.RandomBytes n ->
+       let cells = match lvs with
+         | [ Lnone _ ] -> []
+         | [ Lvar x ] -> cells_of_array x 0 n
+         | [ Lasub(aa, ws, _len, x, ofs) ] ->
+            begin match AbsExpr.aeval_cst_int state.abs ofs with
+            | Some j -> cells_of_array x (access_offset aa ws j) n
+            | None ->
+               debug (fun () ->
+                   Format.eprintf "Warning: cannot compute the offset of the destination of #randombytes@.");
+               []
+            end
+         | _ -> assert false
+       in
+       let abs = List.fold_left AbsDom.is_init state.abs cells in
+       { state with abs }
+
   let rec aeval_ginstr asmOp : ('ty,minfo,'asm) ginstr -> astate -> astate =
     fun ginstr state ->
       debug (fun () ->
@@ -1593,10 +1616,8 @@ end = struct
 
         { state with abs = abs; }
 
-      | Csyscall(lvs, _o, _es) ->
-        let assgns = opn_dflt (List.length lvs) in
-        let abs = AbsExpr.abs_assign_opn state.abs ginstr.i_info lvs assgns in
-        { state with abs = abs; }
+      | Csyscall(lvs, sc, es) ->
+         aeval_syscall state sc lvs es
 
       | Cif(e,c1,c2) ->
         aeval_if asmOp ginstr e c1 c2 state