Remove dead functions after loop unrolling

Fixes #607

CHANGELOG.md

@@ -74,6 +74,10 @@
   ([PR 600]((https://github.com/jasmin-lang/jasmin/pull/600);
   fixes [#599](https://github.com/jasmin-lang/jasmin/issues/599)).
 
+- Remove dead functions after loop unrolling
+  ([PR 611](https://github.com/jasmin-lang/jasmin/pull/611);
+  fixes [#607](https://github.com/jasmin-lang/jasmin/issues/607)).
+
 ## Other changes
 
 - Pretty-printing of Jasmin programs is more precise

compiler/tests/success/common/bug_607.jazz

@@ -0,0 +1,19 @@
+fn f(reg ptr u64[1] a, reg u64 x) -> stack u64[1], reg u64 {
+    stack ptr u64[1] s;
+    s = a;
+    a = s;
+    return a, x;
+}
+
+export
+fn main() {
+    reg u64 x;
+    x = 0;
+
+    stack u64[1] a;
+    a[0] = 0;
+
+    if (false) {
+        _, _ = f(a, x);
+    }
+}

proofs/compiler/compiler.v

@@ -258,6 +258,9 @@ 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 p := dead_calls_err_seq to_keep p in
+  let p := cparams.(print_uprog) RemoveUnusedFunction p in
+
   Let pv := live_range_splitting p in
 
   let pr := remove_init_prog is_reg_array pv in

proofs/compiler/compiler_proof.v

@@ -187,16 +187,17 @@ Proof.
   rewrite !print_uprogP => pd ok_pd.
   rewrite !print_uprogP => pe ok_pe.
   rewrite !print_uprogP => pf ok_pf.
-  rewrite !print_uprogP => pg ok_pg ph ok_ph.
-  rewrite !print_uprogP => ok_fvars pi ok_pi pp.
+  rewrite !print_uprogP => pg ok_pg.
+  rewrite !print_uprogP => ph ok_ph pi ok_pi.
+  rewrite !print_uprogP => ok_fvars pj ok_pj pp.
   rewrite !print_uprogP => ok_pp <- {p'} ok_fn exec_p.
 
   have va_refl := List_Forall2_refl va value_uincl_refl.
   apply: compose_pass_uincl.
   - move=> vr'; apply: (pi_callP (sCP := sCP_unit) ok_pp va_refl).
    apply: compose_pass.
   - move=> vr'.
-    assert (h := lower_slh_prog_sem_call (dc:=direct_c) (hap_hshp haparams) (ev:= tt) ok_pi).
+    assert (h := lower_slh_prog_sem_call (dc:=direct_c) (hap_hshp haparams) (ev:= tt) ok_pj).
     apply h => //.
   apply: compose_pass.
   - move => vr'.
@@ -206,19 +207,21 @@ Proof.
          (lowering_opt cparams)
          (warning cparams)
          ok_fvars).
-  apply: compose_pass; first by move => vr'; apply: (RGP.remove_globP ok_ph).
+  apply: compose_pass; first by move => vr'; apply: (RGP.remove_globP ok_pi).
   apply: compose_pass_uincl'.
-  - move => vr'; apply: (live_range_splittingP ok_pg).
+  - move => vr'; apply: (live_range_splittingP ok_ph).
   apply: compose_pass.
-  - move=> vr' hvr'. assert (h := expand_callP (sip := sip_of_asm_e) ok_pf); apply h => //; apply hvr'.
+  - move=> vr' hvr'. assert (h := expand_callP (sip := sip_of_asm_e) ok_pg); apply h => //; apply hvr'.
   apply: compose_pass_uincl'.
   - by move=>  vr'; apply: indirect_to_direct.
   apply: compose_pass.
-  - by move=> vr'; apply: (makeReferenceArguments_callP (siparams := sip_of_asm_e) ok_pe).
+  - by move=> vr'; apply: (makeReferenceArguments_callP (siparams := sip_of_asm_e) ok_pf).
   apply: compose_pass_uincl; first by move =>vr'; apply: (remove_init_fdPu _ va_refl).
   apply: compose_pass_uincl'.
   - move => vr' Hvr'.
-    apply: (live_range_splittingP ok_pd); exact: Hvr'.
+    apply: (live_range_splittingP ok_pe); exact: Hvr'.
+  apply: compose_pass.
+  - by move => vr'; exact: (dead_calls_err_seqP (sip := sip_of_asm_e) (sCP := sCP_unit) ok_pd).
   apply: compose_pass_uincl; first by move=> vr' Hvr'; apply: (unrollP ok_pc _ va_refl); exact: Hvr'.
   apply: compose_pass_uincl'; first by move => vr' Hvr'; apply: (inliningP ok_pa ok_fn); exact: Hvr'.
   apply: compose_pass; first by move => vr'; apply: (add_init_fdP).