most of the proof BTL.fsem -> BTL.cfgsem.

1 files changed, 267 insertions, 41 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index bf19f4ac..389d8d93 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -17,6 +17,7 @@
 Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import RTL Op Registers OptionMonad.
+Require Import Lia.
 
 Import ListNotations.
 
@@ -380,22 +381,20 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall r m,
       final_state (Returnstate nil (Vint r) m) r.
 
-(** The basic small-step semantics for a BTL program. *)
+(** The "raw" CFG small-step semantics for a BTL program (e.g. close to RTL semantics) *)
 
 (* tid = transfer_identity *)
 Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs.
 
-Definition semantics (p: program) :=
+Definition cfgsem (p: program) :=
   Semantics (step tid) (initial_state p) final_state (Genv.globalenv p).
 
-(** The "functional" small-step semantics for a BTL program. 
+(** The full "functional" small-step semantics for a BTL program.
     at each exit, we only transfer register in "input_regs" (i.e. "alive" registers).
 *)
 Definition transfer_regs (inputs: list reg) (rs: regset): regset :=
   init_regs (rs##inputs) inputs.
 
-(* TODO: LEMMA BELOW ON transfer_regs USEFUL ? *)
-
 Lemma transfer_regs_inputs inputs rs r:
   List.In r inputs -> (transfer_regs inputs rs)#r = rs#r.
 Proof.
@@ -414,18 +413,20 @@ Proof.
   - rewrite Regmap.gso; auto.
 Qed.
 
-Fixpoint inputs_exitrec (f:function) (tbl: list exit): Regset.t :=
+Fixpoint union_inputs (f:function) (tbl: list exit): Regset.t :=
   match tbl with
   | nil => Regset.empty
-  | pc::l => let rs:= inputs_exitrec f l in
+  | pc::l => let rs:= union_inputs f l in
              match f.(fn_code)!pc with
              | None => rs
              | Some ib => Regset.union rs ib.(input_regs)
              end
   end.
 
-Lemma inputs_exitrec_In f tbl r:
-  Regset.In r (inputs_exitrec f tbl) -> (exists pc, List.In pc tbl /\ exists ib, f.(fn_code)!pc = Some ib /\ Regset.In r ib.(input_regs)).
+(* TODO: lemma not yet used
+
+Lemma union_inputs_In f tbl r:
+  Regset.In r (union_inputs f tbl) -> (exists pc, List.In pc tbl /\ exists ib, f.(fn_code)!pc = Some ib /\ Regset.In r ib.(input_regs)).
 Proof.
   induction tbl as [|pc l]; simpl; intros.
   - exploit Regset.empty_1; eauto. intuition.
@@ -437,27 +438,33 @@ Proof.
     + destruct IHl as (pc' & H1 & H2); eauto.
 Qed.
 
-Lemma inputs_exitrec_notIn f tbl r: 
+Lemma union_inputs_notIn f tbl r: 
    (forall pc ib, List.In pc tbl -> f.(fn_code)!pc = Some ib -> ~Regset.In r ib.(input_regs))
-    -> ~Regset.In r (inputs_exitrec f tbl).
+    -> ~Regset.In r (union_inputs f tbl).
 Proof.
   induction tbl as [|pc l]; simpl; intuition eauto.
   - exploit Regset.empty_1; eauto.
   - destruct ((fn_code f) ! pc) eqn:ATpc; intuition eauto.
     exploit Regset.union_1; intuition eauto.
 Qed.
+*)
 
-Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t :=
- let rs := inputs_exitrec f tbl in
+(* This function computes the union of the inputs associated to the exits
+                   minus the optional register in [or] (typically the result of a call or a builtin).
+   i.e. similar to [pre_output_regs] in RTLpath.
+*)
+Definition pre_inputs (f:function) (tbl: list exit) (or: option reg): Regset.t :=
+ let rs := union_inputs f tbl in
  match or with 
  | Some r => Regset.remove r rs
  | None => rs
- end.
+ end
+ .
 
-Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset 
-  := transfer_regs (Regset.elements (inputs_exit f tbl or)).
+(* TODO: lemma pre_inputs_In + pre_inputs_notIn ? *)
 
-(* TODO: BELOW, LEMMA on tr_inputs USEFUL ? *)
+Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset 
+  := transfer_regs (Regset.elements (pre_inputs f tbl or)).
 
 
 (* TODO: move this elsewhere *)
@@ -469,8 +476,8 @@ Proof.
   - induction l; simpl; intuition.
 Qed.
 
-Lemma tr_inputs_exit f tbl or rs r:
-  Regset.In r (inputs_exit f tbl or) -> (tr_inputs f tbl or rs)#r = rs#r.
+Lemma tr_pre_inputs f tbl or rs r:
+  Regset.In r (pre_inputs f tbl or) -> (tr_inputs f tbl or rs)#r = rs#r.
 Proof.
   intros; eapply transfer_regs_inputs.
   rewrite <- SetoidList_InA_eq_equiv.
@@ -478,17 +485,17 @@ Proof.
 Qed.
 
 Lemma tr_inputs_dead f tbl or rs r:
-  ~(Regset.In r (inputs_exit f tbl or)) -> (tr_inputs f tbl or rs)#r = Vundef.
+  ~(Regset.In r (pre_inputs f tbl or)) -> (tr_inputs f tbl or rs)#r = Vundef.
 Proof.
   intros X; eapply transfer_regs_dead; intuition eauto.
   eapply X. eapply Regset.elements_2. 
   rewrite -> SetoidList_InA_eq_equiv; eauto.
 Qed.
 
-Local Hint Resolve tr_inputs_exit Regset.mem_2 Regset.mem_1: core.
+Local Hint Resolve tr_pre_inputs Regset.mem_2 Regset.mem_1: core.
 
 Lemma tr_inputs_get f tbl or rs r:
-  (tr_inputs f tbl or rs)#r = if Regset.mem r (inputs_exit f tbl or) then rs#r else Vundef.
+  (tr_inputs f tbl or rs)#r = if Regset.mem r (pre_inputs f tbl or) then rs#r else Vundef.
 Proof.
   autodestruct; eauto.
   intros; apply tr_inputs_dead; eauto.
@@ -496,13 +503,15 @@ Proof.
   congruence.
 Qed.
 
+(* TODO: not yet used
 Lemma tr_inputs_ext f tbl or rs1 rs2:
-  (forall r, Regset.In r (inputs_exit f tbl or) -> rs1#r = rs2#r) ->
+  (forall r, Regset.In r (pre_inputs f tbl or) -> rs1#r = rs2#r) ->
   (forall r, (tr_inputs f tbl or rs1)#r = (tr_inputs f tbl or rs2)#r).
 Proof.
   intros EQ r. rewrite !tr_inputs_get.
   autodestruct; auto.
 Qed.
+*)
 
 Definition fsem (p: program) :=
   Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p).
@@ -524,7 +533,7 @@ Definition tr_regs: function -> final -> regset -> regset :=
 
 (* TODO: NOT USEFUL ?
 Definition liveout: function -> final -> Regset.t :=
-  poly_tr inputs_exit.
+  poly_tr pre_inputs.
 
 Lemma tr_regs_liveout_equiv f fi : tr_regs f fi = transfer_regs (Regset.elements (liveout f fi)).
 Proof.
@@ -535,30 +544,34 @@ Local Hint Resolve tr_inputs_get: core.
 
 Lemma tr_regs_get f fi rs r: (tr_regs f fi rs)#r = if Regset.mem r (liveout f fi) then rs#r else Vundef.
 Proof.
-   Local Opaque inputs_exit.
+   Local Opaque pre_inputs.
    destruct fi; simpl; auto.
 Qed.
 *)
 
-(* * Reasoning modulo extensionality of [regset] into BTL semantics *)
+(* * Comparing BTL semantics modulo extensionality of [regset].
+
+NB: This is at least used in BTL_SEtheory (and probably in the future BTL_SchedulerProof).
+
+*)
 Inductive equiv_stackframe: stackframe -> stackframe -> Prop :=
-  | equiv_stackframe_intro res f sp pc rs1 rs2
-      (EQUIV: forall r : positive, rs1 !! r = rs2 !! r):
-      equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
+  | equiv_stackframe_intro res f sp pc (rs1 rs2: regset)
+      (EQUIV: forall r, rs1#r = rs2#r)
+      :equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
   .
 
 Inductive equiv_state: state -> state -> Prop :=
-  | State_equiv stack f sp pc rs1 m rs2
-     (EQUIV: forall r, rs1#r = rs2#r): 
-     equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m)
-  | Call_equiv stk stk' f args m
-      (STACKS: list_forall2 equiv_stackframe stk stk'):
-      equiv_state (Callstate stk f args m) (Callstate stk' f args m)
-  | Return_equiv stk stk' v m
-      (STACKS: list_forall2 equiv_stackframe stk stk'):
-      equiv_state (Returnstate stk v m) (Returnstate stk' v m)
+  | State_equiv stk1 stk2 f sp pc rs1 m rs2
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      (EQUIV: forall r, rs1#r = rs2#r)
+      :equiv_state (State stk1 f sp pc rs1 m) (State stk2 f sp pc rs2 m)
+  | Call_equiv stk1 stk2 f args m
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      :equiv_state (Callstate stk1 f args m) (Callstate stk2 f args m)
+  | Return_equiv stk1 stk2 v m
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      :equiv_state (Returnstate stk1 v m) (Returnstate stk2 v m)
   .
-
 Local Hint Constructors equiv_stackframe equiv_state: core.
 
 Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf.
@@ -571,10 +584,10 @@ Proof.
   Local Hint Resolve equiv_stackframe_refl: core.
   induction stk; simpl; constructor; auto.
 Qed.
+Local Hint Resolve equiv_stack_refl: core.
 
 Lemma equiv_state_refl s: equiv_state s s.
 Proof.
-  Local Hint Resolve equiv_stack_refl: core.
   induction s; simpl; constructor; auto.
 Qed.
 
@@ -584,13 +597,13 @@ Proof.
   destruct 1; intros EQ; inv EQ; try econstructor; eauto.
   intros; eapply eq_trans; eauto.
 Qed.
+Local Hint Resolve equiv_stackframe_trans: core.
 
 Lemma equiv_stack_trans stk1 stk2:
   list_forall2 equiv_stackframe stk1 stk2 -> 
   forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
   list_forall2 equiv_stackframe stk1 stk3.
 Proof.
-  Local Hint Resolve equiv_stackframe_trans: core.
   induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
 Qed.
 
@@ -611,7 +624,220 @@ Proof.
   - repeat (rewrite Regmap.gso); auto.
 Qed.
 
+(* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation.
 
+We start by extending the previous [equiv_*] stuff for [Val.lessdef]: we need to also compare memories 
+for Mem.extends, because Vundef values are propagated in memory through stores, allocation, etc.
+
+*)
+
+Inductive lessdef_stackframe: stackframe -> stackframe -> Prop :=
+  | lessdef_stackframe_intro res f sp pc rs1 rs2
+      (REGS: forall r, Val.lessdef rs1#r rs2#r)
+      :lessdef_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
+  .
+
+Inductive lessdef_state: state -> state -> Prop :=
+  | State_lessdef stk1 stk2 f sp pc rs1 m1 rs2 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (REGS: forall r, Val.lessdef rs1#r rs2#r)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (State stk1 f sp pc rs1 m1) (State stk2 f sp pc rs2 m2)
+  | Call_lessdef stk1 stk2 f args1 args2 m1 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (ARGS: Val.lessdef_list args1 args2)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (Callstate stk1 f args1 m1) (Callstate stk2 f args2 m2)
+  | Return_lessdef stk1 stk2 v1 v2 m1 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (REGS: Val.lessdef v1 v2)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (Returnstate stk1 v1 m1) (Returnstate stk2 v2 m2)
+  .
+Local Hint Constructors lessdef_stackframe lessdef_state: core.
+
+Lemma lessdef_stackframe_refl stf: lessdef_stackframe stf stf.
+Proof.
+  destruct stf; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stackframe_refl: core.
+Lemma lessdef_stack_refl stk: list_forall2 lessdef_stackframe stk stk.
+Proof.
+  induction stk; simpl; constructor; auto.
+Qed.
+
+Local Hint Resolve lessdef_stack_refl: core.
+
+Lemma lessdef_list_refl args: Val.lessdef_list args args.
+Proof.
+  induction args; simpl; auto.
+Qed.
+
+Local Hint Resolve lessdef_list_refl Mem.extends_refl: core.
+
+Lemma lessdef_state_refl s: lessdef_state s s.
+Proof.
+  induction s; simpl; constructor; auto.
+Qed.
+
+Local Hint Resolve Val.lessdef_trans: core.
+Lemma lessdef_stackframe_trans stf1 stf2 stf3:
+  lessdef_stackframe stf1 stf2 -> lessdef_stackframe stf2 stf3 -> lessdef_stackframe stf1 stf3.
+Proof.
+  destruct 1. intros LD; inv LD; try econstructor; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stackframe_trans: core.
+Lemma lessdef_stack_trans stk1 stk2:
+  list_forall2 lessdef_stackframe stk1 stk2 -> 
+  forall stk3, list_forall2 lessdef_stackframe stk2 stk3 -> 
+  list_forall2 lessdef_stackframe stk1 stk3.
+Proof.
+  induction 1; intros stk3 LD; inv LD; econstructor; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stack_trans Mem.extends_extends_compose Val.lessdef_list_trans: core.
+Lemma lessdef_state_trans s1 s2 s3: lessdef_state s1 s2 -> lessdef_state s2 s3 -> lessdef_state s1 s3.
+Proof.
+  destruct 1; intros LD; inv LD; econstructor; eauto.
+Qed.
+
+Lemma init_regs_lessdef_preserv args1 args2
+  (ARGS : Val.lessdef_list args1 args2)
+  : forall rl r, Val.lessdef (init_regs args1 rl)#r (init_regs args2 rl)#r.
+Proof.
+  induction ARGS; simpl; auto.
+  intros rl r1; destruct rl; simpl in *; auto.
+  eapply set_reg_lessdef; eauto.
+  intros r2; eauto.
+Qed.
+Local Hint Resolve init_regs_lessdef_preserv: core.
+
+Lemma tr_inputs_lessdef f rs1 rs2 tbl or r
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  :Val.lessdef (tr_inputs f tbl or rs1)#r (tid f tbl or rs2)#r.
+Proof.
+  unfold tid; rewrite tr_inputs_get.
+  autodestruct.
+Qed.
+Local Hint Resolve tr_inputs_lessdef: core.
+
+Lemma find_function_lessdef ge ros rs1 rs2 fd
+  (FIND: find_function ge ros rs1 = Some fd)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  : find_function ge ros rs2 = Some fd.
+Proof.
+  destruct ros; simpl in *; auto.
+  exploit Genv.find_funct_inv; eauto.
+  intros (b & EQ).
+  destruct (REGS r); try congruence.
+Qed.
+Local Hint Resolve find_function_lessdef regs_lessdef_regs: core.
+
+
+Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of
+  (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of)
+  rs2 m2
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS: Mem.extends m1 m2)
+  : exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) 
+     /\ (forall r, Val.lessdef rs1'#r rs2'#r)
+     /\ (Mem.extends m1' m2').
+Proof.
+  induction ISTEP; simpl; try_simplify_someHyps.
+Admitted.
+
+Local Hint Constructors final_step list_forall2: core.
+Local Hint Unfold regs_lessdef: core.
+
+Lemma fsem2cfgsem_finalstep_simu ge stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2
+  (FSTEP: final_step tr_inputs ge stk1 f sp rs1 m1 fin t s1)
+  (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS: Mem.extends m1 m2)
+  : exists s2, final_step tid ge stk2 f sp rs2 m2 fin t s2
+               /\ lessdef_state s1 s2.
+Proof.
+  destruct FSTEP; try (eexists; split; simpl; econstructor; eauto; fail).
+  - (* return *)
+    exploit Mem.free_parallel_extends; eauto.
+    intros (m2' & FREE & MEMS2).
+    eexists; split; simpl; econstructor; eauto.
+    destruct or; simpl; auto.
+  - (* tailcall *)
+    exploit Mem.free_parallel_extends; eauto.
+    intros (m2' & FREE & MEMS2).
+    eexists; split; simpl; econstructor; eauto.
+  - (* builtin *)
+    exploit (eval_builtin_args_lessdef (ge:=ge) (e1:=(fun r => rs1 # r)) (fun r => rs2 # r)); eauto.
+    intros (vl2' & BARGS & VARGS).
+    exploit external_call_mem_extends; eauto.
+    intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED).
+    eexists; split; simpl; econstructor; eauto.
+    intros; apply set_res_lessdef; eauto.
+  - (* jumptable *)
+    eexists; split; simpl; econstructor; eauto.
+    destruct (REGS arg); try congruence.
+Qed.
+
+Lemma fsem2cfgsem_ibstep_simu ge stk1 stk2 f sp rs1 m1 ib t s1 rs2 m2
+  (STEP: iblock_step tr_inputs ge stk1 f sp rs1 m1 ib t s1)
+  (STACKS : list_forall2 lessdef_stackframe stk1 stk2)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS : Mem.extends m1 m2)
+  : exists s2, iblock_step tid ge stk2 f sp rs2 m2 ib t s2
+               /\ lessdef_state s1 s2.
+Proof.
+  destruct STEP as (rs1' & m1' & fin & ISTEP & FSTEP).
+  exploit fsem2cfgsem_ibistep_simu; eauto.
+  intros (rs2' & m2' & ISTEP2 & REGS2 & MEMS2).
+  rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP REGS MEMS.
+  exploit fsem2cfgsem_finalstep_simu; eauto.
+  intros (s2 & FSTEP2 & LESSDEF). clear FSTEP.
+  unfold iblock_step; eexists; split; eauto.
+Qed.
+
+Local Hint Constructors step: core.
+
+Lemma fsem2cfgsem_step_simu ge s1 t s1' s2
+ (STEP: step tr_inputs ge s1 t s1')
+ (REGS: lessdef_state s1 s2)
+ :exists s2' : state,
+   step tid ge s2 t s2' /\
+   lessdef_state s1' s2'.
+Proof.
+  destruct STEP; inv REGS.
+  - (* iblock *)
+    intros; exploit fsem2cfgsem_ibstep_simu; eauto. clear STEP.
+    intros (s2 & STEP2 & REGS2).
+    eexists; split; eauto.
+  - (* internal call *)
+    exploit (Mem.alloc_extends m m2 0 (fn_stacksize f) stk m' 0 (fn_stacksize f)); eauto.
+    1-2: lia.
+    intros (m2' & ALLOC2 & MEMS2). clear ALLOC MEMS.
+    eexists; split; econstructor; eauto.
+  - (* external call *)
+    exploit external_call_mem_extends; eauto.
+    intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). clear EXTCALL MEMS.
+    eexists; split; econstructor; eauto.
+  - (* return *)
+    inversion STACKS as [|d1 d2 d3 d4 STF2 STK2]. subst.
+    inv STF2.
+    eexists; split; econstructor; eauto.
+    intros; eapply set_reg_lessdef; eauto.
+Qed.
+
+Theorem fsem2cfgsem prog:
+  forward_simulation (fsem prog) (cfgsem prog).
+Proof.
+  eapply forward_simulation_step with lessdef_state; simpl; auto.
+  - destruct 1; intros; eexists; intuition eauto. econstructor; eauto.
+  - intros s1 s2 r REGS FINAL; destruct FINAL.
+     inv REGS; inv STACKS; inv REGS0.
+     econstructor; eauto.
+  - intros; eapply fsem2cfgsem_step_simu; eauto.
+Qed.
 
 (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)