From d09c509f8d1bd8335ebedbe260320bb43c5a2723 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 26 Nov 2020 15:11:15 +0100
Subject: ajouté Cond, tout passe
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 backend/CSE3analysis.v | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'backend/CSE3analysis.v')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 137282a4..4b616568 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -146,7 +146,8 @@ Proof.
 Defined.
 
 Inductive equation_or_condition :=
-  | Equ : reg -> sym_op -> list reg -> equation_or_condition.
+| Equ : reg -> sym_op -> list reg -> equation_or_condition
+| Cond : condition -> list reg -> equation_or_condition.
 
 Definition eq_dec_equation :
   forall eq eq' : equation_or_condition, {eq = eq'} + {eq <> eq'}.
@@ -154,6 +155,7 @@ Proof.
   generalize peq.
   generalize eq_dec_sym_op.
   generalize eq_dec_args.
+  generalize eq_condition.
   decide equality.
 Defined.
 
@@ -172,6 +174,7 @@ Definition get_reg_kills (eqs : PTree.t equation_or_condition) :
                 | Equ lhs sop args =>
                   add_i_j lhs eqno
                           (add_ilist_j args eqno already)
+                | Cond cond args => add_ilist_j args eqno already
                 end) eqs
              (PMap.init PSet.empty).
 
@@ -182,15 +185,13 @@ Definition eq_cond_depends_on_mem eq_cond :=
     | SLoad _ _ => true
     | SOp op => op_depends_on_memory op
     end
+  | Cond cond args => cond_depends_on_memory cond
   end.
 
 Definition eq_cond_depends_on_store eq_cond :=
   match eq_cond with
-  | Equ lhs sop args =>
-    match sop with
-    | SLoad _ _ => true
-    | SOp op => false
-    end
+  | Equ _ (SLoad _ _) _ => true
+  | _ => false
   end.
 
 Definition get_mem_kills (eqs : PTree.t equation_or_condition) : PSet.t :=
@@ -229,6 +230,7 @@ Definition get_moves (eqs : PTree.t equation_or_condition) :
                   if is_smove sop
                   then add_i_j lhs eqno already
                   else already
+                | _ => already
                 end) eqs (PMap.init PSet.empty).
   
 Record eq_context := mkeqcontext
@@ -294,11 +296,11 @@ Section OPERATIONS.
     | None => None
     | Some src =>
       match eq_catalog ctx src with
-      | None => None
       | Some (Equ eq_lhs eq_sop eq_args) =>
         if eq_dec_sym_op sop eq_sop && eq_dec_args args eq_args
         then Some eq_lhs
         else None
+      | _ => None
       end
     end.
 
-- 
cgit