Selection: keep track of continuation statement in sel_stmt

The continuation statement is passed to the if-conversion heuristic,
which does not do anything with it currently.

backend/Selection.v

@@ -368,36 +368,48 @@ Fixpoint classify_stmt (s: Cminor.stmt) : stmt_class :=
     and the type at which selection is done. *)
 
 Parameter if_conversion_heuristic:
-  Cminor.expr -> Cminor.expr -> Cminor.expr -> AST.typ -> bool.
+  ident -> Cminor.expr -> Cminor.expr -> Cminor.expr -> AST.typ -> CminorSel.stmt -> bool.
 
 Definition if_conversion_base
       (ki: known_idents) (env: typenv)
-      (cond: Cminor.expr) (id: ident) (ifso ifnot:  Cminor.expr) : option stmt :=
+      (cond: Cminor.expr) (id: ident) (ifso ifnot:  Cminor.expr)
+      (kont: stmt) : option stmt :=
   let ty := env id in
   if is_known ki id
   && safe_expr ki ifso && safe_expr ki ifnot
-  && if_conversion_heuristic cond ifso ifnot ty
+  && if_conversion_heuristic id cond ifso ifnot ty kont
   then option_map
          (fun sel => Sassign id sel)
          (sel_select_opt ty cond ifso ifnot)
   else None.
 
 Definition if_conversion
       (ki: known_idents) (env: typenv)
-      (cond: Cminor.expr) (ifso ifnot: Cminor.stmt) : option stmt :=
+      (cond: Cminor.expr) (ifso ifnot: Cminor.stmt)
+      (kont: stmt) : option stmt :=
   match classify_stmt ifso, classify_stmt ifnot with
   | SCskip, SCassign id a =>
-      if_conversion_base ki env cond id (Cminor.Evar id) a
+      if_conversion_base ki env cond id (Cminor.Evar id) a kont
   | SCassign id a, SCskip =>
-      if_conversion_base ki env cond id a (Cminor.Evar id)
+      if_conversion_base ki env cond id a (Cminor.Evar id) kont
   | SCassign id1 a1, SCassign id2 a2 =>
-      if ident_eq id1 id2 then if_conversion_base ki env cond id1 a1 a2 else None
+      if ident_eq id1 id2
+      then if_conversion_base ki env cond id1 a1 a2 kont
+      else None
   | _, _ => None
   end.
 
 (** Conversion from Cminor statements to Cminorsel statements. *)
 
-Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt :=
+(** [sel_stmt ki env s k] returns the Cminorsel statement corresponding
+    to the Cminor statement [s].
+    [ki] and [env] are typing information used for if-conversion.
+    [k] is the "continuation" of [s]: a Cminorsel statement that comes
+    next after executing the translation of [s].  It's only approximate,
+    and used only by the if-conversion heuristics. [Sskip] is used as
+    the "don't know" value for [k]. *)
+
+Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) (k: stmt): res stmt :=
   match s with
   | Cminor.Sskip => OK Sskip
   | Cminor.Sassign id e => OK (Sassign id (sel_expr e))
@@ -416,19 +428,20 @@ Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt :
       | _            => Stailcall sg (inl _ (sel_expr fn)) (sel_exprlist args)
       end)
   | Cminor.Sseq s1 s2 =>
-      do s1' <- sel_stmt ki env s1; do s2' <- sel_stmt ki env s2;
+      do s2' <- sel_stmt ki env s2 k;
+      do s1' <- sel_stmt ki env s1 s2';
       OK (Sseq s1' s2')
   | Cminor.Sifthenelse e ifso ifnot =>
-      match if_conversion ki env e ifso ifnot with
+      match if_conversion ki env e ifso ifnot k with
       | Some s => OK s
       | None =>
-          do ifso' <- sel_stmt ki env ifso; do ifnot' <- sel_stmt ki env ifnot;
+          do ifso' <- sel_stmt ki env ifso k; do ifnot' <- sel_stmt ki env ifnot k;
           OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot')
       end
   | Cminor.Sloop body =>
-      do body' <- sel_stmt ki env body; OK (Sloop body')
+      do body' <- sel_stmt ki env body Sskip; OK (Sloop body')
   | Cminor.Sblock body =>
-      do body' <- sel_stmt ki env body; OK (Sblock body')
+      do body' <- sel_stmt ki env body k; OK (Sblock body')
   | Cminor.Sexit n => OK (Sexit n)
   | Cminor.Sswitch false e cases dfl =>
       let t := compile_switch Int.modulus dfl cases in
@@ -443,7 +456,7 @@ Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt :
   | Cminor.Sreturn None => OK (Sreturn None)
   | Cminor.Sreturn (Some e) => OK (Sreturn (Some (sel_expr e)))
   | Cminor.Slabel lbl body =>
-      do body' <- sel_stmt ki env body; OK (Slabel lbl body')
+      do body' <- sel_stmt ki env body k; OK (Slabel lbl body')
   | Cminor.Sgoto lbl => OK (Sgoto lbl)
   end.
 
@@ -459,7 +472,7 @@ Definition known_id (f: Cminor.function) : known_idents :=
 Definition sel_function (dm: PTree.t globdef) (hf: helper_functions) (f: Cminor.function) : res function :=
   let ki := known_id f in
   do env <- Cminortyping.type_function f;
-  do body' <- sel_stmt dm ki env f.(Cminor.fn_body);
+  do body' <- sel_stmt dm ki env f.(Cminor.fn_body) Sskip;
   OK (mkfunction
         f.(Cminor.fn_sig)
         f.(Cminor.fn_params)

backend/Selectionaux.ml

@@ -106,7 +106,7 @@ to execute instructions from the other branch in parallel with
 instructions from the first branch.
 *)
 
-let if_conversion_heuristic cond ifso ifnot ty =
+let if_conversion_heuristic cond ifso ifnot ty kont =
   if not !Clflags.option_fifconversion then false else
   if !Clflags.option_Obranchless then true else
   if not (fast_cmove ty) then false else