From 79c039d7b33878d00f22ad8542dc30a78aa8b70a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 9 Dec 2020 11:34:35 +0100
Subject: CSE3 + conditions proof

---
 backend/CSE3analysis.v | 25 ++++++++++++++++++-
 backend/CSE3proof.v    | 67 +++++++++++++++++++++++++-------------------------
 2 files changed, 58 insertions(+), 34 deletions(-)

(limited to 'backend')

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
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index cc4ab686..50a32d56 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -352,6 +352,23 @@ Qed.
 
 Hint Resolve rel_ge : cse3.
 
+Lemma relb_ge:
+  forall inv inv'
+         (GE : RB.ge inv' inv)
+         ctx sp rs m
+         (REL: sem_rel_b sp ctx inv rs m),
+  sem_rel_b sp ctx inv' rs m.
+Proof.
+  intros.
+  destruct inv; cbn in *.
+  2: contradiction.
+  destruct inv'; cbn in *.
+  2: assumption.
+  eapply rel_ge; eassumption.
+Qed.
+
+Hint Resolve relb_ge : cse3.
+
 Lemma sem_rhs_sop :
   forall sp op rs args m v,
   eval_operation ge sp op rs ## args m = Some v ->
@@ -946,23 +963,15 @@ Proof.
       rewrite andb_true_iff in IND_step_me.
       destruct IND_step_me as [IND_so [IND_not ZOT]].
       clear ZOT.
-      destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *.
-      2: discriminate.
-      destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *.
-      2: discriminate.
-      rewrite rel_leb_correct in IND_so.
-      rewrite rel_leb_correct in IND_not.
+      rewrite relb_leb_correct in IND_so.
+      rewrite relb_leb_correct in IND_not.
+      
       destruct b.
-      {
-        rewrite INV_so.
-        cbn.
-        eapply rel_ge; eauto.
-      }
-      {
-        rewrite INV_not.
-        cbn.
-        eapply rel_ge; eauto.
-      }
+      { eapply relb_ge. eassumption. apply apply_cond_sound; auto. }
+      eapply relb_ge. eassumption. apply apply_cond_sound; trivial.
+      rewrite eval_negate_condition.
+      rewrite H0.
+      reflexivity.
       (* END INVARIANT *)
         }
         unfold sem_rel_b in REL.
@@ -1048,23 +1057,15 @@ Proof.
       rewrite andb_true_iff in IND_step_me.
       destruct IND_step_me as [IND_so [IND_not ZOT]].
       clear ZOT.
-      destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *.
-      2: discriminate.
-      destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *.
-      2: discriminate.
-      rewrite rel_leb_correct in IND_so.
-      rewrite rel_leb_correct in IND_not.
+      rewrite relb_leb_correct in IND_so.
+      rewrite relb_leb_correct in IND_not.
+      
       destruct b.
-      {
-        rewrite INV_so.
-        cbn.
-        eapply rel_ge; eauto.
-      }
-      {
-        rewrite INV_not.
-        cbn.
-        eapply rel_ge; eauto.
-      }
+      { eapply relb_ge. eassumption. apply apply_cond_sound; auto. }
+      eapply relb_ge. eassumption. apply apply_cond_sound; trivial.
+      rewrite eval_negate_condition.
+      rewrite H0.
+      reflexivity.
       (* END INVARIANT *)
       
   - (* Ijumptable *)
@@ -1171,7 +1172,7 @@ Proof.
       apply wt_regset_assign; trivial.
       rewrite WTRES0.
       exact WTRES.
-Admitted.
+Qed.
 
 Lemma transf_initial_states:
   forall S1, RTL.initial_state prog S1 ->
-- 
cgit