Linearization: correct info on RET instructions

Author: vbgl

proofs/compiler/linearization.v

@@ -729,7 +729,7 @@ Fixpoint linear_i (i:instr) (lbl:label) (lc:lcmd) :=
   | Cfor _ _ _ => (lbl, lc)
   end.
 
-Definition linear_body (e: stk_fun_extra) (body: cmd) : label * lcmd :=
+Definition linear_body (fi: fun_info) (e: stk_fun_extra) (body: cmd) : label * lcmd :=
   let: (tail, head, lbl) :=
      match sf_return_address e with
      | RAreg r _ =>
@@ -741,7 +741,7 @@ Definition linear_body (e: stk_fun_extra) (body: cmd) : label * lcmd :=
        ( if ra_return is Some ra_return
          then [:: lload (mk_var_i ra_return) rspi z;
                   MkLI dummy_instr_info (Ligoto (Rexpr (Fvar (mk_var_i ra_return)))) ]
-         else [:: MkLI dummy_instr_info Lret ]
+         else [:: MkLI (ret_info_of_fun_info fi) Lret ]
        , MkLI dummy_instr_info (Llabel 1) ::
          (if ra_call is Some ra_call
           then [:: lstore rspi z (mk_var_i ra_call) ]
@@ -786,7 +786,7 @@ Definition linear_fd (fd: sfundef) :=
   let e := fd.(f_extra) in
   let is_export := is_RAnone (sf_return_address e) in
   let res := if is_export then f_res fd else [::] in
-  let body := linear_body e fd.(f_body) in
+  let body := linear_body fd.(f_info) e fd.(f_body) in
   (body.1,
     {| lfd_info := f_info fd
     ; lfd_align := sf_align e

proofs/compiler/linearization_proof.v

@@ -1080,8 +1080,8 @@ Section NUMBER_OF_LABELS.
   Definition linear_i_nb_labels : ∀ i, Pi i :=
     instr_Rect nb_labels_MkI nb_labels_nil nb_labels_cons nb_labels_assign nb_labels_opn nb_labels_syscall nb_labels_if nb_labels_for nb_labels_while nb_labels_call.
 
-  Lemma linear_body_nb_labels fn e body :
-    let: (lbl, lc) := linear_body liparams p fn e body in
+  Lemma linear_body_nb_labels fn fi e body :
+    let: (lbl, lc) := linear_body liparams p fn fi e body in
     (Z.of_nat (size (label_in_lcmd lc)) <= lbl)%Z.
   Proof.
     rewrite /linear_body.
@@ -1313,8 +1313,8 @@ Section PROOF.
   Proof.
     elim: funcs lbl => [|[f fd] funcs ih] lbl //=.
     set linear_f := (fun _ => _).
-    have := ih ((linear_body liparams p f (f_extra fd) (f_body fd)).1)%positive.
-    have := ih (lbl + (linear_body liparams p f (f_extra fd) (f_body fd)).1)%positive.
+    have := ih ((linear_body liparams p f (f_info fd) (f_extra fd) (f_body fd)).1)%positive.
+    have := ih (lbl + (linear_body liparams p f (f_info fd) (f_extra fd) (f_body fd)).1)%positive.
     case: fmap => [nb_lbl' funcs'].
     rewrite Pos.add_assoc => -> ->.
     by rewrite (Pos.add_comm lbl) Pos.add_assoc.
@@ -1331,7 +1331,7 @@ Section PROOF.
     have := fmap_linear_fd_acc ((linear_fd fn f').1)%positive funcs.
     case: fmap ih => [nb_lbl funcs'] /= ih -> /=.
     rewrite size_cat size_map Nat2Z.inj_add.
-    have := linear_body_nb_labels p liparams fn (f_extra f') (f_body f').
+    have := linear_body_nb_labels p liparams fn (f_info f') (f_extra f') (f_body f').
     case: linear_body => [nb_lbl' lc] /=.
     lia.
   Qed.
@@ -4786,7 +4786,7 @@ Section PROOF.
       have := [elaborate (wunsigned_range (top_stack m))].
       by lia.
     set ls0 := ls_export_initial scs lm vm fn.
-    case/(_ m0 sp0 max0 _ _ ls0 lm vm (linear_body liparams p fn fd.(f_extra)
+    case/(_ m0 sp0 max0 _ _ ls0 lm vm (linear_body liparams p fn fd.(f_info) fd.(f_extra)
         fd.(f_body)).2 RAnone None (top_stack m)
         (map fst fd.(f_extra).(sf_to_save)) M _ _ erefl).
     - exact: enough_space.

proofs/lang/expr.v

@@ -433,20 +433,27 @@ Section CMD_RECT.
 
 End CMD_RECT.
 
-Module FunInfo : TAG.
+Module Type FunInfoT <: TAG.
+  Include TAG.
+  Parameter ret_info : t -> instr_info.
+End FunInfoT.
+
+Module FunInfo : FunInfoT.
   Definition t := positive.
   Definition witness : t := 1%positive.
+  Definition ret_info of t := dummy_instr_info.
 End FunInfo.
 
+Definition fun_info := FunInfo.t.
+Definition ret_info_of_fun_info (fi: fun_info) : instr_info := FunInfo.ret_info fi.
+
 Section ASM_OP.
 
 Context `{asmop:asmOp}.
 
 (* ** Functions
  * -------------------------------------------------------------------- *)
 
-Definition fun_info := FunInfo.t.
-
 Class progT := {
   extra_fun_t : Type;
   extra_prog_t : Type;

proofs/lang/extraction.v

@@ -32,6 +32,7 @@ Extract Constant expr.InstrInfo.is_inline => "IInfo.is_inline".
 Extract Constant expr.InstrInfo.var_info_of_ii => "IInfo.var_info_of_ii".
 Extract Constant expr.instr_info => "IInfo.t".
 Extract Constant expr.fun_info => "FInfo.t".
+Extract Constant expr.ret_info_of_fun_info => "FInfo.ret_info".
 Extract Constant waes.MixColumns => "(fun _ -> failwith ""MixColumns is not implemented"")".
 Extract Constant waes.InvMixColumns => "(fun _ -> failwith ""InvMixColumns not implemented"")".