From d575d205b80d2a26ecbd14cfeb1aad477b196f43 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 21 Apr 2020 14:17:00 +0200
Subject: Added and cleaned some comments on RTLpath.v

---
 mppa_k1c/lib/RTLpath.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/lib/RTLpath.v b/mppa_k1c/lib/RTLpath.v
index 6aa0258e..35f6e715 100644
--- a/mppa_k1c/lib/RTLpath.v
+++ b/mppa_k1c/lib/RTLpath.v
@@ -144,6 +144,7 @@ Coercion program_RTL: program >-> RTL.program.
 Record istate := ist { continue: bool; the_pc: node; the_rs: regset; the_mem: mem }.
 
 (* FIXME - prediction *)
+(* Internal step through the path *)
 Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem): option istate :=
   match i with
   | Inop pc' => Some (ist true pc' rs m)
@@ -175,6 +176,7 @@ Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem)
 
 (** Execution of a path in a single step *)
 
+(* Executes until a state [st] is reached where st.(continue) is false *)
 Fixpoint isteps ge (path:nat) (f: function) sp rs m pc: option istate :=
   match path with
   | O => Some (ist true pc rs m)
@@ -244,6 +246,7 @@ Definition state_RTL (s: state): RTL.state :=
   end.
 Coercion state_RTL: state >-> RTL.state.
 
+(* Used to execute the last instruction of a path (isteps is only in charge of executing the instructions before the last) *)
 Inductive path_last_step ge pge stack (f: function): val -> node -> regset -> mem -> trace -> state -> Prop :=
   | exec_istate i sp pc rs m st:
      (fn_code f)!pc = Some i ->
@@ -281,6 +284,7 @@ Inductive path_last_step ge pge stack (f: function): val -> node -> regset -> me
       path_last_step ge pge stack f (Vptr stk Ptrofs.zero) pc rs m
         E0 (Returnstate stack (regmap_optget or Vundef rs) m').
 
+(* Executes an entire path *)
 Inductive path_step ge pge (path:nat) stack f sp rs m pc: trace -> state -> Prop :=
   | exec_early_exit st:
      isteps ge path f sp rs m pc = Some st ->
@@ -292,6 +296,7 @@ Inductive path_step ge pge (path:nat) stack f sp rs m pc: trace -> state -> Prop
      path_last_step ge pge stack f sp st.(the_pc) st.(the_rs) st.(the_mem) t s ->
      path_step ge pge path stack f sp rs m pc t s.
 
+(* Either internal path execution, or the usual exec_function / exec_return borrowed from RTL *)
 Inductive step ge pge: state -> trace -> state -> Prop :=
   | exec_path path stack f sp rs m pc t s: 
       (fn_path f)!pc = Some path ->
@@ -387,6 +392,7 @@ This way can be viewed as a correctness property: all transitions in RTLpath are
 
 Local Hint Resolve RTL.exec_Inop RTL.exec_Iop RTL.exec_Iload RTL.exec_Istore RTL.exec_Icond RTL.exec_Iload_notrap1 RTL.exec_Iload_notrap2: core.
 
+(* istep reflects RTL.step *)
 Lemma istep_correct ge i stack (f:function) sp rs m st :
   istep ge i sp rs m = Some st ->
   forall pc, (fn_code f)!pc = Some i ->
@@ -398,6 +404,7 @@ Qed.
 
 Local Hint Resolve star_refl: core.
 
+(* isteps reflects a star relation on RTL.step *)
 Lemma isteps_correct ge path stack f sp: forall rs m pc st,
   isteps ge path f sp rs m pc = Some st ->
   star RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)).
@@ -692,6 +699,7 @@ Proof.
     destruct (continue st0) eqn: CONT0; eauto.
 Qed.
 
+(* FIXME - add prediction *)
 Inductive is_early_exit pc: instruction -> Prop :=
   | Icond_early_exit cond args ifnot predict:
      is_early_exit pc (Icond cond args pc ifnot predict)
@@ -785,7 +793,6 @@ Definition match_states (idx: nat) (s1:RTL.state) (s2:state): Prop :=
  /\ wf_stackframe (stack_of s2).
 
 (** *** Auxiliary lemmas of completeness *)
-(* FIXME - needs to update to take into account the load_notrap *)
 Lemma istep_complete t i stack f sp rs m pc s':
   RTL.step ge (State stack f sp pc rs m) t s' ->
   (fn_code f)!pc = Some i -> 
-- 
cgit