Adding info field for branching in RTL, LTL, XTL and all associated passes

32 files changed, 97 insertions, 95 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index d18b07a9..2323c050 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -314,10 +314,10 @@ Definition pair_instr_block
           Some(BSbuiltin ef args res mv1 args' res' mv2 s)
       | _ => None
       end
-  | Icond cond args s1 s2 =>
+  | Icond cond args s1 s2 i =>
       let (mv1, b1) := extract_moves nil b in
       match b1 with
-      | Lcond cond' args' s1' s2' :: b2 =>
+      | Lcond cond' args' s1' s2' i' :: b2 =>
           assertion (eq_condition cond cond');
           assertion (peq s1 s1');
           assertion (peq s2 s2');
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index b6880860..3c7df58a 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -169,11 +169,11 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr
                          (Ibuiltin ef args res s)
                          (expand_moves mv1
                            (Lbuiltin ef args' res' :: expand_moves mv2 (Lbranch s :: k)))
-  | ebs_cond: forall cond args mv args' s1 s2 k,
+  | ebs_cond: forall cond args mv args' s1 s2 k i i',
       wf_moves mv ->
       expand_block_shape (BScond cond args mv args' s1 s2)
-                         (Icond cond args s1 s2)
-                         (expand_moves mv (Lcond cond args' s1 s2 :: k))
+                         (Icond cond args s1 s2 i)
+                         (expand_moves mv (Lcond cond args' s1 s2 i' :: k))
   | ebs_jumptable: forall arg mv arg' tbl k,
       wf_moves mv ->
       expand_block_shape (BSjumptable arg mv arg' tbl)
diff --git a/backend/CSE.v b/backend/CSE.v
index 2827161d..1936d4e4 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -496,7 +496,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
           | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ =>
               set_res_unknown before res
           end
-      | Icond cond args ifso ifnot =>
+      | Icond cond args ifso ifnot _ =>
           before
       | Ijumptable arg tbl =>
           before
@@ -549,10 +549,10 @@ Definition transf_instr (n: numbering) (instr: instruction) :=
       let (n1, vl) := valnum_regs n args in
       let (addr', args') := reduce _ combine_addr n1 addr args vl in
       Istore chunk addr' args' src s
-  | Icond cond args s1 s2 =>
+  | Icond cond args s1 s2 i =>
       let (n1, vl) := valnum_regs n args in
       let (cond', args') := reduce _ combine_cond n1 cond args vl in
-      Icond cond' args' s1 s2
+      Icond cond' args' s1 s2 i
   | _ =>
       instr
   end.
diff --git a/backend/CSE2.v b/backend/CSE2.v
index d5444e3b..900a7517 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -405,7 +405,7 @@ Qed.
 Definition apply_instr instr (rel : RELATION.t) : RB.t :=
   match instr with
   | Inop _
-  | Icond _ _ _ _
+  | Icond _ _ _ _ _
   | Ijumptable _ _ => Some rel
   | Istore chunk addr args _ _ => Some (kill_store chunk addr args rel)
   | Iop op args dst _ => Some (gen_oper op dst args rel)
@@ -485,8 +485,8 @@ Definition transf_instr (fmap : option (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 i =>
+    Icond cond (subst_args fmap pc args) s1 s2 i
   | Ijumptable arg tbl =>
     Ijumptable (subst_arg fmap pc arg) tbl
   | Ireturn (Some arg) =>
diff --git a/backend/Constprop.v b/backend/Constprop.v
index eda41b39..0be9438c 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -69,7 +69,7 @@ Fixpoint successor_rec (n: nat) (f: function) (ae: AE.t) (pc: node) : node :=
       match f.(fn_code)!pc with
       | Some (Inop s) =>
           successor_rec n' f ae s
-      | Some (Icond cond args s1 s2) =>
+      | Some (Icond cond args s1 s2 _) =>
           match resolve_branch (eval_static_condition cond (aregs ae args)) with
           | Some b => successor_rec n' f ae (if b then s1 else s2)
           | None => pc
@@ -217,14 +217,14 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem)
              end
           | _, _ => dfl
           end
-      | Icond cond args s1 s2 =>
+      | Icond cond args s1 s2 i =>
           let aargs := aregs ae args in
           match resolve_branch (eval_static_condition cond aargs) with
           | Some b =>
               if b then Inop s1 else Inop s2
           | None =>
               let (cond', args') := cond_strength_reduction cond args aargs in
-              Icond cond' args' s1 s2
+              Icond cond' args' s1 s2 i
           end
       | Ijumptable arg tbl =>
           match areg ae arg with
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 63cfee24..60663503 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -142,8 +142,8 @@ Inductive match_pc (f: function) (rs: regset) (m: mem): nat -> node -> node -> P
       f.(fn_code)!pc = Some (Inop s) ->
       match_pc f rs m n s pcx ->
       match_pc f rs m (S n) pc pcx
-  | match_pc_cond: forall n pc cond args s1 s2 pcx,
-      f.(fn_code)!pc = Some (Icond cond args s1 s2) ->
+  | match_pc_cond: forall n pc cond args s1 s2 pcx i,
+      f.(fn_code)!pc = Some (Icond cond args s1 s2 i) ->
       (forall b,
         eval_condition cond rs##args m = Some b ->
         match_pc f rs m n (if b then s1 else s2) pcx) ->
diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index 1f208a91..3412a6fa 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -142,7 +142,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t)
        nmem_dead_stack f.(fn_stacksize))
   | Some(Ibuiltin ef args res s) =>
       transfer_builtin approx!!pc ef args res ne nm
-  | Some(Icond cond args s1 s2) =>
+  | Some(Icond cond args s1 s2 _) =>
       if peq s1 s2 then after else 
         (add_needs args (needs_of_condition cond) ne, nm)
   | Some(Ijumptable arg tbl) =>
@@ -192,7 +192,7 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t)
       if nmem_contains (snd an!!pc) (aaddr_arg approx!!pc dst) sz
       then instr
       else Inop s
-  | Icond cond args s1 s2 =>
+  | Icond cond args s1 s2 _ =>
       if peq s1 s2 then Inop s1 else instr
   | _ =>
       instr
diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index 82c17367..af85efe4 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -134,8 +134,8 @@ Definition verify_match_inst dupmap inst tinst :=
           else Error (msg "Different ef in Ibuiltin")
       | _ => Error (msg "verify_match_inst Ibuiltin") end
 
-  | Icond cond lr n1 n2 => match tinst with
-      | Icond cond' lr' n1' n2' =>
+  | Icond cond lr n1 n2 i => match tinst with
+      | Icond cond' lr' n1' n2' i' =>
           if (list_eq_dec Pos.eq_dec lr lr') then
             if (eq_condition cond cond') then
               do u1 <- verify_is_copy dupmap n1 n1';
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index d3036b9a..86bc06c9 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -39,7 +39,7 @@ let bfs code entrypoint =
             | Ibuiltin(_, _, _, n) -> Queue.add n to_visit
             | Ijumptable(_, ln) -> List.iter (fun n -> Queue.add n to_visit) ln
             | Itailcall _ | Ireturn _ -> ()
-            | Icond (_, _, n1, n2) -> Queue.add n1 to_visit; Queue.add n2 to_visit
+            | Icond (_, _, n1, n2, _) -> Queue.add n1 to_visit; Queue.add n2 to_visit
             | Inop n | Iop (_, _, _, n) | Iload (_, _, _, _, _, n) | Istore (_, _, _, _, n) -> Queue.add n to_visit
       end
     done;
@@ -56,7 +56,7 @@ let get_predecessors_rtl code =
     let succ = match i with
       | Inop n | Iop (_,_,_,n) | Iload (_, _,_,_,_,n) | Istore (_,_,_,_,n)
       | Icall (_,_,_,_,n) | Ibuiltin (_, _, _, n) -> [n]
-      | Icond (_,_,n1,n2) -> [n1;n2]
+      | Icond (_,_,n1,n2,_) -> [n1;n2]
       | Ijumptable (_,ln) -> ln
       | Itailcall _ | Ireturn _ -> []
     in List.iter (fun s ->
@@ -123,7 +123,7 @@ let get_loop_headers code entrypoint =
           | Some i -> let next_visits = (match i with
             | Icall (_, _, _, _, n) | Ibuiltin (_, _, _, n) | Inop n | Iop (_, _, _, n)
             | Iload (_, _, _, _, _, n) | Istore (_, _, _, _, n) -> [n]
-            | Icond (_, _, n1, n2) -> [n1; n2]
+            | Icond (_, _, n1, n2, _) -> [n1; n2]
             | Itailcall _ | Ireturn _ -> []
             | Ijumptable (_, ln) -> ln
             ) in dfs_visit code next_visits;
@@ -218,7 +218,7 @@ let get_directions code entrypoint =
     (* Printf.printf "\n"; *)
     List.iter (fun n ->
       match (get_some @@ PTree.get n code) with
-      | Icond (cond, lr, ifso, ifnot) ->
+      | Icond (cond, lr, ifso, ifnot, _) ->
           (* Printf.printf "Analyzing %d.." (P.to_int n); *)
           let heuristics = [ do_call_heuristic; do_opcode_heuristic;
             do_return_heuristic; do_store_heuristic; do_loop_heuristic ] in
@@ -251,9 +251,9 @@ let to_ttl_inst direction = function
 | Icall (s, ri, lr, r, n) -> Tleaf (Icall(s, ri, lr, r, n))
 | Itailcall (s, ri, lr) -> Tleaf (Itailcall(s, ri, lr))
 | Ibuiltin (ef, lbr, br, n) -> Tleaf (Ibuiltin(ef, lbr, br, n))
-| Icond (cond, lr, n, n') -> (match direction with
-    | false -> Tnext (n', Icond(cond, lr, n, n'))
-    | true -> Tnext (n, Icond(cond, lr, n, n')))
+| Icond (cond, lr, n, n', i) -> (match direction with
+    | false -> Tnext (n', Icond(cond, lr, n, n', i))
+    | true -> Tnext (n, Icond(cond, lr, n, n', i)))
 | Ijumptable (r, ln) -> Tleaf (Ijumptable(r, ln))
 
 let rec to_ttl_code_rec directions = function
@@ -299,7 +299,7 @@ let dfs code entrypoint =
                   | Itailcall _ | Ireturn _ -> [] 
                   | _ -> failwith "Tleaf case not handled in dfs" )
               | Tnext (n,i) -> (dfs_list code [n]) @ match i with
-                  | Icond (_, _, n1, n2) -> dfs_list code [n1; n2]
+                  | Icond (_, _, n1, n2, _) -> dfs_list code [n1; n2]
                   | Inop _ | Iop _ | Iload _ | Istore _ -> []
                   | _ -> failwith "Tnext case not handled in dfs"
           end
@@ -314,7 +314,7 @@ let get_predecessors_ttl code =
   | Tnext (_, i) -> let succ = match i with
       | Inop n | Iop (_,_,_,n) | Iload (_, _,_,_,_,n) | Istore (_,_,_,_,n)
       | Icall (_,_,_,_,n) | Ibuiltin (_, _, _, n) -> [n]
-      | Icond (_,_,n1,n2) -> [n1;n2]
+      | Icond (_,_,n1,n2,_) -> [n1;n2]
       | Ijumptable (_,ln) -> ln
       | _ -> []
       in List.iter (fun s -> preds := PTree.set s (node::(get_some @@ PTree.get s !preds)) !preds) succ
@@ -413,10 +413,10 @@ let rec change_pointers code n n' = function
         | Ibuiltin(a, b, c, n0) -> assert (n0 == n); Ibuiltin(a, b, c, n')
         | Ijumptable(a, ln) -> assert (optbool @@ List.find_opt (fun e -> e == n) ln);
                                Ijumptable(a, List.map (fun e -> if (e == n) then n' else e) ln)
-        | Icond(a, b, n1, n2) -> assert (n1 == n || n2 == n);
+        | Icond(a, b, n1, n2, i) -> assert (n1 == n || n2 == n);
                                  let n1' = if (n1 == n) then n' else n1
                                  in let n2' = if (n2 == n) then n' else n2
-                                 in Icond(a, b, n1', n2')
+                                 in Icond(a, b, n1', n2', i)
         | Inop n0 -> assert (n0 == n); Inop n'
         | Iop (a, b, c, n0) -> assert (n0 == n); Iop (a, b, c, n')
         | Iload (a, b, c, d, e, n0) -> assert (n0 == n); Iload (a, b, c, d, e, n')
@@ -504,11 +504,12 @@ let rec invert_iconds_trace code = function
   | n::[] -> code
   | n :: n' :: t ->
       let code' = match ptree_get_some n code with
-        | Icond (c, lr, ifso, ifnot) ->
+        | Icond (c, lr, ifso, ifnot, i) ->
             assert (n' == ifso || n' == ifnot);
             if (n' == ifso) then (
               (* Printf.printf "Reversing ifso/ifnot for node %d\n" (P.to_int n); *)
-              PTree.set n (Icond (Op.negate_condition c, lr, ifnot, ifso)) code )
+              let i' = match i with None -> None | Some b -> Some (not b) in
+              PTree.set n (Icond (Op.negate_condition c, lr, ifnot, ifso, i')) code )
             else code
         | _ -> code
       in invert_iconds_trace code' (n'::t)
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index 466b4b75..6b598dc7 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -23,12 +23,12 @@ Inductive match_inst (dupmap: PTree.t node): instruction -> instruction -> Prop
       match_inst dupmap (Itailcall s ri lr) (Itailcall s ri lr)
   | match_inst_builtin: forall n n' ef la br,
       dupmap!n' = (Some n) -> match_inst dupmap (Ibuiltin ef la br n) (Ibuiltin ef la br n')
-  | match_inst_cond: forall ifso ifso' ifnot ifnot' c lr,
+  | match_inst_cond: forall ifso ifso' ifnot ifnot' c lr i i',
       dupmap!ifso' = (Some ifso) -> dupmap!ifnot' = (Some ifnot) ->
-      match_inst dupmap (Icond c lr ifso ifnot) (Icond c lr ifso' ifnot')
-  | match_inst_revcond: forall ifso ifso' ifnot ifnot' c lr,
+      match_inst dupmap (Icond c lr ifso ifnot i) (Icond c lr ifso' ifnot' i')
+  | match_inst_revcond: forall ifso ifso' ifnot ifnot' c lr i i',
       dupmap!ifso' = (Some ifso) -> dupmap!ifnot' = (Some ifnot) ->
-      match_inst dupmap (Icond c lr ifso ifnot) (Icond (negate_condition c) lr ifnot' ifso')
+      match_inst dupmap (Icond c lr ifso ifnot i) (Icond (negate_condition c) lr ifnot' ifso' i')
   | match_inst_jumptable: forall ln ln' r,
       list_forall2 (fun n n' => (dupmap!n' = (Some n))) ln ln' ->
       match_inst dupmap (Ijumptable r ln) (Ijumptable r ln')
diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index c73b0213..7cfd411f 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -250,7 +250,7 @@ Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) :=
 Definition apply_instr instr x :=
   match instr with
   | Inop _
-  | Icond _ _ _ _
+  | Icond _ _ _ _ _
   | Ijumptable _ _
   | Istore _ _ _ _ _ => Some x
   | Iop Omove (src :: nil) dst _ => Some (move src dst x)
@@ -309,8 +309,8 @@ Definition transf_instr (fmap : option (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 i =>
+    Icond cond (subst_args fmap pc args) s1 s2 i
   | Ijumptable arg tbl =>
     Ijumptable (subst_arg fmap pc arg) tbl
   | Ireturn (Some arg) =>
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 9cf535b9..8c7e1898 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -397,9 +397,9 @@ Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit :=
   | Ibuiltin ef args res s =>
       set_instr (spc ctx pc)
                 (Ibuiltin ef (map (sbuiltinarg ctx) args) (sbuiltinres ctx res) (spc ctx s))
-  | Icond cond args s1 s2 =>
+  | Icond cond args s1 s2 info =>
       set_instr (spc ctx pc)
-                (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2))
+                (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2) info)
   | Ijumptable r tbl =>
       set_instr (spc ctx pc)
                 (Ijumptable (sreg ctx r) (List.map (spc ctx) tbl))
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index e20fb373..eba026ec 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -312,9 +312,9 @@ Inductive tr_instr: context -> node -> instruction -> code -> Prop :=
       match res with BR r => Ple r ctx.(mreg) | _ => True end ->
       c!(spc ctx pc) = Some (Ibuiltin ef (map (sbuiltinarg ctx) args) (sbuiltinres ctx res) (spc ctx s)) ->
       tr_instr ctx pc (Ibuiltin ef args res s) c
-  | tr_cond: forall ctx pc cond args s1 s2 c,
-      c!(spc ctx pc) = Some (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2)) ->
-      tr_instr ctx pc (Icond cond args s1 s2) c
+  | tr_cond: forall ctx pc cond args s1 s2 c i,
+      c!(spc ctx pc) = Some (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2) i) ->
+      tr_instr ctx pc (Icond cond args s1 s2 i) c
   | tr_jumptable: forall ctx pc r tbl c,
       c!(spc ctx pc) = Some (Ijumptable (sreg ctx r) (List.map (spc ctx) tbl)) ->
       tr_instr ctx pc (Ijumptable r tbl) c
diff --git a/backend/LTL.v b/backend/LTL.v
index ee8b4826..3edd60a2 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -37,7 +37,7 @@ Inductive instruction: Type :=
   | Ltailcall (sg: signature) (ros: mreg + ident)
   | Lbuiltin (ef: external_function) (args: list (builtin_arg loc)) (res: builtin_res mreg)
   | Lbranch (s: node)
-  | Lcond (cond: condition) (args: list mreg) (s1 s2: node)
+  | Lcond (cond: condition) (args: list mreg) (s1 s2: node) (info: option bool)
   | Ljumptable (arg: mreg) (tbl: list node)
   | Lreturn.
 
@@ -263,11 +263,11 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Lbranch: forall s f sp pc bb rs m,
       step (Block s f sp (Lbranch pc :: bb) rs m)
         E0 (State s f sp pc rs m)
-  | exec_Lcond: forall s f sp cond args pc1 pc2 bb rs b pc rs' m,
+  | exec_Lcond: forall s f sp cond args pc1 pc2 bb rs b pc rs' m i,
       eval_condition cond (reglist rs args) m = Some b ->
       pc = (if b then pc1 else pc2) ->
       rs' = undef_regs (destroyed_by_cond cond) rs ->
-      step (Block s f sp (Lcond cond args pc1 pc2 :: bb) rs m)
+      step (Block s f sp (Lcond cond args pc1 pc2 i :: bb) rs m)
         E0 (State s f sp pc rs' m)
   | exec_Ljumptable: forall s f sp arg tbl bb rs m n pc rs',
       rs (R arg) = Vint n ->
@@ -328,7 +328,7 @@ Fixpoint successors_block (b: bblock) : list node :=
   | nil => nil                          (**r should never happen *)
   | Ltailcall _ _ :: _ => nil
   | Lbranch s :: _ => s :: nil
-  | Lcond _ _ s1 s2 :: _ => s1 :: s2 :: nil
+  | Lcond _ _ s1 s2 _ :: _ => s1 :: s2 :: nil
   | Ljumptable _ tbl :: _ => tbl
   | Lreturn :: _ => nil
   | instr :: b' => successors_block b'
diff --git a/backend/Linearize.v b/backend/Linearize.v
index 4216958c..66b36428 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -179,7 +179,7 @@ Fixpoint linearize_block (b: LTL.bblock) (k: code) : code :=
       Lbuiltin ef args res :: linearize_block b' k
   | LTL.Lbranch s :: b' =>
       add_branch s k
-  | LTL.Lcond cond args s1 s2 :: b' =>
+  | LTL.Lcond cond args s1 s2 _ :: b' =>
       if starts_with s1 k then
         Lcond (negate_condition cond) args s2 :: add_branch s1 k
       else
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index eed58f8d..c9a5d620 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -81,7 +81,7 @@ let basic_blocks f joins =
        | [] -> assert false
        | Lbranch s :: _ -> next_in_block blk minpc s
        | Ltailcall (sig0, ros) :: _ -> end_block blk minpc
-       | Lcond (cond, args, ifso, ifnot) :: _ ->
+       | Lcond (cond, args, ifso, ifnot, _) :: _ ->
              end_block blk minpc; start_block ifso; start_block ifnot
        | Ljumptable(arg, tbl) :: _ ->
              end_block blk minpc; List.iter start_block tbl
@@ -165,7 +165,7 @@ let forward_sequences code entry =
           | Lbuiltin _ -> assert false
           | Ltailcall _ | Lreturn -> ([], [])
           | Lbranch n -> let ln, rem = traverse_fallthrough code n in (ln, rem)
-          | Lcond (_, _, ifso, ifnot) -> let ln, rem = traverse_fallthrough code ifnot in (ln, [ifso] @ rem)
+          | Lcond (_, _, ifso, ifnot, _) -> let ln, rem = traverse_fallthrough code ifnot in (ln, [ifso] @ rem)
           | Ljumptable(_, ln) -> match ln with
               | [] -> ([], [])
               | n :: ln -> let lln, rem = traverse_fallthrough code n in (lln, ln @ rem)
@@ -219,7 +219,7 @@ let can_be_merged code s s' =
   | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
   | Lbuiltin _ | Ltailcall _ | Lreturn -> false
   | Lbranch n -> n == first_s'
-  | Lcond (_, _, ifso, ifnot) -> ifnot == first_s'
+  | Lcond (_, _, ifso, ifnot, _) -> ifnot == first_s'
   | Ljumptable (_, ln) ->
       match ln with
       | [] -> false
@@ -303,7 +303,7 @@ let get_loop_edges code entry =
           | Lbuiltin _ -> assert false
           | Ltailcall _ | Lreturn -> []
           | Lbranch n -> [n]
-          | Lcond (_, _, ifso, ifnot) -> [ifso; ifnot]
+          | Lcond (_, _, ifso, ifnot, _) -> [ifso; ifnot]
           | Ljumptable(_, ln) -> ln
           ) in dfs_visit code (Some node) next_visits;
           visited := PTree.set node Visited !visited;
@@ -371,7 +371,7 @@ let construct_depmap code entry fs =
               match (last_element bb) with
               | Ltailcall _ | Lreturn -> []
               | Lbranch n -> (check_and_update_depmap node n; [n])
-              | Lcond (_, _, ifso, ifnot) -> begin
+              | Lcond (_, _, ifso, ifnot, _) -> begin
                   check_and_update_depmap node ifso;
                   check_and_update_depmap node ifnot;
                   [ifso; ifnot]
diff --git a/backend/Liveness.v b/backend/Liveness.v
index afe11ae6..9652b363 100644
--- a/backend/Liveness.v
+++ b/backend/Liveness.v
@@ -94,7 +94,7 @@ Definition transfer
       | Ibuiltin ef args res s =>
           reg_list_live (params_of_builtin_args args)
             (reg_list_dead (params_of_builtin_res res) after)
-      | Icond cond args ifso ifnot =>
+      | Icond cond args ifso ifnot _ =>
           reg_list_live args after
       | Ijumptable arg tbl =>
           reg_live arg after
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index b309a9f2..f173e374 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -83,7 +83,7 @@ let print_instruction pp succ = function
         (print_builtin_args loc) args
   | Lbranch s ->
       print_succ pp s succ
-  | Lcond(cond, args, s1, s2) ->
+  | Lcond(cond, args, s1, s2, _) ->
       fprintf pp "if (%a) goto %d else goto %d"
         (print_condition mreg) (cond, args)
         (P.to_int s1) (P.to_int s2)
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index c25773e5..5eab9901 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -75,7 +75,7 @@ let print_instruction pp (pc, i) =
         (name_of_external ef)
         (print_builtin_args reg) args;
       print_succ pp s (pc - 1)
-  | Icond(cond, args, s1, s2) ->
+  | Icond(cond, args, s1, s2, _) ->
       fprintf pp "if (%a) goto %d else goto %d\n"
         (PrintOp.print_condition reg) (cond, args)
         (P.to_int s1) (P.to_int s2)
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index 1c7655fb..d1b79623 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -104,7 +104,7 @@ let print_instruction pp succ = function
         (print_builtin_args var) args
   | Xbranch s ->
       print_succ pp s succ
-  | Xcond(cond, args, s1, s2) ->
+  | Xcond(cond, args, s1, s2, _) ->
       fprintf pp "if (%a) goto %d else goto %d"
         (print_condition var) (cond, args)
         (P.to_int s1) (P.to_int s2)
diff --git a/backend/RTL.v b/backend/RTL.v
index 29a49311..dec59ca2 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -67,11 +67,12 @@ Inductive instruction: Type :=
       (** [Ibuiltin ef args dest succ] calls the built-in function
           identified by [ef], giving it the values of [args] as arguments.
           It stores the return value in [dest] and branches to [succ]. *)
-  | Icond: condition -> list reg -> node -> node -> instruction
-      (** [Icond cond args ifso ifnot] evaluates the boolean condition
+  | Icond: condition -> list reg -> node -> node -> option bool -> instruction
+      (** [Icond cond args ifso ifnot info] evaluates the boolean condition
           [cond] over the values of registers [args].  If the condition
           is true, it transitions to [ifso].  If the condition is false,
-          it transitions to [ifnot]. *)
+          it transitions to [ifnot]. [info] is a ghost field there to provide
+          information relative to branch prediction. *)
   | Ijumptable: reg -> list node -> instruction
       (** [Ijumptable arg tbl] transitions to the node that is the [n]-th
           element of the list [tbl], where [n] is the unsigned integer
@@ -262,8 +263,8 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp pc rs m)
          t (State s f sp pc' (regmap_setres res vres rs) m')
   | exec_Icond:
-      forall s f sp pc rs m cond args ifso ifnot b pc',
-      (fn_code f)!pc = Some(Icond cond args ifso ifnot) ->
+      forall s f sp pc rs m cond args ifso ifnot b pc' predb,
+      (fn_code f)!pc = Some(Icond cond args ifso ifnot predb) ->
       eval_condition cond rs##args m = Some b ->
       pc' = (if b then ifso else ifnot) ->
       step (State s f sp pc rs m)
@@ -403,7 +404,7 @@ Definition successors_instr (i: instruction) : list node :=
   | Icall sig ros args res s => s :: nil
   | Itailcall sig ros args => nil
   | Ibuiltin ef args res s => s :: nil
-  | Icond cond args ifso ifnot => ifso :: ifnot :: nil
+  | Icond cond args ifso ifnot _ => ifso :: ifnot :: nil
   | Ijumptable arg tbl => tbl
   | Ireturn optarg => nil
   end.
@@ -424,7 +425,7 @@ Definition instr_uses (i: instruction) : list reg :=
   | Itailcall sig (inl r) args => r :: args
   | Itailcall sig (inr id) args => args
   | Ibuiltin ef args res s => params_of_builtin_args args
-  | Icond cond args ifso ifnot => args
+  | Icond cond args ifso ifnot _ => args
   | Ijumptable arg tbl => arg :: nil
   | Ireturn None => nil
   | Ireturn (Some arg) => arg :: nil
@@ -442,7 +443,7 @@ Definition instr_defs (i: instruction) : option reg :=
   | Itailcall sig ros args => None
   | Ibuiltin ef args res s =>
       match res with BR r => Some r | _ => None end
-  | Icond cond args ifso ifnot => None
+  | Icond cond args ifso ifnot _ => None
   | Ijumptable arg tbl => None
   | Ireturn optarg => None
   end.
@@ -485,7 +486,7 @@ Definition max_reg_instr (m: positive) (pc: node) (i: instruction) :=
   | Ibuiltin ef args res s =>
       fold_left Pos.max (params_of_builtin_args args)
         (fold_left Pos.max (params_of_builtin_res res) m)
-  | Icond cond args ifso ifnot => fold_left Pos.max args m
+  | Icond cond args ifso ifnot _ => fold_left Pos.max args m
   | Ijumptable arg tbl => Pos.max arg m
   | Ireturn None => m
   | Ireturn (Some arg) => Pos.max arg m
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 2c27944a..ac98f3a1 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -479,7 +479,7 @@ with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node)
   match a with
   | CEcond c al =>
       do rl <- alloc_regs map al;
-      do nt <- add_instr (Icond c rl ntrue nfalse);
+      do nt <- add_instr (Icond c rl ntrue nfalse None);
          transl_exprlist map al rl nt
   | CEcondition a b c =>
       do nc <- transl_condexpr map c ntrue nfalse;
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 92b48e2b..30ad7d82 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -744,9 +744,9 @@ Inductive tr_expr (c: code):
 
 with tr_condition (c: code):
        mapping -> list reg -> condexpr -> node -> node -> node -> Prop :=
-  | tr_CEcond: forall map pr cond bl ns ntrue nfalse n1 rl,
+  | tr_CEcond: forall map pr cond bl ns ntrue nfalse n1 rl i,
       tr_exprlist c map pr bl ns n1 rl ->
-      c!n1 = Some (Icond cond rl ntrue nfalse) ->
+      c!n1 = Some (Icond cond rl ntrue nfalse i) ->
       tr_condition c map pr (CEcond cond bl) ns ntrue nfalse
   | tr_CEcondition: forall map pr a1 a2 a3 ns ntrue nfalse n2 n3,
       tr_condition c map pr a1 ns n2 n3 ->
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 857f2211..15ed6d8a 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -139,11 +139,11 @@ Inductive wt_instr : instruction -> Prop :=
       valid_successor s ->
       wt_instr (Ibuiltin ef args res s)
   | wt_Icond:
-      forall cond args s1 s2,
+      forall cond args s1 s2 i,
       map env args = type_of_condition cond ->
       valid_successor s1 ->
       valid_successor s2 ->
-      wt_instr (Icond cond args s1 s2)
+      wt_instr (Icond cond args s1 s2 i)
   | wt_Ijumptable:
       forall arg tbl,
       env arg = Tint ->
@@ -313,7 +313,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
         | _ => type_builtin_args e args sig.(sig_args)
         end;
       type_builtin_res e1 res (proj_sig_res sig)
- | Icond cond args s1 s2 =>
+ | Icond cond args s1 s2 _ =>
       do x1 <- check_successor s1;
       do x2 <- check_successor s2;
       S.set_list e args (type_of_condition cond)
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index f2658b04..ffe26933 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -295,8 +295,8 @@ let block_of_RTL_instr funsig tyenv = function
          (Xbuiltin(ef, args2, res2) ::
             movelist (params_of_builtin_res res2) (params_of_builtin_res res1)
                [Xbranch s])
-  | RTL.Icond(cond, args, s1, s2) ->
-      [Xcond(cond, vregs tyenv args, s1, s2)]
+  | RTL.Icond(cond, args, s1, s2, i) ->
+      [Xcond(cond, vregs tyenv args, s1, s2, i)]
   | RTL.Ijumptable(arg, tbl) ->
       [Xjumptable(vreg tyenv arg, tbl)]
   | RTL.Ireturn None ->
@@ -380,7 +380,7 @@ let live_before instr after =
       vset_addargs args (vset_removeres res after)
   | Xbranch s ->
       after
-  | Xcond(cond, args, s1, s2) ->
+  | Xcond(cond, args, s1, s2, _) ->
       List.fold_right VSet.add args after
   | Xjumptable(arg, tbl) ->
       VSet.add arg after
@@ -575,7 +575,7 @@ let spill_costs f =
             charge_list 10 1 (params_of_builtin_res res)
         end
     | Xbranch _ -> ()
-    | Xcond(cond, args, _, _) ->
+    | Xcond(cond, args, _, _, _) ->
         charge_list 10 1 args
     | Xjumptable(arg, _) ->
         charge 10 1 arg
@@ -718,7 +718,7 @@ let add_interfs_instr g instr live =
       end
   | Xbranch s ->
       ()
-  | Xcond(cond, args, s1, s2) ->
+  | Xcond(cond, args, s1, s2, _) ->
       add_interfs_destroyed g live (destroyed_by_cond cond)
   | Xjumptable(arg, tbl) ->
       add_interfs_destroyed g live destroyed_by_jumptable
@@ -797,7 +797,7 @@ let tospill_instr alloc instr ts =
          (addlist_tospill alloc (params_of_builtin_res res) ts)
   | Xbranch s ->
       ts
-  | Xcond(cond, args, s1, s2) ->
+  | Xcond(cond, args, s1, s2, _) ->
       addlist_tospill alloc args ts
   | Xjumptable(arg, tbl) ->
       add_tospill alloc arg ts
@@ -990,9 +990,9 @@ let spill_instr tospill eqs instr =
       (c1 @ Xbuiltin(ef, args', res') :: c2, eqs2)
   | Xbranch s ->
       ([instr], eqs)
-  | Xcond(cond, args, s1, s2) ->
+  | Xcond(cond, args, s1, s2, i) ->
      let (args', c1, eqs1) = reload_vars tospill eqs args in
-     (c1 @ [Xcond(cond, args', s1, s2)], eqs1)
+     (c1 @ [Xcond(cond, args', s1, s2, i)], eqs1)
   | Xjumptable(arg, tbl) ->
       let (arg', c1, eqs1) = reload_var tospill eqs arg in
       (c1 @ [Xjumptable(arg', tbl)], eqs1)
@@ -1128,8 +1128,8 @@ let transl_instr alloc instr k =
                        AST.map_builtin_res (mreg_of alloc) res) :: k
   | Xbranch s ->
       LTL.Lbranch s :: []
-  | Xcond(cond, args, s1, s2) ->
-      LTL.Lcond(cond, mregs_of alloc args, s1, s2) :: []
+  | Xcond(cond, args, s1, s2, i) ->
+      LTL.Lcond(cond, mregs_of alloc args, s1, s2, i) :: []
   | Xjumptable(arg, tbl) ->
       LTL.Ljumptable(mreg_of alloc arg, tbl) :: []
   | Xreturn optarg ->
diff --git a/backend/Renumber.v b/backend/Renumber.v
index 7ba16658..2727b979 100644
--- a/backend/Renumber.v
+++ b/backend/Renumber.v
@@ -48,7 +48,7 @@ Definition renum_instr (i: instruction) : instruction :=
   | Icall sg ros args res s => Icall sg ros args res (renum_pc s)
   | Itailcall sg ros args => i
   | Ibuiltin ef args res s => Ibuiltin ef args res (renum_pc s)
-  | Icond cond args s1 s2 => Icond cond args (renum_pc s1) (renum_pc s2)
+  | Icond cond args s1 s2 info => Icond cond args (renum_pc s1) (renum_pc s2) info
   | Ijumptable arg tbl => Ijumptable arg (List.map renum_pc tbl)
   | Ireturn or => i
   end.
diff --git a/backend/Splitting.ml b/backend/Splitting.ml
index 78eb66a5..3ca45c3b 100644
--- a/backend/Splitting.ml
+++ b/backend/Splitting.ml
@@ -162,8 +162,8 @@ let ren_instr f maps pc i =
   | Ibuiltin(ef, args, res, s) ->
       Ibuiltin(ef, List.map (AST.map_builtin_arg (ren_reg before)) args,
                    AST.map_builtin_res (ren_reg after) res, s)
-  | Icond(cond, args, s1, s2) ->
-      Icond(cond, ren_regs before args, s1, s2)
+  | Icond(cond, args, s1, s2, i) ->
+      Icond(cond, ren_regs before args, s1, s2, i)
   | Ijumptable(arg, tbl) ->
       Ijumptable(ren_reg before arg, tbl)
   | Ireturn optarg ->
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index da1ce45a..a4c4a195 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -78,11 +78,11 @@ Definition record_gotos (f: LTL.function) : U.t :=
 Definition tunnel_instr (uf: U.t) (i: instruction) : instruction :=
   match i with
   | Lbranch s => Lbranch (U.repr uf s)
-  | Lcond cond args s1 s2 =>
+  | Lcond cond args s1 s2 info =>
       let s1' := U.repr uf s1 in let s2' := U.repr uf s2 in
       if peq s1' s2'
       then Lbranch s1'
-      else Lcond cond args s1' s2'
+      else Lcond cond args s1' s2' info
   | Ljumptable arg tbl => Ljumptable arg (List.map (U.repr uf) tbl)
   | _ => i
   end.
diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v
index 1b5f2547..93ca7af4 100644
--- a/backend/Unusedglob.v
+++ b/backend/Unusedglob.v
@@ -53,7 +53,7 @@ Definition ref_instruction (i: instruction) : list ident :=
   | Itailcall _ (inl r) _ => nil
   | Itailcall _ (inr id) _ => id :: nil
   | Ibuiltin _ args _ _ => globals_of_builtin_args args
-  | Icond cond _ _ _ => nil
+  | Icond cond _ _ _ _ => nil
   | Ijumptable _ _ => nil
   | Ireturn _ => nil
   end.
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index e25d2e5f..2e79d1a9 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -156,7 +156,7 @@ Definition transfer (f: function) (rm: romem) (pc: node) (ae: aenv) (am: amem) :
       VA.Bot
   | Some(Ibuiltin ef args res s) =>
       transfer_builtin ae am rm ef args res
-  | Some(Icond cond args s1 s2) =>
+  | Some(Icond cond args s1 s2 _) =>
       VA.State ae am
   | Some(Ijumptable arg tbl) =>
       VA.State ae am
diff --git a/backend/XTL.ml b/backend/XTL.ml
index c496fafb..1d8e89c0 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -36,7 +36,7 @@ type instruction =
   | Xtailcall of signature * (var, ident) sum * var list
   | Xbuiltin of external_function * var builtin_arg list * var builtin_res
   | Xbranch of node
-  | Xcond of condition * var list * node * node
+  | Xcond of condition * var list * node * node * bool option
   | Xjumptable of var * node list
   | Xreturn of var list
 
@@ -105,7 +105,7 @@ let twin_reg r =
 let rec successors_block = function
   | Xbranch s :: _ -> [s]
   | Xtailcall(sg, vos, args) :: _ -> []
-  | Xcond(cond, args, s1, s2) :: _ -> [s1; s2]
+  | Xcond(cond, args, s1, s2, _) :: _ -> [s1; s2]
   | Xjumptable(arg, tbl) :: _ -> tbl
   | Xreturn  _:: _ -> []
   | instr :: blk -> successors_block blk
@@ -179,7 +179,7 @@ let type_instr = function
       type_builtin_res res (proj_sig_res sg)
   | Xbranch s ->
       ()
-  | Xcond(cond, args, s1, s2) ->
+  | Xcond(cond, args, s1, s2, _) ->
       set_vars_type args (type_of_condition cond)
   | Xjumptable(arg, tbl) ->
       set_var_type arg Tint
diff --git a/backend/XTL.mli b/backend/XTL.mli
index b4b77fab..7b7f7186 100644
--- a/backend/XTL.mli
+++ b/backend/XTL.mli
@@ -37,7 +37,7 @@ type instruction =
   | Xtailcall of signature * (var, ident) sum * var list
   | Xbuiltin of external_function * var builtin_arg list * var builtin_res
   | Xbranch of node
-  | Xcond of condition * var list * node * node
+  | Xcond of condition * var list * node * node * bool option
   | Xjumptable of var * node list
   | Xreturn of var list