From fe7d4a81d4999c71f856372716a4a198c46ded8e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 27 Jan 2020 18:14:47 +0100
Subject: gen_oper_sound

---
 backend/CSE2.v | 38 +++++++++++++++++++++++++++++++++++++-
 1 file changed, 37 insertions(+), 1 deletion(-)

(limited to 'backend/CSE2.v')

diff --git a/backend/CSE2.v b/backend/CSE2.v
index a70c3d9f..1278d729 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -305,12 +305,20 @@ Definition oper1 (op: operation) (dst : reg) (args : list reg)
                                      | Move_case arg' => arg'
                                      | Other_case _ => arg
                                      end) args)) rel'.
+
 Definition oper (op: operation) (dst : reg) (args : list reg)
            (rel : RELATION.t) :=
   if List.in_dec peq dst args
   then kill dst rel
   else oper1 op dst args rel.
 
+Definition gen_oper (op: operation) (dst : reg) (args : list reg)
+           (rel : RELATION.t) :=
+  match op, args with
+  | Omove, src::nil => move src dst rel
+  | _, _ => oper op dst args rel
+  end.
+
 Section SOUNDNESS.
   Parameter F V : Type.
   Parameter genv: Genv.t F V.
@@ -536,7 +544,35 @@ Proof.
   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.
+  (*
 Definition apply_instr instr x :=
   match instr with
   | Inop _
-- 
cgit