Skip to content

GitLab

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 c3bebbcc authored by Léo Gourdin's avatar Léo Gourdin
Browse files

some more proof for fake hsval checker expansions

parent 313443c8
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 772 additions and 370 deletions
riscV/ExpansionOracle.ml
View file @ c3bebbcc
......@@ -388,7 +388,7 @@ let expanse (sb : superblock) code pm =
debug "Iop/Ccomp\n";
exp := cond_int32s false c a1 a2 dest succ [];
was_exp := true
(*| Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
| Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
debug "Iop/Ccompu\n";
exp := cond_int32u false c a1 a2 dest succ [];
was_exp := true
......@@ -432,7 +432,7 @@ let expanse (sb : superblock) code pm =
debug "Iop/Cnotcompfs\n";
exp := expanse_cond_fp true cond_single c f1 f2 dest succ [];
was_exp := true
| Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
(*| Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
debug "Icond/Ccomp\n";
exp := cbranch_int32s false c a1 a2 info succ1 succ2 [];
was_branch := true;
......
riscV/RTLpathSE_simplify.v
View file @ c3bebbcc
This diff is collapsed.
scheduling/RTLpathSE_impl.v
View file @ c3bebbcc
......@@ -7,7 +7,6 @@ Require Import RTL RTLpath.
Require Import Errors.
Require Import RTLpathSE_theory RTLpathLivegenproof.
Require Import Axioms RTLpathSE_simu_specs.
Require Import Asmgen Asmgenproof1.
Require Import RTLpathSE_simplify.
Local Open Scope error_monad_scope.
......@@ -659,214 +658,14 @@ Qed.
end.*)
(*
Definition load_hilo32 (hi lo: int) :=
DO hnil <~ hSnil();;
if Int.eq lo Int.zero then
hSop (OEluiw hi) hnil
else
DO hvs <~ hSop (OEluiw hi) hnil;;
DO hl <~ make_lhsv_single hvs;;
hSop (Oaddimm lo) hl.
Definition load_hilo64 (hi lo: int64) :=
DO hnil <~ hSnil();;
if Int64.eq lo Int64.zero then
hSop (OEluil hi) hnil
else
DO hvs <~ hSop (OEluil hi) hnil;;
DO hl <~ make_lhsv_single hvs;;
hSop (Oaddlimm lo) hl.
Definition loadimm32 (n: int) :=
match make_immed32 n with
| Imm32_single imm =>
DO hnil <~ hSnil();;
hSop (OEaddiwr0 imm) hnil
| Imm32_pair hi lo => load_hilo32 hi lo
end.
Definition loadimm64 (n: int64) :=
DO hnil <~ hSnil();;
match make_immed64 n with
| Imm64_single imm =>
hSop (OEaddilr0 imm) hnil
| Imm64_pair hi lo => load_hilo64 hi lo
| Imm64_large imm => hSop (OEloadli imm) hnil
end.
Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) :=
match make_immed32 n with
| Imm32_single imm =>
DO hl <~ make_lhsv_single hv1;;
hSop (opimm imm) hl
| Imm32_pair hi lo =>
DO hvs <~ load_hilo32 hi lo;;
DO hl <~ make_lhsv_cmp false hv1 hvs;;
hSop op hl
end.
Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> operation) :=
match make_immed64 n with
| Imm64_single imm =>
DO hl <~ make_lhsv_single hv1;;
hSop (opimm imm) hl
| Imm64_pair hi lo =>
DO hvs <~ load_hilo64 hi lo;;
DO hl <~ make_lhsv_cmp false hv1 hvs;;
hSop op hl
| Imm64_large imm =>
DO hnil <~ hSnil();;
DO hvs <~ hSop (OEloadli imm) hnil;;
DO hl <~ make_lhsv_cmp false hv1 hvs;;
hSop op hl
end.
Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw.
Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw.
Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw.
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.
Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
match cmp with
| Ceq => hSop (OEsequw optR0) lhsv
| Cne => hSop (OEsneuw optR0) lhsv
| Clt | Cgt => hSop (OEsltuw optR0) lhsv
| Cle | Cge =>
DO hvs <~ (hSop (OEsltuw optR0) lhsv);;
DO hl <~ make_lhsv_single hvs;;
hSop (OExoriw Int.one) hl
end.
Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
match cmp with
| Ceq => hSop (OEseql optR0) lhsv
| Cne => hSop (OEsnel optR0) lhsv
| Clt | Cgt => hSop (OEsltl optR0) lhsv
| Cle | Cge =>
DO hvs <~ (hSop (OEsltl optR0) lhsv);;
DO hl <~ make_lhsv_single hvs;;
hSop (OExoriw Int.one) hl
end.
Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
match cmp with
| Ceq => hSop (OEsequl optR0) lhsv
| Cne => hSop (OEsneul optR0) lhsv
| Clt | Cgt => hSop (OEsltul optR0) lhsv
| Cle | Cge =>
DO hvs <~ (hSop (OEsltul optR0) lhsv);;
DO hl <~ make_lhsv_single hvs;;
hSop (OExoriw Int.one) hl
end.
Definition cond_float (cmp: comparison) (lhsv: list_hsval) :=
match cmp with
| Ceq | Cne => hSop OEfeqd lhsv
| Clt | Cgt => hSop OEfltd lhsv
| Cle | Cge => hSop OEfled lhsv
end.
Definition cond_single (cmp: comparison) (lhsv: list_hsval) :=
match cmp with
| Ceq | Cne => hSop OEfeqs lhsv
| Clt | Cgt => hSop OEflts lhsv
| Cle | Cge => hSop OEfles lhsv
end.
Definition is_normal_cmp cmp :=
match cmp with | Cne => false | _ => true end.
Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
let normal := is_normal_cmp cmp in
let normal' := if cnot then negb normal else normal in
DO hvs <~ fn_cond cmp lhsv;;
DO hl <~ make_lhsv_single hvs;;
if normal' then RET hvs else hSop (OExoriw Int.one) hl.
Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
let is_inv := is_inv_cmp_int cmp in
if Int.eq n Int.zero then
let optR0 := make_optR0 true is_inv in
DO hl <~ make_lhsv_cmp is_inv hv1 hv1;;
cond_int32s cmp hl optR0
else
match cmp with
| Ceq | Cne =>
let optR0 := make_optR0 true is_inv in
DO hvs <~ xorimm32 hv1 n;;
DO hl <~ make_lhsv_cmp false hvs hvs;;
cond_int32s cmp hl optR0
| Clt => sltimm32 hv1 n
| Cle =>
if Int.eq n (Int.repr Int.max_signed) then
loadimm32 Int.one
else sltimm32 hv1 (Int.add n Int.one)
| _ =>
let optR0 := make_optR0 false is_inv in
DO hvs <~ loadimm32 n;;
DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
cond_int32s cmp hl optR0
end.
Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) :=
let is_inv := is_inv_cmp_int cmp in
if Int.eq n Int.zero then
let optR0 := make_optR0 true is_inv in
DO hl <~ make_lhsv_cmp is_inv hv1 hv1;;
cond_int32u cmp hl optR0
else
match cmp with
| Clt => sltuimm32 hv1 n
| _ =>
let optR0 := make_optR0 false is_inv in
DO hvs <~ loadimm32 n;;
DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
cond_int32u cmp hl optR0
end.
Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
let is_inv := is_inv_cmp_int cmp in
if Int64.eq n Int64.zero then
let optR0 := make_optR0 true is_inv in
DO hl <~ make_lhsv_cmp is_inv hv1 hv1;;
cond_int64s cmp hl optR0
else
match cmp with
| Ceq | Cne =>
let optR0 := make_optR0 true is_inv in
DO hvs <~ xorimm64 hv1 n;;
DO hl <~ make_lhsv_cmp false hvs hvs;;
cond_int64s cmp hl optR0
| Clt => sltimm64 hv1 n
| Cle =>
if Int64.eq n (Int64.repr Int64.max_signed) then
loadimm32 Int.one
else sltimm64 hv1 (Int64.add n Int64.one)
| _ =>
let optR0 := make_optR0 false is_inv in
DO hvs <~ loadimm64 n;;
DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
cond_int64s cmp hl optR0
end.
Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) :=
let is_inv := is_inv_cmp_int cmp in
if Int64.eq n Int64.zero then
let optR0 := make_optR0 true is_inv in
DO hl <~ make_lhsv_cmp is_inv hv1 hv1;;
cond_int64u cmp hl optR0
else
match cmp with
| Clt => sltuimm64 hv1 n
| _ =>
let optR0 := make_optR0 false is_inv in
DO hvs <~ loadimm64 n;;
DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
cond_int64u cmp hl optR0
end.
*)
(** simplify a symbolic value before assignment to a register *)
......@@ -911,27 +710,6 @@ Proof.
intro H0; clear H0; simplify_SOME z; congruence.
Qed.
Lemma xor_neg_ltle_cmp: forall v1 v2,
Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
Some (Val.of_optbool (Val.cmp_bool Cle v2 v1)).
Proof.
intros. eapply f_equal.
destruct v1, v2; simpl; try congruence.
unfold Val.cmp; simpl;
try rewrite Int.eq_sym;
try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl;
try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
auto.
Qed.
Lemma xor_neg_optb: forall v,
Some (Val.xor (Val.of_optbool (option_map negb v))
(Vint Int.one)) = Some (Val.of_optbool v).
Proof.
intros.
destruct v; simpl; trivial.
destruct b; simpl; auto.
Qed.
Lemma xor_ceq_zero: forall v n cmp,
cmp = Ceq \/ cmp = Cne ->
......@@ -966,29 +744,6 @@ Proof.
unfold Val.cmp; simpl; auto.
Qed.*)
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)).
Proof.
intros. eapply f_equal.
destruct v1, v2; simpl; try congruence.
unfold Val.cmpu; simpl;
try rewrite Int.eq_sym;
try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl;
try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
auto.
1,2:
unfold Val.cmpu, Val.cmpu_bool;
destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _);
try destruct (eq_block _ _); auto.
unfold Val.cmpu, Val.cmpu_bool; simpl;
destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
destruct (eq_block b b0); destruct (eq_block b0 b);
try congruence;
try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
simpl; auto;
repeat destruct (_ && _); simpl; auto.
Qed.
(* TODO gourdinl Lemma xor_neg_ltge_cmpu: forall mptr v1 v2,
Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) =
......@@ -1143,16 +898,7 @@ Proof.
repeat destruct (_ && _); simpl; auto.
Qed.
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)).
Proof.
intros. eapply f_equal.
destruct v1, v2; simpl; try congruence;
unfold Val.cmpf; simpl.
rewrite Float.cmp_ne_eq.
destruct (Float.cmp _ _ _); simpl; auto.
Qed.
Lemma xor_neg_eqne_cmpfs: forall v1 v2,
Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) =
......@@ -1443,62 +1189,6 @@ Proof.
Admitted.
(*Qed.*)
Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;; expanse_condimm_int32u c hv1 n ~> hv
THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset)
(m0 : mem) (st : sistate_local),
hsilocal_refines ge sp rs0 m0 hst st ->
hsok_local ge sp rs0 m0 hst ->
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m) <> None ->
seval_sval ge sp (hsval_proj hv) rs0 m0 =
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m)).
Proof.
unfold expanse_condimm_int32u, cond_int32u in *; destruct c;
intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
unfold loadimm32, sltuimm32, opimm32, load_hilo32.
1,3,5,7,9,11:
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence;
try (simplify_SOME z; contradiction; fail);
try erewrite H9; eauto; try erewrite H8; eauto;
try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
4: rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu.
5: intros; replace (Clt) with (swap_comparison Cgt) by auto;
rewrite Val.swap_cmpu_bool; trivial.
6: intros; replace (Clt) with (negate_comparison Cge) by auto;
rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb.
1,2,3,4,5,6: apply Int.same_if_eq in EQIMM; subst; trivial.
all:
specialize make_immed32_sound with n;
destruct (make_immed32 n) eqn:EQMKI;
try destruct (Int.eq lo Int.zero) eqn:EQLO.
all:
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail).
all:
try erewrite H11; eauto;
try erewrite H10; eauto; try erewrite H9; eauto; try erewrite H8; eauto;
try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
all: try apply Int.same_if_eq in H1; subst.
all: try apply Int.same_if_eq in EQLO; subst.
all: try rewrite Int.add_commut, Int.add_zero_l; trivial.
all: try rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu; trivial.
all: intros; replace (Clt) with (negate_comparison Cge) by auto;
rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb; trivial.
Qed.
Lemma simplify_ccompl_correct: forall c r r0 (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;;
......@@ -1576,20 +1266,7 @@ Proof.
- intros; apply xor_neg_ltge_cmplu.
Qed.
(* TODO gourdinl move to common/Values ? *)
Theorem swap_cmpf_bool:
forall c x y,
Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x.
Proof.
destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto.
Qed.
Theorem swap_cmpfs_bool:
forall c x y,
Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x.
Proof.
destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto.
Qed.
Lemma simplify_ccompf_correct: forall c r r0 (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;;
......
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