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