diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-07 23:33:53 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-07 23:33:53 +0200 |
commit | 952a5faf13280e9bed6fe10670561d7e4fe5bc19 (patch) | |
tree | 7c2bfd73048aa6e7bd991ab25281201d77c70799 /backend | |
parent | 3b15828ca868365b285ba611ba72177e90d0061b (diff) | |
download | compcert-kvx-952a5faf13280e9bed6fe10670561d7e4fe5bc19.tar.gz compcert-kvx-952a5faf13280e9bed6fe10670561d7e4fe5bc19.zip |
__builtin_expect seems to work
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CminorSel.v | 8 | ||||
-rw-r--r-- | backend/RTLgen.v | 4 | ||||
-rw-r--r-- | backend/RTLgenaux.ml | 2 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 4 | ||||
-rw-r--r-- | backend/RTLgenspec.v | 4 | ||||
-rw-r--r-- | backend/Selection.v | 41 | ||||
-rw-r--r-- | backend/Selectionproof.v | 6 | ||||
-rw-r--r-- | backend/SplitLong.vp | 5 |
8 files changed, 47 insertions, 27 deletions
diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 96cb8ae6..26f47e23 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -50,7 +50,7 @@ with exprlist : Type := | Econs: expr -> exprlist -> exprlist with condexpr : Type := - | CEcond : condition -> exprlist -> condexpr + | CEcond : condition -> option bool -> exprlist -> condexpr | CEcondition : condexpr -> condexpr -> condexpr -> condexpr | CElet: expr -> condexpr -> condexpr. @@ -207,10 +207,10 @@ with eval_exprlist: letenv -> exprlist -> list val -> Prop := eval_exprlist le (Econs a1 al) (v1 :: vl) with eval_condexpr: letenv -> condexpr -> bool -> Prop := - | eval_CEcond: forall le cond al vl vb, + | eval_CEcond: forall le cond expected al vl vb, eval_exprlist le al vl -> eval_condition cond vl m = Some vb -> - eval_condexpr le (CEcond cond al) vb + eval_condexpr le (CEcond cond expected al) vb | eval_CEcondition: forall le a b c va v, eval_condexpr le a va -> eval_condexpr le (if va then b else c) v -> @@ -495,7 +495,7 @@ with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist := with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr := match a with - | CEcond c al => CEcond c (lift_exprlist p al) + | CEcond c expected al => CEcond c expected (lift_exprlist p al) | CEcondition a b c => CEcondition (lift_condexpr p a) (lift_condexpr p b) (lift_condexpr p c) | CElet a b => CElet (lift_expr p a) (lift_condexpr (S p) b) end. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index ac98f3a1..243d7b7c 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -477,9 +477,9 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node) with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) {struct a} : mon node := match a with - | CEcond c al => + | CEcond c expected al => do rl <- alloc_regs map al; - do nt <- add_instr (Icond c rl ntrue nfalse None); + do nt <- add_instr (Icond c rl ntrue nfalse expected); transl_exprlist map al rl nt | CEcondition a b c => do nc <- transl_condexpr map c ntrue nfalse; diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index e39d3b56..26688e23 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -41,7 +41,7 @@ and size_exprs = function | Econs(e1, el) -> size_expr e1 + size_exprs el and size_condexpr = function - | CEcond(c, args) -> size_exprs args + | CEcond(c, expected, args) -> size_exprs args | CEcondition(c1, c2, c3) -> 1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3 | CElet(a, c) -> diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index b94ec22f..e62aff22 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -799,11 +799,11 @@ Proof. Qed. Lemma transl_condexpr_CEcond_correct: - forall le cond al vl vb, + forall le cond expected al vl vb, eval_exprlist ge sp e m le al vl -> transl_exprlist_prop le al vl -> eval_condition cond vl m = Some vb -> - transl_condexpr_prop le (CEcond cond al) vb. + transl_condexpr_prop le (CEcond cond expected al) vb. Proof. intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 30ad7d82..36b8409d 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -744,10 +744,10 @@ Inductive tr_expr (c: code): with tr_condition (c: code): mapping -> list reg -> condexpr -> node -> node -> node -> Prop := - | tr_CEcond: forall map pr cond bl ns ntrue nfalse n1 rl i, + | tr_CEcond: forall map pr cond expected bl ns ntrue nfalse n1 rl i, tr_exprlist c map pr bl ns n1 rl -> c!n1 = Some (Icond cond rl ntrue nfalse i) -> - tr_condition c map pr (CEcond cond bl) ns ntrue nfalse + tr_condition c map pr (CEcond cond expected bl) ns ntrue nfalse | tr_CEcondition: forall map pr a1 a2 a3 ns ntrue nfalse n2 n3, tr_condition c map pr a1 ns n2 n3 -> tr_condition c map pr a2 n2 ntrue nfalse -> diff --git a/backend/Selection.v b/backend/Selection.v index fcb14127..342bd8ca 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -35,12 +35,13 @@ Local Open Scope error_monad_scope. (** Conversion of conditions *) -Function condexpr_of_expr (e: expr) : condexpr := +Function condexpr_of_expr (e: expr) (expected : option bool) : condexpr := match e with - | Eop (Ocmp c) el => CEcond c el - | Econdition a b c => CEcondition a (condexpr_of_expr b) (condexpr_of_expr c) - | Elet a b => CElet a (condexpr_of_expr b) - | _ => CEcond (Ccompuimm Cne Int.zero) (e ::: Enil) + | Eop (Ocmp c) el => CEcond c expected el + | Econdition a b c => CEcondition a (condexpr_of_expr b expected) + (condexpr_of_expr c expected) + | Elet a b => CElet a (condexpr_of_expr b expected) + | _ => CEcond (Ccompuimm Cne Int.zero) expected (e ::: Enil) end. Function condition_of_expr (e: expr) : condition * exprlist := @@ -167,7 +168,7 @@ 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 + | None => Econdition (condexpr_of_expr cnd None) ifso ifnot end. (** Conversion from Cminor expression to Cminorsel expressions *) @@ -293,16 +294,16 @@ Fixpoint sel_switch (arg: nat) (t: comptree): exitexpr := | CTaction act => XEexit act | CTifeq key act t' => - XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key)) + XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key) None) (XEexit act) (sel_switch arg t') | CTiflt key t1 t2 => - XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key)) + XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key) None) (sel_switch arg t1) (sel_switch arg t2) | CTjumptable ofs sz tbl t' => XElet (make_sub (Eletvar arg) ofs) - (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz)) + (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz) None) (XEjumptable (make_to_int (Eletvar O)) tbl) (sel_switch (S arg) t')) end. @@ -377,6 +378,22 @@ Definition if_conversion | _, _ => None end. +Definition extract_expect1 (e : Cminor.expr) : option bool := + match e with + | Cminor.Ebinop (Cminor.Oexpect ty) e1 (Cminor.Econst (Cminor.Ointconst c)) => + Some (if Int.eq_dec c Int.zero then false else true) + | Cminor.Ebinop (Cminor.Oexpect ty) e1 (Cminor.Econst (Cminor.Olongconst c)) => + Some (if Int64.eq_dec c Int64.zero then false else true) + | _ => None + end. + +Definition extract_expect (e : Cminor.expr) : option bool := + match e with + | Cminor.Ebinop (Cminor.Ocmpu Cne) e1 (Cminor.Econst (Cminor.Ointconst c)) => + if Int.eq_dec c Int.zero then extract_expect1 e1 else None + | _ => extract_expect1 e + end. + (** Conversion from Cminor statements to Cminorsel statements. *) Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt := @@ -404,8 +421,10 @@ Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt : match if_conversion ki env e ifso ifnot with | Some s => OK s | None => - do ifso' <- sel_stmt ki env ifso; do ifnot' <- sel_stmt ki env ifnot; - OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot') + do ifso' <- sel_stmt ki env ifso; + do ifnot' <- sel_stmt ki env ifnot; + OK (Sifthenelse (condexpr_of_expr (sel_expr e) + (extract_expect e)) ifso' ifnot') end | Cminor.Sloop body => do body' <- sel_stmt ki env body; OK (Sloop body') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 53600c7a..955c45a4 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -196,12 +196,12 @@ Variable e: env. Variable m: mem. Lemma eval_condexpr_of_expr: - forall a le v b, + forall expected a le v b, eval_expr tge sp e m le a v -> Val.bool_of_val v b -> - eval_condexpr tge sp e m le (condexpr_of_expr a) b. + eval_condexpr tge sp e m le (condexpr_of_expr a expected) b. Proof. - intros until a. functional induction (condexpr_of_expr a); intros. + intros until a. functional induction (condexpr_of_expr a expected); intros. (* compare *) inv H. econstructor; eauto. simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto. diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index dfe42df0..0f240602 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +(* FIXME: expected branching information not propagated *) (** Instruction selection for 64-bit integer operations *) Require String. @@ -256,7 +257,7 @@ Definition cmpl_ne_zero (e: expr) := Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil)) (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))). @@ -278,7 +279,7 @@ Definition cmplu (c: comparison) (e1 e2: expr) := Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil)) (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))). |