Skip to content

GitLab

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

Branch expansions activated and configured in the checker (but admitted) and... 

Branch expansions activated and configured in the checker (but admitted) and bugfix in the expansion liveness modification
parent 9c9d516b
Hide whitespace changes
Inline Side-by-side
riscV/ExpansionOracle.ml
View file @ fb6325b4
......@@ -442,7 +442,7 @@ let expanse (sb : superblock) code pm =
exp := cbranch_int32u false c a1 a2 info succ1 succ2 [];
was_branch := true;
was_exp := true
(*| Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
| Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
debug "Icond/Ccompimm\n";
exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [];
was_branch := true;
......@@ -451,7 +451,7 @@ let expanse (sb : superblock) code pm =
debug "Icond/Ccompuimm\n";
exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 [];
was_branch := true;
was_exp := true*)
was_exp := true
| Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) ->
debug "Icond/Ccompl\n";
exp := cbranch_int64s false c a1 a2 info succ1 succ2 [];
......@@ -462,7 +462,7 @@ let expanse (sb : superblock) code pm =
exp := cbranch_int64u false c a1 a2 info succ1 succ2 [];
was_branch := true;
was_exp := true
(*| Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
| Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
debug "Icond/Ccomplimm\n";
exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 [];
was_branch := true;
......@@ -492,7 +492,7 @@ let expanse (sb : superblock) code pm =
debug "Icond/Cnotcompfs\n";
exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 [];
was_branch := true;
was_exp := true*)
was_exp := true
| _ -> new_order := n :: !new_order);
if !was_exp then (
node := !node + 1;
......@@ -500,7 +500,8 @@ let expanse (sb : superblock) code pm =
let lives = PTree.get n !liveins in
match lives with
| Some lives ->
liveins := PTree.set (n2p ()) lives !liveins;
let new_branch_pc = Camlcoq.P.of_int (!node - ((List.length !exp) - 1)) in
liveins := PTree.set new_branch_pc lives !liveins;
liveins := PTree.remove n !liveins
| _ -> ());
write_pathmap sb.instructions.(0) (List.length !exp) pm';
......
scheduling/RTLpathSE_impl.v
View file @ fb6325b4
......@@ -893,6 +893,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int64u c lhsv optR0
| (Ccomplimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64s c hv1 imm
| (Ccompluimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64u c hv1 imm
| (Ccompf c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
......@@ -917,12 +923,6 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp true cond_single c lhsv
| (Ccomplimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64s c hv1 imm
| (Ccompluimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64u c hv1 imm
| _, _ =>
DO lhsv <~ hlist_args hst lr;;
hSop op lhsv
......@@ -1317,7 +1317,7 @@ Proof.
rewrite Int.sub_zero_l. unfold Int.shru, Int.shl.
*)
(* TODO gourdinl Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local),
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),
......@@ -1355,51 +1355,37 @@ Proof.
simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
+ apply mkimm_single_equal in EQMKI; subst.
rewrite Int.add_commut, Int.add_zero_l. trivial.
+
2: { intros. destruct (Int.eq n Int.zero) eqn:EQIMM; simpl.
2: { unfold loadimm32. destruct (make_immed32 n) eqn:EQMKI.
2: {
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail);
+ admit.
+ admit.
- (* TODO gourdinl same as first goal *)
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: 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.
2: {
apply mkimm_single_equal in EQMKI; subst.
rewrite Int.add_commut, Int.add_zero_l. trivial.
2: {
apply Int.same_if_eq in EQIMM; subst. trivial.
- admit.
- (* TODO gourdinl same as first goal *)
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail).
2: {
all:
try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
all: 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.cmp, zero32.
all:
try apply Int.same_if_eq in H0; subst; trivial.
erewrite H0.
- intros; apply xor_neg_ltle_cmpu.
- intros; replace (Clt) with (swap_comparison Cgt) by auto;
rewrite Val.swap_cmpu_bool; trivial.
- intros; replace (Clt) with (negate_comparison Cge) by auto;
rewrite Val.negate_cmpu_bool.
rewrite xor_neg_optb; trivial.
Qed.
*)
simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
apply Int.same_if_eq in EQIMM; subst. trivial.
- (* same *) admit.
- (* same *) admit.
- (* same *) admit.
- (* same *) admit.
- (* same *) admit.
- (* same *) admit.
- (* same *) admit.
Admitted.
Lemma simplify_ccompl_correct: forall c r r0 (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;;
......@@ -1791,7 +1777,7 @@ Proof.
rewrite <- X, sok_local_set_sreg. intuition eauto.
- destruct REF; intuition eauto.
- generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto.
Qed.
Qed.
Global Opaque hslocal_set_sreg.
Local Hint Resolve hslocal_set_sreg_correct: wlp.
......@@ -1843,6 +1829,13 @@ Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) :=
| Cge => CEbgeul optR0
end.
Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : ?? (condition * 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_cmp false hvs hvs;;
if normal' then RET ((CEbnew (Some false)), hl) else RET ((CEbeqw (Some false)), hl).
Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : ?? (condition * list_hsval) :=
match cond, args with
| (Ccomp c), (a1 :: a2 :: nil) =>
......@@ -1859,6 +1852,30 @@ Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list
DO hv2 <~ hsi_sreg_get prev a2;;
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
RET (cond, lhsv)
| (Ccompimm c n), (a1 :: nil) =>
let is_inv := is_inv_cmp_int c in
DO hv1 <~ hsi_sreg_get prev a1;;
(if Int.eq n Int.zero then
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in
RET (cond, lhsv)
else
DO hvs <~ loadimm32 n;;
DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
RET (cond, lhsv))
| (Ccompuimm c n), (a1 :: nil) =>
let is_inv := is_inv_cmp_int c in
DO hv1 <~ hsi_sreg_get prev a1;;
(if Int.eq n Int.zero then
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in
RET (cond, lhsv)
else
DO hvs <~ loadimm32 n;;
DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
RET (cond, lhsv))
| (Ccompl c), (a1 :: a2 :: nil) =>
let is_inv := is_inv_cmp_int c in
let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
......@@ -1873,9 +1890,54 @@ Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list
DO hv2 <~ hsi_sreg_get prev a2;;
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
RET (cond, lhsv)
(* | Icond (Ccompimm c n) (a1 :: nil) _ _ _ =>
let cond := transl_cbranch_int32s c (make_optR0 c) in
RET (cond, a1 :: a1 :: nil)*)
| (Ccomplimm c n), (a1 :: nil) =>
let is_inv := is_inv_cmp_int c in
DO hv1 <~ hsi_sreg_get prev a1;;
(if Int64.eq n Int64.zero then
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in
RET (cond, lhsv)
else
DO hvs <~ loadimm64 n;;
DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
RET (cond, lhsv))
| (Ccompluimm c n), (a1 :: nil) =>
let is_inv := is_inv_cmp_int c in
DO hv1 <~ hsi_sreg_get prev a1;;
(if Int64.eq n Int64.zero then
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in
RET (cond, lhsv)
else
DO hvs <~ loadimm64 n;;
DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
RET (cond, lhsv))
| (Ccompf c), (f1 :: f2 :: nil) =>
DO hv1 <~ hsi_sreg_get prev f1;;
DO hv2 <~ hsi_sreg_get prev f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cbranch_fp false cond_float c lhsv
| (Cnotcompf c), (f1 :: f2 :: nil) =>
DO hv1 <~ hsi_sreg_get prev f1;;
DO hv2 <~ hsi_sreg_get prev f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cbranch_fp true cond_float c lhsv
| (Ccompfs c), (f1 :: f2 :: nil) =>
DO hv1 <~ hsi_sreg_get prev f1;;
DO hv2 <~ hsi_sreg_get prev f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cbranch_fp false cond_single c lhsv
| (Cnotcompfs c), (f1 :: f2 :: nil) =>
DO hv1 <~ hsi_sreg_get prev f1;;
DO hv2 <~ hsi_sreg_get prev f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cbranch_fp true cond_single c lhsv
| _, _ =>
DO vargs <~ hlist_args prev args;;
RET (cond, vargs)
......@@ -1984,7 +2046,7 @@ Lemma hsiexec_inst_correct i hst:
exists st', siexec_inst i st = Some st'
/\ (forall (REF:hsistate_refines_stat hst st), hsistate_refines_stat hst' st')
/\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st').
Proof.
Proof. Admitted. (*
destruct i; simpl;
try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail).
- (* refines_dyn Iop *)
......@@ -2020,9 +2082,44 @@ Proof.
destruct NEST as [|st0 se lse TOP NEST];
econstructor; simpl; auto; constructor; auto.
+ admit.
+ repeat (destruct l; try apply hsiexec_cond_noexp).
destruct (Int.eq _ _) eqn:EQIMM; simpl.
1: admit.
unfold loadimm32; destruct make_immed32.
{
wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
* unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
constructor; simpl; eauto.
constructor.
* destruct REF as (EXREF & LREF & NEST).
split.
-- do 2 (constructor; simpl; auto).
intros; erewrite seval_condition_refines; eauto.
destruct c0; simpl; unfold seval_condition.
{ simpl in *.
erewrite H4; eauto.
erewrite H3; eauto; erewrite H2; eauto.
simpl.
erewrite H1; eauto. try erewrite H0; eauto;
try erewrite H; eauto; simplify_SOME z.
2: {
generalize (sok_local_set_sreg_simp (Rop (OEaddiwr0 imm))); simpl; eauto.
intros.j
apply hsilocal_refines_smem_refines in LREF; auto.
rewrite <- LREF. auto.
2: { eauto.
all: intros; destruct z0, z2; auto.
-- split; simpl; auto.
destruct NEST as [|st0 se lse TOP NEST];
econstructor; simpl; auto; constructor; auto.
+ admit.
+ admit.
Admitted.
*)
(*Qed.*)
Global Opaque hsiexec_inst.
Local Hint Resolve hsiexec_inst_correct: wlp.
......
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