From b816d696733c96fdc62428e43c4a4a1f5a09b47b Mon Sep 17 00:00:00 2001
From: Pierre Nigron <pierre.nigron@free.fr>
Date: Tue, 22 Sep 2020 12:32:59 +0200
Subject: RTLgen: use the state and error monad for reserve_labels (#371)

---
 Changelog             |  4 ++++
 backend/RTLgen.v      | 31 +++++++++++++++----------------
 backend/RTLgenproof.v |  5 ++---
 backend/RTLgenspec.v  |  8 +++-----
 4 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/Changelog b/Changelog
index 5dc56c1b..c7d8d2f4 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,7 @@
+Coq development:
+- RTLgen: use the state and error monad for reserving goto labels (#371)
+  (by Pierre Nigron)
+
 Release 3.11, 2022-06-27
 ========================
 
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index f7280c9e..4fd8da45 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -646,21 +646,20 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
 
 (** Preallocate CFG nodes for each label defined in the function body. *)
 
-Definition alloc_label (lbl: Cminor.label) (maps: labelmap * state) : labelmap * state :=
-  let (map, s) := maps in
-  let n := s.(st_nextnode) in
-  (PTree.set lbl n map,
-   mkstate s.(st_nextreg) (Pos.succ s.(st_nextnode)) s.(st_code) (reserve_instr_wf s)).
+Definition alloc_label (lbl: Cminor.label) (map: labelmap) : mon labelmap :=
+  do n <- reserve_instr;
+  ret (PTree.set lbl n map).
+   
 
-Fixpoint reserve_labels (s: stmt) (ms: labelmap * state)
-                        {struct s} : labelmap * state :=
+Fixpoint reserve_labels (s: stmt) (lm: labelmap)
+                        {struct s} : mon labelmap :=
   match s with
-  | Sseq s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
-  | Sifthenelse c s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
-  | Sloop s1 => reserve_labels s1 ms
-  | Sblock s1 => reserve_labels s1 ms
-  | Slabel lbl s1 => alloc_label lbl (reserve_labels s1 ms)
-  | _ => ms
+  | Sseq s1 s2 | Sifthenelse _ s1 s2 =>
+      do lm' <- reserve_labels s2 lm; reserve_labels s1 lm'
+  | Sloop s1 | Sblock s1 => reserve_labels s1 lm
+  | Slabel lbl s1 =>
+      do lm' <- reserve_labels s1 lm; alloc_label lbl lm'
+  | _ => ret lm
   end.
 
 (** Translation of a CminorSel function. *)
@@ -668,7 +667,8 @@ Fixpoint reserve_labels (s: stmt) (ms: labelmap * state)
 Definition ret_reg (sig: signature) (rd: reg) : option reg :=
   if rettype_eq sig.(sig_res) Tvoid then None else Some rd.
 
-Definition transl_fun (f: CminorSel.function) (ngoto: labelmap): mon (node * list reg) :=
+Definition transl_fun (f: CminorSel.function): mon (node * list reg) :=
+  do ngoto <- reserve_labels f.(fn_body) (PTree.empty node);
   do (rparams, map1) <- add_vars init_mapping f.(CminorSel.fn_params);
   do (rvars, map2) <- add_vars map1 f.(CminorSel.fn_vars);
   do rret <- new_reg;
@@ -678,8 +678,7 @@ Definition transl_fun (f: CminorSel.function) (ngoto: labelmap): mon (node * lis
   ret (nentry, rparams).
 
 Definition transl_function (f: CminorSel.function) : Errors.res RTL.function :=
-  let (ngoto, s0) := reserve_labels f.(fn_body) (PTree.empty node, init_state) in
-  match transl_fun f ngoto s0 with
+  match transl_fun f init_state with
   | Error msg => Errors.Error msg
   | OK (nentry, rparams) s i =>
       Errors.OK (RTL.mkfunction
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 79b9319b..90f03c1c 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -397,9 +397,8 @@ Lemma sig_transl_function:
 Proof.
   intros until tf. unfold transl_fundef, transf_partial_fundef.
   case f; intro.
-  unfold transl_function.
-  destruct (reserve_labels (fn_body f0) (PTree.empty node, init_state)) as [ngoto s0].
-  case (transl_fun f0 ngoto s0); simpl; intros.
+  unfold transl_function. 
+  case (transl_fun f0 (init_state)); simpl; intros.
   discriminate.
   destruct p. simpl in H. inversion H. reflexivity.
   intro. inversion H. reflexivity.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 25f9954c..f072b645 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -1339,14 +1339,12 @@ Lemma transl_function_charact:
   tr_function f tf.
 Proof.
   intros until tf. unfold transl_function.
-  caseEq (reserve_labels (fn_body f) (PTree.empty node, init_state)).
-  intros ngoto s0 RESERVE.
-  caseEq (transl_fun f ngoto s0). congruence.
+  caseEq (transl_fun f init_state). congruence.
   intros [nentry rparams] sfinal INCR TR E. inv E.
   monadInv TR.
-  exploit add_vars_valid. eexact EQ. apply init_mapping_valid.
+  exploit add_vars_valid. eexact EQ1. apply init_mapping_valid.
   intros [A B].
-  exploit add_vars_valid. eexact EQ1. auto.
+  exploit add_vars_valid. eexact EQ0. auto.
   intros [C D].
   eapply tr_function_intro; eauto with rtlg.
   eapply transl_stmt_charact; eauto with rtlg.
-- 
cgit