Module Asmgenproof1
Decomposition of integer constants.
Lemma make_immed32_sound:
forall n,
match make_immed32 n with
| Imm32_single imm => n = imm
| Imm32_pair hi lo => n = Int.add (Int.shl hi (Int.repr 12)) lo
end.
Proof.
Lemma make_immed64_sound:
forall n,
match make_immed64 n with
| Imm64_single imm => n = imm
| Imm64_pair hi lo => n = Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo
| Imm64_large imm => n = imm
end.
Proof.
Properties of registers
Lemma ireg_of_not_X31:
forall m r, ireg_of m = OK r -> IR r <> IR X31.
Proof.
intros.
erewrite <-
ireg_of_eq;
eauto with asmgen.
Qed.
Lemma ireg_of_not_X31':
forall m r, ireg_of m = OK r -> r <> X31.
Proof.
Global Hint Resolve ireg_of_not_X31 ireg_of_not_X31': asmgen.
Useful simplification tactic
Ltac Simplif :=
((rewrite nextinstr_inv by eauto with asmgen)
|| (rewrite nextinstr_inv1 by eauto with asmgen)
|| (rewrite Pregmap.gss)
|| (rewrite nextinstr_pc)
|| (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen.
Ltac Simpl := repeat Simplif.
Correctness of RISC-V constructor functions
Section CONSTRUCTORS.
Variable ge: genv.
Variable fn: function.
32-bit integer constants and arithmetic
Lemma load_hilo32_correct:
forall rd hi lo k rs m,
exists rs',
exec_straight ge fn (load_hilo32 rd hi lo k) rs m k rs' m
/\ rs'#rd = Vint (Int.add (Int.shl hi (Int.repr 12)) lo)
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
Lemma loadimm32_correct:
forall rd n k rs m,
exists rs',
exec_straight ge fn (loadimm32 rd n k) rs m k rs' m
/\ rs'#rd = Vint n
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
Lemma opimm32_correct:
forall (op: ireg -> ireg0 -> ireg0 -> instruction)
(opi: ireg -> ireg0 -> int -> instruction)
(sem: val -> val -> val) m,
(forall d s1 s2 rs,
exec_instr ge fn (op d s1 s2) rs m = Next (nextinstr (rs#d <- (sem rs##s1 rs##s2))) m) ->
(forall d s n rs,
exec_instr ge fn (opi d s n) rs m = Next (nextinstr (rs#d <- (sem rs##s (Vint n)))) m) ->
forall rd r1 n k rs,
r1 <> X31 ->
exists rs',
exec_straight ge fn (opimm32 op opi rd r1 n k) rs m k rs' m
/\ rs'#rd = sem rs##r1 (Vint n)
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
64-bit integer constants and arithmetic
Lemma load_hilo64_correct:
forall rd hi lo k rs m,
exists rs',
exec_straight ge fn (load_hilo64 rd hi lo k) rs m k rs' m
/\ rs'#rd = Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo)
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
Lemma loadimm64_correct:
forall rd n k rs m,
exists rs',
exec_straight ge fn (loadimm64 rd n k) rs m k rs' m
/\ rs'#rd = Vlong n
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma opimm64_correct:
forall (op: ireg -> ireg0 -> ireg0 -> instruction)
(opi: ireg -> ireg0 -> int64 -> instruction)
(sem: val -> val -> val) m,
(forall d s1 s2 rs,
exec_instr ge fn (op d s1 s2) rs m = Next (nextinstr (rs#d <- (sem rs###s1 rs###s2))) m) ->
(forall d s n rs,
exec_instr ge fn (opi d s n) rs m = Next (nextinstr (rs#d <- (sem rs###s (Vlong n)))) m) ->
forall rd r1 n k rs,
r1 <> X31 ->
exists rs',
exec_straight ge fn (opimm64 op opi rd r1 n k) rs m k rs' m
/\ rs'#rd = sem rs##r1 (Vlong n)
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
Add offset to pointer
Lemma addptrofs_correct:
forall rd r1 n k rs m,
r1 <> X31 ->
exists rs',
exec_straight ge fn (addptrofs rd r1 n k) rs m k rs' m
/\ Val.lessdef (Val.offset_ptr rs#r1 n) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma addptrofs_correct_2:
forall rd r1 n k (rs: regset) m b ofs,
r1 <> X31 -> rs#r1 = Vptr b ofs ->
exists rs',
exec_straight ge fn (addptrofs rd r1 n k) rs m k rs' m
/\ rs'#rd = Vptr b (Ptrofs.add ofs n)
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
intros.
exploit (
addptrofs_correct rd r1 n);
eauto.
intros (
rs' &
A &
B &
C).
exists rs';
intuition eauto.
rewrite H0 in B.
inv B.
auto.
Qed.
Translation of conditional branches
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 =
eval_branch fn lbl rs m (Some b).
Proof.
intros.
destruct cmp;
simpl;
rewrite ?
H.
-
destruct rs##
r1;
simpl in H;
try discriminate.
destruct rs##
r2;
inv H.
simpl;
auto.
-
destruct rs##
r1;
simpl in H;
try discriminate.
destruct rs##
r2;
inv H.
simpl;
auto.
-
auto.
-
rewrite <-
Val.swap_cmp_bool.
simpl.
rewrite H;
auto.
-
rewrite <-
Val.swap_cmp_bool.
simpl.
rewrite H;
auto.
-
auto.
Qed.
Lemma transl_cbranch_int32u_correct:
forall cmp r1 r2 lbl (rs: regset) m b,
Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b ->
exec_instr ge fn (transl_cbranch_int32u cmp r1 r2 lbl) rs m =
eval_branch fn lbl rs m (Some b).
Proof.
Lemma transl_cbranch_int64s_correct:
forall cmp r1 r2 lbl (rs: regset) m b,
Val.cmpl_bool cmp rs###r1 rs###r2 = Some b ->
exec_instr ge fn (transl_cbranch_int64s cmp r1 r2 lbl) rs m =
eval_branch fn lbl rs m (Some b).
Proof.
intros.
destruct cmp;
simpl;
rewrite ?
H.
-
destruct rs###
r1;
simpl in H;
try discriminate.
destruct rs###
r2;
inv H.
simpl;
auto.
-
destruct rs###
r1;
simpl in H;
try discriminate.
destruct rs###
r2;
inv H.
simpl;
auto.
-
auto.
-
rewrite <-
Val.swap_cmpl_bool.
simpl.
rewrite H;
auto.
-
rewrite <-
Val.swap_cmpl_bool.
simpl.
rewrite H;
auto.
-
auto.
Qed.
Lemma transl_cbranch_int64u_correct:
forall cmp r1 r2 lbl (rs: regset) m b,
Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b ->
exec_instr ge fn (transl_cbranch_int64u cmp r1 r2 lbl) rs m =
eval_branch fn lbl rs m (Some b).
Proof.
Lemma transl_cond_float_correct:
forall (rs: regset) m cmp rd r1 r2 insn normal v,
transl_cond_float cmp rd r1 r2 = (insn, normal) ->
v = (if normal then Val.cmpf cmp rs#r1 rs#r2 else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) ->
exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
Proof.
Lemma transl_cond_single_correct:
forall (rs: regset) m cmp rd r1 r2 insn normal v,
transl_cond_single cmp rd r1 r2 = (insn, normal) ->
v = (if normal then Val.cmpfs cmp rs#r1 rs#r2 else Val.notbool (Val.cmpfs cmp rs#r1 rs#r2)) ->
exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
Proof.
Ltac ArgsInv :=
repeat (match goal with
| [ H: Error _ = OK _ |- _ ] => discriminate
| [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args
| [ H: bind _ _ = OK _ |- _ ] => monadInv H
| [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
| [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
end);
subst;
repeat (match goal with
| [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *
| [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *
end).
Lemma transl_cbranch_correct_1:
forall cond args lbl k c m ms b sp rs m',
transl_cbranch cond args lbl k = OK c ->
eval_condition cond (List.map ms args) m = Some b ->
agree ms sp rs ->
Mem.extends m m' ->
exists rs', exists insn,
exec_straight_opt ge fn c rs m' (insn :: k) rs' m'
/\ exec_instr ge fn insn rs' m' = eval_branch fn lbl rs' m' (Some b)
/\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
Proof.
intros until m';
intros TRANSL EVAL AG MEXT.
set (
vl' :=
map rs (
map preg_of args)).
assert (
EVAL':
eval_condition cond vl' m' =
Some b).
{
apply eval_condition_lessdef with (
map ms args)
m;
auto.
eapply preg_vals;
eauto. }
clear EVAL MEXT AG.
destruct cond;
simpl in TRANSL;
ArgsInv.
-
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.
-
predSpec Int.eq Int.eq_spec n Int.zero.
+
subst n.
exists rs, (
transl_cbranch_int32s c0 x X0 lbl).
intuition auto.
constructor.
apply transl_cbranch_int32s_correct;
auto.
+
exploit (
loadimm32_correct X31 n);
eauto.
intros (
rs' &
A &
B &
C).
exists rs', (
transl_cbranch_int32s c0 x X31 lbl).
split.
constructor;
eexact A.
split;
auto.
apply transl_cbranch_int32s_correct;
auto.
simpl;
rewrite B,
C;
eauto with asmgen.
-
predSpec Int.eq Int.eq_spec n Int.zero.
+
subst n.
exists rs, (
transl_cbranch_int32u c0 x X0 lbl).
intuition auto.
constructor.
apply transl_cbranch_int32u_correct;
auto.
+
exploit (
loadimm32_correct X31 n);
eauto.
intros (
rs' &
A &
B &
C).
exists rs', (
transl_cbranch_int32u c0 x X31 lbl).
split.
constructor;
eexact A.
split;
auto.
apply transl_cbranch_int32u_correct;
auto.
simpl;
rewrite B,
C;
eauto with asmgen.
-
exists rs, (
transl_cbranch_int64s c0 x x0 lbl).
intuition auto.
constructor.
apply transl_cbranch_int64s_correct;
auto.
-
exists rs, (
transl_cbranch_int64u c0 x x0 lbl).
intuition auto.
constructor.
apply transl_cbranch_int64u_correct;
auto.
-
predSpec Int64.eq Int64.eq_spec n Int64.zero.
+
subst n.
exists rs, (
transl_cbranch_int64s c0 x X0 lbl).
intuition auto.
constructor.
apply transl_cbranch_int64s_correct;
auto.
+
exploit (
loadimm64_correct X31 n);
eauto.
intros (
rs' &
A &
B &
C).
exists rs', (
transl_cbranch_int64s c0 x X31 lbl).
split.
constructor;
eexact A.
split;
auto.
apply transl_cbranch_int64s_correct;
auto.
simpl;
rewrite B,
C;
eauto with asmgen.
-
predSpec Int64.eq Int64.eq_spec n Int64.zero.
+
subst n.
exists rs, (
transl_cbranch_int64u c0 x X0 lbl).
intuition auto.
constructor.
apply transl_cbranch_int64u_correct;
auto.
+
exploit (
loadimm64_correct X31 n);
eauto.
intros (
rs' &
A &
B &
C).
exists rs', (
transl_cbranch_int64u c0 x X31 lbl).
split.
constructor;
eexact A.
split;
auto.
apply transl_cbranch_int64u_correct;
auto.
simpl;
rewrite B,
C;
eauto with asmgen.
-
destruct (
transl_cond_float c0 X31 x x0)
as [
insn normal]
eqn:
TC;
inv EQ2.
set (
v :=
if normal then Val.cmpf c0 rs#
x rs#
x0 else Val.notbool (
Val.cmpf c0 rs#
x rs#
x0)).
assert (
V:
v =
Val.of_bool (
eqb normal b)).
{
unfold v,
Val.cmpf.
rewrite EVAL'.
destruct normal,
b;
reflexivity. }
econstructor;
econstructor.
split.
constructor.
apply exec_straight_one.
eapply transl_cond_float_correct with (
v :=
v);
eauto.
auto.
split.
rewrite V;
destruct normal,
b;
reflexivity.
intros;
Simpl.
-
destruct (
transl_cond_float c0 X31 x x0)
as [
insn normal]
eqn:
TC;
inv EQ2.
assert (
EVAL'':
Val.cmpf_bool c0 (
rs x) (
rs x0) =
Some (
negb b)).
{
destruct (
Val.cmpf_bool c0 (
rs x) (
rs x0))
as [[]|];
inv EVAL';
auto. }
set (
v :=
if normal then Val.cmpf c0 rs#
x rs#
x0 else Val.notbool (
Val.cmpf c0 rs#
x rs#
x0)).
assert (
V:
v =
Val.of_bool (
xorb normal b)).
{
unfold v,
Val.cmpf.
rewrite EVAL''.
destruct normal,
b;
reflexivity. }
econstructor;
econstructor.
split.
constructor.
apply exec_straight_one.
eapply transl_cond_float_correct with (
v :=
v);
eauto.
auto.
split.
rewrite V;
destruct normal,
b;
reflexivity.
intros;
Simpl.
-
destruct (
transl_cond_single c0 X31 x x0)
as [
insn normal]
eqn:
TC;
inv EQ2.
set (
v :=
if normal then Val.cmpfs c0 rs#
x rs#
x0 else Val.notbool (
Val.cmpfs c0 rs#
x rs#
x0)).
assert (
V:
v =
Val.of_bool (
eqb normal b)).
{
unfold v,
Val.cmpfs.
rewrite EVAL'.
destruct normal,
b;
reflexivity. }
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.
-
destruct (
transl_cond_single c0 X31 x x0)
as [
insn normal]
eqn:
TC;
inv EQ2.
assert (
EVAL'':
Val.cmpfs_bool c0 (
rs x) (
rs x0) =
Some (
negb b)).
{
destruct (
Val.cmpfs_bool c0 (
rs x) (
rs x0))
as [[]|];
inv EVAL';
auto. }
set (
v :=
if normal then Val.cmpfs c0 rs#
x rs#
x0 else Val.notbool (
Val.cmpfs c0 rs#
x rs#
x0)).
assert (
V:
v =
Val.of_bool (
xorb normal b)).
{
unfold v,
Val.cmpfs.
rewrite EVAL''.
destruct normal,
b;
reflexivity. }
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.
-
destruct optR as [[]|];
unfold apply_bin_oreg_ireg0,
apply_bin_oreg in *;
unfold zero32,
Op.zero32 in *;
destruct (
rs x)
eqn:
EQRS;
simpl in *;
try congruence;
inv EQ2;
eexists;
eexists;
eauto;
split;
constructor;
auto;
simpl in *.
+
rewrite EQRS;
assert (
HB: (
Int.eq Int.zero i) =
b)
by congruence.
rewrite HB;
destruct b;
simpl;
auto.
+
rewrite EQRS;
assert (
HB: (
Int.eq i Int.zero) =
b)
by congruence.
rewrite <-
HB;
destruct b;
simpl;
auto.
+
rewrite EQRS;
destruct (
rs x0);
try congruence.
assert (
HB: (
Int.eq i i0) =
b)
by congruence.
rewrite <-
HB;
destruct b;
simpl;
auto.
-
destruct optR as [[]|];
unfold apply_bin_oreg_ireg0,
apply_bin_oreg in *;
unfold zero32,
Op.zero32 in *;
destruct (
rs x)
eqn:
EQRS;
simpl in *;
try congruence;
inv EQ2;
eexists;
eexists;
eauto;
split;
constructor;
auto;
simpl in *.
+
rewrite EQRS;
assert (
HB:
negb (
Int.eq Int.zero i) =
b)
by congruence.
rewrite HB;
destruct b;
simpl;
auto.
+
rewrite EQRS;
assert (
HB:
negb (
Int.eq i Int.zero) =
b)
by congruence.
rewrite <-
HB;
destruct b;
simpl;
auto.
+
rewrite EQRS;
destruct (
rs x0);
try congruence.
assert (
HB:
negb (
Int.eq i i0) =
b)
by congruence.
rewrite <-
HB;
destruct b;
simpl;
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 [[]|];
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;
destruct (
rs x)
eqn:
EQRS;
simpl in *;
try congruence;
eexists;
eexists;
eauto;
split;
constructor;
simpl in *;
auto.
+
rewrite EQRS;
assert (
HB: (
Int64.eq Int64.zero i) =
b)
by congruence.
rewrite HB;
destruct b;
simpl;
auto.
+
rewrite EQRS;
assert (
HB: (
Int64.eq i Int64.zero) =
b)
by congruence.
rewrite <-
HB;
destruct b;
simpl;
auto.
+
rewrite EQRS;
destruct (
rs x0);
try congruence.
assert (
HB: (
Int64.eq i i0) =
b)
by congruence.
rewrite <-
HB;
destruct b;
simpl;
auto.
-
destruct optR as [[]|];
unfold apply_bin_oreg_ireg0,
apply_bin_oreg in *;
unfold zero32,
Op.zero32 in *;
inv EQ2;
destruct (
rs x)
eqn:
EQRS;
simpl in *;
try congruence;
eexists;
eexists;
eauto;
split;
constructor;
simpl in *;
auto.
+
rewrite EQRS;
assert (
HB:
negb (
Int64.eq Int64.zero i) =
b)
by congruence.
rewrite HB;
destruct b;
simpl;
auto.
+
rewrite EQRS;
assert (
HB:
negb (
Int64.eq i Int64.zero) =
b)
by congruence.
rewrite <-
HB;
destruct b;
simpl;
auto.
+
rewrite EQRS;
destruct (
rs x0);
try congruence.
assert (
HB:
negb (
Int64.eq i i0) =
b)
by congruence.
rewrite <-
HB;
destruct b;
simpl;
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.
-
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.
Lemma transl_cbranch_correct_true:
forall cond args lbl k c m ms sp rs m',
transl_cbranch cond args lbl k = OK c ->
eval_condition cond (List.map ms args) m = Some true ->
agree ms sp rs ->
Mem.extends m m' ->
exists rs', exists insn,
exec_straight_opt ge fn c rs m' (insn :: k) rs' m'
/\ exec_instr ge fn insn rs' m' = goto_label fn lbl rs' m'
/\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma transl_cbranch_correct_false:
forall cond args lbl k c m ms sp rs m',
transl_cbranch cond args lbl k = OK c ->
eval_condition cond (List.map ms args) m = Some false ->
agree ms sp rs ->
Mem.extends m m' ->
exists rs',
exec_straight ge fn c rs m' k rs' m'
/\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
Proof.
Translation of condition operators
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
/\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
Lemma transl_cond_int32u_correct:
forall cmp rd r1 r2 k rs m,
exists rs',
exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m
/\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs##r1 rs##r2
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
Lemma transl_cond_int64s_correct:
forall cmp rd r1 r2 k rs m,
exists rs',
exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m
/\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
Lemma transl_cond_int64u_correct:
forall cmp rd r1 r2 k rs m,
exists rs',
exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m
/\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs###r1 rs###r2)
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
Lemma transl_condimm_int32s_correct:
forall cmp rd r1 n k rs m,
r1 <> X31 ->
exists rs',
exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m
/\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma transl_condimm_int32u_correct:
forall cmp rd r1 n k rs m,
r1 <> X31 ->
exists rs',
exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m
/\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma transl_condimm_int64s_correct:
forall cmp rd r1 n k rs m,
r1 <> X31 ->
exists rs',
exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m
/\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma transl_condimm_int64u_correct:
forall cmp rd r1 n k rs m,
r1 <> X31 ->
exists rs',
exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m
/\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma transl_cond_op_correct:
forall cond rd args k c rs m,
transl_cond_op cond rd args k = OK c ->
exists rs',
exec_straight ge fn c rs m k rs' m
/\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
Some arithmetic properties.
Remark cast32unsigned_from_cast32signed:
forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)).
Proof.
Ltac SimplEval H :=
match type of H with
| Some _ = None _ => discriminate
| Some _ = Some _ => inv H
| ?a = Some ?b => let A := fresh in assert (A: Val.maketotal a = b) by (rewrite H; reflexivity)
end.
Lemma keep_X1 :
forall rs res (v : val),
rs # (preg_of res) <- v X1 = rs X1.
Proof.
intros.
apply Pregmap.gso.
destruct res;
cbn;
discriminate.
Qed.
Lemma keep_X1' :
forall rs res i (v : val),
preg_of res = i ->
rs # i <- v X1 = rs X1.
Proof.
intros.
rewrite <-
H.
apply keep_X1.
Qed.
Hint Resolve keep_X1 : asmgen.
Lemma ireg_of_not_X1':
forall res x,
ireg_of res = OK x -> IR X1 <> x.
Proof.
cbn; destruct res; cbn in *; congruence.
Qed.
Hint Resolve ireg_of_not_X1' : asmgen.
Ltac TranslOpSimpl :=
econstructor; split;
[ apply exec_straight_one; [simpl; eauto | reflexivity]
| split; [ apply Val.lessdef_same; Simpl; fail | split; [intros; Simpl; fail | Simpl; eapply keep_X1'; eassumption]] ].
Lemma transl_op_correct:
forall op args res k (rs: regset) m v c,
transl_op op args res k = OK c ->
eval_operation ge (rs#SP) op (map rs (map preg_of args)) m = Some v ->
exists rs',
exec_straight ge fn c rs m k rs' m
/\ Val.lessdef v rs'#(preg_of res)
/\ (forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r)
/\ rs' RA = rs RA.
Proof.
Memory accesses
Lemma indexed_memory_access_correct:
forall mk_instr base ofs k rs m,
base <> X31 ->
exists base' ofs' rs',
exec_straight_opt ge fn (indexed_memory_access mk_instr base ofs k) rs m
(mk_instr base' ofs' :: k) rs' m
/\ Val.offset_ptr rs'#base' (eval_offset ge ofs') = Val.offset_ptr rs#base ofs
/\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma indexed_load_access_correct:
forall chunk (mk_instr: ireg -> offset -> instruction) rd m,
(forall base ofs rs,
exec_instr ge fn (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) ->
forall (base: ireg) ofs k (rs: regset) v,
Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
base <> X31 -> rd <> PC ->
exists rs',
exec_straight ge fn (indexed_memory_access mk_instr base ofs k) rs m k rs' m
/\ rs'#rd = v
/\ forall r, r <> PC -> r <> X31 -> r <> rd -> rs'#r = rs#r.
Proof.
Lemma indexed_store_access_correct:
forall chunk (mk_instr: ireg -> offset -> instruction) r1 m,
(forall base ofs rs,
exec_instr ge fn (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) ->
forall (base: ireg) ofs k (rs: regset) m',
Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' ->
base <> X31 -> r1 <> X31 -> r1 <> PC ->
exists rs',
exec_straight ge fn (indexed_memory_access mk_instr base ofs k) rs m k rs' m'
/\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma loadind_correct:
forall (base: ireg) ofs ty dst k c (rs: regset) m v,
loadind base ofs ty dst k = OK c ->
Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v ->
base <> X31 ->
exists rs',
exec_straight ge fn c rs m k rs' m
/\ rs'#(preg_of dst) = v
/\ forall r, r <> PC -> r <> X31 -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
Lemma storeind_correct:
forall (base: ireg) ofs ty src k c (rs: regset) m m',
storeind src base ofs ty k = OK c ->
Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) rs#(preg_of src) = Some m' ->
base <> X31 ->
exists rs',
exec_straight ge fn c rs m k rs' m'
/\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma loadind_ptr_correct:
forall (base: ireg) ofs (dst: ireg) k (rs: regset) m v,
Mem.loadv Mptr m (Val.offset_ptr rs#base ofs) = Some v ->
base <> X31 ->
exists rs',
exec_straight ge fn (loadind_ptr base ofs dst k) rs m k rs' m
/\ rs'#dst = v
/\ forall r, r <> PC -> r <> X31 -> r <> dst -> rs'#r = rs#r.
Proof.
Lemma storeind_ptr_correct:
forall (base: ireg) ofs (src: ireg) k (rs: regset) m m',
Mem.storev Mptr m (Val.offset_ptr rs#base ofs) rs#src = Some m' ->
base <> X31 -> src <> X31 ->
exists rs',
exec_straight ge fn (storeind_ptr src base ofs k) rs m k rs' m'
/\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma transl_memory_access_correct:
forall mk_instr addr args k c (rs: regset) m v,
transl_memory_access mk_instr addr args k = OK c ->
eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
exists base ofs rs',
exec_straight_opt ge fn c rs m (mk_instr base ofs :: k) rs' m
/\ Val.offset_ptr rs'#base (eval_offset ge ofs) = v
/\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma transl_load_access_correct:
forall chunk (mk_instr: ireg -> offset -> instruction) addr args k c rd (rs: regset) m v v',
(forall base ofs rs,
exec_instr ge fn (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) ->
transl_memory_access mk_instr addr args k = OK c ->
eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
Mem.loadv chunk m v = Some v' ->
rd <> PC ->
exists rs',
exec_straight ge fn c rs m k rs' m
/\ rs'#rd = v'
/\ forall r, r <> PC -> r <> X31 -> r <> rd -> rs'#r = rs#r.
Proof.
Lemma transl_store_access_correct:
forall chunk (mk_instr: ireg -> offset -> instruction) addr args k c r1 (rs: regset) m v m',
(forall base ofs rs,
exec_instr ge fn (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) ->
transl_memory_access mk_instr addr args k = OK c ->
eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
Mem.storev chunk m v rs#r1 = Some m' ->
r1 <> PC -> r1 <> X31 ->
exists rs',
exec_straight ge fn c rs m k rs' m'
/\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
Proof.
Lemma transl_load_correct:
forall trap chunk addr args dst k c (rs: regset) m a v,
transl_load trap chunk addr args dst k = OK c ->
eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
Mem.loadv chunk m a = Some v ->
exists rs',
exec_straight ge fn c rs m k rs' m
/\ rs'#(preg_of dst) = v
/\ forall r, r <> PC -> r <> X31 -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
intros until v;
intros TR EV LOAD.
destruct trap;
try (
simpl in *;
discriminate).
assert (
A:
exists mk_instr,
transl_memory_access mk_instr addr args k =
OK c
/\
forall base ofs rs,
exec_instr ge fn (
mk_instr base ofs)
rs m =
exec_load ge chunk rs m (
preg_of dst)
base ofs).
{
unfold transl_load in TR;
destruct chunk;
ArgsInv;
econstructor; (
split; [
eassumption|
auto]). }
destruct A as (
mk_instr &
B &
C).
eapply transl_load_access_correct;
eauto with asmgen.
Qed.
Lemma transl_store_correct:
forall chunk addr args src k c (rs: regset) m a m',
transl_store chunk addr args src k = OK c ->
eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
Mem.storev chunk m a rs#(preg_of src) = Some m' ->
exists rs',
exec_straight ge fn c rs m k rs' m'
/\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
Proof.
Function epilogues
Lemma make_epilogue_correct:
forall ge0 f m stk soff cs m' ms rs k tm,
load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) ->
(if Compopts.optim_leaf tt && is_leaf_function f
then (rs (IR X1)) = parent_ra cs
else load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs)) ->
Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
agree ms (Vptr stk soff) rs ->
Mem.extends m tm ->
match_stack ge0 cs ->
exists rs', exists tm',
exec_straight ge fn (make_epilogue f k) rs tm k rs' tm'
/\ agree ms (parent_sp cs) rs'
/\ Mem.extends m' tm'
/\ rs'#RA = parent_ra cs
/\ rs'#SP = parent_sp cs
/\ (forall r, r <> PC -> r <> RA -> r <> SP -> r <> X31 -> rs'#r = rs#r).
Proof.
End CONSTRUCTORS.