diff options
Diffstat (limited to 'common')
-rw-r--r-- | common/Builtins.v | 58 | ||||
-rw-r--r-- | common/Builtins0.v | 509 | ||||
-rw-r--r-- | common/Events.v | 88 |
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. |