checksafety: improve handling of LEA instruction

CHANGELOG.md

@@ -35,6 +35,9 @@
 - Preserve formatting of integer literals in the lexer and when pretty-printing to LATEX
   ([PR #886](https://github.com/jasmin-lang/jasmin/pull/886)).
 
+- Improve handling of instruction `LEA` in the safety checker
+  ([PR #900](https://github.com/jasmin-lang/jasmin/pull/900)).
+
 
 # Jasmin 2024.07.0 — Sophia-Antipolis, 2024-07-09
 

compiler/safety/success/lea.jazz

@@ -0,0 +1,29 @@
+param int N = 4;
+
+export
+fn nested_loops(reg ptr u16[N] array) -> reg ptr u16[N] {
+  reg u64 i;
+  ?{}, i = #set0();
+  while (i < N - 1) {
+    reg u64 j;
+    j = #LEA(i + 1);
+    while (j < N) {
+      array[j] += 1;
+      j += 1;
+    }
+    i += 1;
+  }
+  return array;
+}
+
+export
+fn truncate() -> reg u64 {
+  stack u64[2] s;
+  s[1] = 0;
+  reg u64 x;
+  x = (1<<32);
+  reg u64 y;
+  y = (64u)#LEA_32(x +64u 1);
+  x = s[y];
+  return x;
+}

compiler/safetylib/safetyInterpreter.ml

@@ -1356,6 +1356,14 @@ end = struct
       let e = Papp1 (E.Olnot ws, e1) in
       [Some e]
 
+    | Sopn.Oasm (Arch_extra.BaseOp (x, X86_instr_decl.LEA ws)) ->
+      let e1 = as_seq1 es in
+      let e =
+        match ty_expr e1 with
+        | Bty (U ws') when int_of_ws ws < int_of_ws ws' -> Papp1 (E.Ozeroext (ws, ws'), e1)
+        | _ -> e1 in
+      [Some e]
+
     | Sopn.Oslh op ->
        begin match op with
        | SLHinit -> [ Some (pcast U64 (Pconst (Z.of_int 0))) ]