Commit 0d98d7fe authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Refactoring the mayundef OP to be more general...

parent 17b35c46
......@@ -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)
......
......@@ -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.
......
......@@ -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
......
......@@ -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;
......
......@@ -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)