From 0d98d7fec937d3a9a2324f1731b041cfbf16dcbe Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 30 Mar 2021 10:11:01 +0200 Subject: Refactoring the mayundef OP to be more general... --- riscV/NeedOp.v | 2 - riscV/Op.v | 109 ++++++++++-------------- riscV/PrintOp.ml | 10 ++- riscV/RTLpathSE_simplify.v | 204 ++++++++++++++++++++++++++------------------- riscV/ValueAOp.v | 67 +++++---------- 5 files changed, 191 insertions(+), 201 deletions(-) (limited to 'riscV') diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 4ed9868c..cfadea37 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -117,8 +117,6 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEoril _ => op1 (default nv) | OEloadli _ => op1 (default nv) | OEmayundef _ => op2 (default nv) - | OEshrxundef _ => op2 (default nv) - | OEshrxlundef _ => op2 (default nv) | OEfeqd => op2 (default nv) | OEfltd => op2 (default nv) | OEfled => op2 (default nv) diff --git a/riscV/Op.v b/riscV/Op.v index 0569676a..b8835c61 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -69,6 +69,13 @@ Inductive condition : Type := | CEbgel (optR0: option bool) (**r branch-if-greater-or-equal signed *) | CEbgeul (optR0: option bool). (**r branch-if-greater-or-equal unsigned *) +(* This type will define the eval function of a OEmayundef operation. *) +Inductive mayundef: Type := + | MUint: mayundef + | MUlong: mayundef + | MUshrx: int -> mayundef + | MUshrxl: int -> mayundef. + (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -201,9 +208,7 @@ Inductive operation : Type := | OExoril (n: int64) (**r xor immediate *) | OEluil (n: int64) (**r load upper-immediate *) | OEloadli (n: int64) (**r load an immediate int64 *) - | OEmayundef (is_long: bool) - | OEshrxundef (n: int) - | OEshrxlundef (n: int) + | OEmayundef (mu: mayundef) | OEfeqd (**r compare equal *) | OEfltd (**r compare less-than *) | OEfled (**r compare less-than/equal *) @@ -242,9 +247,9 @@ Defined. Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec; intros. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec Val.eq; intros. decide equality. - all: destruct optR0, optR1; decide equality. + all: try destruct optR0, optR1; try decide equality. Defined. (* Alternate definition: @@ -271,42 +276,28 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 v | Some false => sem v1 vz end. -Definition may_undef_int (is_long: bool) (v1 v2: val): val := - if negb is_long then - match v1 with - | Vint _ => v2 - | _ => Vundef - end - else - match v1 with - | Vlong _ => v2 - | _ => Vundef - end. - -Definition shrx_imm_undef (v1 v2: val): val := - match v1 with - | Vint n1 => - match v2 with - | Vint n2 => - if Int.ltu n2 (Int.repr 31) - then Vint n1 - else Vundef +Definition eval_may_undef (mu: mayundef) (v1 v2: val): val := + match mu with + | MUint => match v1 with + | Vint _ => v2 + | _ => Vundef + end + | MUlong => match v1 with + | Vlong _ => v2 + | _ => Vundef + end + | MUshrx i => + match v1 with + | Vint _ => + if Int.ltu i (Int.repr 31) then v1 else Vundef | _ => Vundef end - | _ => Vundef - end. - -Definition shrxl_imm_undef (v1 v2: val): val := - match v1 with - | Vlong n1 => - match v2 with - | Vint n2 => - if Int.ltu n2 (Int.repr 63) - then Vlong n1 - else Vundef + | MUshrxl i => + match v1 with + | Vlong _ => + if Int.ltu i (Int.repr 63) then v1 else Vundef | _ => Vundef end - | _ => Vundef end. (** * Evaluation functions *) @@ -481,9 +472,7 @@ Definition eval_operation | OEandil n, v1::nil => Some (Val.andl (Vlong n) v1) | OEoril n, v1::nil => Some (Val.orl (Vlong n) v1) | OEloadli n, nil => Some (Vlong n) - | OEmayundef is_long, v1::v2::nil => Some (may_undef_int is_long v1 v2) - | OEshrxundef n, v1::nil => Some (shrx_imm_undef v1 (Vint n)) - | OEshrxlundef n, v1::nil => Some (shrxl_imm_undef v1 (Vint n)) + | OEmayundef mu, v1 :: v2 :: nil => Some (eval_may_undef mu v1 v2) | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2) | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2) | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2) @@ -693,8 +682,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEaddilr0 _ => (nil, Tlong) | OEloadli _ => (nil, Tlong) | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64) - | OEshrxundef _ => (Tint :: nil, Tint) - | OEshrxlundef _ => (Tlong :: nil, Tlong) | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) | OEfltd => (Tfloat :: Tfloat :: nil, Tint) | OEfled => (Tfloat :: Tfloat :: nil, Tint) @@ -736,6 +723,14 @@ Proof. intros. unfold Val.has_type, Val.addl. destruct Archi.ptr64, v1, v2; auto. Qed. +Remark type_mayundef: + forall mu v1 v2, Val.has_type (eval_may_undef mu v1 v2) Tany64. +Proof. + intros. unfold eval_may_undef. + destruct mu eqn:EQMU, v1, v2; simpl; auto. + all: destruct Int.ltu; simpl; auto. +Qed. + Lemma type_of_operation_sound: forall op vl sp v m, op <> Omove -> @@ -946,8 +941,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OExoriw *) - destruct v0... (* OEluiw *) - - unfold may_undef_int; - destruct (Int.ltu _ _); cbn; trivial. + - destruct (Int.ltu _ _); cbn; trivial. (* OEseql *) - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... @@ -986,16 +980,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEloadli *) - trivial. (* OEmayundef *) - - unfold may_undef_int; - destruct is_long, v0, v1; simpl; trivial. - (* OEshrxundef *) - - unfold shrx_imm_undef; - destruct v0; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. - (* OEshrxlundef *) - - unfold shrxl_imm_undef; - destruct v0; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + - apply type_mayundef. (* OEfeqd *) - destruct v0; destruct v1; cbn; auto. destruct Float.cmp; cbn; auto. @@ -1721,7 +1706,7 @@ Proof. (* shru, shruimm *) - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. - (* shrx *) + (* shrx *) - inv H4; cbn; try apply Val.val_inject_undef. destruct (Int.ltu n (Int.repr 63)); cbn. apply Val.inject_long. @@ -1851,17 +1836,9 @@ Proof. (* OExoril *) - inv H4; simpl; auto. (* OEmayundef *) - - destruct is_long; inv H4; inv H2; - unfold may_undef_int; simpl; auto; - eapply Val.inject_ptr; eauto. - (* OEshrxundef *) - - inv H4; - unfold shrx_imm_undef; simpl; auto. - destruct (Int.ltu _ _); auto. - (* OEshrxlundef *) - - inv H4; - unfold shrxl_imm_undef; simpl; auto. - destruct (Int.ltu _ _); auto. + - destruct mu; inv H4; inv H2; simpl; auto; + try destruct (Int.ltu _ _); simpl; auto. + all: eapply Val.inject_ptr; eauto. (* OEfeqd *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index 4494080e..3a775c20 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -30,6 +30,12 @@ let comparison_name = function | Cgt -> ">" | Cge -> ">=" +let mu_name pp = function + | MUint -> fprintf pp "MUint" + | MUlong -> fprintf pp "MUlong" + | MUshrx i -> fprintf pp "MUshrx(%ld)" (camlint_of_coqint i) + | MUshrxl i -> fprintf pp "MUshrxl(%ld)" (camlint_of_coqint i) + let get_optR0_s c reg pp r1 r2 = function | None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2 | Some true -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1 @@ -226,9 +232,7 @@ let print_operation reg pp = function | OEandil n, [r1] -> fprintf pp "OEandil(%a,%ld)" reg r1 (camlint_of_coqint n) | OEoril n, [r1] -> fprintf pp "OEoril(%a,%ld)" reg r1 (camlint_of_coqint n) | OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n) - | OEmayundef isl, [r1;r2] -> fprintf pp "OEmayundef (%b,%a,%a)" isl reg r1 reg r2 - | OEshrxundef n, [r1] -> fprintf pp "OEshrxundef (%ld,%a)" (camlint_of_coqint n) reg r1 - | OEshrxlundef n, [r1] -> fprintf pp "OEshrxlundef (%ld,%a)" (camlint_of_coqint n) reg r1 + | OEmayundef mu, [r1;r2] -> fprintf pp "OEmayundef (%a,%a,%a)" mu_name mu reg r1 reg r2 | OEfeqd, [r1;r2] -> fprintf pp "OEfeqd(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2 | OEfltd, [r1;r2] -> fprintf pp "OEfltd(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2 | OEfled, [r1;r2] -> fprintf pp "OEfled(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2 diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 5804e67e..6066c7f5 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -165,7 +165,7 @@ Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) := if Int.eq n (Int.repr Int.max_signed) then let hvs := loadimm32 Int.one in let hl := make_lhsv_cmp false hv1 hvs in - fSop (OEmayundef false) hl + fSop (OEmayundef MUint) hl else sltimm32 hv1 (Int.add n Int.one) | _ => let optR0 := make_optR0 false is_inv in @@ -208,7 +208,7 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) := if Int64.eq n (Int64.repr Int64.max_signed) then let hvs := loadimm32 Int.one in let hl := make_lhsv_cmp false hv1 hvs in - fSop (OEmayundef true) hl + fSop (OEmayundef MUlong) hl else sltimm64 hv1 (Int64.add n Int64.one) | _ => let optR0 := make_optR0 false is_inv in @@ -440,8 +440,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let hl := make_lhsv_single hv1 in if Int.eq n Int.zero then let move_s := fSop Omove hl in - let move_l := make_lhsv_single move_s in - Some (fSop (OEshrxundef n) move_l) + let move_l := make_lhsv_cmp false move_s move_s in + Some (fSop (OEmayundef (MUshrx n)) move_l) else if Int.eq n Int.one then let srliw_s := fSop (Oshruimm (Int.repr 31)) hl in @@ -449,8 +449,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let addw_s := fSop Oadd srliw_l in let addw_l := make_lhsv_single addw_s in let sraiw_s := fSop (Oshrimm Int.one) addw_l in - let sraiw_l := make_lhsv_single sraiw_s in - Some (fSop (OEshrxundef n) sraiw_l) + let sraiw_l := make_lhsv_cmp false sraiw_s sraiw_s in + Some (fSop (OEmayundef (MUshrx n)) sraiw_l) else let sraiw_s := fSop (Oshrimm (Int.repr 31)) hl in let sraiw_l := make_lhsv_single sraiw_s in @@ -459,15 +459,15 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let addw_s := fSop Oadd srliw_l in let addw_l := make_lhsv_single addw_s in let sraiw_s' := fSop (Oshrimm n) addw_l in - let sraiw_l' := make_lhsv_single sraiw_s' in - Some (fSop (OEshrxundef n) sraiw_l') + let sraiw_l' := make_lhsv_cmp false sraiw_s' sraiw_s' in + Some (fSop (OEmayundef (MUshrx n)) sraiw_l') | Oshrxlimm n, a1 :: nil => let hv1 := fsi_sreg_get hst a1 in let hl := make_lhsv_single hv1 in if Int.eq n Int.zero then let move_s := fSop Omove hl in - let move_l := make_lhsv_single move_s in - Some (fSop (OEshrxlundef n) move_l) + let move_l := make_lhsv_cmp false move_s move_s in + Some (fSop (OEmayundef (MUshrxl n)) move_l) else if Int.eq n Int.one then let srlil_s := fSop (Oshrluimm (Int.repr 63)) hl in @@ -475,8 +475,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let addl_s := fSop Oaddl srlil_l in let addl_l := make_lhsv_single addl_s in let srail_s := fSop (Oshrlimm Int.one) addl_l in - let srail_l := make_lhsv_single srail_s in - Some (fSop (OEshrxlundef n) srail_l) + let srail_l := make_lhsv_cmp false srail_s srail_s in + Some (fSop (OEmayundef (MUshrxl n)) srail_l) else let srail_s := fSop (Oshrlimm (Int.repr 63)) hl in let srail_l := make_lhsv_single srail_s in @@ -485,8 +485,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let addl_s := fSop Oaddl srlil_l in let addl_l := make_lhsv_single addl_s in let srail_s' := fSop (Oshrlimm n) addl_l in - let srail_l' := make_lhsv_single srail_s' in - Some (fSop (OEshrxlundef n) srail_l') + let srail_l' := make_lhsv_cmp false srail_s' srail_s' in + Some (fSop (OEmayundef (MUshrxl n)) srail_l') (*| Oaddrstack n, nil =>*) (*let hv1 := fsi_sreg_get hst a1 in*) (*OK (addptrofs hv1 n)*) @@ -964,7 +964,7 @@ Proof. try rewrite OKv1; try rewrite OK2; try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst; - unfold Val.cmp, may_undef_int, zero32, Val.add; simpl; + unfold Val.cmp, eval_may_undef, zero32, Val.add; simpl; destruct v; auto. all: try rewrite ltu_12_wordsize; @@ -1018,7 +1018,7 @@ Proof. try rewrite OKv1; try rewrite OK2; rewrite HMEM; - unfold may_undef_int, Val.cmpu; + unfold eval_may_undef, Val.cmpu; destruct v; simpl; auto; try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl; try rewrite ltu_12_wordsize; trivial; @@ -1141,7 +1141,7 @@ Proof. unfold Val.cmpl, Val.addl; try rewrite xorl_zero_eq_cmpl; trivial; try rewrite optbool_mktotal; trivial; - unfold may_undef_int, zero32, Val.add; simpl; + unfold eval_may_undef, zero32, Val.add; simpl; destruct v; auto. 1,2,3,4,5,6,7,8,9,10,11,12: try rewrite <- optbool_mktotal; trivial; @@ -1210,7 +1210,7 @@ Proof. all: try apply xor_neg_ltle_cmplu; trivial. (* Others subcases with swap/negation *) all: - unfold Val.cmplu, may_undef_int, zero64, Val.addl; + unfold Val.cmplu, eval_may_undef, zero64, Val.addl; try apply Int64.same_if_eq in EQLO; subst; try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial; try rewrite Int64.add_commut; @@ -1681,41 +1681,57 @@ Lemma simplify_shrximm_correct ge sp rs0 m0 lr hst fsv st args m n: forall hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0) (H : match lr with - | nil => None - | a1 :: nil => - if Int.eq n Int.zero - then - Some - (fSop (OEshrxundef n) - (make_lhsv_single - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) - else - if Int.eq n Int.one + | nil => None + | a1 :: nil => + if Int.eq n Int.zero then Some - (fSop (OEshrxundef n) - (make_lhsv_single - (fSop (Oshrimm Int.one) - (make_lhsv_single - (fSop Oadd - (make_lhsv_cmp false (fsi_sreg_get hst a1) - (fSop (Oshruimm (Int.repr 31)) - (make_lhsv_single (fsi_sreg_get hst a1))))))))) + (fSop (OEmayundef (MUshrx n)) + (make_lhsv_cmp false + (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))) + (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) else - Some - (fSop (OEshrxundef n) - (make_lhsv_single - (fSop (Oshrimm n) - (make_lhsv_single - (fSop Oadd - (make_lhsv_cmp false (fsi_sreg_get hst a1) - (fSop (Oshruimm (Int.sub Int.iwordsize n)) - (make_lhsv_single - (fSop (Oshrimm (Int.repr 31)) - (make_lhsv_single - (fsi_sreg_get hst a1))))))))))) - | a1 :: _ :: _ => None - end = Some fsv) + if Int.eq n Int.one + then + Some + (fSop (OEmayundef (MUshrx n)) + (make_lhsv_cmp false + (fSop (Oshrimm Int.one) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.repr 31)) + (make_lhsv_single (fsi_sreg_get hst a1))))))) + (fSop (Oshrimm Int.one) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.repr 31)) + (make_lhsv_single (fsi_sreg_get hst a1))))))))) + else + Some + (fSop (OEmayundef (MUshrx n)) + (make_lhsv_cmp false + (fSop (Oshrimm n) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.sub Int.iwordsize n)) + (make_lhsv_single + (fSop (Oshrimm (Int.repr 31)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))) + (fSop (Oshrimm n) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.sub Int.iwordsize n)) + (make_lhsv_single + (fSop (Oshrimm (Int.repr 31)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))))) + | a1 :: _ :: _ => None + end = Some fsv) (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp (Oshrximm n) args m. @@ -1734,7 +1750,7 @@ Proof. erewrite !fsi_sreg_get_correct; eauto; destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1; destruct (Val.shrx v (Vint n)) eqn:TOTAL; cbn; - unfold shrx_imm_undef. + unfold eval_may_undef. 2,4,6: unfold Val.shrx in TOTAL; destruct v; simpl in TOTAL; simpl; try congruence; @@ -1769,41 +1785,57 @@ Lemma simplify_shrxlimm_correct ge sp rs0 m0 lr hst fsv st args m n: forall hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0) (H : match lr with - | nil => None - | a1 :: nil => - if Int.eq n Int.zero - then - Some - (fSop (OEshrxlundef n) - (make_lhsv_single - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) - else - if Int.eq n Int.one + | nil => None + | a1 :: nil => + if Int.eq n Int.zero then Some - (fSop (OEshrxlundef n) - (make_lhsv_single - (fSop (Oshrlimm Int.one) - (make_lhsv_single - (fSop Oaddl - (make_lhsv_cmp false (fsi_sreg_get hst a1) - (fSop (Oshrluimm (Int.repr 63)) - (make_lhsv_single (fsi_sreg_get hst a1))))))))) + (fSop (OEmayundef (MUshrxl n)) + (make_lhsv_cmp false + (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))) + (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) else - Some - (fSop (OEshrxlundef n) - (make_lhsv_single - (fSop (Oshrlimm n) - (make_lhsv_single - (fSop Oaddl - (make_lhsv_cmp false (fsi_sreg_get hst a1) - (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) - (make_lhsv_single - (fSop (Oshrlimm (Int.repr 63)) - (make_lhsv_single - (fsi_sreg_get hst a1))))))))))) - | a1 :: _ :: _ => None - end = Some fsv) + if Int.eq n Int.one + then + Some + (fSop (OEmayundef (MUshrxl n)) + (make_lhsv_cmp false + (fSop (Oshrlimm Int.one) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.repr 63)) + (make_lhsv_single (fsi_sreg_get hst a1))))))) + (fSop (Oshrlimm Int.one) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.repr 63)) + (make_lhsv_single (fsi_sreg_get hst a1))))))))) + else + Some + (fSop (OEmayundef (MUshrxl n)) + (make_lhsv_cmp false + (fSop (Oshrlimm n) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) + (make_lhsv_single + (fSop (Oshrlimm (Int.repr 63)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))) + (fSop (Oshrlimm n) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) + (make_lhsv_single + (fSop (Oshrlimm (Int.repr 63)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))))) + | a1 :: _ :: _ => None + end = Some fsv) (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp (Oshrxlimm n) args m. @@ -1822,7 +1854,7 @@ Proof. erewrite !fsi_sreg_get_correct; eauto; destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1; destruct (Val.shrxl v (Vint n)) eqn:TOTAL; cbn; - unfold shrxl_imm_undef. + unfold eval_may_undef. 2,4,6: unfold Val.shrxl in TOTAL; destruct v; simpl in TOTAL; simpl; try congruence; @@ -1850,7 +1882,7 @@ Proof. destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate. rewrite !EQN2. rewrite EQN0. reflexivity. -Qed. + Qed. Lemma simplify_cast32unsigned_correct ge sp rs0 m0 lr hst fsv st args m: forall (SREG: forall r: positive, @@ -2001,7 +2033,7 @@ Proof. try destruct (Int64.eq lo Int64.zero) eqn:EQLO; try apply Int.same_if_eq in EQLO; simpl; trivial; try apply Int64.same_if_eq in EQLO; simpl; trivial; - unfold may_undef_int; + unfold eval_may_undef; try erewrite !fsi_sreg_get_correct; eauto; try rewrite OKv1; simpl; trivial; try destruct v; try rewrite H; diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index fe519921..82291f9c 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -27,42 +27,28 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 | Some false => sem v1 vz end. -Definition may_undef_int (is_long: bool) (v1 v2: aval): aval := - if negb is_long then - match v1 with - | I _ => v2 - | _ => Ifptr Ptop - end - else - match v1 with - | L _ => v2 - | _ => Ifptr Ptop - end. - -Definition shrx_imm_undef (v1 v2: aval): aval := - match v1 with - | I n1 => - match v2 with - | I n2 => - if Int.ltu n2 (Int.repr 31) - then I n1 - else Ifptr Ptop +Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := + match mu with + | MUint => match v1 with + | I _ => v2 + | _ => Ifptr Ptop + end + | MUlong => match v1 with + | L _ => v2 + | _ => Ifptr Ptop + end + | MUshrx i => + match v1 with + | I _ => + if Int.ltu i (Int.repr 31) then v1 else Ifptr Ptop | _ => Ifptr Ptop end - | _ => Ifptr Ptop - end. - -Definition shrxl_imm_undef (v1 v2: aval): aval := - match v1 with - | L n1 => - match v2 with - | I n2 => - if Int.ltu n2 (Int.repr 63) - then L n1 - else Ifptr Ptop + | MUshrxl i => + match v1 with + | L _ => + if Int.ltu i (Int.repr 63) then v1 else Ifptr Ptop | _ => Ifptr Ptop end - | _ => Ifptr Ptop end. Definition eval_static_condition (cond: condition) (vl: list aval): abool := @@ -263,9 +249,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEaddil n, v1::nil => addl (L n) v1 | OEaddilr0 n, nil => addl (L n) zero64 | OEloadli n, nil => L (n) - | OEmayundef is_long, v1::v2::nil => may_undef_int is_long v1 v2 - | OEshrxundef n, v1::nil => shrx_imm_undef v1 (I n) - | OEshrxlundef n, v1::nil => shrxl_imm_undef v1 (I n) + | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2 | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2) | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2) @@ -508,21 +492,16 @@ Proof. 1,10: simpl; eauto with va. 2: - unfold Op.may_undef_int, may_undef_int; destruct is_long; - simpl; inv H0; inv H1; eauto with va; inv H; - apply vmatch_ifptr_p; eauto with va. + unfold Op.eval_may_undef, eval_may_undef; destruct mu; + inv H1; inv H0; eauto with va; + try destruct (Int.ltu _ _); simpl; + try eapply vmatch_ifptr_p, pmatch_top'; eauto with va. 3,4,6: apply eval_cmplu_sound; auto. 1,2,3: apply eval_cmpl_sound; auto. { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. } { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. } { unfold zero64; simpl; eauto with va. } - { unfold Op.shrx_imm_undef, shrx_imm_undef. - simpl; inv H1; eauto with va; - destruct (Int.ltu _ _); simpl; eauto with va. } - { unfold Op.shrxl_imm_undef, shrxl_imm_undef. - simpl; inv H1; eauto with va; - destruct (Int.ltu _ _); simpl; eauto with va. } all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. -- cgit