Common definition and proofs on Asmblock required by various modules
Require Import Coqlib.
Require Import Integers Memory Globalenvs.
Require Import Values.
Require Import Asmblock.
Require Import Axioms.
Definition bblock_simu (
ge:
Genv.t fundef unit) (
f:
function) (
bb bb':
bblock) :=
forall rs m rs' m' t,
exec_bblock ge f bb rs m t rs' m' ->
exec_bblock ge f bb' rs m t rs' m'.
Definition bblock_simu_aux (
ge:
Genv.t fundef unit) (
f:
function) (
bb bb':
bblock) :=
forall rs m,
bbstep ge f bb rs m <>
Stuck ->
bbstep ge f bb rs m =
bbstep ge f bb' rs m.
#[
global]
Hint Extern 2 (_ <> _) =>
congruence:
asmgen.
Lemma preg_of_data:
forall r,
data_preg (
preg_of r) =
true.
Proof.
intros. destruct r; reflexivity.
Qed.
Lemma dreg_of_data:
forall r,
data_preg (
dreg_of r) =
true.
Proof.
intros. destruct r; reflexivity.
Qed.
#[
global]
Hint Resolve preg_of_data dreg_of_data:
asmgen.
Lemma data_diff:
forall r r',
data_preg r =
true ->
data_preg r' =
false ->
r <>
r'.
Proof.
congruence.
Qed.
#[
global]
Hint Resolve data_diff:
asmgen.
Lemma preg_of_not_PC:
forall r,
preg_of r <>
PC.
Proof.
intros.
apply data_diff;
auto with asmgen.
Qed.
Lemma preg_of_not_SP:
forall r,
preg_of r <>
SP.
Proof.
intros.
unfold preg_of;
destruct r;
simpl;
try discriminate.
Qed.
#[
global]
Hint Resolve preg_of_not_SP preg_of_not_PC:
asmgen.
Ltac desif :=
repeat match goal with
| [ |-
context[
if ?
f then _
else _ ] ] =>
destruct f
end.
Ltac decomp :=
repeat match goal with
| [ |-
context[
match (?
rs ?
r)
with | _ => _
end ] ] =>
destruct (
rs r)
end.
Ltac Simplif :=
((
desif)
|| (
unfold compare_int)
|| (
unfold compare_float)
|| (
unfold compare_float32)
||
decomp
|| (
rewrite Pregmap.gss)
|| (
rewrite Pregmap.gso by eauto with asmgen)
);
auto with asmgen.
Ltac Simpl :=
repeat Simplif.
Multi-register load/store helpers: PC is preserved.
Lemma exec_load_multi_i_pc:
forall l base ofs rs rs' m,
exec_load_multi_i base ofs l rs m =
Some rs' ->
rs' PC =
rs PC.
Proof.
induction l as [| [
r chk]
tl IH];
intros base ofs rs rs' m H;
simpl in H.
-
inv H;
reflexivity.
-
destruct (
Mem.loadv chk m (
Val.add base (
Vint (
Int.repr ofs))))
eqn:
LD;
try discriminate.
apply IH in H.
rewrite H.
apply Pregmap.gso.
discriminate.
Qed.
Lemma exec_load_multi_f_pc:
forall l base ofs rs rs' m,
exec_load_multi_f base ofs l rs m =
Some rs' ->
rs' PC =
rs PC.
Proof.
induction l as [| [
r chk]
tl IH];
intros base ofs rs rs' m H;
simpl in H.
-
inv H;
reflexivity.
-
destruct (
Mem.loadv chk m (
Val.add base (
Vint (
Int.repr ofs))))
eqn:
LD;
try discriminate.
apply IH in H.
rewrite H.
apply Pregmap.gso.
discriminate.
Qed.
Theorem exec_basic_instr_pc:
forall ge b rs1 m1 rs2 m2,
exec_basic ge b rs1 m1 =
Next rs2 m2 ->
rs2 PC =
rs1 PC.
Proof.
intros.
destruct b;
repeat destruct i;
repeat destruct ld;
repeat destruct st;
try destruct cp,
mas,
mad;
first [
(
simpl in H;
match type of H with
| (
if ldm_iregs_wf ?
ra ?
l then _
else Stuck) =
Next _ _ =>
destruct (
ldm_iregs_wf ra l)
eqn:
WF;
try discriminate;
destruct (
exec_load_multi_i (
rs1 ra) 0
l rs1 m1)
eqn:
E;
try discriminate;
inv H;
eapply exec_load_multi_i_pc;
eauto
| (
if vldm_fregs_wf ?
l then _
else Stuck) =
Next _ _ =>
destruct (
vldm_fregs_wf l)
eqn:
WF;
try discriminate;
destruct (
exec_load_multi_f (
rs1 _) 0
l rs1 m1)
eqn:
E;
try discriminate;
inv H;
eapply exec_load_multi_f_pc;
eauto
| (
if stm_iregs_wf ?
ra ?
l then _
else Stuck) =
Next _ _ =>
destruct (
stm_iregs_wf ra l)
eqn:
WF;
try discriminate;
destruct (
exec_store_multi_i (
rs1 ra) 0
l rs1 m1)
eqn:
E;
try discriminate;
inv H;
reflexivity
| (
if vstm_fregs_wf ?
l then _
else Stuck) =
Next _ _ =>
destruct (
vstm_fregs_wf l)
eqn:
WF;
try discriminate;
destruct (
exec_store_multi_f (
rs1 _) 0
l rs1 m1)
eqn:
E;
try discriminate;
inv H;
reflexivity
end)
| (
generalize H;
simpl;
unfold exec_load_aux,
exec_load_pi_aux,
exec_load_pd_aux,
exec_load_double_aux,
exec_load_pi_double_aux;
unfold exec_store_aux,
exec_store_pi_aux,
exec_store_pd_aux,
exec_store_double_aux,
exec_store_pi_double_aux;
unfold exec_memcpy_aux;
Simpl;
intros H';
inv H';
Simpl;
reflexivity)
].
Qed.