Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 8fb2a5a1 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

[Admitted checker] Some more proof, version with buggy addirw0

parent c3bebbcc
......@@ -5,7 +5,7 @@ Require Import RTLpathSE_theory.
Require Import RTLpathSE_simu_specs.
Require Import Asmgen Asmgenproof1.
(* Useful functions for conditions/branches expansion *)
(** Useful functions for conditions/branches expansion *)
Definition is_inv_cmp_int (cmp: comparison) : bool :=
match cmp with | Cle | Cgt => true | _ => false end.
......@@ -16,7 +16,7 @@ Definition is_inv_cmp_float (cmp: comparison) : bool :=
Definition make_optR0 (is_x0 is_inv: bool) : option bool :=
if is_x0 then Some is_inv else None.
(* Functions to manage lists of "fake" values *)
(** Functions to manage lists of "fake" values *)
Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval :=
let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in
......@@ -26,7 +26,9 @@ Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval :=
Definition make_lhsv_single (hvs: hsval) : list_hsval :=
fScons hvs fSnil.
(* Expansion functions *)
(** Expansion functions *)
(* Immediate loads *)
Definition load_hilo32 (hi lo: int) :=
if Int.eq lo Int.zero then
......@@ -91,6 +93,9 @@ Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEslt
Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul.
(* Comparisons intructions *)
Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
match cmp with
| Ceq => fSop (OEseqw optR0) lhsv
......@@ -241,7 +246,7 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
let hl := make_lhsv_single hvs in
if normal' then hvs else fSop (OExoriw Int.one) hl.
(* Target op simplifications using "fake" values *)
(** Target op simplifications using "fake" values *)
Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
match op, lr with
......@@ -312,7 +317,9 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
| _, _ => None
end.
(* Auxiliary lemmas on comparisons *)
(** Auxiliary lemmas on comparisons *)
(* Signed ints *)
Lemma xor_neg_ltle_cmp: forall v1 v2,
Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
......@@ -327,6 +334,8 @@ Proof.
auto.
Qed.
(* Unsigned ints *)
Lemma xor_neg_ltle_cmpu: forall mptr v1 v2,
Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) =
Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
......@@ -351,6 +360,8 @@ Proof.
repeat destruct (_ && _); simpl; auto.
Qed.
(* Signed longs *)
Lemma xor_neg_ltle_cmpl: forall v1 v2,
Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) =
Some (Val.of_optbool (Val.cmpl_bool Cle v2 v1)).
......@@ -369,6 +380,46 @@ Proof.
destruct (Int64.lt _ _); auto.
Qed.
Lemma xorl_zero_eq_cmpl: forall c v1 v2,
c = Ceq \/ c = Cne ->
Some
(Val.maketotal
(option_map Val.of_bool
(Val.cmpl_bool c (Val.xorl v1 v2) (Vlong Int64.zero)))) =
Some (Val.of_optbool (Val.cmpl_bool c v1 v2)).
Proof.
intros. destruct c; inv H; try discriminate;
destruct v1, v2; simpl; auto;
destruct (Int64.eq i i0) eqn:EQ0.
1,3:
apply Int64.same_if_eq in EQ0; subst;
rewrite Int64.xor_idem;
rewrite Int64.eq_true; trivial.
1,2:
destruct (Int64.eq (Int64.xor i i0) Int64.zero) eqn:EQ1; simpl; try congruence;
rewrite Int64.xor_is_zero in EQ1; congruence.
Qed.
Lemma cmpl_ltle_add_one: forall v n,
Int64.eq n (Int64.repr Int64.max_signed) = false ->
Some (Val.of_optbool (Val.cmpl_bool Clt v (Vlong (Int64.add n Int64.one)))) =
Some (Val.of_optbool (Val.cmpl_bool Cle v (Vlong n))).
Proof.
intros v n EQMAX. unfold Val.cmpl_bool; destruct v; simpl; auto.
unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
destruct (zlt (Int64.signed n) (Int64.signed i)).
rewrite zlt_false by omega. auto.
rewrite zlt_true by omega. auto.
rewrite Int64.add_signed. symmetry; apply Int64.signed_repr.
specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)).
rewrite EQMAX; simpl; intros.
assert (Int64.signed n <> Int64.max_signed).
{ red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
generalize (Int64.signed_range n); omega.
Qed.
(* Unsigned longs *)
Lemma xor_neg_ltle_cmplu: forall mptr v1 v2,
Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) =
Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
......@@ -413,6 +464,8 @@ Proof.
repeat destruct (_ && _); simpl; auto.
Qed.
(* Floats *)
Lemma xor_neg_eqne_cmpf: forall v1 v2,
Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) =
Some (Val.of_optbool (Val.cmpf_bool Cne v1 v2)).
......@@ -424,6 +477,8 @@ Proof.
destruct (Float.cmp _ _ _); simpl; auto.
Qed.
(* Singles *)
Lemma xor_neg_eqne_cmpfs: forall v1 v2,
Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) =
Some (Val.of_optbool (Val.cmpfs_bool Cne v1 v2)).
......@@ -435,6 +490,8 @@ Proof.
destruct (Float32.cmp _ _ _); simpl; auto.
Qed.
(* More useful lemmas *)
Lemma xor_neg_optb: forall v,
Some (Val.xor (Val.of_optbool (option_map negb v))
(Vint Int.one)) = Some (Val.of_optbool v).
......@@ -645,6 +702,70 @@ Proof.
- apply xor_neg_ltge_cmplu.
Qed.
Lemma simplify_ccomplimm_correct ge sp hst st c r n rs0 m m0 v: forall
(SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
(SREG: forall r: positive,
hsi_sreg_eval ge sp hst r rs0 m0 =
seval_sval ge sp (si_sreg st r) rs0 m0)
(OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
(OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
seval_sval ge sp
(hsval_proj (expanse_condimm_int64s c (fsi_sreg_get hst r) n)) rs0 m0 =
Some (Val.of_optbool (Val.cmpl_bool c v (Vlong n))).
Proof.
intros.
unfold expanse_condimm_int64s, cond_int64s in *; destruct c;
intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl;
unfold loadimm32, loadimm64, sltimm64, xorimm64, opimm64, load_hilo32, load_hilo64;
try erewrite !fsi_sreg_get_correct; eauto;
try rewrite OKv1;
unfold Val.cmpl, zero64.
(* Simplify make immediate and decompose subcases *)
2,4,6,10,12:
try (specialize make_immed64_sound with n;
destruct (make_immed64 n) eqn:EQMKI_A0).
20:
try (specialize make_immed32_sound with (Int.one);
destruct (make_immed32 Int.one) eqn:EQMKI_A1).
20,21:
try (specialize make_immed64_sound with (Int64.add n Int64.one);
destruct (make_immed64 (Int64.add n Int64.one)) eqn:EQMKI_A2).
all:
try destruct (Int.eq lo Int.zero) eqn:EQLO32;
try destruct (Int64.eq lo Int64.zero) eqn:EQLO64;
try destruct (Int64.eq lo0 Int64.zero) eqn:EQLO064;
try destruct (Int64.eq n (Int64.repr Int64.max_signed)) eqn:EQMAX;
try erewrite fSop_correct; eauto; simpl;
try erewrite !fsi_sreg_get_correct; eauto;
try rewrite OKv1;
try rewrite OK2.
(* Ceq, Cne, Clt = itself *)
all: intros; try apply Int64.same_if_eq in EQIMM; subst;
try (rewrite optbool_mktotal; trivial; fail).
(* Others simple subcases *)
all:
unfold Val.cmpl;
try apply Int64.same_if_eq in EQLO64; subst;
try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial;
try (rewrite <- xor_neg_ltle_cmpl; unfold Val.cmpl;
trivial; fail);
try erewrite xorl_zero_eq_cmpl; eauto;
try apply xor_neg_ltle_cmpl;
try apply xor_neg_ltge_cmpl;
trivial;
try rewrite optbool_mktotal; trivial.
all:
try apply Int64.same_if_eq in EQLO064; subst;
try rewrite (Int64.add_commut (Int64.sign_ext 32 (Int64.shl hi0 (Int64.repr 12))) Int64.zero) in H;
try rewrite (Int64.add_commut (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) Int64.zero) in H;
try rewrite Int64.add_zero_l in H; try rewrite <- H;
try apply cmpl_ltle_add_one; auto.
all: admit.
Admitted.
Lemma simplify_ccompluimm_correct ge sp hst st c r n rs0 m m0 v: forall
(SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
......
......@@ -933,23 +933,7 @@ Proof.
destruct (Float.cmp _ _ _); simpl; auto.
Qed.
Lemma cmp_ltle_add_one: forall v n,
Int.eq n (Int.repr Int.max_signed) = false ->
Some (Val.of_optbool (Val.cmp_bool Clt v (Vint (Int.add n Int.one)))) =
Some (Val.of_optbool (Val.cmp_bool Cle v (Vint n))).
Proof.
intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto.
unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
destruct (zlt (Int.signed n) (Int.signed i)).
rewrite zlt_false by omega. auto.
rewrite zlt_true by omega. auto.
rewrite Int.add_signed. symmetry; apply Int.signed_repr.
specialize (Int.eq_spec n (Int.repr Int.max_signed)).
rewrite EQMAX; simpl; intros.
assert (Int.signed n <> Int.max_signed).
{ red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. }
generalize (Int.signed_range n); omega.
Qed.
(* TODO gourdinl Lemma cmp_le_max: forall v*)
(*(CONTRA: Some*)
......@@ -1161,7 +1145,7 @@ Proof.
rewrite Int.add_zero_l in *. apply cmp_ltle_add_one; auto. }
{ rewrite <- H.
rewrite (Int.add_commut (Int.shl hi (Int.repr 12)) Int.zero) in *.
rewrite Int.add_zero_l in *. apply cmp_ltle_add_one; auto. }
rewrite Int.add_zero_l in *. apply cmp_ltle_add_one; auto. }
{ apply cmp_ltle_add_one; auto. }
{ apply Int.same_if_eq in H2; subst.
rewrite (Int.add_commut (Int.shl hi0 (Int.repr 12)) Int.zero) in H.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment