CSE3 + conditions proof

1 files changed, 24 insertions, 1 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 46ae4aea..383147bb 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -461,10 +461,33 @@ Section OPERATIONS.
     | _ => rel
     end.
 
+  Definition apply_cond1 cond args (rel : RELATION.t) : RB.t :=
+    match eq_find (Cond (negate_condition cond) args) with
+    | Some eq_id =>
+      if PSet.contains rel eq_id
+      then RB.bot
+      else Some rel
+    | None => Some rel
+    end.
+
+  Definition apply_cond0 cond args (rel : RELATION.t) : RELATION.t :=
+    match eq_find (Cond cond args) with
+    | Some eq_id => PSet.add eq_id rel
+    | None => rel
+    end.
+
+  Definition apply_cond cond args (rel : RELATION.t) : RB.t :=
+    match apply_cond1 cond args rel with
+    | Some rel => Some (apply_cond0 cond args rel)
+    | None => RB.bot
+    end.
+      
   Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) :=
   match instr with
   | Inop pc' => (pc', (Some rel))::nil
-  | Icond _ _ ifso ifnot _ => (ifso, (Some rel))::(ifnot, (Some rel))::nil
+  | Icond cond args ifso ifnot _ =>
+    (ifso,  (apply_cond cond args rel))::
+    (ifnot, (apply_cond (negate_condition cond) args rel))::nil
   | Ijumptable _ targets => List.map (fun pc' => (pc', (Some rel))) targets
   | Istore chunk addr args src pc' =>
     (pc', (Some (store tenv chunk addr args src rel)))::nil