From 93b1e0034733dcc19dc42c04725439e8bdf3d10d Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 06:53:30 +0100
Subject: CSE2 split in two files

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

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
new file mode 100644
index 00000000..a14988a0
--- /dev/null
+++ b/backend/CSE2proof.v
@@ -0,0 +1,835 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE2.
+
+Lemma args_unaffected:
+  forall rs : regset,
+  forall dst : reg,
+  forall v,
+  forall args : list reg,
+    existsb (fun y : reg => peq dst y) args = false ->
+    (rs # dst <- v ## args) = (rs ## args).
+Proof.
+  induction args; simpl; trivial.
+  destruct (peq dst a) as [EQ | NEQ]; simpl.
+  { discriminate.
+  }
+  intro EXIST.
+  f_equal.
+  {
+    apply Regmap.gso.
+    congruence.
+  }
+  apply IHargs.
+  assumption.
+Qed.
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Section SAME_MEMORY.
+  Variable m : mem.
+
+Definition sem_sym_val sym rs :=
+  match sym with
+  | SMove src => Some (rs # src)
+  | SOp op args =>
+    eval_operation genv sp op (rs ## args) m
+  end.
+    
+Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) : option val :=
+  match rel ! x with
+  | None => Some (rs # x)
+  | Some sym => sem_sym_val sym rs
+  end.
+
+Definition sem_rel (rel : RELATION.t) (rs : regset) :=
+  forall x : reg, (sem_reg rel x rs) = Some (rs # x).
+
+Lemma kill_reg_sound :
+  forall rel : RELATION.t,
+  forall dst : reg,
+  forall rs,
+  forall v,
+    sem_rel rel rs ->
+    sem_rel (kill_reg dst rel) (rs # dst <- v).
+Proof.
+  unfold sem_rel, kill_reg, sem_reg, sem_sym_val.
+  intros until v.
+  intros REL x.
+  rewrite PTree.gfilter1.
+  destruct (Pos.eq_dec dst x).
+  {
+    subst x.
+    rewrite PTree.grs.
+    rewrite Regmap.gss.
+    reflexivity.
+  }
+  rewrite PTree.gro by congruence.
+  rewrite Regmap.gso by congruence.
+  destruct (rel ! x) as [relx | ] eqn:RELx.
+  2: reflexivity.
+  unfold kill_sym_val.
+  pose proof (REL x) as RELinstx.
+  rewrite RELx in RELinstx.
+  destruct relx eqn:SYMVAL.
+  {
+    destruct (peq dst src); simpl.
+    { reflexivity. }
+    rewrite Regmap.gso by congruence.
+    assumption.
+  }
+  { destruct existsb eqn:EXISTS; simpl.
+    { reflexivity. }
+    rewrite args_unaffected by exact EXISTS.
+    assumption.
+  }
+Qed.
+
+Lemma write_same:
+  forall rs : regset,
+  forall src dst : reg,
+    (rs # dst <- (rs # src)) # src = rs # src.
+Proof.
+  intros.
+  destruct (peq src dst).
+  {
+    subst dst.
+    apply Regmap.gss.
+  }
+  rewrite Regmap.gso by congruence.
+  reflexivity.
+Qed.
+
+Lemma move_sound :
+  forall rel : RELATION.t,
+  forall src dst : reg,
+  forall rs,
+    sem_rel rel rs ->
+    sem_rel (move src dst rel) (rs # dst <- (rs # src)).
+Proof.
+  intros until rs. intros REL x.
+  pose proof (kill_reg_sound rel dst rs (rs # src) REL x) as KILL.
+  pose proof (REL src) as RELsrc.
+  unfold move.
+  destruct (peq x dst).
+  {
+    subst x.
+    unfold sem_reg.
+    rewrite PTree.gss.
+    rewrite Regmap.gss.
+    unfold sem_reg in RELsrc.
+    simpl.
+    unfold forward_move.
+    destruct (rel ! src) as [ sv |]; simpl.
+    destruct sv; simpl in *.
+    {
+      destruct (peq dst src0).
+      {
+        subst src0.
+        rewrite Regmap.gss.
+        reflexivity.
+      }
+      rewrite Regmap.gso by congruence.
+      assumption.
+    }
+    all: f_equal; apply write_same.
+  }
+  rewrite Regmap.gso by congruence.
+  unfold sem_reg.
+  rewrite PTree.gso by congruence.
+  rewrite Regmap.gso in KILL by congruence.
+  exact KILL.
+Qed.
+
+Lemma move_cases_neq:
+  forall dst rel a,
+    a <> dst ->
+    (forward_move (kill_reg dst rel) a) <> dst.
+Proof.
+  intros until a. intro NEQ.
+  unfold kill_reg, forward_move.
+  rewrite PTree.gfilter1.
+  rewrite PTree.gro by congruence.
+  destruct (rel ! a); simpl.
+  2: congruence.
+  destruct s.
+  {
+    unfold kill_sym_val.
+    destruct peq; simpl; congruence.
+  }
+  all: simpl;
+    destruct negb; simpl; congruence.
+Qed.
+
+Lemma args_replace_dst :
+  forall rel,
+  forall args : list reg,
+  forall dst : reg,
+  forall rs : regset,
+  forall v,
+    (sem_rel rel rs) ->
+    not (In dst args) ->
+    (rs # dst <- v)
+    ## (map
+          (forward_move (kill_reg dst rel)) args) = rs ## args.
+Proof.
+  induction args; simpl.
+  1: reflexivity.
+  intros until v.
+  intros REL NOT_IN.
+  rewrite IHargs by auto.
+  f_equal.
+  pose proof (REL a) as RELa.
+  rewrite Regmap.gso by (apply move_cases_neq; auto).
+  unfold kill_reg.
+  unfold sem_reg in RELa.
+  unfold forward_move.
+  rewrite PTree.gfilter1.
+  rewrite PTree.gro by auto.
+  destruct (rel ! a); simpl; trivial.
+  destruct s; simpl in *; destruct negb; simpl; congruence.
+Qed.
+
+Lemma oper1_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall v,
+    sem_rel rel rs ->
+    not (In dst args) ->
+    eval_operation genv sp op (rs ## args) m = Some v ->
+    sem_rel (oper1 op dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL NOT_IN EVAL x.
+  pose proof (kill_reg_sound rel dst rs v REL x) as KILL.
+  unfold oper1.
+  destruct (peq x dst).
+  {
+    subst x.
+    unfold sem_reg.
+    rewrite PTree.gss.
+    rewrite Regmap.gss.
+    simpl.
+    rewrite args_replace_dst by auto.
+    assumption.
+  }
+  rewrite Regmap.gso by congruence.
+  unfold sem_reg.
+  rewrite PTree.gso by congruence.
+  rewrite Regmap.gso in KILL by congruence.
+  exact KILL.
+Qed.
+
+Lemma oper_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall v,
+    sem_rel rel rs ->
+    eval_operation genv sp op (rs ## args) m = Some v ->
+    sem_rel (oper op dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL EVAL.
+  unfold oper.
+  destruct in_dec.
+  {
+    apply kill_reg_sound; auto. 
+  }
+  apply oper1_sound; auto.
+Qed.
+
+Lemma gen_oper_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall v,
+    sem_rel rel rs ->
+    eval_operation genv sp op (rs ## args) m = Some v ->
+    sem_rel (gen_oper op dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL EVAL.
+  unfold gen_oper.
+  destruct op.
+  { destruct args as [ | h0 t0].
+    apply oper_sound; auto.
+    destruct t0.
+    {
+      simpl in *.
+      replace v with (rs # h0) by congruence.
+      apply move_sound; auto.
+    }
+    apply oper_sound; auto.
+  }
+  all: apply oper_sound; auto.
+Qed.
+
+
+Lemma find_op_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall src dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+    sem_rel rel rs ->
+    find_op rel op args = Some src ->
+    (eval_operation genv sp op (rs ## args) m) = Some (rs # src).
+Proof.
+  intros until rs.
+  unfold find_op.
+  rewrite PTree.fold_spec.
+  intro REL.
+  assert (
+     forall start,
+             match start with
+             | None => True
+             | Some src => eval_operation genv sp op rs ## args m = Some rs # src
+             end -> fold_left
+    (fun (a : option reg) (p : positive * sym_val) =>
+     find_op_fold op args a (fst p) (snd p)) (PTree.elements rel) start =
+                    Some src ->
+             eval_operation genv sp op rs ## args m = Some rs # src) as REC.
+  {
+    unfold sem_rel, sem_reg in REL.
+    generalize (PTree.elements_complete rel).
+    generalize (PTree.elements rel).
+    induction l; simpl.
+    {
+      intros.
+      subst start.
+      assumption.
+    }
+    destruct a as [r sv]; simpl.
+    intros COMPLETE start GEN.
+    apply IHl.
+    {
+      intros.
+      apply COMPLETE.
+      right.
+      assumption.
+    }
+    unfold find_op_fold.
+    destruct start.
+    assumption.
+    destruct sv.
+    { trivial. }
+    destruct eq_operation; trivial.
+    subst op0.
+    destruct eq_args; trivial.
+    subst args0.
+    simpl.
+    assert ((rel ! r) = Some (SOp op args)) as RELatr.
+    {
+      apply COMPLETE.
+      left.
+      reflexivity.
+    }
+    pose proof (REL r) as RELr.
+    rewrite RELatr in RELr.
+    simpl in RELr.
+    assumption.
+  }
+  apply REC; auto.
+Qed.
+
+End SAME_MEMORY.
+
+Lemma kill_mem_sound :
+  forall m m' : mem,
+  forall rel : RELATION.t,
+  forall rs,
+    sem_rel m rel rs -> sem_rel m' (kill_mem rel) rs.
+Proof.
+  unfold sem_rel, sem_reg.
+  intros until rs.
+  intros SEM x.
+  pose proof (SEM x) as SEMx.
+  unfold kill_mem.
+  rewrite PTree.gfilter1.
+  unfold kill_sym_val_mem.
+  destruct (rel ! x) as [ sv | ].
+  2: reflexivity.
+  destruct sv; simpl in *; trivial.
+  {
+    destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial.
+    rewrite <- SEMx.
+    apply op_depends_on_memory_correct; auto.
+  }
+Qed.
+  
+End SOUNDNESS.
+
+
+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.
+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 : function) (pc : node) (i : instruction),
+  (fn_code f)!pc = Some i ->
+  (fn_code (transf_function f))!pc =
+    Some(transf_instr (forward_map f) pc i).
+Proof.
+  intros until i. intro CODE.
+  unfold transf_function; simpl.
+  rewrite PTree.gmap.
+  unfold option_map.
+  rewrite CODE.
+  reflexivity.
+Qed.
+
+Definition sem_rel_b (relb : RB.t) sp m (rs : regset) :=
+  match relb with
+  | Some rel => sem_rel fundef unit ge sp m rel rs
+  | None => True
+  end.
+
+Definition fmap_sem (fmap : option (PMap.t RB.t))
+  sp m (pc : node) (rs : regset) :=
+  match fmap with
+  | None => True
+  | Some map => sem_rel_b (PMap.get pc map) sp m rs
+  end.
+
+(*
+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'.
+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.
+- (* op *)
+  econstructor; split.
+  eapply exec_Iop with (v := v); eauto.
+  rewrite <- H0.
+  rewrite subst_args_ok by assumption.
+  apply eval_operation_preserved. exact symbols_preserved.
+  constructor; auto.
+
+  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.
+    simpl in GE.
+    apply get_rb_sem_ge with (rb2 := Some (move src res mpc)).
+    assumption.
+    replace v with (rs # src) by congruence.
+    apply move_ok.
+    assumption.
+  }
+  rewrite KILL in GE.
+  apply get_rb_sem_ge with (rb2 := Some (kill res mpc)).
+  assumption.
+  apply kill_ok.
+  assumption.
+  
+(* 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.
+  rewrite subst_args_ok; assumption.
+  constructor; auto.
+
+  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.
+  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.
+
+  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.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload_notrap2; eauto.
+  rewrite subst_args_ok; assumption.
+  constructor; auto.
+
+  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.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Istore; eauto.
+  rewrite subst_args_ok; assumption.
+  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.
+  
+(* 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.
+
+  {
+  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 res mpc)).
+  {
+    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.
+  }
+  apply kill_weaken.
+  assumption.
+  }
+  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.
+  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.
+
+  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.
+  eapply exec_Icond; eauto.
+  rewrite subst_args_ok; eassumption.
+  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.
+    destruct b; tauto.
+  }
+  unfold apply_instr'.
+  unfold get_rb_sem in *.
+  destruct (map # pc) in *; try contradiction.
+  rewrite H.
+  reflexivity.
+  
+(* jumptbl *)
+- econstructor; split.
+  eapply exec_Ijumptable; eauto.
+  rewrite subst_arg_ok; eassumption.
+  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.
+    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 | ].
+  {
+    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.
+
+  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.
+  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.
+
+  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.
+  destruct H8 as [rel' RGE].
+  eapply get_rb_killed; eauto.
+Qed.
+
+
+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.
\ No newline at end of file
-- 
cgit 


From a200d33d3751fad37620a22a9e4d33e0b88176c1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 09:39:08 +0100
Subject: sem_rel_b_ge

---
 backend/CSE2proof.v | 95 +++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 77 insertions(+), 18 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index a14988a0..d9150658 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -438,7 +438,7 @@ Qed.
 Definition sem_rel_b (relb : RB.t) sp m (rs : regset) :=
   match relb with
   | Some rel => sem_rel fundef unit ge sp m rel rs
-  | None => True
+  | None => False
   end.
 
 Definition fmap_sem (fmap : option (PMap.t RB.t))
@@ -448,7 +448,66 @@ Definition fmap_sem (fmap : option (PMap.t RB.t))
   | Some map => sem_rel_b (PMap.get pc map) sp m rs
   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', RELATION.ge rel (kill_reg 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.
+
+
+Lemma sem_rel_b_ge:
+  forall rb1 rb2 : RB.t,
+    (RB.ge rb1 rb2) ->
+    forall sp m,
+    forall rs : regset,
+      (sem_rel_b rb2 sp m rs) -> (sem_rel_b rb1 sp m rs).
+Proof.
+  unfold sem_rel_b, sem_rel, sem_reg.
+  destruct rb1 as [r1 | ];
+    destruct rb2 as [r2 | ]; simpl;
+      intros GE sp m rs RE; try contradiction.
+  intro x.
+  pose proof (RE x) as REx.
+  pose proof (GE x) as GEx.
+  destruct (r1 ! x) as [r1x | ] in *;
+    destruct (r2 ! x) as [r2x | ] in *;
+    congruence.
+Qed.
+
+Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
+| match_frames_intro: forall res f sp pc rs,
+    (forall m : mem, (fmap_sem (forward_map f) sp m 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 :=
+  | match_regular_states: forall stk f sp pc rs m stk'
+                                 (STACKS: list_forall2 match_frames stk stk'),
+      (fmap_sem (forward_map f) sp m 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'
+        (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).
+  
+Ltac TR_AT :=
+  match goal with
+  | [ A: (fn_code _)!_ = Some _ |- _ ] =>
+        generalize (transf_function_at _ _ _ A); intros
+  end.
+
 Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 ->
   forall S1', match_states S1 S1' ->
@@ -462,7 +521,7 @@ 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.
+  apply sem_rel_b_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.
@@ -470,7 +529,7 @@ Proof.
     simpl. tauto.
   }
   unfold apply_instr'.
-  unfold get_rb_sem in *.
+  unfold sem_rel_b in *.
   destruct (map # pc) in *; try contradiction.
   rewrite H.
   reflexivity.
@@ -502,14 +561,14 @@ Proof.
     rewrite MOVE in GE.
     simpl in H0.
     simpl in GE.
-    apply get_rb_sem_ge with (rb2 := Some (move src res mpc)).
+    apply sem_rel_b_ge with (rb2 := Some (move src res mpc)).
     assumption.
     replace v with (rs # src) by congruence.
     apply move_ok.
     assumption.
   }
   rewrite KILL in GE.
-  apply get_rb_sem_ge with (rb2 := Some (kill res mpc)).
+  apply sem_rel_b_ge with (rb2 := Some (kill res mpc)).
   assumption.
   apply kill_ok.
   assumption.
@@ -527,7 +586,7 @@ Proof.
   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)).
+  apply sem_rel_b_ge with (rb2 := Some (kill dst mpc)).
   {
     replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
     {
@@ -555,7 +614,7 @@ Proof.
   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)).
+  apply sem_rel_b_ge with (rb2 := Some (kill dst mpc)).
   {
     replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
     {
@@ -583,7 +642,7 @@ Proof.
   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)).
+  apply sem_rel_b_ge with (rb2 := Some (kill dst mpc)).
   {
     replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
     {
@@ -610,7 +669,7 @@ 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.
+  apply sem_rel_b_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.
@@ -618,7 +677,7 @@ Proof.
     simpl. tauto.
   }
   unfold apply_instr'.
-  unfold get_rb_sem in *.
+  unfold sem_rel_b in *.
   destruct (map # pc) in *; try contradiction.
   rewrite H.
   reflexivity.
@@ -636,7 +695,7 @@ Proof.
   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 res mpc)).
+  apply sem_rel_b_ge with (rb2 := Some (kill res mpc)).
   {
     replace (Some (kill res mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
     {
@@ -689,7 +748,7 @@ Proof.
   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).
+  apply sem_rel_b_ge with (rb2 := Some RELATION.top).
   {
     replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)).
     {
@@ -713,7 +772,7 @@ 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.
+  apply sem_rel_b_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.
@@ -722,7 +781,7 @@ Proof.
     destruct b; tauto.
   }
   unfold apply_instr'.
-  unfold get_rb_sem in *.
+  unfold sem_rel_b in *.
   destruct (map # pc) in *; try contradiction.
   rewrite H.
   reflexivity.
@@ -736,7 +795,7 @@ 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.
+  apply sem_rel_b_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.
@@ -746,7 +805,7 @@ Proof.
     assumption.
   }
   unfold apply_instr'.
-  unfold get_rb_sem in *.
+  unfold sem_rel_b in *.
   destruct (map # pc) in *; try contradiction.
   rewrite H.
   reflexivity.
@@ -773,7 +832,7 @@ Proof.
   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).
+  apply sem_rel_b_ge with (rb2 := Some RELATION.top).
   {
     eapply DS.fixpoint_entry with (code := fn_code f) (successors := successors_instr); try eassumption.
   }
-- 
cgit 


From 427fc1fb431b4200ac5e60981a4d570863e2539f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 11:16:38 +0100
Subject: sem_rel_b_ge

progress
---
 backend/CSE2proof.v | 213 +++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 152 insertions(+), 61 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index d9150658..f2306d21 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -53,6 +53,57 @@ Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) : option val :=
 Definition sem_rel (rel : RELATION.t) (rs : regset) :=
   forall x : reg, (sem_reg rel x rs) = Some (rs # x).
 
+Definition sem_rel_b (relb : RB.t) (rs : regset) :=
+  match relb with
+  | Some rel => sem_rel rel rs
+  | None => False
+  end.
+
+Definition fmap_sem (fmap : option (PMap.t RB.t))
+  (pc : node) (rs : regset) :=
+  match fmap with
+  | None => True
+  | Some m => sem_rel_b (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 sem_rel_b, sem_rel, sem_reg in *.
+  destruct (map # pc).
+  2: contradiction.
+  pose proof (SEM arg) as SEMarg.
+  simpl. unfold forward_move.
+  unfold sem_sym_val in *.
+  destruct (t ! arg); trivial.
+  destruct s; congruence.
+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.
+
 Lemma kill_reg_sound :
   forall rel : RELATION.t,
   forall dst : reg,
@@ -348,6 +399,27 @@ Proof.
   apply REC; auto.
 Qed.
 
+
+Lemma kill_reg_weaken:
+  forall res mpc rs,
+    sem_rel mpc rs ->
+    sem_rel (kill_reg res mpc) rs.
+Proof.
+  Check kill_reg_sound.
+  intros until rs.
+  intros REL x.
+  pose proof (REL x) as RELx.
+  unfold kill_reg, sem_reg in *.
+  rewrite PTree.gfilter1.
+  destruct (peq res x).
+  { subst x.
+    rewrite PTree.grs.
+    reflexivity.
+  }
+  rewrite PTree.gro by congruence.
+  destruct (mpc ! x) as [sv | ]; trivial.
+  destruct negb; trivial.
+Qed.
 End SAME_MEMORY.
 
 Lemma kill_mem_sound :
@@ -435,19 +507,6 @@ Proof.
   reflexivity.
 Qed.
 
-Definition sem_rel_b (relb : RB.t) sp m (rs : regset) :=
-  match relb with
-  | Some rel => sem_rel fundef unit ge sp m rel rs
-  | None => False
-  end.
-
-Definition fmap_sem (fmap : option (PMap.t RB.t))
-  sp m (pc : node) (rs : regset) :=
-  match fmap with
-  | None => True
-  | Some map => sem_rel_b (PMap.get pc map) sp m rs
-  end.
-
 Definition is_killed_in_map (map : PMap.t RB.t) pc res :=
   match PMap.get pc map with
   | None => True
@@ -460,15 +519,19 @@ Definition is_killed_in_fmap fmap pc res :=
   | Some map => is_killed_in_map map pc res
   end.
 
+Definition sem_rel_b' := sem_rel_b fundef unit ge.
+Definition fmap_sem' := fmap_sem fundef unit ge.
+Definition subst_args_ok' := subst_args_ok fundef unit ge.
+Definition kill_mem_sound' := kill_mem_sound fundef unit ge.
 
 Lemma sem_rel_b_ge:
   forall rb1 rb2 : RB.t,
     (RB.ge rb1 rb2) ->
     forall sp m,
     forall rs : regset,
-      (sem_rel_b rb2 sp m rs) -> (sem_rel_b rb1 sp m rs).
+      (sem_rel_b' sp m rb2 rs) -> (sem_rel_b' sp m rb1 rs).
 Proof.
-  unfold sem_rel_b, sem_rel, sem_reg.
+  unfold sem_rel_b', sem_rel_b, sem_rel, sem_reg.
   destruct rb1 as [r1 | ];
     destruct rb2 as [r2 | ]; simpl;
       intros GE sp m rs RE; try contradiction.
@@ -480,9 +543,17 @@ Proof.
     congruence.
 Qed.
 
+Lemma apply_instr'_bot :
+  forall code,
+  forall pc,
+    RB.eq (apply_instr' code pc RB.bot) RB.bot.
+Proof.
+  reflexivity.
+Qed.
+
 Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
 | match_frames_intro: forall res f sp pc rs,
-    (forall m : mem, (fmap_sem (forward_map f) sp m pc rs)) ->
+    (forall m : mem, (fmap_sem' sp m (forward_map f) 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).
@@ -490,7 +561,7 @@ Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
 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'),
-      (fmap_sem (forward_map f) sp m pc rs) ->
+      (fmap_sem' sp m (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'
@@ -519,7 +590,7 @@ Proof.
   constructor; auto.
   
   simpl in *.
-  unfold fmap_sem in *.
+  unfold fmap_sem', fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   apply sem_rel_b_ge with (rb2 := map # pc); trivial.
   replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
@@ -534,6 +605,7 @@ Proof.
   rewrite H.
   reflexivity.
 - (* op *)
+  (*
   econstructor; split.
   eapply exec_Iop with (v := v); eauto.
   rewrite <- H0.
@@ -572,23 +644,24 @@ Proof.
   assumption.
   apply kill_ok.
   assumption.
-  
+   *)
+  admit.
 (* 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.
-  rewrite subst_args_ok; assumption.
+  rewrite (subst_args_ok' sp m); assumption.
   constructor; auto.
 
   simpl in *.
-  unfold fmap_sem in *.
+  unfold fmap_sem', fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
-  apply sem_rel_b_ge with (rb2 := Some (kill dst mpc)).
+  apply sem_rel_b_ge with (rb2 := Some (kill_reg dst mpc)).
   {
-    replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+    replace (Some (kill_reg 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.
@@ -599,9 +672,10 @@ Proof.
     rewrite MPC.
     reflexivity.
   }
-  apply kill_ok.
+  apply kill_reg_sound.
   assumption.
-  
+
+  (* NOT IN THIS VERSION 
 - (* load notrap1 *)
   econstructor; split.
   assert (eval_addressing tge sp addr rs ## args = None).
@@ -657,20 +731,25 @@ Proof.
   }
   apply kill_ok.
   assumption.
+   *)
   
 - (* 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.
-  rewrite subst_args_ok; assumption.
+  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.
+    rewrite (subst_args_ok' sp m); assumption.
+  }
+  
   constructor; auto.
-
   simpl in *.
-  unfold fmap_sem in *.
+  unfold fmap_sem', fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
-  apply sem_rel_b_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 sem_rel_b_ge with (rb2 := Some (kill_mem mpc)); trivial.
+  {
+  replace (Some (kill_mem 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.
@@ -678,39 +757,47 @@ Proof.
   }
   unfold apply_instr'.
   unfold sem_rel_b in *.
-  destruct (map # pc) in *; try contradiction.
+  rewrite MPC.
   rewrite H.
   reflexivity.
+  }
+  apply (kill_mem_sound' sp m).
+  assumption.
   
 (* 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.
+  rewrite (subst_args_ok' sp m) by assumption.
+  constructor. constructor; auto.
 
+  constructor.
   {
-  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 sem_rel_b_ge with (rb2 := Some (kill res mpc)).
-  {
-    replace (Some (kill res mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+    intro m'.
+    unfold fmap_sem', fmap_sem in *.
+    destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+    destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+    apply sem_rel_b_ge with (rb2 := Some (kill_reg res (kill_mem 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_reg res (kill_mem 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'.
-    rewrite H.
-    rewrite MPC.
-    reflexivity.
-  }
-  apply kill_weaken.
-  assumption.
+    apply kill_reg_weaken.
+    apply (kill_mem_sound' sp m).
+    assumption.
   }
+  {
+  simpl in *.
+  unfold fmap_sem', fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   assert (RB.ge (map # pc') (apply_instr' (fn_code f) pc (map # pc))) as GE.
   {
@@ -719,23 +806,27 @@ Proof.
       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.
+  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
   unfold is_killed_in_fmap, is_killed_in_map.
-  unfold RB.ge in GE.
-  destruct (map # pc') as [mpc'|] eqn:MPC' in *; trivial.
-  eauto.
+  destruct (map # pc') as [mpc' |] eqn:MPC' ; try contradiction.
+
+  exists (kill_mem mpc).
+  assumption.
+  }
   
 (* 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.
+  Check subst_args_ok.
+  rewrite (subst_args_ok' (Vptr stk Ptrofs.zero) m) by assumption.
   constructor. auto.
-  
+
+    (* TODO *)
+
 (* builtin *)
 - econstructor; split.
   eapply exec_Ibuiltin; eauto.
-- 
cgit 


From e974c5a24dcc80ecb4e61725bb5131570bc447fc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 12:11:42 +0100
Subject: rework

---
 backend/CSE2proof.v | 69 +++++++++++++++++++++++++++++++++++++----------------
 1 file changed, 49 insertions(+), 20 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index f2306d21..ad11a8e9 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -420,6 +420,30 @@ Proof.
   destruct (mpc ! x) as [sv | ]; trivial.
   destruct negb; trivial.
 Qed.
+
+Lemma top_ok:
+  forall rs, sem_rel RELATION.top rs.
+Proof.
+  unfold sem_rel, sem_reg, RELATION.top.
+  intros.
+  rewrite PTree.gempty.
+  reflexivity.
+Qed.
+
+Lemma sem_rel_ge:
+  forall r1 r2 : RELATION.t,
+    (RELATION.ge r1 r2) ->
+    forall rs : regset,
+      (sem_rel r2 rs) -> (sem_rel r1 rs).
+Proof.
+  intros r1 r2 GE rs RE x.
+  pose proof (RE x) as REx.
+  pose proof (GE x) as GEx.
+  unfold sem_reg in *.
+  destruct (r1 ! x) as [r1x | ] in *;
+    destruct (r2 ! x) as [r2x | ] in *;
+    congruence.
+Qed.
 End SAME_MEMORY.
 
 Lemma kill_mem_sound :
@@ -444,7 +468,7 @@ Proof.
     apply op_depends_on_memory_correct; auto.
   }
 Qed.
-  
+
 End SOUNDNESS.
 
 
@@ -521,6 +545,7 @@ Definition is_killed_in_fmap fmap pc res :=
 
 Definition sem_rel_b' := sem_rel_b fundef unit ge.
 Definition fmap_sem' := fmap_sem fundef unit ge.
+Definition subst_arg_ok' := subst_arg_ok fundef unit ge.
 Definition subst_args_ok' := subst_args_ok fundef unit ge.
 Definition kill_mem_sound' := kill_mem_sound fundef unit ge.
 
@@ -531,16 +556,11 @@ Lemma sem_rel_b_ge:
     forall rs : regset,
       (sem_rel_b' sp m rb2 rs) -> (sem_rel_b' sp m rb1 rs).
 Proof.
-  unfold sem_rel_b', sem_rel_b, sem_rel, sem_reg.
+  unfold sem_rel_b', sem_rel_b.
   destruct rb1 as [r1 | ];
     destruct rb2 as [r2 | ]; simpl;
       intros GE sp m rs RE; try contradiction.
-  intro x.
-  pose proof (RE x) as REx.
-  pose proof (GE x) as GEx.
-  destruct (r1 ! x) as [r1x | ] in *;
-    destruct (r2 ! x) as [r2x | ] in *;
-    congruence.
+  apply sem_rel_ge with (r2 := r2); assumption.
 Qed.
 
 Lemma apply_instr'_bot :
@@ -825,8 +845,6 @@ Proof.
   rewrite (subst_args_ok' (Vptr stk Ptrofs.zero) m) by assumption.
   constructor. auto.
 
-    (* TODO *)
-
 (* builtin *)
 - econstructor; split.
   eapply exec_Ibuiltin; eauto.
@@ -835,7 +853,7 @@ Proof.
   constructor; auto.
 
   simpl in *.
-  unfold fmap_sem in *.
+  unfold fmap_sem', fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
   
@@ -854,14 +872,15 @@ Proof.
   }
   apply top_ok.
   
+
 (* cond *)
 - econstructor; split.
   eapply exec_Icond; eauto.
-  rewrite subst_args_ok; eassumption.
+  rewrite (subst_args_ok' sp m); eassumption.
   constructor; auto.
 
   simpl in *.
-  unfold fmap_sem in *.
+  unfold fmap_sem', fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   apply sem_rel_b_ge with (rb2 := map # pc); trivial.
   replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
@@ -876,15 +895,15 @@ Proof.
   destruct (map # pc) in *; try contradiction.
   rewrite H.
   reflexivity.
-  
+
 (* jumptbl *)
 - econstructor; split.
   eapply exec_Ijumptable; eauto.
-  rewrite subst_arg_ok; eassumption.
+  rewrite (subst_arg_ok' sp m); eassumption.
   constructor; auto.
 
   simpl in *.
-  unfold fmap_sem in *.
+  unfold fmap_sem', fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   apply sem_rel_b_ge with (rb2 := map # pc); trivial.
   replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
@@ -907,7 +926,7 @@ Proof.
     econstructor; split.
     eapply exec_Ireturn; eauto.
     unfold regmap_optget.
-    rewrite subst_arg_ok by eassumption.
+    rewrite (subst_arg_ok' (Vptr stk Ptrofs.zero) m) by eassumption.
     constructor; auto.
   }
     econstructor; split.
@@ -921,7 +940,7 @@ Proof.
   constructor; auto.
 
   simpl in *.
-  unfold fmap_sem in *.
+  unfold fmap_sem', fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   apply sem_rel_b_ge with (rb2 := Some RELATION.top).
   {
@@ -942,12 +961,22 @@ Proof.
   constructor; auto.
 
   simpl in *.
-  unfold fmap_sem in *.
+  unfold fmap_sem', 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.
+  destruct (map # pc) as [mpc |] in *; simpl in *; auto.
   destruct H8 as [rel' RGE].
+
+  (* WRONG *)
+  eapply sem_rel_ge. exact RGE.
+  apply kill_reg_sound.
+  assert (sem_rel fundef unit ge sp m (kill_reg res rel') rs # res <- vres).
+  {
+    
+    eapply sem_rel_ge. eassumption.
+  }
+  eapply kill_reg_sound.
   eapply get_rb_killed; eauto.
 Qed.
 
-- 
cgit 


From 76049f12161c0eeeeec8841d2cc07d6601f39b4f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 12:14:55 +0100
Subject: now going back to op

---
 backend/CSE2proof.v | 51 ++++++---------------------------------------------
 1 file changed, 6 insertions(+), 45 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index ad11a8e9..8e7d7b3b 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -573,9 +573,9 @@ Qed.
 
 Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
 | match_frames_intro: forall res f sp pc rs,
-    (forall m : mem, (fmap_sem' sp m (forward_map f) pc rs)) ->
-    (is_killed_in_fmap (forward_map f) pc res) ->
-      match_frames (Stackframe res f sp pc rs)
+    (forall m : mem,
+     forall vres, (fmap_sem' sp m (forward_map f) pc rs # res <- vres)) ->
+    match_frames (Stackframe res f sp pc rs)
                  (Stackframe res (transf_function f) sp pc rs).
 
 Inductive match_states: RTL.state -> RTL.state -> Prop :=
@@ -794,7 +794,7 @@ Proof.
 
   constructor.
   {
-    intro m'.
+    intros m' vres.
     unfold fmap_sem', fmap_sem in *.
     destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
     destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
@@ -811,30 +811,10 @@ Proof.
       rewrite MPC.
       reflexivity.
     }
-    apply kill_reg_weaken.
+    apply kill_reg_sound.
     apply (kill_mem_sound' sp m).
     assumption.
   }
-  {
-  simpl in *.
-  unfold fmap_sem', fmap_sem in *.
-  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.
-  rewrite H in GE.
-  simpl in GE.
-  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
-  unfold is_killed_in_fmap, is_killed_in_map.
-  destruct (map # pc') as [mpc' |] eqn:MPC' ; try contradiction.
-
-  exists (kill_mem mpc).
-  assumption.
-  }
   
 (* tailcall *)
 - econstructor; split.
@@ -959,26 +939,7 @@ Proof.
   econstructor; split.
   eapply exec_return; eauto.
   constructor; auto.
-
-  simpl in *.
-  unfold fmap_sem', 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 *; simpl in *; auto.
-  destruct H8 as [rel' RGE].
-
-  (* WRONG *)
-  eapply sem_rel_ge. exact RGE.
-  apply kill_reg_sound.
-  assert (sem_rel fundef unit ge sp m (kill_reg res rel') rs # res <- vres).
-  {
-    
-    eapply sem_rel_ge. eassumption.
-  }
-  eapply kill_reg_sound.
-  eapply get_rb_killed; eauto.
-Qed.
+Admitted.
 
 
 Lemma transf_initial_states:
-- 
cgit 


From 47bcd22f7e1febf10bd0629c1774b7ab39fac872 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 13:25:12 +0100
Subject: CSE2 now works for expressions

---
 backend/CSE2proof.v | 105 +++++++++++++++++++++++++++++++++-------------------
 1 file changed, 66 insertions(+), 39 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 8e7d7b3b..558490ba 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -335,7 +335,7 @@ Qed.
 Lemma find_op_sound :
   forall rel : RELATION.t,
   forall op : operation,
-  forall src dst : reg,
+  forall src : reg,
   forall args: list reg,
   forall rs : regset,
     sem_rel rel rs ->
@@ -625,47 +625,75 @@ Proof.
   rewrite H.
   reflexivity.
 - (* op *)
-  (*
-  econstructor; split.
-  eapply exec_Iop with (v := v); eauto.
-  rewrite <- H0.
-  rewrite subst_args_ok by assumption.
-  apply eval_operation_preserved. exact symbols_preserved.
-  constructor; auto.
-
-  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.
+  unfold transf_instr in *.
+  destruct find_op_in_fmap eqn:FIND_OP.
   {
-      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
-      2: apply apply_instr'_bot.
-      simpl. tauto.
+    unfold find_op_in_fmap, fmap_sem', fmap_sem in *.
+    destruct (forward_map f) as [map |] eqn:MAP.
+    2: discriminate.
+    change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
+    destruct (map # pc) as [mpc | ] eqn:MPC.
+    2: discriminate.
+    econstructor; split.
+    {
+      eapply exec_Iop with (v := v); eauto.
+      simpl.
+      rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption.
+      assumption.
+    }
+    constructor; eauto.
+    unfold fmap_sem', fmap_sem in *.
+    rewrite MAP.
+    apply sem_rel_b_ge with (rb2 := Some (gen_oper op res args mpc)).
+    {
+      replace (Some (gen_oper op res args 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 sem_rel_b', sem_rel_b.
+    apply gen_oper_sound; auto.
   }
-  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.
-    simpl in GE.
-    apply sem_rel_b_ge with (rb2 := Some (move src res mpc)).
-    assumption.
-    replace v with (rs # src) by congruence.
-    apply move_ok.
-    assumption.
+    econstructor; split.
+    {
+      eapply exec_Iop with (v := v); eauto.
+      rewrite (subst_args_ok' sp m) by assumption.
+      rewrite <- H0.
+      apply eval_operation_preserved. exact symbols_preserved.
+    }
+    constructor; eauto.
+    unfold fmap_sem', fmap_sem in *.
+    unfold find_op_in_fmap, fmap_sem', fmap_sem in *.
+    destruct (forward_map f) as [map |] eqn:MAP.
+    2: constructor.
+    change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
+    destruct (map # pc) as [mpc | ] eqn:MPC.
+    2: contradiction.
+
+    apply sem_rel_b_ge with (rb2 := Some (gen_oper op res args mpc)).
+    {
+      replace (Some (gen_oper op res args 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 sem_rel_b', sem_rel_b.
+    apply gen_oper_sound; auto.
   }
-  rewrite KILL in GE.
-  apply sem_rel_b_ge with (rb2 := Some (kill res mpc)).
-  assumption.
-  apply kill_ok.
-  assumption.
-   *)
-  admit.
+    
 (* load *)
 - econstructor; split.
   assert (eval_addressing tge sp addr rs ## args = Some a).
@@ -970,6 +998,5 @@ Proof.
   eexact transf_final_states.
   exact step_simulation.
 Qed.
- *)
 
 End PRESERVATION.
\ No newline at end of file
-- 
cgit 


From 5412aea57eafe2868244a514471d480b83fc51bd Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 13:59:55 +0100
Subject: connected (just a silly problem)

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

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 558490ba..1d0a617a 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -405,7 +405,6 @@ Lemma kill_reg_weaken:
     sem_rel mpc rs ->
     sem_rel (kill_reg res mpc) rs.
 Proof.
-  Check kill_reg_sound.
   intros until rs.
   intros REL x.
   pose proof (REL x) as RELx.
@@ -471,6 +470,14 @@ Qed.
 
 End SOUNDNESS.
 
+Definition match_prog (p tp: RTL.program) :=
+  match_program (fun cu f tf => tf = transf_fundef f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_prog p (transf_program p).
+Proof.
+  intros. apply match_transform_program; auto.
+Qed.
 
 Section PRESERVATION.
 
@@ -849,7 +856,6 @@ Proof.
   eapply exec_Itailcall with (fd := transf_fundef fd); eauto.
     eapply find_function_translated; eauto.
     apply sig_preserved.
-  Check subst_args_ok.
   rewrite (subst_args_ok' (Vptr stk Ptrofs.zero) m) by assumption.
   constructor. auto.
 
-- 
cgit 


From a7df9f6f48aa9282cb66b02bb63ca047b01f09b4 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 15:01:39 +0100
Subject: still buggy

---
 backend/CSE2proof.v | 103 ++++++++++++++++++++++++++++++++++------------------
 1 file changed, 67 insertions(+), 36 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 1d0a617a..47b60902 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -249,7 +249,7 @@ Proof.
   destruct s; simpl in *; destruct negb; simpl; congruence.
 Qed.
 
-Lemma oper1_sound :
+Lemma oper2_sound :
   forall rel : RELATION.t,
   forall op : operation,
   forall dst : reg,
@@ -259,12 +259,12 @@ Lemma oper1_sound :
     sem_rel rel rs ->
     not (In dst args) ->
     eval_operation genv sp op (rs ## args) m = Some v ->
-    sem_rel (oper1 op dst args rel) (rs # dst <- v).
+    sem_rel (oper2 op dst args rel) (rs # dst <- v).
 Proof.
   intros until v.
   intros REL NOT_IN EVAL x.
   pose proof (kill_reg_sound rel dst rs v REL x) as KILL.
-  unfold oper1.
+  unfold oper2.
   destruct (peq x dst).
   {
     subst x.
@@ -282,7 +282,7 @@ Proof.
   exact KILL.
 Qed.
 
-Lemma oper_sound :
+Lemma oper1_sound :
   forall rel : RELATION.t,
   forall op : operation,
   forall dst : reg,
@@ -291,45 +291,18 @@ Lemma oper_sound :
   forall v,
     sem_rel rel rs ->
     eval_operation genv sp op (rs ## args) m = Some v ->
-    sem_rel (oper op dst args rel) (rs # dst <- v).
+    sem_rel (oper1 op dst args rel) (rs # dst <- v).
 Proof.
   intros until v.
   intros REL EVAL.
-  unfold oper.
+  unfold oper1.
   destruct in_dec.
   {
     apply kill_reg_sound; auto. 
   }
-  apply oper1_sound; auto.
+  apply oper2_sound; auto.
 Qed.
 
-Lemma gen_oper_sound :
-  forall rel : RELATION.t,
-  forall op : operation,
-  forall dst : reg,
-  forall args: list reg,
-  forall rs : regset,
-  forall v,
-    sem_rel rel rs ->
-    eval_operation genv sp op (rs ## args) m = Some v ->
-    sem_rel (gen_oper op dst args rel) (rs # dst <- v).
-Proof.
-  intros until v.
-  intros REL EVAL.
-  unfold gen_oper.
-  destruct op.
-  { destruct args as [ | h0 t0].
-    apply oper_sound; auto.
-    destruct t0.
-    {
-      simpl in *.
-      replace v with (rs # h0) by congruence.
-      apply move_sound; auto.
-    }
-    apply oper_sound; auto.
-  }
-  all: apply oper_sound; auto.
-Qed.
 
 
 Lemma find_op_sound :
@@ -399,6 +372,59 @@ Proof.
   apply REC; auto.
 Qed.
 
+Lemma oper_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall v,
+    sem_rel rel rs ->
+    eval_operation genv sp op (rs ## args) m = Some v ->
+    sem_rel (oper op dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL EVAL.
+  unfold oper.
+  destruct find_op eqn:FIND.
+  {
+    assert (eval_operation genv sp op rs ## args m = Some rs # r).
+    {
+      apply (find_op_sound rel); trivial.
+    }
+    replace v with (rs # r) by congruence.
+    apply move_sound; auto.
+  }
+  apply oper1_sound; trivial.
+Qed.
+
+Lemma gen_oper_sound :
+  forall rel : RELATION.t,
+  forall op : operation,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall v,
+    sem_rel rel rs ->
+    eval_operation genv sp op (rs ## args) m = Some v ->
+    sem_rel (gen_oper op dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL EVAL.
+  unfold gen_oper.
+  destruct op.
+  { destruct args as [ | h0 t0].
+    apply oper_sound; auto.
+    destruct t0.
+    {
+      simpl in *.
+      replace v with (rs # h0) by congruence.
+      apply move_sound; auto.
+    }
+    apply oper_sound; auto.
+  }
+  all: apply oper_sound; auto.
+Qed.
 
 Lemma kill_reg_weaken:
   forall res mpc rs,
@@ -645,8 +671,13 @@ Proof.
     {
       eapply exec_Iop with (v := v); eauto.
       simpl.
-      rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption.
-      assumption.
+      rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
+      {
+        rewrite MAP in H0.
+        rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption.
+        assumption.
+      }
+      unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
     }
     constructor; eauto.
     unfold fmap_sem', fmap_sem in *.
-- 
cgit 


From 3e15c72f5a5e34ac2e96e77022b2129125abcdd0 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 15:24:11 +0100
Subject: much better - seems to eliminate CSE not containing loads

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

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 47b60902..049423b0 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -372,6 +372,21 @@ Proof.
   apply REC; auto.
 Qed.
 
+Lemma forward_move_map:
+  forall rel args rs,
+    sem_rel rel rs ->
+    rs ## (map (forward_move rel) args) = rs ## args.
+Proof.
+  induction args; simpl; trivial.
+  intros rs REL.
+  f_equal.
+  2: (apply IHargs; assumption).
+  unfold forward_move, sem_rel, sem_reg, sem_sym_val in *.
+  pose proof (REL a) as RELa.
+  destruct (rel ! a); trivial.
+  destruct s; congruence.
+Qed.
+
 Lemma oper_sound :
   forall rel : RELATION.t,
   forall op : operation,
@@ -388,10 +403,11 @@ Proof.
   unfold oper.
   destruct find_op eqn:FIND.
   {
-    assert (eval_operation genv sp op rs ## args m = Some rs # r).
+    assert (eval_operation genv sp op rs ## (map (forward_move rel) args) m = Some rs # r) as FIND_OP.
     {
       apply (find_op_sound rel); trivial.
     }
+    rewrite forward_move_map in FIND_OP by assumption.
     replace v with (rs # r) by congruence.
     apply move_sound; auto.
   }
-- 
cgit 


From 4414da3d406685a05ae20ba8994c1a9247137874 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 15:58:25 +0100
Subject: find_load_sound

---
 backend/CSE2proof.v | 96 ++++++++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 92 insertions(+), 4 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 049423b0..796f3054 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -42,6 +42,11 @@ Definition sem_sym_val sym rs :=
   | SMove src => Some (rs # src)
   | SOp op args =>
     eval_operation genv sp op (rs ## args) m
+  | SLoad chunk addr args =>
+    match eval_addressing genv sp addr rs##args with
+    | Some a => Mem.loadv chunk m a
+    | None   => None
+    end
   end.
     
 Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) : option val :=
@@ -142,6 +147,11 @@ Proof.
     rewrite args_unaffected by exact EXISTS.
     assumption.
   }
+  { destruct existsb eqn:EXISTS; simpl.
+    { reflexivity. }
+    rewrite args_unaffected by exact EXISTS.
+    assumption.
+  }
 Qed.
 
 Lemma write_same:
@@ -303,8 +313,6 @@ Proof.
   apply oper2_sound; auto.
 Qed.
 
-
-
 Lemma find_op_sound :
   forall rel : RELATION.t,
   forall op : operation,
@@ -351,8 +359,7 @@ Proof.
     unfold find_op_fold.
     destruct start.
     assumption.
-    destruct sv.
-    { trivial. }
+    destruct sv; trivial.
     destruct eq_operation; trivial.
     subst op0.
     destruct eq_args; trivial.
@@ -372,6 +379,87 @@ Proof.
   apply REC; auto.
 Qed.
 
+Lemma find_load_sound :
+  forall rel : RELATION.t,
+  forall chunk : memory_chunk,
+  forall addr : addressing,
+  forall src : reg,
+  forall args: list reg,
+  forall rs : regset,
+    sem_rel rel rs ->
+    find_load rel chunk addr args = Some src ->
+    match eval_addressing genv sp addr rs##args with
+    | Some a => (Mem.loadv chunk m a) = Some (rs # src)
+    | None => True
+    end.
+Proof.
+  intros until rs.
+  unfold find_load.
+  rewrite PTree.fold_spec.
+  intro REL.
+  assert (
+     forall start,
+             match start with
+             | None => True
+             | Some src =>
+               match eval_addressing genv sp addr rs##args with
+               | Some a => (Mem.loadv chunk m a) = Some (rs # src)
+               | None => True
+               end               
+             end ->
+    fold_left
+    (fun (a : option reg) (p : positive * sym_val) =>
+     find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements rel) start =
+    Some src ->
+    match eval_addressing genv sp addr rs##args with
+               | Some a => (Mem.loadv chunk m a) = Some (rs # src)
+               | None => True
+               end ) as REC.
+  
+  {
+    unfold sem_rel, sem_reg in REL.
+    generalize (PTree.elements_complete rel).
+    generalize (PTree.elements rel).
+    induction l; simpl.
+    {
+      intros.
+      subst start.
+      assumption.
+    }
+    destruct a as [r sv]; simpl.
+    intros COMPLETE start GEN.
+    apply IHl.
+    {
+      intros.
+      apply COMPLETE.
+      right.
+      assumption.
+    }
+    unfold find_load_fold.
+    destruct start.
+    assumption.
+    destruct sv; trivial.
+    destruct chunk_eq; trivial.
+    subst chunk0.
+    destruct eq_addressing; trivial.
+    subst addr0.
+    destruct eq_args; trivial.
+    subst args0.
+    simpl.
+    assert ((rel ! r) = Some (SLoad chunk addr args)) as RELatr.
+    {
+      apply COMPLETE.
+      left.
+      reflexivity.
+    }
+    pose proof (REL r) as RELr.
+    rewrite RELatr in RELr.
+    simpl in RELr.
+    destruct eval_addressing; trivial.
+  }
+  apply REC; auto.
+Qed.
+
 Lemma forward_move_map:
   forall rel args rs,
     sem_rel rel rs ->
-- 
cgit 


From 2bcac2e8c00493555fb0fb1acd730bab53eb7369 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 16:12:52 +0100
Subject: load_sound

---
 backend/CSE2proof.v | 96 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 96 insertions(+)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 796f3054..5cb85fc2 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -530,6 +530,102 @@ Proof.
   all: apply oper_sound; auto.
 Qed.
 
+
+Lemma load2_sound :
+  forall rel : RELATION.t,
+  forall chunk : memory_chunk,
+  forall addr : addressing,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall a,
+  forall v,
+    sem_rel rel rs ->
+    not (In dst args) ->
+    eval_addressing genv sp addr (rs ## args) = Some a ->
+    Mem.loadv chunk m a = Some v ->
+    sem_rel (load2 chunk addr dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL NOT_IN ADDR LOAD x.
+  pose proof (kill_reg_sound rel dst rs v REL x) as KILL.
+  unfold load2.
+  destruct (peq x dst).
+  {
+    subst x.
+    unfold sem_reg.
+    rewrite PTree.gss.
+    rewrite Regmap.gss.
+    simpl.
+    rewrite args_replace_dst by auto.
+    destruct eval_addressing; congruence.
+  }
+  rewrite Regmap.gso by congruence.
+  unfold sem_reg.
+  rewrite PTree.gso by congruence.
+  rewrite Regmap.gso in KILL by congruence.
+  exact KILL.
+Qed.
+
+Lemma load1_sound :
+  forall rel : RELATION.t,
+  forall chunk : memory_chunk,
+  forall addr : addressing,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall a,
+  forall v,
+    sem_rel rel rs ->
+    eval_addressing genv sp addr (rs ## args) = Some a ->
+    Mem.loadv chunk m a = Some v ->
+    sem_rel (load1 chunk addr dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL ADDR LOAD.
+  unfold load1.
+  destruct in_dec.
+  {
+    apply kill_reg_sound; auto. 
+  }
+  apply load2_sound with (a := a); auto.
+Qed.
+
+Lemma load_sound :
+  forall rel : RELATION.t,
+  forall chunk : memory_chunk,
+  forall addr : addressing,
+  forall dst : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall a,
+  forall v,
+    sem_rel rel rs ->
+    eval_addressing genv sp addr (rs ## args) = Some a ->
+    Mem.loadv chunk m a = Some v ->
+    sem_rel (load chunk addr dst args rel) (rs # dst <- v).
+Proof.
+  intros until v.
+  intros REL ADDR LOAD.
+  unfold load.
+  destruct find_load eqn:FIND.
+  {
+    assert (match eval_addressing genv sp addr rs##(map (forward_move rel) args) with
+    | Some a => (Mem.loadv chunk m a) = Some (rs # r)
+    | None => True
+    end) as FIND_LOAD.
+    {
+      apply (find_load_sound rel); trivial.
+    }
+    rewrite forward_move_map in FIND_LOAD by assumption.
+    destruct eval_addressing in *.
+    2: discriminate.
+    replace v with (rs # r) by congruence.
+    apply move_sound; auto.
+  }
+  apply load1_sound with (a := a); trivial.
+Qed.
+
 Lemma kill_reg_weaken:
   forall res mpc rs,
     sem_rel mpc rs ->
-- 
cgit 


From 3bdfc2288714f1c238a5b59586aa1409f4eda056 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 28 Jan 2020 16:38:57 +0100
Subject: with loads too ?

---
 backend/CSE2proof.v | 73 ++++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 67 insertions(+), 6 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 5cb85fc2..fe2ade4b 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -460,6 +460,24 @@ Proof.
   apply REC; auto.
 Qed.
 
+Lemma find_load_sound' :
+  forall rel : RELATION.t,
+  forall chunk : memory_chunk,
+  forall addr : addressing,
+  forall src : reg,
+  forall args: list reg,
+  forall rs : regset,
+  forall a,
+    sem_rel rel rs ->
+    find_load rel chunk addr args = Some src ->
+    eval_addressing genv sp addr rs##args = Some a ->
+    (Mem.loadv chunk m a) = Some (rs # src).
+Proof.
+  intros until a. intros REL LOAD ADDR.
+  pose proof (find_load_sound rel chunk addr src args rs REL LOAD) as Z.
+  destruct eval_addressing in *; congruence.
+Qed.
+
 Lemma forward_move_map:
   forall rel args rs,
     sem_rel rel rs ->
@@ -933,7 +951,49 @@ Proof.
   }
     
 (* load *)
-- econstructor; split.
+- unfold transf_instr in *.
+  destruct find_load_in_fmap eqn:FIND_LOAD.
+  {
+    unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
+    destruct (forward_map f) as [map |] eqn:MAP.
+    2: discriminate.
+    change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
+    destruct (map # pc) as [mpc | ] eqn:MPC.
+    2: discriminate.
+    econstructor; split.
+    {
+      eapply exec_Iop with (v := v); eauto.
+      simpl.
+      rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
+      {
+        rewrite find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs) in H1; trivial.
+        rewrite MAP in H0.
+        assumption.
+      }
+      unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
+    }
+    constructor; eauto.
+    unfold fmap_sem', fmap_sem in *.
+    rewrite MAP.
+    apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
+    {
+      replace (Some (load chunk addr dst args 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.
+      simpl.
+      reflexivity.
+    }
+    unfold sem_rel_b', sem_rel_b.
+    apply load_sound with (a := a); auto.
+  }
+  {  
+  econstructor; split.
   assert (eval_addressing tge sp addr rs ## args = Some a).
   rewrite <- H0.
   apply eval_addressing_preserved. exact symbols_preserved.
@@ -945,9 +1005,9 @@ Proof.
   unfold fmap_sem', fmap_sem in *.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
-  apply sem_rel_b_ge with (rb2 := Some (kill_reg dst mpc)).
+  apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
   {
-    replace (Some (kill_reg dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+    replace (Some (load chunk addr dst args 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.
@@ -956,11 +1016,12 @@ Proof.
     unfold apply_instr'.
     rewrite H.
     rewrite MPC.
+    simpl.
     reflexivity.
   }
-  apply kill_reg_sound.
-  assumption.
-
+  apply load_sound with (a := a); assumption.
+  }
+  
   (* NOT IN THIS VERSION 
 - (* load notrap1 *)
   econstructor; split.
-- 
cgit