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

[Admitted checker] Checker expansion for reg Ocmp (without scratch)

parent 3104e551
......@@ -105,8 +105,8 @@ Definition addimm32 := opimm32 Paddw Paddiw.
Definition andimm32 := opimm32 Pandw Pandiw.
Definition orimm32 := opimm32 Porw Poriw.
Definition xorimm32 := opimm32 Pxorw Pxoriw.
(* TODO REMOVE Definition sltimm32 := opimm32 Psltw Psltiw.*)
(* TODO REMOVE Definition sltuimm32 := opimm32 Psltuw Psltiuw.*)
Definition sltimm32 := opimm32 Psltw Psltiw.
Definition sltuimm32 := opimm32 Psltuw Psltiuw.
Definition load_hilo64 (r: ireg) (hi lo: int64) k :=
if Int64.eq lo Int64.zero then Pluil r hi :: k
......@@ -132,8 +132,8 @@ Definition addimm64 := opimm64 Paddl Paddil.
Definition andimm64 := opimm64 Pandl Pandil.
Definition orimm64 := opimm64 Porl Poril.
Definition xorimm64 := opimm64 Pxorl Pxoril.
(* TODO REMOVE Definition sltimm64 := opimm64 Psltl Psltil.*)
(* TODO REMOVE Definition sltuimm64 := opimm64 Psltul Psltiul.*)
Definition sltimm64 := opimm64 Psltl Psltil.
Definition sltuimm64 := opimm64 Psltul Psltiul.
Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
if Ptrofs.eq_dec n Ptrofs.zero then
......@@ -145,7 +145,7 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
(** Translation of conditional branches. *)
(* TODO REMOVE Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
match cmp with
| Ceq => Pbeqw r1 r2 lbl
| Cne => Pbnew r1 r2 lbl
......@@ -203,7 +203,7 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
| Cle => (Pfles rd fs1 fs2, true)
| Cgt => (Pflts rd fs2 fs1, true)
| Cge => (Pfles rd fs2 fs1, true)
end.*)
end.
Definition apply_bin_r0_r0r0lbl (optR0: option bool) (sem: ireg0 -> ireg0 -> label -> instruction) (r1 r2: ireg0) (lbl: label) :=
match optR0 with
......@@ -222,7 +222,7 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru
Definition transl_cbranch
(cond: condition) (args: list mreg) (lbl: label) (k: code) :=
match cond, args with
(* TODO REMOVE | Ccomp c, a1 :: a2 :: nil =>
| Ccomp c, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (transl_cbranch_int32s c r1 r2 lbl :: k)
| Ccompu c, a1 :: a2 :: nil =>
......@@ -273,7 +273,7 @@ Definition transl_cbranch
| Cnotcompfs c, f1 :: f2 :: nil =>
do r1 <- freg_of f1; do r2 <- freg_of f2;
let (insn, normal) := transl_cond_single c X31 r1 r2 in
OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)*)
OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
| CEbeqw optR0, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
......@@ -319,7 +319,7 @@ Definition transl_cbranch
[rd] target register to 0 or 1 depending on the truth value of the
condition. *)
(* TODO REMOVE Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
match cmp with
| Ceq => Pseqw rd r1 r2 :: k
| Cne => Psnew rd r1 r2 :: k
......@@ -393,9 +393,9 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
match cmp with
| Clt => sltuimm64 rd r1 n k
| _ => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)
end. *)
end.
(* TODO REMOVE Definition transl_cond_op
Definition transl_cond_op
(cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
match cond, args with
| Ccomp c, a1 :: a2 :: nil =>
......@@ -440,7 +440,7 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
| _, _ =>
Error(msg "Asmgen.transl_cond_op")
end.*)
end.
(** Translation of the arithmetic operation [r <- op(args)].
The corresponding instructions are prepended to [k]. *)
......@@ -755,9 +755,9 @@ Definition transl_op
| Osingleoflongu, a1 :: nil =>
do rd <- freg_of res; do rs <- ireg_of a1;
OK (Pfcvtslu rd rs :: k)
(* TODO REMOVE | Ocmp cmp, _ =>
| Ocmp cmp, _ =>
do rd <- ireg_of res;
transl_cond_op cmp rd args k *)
transl_cond_op cmp rd args k
| OEseqw optR0, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
......
......@@ -161,7 +161,7 @@ Proof.
Qed.
Hint Resolve addptrofs_label: labels.
(* TODO REMOVE Remark transl_cond_float_nolabel:
Remark transl_cond_float_nolabel:
forall c r1 r2 r3 insn normal,
transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn.
Proof.
......@@ -173,14 +173,14 @@ Remark transl_cond_single_nolabel:
transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn.
Proof.
unfold transl_cond_single; intros. destruct c; inv H; exact I.
Qed.*)
Qed.
Remark transl_cbranch_label:
forall cond args lbl k c,
transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.
Proof.
intros. unfold transl_cbranch in H; destruct cond; TailNoLabel.
(* TODO REMOVE - destruct c0; simpl; TailNoLabel.
- destruct c0; simpl; TailNoLabel.
- destruct c0; simpl; TailNoLabel.
- destruct (Int.eq n Int.zero).
destruct c0; simpl; TailNoLabel.
......@@ -211,7 +211,7 @@ Proof.
destruct normal; TailNoLabel.
- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto.
destruct normal; TailNoLabel.*)
destruct normal; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
- destruct optR0 as [[]|]; TailNoLabel.
......@@ -226,7 +226,7 @@ Proof.
- destruct optR0 as [[]|]; TailNoLabel.
Qed.
(* TODO REMOVE Remark transl_cond_op_label:
Remark transl_cond_op_label:
forall cond args r k c,
transl_cond_op cond r args k = OK c -> tail_nolabel k c.
Proof.
......@@ -279,7 +279,7 @@ Proof.
- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto.
destruct normal; TailNoLabel.
Qed.*)
Qed.
Remark transl_op_label:
forall op args r k c,
......@@ -303,7 +303,7 @@ Opaque Int.eq.
- apply opimm64_label; intros; exact I.
- apply opimm64_label; intros; exact I.
- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
(* TODO REMOVE - eapply transl_cond_op_label; eauto.*)
- eapply transl_cond_op_label; eauto.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
- destruct optR0 as [[]|]; simpl; TailNoLabel.
......
......@@ -292,7 +292,7 @@ Qed.
(** Translation of conditional branches *)
(* TODO REMOVE Lemma transl_cbranch_int32s_correct:
Lemma transl_cbranch_int32s_correct:
forall cmp r1 r2 lbl (rs: regset) m b,
Val.cmp_bool cmp rs##r1 rs##r2 = Some b ->
exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m =
......@@ -375,7 +375,7 @@ Proof.
rewrite <- Float32.cmp_swap. auto.
- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
rewrite <- Float32.cmp_swap. auto.
Qed.*)
Qed.
(* TODO UNUSUED ? Remark branch_on_X31:
forall normal lbl (rs: regset) m b,
......@@ -417,7 +417,7 @@ Proof.
{ apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. }
clear EVAL MEXT AG.
destruct cond; simpl in TRANSL; ArgsInv.
(* TODO REMOVE - exists rs, (transl_cbranch_int32s c0 x x0 lbl).
- exists rs, (transl_cbranch_int32s c0 x x0 lbl).
intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
- exists rs, (transl_cbranch_int32u c0 x x0 lbl).
intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
......@@ -492,7 +492,7 @@ Proof.
econstructor; econstructor.
split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
split. rewrite V; destruct normal, b; reflexivity.
intros; Simpl.*)
intros; Simpl.
- destruct optR0 as [[]|];
unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
......@@ -589,7 +589,7 @@ Qed.
(** Translation of condition operators *)
(* TODO REMOVE Lemma transl_cond_int32s_correct:
Lemma transl_cond_int32s_correct:
forall cmp rd r1 r2 k rs m,
exists rs',
exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m
......@@ -984,7 +984,7 @@ Proof.
* econstructor; split.
apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
split; intros; Simpl.
Qed.*)
Qed.
(** Some arithmetic properties. *)
......@@ -1195,8 +1195,8 @@ Opaque Int.eq.
apply exec_straight_one. simpl; reflexivity. auto.
split; intros; Simpl. }
(* cond *)
(* TODO REMOVE { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
exists rs'; split. eexact A. eauto with asmgen. }*)
{ exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
exists rs'; split. eexact A. eauto with asmgen. }
(* Expanded instructions from RTL *)
5: econstructor; split; try apply exec_straight_one; simpl; eauto;
split; intros; Simpl; rewrite Int.add_commut; auto.
......
......@@ -284,7 +284,7 @@ let expanse_condimm_int32u cmp a1 n dest succ k =
(cond_int32u false cmp a1 (r2p ()) dest succ k)
let expanse_condimm_int64s cmp a1 n dest succ k =
if Int.eq n Int.zero then cond_int64s true cmp a1 a1 dest succ k
if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k
else
match cmp with
| Ceq | Cne ->
......@@ -391,14 +391,14 @@ let expanse (sb : superblock) code pm =
debug "Iop/Ccompu\n";
exp := cond_int32u false c a1 a2 dest succ [];
was_exp := true
| Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
(*| Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccompimm\n";
exp := expanse_condimm_int32s c a1 imm dest succ [];
was_exp := true
| Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccompuimm\n";
exp := expanse_condimm_int32u c a1 imm dest succ [];
was_exp := true
was_exp := true*)
| Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
debug "Iop/Ccompl\n";
exp := cond_int64s false c a1 a2 dest succ [];
......@@ -407,14 +407,14 @@ let expanse (sb : superblock) code pm =
debug "Iop/Ccomplu\n";
exp := cond_int64u false c a1 a2 dest succ [];
was_exp := true
| Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
(*| Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccomplimm\n";
exp := expanse_condimm_int64s c a1 imm dest succ [];
was_exp := true
| Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccompluimm\n";
exp := expanse_condimm_int64u c a1 imm dest succ [];
was_exp := true
was_exp := true*)
| Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
debug "Iop/Ccompf\n";
exp := expanse_cond_fp false cond_float c f1 f2 dest succ [];
......@@ -431,7 +431,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;
......@@ -491,7 +491,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;
......
......@@ -7,6 +7,7 @@ Require Import RTL RTLpath.
Require Import Errors.
Require Import RTLpathSE_theory RTLpathLivegenproof.
Require Import Axioms RTLpathSE_simu_specs.
Require Import Asmgen.
Local Open Scope error_monad_scope.
Local Open Scope option_monad_scope.
......@@ -22,7 +23,7 @@ Import ListNotations.
Local Open Scope list_scope.
Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := RET tt. (* TO REMOVE DEBUG INFO *)
(* Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := DO s <~ k x;; println ("DEBUG simu_check:" +; s). (* TO INSERT DEBUG INFO *) *)
(*Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := DO s <~ k x;; println ("DEBUG simu_check:" +; s). (* TO INSERT DEBUG INFO *)*)
Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s).
......@@ -596,16 +597,252 @@ Proof.
explore; try congruence.
Qed.
Definition is_inv_cmp_int (cmp: comparison) : bool :=
match cmp with | Cle | Cgt => true | _ => false end.
Definition is_inv_cmp_float (cmp: comparison) : bool :=
match cmp with | Cge | Cgt => true | _ => false end.
Definition make_optR0 (is_x0 is_inv: bool) : option bool :=
if is_x0 then Some is_inv else None.
(* TODO IF NEEDED LATER Fixpoint hlist_sval (l: list hsval): ?? list_hsval :=
match l with
| nil => hSnil()
| r::l =>
DO lhsv <~ hlist_sval l;;
hScons r lhsv
end.*)
Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : ?? list_hsval :=
DO hnil <~ hSnil();;
let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in
DO lhsv <~ hScons hvfirst hnil;;
DO lhsv <~ hScons hvsec lhsv;;
RET lhsv.
Definition make_lhsv_single (hvs: hsval) : ?? list_hsval :=
DO hnil <~ hSnil();;
DO hl <~ hScons hvs hnil;;
RET hl.
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 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 xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
match cmp with
| Ceq => hSop (OEseqw optR0) lhsv
| Cne => hSop (OEsnew optR0) lhsv
| Clt | Cgt => hSop (OEsltw optR0) lhsv
| Cle | Cge=>
DO hvs <~ (hSop (OEsltw optR0) lhsv);;
DO hl <~ make_lhsv_single hvs;;
hSop (OExoriw Int.one) hl
end.
Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
match cmp with
| Ceq => hSop (OEseqw optR0) lhsv
| Cne => hSop (OEsnew 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 (OEseql optR0) lhsv
| Cne => hSop (OEsnel 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_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.
(** simplify a symbolic value before assignment to a register *)
Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval :=
match rsv with
| Rop op =>
match is_move_operation op lr with
| Some arg => hsi_sreg_get hst arg (** optimization of Omove *)
| None =>
DO lhsv <~ hlist_args hst lr;;
hSop op lhsv
end
(*match is_move_operation op lr with*)
(*| Some arg => hsi_sreg_get hst arg [>* optimization of Omove <]*)
(*| None =>*)
(*DO lhsv <~ hlist_args hst lr;;*)
(*hSop op lhsv*)
(*end;;*)
match op, lr with
| Ocmp (Ccomp c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int32s c lhsv optR0
| Ocmp (Ccompu c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int32u c lhsv optR0
| Ocmp (Ccompl c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int64s c lhsv optR0
| Ocmp (Ccomplu c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int64u c lhsv optR0
| Ocmp (Ccompf c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp false cond_float c lhsv
| Ocmp (Cnotcompf c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp true cond_float c lhsv
| Ocmp (Ccompfs c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp false cond_single c lhsv
| Ocmp (Cnotcompfs c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
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
(*| Ocmp (Ccomplimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64s c hv1 imm*)
| _, _ =>
DO lhsv <~ hlist_args hst lr;;
hSop op lhsv
end
| Rload _ chunk addr =>
DO lhsv <~ hlist_args hst lr;;
hSload hst NOTRAP chunk addr lhsv
......@@ -618,8 +855,15 @@ Lemma simplify_correct rsv lr hst:
(OK1: seval_sval ge sp (rsv lr st) rs0 m0 <> None),
sval_refines ge sp rs0 m0 hv (rsv lr st).
Proof.
destruct rsv; simpl; auto.
- (* Rop *)
(* destruct rsv; simpl; auto.
- destruct op; wlp_simplify.
try (generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0;
destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto;
intro H0; clear H0; simplify_SOME z; congruence). (* absurd case *)
erewrite H0; eauto. simplify_SOME args.
intros. congruence. eauto.
destruct (is_move_operation _ _) eqn: Hmove; wlp_simplify.
+ exploit is_move_operation_correct; eauto.
intros (Hop & Hlsv); subst; simpl in *.
......@@ -640,7 +884,7 @@ Proof.
destruct (eval_addressing _ _ _ _) as [a|] eqn: Ha; try congruence.
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
destruct (Mem.loadv _ _ _); try congruence.
Qed.
Qed.*) Admitted.
Global Opaque simplify.
Local Hint Resolve simplify_correct: wlp.
......@@ -708,7 +952,7 @@ Lemma hslocal_set_sreg_correct hst r rsv lr:
WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN forall ge sp rs0 m0 st
(REF: hsilocal_refines ge sp rs0 m0 hst st),
hsilocal_refines ge sp rs0 m0 hst' (slocal_set_sreg st r (rsv lr st)).
Proof.
Proof. (* TODO
wlp_simplify.
+ (* may_trap ~> true *)
assert (X: sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) <->
......@@ -740,7 +984,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.