Add a built-in function for "select" (strict conditional)

The built-in is called `EF_select` and has type `(int, T, T) -> T` for
a given Cminor type T.

During instruction selection, it is turned into an `Osel` operation if
available, otherwise into an if/then/else.

12 files changed, 216 insertions, 31 deletions

diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index dfad6972..20b94c02 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -179,7 +179,8 @@ let pp_instructions pp ic =
         | EF_memcpy _
         | EF_runtime _
         | EF_vload _
-        | EF_vstore _ -> assert false
+        | EF_vstore _
+        | EF_select _ -> assert false
       end
     (* Stackframe, should not occur *)
     | Pallocframe _ -> assert false
diff --git a/backend/CSE.v b/backend/CSE.v
index 6d3f6f33..30cf5e21 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -486,7 +486,8 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
               | _ =>
                   empty_numbering
               end
-          | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ =>
+          | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _
+          | EF_debug _ _ _ | EF_select _ =>
               set_res_unknown before res
           end
       | Icond cond args ifso ifnot =>
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index a60c316b..d0d89175 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -1152,6 +1152,7 @@ Proof.
   + apply CASE2; inv H1; auto.
   + apply CASE1.
   + apply CASE2; inv H1; auto.
+  + apply CASE2; inv H1; auto.
 * apply set_res_lessdef; auto.
 
 - (* Icond *)
diff --git a/backend/Selection.v b/backend/Selection.v
index 4520cb0c..499c26a1 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -43,6 +43,12 @@ Function condexpr_of_expr (e: expr) : condexpr :=
   | _ => CEcond (Ccompuimm Cne Int.zero) (e ::: Enil)
   end.
 
+Function condition_of_expr (e: expr) : condition * exprlist :=
+  match e with
+  | Eop (Ocmp c) el => (c, el)
+  | _ => (Ccompuimm Cne Int.zero, e ::: Enil)
+  end.
+
 (** Conversion of loads and stores *)
 
 Definition load (chunk: memory_chunk) (e1: expr) :=
@@ -156,6 +162,13 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   | Cminor.Ocmplu c => cmplu c arg1 arg2
   end.
 
+Definition sel_select (ty: typ) (arg1 arg2 arg3: expr) : expr :=
+  let (cond, args) := condition_of_expr arg1 in
+  match select ty cond args arg2 arg3 with
+  | Some e => e
+  | None   => Econdition (condexpr_of_expr arg1) arg2 arg3
+  end.
+
 (** Conversion from Cminor expression to Cminorsel expressions *)
 
 Fixpoint sel_expr (a: Cminor.expr) : expr :=
@@ -221,6 +234,20 @@ Definition sel_builtin_res (optid: option ident) : builtin_res ident :=
   | Some id => BR id
   end.
 
+Definition sel_builtin_default (optid: option ident) (ef: external_function)
+                               (args: list Cminor.expr) :=
+  Sbuiltin (sel_builtin_res optid) ef
+           (sel_builtin_args args (Machregs.builtin_constraints ef)).
+
+Function sel_builtin (optid: option ident) (ef: external_function)
+                     (args: list Cminor.expr) :=
+  match ef, optid, args with
+  | EF_select ty, Some id, e1 :: e2 :: e3 :: nil =>
+      Sassign id (sel_select ty (sel_expr e1) (sel_expr e2) (sel_expr e3))
+  | _, _, _ =>
+      sel_builtin_default optid ef args
+  end.
+
 (** Conversion of Cminor [switch] statements to decision trees. *)
 
 Parameter compile_switch: Z -> nat -> table -> comptree.
@@ -278,13 +305,10 @@ Fixpoint sel_stmt (s: Cminor.stmt) : res stmt :=
       OK (match classify_call fn with
       | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args)
       | Call_imm id  => Scall optid sg (inr _ id) (sel_exprlist args)
-      | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef
-                                    (sel_builtin_args args
-                                       (Machregs.builtin_constraints ef))
+      | Call_builtin ef => sel_builtin optid ef args
       end)
   | Cminor.Sbuiltin optid ef args =>
-      OK (Sbuiltin (sel_builtin_res optid) ef
-                   (sel_builtin_args args (Machregs.builtin_constraints ef)))
+      OK (sel_builtin optid ef args)
   | Cminor.Stailcall sg fn args =>
       OK (match classify_call fn with
       | Call_imm id  => Stailcall sg (inr _ id) (sel_exprlist args)
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 621459d0..19e3e077 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -202,6 +202,25 @@ Proof.
   simpl. inv H0. auto.
 Qed.
 
+Lemma eval_condition_of_expr:
+  forall a le v b,
+  eval_expr tge sp e m le a v ->
+  Val.bool_of_val v b ->
+  let (cond, al) := condition_of_expr a in
+  exists vl,
+     eval_exprlist tge sp e m le al vl
+  /\ eval_condition cond vl m = Some b.
+Proof.
+  intros until a. functional induction (condition_of_expr a); intros.
+(* compare *)
+  inv H. simpl in H6. inv H6. apply Val.bool_of_val_of_optbool in H0.
+  exists vl; auto.
+(* default *)
+  exists (v :: nil); split.
+  econstructor. auto. constructor.
+  simpl. inv H0. auto.
+Qed.
+
 Lemma eval_load:
   forall le a v chunk v',
   eval_expr tge sp e m le a v ->
@@ -324,6 +343,28 @@ Proof.
   exists v; split; auto. eapply eval_cmplu; eauto.
 Qed.
 
+Lemma eval_sel_select:
+  forall le ty a1 a2 a3 v1 v2 v3 b,
+  eval_expr tge sp e m le a1 v1 ->
+  eval_expr tge sp e m le a2 v2 ->
+  eval_expr tge sp e m le a3 v3 ->
+  Val.bool_of_val v1 b ->
+  exists v,
+     eval_expr tge sp e m le (sel_select ty a1 a2 a3) v
+  /\ Val.lessdef (Val.normalize (if b then v2 else v3) ty) v.
+Proof.
+  unfold sel_select; intros.
+  destruct (condition_of_expr a1) as [cond args] eqn:C.
+  destruct (select ty cond args a2 a3) as [a|] eqn:SEL.
+- exploit eval_condition_of_expr. eexact H. eauto. rewrite C.  intros (vl & A & B).
+  exploit eval_select; eauto.
+- exists (if b then v2 else v3); split.
+  apply eval_Econdition with b.
+  eapply eval_condexpr_of_expr; eauto.
+  destruct b; auto.
+  apply Val.lessdef_normalize.
+Qed.
+
 End CMCONSTR.
 
 (** Recognition of calls to built-in functions *)
@@ -741,6 +782,41 @@ Proof.
   intros. destruct oid; simpl; auto. apply set_var_lessdef; auto.
 Qed.
 
+Lemma sel_builtin_correct:
+  forall optid ef al e1 m1 vl e1' m1' t v m2 f k sp,
+  env_lessdef e1 e1' -> Mem.extends m1 m1' ->
+  Cminor.eval_exprlist ge sp e1 m1 al vl ->
+  external_call ef ge vl m1 t v m2 ->
+  exists e2' m2',
+     step tge (State f (sel_builtin optid ef al) k sp e1' m1')
+            t (State f Sskip k sp e2' m2')
+  /\ env_lessdef (set_optvar optid v e1) e2'
+  /\ Mem.extends m2 m2'.
+Proof.
+  intros until al. functional induction (sel_builtin optid ef al); intros.
+- (* select *)
+  inv H2. inv H1. inv H8. inv H9.
+  exploit sel_expr_correct. eexact H6. eauto. eauto. intros (v1' & E1 & L1).
+  exploit sel_expr_correct. eexact H5. eauto. eauto. intros (v2' & E2 & L2).
+  exploit sel_expr_correct. eexact H7. eauto. eauto. intros (v3' & E3 & L3).
+  assert (Val.bool_of_val v1' b) by (inv H3; inv L1; constructor).
+  exploit eval_sel_select. eexact E1. eexact E2. eexact E3. eauto.
+  intros (v' & A & B).
+  econstructor; econstructor; split; [|split].
+  constructor. eexact A.
+  apply set_var_lessdef; auto. eapply Val.lessdef_trans; [|eexact B].
+  apply Val.normalize_lessdef. destruct b; auto.
+  auto.
+- (* default *)
+  unfold sel_builtin_default.
+  exploit sel_builtin_args_correct; eauto. intros (vl' & A & B).
+  exploit external_call_mem_extends; eauto. intros (v' & m2' & C & D & E & F).
+  econstructor; econstructor; split; [|split].
+  econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  apply sel_builtin_res_correct; eauto.
+  auto.
+Qed.
+
 End EXPRESSIONS.
 
 (** Semantic preservation for functions and statements. *)
@@ -793,29 +869,27 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
       match_states
         (Cminor.Returnstate v k m)
         (Returnstate v' k' m')
-  | match_builtin_1: forall cunit hf ef args args' optid f sp e k m al f' e' k' m'
+  | match_builtin_1: forall cunit hf ef al vl optid f sp e k m f' e' k' m'
         (LINK: linkorder cunit prog)
         (HF: helper_functions_declared cunit hf)
         (TF: sel_function (prog_defmap cunit) hf f = OK f')
         (MC: match_cont cunit hf k k')
-        (LDA: Val.lessdef_list args args')
         (LDE: env_lessdef e e')
         (ME: Mem.extends m m')
-        (EA: list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') al args'),
+        (EA: Cminor.eval_exprlist ge sp e m al vl),
       match_states
-        (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m)
-        (State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e' m')
-  | match_builtin_2: forall cunit hf v v' optid f sp e k m f' e' m' k'
+        (Cminor.Callstate (External ef) vl (Cminor.Kcall optid f sp e k) m)
+        (State f' (sel_builtin optid ef al) k' sp e' m')
+  | match_builtin_2: forall cunit hf v optid f sp e k m f' e' m' k'
         (LINK: linkorder cunit prog)
         (HF: helper_functions_declared cunit hf)
         (TF: sel_function (prog_defmap cunit) hf f = OK f')
         (MC: match_cont cunit hf k k')
-        (LDV: Val.lessdef v v')
-        (LDE: env_lessdef e e')
+        (LDE: env_lessdef (set_optvar optid v e) e')
         (ME: Mem.extends m m'),
       match_states
         (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m)
-        (State f' Sskip k' sp (set_builtin_res (sel_builtin_res optid) v' e') m').
+        (State f' Sskip k' sp e' m').
 
 Remark call_cont_commut:
   forall cunit hf k k', match_cont cunit hf k k' -> match_call_cont (Cminor.call_cont k) (call_cont k').
@@ -843,6 +917,13 @@ Proof.
   exists cunit, hf; auto.
 Qed.
 
+Remark find_label_set_builtin:
+  forall (hf: helper_functions) lbl optid ef al k,
+  find_label lbl (sel_builtin optid ef al) k = None.
+Proof.
+  intros. functional induction (sel_builtin optid ef al); reflexivity.
+Qed.
+
 Remark find_label_commut:
   forall cunit hf lbl s k s' k',
   match_cont cunit hf k k' ->
@@ -857,9 +938,9 @@ Proof.
 (* store *)
   unfold store. destruct (addressing m (sel_expr e)); simpl; auto.
 (* call *)
-  destruct (classify_call (prog_defmap cunit) e); simpl; auto.
+  destruct (classify_call (prog_defmap cunit) e); simpl; auto. rewrite find_label_set_builtin; auto.
 (* tailcall *)
-  destruct (classify_call (prog_defmap cunit) e); simpl; auto.
+  destruct (classify_call (prog_defmap cunit) e); simpl; auto. rewrite find_label_set_builtin; auto.
 (* seq *)
   exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto.
   destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ];
@@ -947,7 +1028,6 @@ Proof.
   red; intros; eapply match_cont_call with (cunit := cunit) (hf := hf); eauto.
 + (* turned into Sbuiltin *)
   intros EQ. subst fd.
-  exploit sel_builtin_args_correct; eauto. intros [vargs' [C D]].
   right; split. simpl. omega. split. auto.
   econstructor; eauto.
 - (* Stailcall *)
@@ -966,12 +1046,8 @@ Proof.
   eapply match_callstate with (cunit := cunit'); eauto.
   eapply call_cont_commut; eauto.
 - (* Sbuiltin *)
-  exploit sel_builtin_args_correct; eauto. intros [vargs' [P Q]].
-  exploit external_call_mem_extends; eauto.
-  intros [vres' [m2 [A [B [C D]]]]].
-  left; econstructor; split.
-  econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  econstructor; eauto. apply sel_builtin_res_correct; auto.
+  exploit sel_builtin_correct; eauto. intros (e2' & m2' & A & B & C).
+  left; econstructor; split. eexact A. econstructor; eauto.
 - (* Seq *)
   left; econstructor; split.
   constructor.
@@ -1051,10 +1127,9 @@ Proof.
   econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
 - (* external call turned into a Sbuiltin *)
-  exploit external_call_mem_extends; eauto.
-  intros [vres' [m2 [A [B [C D]]]]].
+  exploit sel_builtin_correct; eauto. intros (e2' & m2' & A & B & C).
   left; econstructor; split.
-  econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  eexact A.
   econstructor; eauto.
 - (* return *)
   apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC).
@@ -1064,7 +1139,6 @@ Proof.
   econstructor; eauto. destruct optid; simpl; auto. apply set_var_lessdef; auto.
 - (* return of an external call turned into a Sbuiltin *)
   right; split. simpl; omega. split. auto. econstructor; eauto.
-  apply sel_builtin_res_correct; auto.
 Qed.
 
 Lemma sel_initial_states:
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 7f5fe355..fba00b35 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -501,6 +501,14 @@ Definition do_ef_debug (kind: positive) (text: ident) (targs: list typ)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   Some(w, E0, Vundef, m).
 
+Definition do_ef_select (ty: typ)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | Vint n :: v1 :: v2 :: nil =>
+      Some(w, E0, Val.normalize (if negb (Int.eq n Int.zero) then v1 else v2) ty, m)
+  | _ => None
+  end.
+
 Definition do_external (ef: external_function):
        world -> list val -> mem -> option (world * trace * val * mem) :=
   match ef with
@@ -516,6 +524,7 @@ Definition do_external (ef: external_function):
   | EF_annot_val kind text targ => do_ef_annot_val text targ
   | EF_inline_asm text sg clob => do_inline_assembly text sg ge
   | EF_debug kind text targs => do_ef_debug kind text targs
+  | EF_select ty => do_ef_select ty
   end.
 
 Lemma do_ef_external_sound:
@@ -568,6 +577,10 @@ Proof with try congruence.
   eapply do_inline_assembly_sound; eauto.
 (* EF_debug *)
   unfold do_ef_debug. mydestr. split; constructor.
+(* EF_select *)
+  unfold do_ef_select. destruct vargs... destruct v... destruct vargs... destruct vargs... destruct vargs... mydestr.
+  split. constructor. constructor.
+  constructor.
 Qed.
 
 Lemma do_ef_external_complete:
@@ -612,6 +625,8 @@ Proof.
   eapply do_inline_assembly_complete; eauto.
 (* EF_debug *)
   inv H. inv H0. reflexivity.
+(* EF_select *)
+  inv H. inv H0. inv H1. reflexivity.
 Qed.
 
 (** * Reduction of expressions *)
diff --git a/common/AST.v b/common/AST.v
index 145f4919..5e2d46f3 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -465,10 +465,17 @@ Inductive external_function : Type :=
          used with caution, as it can invalidate the semantic
          preservation theorem.  Generated only if [-finline-asm] is
          given. *)
-  | EF_debug (kind: positive) (text: ident) (targs: list typ).
+  | EF_debug (kind: positive) (text: ident) (targs: list typ)
      (** Transport debugging information from the front-end to the generated
          assembly.  Takes zero, one or several arguments like [EF_annot].
          Unlike [EF_annot], produces no observable event. *)
+  | EF_select (ty: typ).
+     (** Conditional expression with strict semantics, also known as
+         "conditional move".
+         Takes a boolean [b] and two values [v1], [v2] of type [ty].
+         Returns [v1] if [b] is true, [v2] if [b] is false.
+         This builtin is expanded to a conditional move instruction
+         or a branchless instruction sequence when possible. *)
 
 (** The type signature of an external function. *)
 
@@ -486,6 +493,7 @@ Definition ef_sig (ef: external_function): signature :=
   | EF_annot_val kind text targ => mksignature (targ :: nil) (Some targ) cc_default
   | EF_inline_asm text sg clob => sg
   | EF_debug kind text targs => mksignature targs None cc_default
+  | EF_select ty => mksignature (Tint :: ty :: ty :: nil) (Some ty) cc_default
   end.
 
 (** Whether an external function should be inlined by the compiler. *)
@@ -504,6 +512,7 @@ Definition ef_inline (ef: external_function) : bool :=
   | EF_annot_val kind Text rg => true
   | EF_inline_asm text sg clob => true
   | EF_debug kind text targs => true
+  | EF_select ty => true
   end.
 
 (** Whether an external function must reload its arguments. *)
diff --git a/common/Events.v b/common/Events.v
index 26dd505f..238bfa60 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1377,6 +1377,59 @@ Proof.
   split. constructor. auto.
 Qed.
 
+(** ** Semantics of the [select] built-in *)
+
+Inductive extcall_select_sem (ty: typ) (ge: Senv.t):
+              list val -> mem -> trace -> val -> mem -> Prop :=
+  | extcall_select_sem_intro: forall v1 v2 v3 m b,
+      Val.bool_of_val v1 b ->
+      extcall_select_sem ty ge (v1 :: v2 :: v3 :: nil) m
+                            E0 (Val.normalize (if b then v2 else v3) ty) m.
+
+Lemma extcall_select_ok: forall ty,
+  extcall_properties (extcall_select_sem ty)
+                     (mksignature (Tint :: ty :: ty :: nil) (Some ty) cc_default).
+Proof.
+  constructor; intros.
+(* well typed *)
+- inv H. unfold proj_sig_res. simpl. apply Val.normalize_type.
+(* symbols preserved *)
+- inv H0; econstructor; eauto.
+(* valid block *)
+- inv H; auto.
+(* perms *)
+- inv H; auto.
+(* readonly *)
+- inv H. apply Mem.unchanged_on_refl.
+(* mem extends *)
+- inv H. inv H1. inv H6. inv H7. inv H8.
+  assert (Val.bool_of_val v4 b). { inv H2; inv H4; constructor. }
+  exists (Val.normalize (if b then v5 else v6) ty), m1'.
+  split. econstructor; eauto.
+  split. apply Val.normalize_lessdef. destruct b; auto.
+  auto using Mem.unchanged_on_refl.
+(* mem inject *)
+- inv H0. inv H2. inv H7. inv H8. inv H9.
+  assert (Val.bool_of_val v' b). { inv H3; inv H5; constructor. }
+  exists f, (Val.normalize (if b then v'0 else v'1) ty), m1'.
+  split. econstructor; eauto.
+  split. apply Val.normalize_inject. destruct b; auto.
+  split. auto.
+  split. apply Mem.unchanged_on_refl.
+  split. apply Mem.unchanged_on_refl.
+  split. apply inject_incr_refl.
+  red; intros; congruence.
+(* trace length *)
+- inv H; simpl; omega.
+(* receptive *)
+- assert (t1 = t2). inv H; inv H0; auto. subst t2.
+  exists vres1; exists m1; auto.
+(* determ *)
+- inv H; inv H0.
+  assert (b = b0) by (inv H1; inv H8; auto). subst b0.
+  split; auto. constructor.
+Qed.
+
 (** ** Semantics of external functions. *)
 
 (** For functions defined outside the program ([EF_external],
@@ -1423,6 +1476,7 @@ Definition external_call (ef: external_function): extcall_sem :=
   | EF_annot_val kind txt targ => extcall_annot_val_sem txt targ
   | EF_inline_asm txt sg clb => inline_assembly_sem txt sg
   | EF_debug kind txt targs => extcall_debug_sem
+  | EF_select ty         => extcall_select_sem ty
   end.
 
 Theorem external_call_spec:
@@ -1442,6 +1496,7 @@ Proof.
   apply extcall_annot_val_ok.
   apply inline_assembly_properties.
   apply extcall_debug_ok.
+  apply extcall_select_ok.
 Qed.
 
 Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef).
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index e477957a..ef8b98a5 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -54,6 +54,7 @@ let name_of_external = function
   | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (camlstring_of_coqstring text)
   | EF_debug(kind, text, targs) ->
       sprintf "debug%d %S" (P.to_int kind) (extern_atom text)
+  | EF_select ty -> sprintf "select %s" (name_of_type ty)
 
 let rec print_builtin_arg px oc = function
   | BA x -> px oc x
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index b124586a..05cbed71 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -269,6 +269,8 @@ let external_function p = function
               coqstring text
               signatur sg
               (print_list coqstring) clob
+  | EF_select ty ->
+      fprintf p "@[<hov 2>(EF_select %a)@]" asttype ty
 
 (* Expressions *)
 
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index ee3eaca8..ca79a8a2 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -369,7 +369,8 @@ let pp_instructions pp ic =
       | EF_memcpy _
       | EF_runtime _
       | EF_vload _
-      | EF_vstore _ -> assert false
+      | EF_vstore _
+      | EF_select _ -> assert false
     end
   | Pcfi_adjust _  (* Only debug relevant *)
   | Pcfi_rel_offset _ -> assert false in (* Only debug relevant *)
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 41bc0efc..cf2c8de4 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -43,6 +43,7 @@ Require Import Integers.
 Require Import Floats.
 Require Import Op.
 Require Import CminorSel.
+Require Archi.
 
 Local Open Scope cminorsel_scope.