diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | arm/Builtins1.v | 33 | ||||
| -rw-r--r-- | arm/SelectOp.vp | 12 | ||||
| -rw-r--r-- | arm/SelectOpproof.v | 25 | ||||
| -rw-r--r-- | backend/Selection.v | 53 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 157 | ||||
| -rw-r--r-- | backend/SplitLongproof.v | 133 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 43 | ||||
| -rw-r--r-- | common/Builtins.v | 58 | ||||
| -rw-r--r-- | common/Builtins0.v | 509 | ||||
| -rw-r--r-- | common/Events.v | 88 | ||||
| -rw-r--r-- | powerpc/Builtins1.v | 33 | ||||
| -rw-r--r-- | powerpc/SelectOp.vp | 12 | ||||
| -rw-r--r-- | powerpc/SelectOpproof.v | 25 | ||||
| -rw-r--r-- | riscV/Builtins1.v | 33 | ||||
| -rw-r--r-- | riscV/SelectOp.vp | 12 | ||||
| -rw-r--r-- | riscV/SelectOpproof.v | 28 | ||||
| -rw-r--r-- | x86/Builtins1.v | 54 | ||||
| -rw-r--r-- | x86/SelectOp.vp | 7 | ||||
| -rw-r--r-- | x86/SelectOpproof.v | 24 |
20 files changed, 1154 insertions, 187 deletions
@@ -63,7 +63,7 @@ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ COMMON=Errors.v AST.v Linking.v \ Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \ Values.v Smallstep.v Behaviors.v Switch.v Determinism.v Unityping.v \ - Separation.v + Separation.v Builtins0.v Builtins1.v Builtins.v # Back-end modules (in backend/, $(ARCH)/) diff --git a/arm/Builtins1.v b/arm/Builtins1.v new file mode 100644 index 00000000..f6e643d2 --- /dev/null +++ b/arm/Builtins1.v @@ -0,0 +1,33 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Platform-specific built-in functions *) + +Require Import String Coqlib. +Require Import AST Integers Floats Values. +Require Import Builtins0. + +Inductive platform_builtin : Type := . + +Local Open Scope string_scope. + +Definition platform_builtin_table : list (string * platform_builtin) := + nil. + +Definition platform_builtin_sig (b: platform_builtin) : signature := + match b with end. + +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := + match b with end. diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index d04832d6..1220abc4 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -38,11 +38,8 @@ Require Import Coqlib. Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. +Require Import AST Integers Floats Builtins. +Require Import Op CminorSel. Local Open Scope cminorsel_scope. @@ -518,3 +515,8 @@ Nondetfunction builtin_arg (e: expr) := | Eop (Oaddimm n) (e1:::Enil) => BA_addptr (BA e1) (BA_int n) | _ => BA e end. + +(** Platform-specific known builtins *) + +Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := + None. diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 8b546971..5d54d94f 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -13,16 +13,9 @@ (** Correctness of instruction selection for operators *) Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. +Require Import AST Integers Floats. +Require Import Values Memory Builtins Globalenvs. +Require Import Cminor Op CminorSel. Require Import SelectOp. Local Open Scope cminorsel_scope. @@ -909,4 +902,16 @@ Proof. - constructor; auto. Qed. +(** Platform-specific known builtins *) + +Theorem eval_platform_builtin: + forall bf al a vl v le, + platform_builtin bf al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem bf vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + intros. discriminate. +Qed. + End CMCONSTR. diff --git a/backend/Selection.v b/backend/Selection.v index 4154659c..c9771d99 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -24,7 +24,7 @@ Require String. Require Import Coqlib Maps. -Require Import AST Errors Integers Globalenvs Switch. +Require Import AST Errors Integers Globalenvs Builtins Switch. Require Cminor. Require Import Op CminorSel Cminortyping. Require Import SelectOp SplitLong SelectLong SelectDiv. @@ -162,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) (cnd ifso ifnot: expr) : expr := + let (cond, args) := condition_of_expr cnd in + match SelectOp.select ty cond args ifso ifnot with + | Some a => a + | None => Econdition (condexpr_of_expr cnd) ifso ifnot + end. + (** Conversion from Cminor expression to Cminorsel expressions *) Fixpoint sel_expr (a: Cminor.expr) : expr := @@ -231,6 +238,43 @@ Definition sel_builtin_res (optid: option ident) : builtin_res ident := | Some id => BR id end. +(** Known builtin functions *) + +Function sel_known_builtin (bf: builtin_function) (args: exprlist) := + match bf, args with + | BI_platform b, _ => + SelectOp.platform_builtin b args + | BI_standard (BI_select ty), a1 ::: a2 ::: a3 ::: Enil => + Some (sel_select ty a1 a2 a3) + | BI_standard BI_fabs, a1 ::: Enil => + Some (SelectOp.absf a1) + | _, _ => + None + end. + +(** Builtin functions in general *) + +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)). + +Definition sel_builtin (optid: option ident) (ef: external_function) + (args: list Cminor.expr) := + match optid, ef with + | Some id, EF_builtin name sg => + match lookup_builtin_function name sg with + | Some bf => + match sel_known_builtin bf (sel_exprlist args) with + | Some a => Sassign id a + | None => sel_builtin_default optid ef args + end + | None => sel_builtin_default optid ef args + end + | _, _ => + sel_builtin_default optid ef args + end. + (** Conversion of Cminor [switch] statements to decision trees. *) Parameter compile_switch: Z -> nat -> table -> comptree. @@ -342,13 +386,10 @@ Fixpoint sel_stmt (ki: known_idents) (env: typenv) (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 50875086..ee3ed358 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -14,7 +14,8 @@ Require Import FunInd. Require Import Coqlib Maps. -Require Import AST Linking Errors Integers Values Memory Events Globalenvs Smallstep. +Require Import AST Linking Errors Integers. +Require Import Values Memory Builtins Events Globalenvs Smallstep. Require Import Switch Cminor Op CminorSel Cminortyping. Require Import SelectOp SelectDiv SplitLong SelectLong Selection. Require Import SelectOpproof SelectDivproof SplitLongproof SelectLongproof. @@ -216,19 +217,16 @@ 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. + eval_exprlist tge sp e m le (snd (condition_of_expr a)) vl + /\ eval_condition (fst (condition_of_expr a)) 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. + intros a; functional induction (condition_of_expr a); intros; simpl. +- inv H. exists vl; split; auto. + simpl in H6. inv H6. apply Val.bool_of_val_of_optbool in H0. auto. +- exists (v :: nil); split. + constructor; auto; constructor. + inv H0; simpl; auto. Qed. Lemma eval_load: @@ -353,6 +351,52 @@ Proof. exists v; split; auto. eapply eval_cmplu; eauto. Qed. +Lemma eval_sel_select: + forall le a1 a2 a3 v1 v2 v3 b ty, + 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.select (Some b) v2 v3 ty) v. +Proof. + unfold sel_select; intros. + specialize (eval_condition_of_expr _ _ _ _ H H2). + destruct (condition_of_expr a1) as [cond args]; simpl fst; simpl snd. intros (vl & A & B). + destruct (select ty cond args a2 a3) as [a|] eqn:SEL. +- eapply eval_select; eauto. +- exists (if b then v2 else v3); split. + econstructor; eauto. eapply eval_condexpr_of_expr; eauto. destruct b; auto. + apply Val.lessdef_normalize. +Qed. + +(** Known built-in functions *) + +Lemma eval_sel_known_builtin: + forall bf args a vl v le, + sel_known_builtin bf args = Some a -> + eval_exprlist tge sp e m le args vl -> + builtin_function_sem bf vl = Some v -> + exists v', eval_expr tge sp e m le a v' /\ Val.lessdef v v'. +Proof. + intros until le; intros SEL ARGS SEM. + destruct bf as [bf|bf]; simpl in SEL. +- destruct bf; try discriminate. ++ (* select *) + inv ARGS; try discriminate. inv H0; try discriminate. inv H2; try discriminate. inv H3; try discriminate. + inv SEL. + simpl in SEM. destruct v1; inv SEM. + replace (Val.normalize (if Int.eq i Int.zero then v2 else v0) t) + with (Val.select (Some (negb (Int.eq i Int.zero))) v0 v2 t) + by (destruct (Int.eq i Int.zero); reflexivity). + eapply eval_sel_select; eauto. constructor. ++ (* fabs *) + inv ARGS; try discriminate. inv H0; try discriminate. + inv SEL. + simpl in SEM; inv SEM. apply eval_absf; auto. +- eapply eval_platform_builtin; eauto. +Qed. + End CMCONSTR. (** Recognition of calls to built-in functions *) @@ -793,6 +837,51 @@ Proof. intros. destruct oid; simpl; auto. apply set_var_lessdef; auto. Qed. +Lemma sel_builtin_default_correct: + forall optid ef al sp e1 m1 vl t v m2 e1' m1' f k, + Cminor.eval_exprlist ge sp e1 m1 al vl -> + external_call ef ge vl m1 t v m2 -> + env_lessdef e1 e1' -> Mem.extends m1 m1' -> + exists e2' m2', + step tge (State f (sel_builtin_default 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. unfold sel_builtin_default. + exploit sel_builtin_args_correct; eauto. intros (vl' & A & B). + exploit external_call_mem_extends; eauto. intros (v' & m2' & D & E & F & _). + econstructor; exists m2'; split. + econstructor. eexact A. eapply external_call_symbols_preserved. eexact senv_preserved. eexact D. + split; auto. apply sel_builtin_res_correct; auto. +Qed. + +Lemma sel_builtin_correct: + forall optid ef al sp e1 m1 vl t v m2 e1' m1' f k, + Cminor.eval_exprlist ge sp e1 m1 al vl -> + external_call ef ge vl m1 t v m2 -> + env_lessdef e1 e1' -> Mem.extends m1 m1' -> + 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. + exploit sel_exprlist_correct; eauto. intros (vl' & A & B). + exploit external_call_mem_extends; eauto. intros (v' & m2' & D & E & F & _). + unfold sel_builtin. + destruct optid as [id|]; eauto using sel_builtin_default_correct. + destruct ef; eauto using sel_builtin_default_correct. + destruct (lookup_builtin_function name sg) as [bf|] eqn:LKUP; eauto using sel_builtin_default_correct. + destruct (sel_known_builtin bf (sel_exprlist al)) as [a|] eqn:SKB; eauto using sel_builtin_default_correct. + simpl in D. red in D. rewrite LKUP in D. inv D. + exploit eval_sel_known_builtin; eauto. intros (v'' & U & V). + econstructor; exists m2'; split. + econstructor. eexact U. + split; auto. apply set_var_lessdef; auto. apply Val.lessdef_trans with v'; auto. +Qed. + (** If-conversion *) Lemma classify_stmt_sound_1: @@ -982,19 +1071,18 @@ 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' env + | match_builtin_1: forall cunit hf ef args optid f sp e k m al f' e' k' m' env (LINK: linkorder cunit prog) (HF: helper_functions_declared cunit hf) (TF: sel_function (prog_defmap cunit) hf f = OK f') (TYF: type_function f = OK env) (MC: match_cont cunit hf (known_id f) env k k') - (LDA: Val.lessdef_list args args') + (EA: Cminor.eval_exprlist ge sp e m al args) (LDE: env_lessdef e e') - (ME: Mem.extends m m') - (EA: list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') al args'), + (ME: Mem.extends m m'), 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') + (State f' (sel_builtin 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' env (LINK: linkorder cunit prog) (HF: helper_functions_declared cunit hf) @@ -1002,11 +1090,11 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (TYF: type_function f = OK env) (MC: match_cont cunit hf (known_id f) env 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 ki env k k', @@ -1078,6 +1166,14 @@ Proof. destruct (ident_eq id id0). conclude. discriminate. Qed. +Remark sel_builtin_nolabel: + forall (hf: helper_functions) optid ef args, nolabel' (sel_builtin optid ef args). +Proof. + unfold sel_builtin; intros; red; intros. + destruct optid; auto. destruct ef; auto. destruct lookup_builtin_function; auto. + destruct sel_known_builtin; auto. +Qed. + Remark find_label_commut: forall cunit hf ki env lbl s k s' k', match_cont cunit hf ki env k k' -> @@ -1093,8 +1189,11 @@ Proof. unfold store. destruct (addressing m (sel_expr e)); simpl; auto. (* call *) destruct (classify_call (prog_defmap cunit) e); simpl; auto. + rewrite sel_builtin_nolabel; auto. (* tailcall *) destruct (classify_call (prog_defmap cunit) e); simpl; auto. +(* builtin *) + rewrite sel_builtin_nolabel; auto. (* seq *) exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; @@ -1188,9 +1287,7 @@ Proof. 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; left; split. simpl. omega. split. auto. - econstructor; eauto. + right; left; split. simpl; omega. split; auto. econstructor; eauto. - (* Stailcall *) exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. erewrite <- stackspace_function_translated in P by eauto. @@ -1207,12 +1304,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' & P & Q & R). + left; econstructor; split. eexact P. econstructor; eauto. - (* Seq *) left; econstructor; split. constructor. @@ -1303,11 +1396,8 @@ 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]]]]]. - left; econstructor; split. - econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. - econstructor; eauto. + exploit sel_builtin_correct; eauto. intros (e2' & m2' & P & Q & R). + left; econstructor; split. eexact P. econstructor; eauto. - (* return *) inv MC. left; econstructor; split. @@ -1315,7 +1405,6 @@ Proof. econstructor; eauto. destruct optid; simpl; auto. apply set_var_lessdef; auto. - (* return of an external call turned into a Sbuiltin *) right; left; split. simpl; omega. split. auto. econstructor; eauto. - apply sel_builtin_res_correct; auto. Qed. Lemma sel_initial_states: diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index f1e8b590..18c1f18d 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -15,42 +15,13 @@ Require Import String. Require Import Coqlib Maps. Require Import AST Errors Integers Floats. -Require Import Values Memory Globalenvs Events Cminor Op CminorSel. +Require Import Values Memory Globalenvs Builtins Events Cminor Op CminorSel. Require Import SelectOp SelectOpproof SplitLong. Local Open Scope cminorsel_scope. Local Open Scope string_scope. -(** * Axiomatization of the helper functions *) - -Definition external_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := - forall F V (ge: Genv.t F V) m, - external_call (EF_runtime name sg) ge vargs m E0 vres m. - -Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := - forall F V (ge: Genv.t F V) m, - external_call (EF_builtin name sg) ge vargs m E0 vres m. - -Axiom i64_helpers_correct : - (forall x z, Val.longoffloat x = Some z -> external_implements "__compcert_i64_dtos" sig_f_l (x::nil) z) - /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__compcert_i64_dtou" sig_f_l (x::nil) z) - /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__compcert_i64_stod" sig_l_f (x::nil) z) - /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__compcert_i64_utod" sig_l_f (x::nil) z) - /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__compcert_i64_stof" sig_l_s (x::nil) z) - /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__compcert_i64_utof" sig_l_s (x::nil) z) - /\ (forall x, builtin_implements "__builtin_negl" sig_l_l (x::nil) (Val.negl x)) - /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y)) - /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y)) - /\ (forall x y, builtin_implements "__builtin_mull" sig_ii_l (x::y::nil) (Val.mull' x y)) - /\ (forall x y z, Val.divls x y = Some z -> external_implements "__compcert_i64_sdiv" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i64_udiv" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i64_smod" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i64_umod" sig_ll_l (x::y::nil) z) - /\ (forall x y, external_implements "__compcert_i64_shl" sig_li_l (x::y::nil) (Val.shll x y)) - /\ (forall x y, external_implements "__compcert_i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y)) - /\ (forall x y, external_implements "__compcert_i64_sar" sig_li_l (x::y::nil) (Val.shrl x y)) - /\ (forall x y, external_implements "__compcert_i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y)) - /\ (forall x y, external_implements "__compcert_i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y)). +(** * Properties of the helper functions *) Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))). @@ -84,60 +55,67 @@ Variable sp: val. Variable e: env. Variable m: mem. -Ltac UseHelper := decompose [Logic.and] i64_helpers_correct; eauto. Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. Lemma eval_helper: - forall le id name sg args vargs vres, + forall bf le id name sg args vargs vres, eval_exprlist ge sp e m le args vargs -> helper_declared prog id name sg -> - external_implements name sg vargs vres -> + lookup_builtin_function name sg = Some bf -> + builtin_function_sem bf vargs = Some vres -> eval_expr ge sp e m le (Eexternal id sg args) vres. Proof. intros. red in H0. apply Genv.find_def_symbol in H0. destruct H0 as (b & P & Q). rewrite <- Genv.find_funct_ptr_iff in Q. - econstructor; eauto. + econstructor; eauto. + simpl. red. rewrite H1. constructor; auto. Qed. Corollary eval_helper_1: - forall le id name sg arg1 varg1 vres, + forall bf le id name sg arg1 varg1 vres, eval_expr ge sp e m le arg1 varg1 -> helper_declared prog id name sg -> - external_implements name sg (varg1::nil) vres -> + lookup_builtin_function name sg = Some bf -> + builtin_function_sem bf (varg1 :: nil) = Some vres -> eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres. Proof. intros. eapply eval_helper; eauto. constructor; auto. constructor. Qed. Corollary eval_helper_2: - forall le id name sg arg1 arg2 varg1 varg2 vres, + forall bf le id name sg arg1 arg2 varg1 varg2 vres, eval_expr ge sp e m le arg1 varg1 -> eval_expr ge sp e m le arg2 varg2 -> helper_declared prog id name sg -> - external_implements name sg (varg1::varg2::nil) vres -> + lookup_builtin_function name sg = Some bf -> + builtin_function_sem bf (varg1 :: varg2 :: nil) = Some vres -> eval_expr ge sp e m le (Eexternal id sg (arg1 ::: arg2 ::: Enil)) vres. Proof. intros. eapply eval_helper; eauto. constructor; auto. constructor; auto. constructor. Qed. Remark eval_builtin_1: - forall le id sg arg1 varg1 vres, + forall bf le id sg arg1 varg1 vres, eval_expr ge sp e m le arg1 varg1 -> - builtin_implements id sg (varg1::nil) vres -> + lookup_builtin_function id sg = Some bf -> + builtin_function_sem bf (varg1 :: nil) = Some vres -> eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: Enil)) vres. Proof. - intros. econstructor. econstructor. eauto. constructor. apply H0. + intros. econstructor. econstructor. eauto. constructor. + simpl. red. rewrite H0. constructor. auto. Qed. Remark eval_builtin_2: - forall le id sg arg1 arg2 varg1 varg2 vres, + forall bf le id sg arg1 arg2 varg1 varg2 vres, eval_expr ge sp e m le arg1 varg1 -> eval_expr ge sp e m le arg2 varg2 -> - builtin_implements id sg (varg1::varg2::nil) vres -> + lookup_builtin_function id sg = Some bf -> + builtin_function_sem bf (varg1 :: varg2 :: nil) = Some vres -> eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: arg2 ::: Enil)) vres. Proof. - intros. econstructor. constructor; eauto. constructor; eauto. constructor. apply H1. + intros. econstructor. constructor; eauto. constructor; eauto. constructor. + simpl. red. rewrite H1. constructor. auto. Qed. Definition unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop := @@ -386,9 +364,10 @@ Qed. Theorem eval_negl: unary_constructor_sound negl Val.negl. Proof. unfold negl; red; intros. destruct (is_longconst a) eqn:E. - econstructor; split. apply eval_longconst. +- econstructor; split. apply eval_longconst. exploit is_longconst_sound; eauto. intros EQ; subst x. simpl. auto. - econstructor; split. eapply eval_builtin_1; eauto. UseHelper. auto. +- exists (Val.negl x); split; auto. + eapply (eval_builtin_1 (BI_standard BI_negl)); eauto. Qed. Theorem eval_notl: unary_constructor_sound notl Val.notl. @@ -410,7 +389,7 @@ Theorem eval_longoffloat: exists v, eval_expr ge sp e m le (longoffloat a) v /\ Val.lessdef y v. Proof. intros; unfold longoffloat. econstructor; split. - eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. + eapply (eval_helper_1 (BI_standard BI_i64_dtos)); eauto. DeclHelper. auto. auto. Qed. Theorem eval_longuoffloat: @@ -420,7 +399,7 @@ Theorem eval_longuoffloat: exists v, eval_expr ge sp e m le (longuoffloat a) v /\ Val.lessdef y v. Proof. intros; unfold longuoffloat. econstructor; split. - eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. + eapply (eval_helper_1 (BI_standard BI_i64_dtou)); eauto. DeclHelper. auto. auto. Qed. Theorem eval_floatoflong: @@ -429,8 +408,9 @@ Theorem eval_floatoflong: Val.floatoflong x = Some y -> exists v, eval_expr ge sp e m le (floatoflong a) v /\ Val.lessdef y v. Proof. - intros; unfold floatoflong. econstructor; split. - eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. + intros; unfold floatoflong. exists y; split; auto. + eapply (eval_helper_1 (BI_standard BI_i64_stod)); eauto. DeclHelper. auto. + simpl. destruct x; simpl in H0; inv H0; auto. Qed. Theorem eval_floatoflongu: @@ -439,8 +419,9 @@ Theorem eval_floatoflongu: Val.floatoflongu x = Some y -> exists v, eval_expr ge sp e m le (floatoflongu a) v /\ Val.lessdef y v. Proof. - intros; unfold floatoflongu. econstructor; split. - eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. + intros; unfold floatoflongu. exists y; split; auto. + eapply (eval_helper_1 (BI_standard BI_i64_utod)); eauto. DeclHelper. auto. + simpl. destruct x; simpl in H0; inv H0; auto. Qed. Theorem eval_longofsingle: @@ -477,8 +458,9 @@ Theorem eval_singleoflong: Val.singleoflong x = Some y -> exists v, eval_expr ge sp e m le (singleoflong a) v /\ Val.lessdef y v. Proof. - intros; unfold singleoflong. econstructor; split. - eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. + intros; unfold singleoflong. exists y; split; auto. + eapply (eval_helper_1 (BI_standard BI_i64_stof)); eauto. DeclHelper. auto. + simpl. destruct x; simpl in H0; inv H0; auto. Qed. Theorem eval_singleoflongu: @@ -487,8 +469,9 @@ Theorem eval_singleoflongu: Val.singleoflongu x = Some y -> exists v, eval_expr ge sp e m le (singleoflongu a) v /\ Val.lessdef y v. Proof. - intros; unfold singleoflongu. econstructor; split. - eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. + intros; unfold singleoflongu. exists y; split; auto. + eapply (eval_helper_1 (BI_standard BI_i64_utof)); eauto. DeclHelper. auto. + simpl. destruct x; simpl in H0; inv H0; auto. Qed. Theorem eval_andl: binary_constructor_sound andl Val.andl. @@ -615,7 +598,9 @@ Proof. simpl. erewrite <- Int64.decompose_shl_2. instantiate (1 := Int64.hiword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. + econstructor; split. + eapply eval_helper_2; eauto. EvalOp. DeclHelper. reflexivity. reflexivity. + auto. Qed. Theorem eval_shll: binary_constructor_sound shll Val.shll. @@ -626,7 +611,7 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shllimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. reflexivity. auto. Qed. Lemma eval_shrluimm: @@ -660,7 +645,9 @@ Proof. simpl. erewrite <- Int64.decompose_shru_2. instantiate (1 := Int64.loword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. + econstructor; split. + eapply eval_helper_2; eauto. EvalOp. DeclHelper. reflexivity. reflexivity. + auto. Qed. Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu. @@ -671,7 +658,7 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shrluimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. reflexivity. auto. Qed. Lemma eval_shrlimm: @@ -709,7 +696,9 @@ Proof. erewrite <- Int64.decompose_shr_2. instantiate (1 := Int64.loword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. + econstructor; split. + eapply eval_helper_2; eauto. EvalOp. DeclHelper. reflexivity. reflexivity. + auto. Qed. Theorem eval_shrl: binary_constructor_sound shrl Val.shrl. @@ -720,7 +709,7 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shrlimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. reflexivity. auto. Qed. Theorem eval_addl: Archi.ptr64 = false -> binary_constructor_sound addl Val.addl. @@ -730,7 +719,7 @@ Proof. assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.addl x y) v). { - econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. reflexivity. reflexivity. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -753,7 +742,7 @@ Proof. assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.subl x y) v). { - econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. reflexivity. reflexivity. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -784,7 +773,7 @@ Proof. exploit eval_add. eexact E2. eexact E3. intros [v5 [E5 L5]]. exploit eval_add. eexact E5. eexact E4. intros [v6 [E6 L6]]. exists (Val.longofwords v6 (Val.loword p)); split. - EvalOp. eapply eval_builtin_2; eauto. UseHelper. + EvalOp. eapply eval_builtin_2; eauto. reflexivity. reflexivity. intros. unfold le1, p in *; subst; simpl in *. inv L3. inv L4. inv L5. simpl in L6. inv L6. simpl. f_equal. symmetry. apply Int64.decompose_mul. @@ -832,14 +821,14 @@ Theorem eval_mullhu: forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)). Proof. unfold mullhu; intros; red; intros. econstructor; split; eauto. - eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. + eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper. reflexivity. reflexivity. Qed. Theorem eval_mullhs: forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)). Proof. unfold mullhs; intros; red; intros. econstructor; split; eauto. - eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. + eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper. reflexivity. reflexivity. Qed. Theorem eval_shrxlimm: @@ -881,7 +870,7 @@ Theorem eval_divlu_base: exists v, eval_expr ge sp e m le (divlu_base a b) v /\ Val.lessdef z v. Proof. intros; unfold divlu_base. - econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. eassumption. auto. Qed. Theorem eval_modlu_base: @@ -892,7 +881,7 @@ Theorem eval_modlu_base: exists v, eval_expr ge sp e m le (modlu_base a b) v /\ Val.lessdef z v. Proof. intros; unfold modlu_base. - econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. eassumption. auto. Qed. Theorem eval_divls_base: @@ -903,7 +892,7 @@ Theorem eval_divls_base: exists v, eval_expr ge sp e m le (divls_base a b) v /\ Val.lessdef z v. Proof. intros; unfold divls_base. - econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. eassumption. auto. Qed. Theorem eval_modls_base: @@ -914,7 +903,7 @@ Theorem eval_modls_base: exists v, eval_expr ge sp e m le (modls_base a b) v /\ Val.lessdef z v. Proof. intros; unfold modls_base. - econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. reflexivity. eassumption. auto. Qed. Remark decompose_cmpl_eq_zero: diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 7f5fe355..e6bf2129 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -16,7 +16,7 @@ Require Import FunInd. Require Import Axioms Classical. Require Import String Coqlib Decidableplus. Require Import Errors Maps Integers Floats. -Require Import AST Values Memory Events Globalenvs Determinism. +Require Import AST Values Memory Events Globalenvs Builtins Determinism. Require Import Ctypes Cop Csyntax Csem. Require Cstrategy. @@ -501,12 +501,19 @@ 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_builtin_or_external (name: string) (sg: signature) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match lookup_builtin_function name sg with + | Some bf => match builtin_function_sem bf vargs with Some v => Some(w, E0, v, m) | None => None end + | None => do_external_function name sg ge w vargs m + end. + Definition do_external (ef: external_function): world -> list val -> mem -> option (world * trace * val * mem) := match ef with | EF_external name sg => do_external_function name sg ge - | EF_builtin name sg => do_external_function name sg ge - | EF_runtime name sg => do_external_function name sg ge + | EF_builtin name sg => do_builtin_or_external name sg + | EF_runtime name sg => do_builtin_or_external name sg | EF_vload chunk => do_ef_volatile_load chunk | EF_vstore chunk => do_ef_volatile_store chunk | EF_malloc => do_ef_malloc @@ -523,17 +530,26 @@ Lemma do_ef_external_sound: do_external ef w vargs m = Some(w', t, vres, m') -> external_call ef ge vargs m t vres m' /\ possible_trace w t w'. Proof with try congruence. + intros until m'. assert (SIZE: forall v sz, do_alloc_size v = Some sz -> v = Vptrofs sz). { intros until sz; unfold Vptrofs; destruct v; simpl; destruct Archi.ptr64 eqn:SF; intros EQ; inv EQ; f_equal; symmetry; eauto with ptrofs. } - intros until m'. + assert (BF_EX: forall name sg, + do_builtin_or_external name sg w vargs m = Some (w', t, vres, m') -> + builtin_or_external_sem name sg ge vargs m t vres m' /\ possible_trace w t w'). + { unfold do_builtin_or_external, builtin_or_external_sem; intros. + destruct (lookup_builtin_function name sg ) as [bf|]. + - destruct (builtin_function_sem bf vargs) as [vres1|] eqn:BF; inv H. + split. constructor; auto. constructor. + - eapply do_external_function_sound; eauto. + } destruct ef; simpl. (* EF_external *) eapply do_external_function_sound; eauto. (* EF_builtin *) - eapply do_external_function_sound; eauto. + eapply BF_EX; eauto. (* EF_runtime *) - eapply do_external_function_sound; eauto. + eapply BF_EX; eauto. (* EF_vload *) unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... mydestr. destruct p as [[w'' t''] v]; mydestr. @@ -575,17 +591,26 @@ Lemma do_ef_external_complete: external_call ef ge vargs m t vres m' -> possible_trace w t w' -> do_external ef w vargs m = Some(w', t, vres, m'). Proof. + intros. assert (SIZE: forall n, do_alloc_size (Vptrofs n) = Some n). { unfold Vptrofs, do_alloc_size; intros; destruct Archi.ptr64 eqn:SF. rewrite Ptrofs.of_int64_to_int64; auto. rewrite Ptrofs.of_int_to_int; auto. } - intros. destruct ef; simpl in *. + assert (BF_EX: forall name sg, + builtin_or_external_sem name sg ge vargs m t vres m' -> + do_builtin_or_external name sg w vargs m = Some (w', t, vres, m')). + { unfold do_builtin_or_external, builtin_or_external_sem; intros. + destruct (lookup_builtin_function name sg) as [bf|]. + - inv H1. inv H0. rewrite H2. auto. + - eapply do_external_function_complete; eauto. + } + destruct ef; simpl in *. (* EF_external *) eapply do_external_function_complete; eauto. (* EF_builtin *) - eapply do_external_function_complete; eauto. + eapply BF_EX; eauto. (* EF_runtime *) - eapply do_external_function_complete; eauto. + eapply BF_EX; eauto. (* EF_vload *) inv H; unfold do_ef_volatile_load. exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto. 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. diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v new file mode 100644 index 00000000..f6e643d2 --- /dev/null +++ b/powerpc/Builtins1.v @@ -0,0 +1,33 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Platform-specific built-in functions *) + +Require Import String Coqlib. +Require Import AST Integers Floats Values. +Require Import Builtins0. + +Inductive platform_builtin : Type := . + +Local Open Scope string_scope. + +Definition platform_builtin_table : list (string * platform_builtin) := + nil. + +Definition platform_builtin_sig (b: platform_builtin) : signature := + match b with end. + +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := + match b with end. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 24aeb531..ba6612e8 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -38,11 +38,8 @@ Require Import Coqlib. Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. +Require Import AST Integers Floats Builtins. +Require Import Op CminorSel. Require Archi. Local Open Scope cminorsel_scope. @@ -566,3 +563,8 @@ Nondetfunction builtin_arg (e: expr) := | Eop Oadd (e1:::e2:::Enil) => BA_addptr (BA e1) (BA e2) | _ => BA e end. + +(** Platform-specific known builtins *) + +Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := + None. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 5d7cd52b..1f23f4bd 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -13,17 +13,10 @@ (** Correctness of instruction selection for operators *) Require Import Coqlib. -Require Import Maps. +Require Import AST Integers Floats. +Require Import Values Memory Builtins Globalenvs. +Require Import Cminor Op CminorSel. Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. Require Import SelectOp. Local Open Scope cminorsel_scope. @@ -1065,4 +1058,16 @@ Proof. - constructor; auto. Qed. +(** Platform-specific known builtins *) + +Theorem eval_platform_builtin: + forall bf al a vl v le, + platform_builtin bf al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem bf vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + intros. discriminate. +Qed. + End CMCONSTR. diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v new file mode 100644 index 00000000..f6e643d2 --- /dev/null +++ b/riscV/Builtins1.v @@ -0,0 +1,33 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Platform-specific built-in functions *) + +Require Import String Coqlib. +Require Import AST Integers Floats Values. +Require Import Builtins0. + +Inductive platform_builtin : Type := . + +Local Open Scope string_scope. + +Definition platform_builtin_table : list (string * platform_builtin) := + nil. + +Definition platform_builtin_sig (b: platform_builtin) : signature := + match b with end. + +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := + match b with end. diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index 760f06af..99806006 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -44,11 +44,8 @@ Require Archi. Require Import Coqlib. Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. +Require Import AST Integers Floats Builtins. +Require Import Op CminorSel. Local Open Scope cminorsel_scope. @@ -454,3 +451,8 @@ Nondetfunction builtin_arg (e: expr) := if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e | _ => BA e end. + +(** Platform-specific known builtins *) + +Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := + None. diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index d0e6979c..18bc5dfe 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -17,18 +17,10 @@ (** Correctness of instruction selection for operators *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Zbits. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. +Require Import Coqlib Zbits. +Require Import AST Integers Floats. +Require Import Values Memory Builtins Globalenvs. +Require Import Cminor Op CminorSel. Require Import SelectOp. Local Open Scope cminorsel_scope. @@ -937,4 +929,16 @@ Proof. - constructor; auto. Qed. +(** Platform-specific known builtins *) + +Theorem eval_platform_builtin: + forall bf al a vl v le, + platform_builtin bf al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem bf vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + intros. discriminate. +Qed. + End CMCONSTR. diff --git a/x86/Builtins1.v b/x86/Builtins1.v new file mode 100644 index 00000000..6103cc4c --- /dev/null +++ b/x86/Builtins1.v @@ -0,0 +1,54 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Platform-specific built-in functions *) + +Require Import String Coqlib. +Require Import AST Integers Floats Values. +Require Import Builtins0. + +Inductive platform_builtin : Type := + | BI_fmin + | BI_fmax. + +Local Open Scope string_scope. + +Definition platform_builtin_table : list (string * platform_builtin) := + ("__builtin_fmin", BI_fmin) + :: ("__builtin_fmax", BI_fmax) + :: nil. + +Definition platform_builtin_sig (b: platform_builtin) : signature := + match b with + | BI_fmin | BI_fmax => + mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default + end. + +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := + match b with + | BI_fmin => + mkbuiltin_n2t Tfloat Tfloat Tfloat + (fun f1 f2 => match Float.compare f1 f2 with + | Some Eq | Some Lt => f1 + | Some Gt | None => f2 + end) + | BI_fmax => + mkbuiltin_n2t Tfloat Tfloat Tfloat + (fun f1 f2 => match Float.compare f1 f2 with + | Some Eq | Some Gt => f1 + | Some Lt | None => f2 + end) + end. + diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index cf0f37ec..378590ce 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -38,7 +38,7 @@ Require Import Coqlib. Require Import Compopts. -Require Import AST Integers Floats. +Require Import AST Integers Floats Builtins. Require Import Op CminorSel. Local Open Scope cminorsel_scope. @@ -568,3 +568,8 @@ Nondetfunction builtin_arg (e: expr) := | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs | _ => BA e end. + +(** Platform-specific known builtins *) + +Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := + None. diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index b412ccf7..821a54e8 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -13,15 +13,9 @@ (** Correctness of instruction selection for operators *) Require Import Coqlib. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. +Require Import AST Integers Floats. +Require Import Values Memory Builtins Globalenvs. +Require Import Cminor Op CminorSel. Require Import SelectOp. Local Open Scope cminorsel_scope. @@ -1010,4 +1004,16 @@ Proof. - constructor; auto. Qed. +(** Platform-specific known builtins *) + +Theorem eval_platform_builtin: + forall bf al a vl v le, + platform_builtin bf al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem bf vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + intros. discriminate. +Qed. + End CMCONSTR. |