Merge remote-tracking branch 'origin/mppa-expect3' into mppa-work

26 files changed, 212 insertions, 128 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1f854fc3..069b9012 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -3,7 +3,7 @@ stages:
 
 check-admitted:
   stage: build
-  image: "coqorg/coq"
+  image: "coqorg/coq:8.10"
   before_script:
     - opam switch 4.07.1+flambda
     - eval `opam config env`
@@ -22,7 +22,7 @@ check-admitted:
     
 build_x86_64:
   stage: build
-  image: "coqorg/coq"
+  image: "coqorg/coq:8.10"
   before_script:
     - opam switch 4.07.1+flambda
     - eval `opam config env`
@@ -43,7 +43,7 @@ build_x86_64:
 
 build_ia32:
   stage: build
-  image: "coqorg/coq"
+  image: "coqorg/coq:8.10"
   before_script:
     - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
     - sudo apt-get -y install gcc-multilib
@@ -66,7 +66,7 @@ build_ia32:
 
 build_aarch64:
   stage: build
-  image: "coqorg/coq"
+  image: "coqorg/coq:8.10"
   before_script:
     - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
     - sudo apt-get -y install gcc-aarch64-linux-gnu qemu-user
@@ -89,7 +89,7 @@ build_aarch64:
 
 build_arm:
   stage: build
-  image: "coqorg/coq"
+  image: "coqorg/coq:8.10"
   before_script:
     - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
     - sudo apt-get -y install gcc-arm-linux-gnueabi qemu-user
@@ -113,7 +113,7 @@ build_arm:
 
 build_armhf:
   stage: build
-  image: "coqorg/coq"
+  image: "coqorg/coq:8.10"
   before_script:
     - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
     - sudo apt-get -y install gcc-arm-linux-gnueabihf qemu-user
@@ -136,7 +136,7 @@ build_armhf:
 
 build_ppc:
   stage: build
-  image: "coqorg/coq"
+  image: "coqorg/coq:8.10"
   before_script:
     - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
     - sudo apt-get -y install gcc-powerpc-linux-gnu qemu-user
@@ -157,7 +157,7 @@ build_ppc:
 
 build_ppc64:
   stage: build
-  image: "coqorg/coq"
+  image: "coqorg/coq:8.10"
   before_script:
     - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
     - sudo apt-get -y install gcc-powerpc64-linux-gnu
@@ -178,7 +178,7 @@ build_ppc64:
 
 build_rv64:
   stage: build
-  image: "coqorg/coq"
+  image: "coqorg/coq:8.10"
   before_script:
     - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
     - sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user
@@ -201,7 +201,7 @@ build_rv64:
 
 build_rv32:
   stage: build
-  image: "coqorg/coq"
+  image: "coqorg/coq:8.10"
   before_script:
     - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
     - sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user
@@ -222,7 +222,7 @@ build_rv32:
 
 build_k1c:
   stage: build
-  image: "coqorg/coq"
+  image: "coqorg/coq:8.10"
   before_script:
     - opam switch 4.07.1+flambda
     - eval `opam config env`
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 91a4c104..dcebbb86 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -77,6 +77,7 @@ Inductive unary_operation : Type :=
   | Osingleoflongu: unary_operation.       (**r unsigned long to float32 *)
 
 Inductive binary_operation : Type :=
+  | Oexpect: typ -> binary_operation       (**r first value, second is expected*)
   | Oadd: binary_operation                 (**r integer addition *)
   | Osub: binary_operation                 (**r integer subtraction *)
   | Omul: binary_operation                 (**r integer multiplication *)
@@ -301,6 +302,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
 Definition eval_binop
             (op: binary_operation) (arg1 arg2: val) (m: mem): option val :=
   match op with
+  | Oexpect ty => Some (Val.normalize arg1 ty)
   | Oadd => Some (Val.add arg1 arg2)
   | Osub => Some (Val.sub arg1 arg2)
   | Omul => Some (Val.mul arg1 arg2)
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 96cb8ae6..26f47e23 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -50,7 +50,7 @@ with exprlist : Type :=
   | Econs: expr -> exprlist -> exprlist
 
 with condexpr : Type :=
-  | CEcond : condition -> exprlist -> condexpr
+  | CEcond : condition -> option bool -> exprlist -> condexpr
   | CEcondition : condexpr -> condexpr -> condexpr -> condexpr
   | CElet: expr -> condexpr -> condexpr.
 
@@ -207,10 +207,10 @@ with eval_exprlist: letenv -> exprlist -> list val -> Prop :=
       eval_exprlist le (Econs a1 al) (v1 :: vl)
 
 with eval_condexpr: letenv -> condexpr -> bool -> Prop :=
-  | eval_CEcond: forall le cond al vl vb,
+  | eval_CEcond: forall le cond expected al vl vb,
       eval_exprlist le al vl ->
       eval_condition cond vl m = Some vb ->
-      eval_condexpr le (CEcond cond al) vb
+      eval_condexpr le (CEcond cond expected al) vb
   | eval_CEcondition: forall le a b c va v,
       eval_condexpr le a va ->
       eval_condexpr le (if va then b else c) v ->
@@ -495,7 +495,7 @@ with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist :=
 
 with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr :=
   match a with
-  | CEcond c al => CEcond c (lift_exprlist p al)
+  | CEcond c expected al => CEcond c expected (lift_exprlist p al)
   | CEcondition a b c => CEcondition (lift_condexpr p a) (lift_condexpr p b) (lift_condexpr p c)
   | CElet a b => CElet (lift_expr p a) (lift_condexpr (S p) b)
   end.
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v
index 92ec45f2..8945cecf 100644
--- a/backend/Cminortyping.v
+++ b/backend/Cminortyping.v
@@ -64,6 +64,7 @@ Definition type_binop (op: binary_operation) : typ * typ * typ :=
   | Ocmpf _ => (Tfloat, Tfloat, Tint)
   | Ocmpfs _ => (Tsingle, Tsingle, Tint)
   | Ocmpl _ | Ocmplu _ => (Tlong, Tlong, Tint)
+  | Oexpect ty => (ty, ty, ty)
   end.
 
 Module RTLtypes <: TYPE_ALGEBRA.
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index c9a6d399..051225a4 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -34,6 +34,7 @@ let precedence = function
   | Ebinop((Oadd|Osub|Oaddf|Osubf|Oaddfs|Osubfs|Oaddl|Osubl), _, _) -> (12, LtoR)
   | Ebinop((Oshl|Oshr|Oshru|Oshll|Oshrl|Oshrlu), _, _) -> (11, LtoR)
   | Ebinop((Ocmp _|Ocmpu _|Ocmpf _|Ocmpfs _|Ocmpl _|Ocmplu _), _, _) -> (10, LtoR)
+  | Ebinop((Oexpect _), _, _) -> (9, LtoR)
   | Ebinop((Oand|Oandl), _, _) -> (8, LtoR)
   | Ebinop((Oxor|Oxorl), _, _) -> (7, LtoR)
   | Ebinop((Oor|Oorl), _, _) -> (6, LtoR)
@@ -89,6 +90,7 @@ let comparison_name = function
   | Cge -> ">="
 
 let name_of_binop = function
+  | Oexpect _ -> "expect"
   | Oadd -> "+"
   | Osub -> "-"
   | Omul -> "*"
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index ac98f3a1..243d7b7c 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -477,9 +477,9 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node)
 with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node)
                      {struct a} : mon node :=
   match a with
-  | CEcond c al =>
+  | CEcond c expected al =>
       do rl <- alloc_regs map al;
-      do nt <- add_instr (Icond c rl ntrue nfalse None);
+      do nt <- add_instr (Icond c rl ntrue nfalse expected);
          transl_exprlist map al rl nt
   | CEcondition a b c =>
       do nc <- transl_condexpr map c ntrue nfalse;
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index e39d3b56..26688e23 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -41,7 +41,7 @@ and size_exprs = function
   | Econs(e1, el) -> size_expr e1 + size_exprs el
 
 and size_condexpr = function
-  | CEcond(c, args) -> size_exprs args
+  | CEcond(c, expected, args) -> size_exprs args
   | CEcondition(c1, c2, c3) ->
       1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3
   | CElet(a, c) ->
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index b94ec22f..e62aff22 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -799,11 +799,11 @@ Proof.
 Qed.
 
 Lemma transl_condexpr_CEcond_correct:
-  forall le cond al vl vb,
+  forall le cond expected al vl vb,
   eval_exprlist ge sp e m le al vl ->
   transl_exprlist_prop le al vl ->
   eval_condition cond vl m = Some vb ->
-  transl_condexpr_prop le (CEcond cond al) vb.
+  transl_condexpr_prop le (CEcond cond expected al) vb.
 Proof.
   intros; red; intros. inv TE.
   exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]].
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 30ad7d82..36b8409d 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -744,10 +744,10 @@ 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 i,
+  | tr_CEcond: forall map pr cond expected bl ns ntrue nfalse n1 rl i,
       tr_exprlist c map pr bl ns n1 rl ->
       c!n1 = Some (Icond cond rl ntrue nfalse i) ->
-      tr_condition c map pr (CEcond cond bl) ns ntrue nfalse
+      tr_condition c map pr (CEcond cond expected 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 ->
       tr_condition c map pr a2 n2 ntrue nfalse ->
diff --git a/backend/Selection.v b/backend/Selection.v
index 4ab3331e..342bd8ca 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -35,12 +35,13 @@ Local Open Scope error_monad_scope.
 
 (** Conversion of conditions *)
 
-Function condexpr_of_expr (e: expr) : condexpr :=
+Function condexpr_of_expr (e: expr) (expected : option bool) : condexpr :=
   match e with
-  | Eop (Ocmp c) el => CEcond c el
-  | Econdition a b c => CEcondition a (condexpr_of_expr b) (condexpr_of_expr c)
-  | Elet a b => CElet a (condexpr_of_expr b)
-  | _ => CEcond (Ccompuimm Cne Int.zero) (e ::: Enil)
+  | Eop (Ocmp c) el => CEcond c expected el
+  | Econdition a b c => CEcondition a (condexpr_of_expr b expected)
+                                      (condexpr_of_expr c expected)
+  | Elet a b => CElet a (condexpr_of_expr b expected)
+  | _ => CEcond (Ccompuimm Cne Int.zero) expected (e ::: Enil)
   end.
 
 Function condition_of_expr (e: expr) : condition * exprlist :=
@@ -120,6 +121,7 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
 
 Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   match op with
+  | Cminor.Oexpect ty => arg1
   | Cminor.Oadd => add arg1 arg2
   | Cminor.Osub => sub arg1 arg2
   | Cminor.Omul => mul arg1 arg2
@@ -166,7 +168,7 @@ Definition sel_select (ty: typ) (cnd ifso ifnot: expr) : expr :=
    let (cond, args) := condition_of_expr cnd in
    match SelectOp.select ty cond args ifso ifnot with
    | Some a => a
-   | None => Econdition (condexpr_of_expr cnd) ifso ifnot
+   | None => Econdition (condexpr_of_expr cnd None) ifso ifnot
    end.
 
 (** Conversion from Cminor expression to Cminorsel expressions *)
@@ -243,7 +245,8 @@ Definition sel_builtin_res (optid: option ident) : builtin_res ident :=
 Function sel_known_builtin (bf: builtin_function) (args: exprlist) :=
   match bf, args with
   | BI_platform b, _ =>
-      SelectOp.platform_builtin b args
+    SelectOp.platform_builtin b args
+(*  | BI_standard BI_expect, a1 ::: a2 ::: Enil => Some a1 *)
   | BI_standard (BI_select ty), a1 ::: a2 ::: a3 ::: Enil =>
       Some (sel_select ty a1 a2 a3)
   | BI_standard BI_fabs, a1 ::: Enil =>
@@ -291,16 +294,16 @@ Fixpoint sel_switch (arg: nat) (t: comptree): exitexpr :=
   | CTaction act =>
       XEexit act
   | CTifeq key act t' =>
-      XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key))
+      XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key) None)
                   (XEexit act)
                   (sel_switch arg t')
   | CTiflt key t1 t2 =>
-      XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key))
+      XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key) None)
                   (sel_switch arg t1)
                   (sel_switch arg t2)
   | CTjumptable ofs sz tbl t' =>
       XElet (make_sub (Eletvar arg) ofs)
-        (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz))
+        (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz) None)
                      (XEjumptable (make_to_int (Eletvar O)) tbl)
                      (sel_switch (S arg) t'))
   end.
@@ -375,6 +378,22 @@ Definition if_conversion
   | _, _ => None
   end.
 
+Definition extract_expect1 (e : Cminor.expr) : option bool :=
+  match e with
+  | Cminor.Ebinop (Cminor.Oexpect ty) e1 (Cminor.Econst (Cminor.Ointconst c)) =>
+    Some (if Int.eq_dec c Int.zero then false else true)
+  | Cminor.Ebinop (Cminor.Oexpect ty) e1 (Cminor.Econst (Cminor.Olongconst c)) =>
+    Some (if Int64.eq_dec c Int64.zero then false else true)
+  | _ => None
+  end.
+
+Definition extract_expect (e : Cminor.expr) : option bool :=
+  match e with
+  | Cminor.Ebinop (Cminor.Ocmpu Cne) e1 (Cminor.Econst (Cminor.Ointconst c)) =>
+    if Int.eq_dec c Int.zero then extract_expect1 e1 else None
+  | _ => extract_expect1 e
+  end.
+
 (** Conversion from Cminor statements to Cminorsel statements. *)
 
 Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt :=
@@ -402,8 +421,10 @@ Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt :
       match if_conversion ki env e ifso ifnot with
       | Some s => OK s
       | None =>
-          do ifso' <- sel_stmt ki env ifso; do ifnot' <- sel_stmt ki env ifnot;
-          OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot')
+        do ifso' <- sel_stmt ki env ifso;
+        do ifnot' <- sel_stmt ki env ifnot;
+        OK (Sifthenelse (condexpr_of_expr (sel_expr e)
+                          (extract_expect e)) ifso' ifnot')
       end
   | Cminor.Sloop body =>
       do body' <- sel_stmt ki env body; OK (Sloop body')
diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml
index 26a79fd7..5a8bde8c 100644
--- a/backend/Selectionaux.ml
+++ b/backend/Selectionaux.ml
@@ -39,6 +39,7 @@ let cost_unop = function
   | Osingleoflong | Osingleoflongu -> assert false
 
 let cost_binop = function
+  | Oexpect _ -> 0
   | Oadd  | Osub -> 1
   | Omul -> 2
   | Odiv  | Odivu | Omod  | Omodu -> assert false
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index aa53c9cb..955c45a4 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -196,12 +196,12 @@ Variable e: env.
 Variable m: mem.
 
 Lemma eval_condexpr_of_expr:
-  forall a le v b,
+  forall expected a le v b,
   eval_expr tge sp e m le a v ->
   Val.bool_of_val v b ->
-  eval_condexpr tge sp e m le (condexpr_of_expr a) b.
+  eval_condexpr tge sp e m le (condexpr_of_expr a expected) b.
 Proof.
-  intros until a. functional induction (condexpr_of_expr a); intros.
+  intros until a. functional induction (condexpr_of_expr a expected); intros.
 (* compare *)
   inv H. econstructor; eauto.
   simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto.
@@ -310,46 +310,47 @@ Lemma eval_sel_binop:
   exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
-  apply eval_add; auto.
-  apply eval_sub; auto.
-  apply eval_mul; auto.
-  eapply eval_divs; eauto.
-  eapply eval_divu; eauto.
-  eapply eval_mods; eauto.
-  eapply eval_modu; eauto.
-  apply eval_and; auto.
-  apply eval_or; auto.
-  apply eval_xor; auto.
-  apply eval_shl; auto.
-  apply eval_shr; auto.
-  apply eval_shru; auto.
-  apply eval_addf; auto.
-  apply eval_subf; auto.
-  apply eval_mulf; auto.
-  apply eval_divf; auto.
-  apply eval_addfs; auto.
-  apply eval_subfs; auto.
-  apply eval_mulfs; auto.
-  apply eval_divfs; auto.
-  eapply eval_addl; eauto.
-  eapply eval_subl; eauto.
-  eapply eval_mull; eauto.
-  eapply eval_divls; eauto.
-  eapply eval_divlu; eauto.
-  eapply eval_modls; eauto.
-  eapply eval_modlu; eauto.
-  eapply eval_andl; eauto.
-  eapply eval_orl; eauto.
-  eapply eval_xorl; eauto.
-  eapply eval_shll; eauto.
-  eapply eval_shrl; eauto.
-  eapply eval_shrlu; eauto.
-  apply eval_comp; auto.
-  apply eval_compu; auto.
-  apply eval_compf; auto.
-  apply eval_compfs; auto.
-  exists v; split; auto. eapply eval_cmpl; eauto.
-  exists v; split; auto. eapply eval_cmplu; eauto.
+  - exists v1; split; trivial. apply Val.lessdef_normalize.
+  - apply eval_add; auto.
+  - apply eval_sub; auto.
+  - apply eval_mul; auto.
+  - eapply eval_divs; eauto.
+  - eapply eval_divu; eauto.
+  - eapply eval_mods; eauto.
+  - eapply eval_modu; eauto.
+  - apply eval_and; auto.
+  - apply eval_or; auto.
+  - apply eval_xor; auto.
+  - apply eval_shl; auto.
+  - apply eval_shr; auto.
+  - apply eval_shru; auto.
+  - apply eval_addf; auto.
+  - apply eval_subf; auto.
+  - apply eval_mulf; auto.
+  - apply eval_divf; auto.
+  - apply eval_addfs; auto.
+  - apply eval_subfs; auto.
+  - apply eval_mulfs; auto.
+  - apply eval_divfs; auto.
+  - eapply eval_addl; eauto.
+  - eapply eval_subl; eauto.
+  - eapply eval_mull; eauto.
+  - eapply eval_divls; eauto.
+  - eapply eval_divlu; eauto.
+  - eapply eval_modls; eauto.
+  - eapply eval_modlu; eauto.
+  - eapply eval_andl; eauto.
+  - eapply eval_orl; eauto.
+  - eapply eval_xorl; eauto.
+  - eapply eval_shll; eauto.
+  - eapply eval_shrl; eauto.
+  - eapply eval_shrlu; eauto.
+  - apply eval_comp; auto.
+  - apply eval_compu; auto.
+  - apply eval_compf; auto.
+  - apply eval_compfs; auto.
+  - exists v; split; auto. eapply eval_cmpl; eauto.
+  - exists v; split; auto. eapply eval_cmplu; eauto.
 Qed.
 
 Lemma eval_sel_select:
@@ -395,6 +396,13 @@ Proof.
   inv ARGS; try discriminate. inv H0; try discriminate.
   inv SEL.  
   simpl in SEM; inv SEM. apply eval_absf; auto.
+  (* + (* expect *)
+  inv ARGS; try discriminate.
+  inv H0; try discriminate.
+  inv H2; try discriminate.
+  simpl in SEM. inv SEM. inv SEL.
+  destruct v1; destruct v0.
+  all: econstructor; split; eauto. *)
 - eapply eval_platform_builtin; eauto.
 Qed.
 
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp
index dfe42df0..0f240602 100644
--- a/backend/SplitLong.vp
+++ b/backend/SplitLong.vp
@@ -10,6 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+(* FIXME: expected branching information not propagated *)
 (** Instruction selection for 64-bit integer operations *)
 
 Require String.
@@ -256,7 +257,7 @@ Definition cmpl_ne_zero (e: expr) :=
 
 Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) :=
   splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
-    Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil))
+    Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil))
                (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil))
                (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))).
 
@@ -278,7 +279,7 @@ Definition cmplu (c: comparison) (e1 e2: expr) :=
 
 Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) :=
   splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
-    Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil))
+    Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil))
                (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil))
                (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))).
 
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index f637b5e4..75f5eb3e 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -181,9 +181,10 @@ let ais_annot_functions =
 let builtins_generic = {
   builtin_typedefs = [];
   builtin_functions =
-    ais_annot_functions
-      @
+    ais_annot_functions @
     [
+    "__builtin_expect",
+    (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false);
     (* Integer arithmetic *)
     "__builtin_bswap64",
     (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
@@ -912,6 +913,14 @@ let rec convertExpr env e =
   | C.ECompound(ty1, ie) ->
       unsupported "compound literals"; ezero
 
+  | C.ECall({edesc = C.EVar {name = "__builtin_expect"}}, args) ->
+     (match args with
+      | [e1; e2] ->
+         ewrap (Ctyping.ebinop Cop.Oexpect (convertExpr env e1) (convertExpr env e2))
+      | _ -> 
+       error "__builtin_expect wants two arguments";
+       ezero)
+
   | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) when List.length args < 2 ->
       error "too few arguments to function call, expected at least 2, have 0";
       ezero
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 5acb996d..744df818 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1335,6 +1335,7 @@ Lemma eval_binop_compat:
   /\ Val.inject f v tv.
 Proof.
   destruct op; simpl; intros; inv H.
+- TrivialExists. apply Val.normalize_inject; auto.
 - TrivialExists. apply Val.add_inject; auto.
 - TrivialExists. apply Val.sub_inject; auto.
 - TrivialExists. inv H0; inv H1; constructor.
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 143e87a3..47a02851 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -33,6 +33,7 @@ Inductive unary_operation : Type :=
   | Oabsfloat : unary_operation.        (**r floating-point absolute value *)
 
 Inductive binary_operation : Type :=
+  | Oexpect : binary_operation          (**r return first argument *)
   | Oadd : binary_operation             (**r addition (binary [+]) *)
   | Osub : binary_operation             (**r subtraction (binary [-]) *)
   | Omul : binary_operation             (**r multiplication (binary [*]) *)
@@ -763,6 +764,14 @@ Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :
     (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2)))
     v1 t1 v2 t2 m.
 
+Definition sem_expect (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
+  sem_binarith
+    (fun sg n1 n2 => Some(Vint n1))
+    (fun sg n1 n2 => Some(Vlong n1))
+    (fun n1 n2 => Some(Vfloat n1))
+    (fun n1 n2 => Some(Vsingle n1))
+    v1 t1 v2 t2 m.
+
 Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 =>
@@ -1050,6 +1059,7 @@ Definition sem_binary_operation
     (v1: val) (t1: type) (v2: val) (t2:type)
     (m: mem): option val :=
   match op with
+  | Oexpect => sem_expect v1 t1 v2 t2 m
   | Oadd => sem_add cenv v1 t1 v2 t2 m
   | Osub => sem_sub cenv v1 t1 v2 t2 m
   | Omul => sem_mul v1 t1 v2 t2 m
@@ -1290,6 +1300,9 @@ Lemma sem_binary_operation_inj:
   exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv.
 Proof.
   unfold sem_binary_operation; intros; destruct op.
+- (* expect *)
+  unfold sem_expect in *.
+  eapply sem_binarith_inject; eauto; intros; exact I.
 - (* add *)
   assert (A: forall cenv ty si v1' v2' tv1' tv2',
              Val.inject f v1' tv1' -> Val.inject f v2' tv2' ->
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 5bd12d00..f78b52ae 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -259,6 +259,11 @@ Definition make_add_ptr_long (ce: composite_env) (ty: type) (e1 e2: expr) :=
     let n := make_intconst (Int.repr sz) in
     OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))).
 
+Definition make_expect (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  make_binarith (Oexpect AST.Tint) (Oexpect AST.Tint)
+                (Oexpect AST.Tfloat) (Oexpect AST.Tsingle)
+                (Oexpect AST.Tlong) (Oexpect AST.Tlong) e1 ty1 e2 ty2.
+
 Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_add ty1 ty2 with
   | add_case_pi ty si => make_add_ptr_int ce ty si e1 e2
@@ -421,6 +426,7 @@ Definition transl_binop (ce: composite_env)
                         (a: expr) (ta: type)
                         (b: expr) (tb: type) : res expr :=
   match op with
+  | Cop.Oexpect => make_expect a ta b tb
   | Cop.Oadd => make_add ce a ta b tb
   | Cop.Osub => make_sub ce a ta b tb
   | Cop.Omul => make_mul a ta b tb
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 1ceb8e4d..c5ba19d5 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -619,6 +619,11 @@ End MAKE_BIN.
 
 Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm.
 
+Lemma make_expect_correct: binary_constructor_correct make_expect sem_expect.
+Proof.
+  apply make_binarith_correct; intros; auto.
+Qed.
+
 Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)).
 Proof.
   assert (A: forall ty si a b c e le m va vb v,
@@ -922,22 +927,23 @@ Lemma transl_binop_correct:
   eval_expr ge e le m c v.
 Proof.
   intros. destruct op; simpl in *.
-  eapply make_add_correct; eauto.
-  eapply make_sub_correct; eauto.
-  eapply make_mul_correct; eauto.
-  eapply make_div_correct; eauto.
-  eapply make_mod_correct; eauto.
-  eapply make_and_correct; eauto.
-  eapply make_or_correct; eauto.
-  eapply make_xor_correct; eauto.
-  eapply make_shl_correct; eauto.
-  eapply make_shr_correct; eauto.
-  eapply make_cmp_correct; eauto.
-  eapply make_cmp_correct; eauto.
-  eapply make_cmp_correct; eauto.
-  eapply make_cmp_correct; eauto.
-  eapply make_cmp_correct; eauto.
-  eapply make_cmp_correct; eauto.
+- eapply make_expect_correct; eauto.
+- eapply make_add_correct; eauto.
+- eapply make_sub_correct; eauto.
+- eapply make_mul_correct; eauto.
+- eapply make_div_correct; eauto.
+- eapply make_mod_correct; eauto.
+- eapply make_and_correct; eauto.
+- eapply make_or_correct; eauto.
+- eapply make_xor_correct; eauto.
+- eapply make_shl_correct; eauto.
+- eapply make_shr_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
 Qed.
 
 Lemma make_load_correct:
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 00fcf8ab..bde4001f 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -111,6 +111,7 @@ Definition comparison_type (ty1 ty2: type) (m: string): res type :=
 
 Definition type_binop (op: binary_operation) (ty1 ty2: type) : res type :=
   match op with
+  | Oexpect => binarith_type ty1 ty2 "__builtin_expect"
   | Oadd =>
       match classify_add ty1 ty2 with
       | add_case_pi ty _ | add_case_ip _ ty
@@ -1546,6 +1547,8 @@ Lemma pres_sem_binop:
 Proof.
   intros until m; intros TY SEM WT1 WT2.
   destruct op; simpl in TY; simpl in SEM.
+- (* expect *)
+  unfold sem_expect in SEM. eapply pres_sem_binarith; eauto; intros; exact I.    
 - (* add *)
   unfold sem_add, sem_add_ptr_int, sem_add_ptr_long in SEM; DestructCases; auto with ty.
   eapply pres_sem_binarith; eauto; intros; exact I.
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 0e735d2d..0aefde31 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -62,6 +62,7 @@ let precedence = function
   | Ebinop(Oand, _, _, _) -> (8, LtoR)
   | Ebinop(Oxor, _, _, _) -> (7, LtoR)
   | Ebinop(Oor, _, _, _) -> (6, LtoR)
+  | Ebinop(Oexpect, _, _, _) -> (5, LtoR)
 
 (* Expressions *)
 
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 03dc5837..beca056f 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -30,6 +30,7 @@ let name_unop = function
   | Oabsfloat -> "__builtin_fabs"
 
 let name_binop = function
+  | Oexpect -> "expect"
   | Oadd -> "+"
   | Osub -> "-"
   | Omul -> "*"
@@ -158,6 +159,7 @@ let rec precedence = function
   | Ebinop(Oand, _, _, _) -> (8, LtoR)
   | Ebinop(Oxor, _, _, _) -> (7, LtoR)
   | Ebinop(Oor, _, _, _) -> (6, LtoR)
+  | Ebinop(Oexpect, _, _, _) -> (5, LtoR) (* fixme *)
   | Eseqand _ -> (5, LtoR)
   | Eseqor _ -> (4, LtoR)
   | Econdition _ -> (3, RtoL)
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index e7d57a1c..95e3957c 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -770,53 +770,53 @@ Proof.
 (* val *)
   simpl in H. destruct v; monadInv H; exists (@nil ident); split; auto with gensym.
 Opaque makeif.
-  intros. destruct dst; simpl in *; inv H2.
+- intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-  intros. destruct dst; simpl in *; inv H2.
+- intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-  intros. destruct dst; simpl in *; inv H2.
+- intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-  intros. destruct dst; simpl in *; inv H2.
+- intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
 (* var *)
-  monadInv H; econstructor; split; auto with gensym. UseFinish. constructor.
+- monadInv H; econstructor; split; auto with gensym. UseFinish. constructor.
 (* field *)
-  monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish.
+- monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
 (* valof *)
-  monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. UseFinish.
   exists (tmp1 ++ tmp2); split.
   intros; apply tr_expr_add_dest. econstructor; eauto with gensym.
   eauto with gensym.
 (* deref *)
-  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
+- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
 (* addrof *)
-  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
+- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. econstructor; eauto.
 (* unop *)
-  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
+- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
 (* binop *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]]. UseFinish.
   exists (tmp1 ++ tmp2); split.
   intros; apply tr_expr_add_dest. econstructor; eauto with gensym.
   eauto with gensym.
 (* cast *)
-  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
+- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
 (* seqand *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
   (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
@@ -840,7 +840,7 @@ Opaque makeif.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_app; eauto with gensym.
 (* seqor *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
   (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
@@ -864,7 +864,7 @@ Opaque makeif.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_app; eauto with gensym.
 (* condition *)
-  monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
   (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
@@ -896,13 +896,13 @@ Opaque makeif.
   apply contained_app; eauto with gensym.
   apply contained_app; eauto with gensym.
 (* sizeof *)
-  monadInv H. UseFinish.
+- monadInv H. UseFinish.
   exists (@nil ident); split; auto with gensym. constructor.
 (* alignof *)
-  monadInv H. UseFinish.
+- monadInv H. UseFinish.
   exists (@nil ident); split; auto with gensym. constructor.
 (* assign *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   destruct dst; monadInv EQ2; simpl add_dest in *.
   (* for value *)
@@ -921,7 +921,7 @@ Opaque makeif.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
 (* assignop *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]].
   destruct dst; monadInv EQ3; simpl add_dest in *.
@@ -941,7 +941,7 @@ Opaque makeif.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
 (* postincr *)
-  monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0; simpl add_dest in *.
   (* for value *)
   exists (x0 :: tmp1); split.
@@ -958,7 +958,7 @@ Opaque makeif.
   econstructor; eauto with gensym.
   apply contained_cons; eauto with gensym.
 (* comma *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
@@ -968,7 +968,7 @@ Opaque makeif.
   destruct dst; simpl; auto with gensym.
   apply contained_app; eauto with gensym.
 (* call *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   destruct dst; monadInv EQ2; simpl add_dest in *.
   (* for value *)
@@ -986,7 +986,7 @@ Opaque makeif.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
 (* builtin *)
-  monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0; simpl add_dest in *.
   (* for value *)
   exists (x0 :: tmp1); split.
@@ -1001,13 +1001,13 @@ Opaque makeif.
   repeat rewrite app_ass. econstructor; eauto with gensym. congruence.
   apply contained_cons; eauto with gensym.
 (* loc *)
-  monadInv H.
+- monadInv H.
 (* paren *)
-  monadInv H0.
+- monadInv H0.
 (* nil *)
-  monadInv H; exists (@nil ident); split; auto with gensym. constructor.
+- monadInv H; exists (@nil ident); split; auto with gensym. constructor.
 (* cons *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 50b1bdd6..52f4f855 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -472,7 +472,7 @@ Definition intuoffloat (e: expr) :=
   else
     Elet e
     (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
-      (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
+      (Econdition (CEcond (Ccompf Clt) None (Eletvar 1 ::: Eletvar 0 ::: Enil))
         (intoffloat (Eletvar 1))
         (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
 
diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_k1c_fixes.h
index 69097d06..7f111742 100644
--- a/runtime/include/ccomp_k1c_fixes.h
+++ b/runtime/include/ccomp_k1c_fixes.h
@@ -25,6 +25,6 @@ extern long long __compcert_afaddd(void *address, unsigned long long incr);
 extern int __compcert_afaddw(void *address, unsigned int incr);
 #endif
 
-#define __builtin_expect(x, y) (x)
+/* #define __builtin_expect(x, y) (x) */
 #define __builtin_ctz(x) __builtin_k1_ctzw(x)
 #define __builtin_clz(x) __builtin_k1_clzw(x)
diff --git a/test/monniaux/expect/expect.c b/test/monniaux/expect/expect.c
new file mode 100644
index 00000000..30e0742a
--- /dev/null
+++ b/test/monniaux/expect/expect.c
@@ -0,0 +1,7 @@
+#ifndef PREDICTED
+#define PREDICTED 0
+#endif
+
+int expect(int x, int *y, int *z) {
+  return __builtin_expect(x, PREDICTED) ? *y : *z;
+}
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index a23c37d5..2a09207b 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -503,7 +503,7 @@ Definition intuoffloat (e: expr) :=
   if Archi.splitlong then
     Elet e
       (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
-        (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
+        (Econdition (CEcond (Ccompf Clt) None (Eletvar 1 ::: Eletvar 0 ::: Enil))
           (intoffloat (Eletvar 1))
           (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat
   else
@@ -516,7 +516,7 @@ Nondetfunction floatofintu (e: expr) :=
     if Archi.splitlong then
       let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in
       Elet e
-        (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
+        (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) None (Eletvar O ::: Enil))
           (floatofint (Eletvar O))
           (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f))
     else