Verify the transformations in EasyCrypt extraction

compiler/entry/jasmin2ec.ml

@@ -32,6 +32,20 @@ let parse_and_extract arch call_conv idirs =
   let module A = (val CoreArchFactory.get_arch_module arch call_conv) in
   let extract model amodel functions array_dir output pass file =
     let prog = parse_and_compile (module A) ~wi2i:true pass file idirs in
+    let fresh_var_ident k ii n ty =
+      Conv.fresh_var_ident k ii (Uint63.of_int 0) n ty
+    in
+    let rename = LegalizeNames.build_rename prog in
+    let prog =
+      match
+        Conv.cuprog_of_prog prog
+        |> ToEC_jazz.toEC_prog A.asm_e fresh_var_ident rename (model = Normal)
+      with
+      | Utils0.Error e ->
+          let e = Conv.error_of_cerror (Printer.pp_err ~debug:false) e in
+          raise (HiError e)
+      | Utils0.Ok cp -> Conv.prog_of_cuprog cp
+    in
     extract_to_file prog arch A.reg_size A.msf_size A.asmOp model amodel
       functions array_dir output
   in

compiler/examples/extraction-unit-tests/.gitignore

@@ -3,5 +3,26 @@ gcd.ec
 loops.ec
 sdiv.ec
 string.ec
+normalize_cond.ec
+refresh_for.ec
+init_local_arrays.ec
+legalize_names.ec
+for_to_while.ec
+flatten_while.ec
+remove_baseop_casts.ec
+normalize_calls.ec
+make_coercions_explicit.ec
+remove_nullary_opns.ec
+Array1.ec
 Array2.ec
+Array4.ec
+Array8.ec
 BArray2.ec
+BArray4.ec
+BArray8.ec
+BArray16.ec
+BArray32.ec
+SBArray8_4.ec
+SBArray16_16.ec
+SBArray32_16.ec
+SBArray32_32.ec

compiler/examples/extraction-unit-tests/flatten_while.jazz

@@ -0,0 +1,59 @@
+export
+fn t_while_pre() -> reg u32 {
+  inline int i c;
+  i = 0;
+  c = 0;
+  while {
+    c = c + 1;
+  } (i < 5) {
+    i = i + 1;
+  }
+  reg u32 r = c;
+  return r;
+}
+
+export
+fn t_nested_while_pre() -> reg u32 {
+  inline int i j c;
+  i = 0;
+  c = 0;
+  while {
+    j = 0;
+  } (i < 3) {
+    while {
+      c = c + 1;
+    } (j < 2) {
+      j = j + 1;
+    }
+    i = i + 1;
+  }
+  reg u32 r = c;
+  return r;
+}
+
+export
+fn t_do_while() -> reg u32 {
+  inline int i c;
+  i = 0;
+  c = 0;
+  while {
+    c = c + 1;
+    i = i + 1;
+  } (i < 4) {
+  }
+  reg u32 r = c;
+  return r;
+}
+
+export
+fn t_plain_while() -> reg u32 {
+  inline int i c;
+  i = 0;
+  c = 0;
+  while (i < 5) {
+    c = c + 1;
+    i = i + 1;
+  }
+  reg u32 r = c;
+  return r;
+}

compiler/examples/extraction-unit-tests/for_to_while.jazz

@@ -0,0 +1,108 @@
+export
+fn t_up_const() -> reg u32 {
+  inline int i;
+  reg u32 r;
+  r = 0;
+  for i = 0 to 5 {
+    r += i;
+  }
+  return r;
+}
+
+export
+fn t_up_dynamic() -> reg u32 {
+  inline int i x y;
+  reg u32 r;
+  x = 1;
+  y = 4;
+  r = 0;
+  for i = x to y {
+    r += i;
+  }
+  return r;
+}
+
+export
+fn t_downto() -> reg u32 {
+  inline int i;
+  reg u32 r;
+  r = 0;
+  for i = 4 downto 0 {
+    r += i;
+  }
+  return r;
+}
+
+export
+fn t_nested() -> reg u32 {
+  inline int i j;
+  reg u32 k;
+  k = 0;
+  for i = 0 to 3 {
+    for j = 0 to 3 {
+      k += 1;
+    }
+  }
+  return k;
+}
+
+export
+fn t_empty_range_counter() -> reg u32 {
+  inline int i;
+  reg u32 r;
+  i = 42;
+  for i = 3 to 3 {
+    r = 0;
+  }
+  r = (32u) i;
+  return r;
+}
+
+export
+fn t_empty_range_dynamic() -> reg u32 {
+  inline int i x;
+  reg u32 r;
+  x = 7;
+  i = 99;
+  for i = x to x {
+    r = 0;
+  }
+  r = (32u) i;
+  return r;
+}
+
+export
+fn t_body_writes_counter() -> reg u32 {
+  inline int i;
+  reg u32 r;
+  r = 0;
+  for i = 0 to 5 {
+    r += i;
+    i = 0;
+  }
+  return r;
+}
+
+export
+fn t_bound_written_by_body() -> reg u32 {
+  inline int i n;
+  reg u32 r;
+  n = 4;
+  r = 0;
+  for i = 0 to n {
+    n = 0;
+    r += 1;
+  }
+  return r;
+}
+
+export
+fn t_counter_after_loop() -> reg u32 {
+  inline int i;
+  reg u32 r;
+  for i = 0 to 5 {
+    r = 0;
+  }
+  r = (32u) i;
+  return r;
+}

compiler/examples/extraction-unit-tests/init_local_arrays.jazz

@@ -0,0 +1,77 @@
+fn helper_read(reg ptr u64[4] p) -> reg u64 {
+  reg u64 s;
+  s = p[0] + p[1];
+  return s;
+}
+
+fn param_not_reinit(reg ptr u64[4] p, reg u64 x) -> reg ptr u64[4], reg u64 {
+  reg u64 r;
+  r = p[0];
+  p[1] = x;
+  return p, r;
+}
+
+export
+fn t_one_array(reg u64 x) -> reg u64 {
+  stack u64[4] a;
+  reg u64 r;
+  a[0] = x;
+  a[1] = x + 1;
+  r = a[0] + a[1];
+  return r;
+}
+
+export
+fn t_several_arrays(reg u64 x) -> reg u64 {
+  stack u32[4] a;
+  stack u64[2] b;
+  stack u8[8] c;
+  reg u64 r;
+  a[0] = (32u) x;
+  b[0] = x;
+  c[0] = (8u) x;
+  r = (64u) a[0] + b[0] + (64u) c[0];
+  return r;
+}
+
+export
+fn t_partial_write(reg u64 x) -> reg u64 {
+  stack u64[4] a;
+  reg ptr u64[4] p;
+  reg u64 r;
+  a[0] = x;
+  a[1] = x + 1;
+  p = a[0:4];
+  r = helper_read(p);
+  a[0:4] = p[0:4];
+  return r;
+}
+
+export
+fn t_regptr_local(reg u64 x) -> reg u64 {
+  stack u64[4] a;
+  reg ptr u64[4] p;
+  reg u64 r;
+  p = a[0:4];
+  p[0] = x;
+  p[1] = x + 1;
+  r = p[0] + p[1];
+  a[0:4] = p[0:4];
+  return r;
+}
+
+export
+fn t_call_param(reg u64 x) -> reg u64 {
+  stack u64[4] a;
+  reg ptr u64[4] p;
+  reg u64 r;
+  a[0] = 111;
+  a[1] = 222;
+  a[2] = 333;
+  a[3] = 444;
+  p = a[0:4];
+  p, r = param_not_reinit(p, x);
+  a[0:4] = p[0:4];
+  r += a[0];
+  return r;
+}

compiler/examples/extraction-unit-tests/legalize_names.jazz

@@ -0,0 +1,52 @@
+/* Tests legalize_names: variables whose source name is an EasyCrypt
+   keyword, an EasyCrypt "internal" pseudo-keyword, an uppercase-initial
+   identifier, a classic `res` clash (as both a param and a local), and
+   two distinct variables sharing one source name via inner-block
+   shadowing. The assertion is simply that the extracted `.ec` typechecks
+   -- that is exactly what legalization is for. */
+
+/* Locals named like EasyCrypt keywords/pseudo-keywords. */
+export
+fn t_keywords(reg u64 var, reg u64 axiom) -> reg u64 {
+  inline int end;
+  reg u64 leakages;
+  end = 0;
+  leakages = var + axiom + (64u)end;
+  return leakages;
+}
+
+/* An uppercase-initial local: EasyCrypt module-scoped names must be
+   lowercase-initial, the printer already lowercases global var names but
+   legalize_names must not accidentally produce a collision for it. */
+export
+fn t_uppercase(reg u64 x) -> reg u64 {
+  reg u64 Foo;
+  Foo = x + 1;
+  return Foo;
+}
+
+/* A param named `res`, the classic EasyCrypt clash (EC's own `res`
+   refers to the procedure's return value inside Hoare/pHoare triples). */
+export
+fn t_param_res(reg u64 res) -> reg u64 {
+  reg u64 r;
+  r = res + 1;
+  return r;
+}
+
+/* Two distinct Jasmin variables sharing the source name `x`: the
+   parameter `x` and an inner-block-local `x` that shadows it. Jasmin
+   itself resolves this via ordinary (non-block-scoped) shadowing; the
+   extracted EasyCrypt module must give the two live ranges distinct
+   identifiers. */
+export
+fn t_shadow(reg u32 x) -> reg u32 {
+  reg u32 a;
+  a = x;
+  if x <s 0 {
+    reg u32 x = 0;
+    a += x;
+  }
+  a += x;
+  return a;
+}

compiler/examples/extraction-unit-tests/make_coercions_explicit.jazz

@@ -0,0 +1,43 @@
+fn callee32(reg u32 p) -> reg u32 {
+  return p;
+}
+
+export
+fn t_assign_narrow(reg u64 y) -> reg u32 {
+  reg u32 x;
+  x = y;
+  return x;
+}
+
+export
+fn t_operand_narrow(reg u32 a, reg u64 y) -> reg u32 {
+  a = a + y;
+  return a;
+}
+
+export
+fn t_shift_narrow(reg u32 a, reg u64 y) -> reg u32 {
+  a = a << y;
+  return a;
+}
+
+export
+fn t_ternary_narrow(reg u64 x, reg u32 z, reg u64 y) -> reg u32 {
+  z = y <u 0 ? x : z;
+  return z;
+}
+
+export
+fn t_call_narrow(reg u64 y) -> reg u32 {
+  reg u32 r;
+  r = callee32(y);
+  return r;
+}
+
+export
+fn t_opn_narrow(reg u64 a, reg u64 b) -> reg u32 {
+  reg bool cf;
+  reg u32 r;
+  ?{}, r = #ADD_32(a, b);
+  return r;
+}