Compiler: perform two rounds of range splitting

CHANGELOG.md

@@ -80,6 +80,10 @@
   can be expressed using equality and disequality tests
   ([PR #270](https://github.com/jasmin-lang/jasmin/pull/270)).
 
+- The live-range-splitting transformation is run a second time after
+  expansion of register arrays
+  ([PR #341](https://github.com/jasmin-lang/jasmin/pull/341)).
+
 # Jasmin 2022.09.0
 
 ## Bug fixes

compiler/tests/success/bug_340.jazz

@@ -0,0 +1,13 @@
+inline fn xor(reg u256 a b) -> reg u256 {
+  reg u256 c;
+  c = a ^ b;
+  return c;
+}
+
+export
+fn main(reg u256 x) -> reg u256 {
+  reg u256[1] a;
+  a[0] = x;
+  x = xor(a[0], a[0]);
+  return x;
+}

proofs/compiler/compiler.v

@@ -225,6 +225,18 @@ Definition check_no_ptr entries (ao: funname -> stk_alloc_oracle_t) : cexec unit
        assert (allNone sao.(sao_return)) (pp_at_fn fn (stack_alloc.E.stk_error_no_var "export functions don’t support “ptr” return values")))
     entries.
 
+Definition live_range_splitting (p: uprog) : cexec uprog :=
+  let pv := split_live_ranges_prog p in
+  let pv := cparams.(print_uprog) Splitting pv in
+  let pv := renaming_prog pv in
+  let pv := cparams.(print_uprog) Renaming pv in
+  let pv := remove_phi_nodes_prog pv in
+  let pv := cparams.(print_uprog) RemovePhiNodes pv in
+  Let _ := check_uprog p.(p_extra) p.(p_funcs) pv.(p_extra) pv.(p_funcs) in
+  Let pv := dead_code_prog (ap_is_move_op aparams) pv false in
+  let p := cparams.(print_uprog) DeadCode_Renaming pv in
+  ok p.
+
 Definition compiler_first_part (to_keep: seq funname) (p: prog) : cexec uprog :=
 
   Let p := array_copy_prog cparams.(fresh_counter) p in
@@ -242,22 +254,16 @@ Definition compiler_first_part (to_keep: seq funname) (p: prog) : cexec uprog :=
   Let p := unroll_loop (ap_is_move_op aparams) p in
   let p := cparams.(print_uprog) Unrolling p in
 
-  let pv := split_live_ranges_prog p in
-  let pv := cparams.(print_uprog) Splitting pv in
-  let pv := renaming_prog pv in
-  let pv := cparams.(print_uprog) Renaming pv in
-  let pv := remove_phi_nodes_prog pv in
-  let pv := cparams.(print_uprog) RemovePhiNodes pv in
-  Let _ := check_uprog p.(p_extra) p.(p_funcs) pv.(p_extra) pv.(p_funcs) in
-  Let pv := dead_code_prog (ap_is_move_op aparams) pv false in
-  let pv := cparams.(print_uprog) DeadCode_Renaming pv in
+  Let pv := live_range_splitting p in
 
   let pr := remove_init_prog cparams.(is_reg_array) pv in
   let pr := cparams.(print_uprog) RemoveArrInit pr in
 
   Let pe := expand_prog cparams.(expand_fd) pr in
   let pe := cparams.(print_uprog) RegArrayExpansion pe in
 
+  Let pe := live_range_splitting pe in
+
   Let pg := remove_glob_prog cparams.(is_glob) cparams.(fresh_id) pe in
   let pg := cparams.(print_uprog) RemoveGlobal pg in
 

proofs/compiler/compiler_proof.v

@@ -110,6 +110,37 @@ Definition compose_pass_uincl : ∀ vr (P Q: _ → Prop),
       let 'ex_intro vr2 (conj q v) := h _ p in
       ex_intro2 _ _ vr2 (Forall2_trans value_uincl_trans u v) q.
 
+Definition compose_pass_uincl' : ∀ vr (P Q: _ → Prop),
+        (∀ vr, P vr → exists2 vr', List.Forall2 value_uincl vr vr' & Q vr') →
+        (exists2 vr', List.Forall2 value_uincl vr vr' & P vr') →
+        (exists2 vr', List.Forall2 value_uincl vr vr' & Q vr')
+  :=
+      λ vr P Q h x,
+      let 'ex_intro2 vr1 u p := x in
+      let 'ex_intro2 vr2 v q := h _ p in
+      ex_intro2 _ _ vr2 (Forall2_trans value_uincl_trans u v) q.
+
+Lemma live_range_splittingP (p p': uprog) scs m fn va scs' m' vr :
+  live_range_splitting aparams cparams p = ok p' →
+  psem.sem_call p tt scs m fn va scs' m' vr →
+  exists2 vr',
+      List.Forall2 value_uincl vr vr' &
+      psem.sem_call p' tt scs m fn va scs' m' vr'.
+Proof.
+  rewrite /live_range_splitting; t_xrbindP.
+  rewrite !print_uprogP => ok_p' pa ok_pa.
+  rewrite print_uprogP => ? exec_p; subst pa.
+  have va_refl := List_Forall2_refl va value_uincl_refl.
+  apply: compose_pass_uincl.
+  - move=> vr' Hvr'.
+    apply: (dead_code_callPu (hap_is_move_opP haparams) ok_pa va_refl).
+    exact: Hvr'.
+  apply: compose_pass_uincl; first by move => vr'; apply: (alloc_call_uprogP (spp := mk_spp) ok_p').
+  exists vr.
+  - exact: (List_Forall2_refl _ value_uincl_refl).
+  by rewrite surj_prog.
+Qed.
+
 Lemma compiler_first_partP entries (p: prog) (p': uprog) scs m fn va scs' m' vr :
   compiler_first_part aparams cparams entries p = ok p' →
   fn \in entries →
@@ -123,11 +154,11 @@ Proof.
   rewrite print_uprogP => ok_pa pb.
   rewrite print_uprogP => ok_pb pc.
   rewrite print_uprogP => ok_pc.
-  rewrite !print_uprogP => ok_pd pe ok_pe.
-  rewrite !print_uprogP => pf ok_pf pg.
-  rewrite !print_uprogP => ok_pg ph ok_ph.
-  rewrite print_uprogP => ok_fvars.
-  rewrite print_uprogP => pp ok_pp.
+  rewrite !print_uprogP => pd ok_pd.
+  rewrite !print_uprogP => pe ok_pe.
+  rewrite !print_uprogP => pf ok_pf pg ok_pg.
+  rewrite !print_uprogP => ph ok_ph.
+  rewrite !print_uprogP => ok_fvars pp ok_pp.
   rewrite print_uprogP => <- {p'} ok_fn exec_p.
   have va_refl := List_Forall2_refl va value_uincl_refl.
   apply: compose_pass_uincl.
@@ -147,15 +178,15 @@ Proof.
     first by move=> vr';
       apply: (makeReferenceArguments_callP (spp := mk_spp) ok_ph).
   apply: compose_pass; first by move => vr'; apply: (RGP.remove_globP ok_pg).
+  apply: compose_pass_uincl'.
+  - move => vr' Hvr'.
+    apply: (live_range_splittingP ok_pf); exact: Hvr'.
   apply: compose_pass;
-    first by move=> vr'; apply:(expand_callP (spp := mk_spp) ok_pf).
+    first by move=> vr'; apply:(expand_callP (spp := mk_spp) ok_pe).
   apply: compose_pass_uincl; first by move =>vr'; apply: (remove_init_fdPu _ va_refl).
-  apply: compose_pass_uincl.
+  apply: compose_pass_uincl'.
   - move => vr' Hvr'.
-    apply: (dead_code_callPu (hap_is_move_opP haparams) ok_pe va_refl).
-    exact: Hvr'.
-  apply: compose_pass_uincl; first by move => vr'; apply: (alloc_call_uprogP (spp := mk_spp) ok_pd).
-  rewrite surj_prog.
+    apply: (live_range_splittingP ok_pd); exact: Hvr'.
   apply: compose_pass_uincl; first by move=> vr' Hvr'; apply: (unrollP ok_pc _ va_refl); exact: Hvr'.
   apply: compose_pass;
     first by move => vr';