SCT: More precise detection of speculative safe loads

CHANGELOG.md

@@ -33,6 +33,9 @@
   ([PR #541](https://github.com/jasmin-lang/jasmin/pull/541);
   fixes [#540](https://github.com/jasmin-lang/jasmin/issues/540)).
 
+ - More precise detection of speculative safe loads in the SCT checker
+  ([PR #556](https://github.com/jasmin-lang/jasmin/pull/556)).
+
 ## Other changes
 
 - Pretty-printing of Jasmin programs is more precise

compiler/src/coreConv.ml

@@ -1,11 +1,14 @@
-let rec pos_of_z z =
+let pos_of_z z =
   let open Z.Compare in
-  if z <= Z.one then BinNums.Coq_xH
-  else
-    let p = pos_of_z (Z.shift_right z 1) in
-    if (Z.erem z (Z.of_int 2)) = Z.one
-    then BinNums.Coq_xI p
-    else BinNums.Coq_xO p
+  assert (Z.one <= z);
+  let rec pos_of_z z =
+    if z <= Z.one then BinNums.Coq_xH
+    else
+      let p = pos_of_z (Z.shift_right z 1) in
+      if (Z.erem z (Z.of_int 2)) = Z.one
+      then BinNums.Coq_xI p
+      else BinNums.Coq_xO p
+  in pos_of_z z
 
 let rec z_of_pos pos =
   let open Z in

compiler/src/sct_checker_forward.ml

@@ -554,7 +554,7 @@ let ssafe_test x i =
   match x.v_kind, x.v_ty, i with
   | Reg (_, Direct), _, _ -> true
   | _, Arr (_ (* word size. should be used ? *), len), Pconst v ->
-      let v = Conv.int_of_pos (Conv.pos_of_z v) in v < len
+      Z.(leq zero v && lt v (of_int len))
   | _ -> false
 
 let content_ty = function

compiler/tests/sct-checker/local-stack-array.jazz

@@ -0,0 +1,9 @@
+export
+fn main(#transient reg u64 io) -> #public reg u64 {
+  _ = #init_msf();
+  stack u64[1] local;
+  local[0] = 42;
+  reg u64 r;
+  r = local[0];
+  return r;
+}