Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

3 files changed, 647 insertions, 8 deletions

diff --git a/common/Builtins.v b/common/Builtins.v
new file mode 100644
index 00000000..c9097e86
--- /dev/null
+++ b/common/Builtins.v
@@ -0,0 +1,58 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Known built-in functions *)
+
+Require Import String Coqlib.
+Require Import AST Integers Floats Values.
+Require Export Builtins0 Builtins1.
+
+Inductive builtin_function : Type :=
+  | BI_standard (b: standard_builtin)
+  | BI_platform (b: platform_builtin).
+
+Definition builtin_function_sig (b: builtin_function) : signature :=
+  match b with
+  | BI_standard b => standard_builtin_sig b
+  | BI_platform b => platform_builtin_sig b
+  end.
+
+Definition builtin_function_sem (b: builtin_function) : builtin_sem (proj_sig_res (builtin_function_sig b)) :=
+  match b with
+  | BI_standard b => standard_builtin_sem b
+  | BI_platform b => platform_builtin_sem b
+  end.
+
+Definition lookup_builtin_function (name: string) (sg: signature) : option builtin_function :=
+  match lookup_builtin standard_builtin_sig name sg standard_builtin_table with
+  | Some b => Some (BI_standard b)
+  | None => 
+  match lookup_builtin platform_builtin_sig name sg platform_builtin_table with
+  | Some b => Some (BI_platform b)
+  | None => None
+  end end.
+
+Lemma lookup_builtin_function_sig:
+  forall name sg b, lookup_builtin_function name sg = Some b -> builtin_function_sig b = sg.
+Proof.
+  unfold lookup_builtin_function; intros.
+  destruct (lookup_builtin standard_builtin_sig name sg standard_builtin_table) as [bs|] eqn:E.
+  inv H. simpl. eapply lookup_builtin_sig; eauto.
+  destruct (lookup_builtin platform_builtin_sig name sg platform_builtin_table) as [bp|] eqn:E'.
+  inv H. simpl. eapply lookup_builtin_sig; eauto.
+  discriminate.
+Qed.
+
+
diff --git a/common/Builtins0.v b/common/Builtins0.v
new file mode 100644
index 00000000..c6a299d9
--- /dev/null
+++ b/common/Builtins0.v
@@ -0,0 +1,509 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Associating semantics to built-in functions *)
+
+Require Import String Coqlib.
+Require Import AST Integers Floats Values.
+
+(** This module provides definitions and mechanisms to associate semantics
+  with names of built-in functions.
+
+  This module is independent of the target architecture.  Each target
+  provides a [Builtins1] module that lists the built-ins semantics
+  appropriate for the target.
+*)
+
+Definition val_opt_has_type (ov: option val) (t: typ) : Prop :=
+  match ov with Some v => Val.has_type v t | None => True end.
+
+Definition val_opt_inject (j: meminj) (ov ov': option val) : Prop :=
+  match ov, ov' with
+  | None, _ => True
+  | Some v, Some v' => Val.inject j v v'
+  | _, None => False
+  end.
+
+(** The semantics of a built-in function is a partial function
+  from list of values to values.  
+  It must agree with the return type stated in the signature,
+  and be compatible with value injections.
+*)
+
+Record builtin_sem (tret: typ) : Type := mkbuiltin {
+  bs_sem :> list val -> option val;
+  bs_well_typed: forall vl, 
+    val_opt_has_type (bs_sem vl) tret;
+  bs_inject: forall j vl vl',
+    Val.inject_list j vl vl' -> val_opt_inject j (bs_sem vl) (bs_sem vl')
+}.
+
+(** Builtin functions can be created from functions over values, such as those
+  from the [Values.Val] module.  Proofs of well-typedness and compatibility with
+  injections must be provided. The constructor functions have names
+- [mkbuiltin_vNt] for a [t]otal function of [N] arguments that are [v]alues, or
+- [mkbuiltin_vNp] for a [p]artial function of [N] arguments that are [v]alues.
+*)
+
+Local Unset Program Cases.
+
+Program Definition mkbuiltin_v1t 
+     (tret: typ) (f: val -> val)
+     (WT: forall v1, Val.has_type (f v1) tret)
+     (INJ: forall j v1 v1', Val.inject j v1 v1' -> Val.inject j (f v1) (f v1')) :=
+  mkbuiltin tret (fun vl => match vl with v1 :: nil => Some (f v1) | _ => None end) _ _.
+Next Obligation.
+  red; destruct vl; auto. destruct vl; auto.
+Qed.
+Next Obligation.
+  red; inv H; auto. inv H1; auto. 
+Qed.
+
+Program Definition mkbuiltin_v2t 
+     (tret: typ) (f: val -> val -> val)
+     (WT: forall v1 v2, Val.has_type (f v1 v2) tret)
+     (INJ: forall j v1 v1' v2 v2',
+           Val.inject j v1 v1' -> Val.inject j v2 v2' ->
+           Val.inject j (f v1 v2) (f v1' v2')) :=
+  mkbuiltin tret (fun vl => match vl with v1 :: v2 :: nil => Some (f v1 v2) | _ => None end) _ _.
+Next Obligation.
+  red; destruct vl; auto. destruct vl; auto. destruct vl; auto.
+Qed.
+Next Obligation.
+  red; inv H; auto. inv H1; auto. inv H2; auto.
+Qed.
+
+Program Definition mkbuiltin_v3t 
+     (tret: typ) (f: val -> val -> val -> val)
+     (WT: forall v1 v2 v3, Val.has_type (f v1 v2 v3) tret)
+     (INJ: forall j v1 v1' v2 v2' v3 v3',
+           Val.inject j v1 v1' -> Val.inject j v2 v2' -> Val.inject j v3 v3' ->
+           Val.inject j (f v1 v2 v3) (f v1' v2' v3')) :=
+  mkbuiltin tret (fun vl => match vl with v1 :: v2 :: v3 :: nil => Some (f v1 v2 v3) | _ => None end) _ _.
+Next Obligation.
+  red; destruct vl; auto. destruct vl; auto. destruct vl; auto. destruct vl; auto.
+Qed.
+Next Obligation.
+  red; inv H; auto. inv H1; auto. inv H2; auto. inv H3; auto.
+Qed.
+
+Program Definition mkbuiltin_v1p
+     (tret: typ) (f: val -> option val)
+     (WT: forall v1, val_opt_has_type (f v1) tret)
+     (INJ: forall j v1 v1',
+        Val.inject j v1 v1' -> val_opt_inject j (f v1) (f v1')) :=
+  mkbuiltin tret (fun vl => match vl with v1 :: nil => f v1 | _ => None end) _ _.
+Next Obligation.
+  red; destruct vl; auto. destruct vl; auto. apply WT.
+Qed.
+Next Obligation.
+  red; inv H; auto. inv H1; auto. apply INJ; auto. 
+Qed.
+
+Program Definition mkbuiltin_v2p
+     (tret: typ) (f: val -> val -> option val)
+     (WT: forall v1 v2, val_opt_has_type (f v1 v2) tret)
+     (INJ: forall j v1 v1' v2 v2',
+        Val.inject j v1 v1' -> Val.inject j v2 v2' ->
+        val_opt_inject j (f v1 v2) (f v1' v2')) :=
+  mkbuiltin tret (fun vl => match vl with v1 :: v2 :: nil => f v1 v2 | _ => None end)  _ _.
+Next Obligation.
+  red; destruct vl; auto. destruct vl; auto. destruct vl; auto. apply WT.
+Qed.
+Next Obligation.
+  red; inv H; auto. inv H1; auto. inv H2; auto. apply INJ; auto. 
+Qed.
+
+(** For numerical functions, involving only integers and floating-point numbers
+  but no pointer values, we can automate the proofs of well-typedness and
+  of compatibility with injections. *)
+
+(** First we define a mapping from syntactic Cminor types ([Tint], [Tfloat], etc) to semantic Coq types. *)
+
+Definition valty (t: typ) : Type :=
+  match t with
+  | Tint => int
+  | Tlong => int64
+  | Tfloat => float
+  | Tsingle => float32
+  | Tany32 | Tany64 => Empty_set (**r no clear semantic meaning *)
+  end.
+
+(** We can inject and project between the numerical type [valty t] and the type [val]. *)
+
+Definition inj_num (t: typ) : valty t -> val :=
+  match t with
+  | Tint => Vint
+  | Tlong => Vlong
+  | Tfloat => Vfloat
+  | Tsingle => Vsingle
+  | Tany32 | Tany64 => fun _ => Vundef
+  end.
+
+Definition proj_num {A: Type} (t: typ) (k0: A) (v: val): (valty t -> A) -> A :=
+  match t with
+  | Tint => fun k1 => match v with Vint n => k1 n | _ => k0 end
+  | Tlong => fun k1 => match v with Vlong n => k1 n | _ => k0 end
+  | Tfloat => fun k1 => match v with Vfloat n => k1 n | _ => k0 end
+  | Tsingle => fun k1 => match v with Vsingle n => k1 n | _ => k0 end
+  | Tany32 | Tany64 => fun k1 => k0
+  end.
+
+Lemma inj_num_wt: forall t x, Val.has_type (inj_num t x) t.
+Proof.
+  destruct t; intros; exact I.
+Qed.
+
+Lemma inj_num_inject: forall j t x, Val.inject j (inj_num t x) (inj_num t x).
+Proof.
+  destruct t; intros; constructor.
+Qed.
+
+Lemma inj_num_opt_wt: forall t x, val_opt_has_type (option_map (inj_num t) x) t.
+Proof.
+  intros. destruct x; simpl. apply inj_num_wt. auto. 
+Qed.
+
+Lemma inj_num_opt_inject: forall j t x,
+  val_opt_inject j (option_map (inj_num t) x) (option_map (inj_num t) x).
+Proof.
+  destruct x; simpl. apply inj_num_inject. auto.
+Qed.
+
+Lemma proj_num_wt:
+  forall tres t k1 v,
+  (forall x, Val.has_type (k1 x) tres) ->
+  Val.has_type (proj_num t Vundef v k1) tres.
+Proof.
+  intros. destruct t; simpl; destruct v; auto; exact I.
+Qed.
+
+Lemma proj_num_inject:
+  forall j t k1 v k1' v',
+  (forall x, Val.inject j (k1 x) (k1' x)) ->
+  Val.inject j v v' -> 
+  Val.inject j (proj_num t Vundef v k1) (proj_num t Vundef v' k1').
+Proof.
+  intros. destruct t; simpl; inv H0; auto.
+Qed.
+
+Lemma proj_num_opt_wt:
+  forall tres t k0 k1 v,
+  k0 = None \/ k0 = Some Vundef ->
+  (forall x, val_opt_has_type (k1 x) tres) ->
+  val_opt_has_type (proj_num t k0 v k1) tres.
+Proof.
+  intros.
+  assert (val_opt_has_type k0 tres). { destruct H; subst k0; exact I. }
+  destruct t; simpl; destruct v; auto.
+Qed.
+
+Lemma proj_num_opt_inject:
+  forall j k0 t k1 v k1' v',
+  (forall ov, val_opt_inject j k0 ov) ->
+  (forall x, val_opt_inject j (k1 x) (k1' x)) ->
+  Val.inject j v v' -> 
+  val_opt_inject j (proj_num t k0 v k1) (proj_num t k0 v' k1').
+Proof.
+  intros. destruct t; simpl; inv H1; auto.
+Qed.
+
+(** Wrapping numerical functions as built-ins.  The constructor functions
+  have names
+- [mkbuiltin_nNt] for a [t]otal function of [N] numbers, or
+- [mkbuiltin_vNp] for a [p]artial function of [N] numbers.
+ *)
+
+Program Definition mkbuiltin_n1t 
+    (targ1: typ) (tres: typ)
+    (f: valty targ1 -> valty tres) :=
+  mkbuiltin_v1t tres
+    (fun v1 => proj_num targ1 Vundef v1 (fun x => inj_num tres (f x)))
+    _ _.
+Next Obligation.
+  auto using proj_num_wt, inj_num_wt.
+Qed.
+Next Obligation.
+  auto using proj_num_inject, inj_num_inject.
+Qed.
+
+Program Definition mkbuiltin_n2t 
+    (targ1 targ2: typ) (tres: typ)
+    (f: valty targ1 -> valty targ2 -> valty tres) :=
+  mkbuiltin_v2t tres
+    (fun v1 v2 =>
+       proj_num targ1 Vundef v1 (fun x1 =>
+       proj_num targ2 Vundef v2 (fun x2 => inj_num tres (f x1 x2))))
+    _ _.
+Next Obligation.
+  auto using proj_num_wt, inj_num_wt.
+Qed.
+Next Obligation.
+  auto using proj_num_inject, inj_num_inject.
+Qed.
+
+Program Definition mkbuiltin_n3t 
+    (targ1 targ2 targ3: typ) (tres: typ)
+    (f: valty targ1 -> valty targ2 -> valty targ3 -> valty tres) :=
+  mkbuiltin_v3t tres
+    (fun v1 v2 v3 =>
+       proj_num targ1 Vundef v1 (fun x1 =>
+       proj_num targ2 Vundef v2 (fun x2 =>
+       proj_num targ3 Vundef v3 (fun x3 => inj_num tres (f x1 x2 x3)))))
+    _ _.
+Next Obligation.
+  auto using proj_num_wt, inj_num_wt.
+Qed.
+Next Obligation.
+  auto using proj_num_inject, inj_num_inject.
+Qed.
+
+Program Definition mkbuiltin_n1p
+    (targ1: typ) (tres: typ)
+    (f: valty targ1 -> option (valty tres)) :=
+  mkbuiltin_v1p tres
+    (fun v1 => proj_num targ1 None v1 (fun x => option_map (inj_num tres) (f x)))
+    _ _.
+Next Obligation.
+  auto using proj_num_opt_wt, inj_num_opt_wt.
+Qed.
+Next Obligation.
+  apply proj_num_opt_inject; auto. intros; red; auto. intros; apply inj_num_opt_inject.
+Qed.
+
+Program Definition mkbuiltin_n2p
+    (targ1 targ2: typ) (tres: typ)
+    (f: valty targ1 -> valty targ2 -> option (valty tres)) :=
+  mkbuiltin_v2p tres
+    (fun v1 v2 =>
+      proj_num targ1 None v1 (fun x1 =>
+      proj_num targ2 None v2 (fun x2 => option_map (inj_num tres) (f x1 x2))))
+    _ _.
+Next Obligation.
+  auto using proj_num_opt_wt, inj_num_opt_wt.
+Qed.
+Next Obligation.
+  apply proj_num_opt_inject; auto. intros; red; auto. intros.
+  apply proj_num_opt_inject; auto. intros; red; auto. intros.
+  apply inj_num_opt_inject.
+Qed.
+
+(** Looking up builtins by name and signature *)
+
+Section LOOKUP.
+
+Context {A: Type} (sig_of: A -> signature).
+
+Fixpoint lookup_builtin (name: string) (sg: signature) (l: list (string * A)) : option A :=
+  match l with
+  | nil => None
+  | (n, b) :: l =>
+      if string_dec name n && signature_eq sg (sig_of b)
+      then Some b
+      else lookup_builtin name sg l
+  end.
+
+Lemma lookup_builtin_sig: forall name sg b l,
+  lookup_builtin name sg l = Some b -> sig_of b = sg.
+Proof.
+  induction l as [ | [n b'] l ]; simpl; intros.
+- discriminate.
+- destruct (string_dec name n && signature_eq sg (sig_of b')) eqn:E.
++ InvBooleans. congruence.
++ auto.
+Qed.
+
+End LOOKUP.
+
+(** The standard, platform-independent built-ins *)
+
+Inductive standard_builtin : Type :=
+  | BI_select (t: typ)
+  | BI_fabs
+  | BI_fsqrt
+  | BI_negl
+  | BI_addl
+  | BI_subl
+  | BI_mull
+  | BI_i64_umulh
+  | BI_i64_smulh
+  | BI_i64_sdiv
+  | BI_i64_udiv
+  | BI_i64_smod
+  | BI_i64_umod
+  | BI_i64_shl
+  | BI_i64_shr
+  | BI_i64_sar
+  | BI_i64_dtos
+  | BI_i64_dtou
+  | BI_i64_stod
+  | BI_i64_utod
+  | BI_i64_stof
+  | BI_i64_utof.
+
+Local Open Scope string_scope.
+
+Definition standard_builtin_table : list (string * standard_builtin) :=
+    ("__builtin_sel", BI_select Tint)
+ :: ("__builtin_sel", BI_select Tlong)
+ :: ("__builtin_sel", BI_select Tfloat)
+ :: ("__builtin_sel", BI_select Tsingle)
+ :: ("__builtin_fabs", BI_fabs)
+ :: ("__builtin_fsqrt", BI_fsqrt)
+ :: ("__builtin_negl", BI_negl)
+ :: ("__builtin_addl", BI_addl)
+ :: ("__builtin_subl", BI_subl)
+ :: ("__builtin_mull", BI_mull)
+ :: ("__compcert_i64_umulh", BI_i64_umulh)
+ :: ("__compcert_i64_smulh", BI_i64_smulh)
+ :: ("__compcert_i64_sdiv", BI_i64_sdiv)
+ :: ("__compcert_i64_udiv", BI_i64_udiv)
+ :: ("__compcert_i64_smod", BI_i64_smod)
+ :: ("__compcert_i64_umod", BI_i64_umod)
+ :: ("__compcert_i64_shl", BI_i64_shl)
+ :: ("__compcert_i64_shr", BI_i64_shr)
+ :: ("__compcert_i64_sar", BI_i64_sar)
+ :: ("__compcert_i64_dtos", BI_i64_dtos)
+ :: ("__compcert_i64_dtou", BI_i64_dtou)
+ :: ("__compcert_i64_stod", BI_i64_stod)
+ :: ("__compcert_i64_utod", BI_i64_utod)
+ :: ("__compcert_i64_stof", BI_i64_stof)
+ :: ("__compcert_i64_utof", BI_i64_utof)
+ :: nil.
+
+Definition standard_builtin_sig (b: standard_builtin) : signature :=
+  match b with
+  | BI_select t =>
+      mksignature (Tint :: t :: t :: nil) (Some t) cc_default
+  | BI_fabs | BI_fsqrt =>
+      mksignature (Tfloat :: nil) (Some Tfloat) cc_default
+  | BI_negl =>
+      mksignature (Tlong :: nil) (Some Tlong) cc_default
+  | BI_addl | BI_subl | BI_i64_umulh| BI_i64_smulh 
+  | BI_i64_sdiv | BI_i64_udiv | BI_i64_smod | BI_i64_umod =>
+      mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default
+  | BI_mull =>
+      mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default
+  | BI_i64_shl  | BI_i64_shr | BI_i64_sar =>
+      mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default
+  | BI_i64_dtos | BI_i64_dtou =>
+      mksignature (Tfloat :: nil) (Some Tlong) cc_default
+  | BI_i64_stod | BI_i64_utod =>
+      mksignature (Tlong :: nil) (Some Tfloat) cc_default
+  | BI_i64_stof | BI_i64_utof =>
+      mksignature (Tlong :: nil) (Some Tsingle) cc_default
+  end.
+
+Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (proj_sig_res (standard_builtin_sig b)) :=
+  match b with
+  | BI_select t =>
+      mkbuiltin t 
+       (fun vargs => match vargs with
+          | Vint n :: v1 :: v2 :: nil => Some (Val.normalize (if Int.eq n Int.zero then v2 else v1) t)
+          | _ => None
+        end) _ _
+  | BI_fabs => mkbuiltin_n1t Tfloat Tfloat Float.abs
+  | BI_fsqrt => mkbuiltin_n1t Tfloat Tfloat Float.sqrt
+  | BI_negl => mkbuiltin_n1t Tlong Tlong Int64.neg
+  | BI_addl => mkbuiltin_v2t Tlong Val.addl _ _ 
+  | BI_subl => mkbuiltin_v2t Tlong Val.subl _ _
+  | BI_mull => mkbuiltin_v2t Tlong Val.mull' _ _
+  | BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
+  | BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
+  | BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _
+  | BI_i64_udiv => mkbuiltin_v2p Tlong Val.divlu _ _
+  | BI_i64_smod => mkbuiltin_v2p Tlong Val.modls _ _
+  | BI_i64_umod => mkbuiltin_v2p Tlong Val.modlu _ _
+  | BI_i64_shl => mkbuiltin_v2t Tlong Val.shll _ _
+  | BI_i64_shr => mkbuiltin_v2t Tlong Val.shrlu _ _
+  | BI_i64_sar => mkbuiltin_v2t Tlong Val.shrl _ _
+  | BI_i64_dtos => mkbuiltin_n1p Tfloat Tlong Float.to_long
+  | BI_i64_dtou => mkbuiltin_n1p Tfloat Tlong Float.to_longu
+  | BI_i64_stod => mkbuiltin_n1t Tlong Tfloat Float.of_long
+  | BI_i64_utod => mkbuiltin_n1t Tlong Tfloat Float.of_longu
+  | BI_i64_stof => mkbuiltin_n1t Tlong Tsingle Float32.of_long
+  | BI_i64_utof => mkbuiltin_n1t Tlong Tsingle Float32.of_longu
+  end.
+Next Obligation. 
+  red. destruct vl; auto. destruct v; auto. 
+  destruct vl; auto. destruct vl; auto. destruct vl; auto.
+  apply Val.normalize_type.
+Qed.
+Next Obligation.
+  red. inv H; auto. inv H0; auto. inv H1; auto. inv H0; auto. inv H2; auto.
+  apply Val.normalize_inject. destruct (Int.eq i Int.zero); auto.
+Qed.
+Next Obligation.
+  unfold Val.addl, Val.has_type; destruct v1; auto; destruct v2; auto; destruct Archi.ptr64; auto.
+Qed.
+Next Obligation.
+  apply Val.addl_inject; auto.
+Qed.   
+Next Obligation.
+  unfold Val.subl, Val.has_type, negb; destruct v1; auto; destruct v2; auto;
+  destruct Archi.ptr64; auto; destruct (eq_block b0 b1); auto.
+Qed.
+Next Obligation.
+  apply Val.subl_inject; auto.
+Qed.
+Next Obligation.
+  unfold Val.mull', Val.has_type; destruct v1; simpl; auto; destruct v2; auto.
+Qed.
+Next Obligation.
+  inv H; simpl; auto. inv H0; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct orb; exact I.
+Qed.
+Next Obligation.
+  red. inv H; simpl; auto. inv H0; auto. destruct orb; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct Int64.eq; exact I.
+Qed.
+Next Obligation.
+  red. inv H; simpl; auto. inv H0; auto. destruct Int64.eq; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct orb; exact I.
+Qed.
+Next Obligation.
+  red. inv H; simpl; auto. inv H0; auto. destruct orb; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct Int64.eq; exact I.
+Qed.
+Next Obligation.
+  red. inv H; simpl; auto. inv H0; auto. destruct Int64.eq; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct Int.ltu; auto.
+Qed.
+Next Obligation.
+  inv H; simpl; auto. inv H0; auto. destruct Int.ltu; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct Int.ltu; auto.
+Qed.
+Next Obligation.
+  inv H; simpl; auto. inv H0; auto. destruct Int.ltu; auto.
+Qed.
+Next Obligation.
+  red. destruct v1; simpl; auto. destruct v2; auto. destruct Int.ltu; auto.
+Qed.
+Next Obligation.
+  inv H; simpl; auto. inv H0; auto. destruct Int.ltu; auto.
+Qed.
+
diff --git a/common/Events.v b/common/Events.v
index 26dd505f..3fb84f49 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -24,6 +24,7 @@ Require Import Floats.
 Require Import Values.
 Require Import Memory.
 Require Import Globalenvs.
+Require Import Builtins.
 
 (** * Events and traces *)
 
@@ -1377,12 +1378,67 @@ Proof.
   split. constructor. auto.
 Qed.
 
+(** ** Semantics of known built-in functions. *)
+
+(** Some built-in functions and runtime support functions have known semantics
+  as defined in the [Builtin] modules.
+  These built-in functions have no observable effects and do not access memory. *)
+
+Inductive known_builtin_sem (bf: builtin_function) (ge: Senv.t):
+              list val -> mem -> trace -> val -> mem -> Prop :=
+  | known_builtin_sem_intro: forall vargs vres m,
+      builtin_function_sem bf vargs = Some vres ->
+      known_builtin_sem bf ge vargs m E0 vres m.
+
+Lemma known_builtin_ok: forall bf,
+  extcall_properties (known_builtin_sem bf) (builtin_function_sig bf).
+Proof.
+  intros. set (bsem := builtin_function_sem bf). constructor; intros.
+(* well typed *)
+- inv H.
+  specialize (bs_well_typed  _ bsem vargs). unfold val_opt_has_type, bsem; rewrite H0.
+  auto.
+(* symbols *)
+- inv H0. econstructor; eauto.
+(* valid blocks *)
+- inv H; auto.
+(* perms *)
+- inv H; auto.
+(* readonly *)
+- inv H. apply Mem.unchanged_on_refl.
+(* mem extends *)
+- inv H. fold bsem in H2. apply val_inject_list_lessdef in H1.
+  specialize (bs_inject _ bsem _ _ _ H1).
+  unfold val_opt_inject; rewrite H2; intros.
+  destruct (bsem vargs') as [vres'|] eqn:?; try contradiction.
+  exists vres', m1'; intuition auto using Mem.extends_refl, Mem.unchanged_on_refl.
+  constructor; auto.
+  apply val_inject_lessdef; auto.
+(* mem injects *)
+- inv H0. fold bsem in H3.
+  specialize (bs_inject _ bsem _ _ _ H2).
+  unfold val_opt_inject; rewrite H3; intros.
+  destruct (bsem vargs') as [vres'|] eqn:?; try contradiction.
+  exists f, vres', m1'; intuition auto using Mem.extends_refl, Mem.unchanged_on_refl.
+  constructor; auto.
+  red; intros; congruence.
+(* trace length *)
+- inv H; simpl; omega.
+(* receptive *)
+- inv H; inv H0. exists vres1, m1; constructor; auto. 
+(* determ *)
+- inv H; inv H0.
+  split. constructor. intuition congruence. 
+Qed.
+
 (** ** Semantics of external functions. *)
 
-(** For functions defined outside the program ([EF_external],
-  [EF_builtin] and [EF_runtime]), we do not define their
-  semantics, but only assume that it satisfies
-  [extcall_properties]. *)
+(** For functions defined outside the program ([EF_external]),
+  we do not define their semantics, but only assume that it satisfies
+  [extcall_properties].
+  We do the same for built-in functions and runtime support functions that
+  are not described in [Builtins].
+*)
 
 Parameter external_functions_sem: String.string -> signature -> extcall_sem.
 
@@ -1398,6 +1454,22 @@ Axiom inline_assembly_properties:
 
 (** ** Combined semantics of external calls *)
 
+Definition builtin_or_external_sem name sg :=
+  match lookup_builtin_function name sg with
+  | Some bf => known_builtin_sem bf
+  | None => external_functions_sem name sg
+  end.
+
+Lemma builtin_or_external_sem_ok: forall name sg,
+  extcall_properties (builtin_or_external_sem name sg) sg.
+Proof.
+  unfold builtin_or_external_sem; intros. 
+  destruct (lookup_builtin_function name sg) as [bf|] eqn:L.
+- exploit lookup_builtin_function_sig; eauto. intros EQ; subst sg.
+  apply known_builtin_ok.
+- apply external_functions_properties.
+Qed.
+
 (** Combining the semantics given above for the various kinds of external calls,
   we define the predicate [external_call] that relates:
 - the external function being invoked
@@ -1412,8 +1484,8 @@ This predicate is used in the semantics of all CompCert languages. *)
 Definition external_call (ef: external_function): extcall_sem :=
   match ef with
   | EF_external name sg  => external_functions_sem name sg
-  | EF_builtin name sg   => external_functions_sem name sg
-  | EF_runtime name sg   => external_functions_sem name sg
+  | EF_builtin name sg   => builtin_or_external_sem name sg
+  | EF_runtime name sg   => builtin_or_external_sem name sg
   | EF_vload chunk       => volatile_load_sem chunk
   | EF_vstore chunk      => volatile_store_sem chunk
   | EF_malloc            => extcall_malloc_sem
@@ -1431,8 +1503,8 @@ Theorem external_call_spec:
 Proof.
   intros. unfold external_call, ef_sig; destruct ef.
   apply external_functions_properties.
-  apply external_functions_properties.
-  apply external_functions_properties.
+  apply builtin_or_external_sem_ok.
+  apply builtin_or_external_sem_ok.
   apply volatile_load_ok.
   apply volatile_store_ok.
   apply extcall_malloc_ok.