From 22c73e96f9dfb4120541ee5e11334d0ba2d38fe8 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Jan 2020 07:04:13 +0100
Subject: begin lattice

---
 backend/ForwardMoves.v | 57 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)
 create mode 100644 backend/ForwardMoves.v

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
new file mode 100644
index 00000000..420e71f9
--- /dev/null
+++ b/backend/ForwardMoves.v
@@ -0,0 +1,57 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Module RELATION.
+  
+Definition t := (PTree.t reg).
+Definition eq (r1 r2 : t) :=
+  forall x, (PTree.get x r1) = (PTree.get x r2).
+
+Lemma eq_refl: forall x, eq x x.
+Proof.
+  unfold eq.
+  intros; reflexivity.
+Qed.
+
+Lemma eq_sym: forall x y, eq x y -> eq y x.
+Proof.
+  unfold eq.
+  intros; eauto.
+Qed.
+
+Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
+Proof.
+  unfold eq.
+  intros; congruence.
+Qed.
+
+Definition reg_beq (x y : reg) :=
+  if Pos.eq_dec x y then true else false.
+
+Definition beq (r1 r2 : t) := PTree.beq reg_beq r1 r2.
+
+Lemma beq_correct: forall r1 r2, beq r1 r2 = true -> eq r1 r2.
+Proof.
+  unfold beq, eq. intros r1 r2 EQ x.
+  pose proof (PTree.beq_correct reg_beq r1 r2) as CORRECT.
+  destruct CORRECT as [CORRECTF CORRECTB].
+  pose proof (CORRECTF EQ x) as EQx.
+  clear CORRECTF CORRECTB EQ.
+  unfold reg_beq in *.
+  destruct (r1 ! x) as [R1x | ] in *;
+    destruct (r2 ! x) as [R2x | ] in *;
+    trivial; try contradiction.
+  destruct (Pos.eq_dec R1x R2x) in *; congruence.
+Qed.
+
+(*
+  Parameter ge: t -> t -> Prop.
+  Axiom ge_refl: forall x y, eq x y -> ge x y.
+  Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Parameter bot: t.
+  Axiom ge_bot: forall x, ge x bot.
+  Parameter lub: t -> t -> t.
+  Axiom ge_lub_left: forall x y, ge (lub x y) x.
+  Axiom ge_lub_right: forall x y, ge (lub x y) y.
+*)
\ No newline at end of file
-- 
cgit 


From b24140ca3257e9d77df8dcea22172a4b06679243 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Jan 2020 08:50:46 +0100
Subject: continue implementing semilattice

---
 backend/ForwardMoves.v | 72 +++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 65 insertions(+), 7 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 420e71f9..2a135768 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -45,13 +45,71 @@ Proof.
   destruct (Pos.eq_dec R1x R2x) in *; congruence.
 Qed.
 
+Definition ge (r1 r2 : t) :=
+  forall x,
+    match PTree.get x r1 with
+    | None => True
+    | Some v => (PTree.get x r2) = Some v
+    end.
+
+Lemma ge_refl: forall r1 r2, eq r1 r2 -> ge r1 r2.
+Proof.
+  unfold eq, ge.
+  intros r1 r2 EQ x.
+  pose proof (EQ x) as EQx.
+  clear EQ.
+  destruct (r1 ! x).
+  - congruence.
+  - trivial.
+Qed.
+
+Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+Proof.
+  unfold ge.
+  intros r1 r2 r3 GE12 GE23 x.
+  pose proof (GE12 x) as GE12x; clear GE12.
+  pose proof (GE23 x) as GE23x; clear GE23.
+  destruct (r1 ! x); trivial.
+  destruct (r2 ! x); congruence.
+Qed.
+
+Definition lub (r1 r2 : t) :=
+  PTree.combine
+    (fun ov1 ov2 =>
+       match ov1, ov2 with
+       | (Some v1), (Some v2) =>
+         if Pos.eq_dec v1 v2
+         then ov1
+         else None
+       | None, _
+       | _, None => None
+       end)
+    r1 r2.
+
+Lemma ge_lub_left: forall x y, ge (lub x y) x.
+Proof.
+  unfold ge, lub.
+  intros r1 r2 x.
+  rewrite PTree.gcombine by reflexivity.
+  destruct (_ ! _); trivial.
+  destruct (_ ! _); trivial.
+  destruct (Pos.eq_dec _ _); trivial.
+Qed.
+
+Lemma ge_lub_right: forall x y, ge (lub x y) y.
+Proof.
+  unfold ge, lub.
+  intros r1 r2 x.
+  rewrite PTree.gcombine by reflexivity.
+  destruct (_ ! _); trivial.
+  destruct (_ ! _); trivial.
+  destruct (Pos.eq_dec _ _); trivial.
+  congruence.
+Qed.
+
+End RELATION.
+
 (*
-  Parameter ge: t -> t -> Prop.
-  Axiom ge_refl: forall x y, eq x y -> ge x y.
-  Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
   Parameter bot: t.
   Axiom ge_bot: forall x, ge x bot.
-  Parameter lub: t -> t -> t.
-  Axiom ge_lub_left: forall x y, ge (lub x y) x.
-  Axiom ge_lub_right: forall x y, ge (lub x y) y.
-*)
\ No newline at end of file
+ *)
-- 
cgit 


From 963286169bf5fb31d70377f8dfccbf7470a32212 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Jan 2020 09:34:02 +0100
Subject: more on semilattices (ADD_BOTTOM)

---
 backend/ForwardMoves.v | 118 +++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 114 insertions(+), 4 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 2a135768..317ffd8c 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -109,7 +109,117 @@ Qed.
 
 End RELATION.
 
-(*
-  Parameter bot: t.
-  Axiom ge_bot: forall x, ge x bot.
- *)
+Module Type SEMILATTICE_WITHOUT_BOTTOM.
+
+  Parameter t: Type.
+  Parameter eq: t -> t -> Prop.
+  Axiom eq_refl: forall x, eq x x.
+  Axiom eq_sym: forall x y, eq x y -> eq y x.
+  Axiom eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
+  Parameter beq: t -> t -> bool.
+  Axiom beq_correct: forall x y, beq x y = true -> eq x y.
+  Parameter ge: t -> t -> Prop.
+  Axiom ge_refl: forall x y, eq x y -> ge x y.
+  Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Parameter lub: t -> t -> t.
+  Axiom ge_lub_left: forall x y, ge (lub x y) x.
+  Axiom ge_lub_right: forall x y, ge (lub x y) y.
+
+End SEMILATTICE_WITHOUT_BOTTOM.
+
+Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM) : SEMILATTICE.
+  Definition t := option L.t.
+  Definition eq (a b : t) :=
+    match a, b with
+    | None, None => True
+    | Some x, Some y => L.eq x y
+    | Some _, None | None, Some _ => False
+    end.
+  
+  Lemma eq_refl: forall x, eq x x.
+  Proof.
+    unfold eq; destruct x; trivial.
+    apply L.eq_refl.
+  Qed.
+
+  Lemma eq_sym: forall x y, eq x y -> eq y x.
+  Proof.
+    unfold eq; destruct x; destruct y; trivial.
+    apply L.eq_sym.
+  Qed.
+  
+  Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
+  Proof.
+    unfold eq; destruct x; destruct y; destruct z; trivial.
+    - apply L.eq_trans.
+    - contradiction.
+  Qed.
+  
+  Definition beq (x y : t) :=
+    match x, y with
+    | None, None => true
+    | Some x, Some y => L.beq x y
+    | Some _, None | None, Some _ => false
+    end.
+  
+  Lemma beq_correct: forall x y, beq x y = true -> eq x y.
+  Proof.
+    unfold beq, eq.
+    destruct x; destruct y; trivial; try congruence.
+    apply L.beq_correct.
+  Qed.
+  
+  Definition ge (x y : t) :=
+    match x, y with
+    | None, Some _ => False
+    | _, None => True
+    | Some a, Some b => L.ge a b
+    end.
+  
+  Lemma ge_refl: forall x y, eq x y -> ge x y.
+  Proof.
+    unfold eq, ge.
+    destruct x; destruct y; trivial.
+    apply L.ge_refl.
+  Qed.
+  
+  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Proof.
+    unfold ge.
+    destruct x; destruct y; destruct z; trivial; try contradiction.
+    apply L.ge_trans.
+  Qed.
+  
+  Definition bot: t := None.
+  Lemma ge_bot: forall x, ge x bot.
+  Proof.
+    unfold ge, bot.
+    destruct x; trivial.
+  Qed.
+  
+  Definition lub (a b : t) :=
+    match a, b with
+    | None, _ => b
+    | _, None => a
+    | (Some x), (Some y) => Some (L.lub x y)
+    end.
+
+  Lemma ge_lub_left: forall x y, ge (lub x y) x.
+  Proof.
+    unfold ge, lub.
+    destruct x; destruct y; trivial.
+    - apply L.ge_lub_left.
+    - apply L.ge_refl.
+      apply L.eq_refl.
+  Qed.
+  
+  Lemma ge_lub_right: forall x y, ge (lub x y) y.
+  Proof.
+    unfold ge, lub.
+    destruct x; destruct y; trivial.
+    - apply L.ge_lub_right.
+    - apply L.ge_refl.
+      apply L.eq_refl.
+  Qed.
+End ADD_BOTTOM.
+
-- 
cgit 


From a5be6f574c3b001254c9b370762045f1675702c1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Jan 2020 11:16:50 +0100
Subject: transfer function

---
 backend/ForwardMoves.v | 45 ++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 44 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 317ffd8c..ae836c1a 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -8,6 +8,8 @@ Definition t := (PTree.t reg).
 Definition eq (r1 r2 : t) :=
   forall x, (PTree.get x r1) = (PTree.get x r2).
 
+Definition top : t := PTree.empty reg.
+
 Lemma eq_refl: forall x, eq x x.
 Proof.
   unfold eq.
@@ -127,7 +129,7 @@ Module Type SEMILATTICE_WITHOUT_BOTTOM.
 
 End SEMILATTICE_WITHOUT_BOTTOM.
 
-Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM) : SEMILATTICE.
+Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM).
   Definition t := option L.t.
   Definition eq (a b : t) :=
     match a, b with
@@ -223,3 +225,44 @@ Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM) : SEMILATTICE.
   Qed.
 End ADD_BOTTOM.
 
+Module RB := ADD_BOTTOM(RELATION).
+Module DS := Dataflow_Solver(RB)(NodeSetForward).
+
+Definition kill (dst : reg) (rel : RELATION.t) :=
+  PTree.remove dst rel.
+
+Definition move (src dst : reg) (rel : RELATION.t) :=
+  PTree.set dst src rel.
+
+Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) :=
+  match res with
+  | BR z => kill z rel
+  | BR_none => rel
+  | BR_splitlong hi lo => kill_builtin_res hi (kill_builtin_res lo rel)
+  end.
+
+Definition apply_instr instr x :=
+  match instr with
+  | Inop _
+  | Istore _ _ _ _ _ => Some x
+  | Iop Omove (src :: nil) dst _ => Some (move src dst x)
+  | Iop _ _ dst _
+  | Iload _ _ _ _ dst _
+  | Icall _ _ _ dst _ => Some (kill dst x)
+  | Ibuiltin _ _ res _ => Some (kill_builtin_res res x)
+  | Icond _ _ _ _ | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot
+  end.
+
+Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t :=
+  match ro with
+  | None => None
+  | Some x =>
+    match code ! pc with
+    | None => RB.bot
+    | Some instr => apply_instr instr x
+    end
+  end.
+
+Definition forward_map (f : RTL.function) := DS.fixpoint
+  (RTL.fn_code f) RTL.successors_instr
+  (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
\ No newline at end of file
-- 
cgit 


From 80395b0b52beac8edafb7c4d748a3d4d45bd3fa7 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Jan 2020 11:41:31 +0100
Subject: I *think* the transformation is now done

---
 backend/ForwardMoves.v | 59 ++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 57 insertions(+), 2 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index ae836c1a..b812b22d 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -2,6 +2,8 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
 Require Import AST Linking.
 Require Import Memory Registers Op RTL Maps.
 
+(* Static analysis *)
+
 Module RELATION.
   
 Definition t := (PTree.t reg).
@@ -232,7 +234,10 @@ Definition kill (dst : reg) (rel : RELATION.t) :=
   PTree.remove dst rel.
 
 Definition move (src dst : reg) (rel : RELATION.t) :=
-  PTree.set dst src rel.
+  PTree.set dst (match PTree.get src rel with
+                 | Some src' => src'
+                 | None => src
+                 end) rel.
 
 Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) :=
   match res with
@@ -265,4 +270,54 @@ Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t :=
 
 Definition forward_map (f : RTL.function) := DS.fixpoint
   (RTL.fn_code f) RTL.successors_instr
-  (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
\ No newline at end of file
+  (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
+
+Definition subst_arg (rel : RELATION.t) (x : reg) : reg :=
+  match PTree.get x rel with
+  | None => x
+  | Some src => src
+  end.
+
+Definition subst_args rel := List.map (subst_arg rel).
+
+(* Transform *)
+Definition transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) :=
+  match fmap !! pc with
+  | None => instr
+  | Some rel =>
+    match instr with
+    | Iop op args dst s =>
+      Iop op (subst_args rel args) dst s
+    | Iload trap chunk addr args dst s =>
+      Iload trap chunk addr (subst_args rel args) dst s
+    | Icall sig ros args dst s =>
+      Icall sig ros (subst_args rel args) dst s
+    | Itailcall sig ros args =>
+      Itailcall sig ros (subst_args rel args)
+    | Icond cond args s1 s2 =>
+      Icond cond (subst_args rel args) s1 s2
+    | Ijumptable arg tbl =>
+      Ijumptable (subst_arg rel arg) tbl
+    | Ireturn (Some arg) =>
+      Ireturn (Some (subst_arg rel arg))
+    | _ => instr
+    end
+  end.
+
+Definition transf_function (f: function) : function :=
+  match forward_map f with
+  | None => f (* can't analyze due to errors ?! *)
+  | Some fmap =>
+    {| fn_sig := f.(fn_sig);
+       fn_params := f.(fn_params);
+       fn_stacksize := f.(fn_stacksize);
+       fn_code := PTree.map (transf_instr fmap) f.(fn_code);
+       fn_entrypoint := f.(fn_entrypoint) |}
+  end.
+
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
-- 
cgit 


From 44e97d0614bf1d66147aa9a09c1b04278ce80e87 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Jan 2020 13:16:27 +0100
Subject: bogus proof

---
 backend/ForwardMovesproof.v | 141 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 141 insertions(+)
 create mode 100644 backend/ForwardMovesproof.v

(limited to 'backend')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
new file mode 100644
index 00000000..936e9e56
--- /dev/null
+++ b/backend/ForwardMovesproof.v
@@ -0,0 +1,141 @@
+Require Import FunInd.
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import ForwardMoves.
+
+
+Definition match_prog (p tp: RTL.program) :=
+  match_program (fun ctx f tf => tf = transf_fundef f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_prog p (transf_program p).
+Proof.
+  intros. eapply match_transform_program; eauto.
+Qed.
+
+Section PRESERVATION.
+
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_transf TRANSL).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  Genv.find_funct_ptr tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_ptr_transf TRANSL).
+
+Lemma symbols_preserved:
+  forall id,
+  Genv.find_symbol tge id = Genv.find_symbol ge id.
+Proof (Genv.find_symbol_transf TRANSL).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_transf TRANSL).
+
+Lemma sig_preserved:
+  forall f, funsig (transf_fundef f) = funsig f.
+Proof.
+  destruct f; trivial.
+  simpl.
+  unfold transf_function.
+  destruct (forward_map _); reflexivity.
+Qed.
+
+Lemma find_function_translated:
+  forall ros rs fd,
+  find_function ge ros rs = Some fd ->
+  find_function tge ros rs = Some (transf_fundef fd).
+Proof.
+  unfold find_function; intros. destruct ros as [r|id].
+  eapply functions_translated; eauto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
+  eapply function_ptr_translated; eauto.
+Qed.
+
+(*
+Lemma transf_function_at:
+  forall f pc i,
+  f.(fn_code)!pc = Some i ->
+  (transf_function f).(fn_code)!pc = Some(transf_instr pc i).
+Proof.
+  intros until i. intro Hcode.
+  unfold transf_function; simpl.
+  rewrite PTree.gmap.
+  unfold option_map.
+  rewrite Hcode.
+  reflexivity.
+Qed.
+
+Ltac TR_AT :=
+  match goal with
+  | [ A: (fn_code _)!_ = Some _ |- _ ] =>
+        generalize (transf_function_at _ _ _ A); intros
+  end.
+*)
+
+Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
+  | match_frames_intro: forall res f sp pc rs,
+      match_frames (Stackframe res f sp pc rs)
+                   (Stackframe res (transf_function f) sp pc rs).
+
+Inductive match_states: RTL.state -> RTL.state -> Prop :=
+  | match_regular_states: forall stk f sp pc rs m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (State stk f sp pc rs m)
+                   (State stk' (transf_function f) sp pc rs m)
+  | match_callstates: forall stk f args m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Callstate stk f args m)
+                   (Callstate stk' (transf_fundef f) args m)
+  | match_returnstates: forall stk v m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Returnstate stk v m)
+                   (Returnstate stk' v m).
+
+Lemma step_simulation:
+  forall S1 t S2, RTL.step ge S1 t S2 ->
+  forall S1', match_states S1 S1' ->
+  exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
+Admitted.
+
+Lemma transf_initial_states:
+  forall S1, RTL.initial_state prog S1 ->
+  exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2.
+Proof.
+  intros. inv H. econstructor; split.
+  econstructor.
+    eapply (Genv.init_mem_transf TRANSL); eauto.
+    rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto.
+    eapply function_ptr_translated; eauto.
+    rewrite <- H3; apply sig_preserved.
+  constructor. constructor.
+Qed.
+
+Lemma transf_final_states:
+  forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
+Proof.
+  eapply forward_simulation_step.
+  apply senv_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact step_simulation.
+Qed.
+
+End PRESERVATION.
-- 
cgit 


From bc29d9b7abd397e30bd4a9cc5b1f43b9cec409bc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Jan 2020 19:37:04 +0100
Subject: progressing towards a proof

---
 backend/ForwardMoves.v      |  71 +++++++++++++------------
 backend/ForwardMovesproof.v | 126 +++++++++++++++++++++++++++++++++++++++-----
 2 files changed, 150 insertions(+), 47 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index b812b22d..47fd2457 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -272,48 +272,51 @@ Definition forward_map (f : RTL.function) := DS.fixpoint
   (RTL.fn_code f) RTL.successors_instr
   (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
 
-Definition subst_arg (rel : RELATION.t) (x : reg) : reg :=
-  match PTree.get x rel with
+Definition get_rb (rb : RB.t) (x : reg) :=
+  match rb with
   | None => x
-  | Some src => src
+  | Some rel =>
+    match PTree.get x rel with
+    | None => x
+    | Some src => src
+    end
+  end.
+
+Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg :=
+  match fmap with
+  | None => x
+  | Some inv => get_rb (PMap.get pc inv) x
   end.
 
-Definition subst_args rel := List.map (subst_arg rel).
+Definition subst_args fmap pc := List.map (subst_arg fmap pc).
 
 (* Transform *)
-Definition transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) :=
-  match fmap !! pc with
-  | None => instr
-  | Some rel =>
-    match instr with
-    | Iop op args dst s =>
-      Iop op (subst_args rel args) dst s
-    | Iload trap chunk addr args dst s =>
-      Iload trap chunk addr (subst_args rel args) dst s
-    | Icall sig ros args dst s =>
-      Icall sig ros (subst_args rel args) dst s
-    | Itailcall sig ros args =>
-      Itailcall sig ros (subst_args rel args)
-    | Icond cond args s1 s2 =>
-      Icond cond (subst_args rel args) s1 s2
-    | Ijumptable arg tbl =>
-      Ijumptable (subst_arg rel arg) tbl
-    | Ireturn (Some arg) =>
-      Ireturn (Some (subst_arg rel arg))
-    | _ => instr
-    end
+Definition transf_instr (fmap : option (PMap.t RB.t))
+           (pc: node) (instr: instruction) :=
+  match instr with
+  | Iop op args dst s =>
+    Iop op (subst_args fmap pc args) dst s
+  | Iload trap chunk addr args dst s =>
+    Iload trap chunk addr (subst_args fmap pc args) dst s
+  | Icall sig ros args dst s =>
+    Icall sig ros (subst_args fmap pc args) dst s
+  | Itailcall sig ros args =>
+    Itailcall sig ros (subst_args fmap pc args)
+  | Icond cond args s1 s2 =>
+    Icond cond (subst_args fmap pc args) s1 s2
+  | Ijumptable arg tbl =>
+    Ijumptable (subst_arg fmap pc arg) tbl
+  | Ireturn (Some arg) =>
+    Ireturn (Some (subst_arg fmap pc arg))
+  | _ => instr
   end.
 
 Definition transf_function (f: function) : function :=
-  match forward_map f with
-  | None => f (* can't analyze due to errors ?! *)
-  | Some fmap =>
-    {| fn_sig := f.(fn_sig);
-       fn_params := f.(fn_params);
-       fn_stacksize := f.(fn_stacksize);
-       fn_code := PTree.map (transf_instr fmap) f.(fn_code);
-       fn_entrypoint := f.(fn_entrypoint) |}
-  end.
+  {| fn_sig := f.(fn_sig);
+     fn_params := f.(fn_params);
+     fn_stacksize := f.(fn_stacksize);
+     fn_code := PTree.map (transf_instr (forward_map f)) f.(fn_code);
+     fn_entrypoint := f.(fn_entrypoint) |}.
 
 
 Definition transf_fundef (fd: fundef) : fundef :=
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 936e9e56..c56ba042 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -47,9 +47,6 @@ Lemma sig_preserved:
   forall f, funsig (transf_fundef f) = funsig f.
 Proof.
   destruct f; trivial.
-  simpl.
-  unfold transf_function.
-  destruct (forward_map _); reflexivity.
 Qed.
 
 Lemma find_function_translated:
@@ -63,35 +60,58 @@ Proof.
   eapply function_ptr_translated; eauto.
 Qed.
 
-(*
 Lemma transf_function_at:
   forall f pc i,
   f.(fn_code)!pc = Some i ->
-  (transf_function f).(fn_code)!pc = Some(transf_instr pc i).
+  (transf_function f).(fn_code)!pc =
+    Some(transf_instr (forward_map f) pc i).
 Proof.
-  intros until i. intro Hcode.
+  intros until i. intro CODE.
   unfold transf_function; simpl.
   rewrite PTree.gmap.
   unfold option_map.
-  rewrite Hcode.
+  rewrite CODE.
+  reflexivity.
+Qed.
+
+Definition fmap_sem (fmap : option (PMap.t RB.t)) (pc : node) (rs : regset) :=
+  forall x : reg,
+    (rs # (subst_arg fmap pc x)) = (rs # x).
+
+Lemma apply_instr'_bot :
+  forall code,
+  forall pc,
+    RB.eq (apply_instr' code pc RB.bot) RB.bot.
+Proof.
   reflexivity.
 Qed.
 
+(*Lemma fmap_sem_step :
+  forall f : function,
+  forall pc pc' : node,
+  forall instr,
+    (f.fn_code ! pc) = Some instr ->
+    In pc' (successors_instr instr) ->
+    (fmap_sem (forward_map f) pc rs) ->
+    (fmap_sem (forward_map f) pc' rs').
+ *)
+
 Ltac TR_AT :=
   match goal with
   | [ A: (fn_code _)!_ = Some _ |- _ ] =>
         generalize (transf_function_at _ _ _ A); intros
   end.
-*)
 
 Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
-  | match_frames_intro: forall res f sp pc rs,
-      match_frames (Stackframe res f sp pc rs)
-                   (Stackframe res (transf_function f) sp pc rs).
+| match_frames_intro: forall res f sp pc rs,
+    (fmap_sem (forward_map f) pc rs) ->
+    match_frames (Stackframe res f sp pc rs)
+                 (Stackframe res (transf_function f) sp pc rs).
 
 Inductive match_states: RTL.state -> RTL.state -> Prop :=
   | match_regular_states: forall stk f sp pc rs m stk'
-        (STACKS: list_forall2 match_frames stk stk'),
+                                 (STACKS: list_forall2 match_frames stk stk'),
+      (fmap_sem (forward_map f) pc rs) ->
       match_states (State stk f sp pc rs m)
                    (State stk' (transf_function f) sp pc rs m)
   | match_callstates: forall stk f args m stk'
@@ -106,8 +126,88 @@ Inductive match_states: RTL.state -> RTL.state -> Prop :=
 Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 ->
   forall S1', match_states S1 S1' ->
-  exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
+              exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
 Admitted.
+(*
+  induction 1; intros S1' MS; inv MS; try TR_AT.
+- (* nop *)
+  econstructor; split. eapply exec_Inop; eauto.
+  constructor; auto.
+- (* op *)
+  econstructor; split.
+  eapply exec_Iop with (v := v); eauto.
+  rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
+  constructor; auto.
+(* load *)
+- econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload; eauto.
+  constructor; auto.
+- (* load notrap1 *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = None).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload_notrap1; eauto.
+  constructor; auto.
+- (* load notrap2 *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload_notrap2; eauto.
+  constructor; auto. 
+- (* store *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Istore; eauto.
+  constructor; auto. 
+(* call *)
+- econstructor; split.
+  eapply exec_Icall with (fd := transf_fundef fd); eauto.
+    eapply find_function_translated; eauto.
+    apply sig_preserved.
+  constructor. constructor; auto. constructor.
+(* tailcall *)
+- econstructor; split.
+  eapply exec_Itailcall with (fd := transf_fundef fd); eauto.
+    eapply find_function_translated; eauto.
+    apply sig_preserved.
+  constructor. auto.
+(* builtin *)
+- econstructor; split.
+  eapply exec_Ibuiltin; eauto.
+    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  constructor; auto.
+(* cond *)
+- econstructor; split.
+  eapply exec_Icond; eauto.
+  constructor; auto.
+(* jumptbl *)
+- econstructor; split.
+  eapply exec_Ijumptable; eauto.
+  constructor; auto.
+(* return *)
+- econstructor; split.
+  eapply exec_Ireturn; eauto.
+  constructor; auto.
+(* internal function *)
+-  simpl. econstructor; split.
+  eapply exec_function_internal; eauto.
+  constructor; auto.
+(* external function *)
+- econstructor; split.
+  eapply exec_function_external; eauto.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  constructor; auto.
+(* return *)
+- inv STACKS. inv H1.
+  econstructor; split.
+  eapply exec_return; eauto.
+  constructor; auto.
+Qed.
+ *)
 
 Lemma transf_initial_states:
   forall S1, RTL.initial_state prog S1 ->
-- 
cgit 


From 2e8e84aea389d41332ebd5a569b474d3c1de23d6 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Jan 2020 20:31:41 +0100
Subject: correct semantics for bottom

---
 backend/ForwardMoves.v      | 12 +++++++-----
 backend/ForwardMovesproof.v | 47 ++++++++++++++++++++++++++++++++++++---------
 2 files changed, 45 insertions(+), 14 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 47fd2457..96a19ecd 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -272,14 +272,16 @@ Definition forward_map (f : RTL.function) := DS.fixpoint
   (RTL.fn_code f) RTL.successors_instr
   (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
 
+Definition get_r (rel : RELATION.t) (x : reg) :=
+  match PTree.get x rel with
+  | None => x
+  | Some src => src
+  end.
+
 Definition get_rb (rb : RB.t) (x : reg) :=
   match rb with
   | None => x
-  | Some rel =>
-    match PTree.get x rel with
-    | None => x
-    | Some src => src
-    end
+  | Some rel => get_r rel x
   end.
 
 Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg :=
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index c56ba042..4e24dab6 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -74,9 +74,11 @@ Proof.
   reflexivity.
 Qed.
 
+(*
 Definition fmap_sem (fmap : option (PMap.t RB.t)) (pc : node) (rs : regset) :=
   forall x : reg,
     (rs # (subst_arg fmap pc x)) = (rs # x).
+ *)
 
 Lemma apply_instr'_bot :
   forall code,
@@ -86,15 +88,42 @@ Proof.
   reflexivity.
 Qed.
 
-(*Lemma fmap_sem_step :
-  forall f : function,
-  forall pc pc' : node,
-  forall instr,
-    (f.fn_code ! pc) = Some instr ->
-    In pc' (successors_instr instr) ->
-    (fmap_sem (forward_map f) pc rs) ->
-    (fmap_sem (forward_map f) pc' rs').
- *)
+Definition get_rb_sem (rb : RB.t) (rs : regset) :=
+  match rb with
+  | None => False
+  | Some rel =>
+    forall x : reg,
+      (rs # (get_r rel x)) = (rs # x)
+  end.
+
+Lemma get_rb_sem_ge:
+  forall rb1 rb2 : RB.t,
+    (RB.ge rb1 rb2) ->
+    forall rs : regset,
+      (get_rb_sem rb2 rs) -> (get_rb_sem rb1 rs).
+Proof.
+  destruct rb1 as [r1 | ];
+    destruct rb2 as [r2 | ];
+    unfold get_rb_sem;
+    simpl;
+    intros GE rs RB2RS;
+    try contradiction.
+  unfold RELATION.ge in GE.
+  unfold get_r in *.
+  intro x.
+  pose proof (GE x) as GEx.
+  pose proof (RB2RS x) as RB2RSx.
+  destruct (r1 ! x) as [r1x | ] in *;
+    destruct (r2 ! x) as [r2x | ] in *;
+    congruence.
+Qed.
+
+Definition fmap_sem (fmap : option (PMap.t RB.t))
+  (pc : node) (rs : regset) :=
+  match fmap with
+  | None => True
+  | Some m => get_rb_sem (PMap.get pc m) rs
+  end.
 
 Ltac TR_AT :=
   match goal with
-- 
cgit 


From 5be5afc63935c9dc534fe153026ff1ac4326e7c5 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Jan 2020 22:00:23 +0100
Subject: moving forward in proofs

---
 backend/ForwardMovesproof.v | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 4e24dab6..34c3c688 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -156,12 +156,29 @@ Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 ->
   forall S1', match_states S1 S1' ->
               exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
-Admitted.
-(*
+Proof.
   induction 1; intros S1' MS; inv MS; try TR_AT.
 - (* nop *)
   econstructor; split. eapply exec_Inop; eauto.
   constructor; auto.
+  
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply get_rb_sem_ge with (rb2 := map # pc); trivial.
+  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
+  {
+    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+    2: apply apply_instr'_bot.
+    simpl. tauto.
+  }
+  unfold apply_instr'.
+  unfold get_rb_sem in *.
+  destruct (map # pc) in *; try contradiction.
+  rewrite H.
+  reflexivity.
+Admitted.
+(*
 - (* op *)
   econstructor; split.
   eapply exec_Iop with (v := v); eauto.
-- 
cgit 


From fd24564480c438da9456d781ec17bfa3ac6277c1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Jan 2020 22:46:55 +0100
Subject: progressing in proofs

---
 backend/ForwardMoves.v      |   2 +
 backend/ForwardMovesproof.v | 111 +++++++++++++++++++++++++++++++++++++++-----
 2 files changed, 101 insertions(+), 12 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 96a19ecd..65d66b16 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -300,6 +300,8 @@ Definition transf_instr (fmap : option (PMap.t RB.t))
     Iop op (subst_args fmap pc args) dst s
   | Iload trap chunk addr args dst s =>
     Iload trap chunk addr (subst_args fmap pc args) dst s
+  | Istore chunk addr args src s =>
+    Istore chunk addr (subst_args fmap pc args) src s
   | Icall sig ros args dst s =>
     Icall sig ros (subst_args fmap pc args) dst s
   | Itailcall sig ros args =>
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 34c3c688..28befed3 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -125,6 +125,40 @@ Definition fmap_sem (fmap : option (PMap.t RB.t))
   | Some m => get_rb_sem (PMap.get pc m) rs
   end.
 
+Lemma subst_arg_ok:
+  forall f,
+  forall pc,
+  forall rs,
+  forall arg,
+    fmap_sem (forward_map f) pc rs ->
+    rs # (subst_arg (forward_map f) pc arg) = rs # arg.
+Proof.
+  intros until arg.
+  intro SEM.
+  unfold fmap_sem in SEM.
+  destruct (forward_map f) as [map |]in *; trivial.
+  simpl.
+  unfold get_rb_sem in *.
+  destruct (map # pc).
+  2: contradiction.
+  apply SEM.
+Qed.
+
+Lemma subst_args_ok:
+  forall f,
+  forall pc,
+  forall rs,
+  fmap_sem (forward_map f) pc rs ->
+  forall args,
+    rs ## (subst_args (forward_map f) pc args) = rs ## args.
+Proof.
+  induction args; trivial.
+  simpl.
+  f_equal.
+  apply subst_arg_ok; assumption.
+  assumption.
+Qed.
+
 Ltac TR_AT :=
   match goal with
   | [ A: (fn_code _)!_ = Some _ |- _ ] =>
@@ -177,83 +211,136 @@ Proof.
   destruct (map # pc) in *; try contradiction.
   rewrite H.
   reflexivity.
-Admitted.
-(*
 - (* op *)
   econstructor; split.
   eapply exec_Iop with (v := v); eauto.
-  rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
+  rewrite <- H0.
+  rewrite subst_args_ok by assumption.
+  apply eval_operation_preserved. exact symbols_preserved.
   constructor; auto.
+  
+  admit.
+  
 (* load *)
 - econstructor; split.
   assert (eval_addressing tge sp addr rs ## args = Some a).
-  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  rewrite <- H0.
+  apply eval_addressing_preserved. exact symbols_preserved.
   eapply exec_Iload; eauto.
+  rewrite subst_args_ok; assumption.
   constructor; auto.
+
+  admit.
+  
 - (* load notrap1 *)
   econstructor; split.
   assert (eval_addressing tge sp addr rs ## args = None).
   rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
   eapply exec_Iload_notrap1; eauto.
+  rewrite subst_args_ok; assumption.
   constructor; auto.
+
+  admit.
+  
 - (* load notrap2 *)
   econstructor; split.
   assert (eval_addressing tge sp addr rs ## args = Some a).
   rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
   eapply exec_Iload_notrap2; eauto.
-  constructor; auto. 
+  rewrite subst_args_ok; assumption.
+  constructor; auto.
+
+  admit.
+  
 - (* store *)
   econstructor; split.
   assert (eval_addressing tge sp addr rs ## args = Some a).
   rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
   eapply exec_Istore; eauto.
-  constructor; auto. 
+  rewrite subst_args_ok; assumption.
+  constructor; auto.
+
+  admit.
+  
 (* call *)
 - econstructor; split.
   eapply exec_Icall with (fd := transf_fundef fd); eauto.
     eapply find_function_translated; eauto.
     apply sig_preserved.
+  rewrite subst_args_ok by assumption.
   constructor. constructor; auto. constructor.
+
+  admit.
+  
 (* tailcall *)
 - econstructor; split.
   eapply exec_Itailcall with (fd := transf_fundef fd); eauto.
     eapply find_function_translated; eauto.
     apply sig_preserved.
+  rewrite subst_args_ok by assumption.
   constructor. auto.
+  
 (* builtin *)
 - econstructor; split.
   eapply exec_Ibuiltin; eauto.
     eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
     eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   constructor; auto.
+
+  admit.
+  
 (* cond *)
 - econstructor; split.
   eapply exec_Icond; eauto.
+  rewrite subst_args_ok; eassumption.
   constructor; auto.
+
+  admit.
+  
 (* jumptbl *)
 - econstructor; split.
   eapply exec_Ijumptable; eauto.
+  rewrite subst_arg_ok; eassumption.
   constructor; auto.
+
+  admit.
+  
 (* return *)
-- econstructor; split.
-  eapply exec_Ireturn; eauto.
-  constructor; auto.
+- destruct or as [arg | ].
+  {
+    econstructor; split.
+    eapply exec_Ireturn; eauto.
+    unfold regmap_optget.
+    rewrite subst_arg_ok by eassumption.
+    constructor; auto.
+  }
+    econstructor; split.
+    eapply exec_Ireturn; eauto.
+    constructor; auto.
+  
+  
 (* internal function *)
 -  simpl. econstructor; split.
   eapply exec_function_internal; eauto.
   constructor; auto.
+
+  admit.
+  
 (* external function *)
 - econstructor; split.
   eapply exec_function_external; eauto.
     eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  constructor; auto.
+    constructor; auto.
+
 (* return *)
 - inv STACKS. inv H1.
   econstructor; split.
   eapply exec_return; eauto.
   constructor; auto.
-Qed.
- *)
+
+  admit.
+Admitted.
+
 
 Lemma transf_initial_states:
   forall S1, RTL.initial_state prog S1 ->
-- 
cgit 


From 123074c38671e76dbf8678a5f116970ab2f5a799 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 06:41:49 +0100
Subject: fix bug in xfer function

---
 backend/ForwardMoves.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 65d66b16..0e71b6b5 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -231,7 +231,8 @@ Module RB := ADD_BOTTOM(RELATION).
 Module DS := Dataflow_Solver(RB)(NodeSetForward).
 
 Definition kill (dst : reg) (rel : RELATION.t) :=
-  PTree.remove dst rel.
+  PTree.filter1 (fun x => if Pos.eq_dec dst x then false else true)
+                (PTree.remove dst rel).
 
 Definition move (src dst : reg) (rel : RELATION.t) :=
   PTree.set dst (match PTree.get src rel with
-- 
cgit 


From bea5025d84a4207011cbc8c5c435d399aa5bfdef Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 07:27:02 +0100
Subject: moving forward with proofs

---
 backend/ForwardMovesproof.v | 60 ++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 59 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 28befed3..3db67ed6 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -159,6 +159,46 @@ Proof.
   assumption.
 Qed.
 
+Lemma kill_ok:
+  forall dst,
+  forall mpc,
+  forall rs,
+  forall v,
+    get_rb_sem (Some mpc) rs ->
+    get_rb_sem (Some (kill dst mpc)) rs # dst <- v.
+Proof.
+  unfold get_rb_sem.
+  intros until v.
+  intros SEM x.
+  destruct (Pos.eq_dec x dst) as [EQ | NEQ].
+  {
+    subst dst.
+    rewrite Regmap.gss.
+    unfold kill, get_r.
+    rewrite PTree.gfilter1.
+    rewrite PTree.grs.
+    apply Regmap.gss.
+  }
+  rewrite (Regmap.gso v rs NEQ).
+  unfold kill, get_r in *.
+  rewrite PTree.gfilter1.
+  rewrite PTree.gro by assumption.
+  pose proof (SEM x) as SEMx.
+  destruct (mpc ! x).
+  {
+    destruct (Pos.eq_dec dst r).
+    {
+      subst dst.
+      rewrite Regmap.gso by assumption.
+      reflexivity.
+    }
+    rewrite Regmap.gso by congruence.
+    assumption.
+  }
+  rewrite Regmap.gso by assumption.
+  reflexivity.
+Qed.
+
 Ltac TR_AT :=
   match goal with
   | [ A: (fn_code _)!_ = Some _ |- _ ] =>
@@ -230,7 +270,25 @@ Proof.
   rewrite subst_args_ok; assumption.
   constructor; auto.
 
-  admit.
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+  apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)).
+  {
+    replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+    {
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
+    }
+    unfold apply_instr'.
+    rewrite H.
+    rewrite MPC.
+    reflexivity.
+  }
+  apply kill_ok.
+  assumption.
   
 - (* load notrap1 *)
   econstructor; split.
-- 
cgit 


From 5787da9e4d024dc3a3190bff0fe29385abbcece9 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 07:47:27 +0100
Subject: some more proof

---
 backend/ForwardMovesproof.v | 56 ++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 53 insertions(+), 3 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 3db67ed6..99b546c7 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -298,7 +298,25 @@ Proof.
   rewrite subst_args_ok; assumption.
   constructor; auto.
 
-  admit.
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+  apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)).
+  {
+    replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+    {
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
+    }
+    unfold apply_instr'.
+    rewrite H.
+    rewrite MPC.
+    reflexivity.
+  }
+  apply kill_ok.
+  assumption.
   
 - (* load notrap2 *)
   econstructor; split.
@@ -308,7 +326,25 @@ Proof.
   rewrite subst_args_ok; assumption.
   constructor; auto.
 
-  admit.
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+  apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)).
+  {
+    replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+    {
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
+    }
+    unfold apply_instr'.
+    rewrite H.
+    rewrite MPC.
+    reflexivity.
+  }
+  apply kill_ok.
+  assumption.
   
 - (* store *)
   econstructor; split.
@@ -318,7 +354,21 @@ Proof.
   rewrite subst_args_ok; assumption.
   constructor; auto.
 
-  admit.
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply get_rb_sem_ge with (rb2 := map # pc); trivial.
+  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
+  {
+    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+    2: apply apply_instr'_bot.
+    simpl. tauto.
+  }
+  unfold apply_instr'.
+  unfold get_rb_sem in *.
+  destruct (map # pc) in *; try contradiction.
+  rewrite H.
+  reflexivity.
   
 (* call *)
 - econstructor; split.
-- 
cgit 


From a36948c2af873559e5df4a2d96fdbc5bbfcfaca8 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 08:02:36 +0100
Subject: fix bug and forward in proofs

---
 backend/ForwardMoves.v      |  3 ++-
 backend/ForwardMovesproof.v | 17 ++++++++++++++++-
 2 files changed, 18 insertions(+), 2 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 0e71b6b5..660d0458 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -250,13 +250,14 @@ Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) :=
 Definition apply_instr instr x :=
   match instr with
   | Inop _
+  | Icond _ _ _ _
   | Istore _ _ _ _ _ => Some x
   | Iop Omove (src :: nil) dst _ => Some (move src dst x)
   | Iop _ _ dst _
   | Iload _ _ _ _ dst _
   | Icall _ _ _ dst _ => Some (kill dst x)
   | Ibuiltin _ _ res _ => Some (kill_builtin_res res x)
-  | Icond _ _ _ _ | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot
+  | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot
   end.
 
 Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t :=
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 99b546c7..aa516df4 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -403,7 +403,22 @@ Proof.
   rewrite subst_args_ok; eassumption.
   constructor; auto.
 
-  admit.
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply get_rb_sem_ge with (rb2 := map # pc); trivial.
+  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
+  {
+    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+    2: apply apply_instr'_bot.
+    simpl.
+    destruct b; tauto.
+  }
+  unfold apply_instr'.
+  unfold get_rb_sem in *.
+  destruct (map # pc) in *; try contradiction.
+  rewrite H.
+  reflexivity.
   
 (* jumptbl *)
 - econstructor; split.
-- 
cgit 


From 2e613cd29123583fb3378d5727217c359e818611 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 08:54:33 +0100
Subject: more proofs

---
 backend/ForwardMovesproof.v | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index aa516df4..6562fc7b 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -199,6 +199,16 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma top_ok :
+  forall rs, get_rb_sem (Some RELATION.top) rs.
+Proof.
+  unfold get_rb_sem, RELATION.top.
+  intros.
+  unfold get_r.
+  rewrite PTree.gempty.
+  reflexivity.
+Qed.
+
 Ltac TR_AT :=
   match goal with
   | [ A: (fn_code _)!_ = Some _ |- _ ] =>
@@ -447,7 +457,14 @@ Proof.
   eapply exec_function_internal; eauto.
   constructor; auto.
 
-  admit.
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply get_rb_sem_ge with (rb2 := Some RELATION.top).
+  {
+    eapply DS.fixpoint_entry with (code := fn_code f) (successors := successors_instr); try eassumption.
+  }
+  apply top_ok.
   
 (* external function *)
 - econstructor; split.
-- 
cgit 


From 36f336d8c57f053342ec794e5bc802ebb66fc82b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 08:59:28 +0100
Subject: proof for jumptable

---
 backend/ForwardMovesproof.v | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 6562fc7b..7727bc38 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -436,7 +436,23 @@ Proof.
   rewrite subst_arg_ok; eassumption.
   constructor; auto.
 
-  admit.
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply get_rb_sem_ge with (rb2 := map # pc); trivial.
+  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
+  {
+    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+    2: apply apply_instr'_bot.
+    simpl.
+    apply list_nth_z_in with (n := Int.unsigned n).
+    assumption.
+  }
+  unfold apply_instr'.
+  unfold get_rb_sem in *.
+  destruct (map # pc) in *; try contradiction.
+  rewrite H.
+  reflexivity.
   
 (* return *)
 - destruct or as [arg | ].
-- 
cgit 


From 35a17f7c9a42e654a646114aeecfbba60fd71b06 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 09:08:15 +0100
Subject: moving forward with proofs

---
 backend/ForwardMoves.v      |  9 +++++----
 backend/ForwardMovesproof.v | 16 +++++++++++++++-
 2 files changed, 20 insertions(+), 5 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 660d0458..e820723c 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -251,13 +251,14 @@ Definition apply_instr instr x :=
   match instr with
   | Inop _
   | Icond _ _ _ _
-  | Istore _ _ _ _ _ => Some x
+  | Ijumptable _ _
+  | Istore _ _ _ _ _
+  | Icall _ _ _ _ _ => Some x
   | Iop Omove (src :: nil) dst _ => Some (move src dst x)
   | Iop _ _ dst _
-  | Iload _ _ _ _ dst _
-  | Icall _ _ _ dst _ => Some (kill dst x)
+  | Iload _ _ _ _ dst _=> Some (kill dst x)
   | Ibuiltin _ _ res _ => Some (kill_builtin_res res x)
-  | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot
+  | Itailcall _ _ _ | Ireturn _ => RB.bot
   end.
 
 Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t :=
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 7727bc38..c44d4084 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -388,7 +388,21 @@ Proof.
   rewrite subst_args_ok by assumption.
   constructor. constructor; auto. constructor.
 
-  admit.
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply get_rb_sem_ge with (rb2 := map # pc); trivial.
+  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
+  {
+    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+    2: apply apply_instr'_bot.
+    simpl. tauto.
+  }
+  unfold apply_instr'.
+  unfold get_rb_sem in *.
+  destruct (map # pc) in *; try contradiction.
+  rewrite H.
+  reflexivity.
   
 (* tailcall *)
 - econstructor; split.
-- 
cgit 


From b4092913eceb102c52660b5e7dc9f0aefb9eb4f2 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 09:28:36 +0100
Subject: we still have issues with call stacks

---
 backend/ForwardMoves.v      |  6 ++---
 backend/ForwardMovesproof.v | 60 ++++++++++++++++++++++++++++++++++++---------
 2 files changed, 51 insertions(+), 15 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index e820723c..4cc9d5bc 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -252,11 +252,11 @@ Definition apply_instr instr x :=
   | Inop _
   | Icond _ _ _ _
   | Ijumptable _ _
-  | Istore _ _ _ _ _
-  | Icall _ _ _ _ _ => Some x
+  | Istore _ _ _ _ _ => Some x
   | Iop Omove (src :: nil) dst _ => Some (move src dst x)
   | Iop _ _ dst _
-  | Iload _ _ _ _ dst _=> Some (kill dst x)
+  | Iload _ _ _ _ dst _
+  | Icall _ _ _ dst _ => Some (kill dst x)
   | Ibuiltin _ _ res _ => Some (kill_builtin_res res x)
   | Itailcall _ _ _ | Ireturn _ => RB.bot
   end.
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index c44d4084..645030f8 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -199,6 +199,39 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma kill_weaken:
+  forall dst,
+  forall mpc,
+  forall rs,
+    get_rb_sem (Some mpc) rs ->
+    get_rb_sem (Some (kill dst mpc)) rs.
+Proof.
+  unfold get_rb_sem.
+  intros until rs.
+  intros SEM x.
+  destruct (Pos.eq_dec x dst) as [EQ | NEQ].
+  {
+    subst dst.
+    unfold kill, get_r.
+    rewrite PTree.gfilter1.
+    rewrite PTree.grs.
+    reflexivity.
+  }
+  unfold kill, get_r in *.
+  rewrite PTree.gfilter1.
+  rewrite PTree.gro by assumption.
+  pose proof (SEM x) as SEMx.
+  destruct (mpc ! x).
+  {
+    destruct (Pos.eq_dec dst r).
+    {
+      reflexivity.
+    }
+    assumption.
+  }
+  reflexivity.
+Qed.
+
 Lemma top_ok :
   forall rs, get_rb_sem (Some RELATION.top) rs.
 Proof.
@@ -268,7 +301,7 @@ Proof.
   rewrite subst_args_ok by assumption.
   apply eval_operation_preserved. exact symbols_preserved.
   constructor; auto.
-  
+
   admit.
   
 (* load *)
@@ -391,18 +424,22 @@ Proof.
   simpl in *.
   unfold fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
-  apply get_rb_sem_ge with (rb2 := map # pc); trivial.
-  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
+  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+  apply get_rb_sem_ge with (rb2 := Some (kill res mpc)).
   {
-    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
-    2: apply apply_instr'_bot.
-    simpl. tauto.
+    replace (Some (kill res mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+    {
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
+    }
+    unfold apply_instr'.
+    rewrite H.
+    rewrite MPC.
+    reflexivity.
   }
-  unfold apply_instr'.
-  unfold get_rb_sem in *.
-  destruct (map # pc) in *; try contradiction.
-  rewrite H.
-  reflexivity.
+  apply kill_weaken.
+  assumption.
   
 (* tailcall *)
 - econstructor; split.
@@ -508,7 +545,6 @@ Proof.
   eapply exec_return; eauto.
   constructor; auto.
 
-  admit.
 Admitted.
 
 
-- 
cgit 


From cb3f8a833882d1e24704530bc778b37a5b66f69c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 14:51:06 +0100
Subject: proof of return

---
 backend/ForwardMovesproof.v | 60 ++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 59 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 645030f8..6fa70562 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -248,10 +248,48 @@ Ltac TR_AT :=
         generalize (transf_function_at _ _ _ A); intros
   end.
 
+Definition is_killed_in_map (map : PMap.t RB.t) pc res :=
+  match PMap.get pc map with
+  | None => True
+  | Some rel => exists rel', rel = (kill res rel')
+  end.
+
+Definition is_killed_in_fmap fmap pc res :=
+  match fmap with
+  | None => True
+  | Some map => is_killed_in_map map pc res
+  end.
+
+Definition killed_twice:
+  forall rel : RELATION.t,
+  forall res,
+    RELATION.eq (kill res rel) (kill res (kill res rel)).
+Proof.
+  unfold kill, RELATION.eq.
+  intros.
+  rewrite PTree.gfilter1.
+  rewrite PTree.gfilter1.
+  destruct (Pos.eq_dec res x).
+  {
+    subst res.
+    rewrite PTree.grs.
+    rewrite PTree.grs.
+    reflexivity.
+  }
+  rewrite PTree.gro by congruence. 
+  rewrite PTree.gro by congruence. 
+  rewrite PTree.gfilter1.
+  rewrite PTree.gro by congruence.
+  destruct (rel ! x) as [relx | ]; trivial.
+  destruct (Pos.eq_dec res relx); trivial.
+  destruct (Pos.eq_dec res relx); congruence.
+Qed.
+
 Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
 | match_frames_intro: forall res f sp pc rs,
     (fmap_sem (forward_map f) pc rs) ->
-    match_frames (Stackframe res f sp pc rs)
+    (is_killed_in_fmap (forward_map f) pc res) ->
+      match_frames (Stackframe res f sp pc rs)
                  (Stackframe res (transf_function f) sp pc rs).
 
 Inductive match_states: RTL.state -> RTL.state -> Prop :=
@@ -421,6 +459,7 @@ Proof.
   rewrite subst_args_ok by assumption.
   constructor. constructor; auto. constructor.
 
+  {
   simpl in *.
   unfold fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
@@ -440,6 +479,8 @@ Proof.
   }
   apply kill_weaken.
   assumption.
+  }
+  admit.
   
 (* tailcall *)
 - econstructor; split.
@@ -545,6 +586,23 @@ Proof.
   eapply exec_return; eauto.
   constructor; auto.
 
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  unfold is_killed_in_fmap in H8.
+   unfold is_killed_in_map in H8.
+  destruct (map # pc) as [mpc |] in *; try contradiction.
+  apply get_rb_sem_ge with (rb2 := Some (kill res mpc)).
+  {
+    destruct H8 as [rel' REL].
+    subst mpc.
+    apply RB.ge_refl.
+    simpl.
+    apply killed_twice.
+  }
+  apply kill_ok.
+  assumption.
+  
 Admitted.
 
 
-- 
cgit 


From 2e79fb4d9bb98f497d59cf52ca3df5cc90515d53 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 15:59:57 +0100
Subject: return is ok

---
 backend/ForwardMovesproof.v | 67 +++++++++++++++++++++++++++++++++++----------
 1 file changed, 53 insertions(+), 14 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 6fa70562..f32fe430 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -251,7 +251,7 @@ Ltac TR_AT :=
 Definition is_killed_in_map (map : PMap.t RB.t) pc res :=
   match PMap.get pc map with
   | None => True
-  | Some rel => exists rel', rel = (kill res rel')
+  | Some rel => exists rel', RELATION.ge rel (kill res rel')
   end.
 
 Definition is_killed_in_fmap fmap pc res :=
@@ -285,6 +285,39 @@ Proof.
   destruct (Pos.eq_dec res relx); congruence.
 Qed.
 
+Lemma get_rb_killed:
+  forall mpc,
+  forall rs,
+  forall rel,
+  forall res,
+  forall vres,
+    (get_rb_sem (Some mpc) rs) ->
+    (RELATION.ge mpc (kill res rel)) ->
+    (get_rb_sem (Some mpc) rs # res <- vres).
+Proof.
+  simpl.
+  intros until vres.
+  intros SEM GE x.
+  pose proof (GE x) as GEx.
+  pose proof (SEM x) as SEMx.
+  unfold get_r in *.
+  destruct (mpc ! x) as [mpcx | ] in *; trivial.
+  unfold kill in GEx.
+  rewrite PTree.gfilter1 in GEx.
+  destruct (Pos.eq_dec res x) as [ | res_NE_x].
+  {
+    subst res.
+    rewrite PTree.grs in GEx.
+    discriminate.
+  }
+  rewrite PTree.gro in GEx by congruence.
+  rewrite Regmap.gso with (i := x) by congruence.
+  destruct (rel ! x) as [relx | ]; try discriminate.
+  destruct (Pos.eq_dec res relx) as [ res_EQ_relx | res_NE_relx] in *; try discriminate.
+  rewrite Regmap.gso by congruence.
+  congruence.
+Qed.
+  
 Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
 | match_frames_intro: forall res f sp pc rs,
     (fmap_sem (forward_map f) pc rs) ->
@@ -480,7 +513,22 @@ Proof.
   apply kill_weaken.
   assumption.
   }
-  admit.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  assert (RB.ge (map # pc') (apply_instr' (fn_code f) pc (map # pc))) as GE.
+  {
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
+  }
+  unfold apply_instr' in GE.
+  unfold fmap_sem in *.
+  destruct (map # pc) as [mpc |] in *; try contradiction.
+  rewrite H in GE.
+  simpl in GE.
+  unfold is_killed_in_fmap, is_killed_in_map.
+  unfold RB.ge in GE.
+  destruct (map # pc') as [mpc'|] eqn:MPC' in *; trivial.
+  eauto.
   
 (* tailcall *)
 - econstructor; split.
@@ -590,19 +638,10 @@ Proof.
   unfold fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   unfold is_killed_in_fmap in H8.
-   unfold is_killed_in_map in H8.
+  unfold is_killed_in_map in H8.
   destruct (map # pc) as [mpc |] in *; try contradiction.
-  apply get_rb_sem_ge with (rb2 := Some (kill res mpc)).
-  {
-    destruct H8 as [rel' REL].
-    subst mpc.
-    apply RB.ge_refl.
-    simpl.
-    apply killed_twice.
-  }
-  apply kill_ok.
-  assumption.
-  
+  destruct H8 as [rel' RGE].
+  eapply get_rb_killed; eauto.
 Admitted.
 
 
-- 
cgit 


From fb5029eb72a3a28b26f3d982c30badc8d027f405 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 17:40:52 +0100
Subject: fix move

---
 backend/ForwardMoves.v      |   4 +-
 backend/ForwardMovesproof.v | 120 +++++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 120 insertions(+), 4 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 4cc9d5bc..c73b0213 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -238,7 +238,7 @@ Definition move (src dst : reg) (rel : RELATION.t) :=
   PTree.set dst (match PTree.get src rel with
                  | Some src' => src'
                  | None => src
-                 end) rel.
+                 end) (kill dst rel).
 
 Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) :=
   match res with
@@ -257,7 +257,7 @@ Definition apply_instr instr x :=
   | Iop _ _ dst _
   | Iload _ _ _ _ dst _
   | Icall _ _ _ dst _ => Some (kill dst x)
-  | Ibuiltin _ _ res _ => Some (kill_builtin_res res x)
+  | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *)
   | Itailcall _ _ _ | Ireturn _ => RB.bot
   end.
 
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index f32fe430..8e2ba9af 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -242,6 +242,64 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma move_ok:
+  forall mpc : RELATION.t,
+  forall src res : reg,
+  forall rs : regset,
+    get_rb_sem (Some mpc) rs ->
+    get_rb_sem (Some (move src res mpc)) (rs # res <- (rs # src)).
+Proof.
+  unfold get_rb_sem, move.
+  intros until rs.
+  intros SEM x.
+  unfold get_r in *.
+  destruct (Pos.eq_dec res x).
+  {
+    subst res.
+    rewrite PTree.gss.
+    rewrite Regmap.gss.
+    pose proof (SEM src) as SEMsrc.
+    destruct (mpc ! src) as [mpcsrc | ] in *.
+    {
+      destruct (Pos.eq_dec x mpcsrc).
+      {
+        subst mpcsrc.
+        rewrite Regmap.gss.
+        reflexivity.
+      }
+      rewrite Regmap.gso by congruence.
+      assumption.
+    }
+    destruct (Pos.eq_dec x src).
+    {
+      subst src.
+      rewrite Regmap.gss.
+      reflexivity.
+    }
+    rewrite Regmap.gso by congruence.
+    reflexivity.
+  }
+  rewrite PTree.gso by congruence.
+  rewrite Regmap.gso with (i := x) by congruence.
+  unfold kill.
+  rewrite PTree.gfilter1.
+  rewrite PTree.gro by congruence.
+  pose proof (SEM x) as SEMx.
+  destruct (mpc ! x) as [ r |].
+  {
+    destruct (Pos.eq_dec res r).
+    {
+      subst r.
+      rewrite Regmap.gso by congruence.
+      trivial.
+    }
+    rewrite Regmap.gso by congruence.
+    assumption.
+  }
+  rewrite Regmap.gso by congruence.
+  reflexivity.
+Qed.
+  
 Ltac TR_AT :=
   match goal with
   | [ A: (fn_code _)!_ = Some _ |- _ ] =>
@@ -340,6 +398,24 @@ Inductive match_states: RTL.state -> RTL.state -> Prop :=
       match_states (Returnstate stk v m)
                    (Returnstate stk' v m).
 
+Lemma op_cases:
+  forall op,
+  forall args,
+  forall dst,
+  forall s,
+  forall x,
+    (exists src, op=Omove /\ args = src :: nil /\
+                 (apply_instr (Iop op args dst s) x) = Some (move src dst x))
+    \/
+    (apply_instr (Iop op args dst s) x) = Some (kill dst x).
+Proof.
+  destruct op; try (right; simpl; reflexivity).
+  destruct args as [| arg0 args0t]; try (right; simpl; reflexivity).
+  destruct args0t as [| arg1 args1t]; try (right; simpl; reflexivity).
+  left.
+  eauto.
+Qed.
+
 Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 ->
   forall S1', match_states S1 S1' ->
@@ -373,7 +449,29 @@ Proof.
   apply eval_operation_preserved. exact symbols_preserved.
   constructor; auto.
 
-  admit.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+  assert (RB.ge (map # pc') (apply_instr' (fn_code f) pc (map # pc))) as GE.
+  {
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
+  }
+  unfold apply_instr' in GE.
+  rewrite MPC in GE.
+  rewrite H in GE.
+  
+  destruct (op_cases op args res pc' mpc) as [[src [OP [ARGS MOVE]]] | KILL].
+  {
+    subst op.
+    subst args.
+    rewrite MOVE in GE.
+    simpl in H0.
+    destruct (map # pc') as [mpc' | ] in *; try discriminate.
+    simpl in GE.
+    unfold move in GE.
+  }
   
 (* load *)
 - econstructor; split.
@@ -545,7 +643,25 @@ Proof.
     eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   constructor; auto.
 
-  admit.
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+  
+  apply get_rb_sem_ge with (rb2 := Some RELATION.top).
+  {
+    replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)).
+    {
+      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+      2: apply apply_instr'_bot.
+      simpl. tauto.
+    }
+    unfold apply_instr'.
+    rewrite H.
+    rewrite MPC.
+    reflexivity.
+  }
+  apply top_ok.
   
 (* cond *)
 - econstructor; split.
-- 
cgit 


From a8dd20cd96a1c8636add5b8b45b6ee5ff5982f9a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 17:43:52 +0100
Subject: fix move

---
 backend/ForwardMovesproof.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 8e2ba9af..b1425401 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -470,8 +470,10 @@ Proof.
     simpl in H0.
     destruct (map # pc') as [mpc' | ] in *; try discriminate.
     simpl in GE.
-    unfold move in GE.
+    admit.
+    admit.
   }
+  admit.
   
 (* load *)
 - econstructor; split.
-- 
cgit 


From b8823bfa481e4322e809d600624c59634447ec4d Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 17:50:12 +0100
Subject: nearly done

---
 backend/ForwardMovesproof.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index b1425401..8c036851 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -468,10 +468,12 @@ Proof.
     subst args.
     rewrite MOVE in GE.
     simpl in H0.
-    destruct (map # pc') as [mpc' | ] in *; try discriminate.
     simpl in GE.
-    admit.
-    admit.
+    apply get_rb_sem_ge with (rb2 := Some (move src res mpc)).
+    assumption.
+    replace v with (rs # src) by congruence.
+    apply move_ok.
+    assumption.
   }
   admit.
   
-- 
cgit 


From 7d3ac44ff5b909a6d00a94e6d30748e15054daf5 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 17:54:40 +0100
Subject: FINISHED the forward-moves pass

---
 backend/ForwardMovesproof.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'backend')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 8c036851..826d4250 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -475,7 +475,11 @@ Proof.
     apply move_ok.
     assumption.
   }
-  admit.
+  rewrite KILL in GE.
+  apply get_rb_sem_ge with (rb2 := Some (kill res mpc)).
+  assumption.
+  apply kill_ok.
+  assumption.
   
 (* load *)
 - econstructor; split.
@@ -762,7 +766,7 @@ Proof.
   destruct (map # pc) as [mpc |] in *; try contradiction.
   destruct H8 as [rel' RGE].
   eapply get_rb_killed; eauto.
-Admitted.
+Qed.
 
 
 Lemma transf_initial_states:
-- 
cgit