aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/CminorSel.v8
-rw-r--r--backend/RTLgen.v4
-rw-r--r--backend/RTLgenaux.ml2
-rw-r--r--backend/RTLgenproof.v4
-rw-r--r--backend/RTLgenspec.v4
-rw-r--r--backend/Selection.v41
-rw-r--r--backend/Selectionproof.v6
-rw-r--r--backend/SplitLong.vp5
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))).
generated by cgit (git 2.34.1) at 2024-06-12 00:20:59 +0000