From 6ae48a2f079d6c420df57cb8616692c3d6cdd0ca Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 16 Apr 2020 18:01:25 +0200
Subject: adapt for Icond with predicted direction

---
 backend/CSE3.v         |  4 ++--
 backend/CSE3analysis.v |  2 +-
 backend/Inject.v       |  4 ++--
 backend/Injectproof.v  | 16 ++++++++--------
 4 files changed, 13 insertions(+), 13 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE3.v b/backend/CSE3.v
index d0dc3aef..352cc895 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -62,8 +62,8 @@ Definition transf_instr (fmap : PMap.t RB.t)
     Icall sig ros (subst_args fmap pc args) dst s
   | Itailcall sig ros args =>
     Itailcall sig ros (subst_args fmap pc args)
-  | Icond cond args s1 s2 =>
-    Icond cond (subst_args fmap pc args) s1 s2
+  | Icond cond args s1 s2 expected =>
+    Icond cond (subst_args fmap pc args) s1 s2 expected
   | Ijumptable arg tbl =>
     Ijumptable (subst_arg fmap pc arg) tbl
   | Ireturn (Some arg) =>
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 12fb2d1f..90ce4ce7 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -328,7 +328,7 @@ Section OPERATIONS.
   Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t :=
   match instr with
   | Inop _
-  | Icond _ _ _ _
+  | Icond _ _ _ _ _
   | Ijumptable _ _ => Some rel
   | Istore chunk addr args src _ =>
     Some (store chunk addr args src (tenv src) rel)
diff --git a/backend/Inject.v b/backend/Inject.v
index 2350c149..971a5423 100644
--- a/backend/Inject.v
+++ b/backend/Inject.v
@@ -34,7 +34,7 @@ Definition successor (i : instruction) : node :=
   | Istore _ _ _ _ pc' => pc'
   | Icall _ _ _ _ pc' => pc'
   | Ibuiltin _ _ _ pc' => pc'
-  | Icond _ _ pc' _ => pc'
+  | Icond _ _ pc' _ _ => pc'
   | Itailcall _ _ _
   | Ijumptable _ _
   | Ireturn _ => 1
@@ -47,7 +47,7 @@ Definition alter_successor (i : instruction) (pc' : node) : instruction :=
   | Iload trap chunk addr args dst _ => Iload trap chunk addr args dst pc'
   | Istore chunk addr args src _ => Istore chunk addr args src pc'
   | Ibuiltin ef args res _ => Ibuiltin ef args res pc'
-  | Icond cond args _ pc2 => Icond cond args pc' pc2
+  | Icond cond args _ pc2 expected => Icond cond args pc' pc2 expected
   | Icall sig ros args res _ => Icall sig ros args res pc'
   | Itailcall _ _ _
   | Ijumptable _ _
diff --git a/backend/Injectproof.v b/backend/Injectproof.v
index 2506bcc8..75fed25f 100644
--- a/backend/Injectproof.v
+++ b/backend/Injectproof.v
@@ -1651,9 +1651,9 @@ Section INJECTOR.
              destruct SKIP as [trs' [MATCH PLUS]].
              econstructor; split.
              * eapply Smallstep.plus_left.
-               ** apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot).
+               ** apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot) (predb := predb).
                    exact ALTER.
-                   replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity.
+                   replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity.
                    rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
                    simpl. reflexivity.
                ** apply Smallstep.plus_star.
@@ -1669,28 +1669,28 @@ Section INJECTOR.
              destruct SKIP as [trs' [MATCH PLUS]].
              econstructor; split.
              * eapply Smallstep.plus_one.
-               apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot).
+               apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot) (predb := predb).
                exact ALTER.
-               replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity.
+               replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity.
                rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
                simpl. reflexivity.
              * simpl. constructor; auto.
         + destruct b eqn:B.
           * econstructor; split.
             ** eapply Smallstep.plus_one.
-               apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot).
+               apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot) (predb := predb).
                *** rewrite transf_function_preserves with (f:=f); eauto.
                    eapply max_pc_function_sound; eauto.
-               *** replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity.
+               *** replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity.
                    rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
                *** reflexivity.
             ** constructor; auto.
           *  econstructor; split.
             ** eapply Smallstep.plus_one.
-               apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot).
+               apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot) (predb := predb).
                *** rewrite transf_function_preserves with (f:=f); eauto.
                    eapply max_pc_function_sound; eauto.
-               *** replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity.
+               *** replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity.
                    rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
                *** reflexivity.
             ** constructor; auto.
-- 
cgit