From ed0cfe4b38208f15763f2d1c0372c441a320ea56 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 17 Jun 2019 14:22:22 +0200 Subject: Extended asm: print register names according to their types When printing an extended asm code fragment, placeholders %n are replaced by register names. Currently we ignore the fact that some assemblers use different register names depending on the width of the data that resides in the register. For example, x86_64 uses %rax for a 64-bit quantity and %eax for a 32-bit quantity, but CompCert always prints %rax in extended asm statements. This is problematic if we want to use 32-bit integer instructions in extended asm, e.g. int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); produces addl %rax, %rdx which is syntactically incorrect. Another example is ARM FP registers: D0 is a double-precision float, but S0 is a single-precision float. This commit partially solves this issue by taking into account the Cminor type of the asm parameter when printing the corresponding register. Continuing the previous example, int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); now produces addl %eax, %edx This is not perfect yet: we use Cminor types, because this is all we have at hand, and not source C types, hence "char" and "short" parameters are still printed like "int" parameters, which is not good for x86. (I.e. we produce %eax where GCC might have produced %al or %ax.) We'll leave this issue open. --- backend/PrintAsmaux.ml | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) (limited to 'backend') diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 7e075f04..8652b2c5 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -245,14 +245,15 @@ let print_debug_info comment print_line preg_string sp_name oc kind txt args = (** Inline assembly *) -let print_asm_argument print_preg oc modifier = function - | BA r -> print_preg oc r +let print_asm_argument print_preg oc modifier typ = function + | BA r -> print_preg oc typ r | BA_splitlong(BA hi, BA lo) -> begin match modifier with - | "R" -> print_preg oc hi - | "Q" -> print_preg oc lo - | _ -> fprintf oc "%a:%a" print_preg hi print_preg lo - (* Probably not what was intended *) + | "R" -> print_preg oc Tint hi + | "Q" -> print_preg oc Tint lo + | _ -> print_preg oc Tint hi; fprintf oc ":"; print_preg oc Tint lo + (* This case (printing a split long in full) should never + happen because of the checks done in ExtendedAsm.ml *) end | _ -> failwith "bad asm argument" @@ -265,8 +266,10 @@ let re_asm_param_1 = Str.regexp "%%\\|%[QR]?[0-9]+" let re_asm_param_2 = Str.regexp "%\\([QR]?\\)\\([0-9]+\\)" let print_inline_asm print_preg oc txt sg args res = - let operands = - if sg.sig_res = None then args else builtin_arg_of_res res :: args in + let (operands, ty_operands) = + match sg.sig_res with + | None -> (args, sg.sig_args) + | Some tres -> (builtin_arg_of_res res :: args, tres :: sg.sig_args) in let print_fragment = function | Str.Text s -> output_string oc s @@ -277,7 +280,9 @@ let print_inline_asm print_preg oc txt sg args res = let modifier = Str.matched_group 1 s and number = int_of_string (Str.matched_group 2 s) in try - print_asm_argument print_preg oc modifier (List.nth operands number) + print_asm_argument print_preg oc modifier + (List.nth ty_operands number) + (List.nth operands number) with Failure _ -> fprintf oc "" s in List.iter print_fragment (Str.full_split re_asm_param_1 txt); -- cgit From ea6807fdaeaa2e46e1c7471c91056fdc4736cc2f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 5 Jul 2019 15:38:45 +0200 Subject: Rename option `-ffavor-branchless` into `-Obranchless` Easier to type, and consistent with `-Os` (optimize for smaller code / optimize for fewer conditional branches). --- backend/Selectionaux.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend') diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml index de8127c6..4ca7dd21 100644 --- a/backend/Selectionaux.ml +++ b/backend/Selectionaux.ml @@ -80,10 +80,10 @@ let fast_cmove ty = assert false (* The if-conversion heuristic depend on the - -fif-conversion and -ffavor-branchless flags. + -fif-conversion and -Obranchless flags. With [-fno-if-conversion] or [-0O], if-conversion is turned off entirely. -With [-ffavor-branchless], if-conversion is performed whenever semantically +With [-Obranchless], if-conversion is performed whenever semantically correct, regardless of how much it could cost. Otherwise (and by default), optimization is performed when it seems beneficial. @@ -106,7 +106,7 @@ instructions from the first branch. let if_conversion_heuristic cond ifso ifnot ty = if not !Clflags.option_fifconversion then false else - if !Clflags.option_ffavor_branchless then true else + if !Clflags.option_Obranchless then true else if not (fast_cmove ty) then false else let c1 = cost_expr ifso and c2 = cost_expr ifnot in c1 + c2 <= 24 && abs (c1 - c2) <= 8 -- cgit From 96383f6dbccd4b280acad395b9a2683a645a9de3 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 8 Jul 2019 10:48:24 +0200 Subject: Compatibility with OCaml 4.08 (#302) * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300 --- backend/Linearizeaux.ml | 2 +- backend/PrintAsm.ml | 3 +-- backend/PrintCminor.ml | 2 +- backend/PrintLTL.ml | 2 +- backend/PrintRTL.ml | 2 +- backend/PrintXTL.ml | 2 +- 6 files changed, 6 insertions(+), 7 deletions(-) (limited to 'backend') diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 46d5c3f1..902724e0 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -106,7 +106,7 @@ let flatten_blocks blks = let cmp_minpc (mpc1, _) (mpc2, _) = if mpc1 = mpc2 then 0 else if mpc1 > mpc2 then -1 else 1 in - List.flatten (List.map Pervasives.snd (List.sort cmp_minpc blks)) + List.flatten (List.map snd (List.sort cmp_minpc blks)) (* Build the enumeration *) diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index dd428808..155f5e55 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -13,7 +13,6 @@ open AST open Camlcoq -open DwarfPrinter open PrintAsmaux open Printf open Sections @@ -177,7 +176,7 @@ module Printer(Target:TARGET) = let address = Target.address end - module DebugPrinter = DwarfPrinter (DwarfTarget) + module DebugPrinter = DwarfPrinter.DwarfPrinter (DwarfTarget) end let print_program oc p = diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index f68c1267..8c255a65 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -16,7 +16,7 @@ (** Pretty-printer for Cminor *) open Format -open Camlcoq +open !Camlcoq open Integers open AST open PrintAST diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index d0557073..1c449e74 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -112,7 +112,7 @@ let print_function pp id f = fprintf pp "%s() {\n" (extern_atom id); let instrs = List.sort - (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) (List.rev_map (fun (pc, i) -> (P.to_int pc, i)) (PTree.elements f.fn_code)) in diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index ba336b0a..841540b6 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -93,7 +93,7 @@ let print_function pp id f = fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; let instrs = List.sort - (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) (List.rev_map (fun (pc, i) -> (P.to_int pc, i)) (PTree.elements f.fn_code)) in diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml index cc1f7d49..6432682a 100644 --- a/backend/PrintXTL.ml +++ b/backend/PrintXTL.ml @@ -138,7 +138,7 @@ let print_function pp ?alloc ?live f = fprintf pp "f() {\n"; let instrs = List.sort - (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) (List.map (fun (pc, i) -> (P.to_int pc, i)) (PTree.elements f.fn_code)) in -- cgit From d08b080747225160b80c3f04bdfd9cd67550b425 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 2 Jul 2019 16:25:40 +0200 Subject: Give formal semantics to some built-in functions and run-time functions This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later. --- backend/Selection.v | 53 ++++++++++++++-- backend/Selectionproof.v | 157 +++++++++++++++++++++++++++++++++++++---------- backend/SplitLongproof.v | 133 ++++++++++++++++++--------------------- 3 files changed, 231 insertions(+), 112 deletions(-) (limited to 'backend') 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: -- cgit From e16b34d9fc1aa7854759787fd52ad59c964c2d4b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 3 Jul 2019 11:06:07 +0200 Subject: Perform constant propagation for known built-in functions When an external function is a known built-in function and it is applied to compile-time integer or FP constants, we can use the known semantics of the builtin to compute the result at compile-time. --- backend/Constprop.v | 44 ++++++++++++++++++++++++++++++++++++++-- backend/Constpropproof.v | 44 ++++++++++++++++++++++++++++++---------- backend/ValueAnalysis.v | 52 +++++++++++++++++++++++++++++++++++++++++++++++- backend/ValueDomain.v | 44 ++++++++++++++++++++++++++++++++++++++-- 4 files changed, 168 insertions(+), 16 deletions(-) (limited to 'backend') diff --git a/backend/Constprop.v b/backend/Constprop.v index d8211ffe..4aab7677 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -15,7 +15,7 @@ and the corresponding code rewriting. *) Require Import Coqlib Maps Integers Floats Lattice Kildall. -Require Import AST Linking. +Require Import AST Linking Builtins. Require Compopts Machregs. Require Import Op Registers RTL. Require Import Liveness ValueDomain ValueAOp ValueAnalysis. @@ -139,6 +139,30 @@ Definition builtin_strength_reduction | _ => builtin_args_strength_reduction ae al (Machregs.builtin_constraints ef) end. +(* +Definition transf_builtin + (ae: AE.t) (am: amem) (rm: romem) + (ef: external_function) + (args: list (builtin_arg reg)) (res: builtin_res reg) (s: node) := + let dfl := Ibuiltin ef (builtin_strength_reduction ae ef args) res s in + match ef, res with + | EF_builtin name sg, BR rd => + match lookup_builtin_function name sg with + | Some bf => + match eval_static_builtin_function ae am rm bf args with + | Some a => + match const_for_result a with + | Some cop => Iop cop nil rd s + | None => dfl + end + | None => dfl + end + | None => dfl + end + | _, _ => dfl + end. +*) + Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) (pc: node) (instr: instruction) := match an!!pc with @@ -176,7 +200,23 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) | Itailcall sig ros args => Itailcall sig (transf_ros ae ros) args | Ibuiltin ef args res s => - Ibuiltin ef (builtin_strength_reduction ae ef args) res s + let dfl := Ibuiltin ef (builtin_strength_reduction ae ef args) res s in + match ef, res with + | EF_builtin name sg, BR rd => + match lookup_builtin_function name sg with + | Some bf => + match eval_static_builtin_function ae am rm bf args with + | Some a => + match const_for_result a with + | Some cop => Iop cop nil rd s + | None => dfl + end + | None => dfl + end + | None => dfl + end + | _, _ => dfl + end | Icond cond args s1 s2 => let aargs := aregs ae args in match resolve_branch (eval_static_condition cond aargs) with diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index e28519ca..a5d08a0f 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -14,7 +14,7 @@ Require Import Coqlib Maps Integers Floats Lattice Kildall. Require Import AST Linking. -Require Import Values Events Memory Globalenvs Smallstep. +Require Import Values Builtins Events Memory Globalenvs Smallstep. Require Compopts Machregs. Require Import Op Registers RTL. Require Import Liveness ValueDomain ValueAOp ValueAnalysis. @@ -474,19 +474,41 @@ Proof. - (* Ibuiltin *) rename pc'0 into pc. TransfInstr; intros. Opaque builtin_strength_reduction. - exploit builtin_strength_reduction_correct; eauto. intros (vargs' & P & Q). - exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)). + set (dfl := Ibuiltin ef (builtin_strength_reduction ae ef args) res pc') in *. + set (rm := romem_for cu) in *. + assert (DFL: (fn_code (transf_function rm f))!pc = Some dfl -> + exists (n2 : nat) (s2' : state), + step tge + (State s' (transf_function rm f) (Vptr sp0 Ptrofs.zero) pc rs' m'0) t s2' /\ + match_states n2 + (State s f (Vptr sp0 Ptrofs.zero) pc' (regmap_setres res vres rs) m') s2'). + { + exploit builtin_strength_reduction_correct; eauto. intros (vargs' & P & Q). + exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)). apply REGS. eauto. eexact P. - intros (vargs'' & U & V). - exploit external_call_mem_extends; eauto. - intros [v' [m2' [A [B [C D]]]]]. + intros (vargs'' & U & V). + exploit external_call_mem_extends; eauto. + intros (v' & m2' & A & B & C & D). + econstructor; econstructor; split. + eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_preserved. eexact symbols_preserved. eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + eapply match_states_succ; eauto. + apply set_res_lessdef; auto. + } + destruct ef; auto. + destruct res; auto. + destruct (lookup_builtin_function name sg) as [bf|] eqn:LK; auto. + destruct (eval_static_builtin_function ae am rm bf args) as [a|] eqn:ES; auto. + destruct (const_for_result a) as [cop|] eqn:CR; auto. + clear DFL. simpl in H1; red in H1; rewrite LK in H1; inv H1. + exploit const_for_result_correct; eauto. + eapply eval_static_builtin_function_sound; eauto. + intros (v' & A & B). left; econstructor; econstructor; split. - eapply exec_Ibuiltin; eauto. - eapply eval_builtin_args_preserved. eexact symbols_preserved. eauto. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. + eapply exec_Iop; eauto. eapply match_states_succ; eauto. - apply set_res_lessdef; auto. - + apply set_reg_lessdef; auto. - (* Icond, preserved *) rename pc'0 into pc. TransfInstr. set (ac := eval_static_condition cond (aregs ae args)). diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 1f80c293..8dbb67a7 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -13,7 +13,7 @@ Require Import FunInd. Require Import Coqlib Maps Integers Floats Lattice Kildall. Require Import Compopts AST Linking. -Require Import Values Memory Globalenvs Events. +Require Import Values Memory Globalenvs Builtins Events. Require Import Registers Op RTL. Require Import ValueDomain ValueAOp Liveness. @@ -78,6 +78,15 @@ Definition transfer_builtin_default let (av, am') := analyze_call am (map (abuiltin_arg ae am rm) args) in VA.State (set_builtin_res res av ae) am'. +Definition eval_static_builtin_function + (ae: aenv) (am: amem) (rm: romem) + (bf: builtin_function) (args: list (builtin_arg reg)) := + match builtin_function_sem bf + (map val_of_aval (map (abuiltin_arg ae am rm) args)) with + | Some v => aval_of_val v + | None => None + end. + Definition transfer_builtin (ae: aenv) (am: amem) (rm: romem) (ef: external_function) (args: list (builtin_arg reg)) (res: builtin_res reg) := @@ -105,6 +114,15 @@ Definition transfer_builtin | EF_annot_val _ _ _, v :: nil => let av := abuiltin_arg ae am rm v in VA.State (set_builtin_res res av ae) am + | EF_builtin name sg, _ => + match lookup_builtin_function name sg with + | Some bf => + match eval_static_builtin_function ae am rm bf args with + | Some av => VA.State (set_builtin_res res av ae) am + | None => transfer_builtin_default ae am rm args res + end + | None => transfer_builtin_default ae am rm args res + end | _, _ => transfer_builtin_default ae am rm args res end. @@ -372,6 +390,31 @@ Proof. intros. destruct res; simpl; auto. apply ematch_update; auto. Qed. +Lemma eval_static_builtin_function_sound: + forall bc ge rs sp m ae rm am (bf: builtin_function) al vl v va, + ematch bc rs ae -> + romatch bc m rm -> + mmatch bc m am -> + genv_match bc ge -> + bc sp = BCstack -> + eval_builtin_args ge (fun r => rs#r) (Vptr sp Ptrofs.zero) m al vl -> + eval_static_builtin_function ae am rm bf al = Some va -> + builtin_function_sem bf vl = Some v -> + vmatch bc v va. +Proof. + unfold eval_static_builtin_function; intros. + exploit abuiltin_args_sound; eauto. + set (vla := map (abuiltin_arg ae am rm) al) in *. intros VMA. + destruct (builtin_function_sem bf (map val_of_aval vla)) as [v0|] eqn:A; try discriminate. + assert (LD: Val.lessdef v0 v). + { apply val_inject_lessdef. + exploit (bs_inject _ (builtin_function_sem bf)). + apply val_inject_list_lessdef. eapply list_val_of_aval_sound; eauto. + rewrite A, H6; simpl. auto. + } + inv LD. apply aval_of_val_sound; auto. discriminate. +Qed. + (** ** Constructing block classifications *) Definition bc_nostack (bc: block_classification) : Prop := @@ -1343,6 +1386,13 @@ Proof. } unfold transfer_builtin in TR. destruct ef; auto. ++ (* builtin function *) + destruct (lookup_builtin_function name sg) as [bf|] eqn:LK; auto. + destruct (eval_static_builtin_function ae am rm bf args) as [av|] eqn:ES; auto. + simpl in H1. red in H1. rewrite LK in H1. inv H1. + eapply sound_succ_state; eauto. simpl; auto. + apply set_builtin_res_sound; auto. + eapply eval_static_builtin_function_sound; eauto. + (* volatile load *) inv H0; auto. inv H3; auto. inv H1. exploit abuiltin_arg_sound; eauto. intros VM1. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index f6afa836..fd3bd5ae 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -13,7 +13,7 @@ Require Import FunInd. Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice. Require Import Compopts AST. -Require Import Values Memory Globalenvs Events. +Require Import Values Memory Globalenvs Builtins Events. Require Import Registers RTL. (** The abstract domains for value analysis *) @@ -3038,7 +3038,47 @@ Proof with (auto using provenance_monotone with va). - destruct (zlt n 16)... Qed. -(** Abstracting memory blocks *) +(** Analysis of known builtin functions. All we have is a dynamic semantics + as a function [list val -> option val], but we can still perform + some constant propagation. *) + +Definition val_of_aval (a: aval) : val := + match a with + | I n => Vint n + | L n => Vlong n + | F f => Vfloat f + | FS f => Vsingle f + | _ => Vundef + end. + +Definition aval_of_val (v: val) : option aval := + match v with + | Vint n => Some (I n) + | Vlong n => Some (L n) + | Vfloat f => Some (F f) + | Vsingle f => Some (FS f) + | _ => None + end. + +Lemma val_of_aval_sound: + forall v a, vmatch v a -> Val.lessdef (val_of_aval a) v. +Proof. + destruct 1; simpl; auto. +Qed. + +Corollary list_val_of_aval_sound: + forall vl al, list_forall2 vmatch vl al -> Val.lessdef_list (map val_of_aval al) vl. +Proof. + induction 1; simpl; constructor; auto using val_of_aval_sound. +Qed. + +Lemma aval_of_val_sound: + forall v a, aval_of_val v = Some a -> vmatch v a. +Proof. + intros v a E; destruct v; simpl in E; inv E; constructor. +Qed. + +(** * Abstracting memory blocks *) Inductive acontent : Type := | ACval (chunk: memory_chunk) (av: aval). -- cgit From 10aa130361a5a673a14a7b38ed9c077103f9155f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 3 Jul 2019 19:08:18 +0200 Subject: Improve CSE for known built-in functions Known built-in functions are guaranteed not to change memory. --- backend/CSE.v | 15 ++++++++++----- backend/CSEproof.v | 6 ++++-- 2 files changed, 14 insertions(+), 7 deletions(-) (limited to 'backend') diff --git a/backend/CSE.v b/backend/CSE.v index 6d3f6f33..ecfa1f9e 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -14,7 +14,7 @@ proceeds by value numbering over extended basic blocks. *) Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. -Require Import AST Linking. +Require Import AST Linking Builtins. Require Import Values Memory. Require Import Op Registers RTL. Require Import ValueDomain ValueAnalysis CSEdomain CombineOp. @@ -444,10 +444,10 @@ Module Solver := BBlock_solver(Numbering). ([EF_external], [EF_runtime], [EF_malloc], [EF_free]). - Forget equations involving loads but keep equations over registers. This is appropriate for builtins that can modify memory, - e.g. volatile stores, or [EF_builtin] + e.g. volatile stores, or [EF_builtin] for unknown builtin functions. - Keep all equations, taking advantage of the fact that neither memory - nor registers are modified. This is appropriate for annotations - and for volatile loads. + nor registers are modified. This is appropriate for annotations, + volatile loads, and known builtin functions. *) Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numbering) := @@ -473,8 +473,13 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb match ef with | EF_external _ _ | EF_runtime _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ => empty_numbering - | EF_builtin _ _ | EF_vstore _ => + | EF_vstore _ => set_res_unknown (kill_all_loads before) res + | EF_builtin name sg => + match lookup_builtin_function name sg with + | Some bf => set_res_unknown before res + | None => set_res_unknown (kill_all_loads before) res + end | EF_memcpy sz al => match args with | dst :: src :: nil => diff --git a/backend/CSEproof.v b/backend/CSEproof.v index a60c316b..03c7ecfc 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -14,7 +14,7 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. -Require Import Values Memory Events Globalenvs Smallstep. +Require Import Values Memory Builtins Events Globalenvs Smallstep. Require Import Op Registers RTL. Require Import ValueDomain ValueAOp ValueAnalysis. Require Import CSEdomain CombineOp CombineOpproof CSE. @@ -1129,7 +1129,9 @@ Proof. { exists valu. apply set_res_unknown_holds. eapply kill_all_loads_hold; eauto. } destruct ef. + apply CASE1. - + apply CASE3. + + destruct (lookup_builtin_function name sg) as [bf|] eqn:LK. + ++ apply CASE2. simpl in H1; red in H1; rewrite LK in H1; inv H1. auto. + ++ apply CASE3. + apply CASE1. + apply CASE2; inv H1; auto. + apply CASE3. -- cgit