Give formal semantics to some built-in functions and run-time functions

This commit adds mechanisms to
- recognize certain built-in and run-time functions by name and signature;
- associate semantics to these functions, as a partial function from
  list of values to values;
- interpret external calls to these functions according to this semantics
  (pure function from values to values, memory unchanged, no observable
  events in the trace);
- external calls to unknown built-in and run-time functions remain
  interpreted as generating observable events and possibly changing
  memory, like before.

The description of the built-ins is split into a target-independent
part (in common/Builtins0.v) and a target-specific part (in
$ARCH/Builtins1.v).

Instruction selection uses the new mechanism in order to
- recognize some built-in functions and turn them into operations
  of the target processor.  Currently, this is done for
  __builtin_sel and __builtin_fabs; more to come.
- remove the axioms about int64 helper functions from the standard
  library.  More precisely, the behavior of these functions is
  still axiomatized, but now it is specified using the more general
  machinery introduced in this commit, rather than ad-hoc axioms
  in backend/SplitLongproof.

The only built-ins currently described are __builtin_fsqrt (for all platforms)
and __builtin_fmin / __builtin_fmax (for x86).  More built-ins will be
added later.

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.