From 9ec01ece75310b28c79b57697238b57517eb4392 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 27 Jan 2020 18:01:36 +0100
Subject: oper_sound

---
 backend/CSE2.v | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

(limited to 'backend/CSE2.v')

diff --git a/backend/CSE2.v b/backend/CSE2.v
index 87460f90..a70c3d9f 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -305,6 +305,12 @@ 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.
+
 Section SOUNDNESS.
   Parameter F V : Type.
   Parameter genv: Genv.t F V.
@@ -509,6 +515,27 @@ Proof.
   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_sound; auto. 
+  }
+  apply oper1_sound; auto.
+Qed.
+
 (*
 Definition apply_instr instr x :=
   match instr with
-- 
cgit