1 files changed, 129 insertions, 0 deletions
diff --git a/backend/Ifconv.v b/backend/Ifconv.v
new file mode 100644
index 00000000..0c9c5b5c
--- /dev/null
+++ b/backend/Ifconv.v
@@ -0,0 +1,129 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, Collège de France and Inria Paris            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import Coqlib Maps Errors.
+Require Import AST Events Cminor.
+Require Import Cminortyping.
+
+Definition tyenv := ident -> typ.
+Definition known_idents := PTree.t unit.
+
+Definition is_known (ki: known_idents) (id: ident) :=
+  match ki!id with Some _ => true | None => false end.
+
+Definition safe_unop (op: unary_operation) : bool :=
+  match op with
+  | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => false
+  | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => false
+  | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => false
+  | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => false
+  | _ => true
+  end.
+
+Definition safe_binop (op: binary_operation) : bool :=
+  match op with
+  | Odiv | Odivu | Omod | Omodu => false
+  | Odivl | Odivlu | Omodl | Omodlu => false
+  | Ocmpl _ | Ocmplu _ => false
+  | _ => true
+  end.
+
+Fixpoint safe_expr (ki: known_idents) (a: expr) : bool :=
+  match a with
+  | Evar v => is_known ki v
+  | Econst c => true
+  | Eunop op e1 => safe_unop op && safe_expr ki e1
+  | Ebinop op e1 e2 => safe_binop op && safe_expr ki e1 && safe_expr ki e2
+  | Eload chunk e => false
+  end.
+
+Definition Sselection (id: ident) (ty: typ) (cond ifso ifnot: expr) : stmt :=
+  Sbuiltin (Some id) (EF_select ty) (cond :: ifso :: ifnot :: nil).
+
+Inductive stmt_class : Type :=
+  | SCskip
+  | SCassign (id: ident) (a: expr)
+  | SCother.
+
+Function classify_stmt (s: stmt) : stmt_class :=
+  match s with
+  | Sskip => SCskip
+  | Sassign id a => SCassign id a
+  | Sseq Sskip s => classify_stmt s
+  | Sseq s Sskip => classify_stmt s
+  | _ => SCother
+  end.
+
+Definition if_conversion_base
+      (ki: known_idents) (env: tyenv)
+      (cond: expr) (id: ident) (ifso ifnot: expr) : option stmt :=
+  if is_known ki id && safe_expr ki ifso && safe_expr ki ifnot
+  then Some (Sselection id (env id) cond ifso ifnot)
+  else None.
+
+Definition if_conversion
+      (ki: known_idents) (env: tyenv)
+      (cond: expr) (ifso ifnot: stmt) : option stmt :=
+  match classify_stmt ifso, classify_stmt ifnot with
+  | SCskip, SCassign id a =>
+      if_conversion_base ki env cond id (Evar id) a
+  | SCassign id a, SCskip =>
+      if_conversion_base ki env cond id a (Evar id)
+  | SCassign id1 a1, SCassign id2 a2 =>
+      if ident_eq id1 id2 then if_conversion_base ki env cond id1 a1 a2 else None
+  | _, _ => None
+  end.
+
+Fixpoint transf_stmt (ki: known_idents) (env: tyenv) (s: stmt) : stmt :=
+  match s with
+  | Sskip => s
+  | Sassign _ _ => s
+  | Sstore _ _ _ => s
+  | Scall _ _ _ _ => s
+  | Stailcall _ _ _ => s
+  | Sbuiltin _ _ _ => s
+  | Sseq s1 s2 => Sseq (transf_stmt ki env s1) (transf_stmt ki env s2)
+  | Sifthenelse e s1 s2 =>
+      match if_conversion ki env e s1 s2 with
+      | Some s => s
+      | None => Sifthenelse e (transf_stmt ki env s1) (transf_stmt ki env s2)
+      end
+  | Sloop s1 => Sloop (transf_stmt ki env s1)
+  | Sblock s1 => Sblock (transf_stmt ki env s1)
+  | Sexit _ => s
+  | Sswitch _ _ _ _ => s
+  | Sreturn _ => s
+  | Slabel lbl s1 => Slabel lbl (transf_stmt ki env s1)
+  | Sgoto _ => s
+  end.
+
+Definition known_id (f: function) : known_idents :=
+  let add (ki: known_idents) (id: ident) := PTree.set id tt ki in
+  List.fold_left add f.(fn_vars)
+      (List.fold_left add f.(fn_params) (PTree.empty unit)).
+
+Local Open Scope error_monad_scope.
+
+Definition transf_function (f: function) : res function :=
+  let ki := known_id f in
+  do env <- type_function f;
+  OK (mkfunction f.(fn_sig) f.(fn_params) f.(fn_vars) f.(fn_stackspace)
+                 (transf_stmt ki env f.(fn_body))).
+
+Definition transf_fundef (fd: fundef) : res fundef :=
+  transf_partial_fundef transf_function fd.
+
+Definition transf_program (p: program) : res program :=
+  transform_partial_program transf_fundef p.