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

Important commit on expansions' mini CSE, and a draft for addptrofs

parent df9aab80
......@@ -868,7 +868,8 @@ Qed.
Remark transl_destroyed_by_op:
forall op e, destroyed_by_op (transl_op e op) = destroyed_by_op op.
Proof.
intros; destruct op; reflexivity.
intros; destruct op; try reflexivity; simpl.
all: destruct optR as [[]|]; simpl; try reflexivity.
Qed.
Remark transl_destroyed_by_load:
......
......@@ -982,6 +982,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
end
| Pbuiltin ef args res =>
Stuck (**r treated specially below *)
| Pnop => Next (nextinstr rs) m (**r Pnop is used by an oracle during expansion *)
(** The following instructions and directives are not generated directly by Asmgen,
so we do not model them. *)
......@@ -1002,7 +1003,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pfmsubd _ _ _ _
| Pfnmaddd _ _ _ _
| Pfnmsubd _ _ _ _
| Pnop
=> Stuck
end.
......
......@@ -204,19 +204,23 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
| Cgt => (Pflts rd fs2 fs1, true)
| Cge => (Pfles rd fs2 fs1, true)
end.
(** Functions to select a special register according to the op "oreg" argument from RTL *)
Definition apply_bin_oreg_ireg0 (optR: option oreg) (r1 r2: ireg0): (ireg0 * ireg0) :=
match optR with
| None => (r1, r2)
| Some X0_L => (X0, r1)
| Some X0_R => (r1, X0)
| Some SP_S => (X SP, r1)
end.
Definition get_opimmR0 (rd: ireg) (opi: opimm) :=
match opi with
| OPimmADD i => Paddiw rd X0 i
| OPimmADDL i => Paddil rd X0 i
end.
Definition get_oreg (optR: option oreg) (r: ireg0) :=
match optR with
| Some SP_S => X SP
| Some X0_L | Some X0_R => X0
| _ => r
end.
Definition transl_cbranch
(cond: condition) (args: list mreg) (lbl: label) (k: code) :=
......@@ -785,9 +789,8 @@ Definition transl_op
| Ocmp cmp, _ =>
do rd <- ireg_of res;
transl_cond_op cmp rd args k
| OEimmR0 opi, nil =>
do rd <- ireg_of res;
OK (get_opimmR0 rd opi :: k)
(* Instructions expanded in RTL *)
| OEseqw optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
......@@ -839,10 +842,21 @@ Definition transl_op
| OEluiw n, nil =>
do rd <- ireg_of res;
OK (Pluiw rd n :: k)
| OEaddiw n, a1 :: nil =>
| OEaddiw optR n, nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
let rs := get_oreg optR X0 in
OK (Paddiw rd rs n :: k)
| OEaddiw (Some SP_S) n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
if Int.eq n Int.zero then
OK (Paddw rd SP rs :: k)
else Error (msg "Asmgen.transl_op")
| OEaddiw optR n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
let rs' := get_oreg optR rs in
OK (Paddiw rd rs' n :: k)
| OEandiw n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
......@@ -902,10 +916,21 @@ Definition transl_op
| OEluil n, nil =>
do rd <- ireg_of res;
OK (Pluil rd n :: k)
| OEaddil n, a1 :: nil =>
| OEaddil optR n, nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
let rs := get_oreg optR X0 in
OK (Paddil rd rs n :: k)
| OEaddil (Some SP_S) n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
if Int64.eq n Int64.zero then
OK (Paddl rd SP rs :: k)
else Error (msg "Asmgen.transl_op")
| OEaddil optR n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
let rs' := get_oreg optR rs in
OK (Paddil rd rs' n :: k)
| OEandil n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
......@@ -947,6 +972,13 @@ Definition transl_op
do r1 <- freg_of f1;
do r2 <- freg_of f2;
OK (Pfles rd r1 r2 :: k)
| OEmayundef _, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do r2 <- ireg_of a2;
if ireg_eq rd r2 then
OK (Pnop :: k)
else
OK (Pmv rd r2 :: k)
| Obits_of_single, a1 :: nil =>
do rd <- ireg_of res; do rs <- freg_of a1;
......
......@@ -308,7 +308,8 @@ Opaque Int.eq.
- apply opimm64_label; intros; exact I.
- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
- eapply transl_cond_op_label; eauto.
- destruct opi; simpl; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
......
......@@ -529,31 +529,37 @@ Proof.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
......@@ -591,31 +597,37 @@ Proof.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
Qed.
......@@ -1262,12 +1274,7 @@ Opaque Int.eq.
{ exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
exists rs'; split. eexact A. eauto with asmgen. }
(* Expanded instructions from RTL *)
{ unfold get_opimmR0; destruct opi; simpl;
econstructor; split; try apply exec_straight_one; simpl; eauto;
split; intros; Simpl.
try rewrite Int.add_commut; auto.
try rewrite Int64.add_commut; auto. }
7,8,9,16,17,18:
8,9,17,18:
econstructor; split; try apply exec_straight_one; simpl; eauto;
split; intros; Simpl; try destruct (rs x0);
try rewrite Int64.add_commut;
......@@ -1276,12 +1283,41 @@ Opaque Int.eq.
try rewrite Int.and_commut; auto;
try rewrite Int64.or_commut;
try rewrite Int.or_commut; auto.
1-12:
destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; inv EQ3;
1-14:
destruct optR as [[]|]; try discriminate;
try (ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl);
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; try inv EQ3; try inv EQ2;
try destruct (Int.eq _ _) eqn:A; try inv H0;
try destruct (Int64.eq _ _) eqn:A; try inv H1;
econstructor; split; try apply exec_straight_one; simpl; eauto;
split; intros; Simpl;
destruct (rs x0); auto;
destruct (rs x1); auto.
try apply Int.same_if_eq in A; subst;
try apply Int64.same_if_eq in A; subst;
unfold get_sp;
try destruct (rs x0); auto;
try destruct (rs x1); auto;
try destruct (rs X2); auto;
try destruct Archi.ptr64 eqn:B;
try fold (Val.add (Vint Int.zero) (get_sp (rs X2)));
try fold (Val.addl (Vlong Int64.zero) (get_sp (rs X2)));
try rewrite Val.add_commut; auto;
try rewrite Val.addl_commut; auto;
try rewrite Int.add_commut; auto;
try rewrite Int64.add_commut; auto;
replace (Ptrofs.of_int Int.zero) with (Ptrofs.zero) by auto;
replace (Ptrofs.of_int64 Int64.zero) with (Ptrofs.zero) by auto;
try rewrite Ptrofs.add_zero; auto.
(* mayundef *)
{ destruct (ireg_eq x x0); inv EQ2;
econstructor; split;
try apply exec_straight_one; simpl; eauto;
split; unfold eval_may_undef;
destruct mu eqn:EQMU; simpl; intros; Simpl; auto.
all:
destruct (rs (preg_of m0)) eqn:EQM0; simpl; auto;
destruct (rs x0); simpl; auto; Simpl;
try destruct (Int.ltu _ _); simpl;
Simpl; auto. }
(* select *)
{ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
split; intros; Simpl.
......
This diff is collapsed.
......@@ -87,7 +87,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv)
| Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv)
| Ocmp c => needs_of_condition c
| OEimmR0 _ => op1 (default nv)
| OEmoveSP => nil
| OEseqw _ => op2 (default nv)
| OEsnew _ => op2 (default nv)
| OEsequw _ => op2 (default nv)
......@@ -98,7 +98,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| OEsltiuw _ => op1 (default nv)
| OExoriw _ => op1 (bitwise nv)
| OEluiw _ => op1 (default nv)
| OEaddiw _ => op1 (default nv)
| OEaddiw _ _ => op1 (default nv)
| OEandiw n => op1 (andimm nv n)
| OEoriw n => op1 (orimm nv n)
| OEseql _ => op2 (default nv)
......@@ -111,7 +111,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| OEsltiul _ => op1 (default nv)
| OExoril _ => op1 (default nv)
| OEluil _ => op1 (default nv)
| OEaddil _ => op1 (default nv)
| OEaddil _ _ => op1 (default nv)
| OEandil _ => op1 (default nv)
| OEoril _ => op1 (default nv)
| OEloadli _ => op1 (default nv)
......
This diff is collapsed.
......@@ -36,14 +36,16 @@ let mu_name pp = function
| MUshrx i -> fprintf pp "MUshrx(%ld)" (camlint_of_coqint i)
| MUshrxl i -> fprintf pp "MUshrxl(%ld)" (camlint_of_coqint i)
let get_immR0 pp = function
| OPimmADD i -> fprintf pp "OPimmADD(%ld)" (camlint_of_coqint i)
| OPimmADDL i -> fprintf pp "OPimmADDL(%ld)" (camlint_of_coqint i)
let get_optR_s c reg pp r1 r2 = function
| None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2
| Some X0_L -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1
| Some X0_R -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c)
| Some SP_S -> failwith "PrintOp: SP_S in get_optR_s instruction (problem with RTL expansions?)"
let get_optR_a pp = function
| None -> failwith "PrintOp: None in get_optR_a instruction (problem with RTL expansions?)"
| Some X0_L | Some X0_R -> fprintf pp "X0"
| Some SP_S -> fprintf pp "SP"
let print_condition reg pp = function
| (Ccomp c, [r1;r2]) ->
......@@ -203,7 +205,6 @@ let print_operation reg pp = function
| Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1
| Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1
| Ocmp c, args -> print_condition reg pp (c, args)
| OEimmR0 opi, [] -> fprintf pp "OEimmR0(%a)" get_immR0 opi
| OEseqw optR, [r1;r2] -> fprintf pp "OEseqw"; (get_optR_s Ceq reg pp r1 r2 optR)
| OEsnew optR, [r1;r2] -> fprintf pp "OEsnew"; (get_optR_s Cne reg pp r1 r2 optR)
| OEsequw optR, [r1;r2] -> fprintf pp "OEsequw"; (get_optR_s Ceq reg pp r1 r2 optR)
......@@ -214,7 +215,8 @@ let print_operation reg pp = function
| OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
| OEaddiw n, [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEaddiw (optR, n), [] -> fprintf pp "OEaddiw(%a,%ld)" get_optR_a optR (camlint_of_coqint n)
| OEaddiw (optR, n), [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEandiw n, [r1] -> fprintf pp "OEandiw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEoriw n, [r1] -> fprintf pp "OEoriw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEseql optR, [r1;r2] -> fprintf pp "OEseql"; (get_optR_s Ceq reg pp r1 r2 optR)
......@@ -227,7 +229,8 @@ let print_operation reg pp = function
| OEsltiul n, [r1] -> fprintf pp "OEsltiul(%a,%ld)" reg r1 (camlint_of_coqint n)
| OExoril n, [r1] -> fprintf pp "OExoril(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n)
| OEaddil n, [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEaddil (optR, n), [] -> fprintf pp "OEaddil(%a,%ld)" get_optR_a optR (camlint_of_coqint n)
| OEaddil (optR, n), [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n)
| 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)
......
......@@ -30,9 +30,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 *)
(** ** Immediate loads *)
Definition load_hilo32 (hi lo: int) :=
if Int.eq lo Int.zero then
......@@ -40,7 +40,7 @@ Definition load_hilo32 (hi lo: int) :=
else
let hvs := fSop (OEluiw hi) fSnil in
let hl := make_lhsv_single hvs in
fSop (OEaddiw lo) hl.
fSop (OEaddiw None lo) hl.
Definition load_hilo64 (hi lo: int64) :=
if Int64.eq lo Int64.zero then
......@@ -48,19 +48,19 @@ Definition load_hilo64 (hi lo: int64) :=
else
let hvs := fSop (OEluil hi) fSnil in
let hl := make_lhsv_single hvs in
fSop (OEaddil lo) hl.
fSop (OEaddil None lo) hl.
Definition loadimm32 (n: int) :=
match make_immed32 n with
| Imm32_single imm =>
fSop (OEimmR0 (OPimmADD imm)) fSnil
fSop (OEaddiw (Some X0_R) imm) fSnil
| Imm32_pair hi lo => load_hilo32 hi lo
end.
Definition loadimm64 (n: int64) :=
match make_immed64 n with
| Imm64_single imm =>
fSop (OEimmR0 (OPimmADDL imm)) fSnil
fSop (OEaddil (Some X0_R) imm) fSnil
| Imm64_pair hi lo => load_hilo64 hi lo
| Imm64_large imm => fSop (OEloadli imm) fSnil
end.
......@@ -91,20 +91,20 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper
fSop op hl
end.
Definition addimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oadd OEaddiw.
Definition addimm32 (hv1: hsval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or).
Definition andimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oand OEandiw.
Definition orimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oor OEoriw.
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 addimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oaddl OEaddil.
Definition addimm64 (hv1: hsval) (n: int64) (or: option oreg) := opimm64 hv1 n Oaddl (OEaddil or).
Definition andimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oandl OEandil.
Definition orimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oorl OEoril.
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 *)
(** ** Comparisons intructions *)
Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) :=
match cmp with
......@@ -260,7 +260,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.
(* Branches instructions *)
(** ** Branches instructions *)
Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) :=
match cmp with
......@@ -309,18 +309,37 @@ Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (con
let hl := make_lhsv_cmp false hvs hvs in
if normal' then ((CEbnew (Some X0_R)), hl) else ((CEbeqw (Some X0_R)), hl).
(** Add pointer expansion *)
(** ** Add pointer expansion *)
(*Definition addptrofs (hv1: hsval) (n: ptrofs) :=*)
(*if Ptrofs.eq_dec n Ptrofs.zero then*)
(*let lhsv := make_lhsv_single hv1 in*)
(*fSop Omove lhsv*)
(*else*)
(*if Archi.ptr64*)
(*then addimm64 hv1 (Ptrofs.to_int64 n)*)
(*else addimm32 hv1 (Ptrofs.to_int n).*)
(** Target op simplifications using "fake" values *)
Definition addptrofs (n: ptrofs) :=
if Ptrofs.eq_dec n Ptrofs.zero then
fSop OEmoveSP fSnil
else
if Archi.ptr64
then (
match make_immed64 (Ptrofs.to_int64 n) with
| Imm64_single imm =>
fSop (OEaddil (Some SP_S) imm) fSnil
| Imm64_pair hi lo =>
let hvs := load_hilo64 hi lo in
let hl := make_lhsv_single hvs in
fSop (OEaddil (Some SP_S) Int64.zero) hl
| Imm64_large imm =>
let hvs := fSop (OEloadli imm) fSnil in
let hl := make_lhsv_single hvs in
fSop (OEaddil (Some SP_S) Int64.zero) hl
end)
else (
match make_immed32 (Ptrofs.to_int n) with
| Imm32_single imm =>
fSop (OEaddiw (Some SP_S) imm) fSnil
| Imm32_pair hi lo =>
let hvs := load_hilo32 hi lo in
let hl := make_lhsv_single hvs in
fSop (OEaddiw (Some SP_S) Int.zero) hl
end).
(** * Target simplifications using "fake" values *)
Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
match op, lr with
......@@ -402,10 +421,10 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
Some (loadimm64 n)
| Oaddimm n, a1 :: nil =>
let hv1 := fsi_sreg_get hst a1 in
Some (addimm32 hv1 n)
Some (addimm32 hv1 n None)
| Oaddlimm n, a1 :: nil =>
let hv1 := fsi_sreg_get hst a1 in
Some (addimm64 hv1 n)
Some (addimm64 hv1 n None)
| Oandimm n, a1 :: nil =>
let hv1 := fsi_sreg_get hst a1 in
Some (andimm32 hv1 n)
......@@ -442,9 +461,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
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_cmp false move_s move_s in
Some (fSop (OEmayundef (MUshrx n)) move_l)
let lhl := make_lhsv_cmp false hv1 hv1 in
Some (fSop (OEmayundef (MUshrx n)) lhl)
else
if Int.eq n Int.one then
let srliw_s := fSop (Oshruimm (Int.repr 31)) hl in
......@@ -468,9 +486,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
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_cmp false move_s move_s in
Some (fSop (OEmayundef (MUshrxl n)) move_l)
let lhl := make_lhsv_cmp false hv1 hv1 in
Some (fSop (OEmayundef (MUshrxl n)) lhl)
else
if Int.eq n Int.one then
let srlil_s := fSop (Oshrluimm (Int.repr 63)) hl in
......@@ -490,9 +507,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
let srail_s' := fSop (Oshrlimm n) addl_l in
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)*)
(* TODO gourdinl | Oaddrstack n, nil =>*)
(*Some (addptrofs n)*)
| _, _ => None
end.
......@@ -601,9 +617,9 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
| _, _ => None
end.
(** Auxiliary lemmas on comparisons *)
(** * Auxiliary lemmas on comparisons *)
(* Signed ints *)
(** ** Signed ints *)
Lemma xor_neg_ltle_cmp: forall v1 v2,
Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
......@@ -618,7 +634,7 @@ Proof.
auto.
Qed.
(* Unsigned ints *)
(** ** 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)) =
......@@ -652,7 +668,7 @@ Proof.
rewrite !Int.unsigned_repr; try cbn; try omega.
Qed.
(* Signed longs *)
(** ** Signed longs *)
Lemma xor_neg_ltle_cmpl: forall v1 v2,
Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) =
......@@ -748,7 +764,7 @@ Proof.
apply Z.le_ge. trivial.
Qed.
(* Unsigned longs *)
(** ** 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)) =
......@@ -794,7 +810,7 @@ Proof.
repeat destruct (_ && _); simpl; auto.
Qed.
(* Floats *)
(** ** Floats *)
Lemma xor_neg_eqne_cmpf: forall v1 v2,
Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) =
......@@ -807,7 +823,7 @@ Proof.
destruct (Float.cmp _ _ _); simpl; auto.
Qed.
(* Singles *)
(** ** Singles *)
Lemma xor_neg_eqne_cmpfs: forall v1 v2,
Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) =
......@@ -820,7 +836,7 @@ Proof.
destruct (Float32.cmp _ _ _); simpl; auto.
Qed.
(* More useful lemmas *)