Require Import Coqlib Maps.
Require Import AST Values Events Globalenvs Smallstep.
Require Import RTL Op OptionMonad.
Require Import Errors Linking RTLtoBTL.
Module RTLtoBTL_Translationproof (
B:
RTLtoBTL_TranslationOracle).
Include RTLtoBTL_Translation B.
Normalization of BTL iblock for simulation of RTL
Below normRTL normalizes the representation of BTL blocks,
in order to represent them as sequences of RTL instructions.
This eases the expression of properties in the below proof.
Definition is_RTLatom (
ib:
iblock):
bool :=
match ib with
|
Bseq _ _ |
Bcond _ _ _ _ _ |
Bnop None =>
false
|
_ =>
true
end.
Definition is_RTLbasic (
ib:
iblock):
bool :=
match ib with
|
Bseq _ _ |
Bcond _ _ _ _ _ |
Bnop None |
BF _ _ =>
false
|
_ =>
true
end.
The strict is_normRTL property specifying the ouput of normRTL below
Inductive is_normRTL:
iblock ->
Prop :=
|
norm_Bseq ib1 ib2:
is_RTLbasic ib1 =
true ->
is_normRTL ib2 ->
is_normRTL (
Bseq ib1 ib2)
|
norm_Bcond cond args ib1 ib2 i:
is_normRTL ib1 ->
is_normRTL ib2 ->
is_normRTL (
Bcond cond args ib1 ib2 i)
|
norm_others ib:
is_RTLatom ib =
true ->
is_normRTL ib
.
Local Hint Constructors is_normRTL:
core.
Weaker version allowing for trailing Bnop None.
Inductive is_wnormRTL:
iblock ->
Prop :=
|
wnorm_Bseq ib1 ib2:
is_RTLbasic ib1 =
true ->
(
ib2 <>
Bnop None ->
is_wnormRTL ib2) ->
is_wnormRTL (
Bseq ib1 ib2)
|
wnorm_Bcond cond args ib1 ib2 iinfo:
(
ib1 <>
Bnop None ->
is_wnormRTL ib1) ->
(
ib2 <>
Bnop None ->
is_wnormRTL ib2) ->
is_wnormRTL (
Bcond cond args ib1 ib2 iinfo)
|
wnorm_others ib:
is_RTLatom ib =
true ->
is_wnormRTL ib
.
Local Hint Constructors is_wnormRTL:
core.
Fixpoint normRTLrec (
ib:
iblock) (
k:
iblock):
iblock :=
match ib with
|
Bseq ib1 ib2 =>
normRTLrec ib1 (
normRTLrec ib2 k)
|
Bcond cond args ib1 ib2 iinfo =>
Bcond cond args (
normRTLrec ib1 k) (
normRTLrec ib2 k)
iinfo
|
BF fin iinfo =>
BF fin iinfo
|
Bnop None =>
k
|
ib =>
Bseq ib k
end.
Definition normRTL ib :=
normRTLrec ib (
Bnop None).
Lemma normRTLrec_wcorrect ib:
forall k,
(
k <> (
Bnop None) ->
is_wnormRTL k) ->
(
normRTLrec ib k) <>
Bnop None ->
is_wnormRTL (
normRTLrec ib k).
Proof.
induction ib; simpl; intros; repeat autodestruct; auto.
Qed.
Lemma normRTL_wcorrect ib:
(
normRTL ib) <>
Bnop None ->
is_wnormRTL (
normRTL ib).
Proof.
Lemma is_join_opt_None {
A} (
opc1 opc2:
option A):
is_join_opt opc1 opc2 None ->
opc1 =
None /\
opc2 =
None.
Proof.
intros X. inv X; auto.
Qed.
Lemma match_iblock_None_not_Bnop dupmap cfg cfg'
indirect isfst pc ib:
match_iblock dupmap cfg cfg'
indirect isfst pc ib None ->
ib <>
Bnop None.
Proof.
intros X; inv X; try congruence.
Qed.
Local Hint Resolve match_iblock_None_not_Bnop:
core.
Lemma is_wnormRTL_normRTL dupmap cfg cfg'
indirect ib:
is_wnormRTL ib ->
forall isfst pc
(
MIB:
match_iblock dupmap cfg cfg'
indirect isfst pc ib None),
is_normRTL ib.
Proof.
induction 1;
simpl;
intros;
auto;
try (
inv MIB);
eauto.
destruct (
is_join_opt_None opc1 opc2);
subst;
eauto.
econstructor;
eauto.
Qed.
Local Hint Constructors iblock_istep:
core.
Lemma normRTLrec_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin1:
forall (
ISTEP:
iblock_istep tge sp None rs0 m0 ib rs1 m1 ofin1)
k ofin2 rs2 m2
(
CONT:
match ofin1 with
|
None =>
iblock_istep tge sp None rs1 m1 k rs2 m2 ofin2
|
Some fin1 =>
rs2=
rs1 /\
m2=
m1 /\
ofin2=
Some fin1
end),
iblock_istep tge sp None rs0 m0 (
normRTLrec ib k)
rs2 m2 ofin2.
Proof.
induction 1;
simpl;
intuition subst;
eauto.
-
autodestruct;
eauto.
-
repeat econstructor;
eauto.
-
inv LOAD.
+
repeat econstructor;
eauto.
+
do 2 (
econstructor;
eauto).
eapply has_loaded_default;
eauto.
-
repeat econstructor;
eauto.
destruct ofin;
intuition subst;
destruct b;
eapply IHISTEP;
eauto.
Qed.
Lemma normRTL_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin:
iblock_istep tge sp None rs0 m0 ib rs1 m1 ofin ->
iblock_istep tge sp None rs0 m0 (
normRTL ib)
rs1 m1 ofin.
Proof.
Lemma normRTLrec_iblock_istep_run_None tge sp ib:
forall rs0 m0 k
(
CONT:
match iblock_istep_run tge sp None ib rs0 m0 with
|
Some (
out rs1 m1 ofin) =>
ofin =
None /\
iblock_istep_run tge sp None k rs1 m1 =
None
|
_ =>
True
end),
iblock_istep_run tge sp None (
normRTLrec ib k)
rs0 m0 =
None.
Proof.
induction ib; simpl; intros; subst; intuition (try discriminate).
-
intros. autodestruct; auto.
-
intros; repeat autodestruct; simpl; intuition congruence.
-
intros; repeat autodestruct; simpl; intuition congruence.
-
intros; repeat autodestruct; simpl; intuition congruence.
-
intros.
eapply IHib1; eauto.
autodestruct; simpl in *; destruct o; simpl in *; intuition eauto.
+ destruct _fin; intuition eauto.
+ destruct _fin; intuition congruence || eauto.
-
intros; repeat autodestruct; simpl; intuition congruence || eauto.
Qed.
Lemma normRTL_preserves_iblock_istep_run_None tge sp ib:
forall rs m,
iblock_istep_run tge sp None ib rs m =
None
->
iblock_istep_run tge sp None (
normRTL ib)
rs m =
None.
Proof.
Lemma normRTL_preserves_iblock_istep_run tge sp ib:
forall rs m,
iblock_istep_run tge sp None ib rs m =
iblock_istep_run tge sp None (
normRTL ib)
rs m.
Proof.
Local Hint Constructors match_iblock:
core.
Lemma normRTLrec_matchiblock_correct dupmap cfg cfg'
indirect ib pc isfst:
forall opc1
(
MIB:
match_iblock dupmap cfg cfg'
indirect isfst pc ib opc1)
k opc2
(
CONT:
match opc1 with
|
Some pc' =>
match_iblock dupmap cfg cfg'
indirect false pc'
k opc2
|
None =>
opc2=
opc1
end),
match_iblock dupmap cfg cfg'
indirect isfst pc (
normRTLrec ib k)
opc2.
Proof.
induction 1; simpl; intros; subst; eauto.
intros. inv H0;
econstructor; eauto; try econstructor.
destruct opc0; econstructor.
Qed.
Lemma normRTL_matchiblock_correct dupmap cfg cfg'
indirect ib pc isfst opc:
match_iblock dupmap cfg cfg'
indirect isfst pc ib opc ->
match_iblock dupmap cfg cfg'
indirect isfst pc (
normRTL ib)
opc.
Proof.
Lemma is_normRTL_correct dupmap cfg cfg'
indirect ib pc
(
MI :
match_iblock dupmap cfg cfg'
indirect true pc ib None):
is_normRTL (
normRTL ib).
Proof.
Local Hint Resolve normRTL_matchiblock_correct is_normRTL_correct:
core.
Matching relation on functions
Definition match_function dupmap (
f:
RTL.function) (
tf:
BTL.function):
Prop :=
BTLmatchRTL.match_function dupmap tf f true.
Inductive match_fundef:
RTL.fundef ->
BTL.fundef ->
Prop :=
|
match_Internal dupmap f f':
match_function dupmap f f' ->
match_fundef (
Internal f) (
Internal f')
|
match_External ef:
match_fundef (
External ef) (
External ef).
Inductive match_stackframes:
RTL.stackframe ->
BTL.stackframe ->
Prop :=
|
match_stackframe_intro
dupmap indirect res f sp pc rs f'
pc'
(
TRANSF:
match_function dupmap f f')
(
MN:
match_nodes dupmap (
fn_code f')
indirect pc'
pc)
:
match_stackframes (
RTL.Stackframe res f sp pc rs) (
BTL.Stackframe res f'
sp pc'
rs).
Lemma transf_function_correct f f':
transf_function f =
OK f' ->
exists dupmap,
match_function dupmap f f'.
Proof.
Lemma transf_fundef_correct f f':
transf_fundef f =
OK f' ->
match_fundef f f'.
Proof.
Definition match_prog (
p:
RTL.program) (
tp:
program) :=
match_program (
fun _ f tf =>
transf_fundef f =
OK tf)
eq p tp.
Lemma transf_program_match:
forall prog tprog,
transf_program prog =
OK tprog ->
match_prog prog tprog.
Proof.
Section BTL_SIMULATES_RTL.
Variable prog:
RTL.program.
Variable tprog:
program.
Hypothesis TRANSL:
match_prog prog tprog.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Local Open Scope nat_scope.
Match relation from a RTL state to a BTL state
The "option iblock" parameter represents the current BTL execution state.
Thus, each RTL single step is symbolized by a new BTL "option iblock"
starting at the equivalent PC, which is always pcB below.
The entry of this block is obtained by the ATpcB hypothesis.
The simulation diagram for match_states_intro is as follows:
If there is no synthetic node, then pcX = pcB
else, pcX is pointing to the synthetic node and pcB to the original one.
RTL state match_states_intro BTL state
[pcR0,rs0,m0] --------------------------- [pcX,rs0,m0]
| |
| | BTL_RUN of the synth node
| | if it exists
| |
| [pcB,rs0,m0]
| |
RTL_RUN | *E0 | BTL_RUN of the orig node
| |
| MIB |
[pcR1,rs1,m1] ------------------------------- [ib]
Inductive match_strong_state dupmap st st'
f f'
sp rs1 m1 rs0 m0 pcX pcB pcR0 pcR1 ib ib0 isfst:
Prop :=
|
match_strong_state_intro indirect
(
STACKS:
list_forall2 match_stackframes st st')
(
TRANSF:
match_function dupmap f f')
(
MSN:
match_synthetic_node dupmap (
fn_code f')
indirect pcX pcB pcR0)
(
ATpcB: (
fn_code f')!
pcB =
Some ib0)
(
MIB:
match_iblock dupmap (
fn_code f') (
RTL.fn_code f)
indirect isfst pcR1 ib None)
(
IS_EXPD:
is_normRTL ib)
(
RTL_RUN:
star RTL.step ge (
RTL.State st f sp pcR0 rs0 m0)
E0 (
RTL.State st f sp pcR1 rs1 m1))
(
BTL_RUN:
iblock_istep_run tge sp None ib0.(
entry)
rs0 m0 =
iblock_istep_run tge sp None ib rs1 m1)
:
match_strong_state dupmap st st'
f f'
sp rs1 m1 rs0 m0 pcX pcB pcR0 pcR1 ib ib0 isfst
.
Inductive match_states: (
option iblock) ->
RTL.state ->
state ->
Prop :=
|
match_states_intro
dupmap st st'
f f'
sp rs1 m1 rs0 m0 bc pcX pcB pcR0 pcR1 ib ib0 isfst
(
MSTRONG:
match_strong_state dupmap st st'
f f'
sp rs1 m1 rs0 m0 pcX pcB pcR0 pcR1 ib ib0 isfst)
(
NGOTO:
is_goto ib =
false)
:
match_states (
Some ib) (
RTL.State st f sp pcR1 rs1 m1) (
State st'
f'
sp pcX rs0 m0 bc)
|
match_states_call
st st'
f f'
args m bc
(
STACKS:
list_forall2 match_stackframes st st')
(
TRANSF:
match_fundef f f')
:
match_states None (
RTL.Callstate st f args m) (
Callstate st'
f'
args m bc)
|
match_states_return
st st'
v m bc
(
STACKS:
list_forall2 match_stackframes st st')
:
match_states None (
RTL.Returnstate st v m) (
Returnstate st'
v m bc)
.
Lemma symbols_preserved s:
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof.
Lemma senv_preserved:
Senv.equiv ge tge.
Proof.
Lemma functions_translated (
v:
val) (
f:
RTL.fundef):
Genv.find_funct ge v =
Some f ->
exists tf cunit,
transf_fundef f =
OK tf /\
Genv.find_funct tge v =
Some tf /\
linkorder cunit prog.
Proof.
Lemma function_ptr_translated v f:
Genv.find_funct_ptr ge v =
Some f ->
exists tf,
Genv.find_funct_ptr tge v =
Some tf /\
transf_fundef f =
OK tf.
Proof.
Lemma function_sig_translated f tf:
transf_fundef f =
OK tf ->
funsig tf =
RTL.funsig f.
Proof.
Lemma transf_initial_states s1:
RTL.initial_state prog s1 ->
exists ib s2,
initial_state tprog s2 /\
match_states ib s1 s2.
Proof.
Lemma transf_final_states ib s1 s2 r:
match_states ib s1 s2 ->
RTL.final_state s1 r ->
final_state s2 r.
Proof.
intros. inv H0. inv H. inv STACKS. constructor.
Qed.
Lemma find_function_preserved ri rs0 fd
(
FIND :
RTL.find_function ge ri rs0 =
Some fd)
:
exists fd',
find_function tge ri rs0 =
Some fd'
/\
transf_fundef fd =
OK fd'.
Proof.
Representing an intermediate BTL state
We keep a measure of code that remains to be executed with the omeasure
type defined below. Intuitively, each RTL step corresponds to either
- a single BTL step if we are on the last instruction of the block
- no BTL step (as we use a "big step" semantics) but a change in
the measure which represents the new intermediate state of the BTL code
Fixpoint measure ib:
nat :=
match ib with
|
Bseq ib1 ib2
|
Bcond _ _ ib1 ib2 _ =>
measure ib1 +
measure ib2
|
ib => 1
end.
Definition omeasure (
oib:
option iblock):
nat :=
match oib with
|
None => 0
|
Some ib =>
measure ib
end.
Remark measure_pos:
forall ib,
measure ib > 0.
Proof.
induction ib; simpl; auto; lia.
Qed.
Lemma match_iblock_true_isnt_goto dupmap cfg cfg'
indirect pc ib opc:
match_iblock dupmap cfg cfg'
indirect true pc ib opc ->
is_goto ib =
false.
Proof.
intros MIB; inversion MIB as [d1 d2 d3 d4 d5 H H0| | | | | | |Â |]; subst; simpl; try congruence.
inv H0; congruence.
Qed.
Local Hint Resolve match_iblock_true_isnt_goto normRTL_preserves_iblock_istep_run star_refl star_right:
core.
Local Hint Constructors match_strong_state RTL.step:
core.
At entry in a block: we init match_states on normRTL to normalize the block.
The "direct" lemma match the RTL state on pcR to ib, the corresponding
iblock starting at pcB, and the "indirect" one match pcR to the
synthetic node at pcX whose successor is ib at pcB.
Lemma match_states_entry_direct dupmap st f sp pcR ib rs m bc st'
f'
pcB indirect
(
STACKS :
list_forall2 match_stackframes st st')
(
TRANSF :
match_function dupmap f f')
(
FN : (
fn_code f') !
pcB =
Some ib)
(
MI :
match_iblock dupmap (
fn_code f') (
RTL.fn_code f)
indirect true pcR (
entry ib)
None)
(
DUP:
dupmap !
pcB =
Some pcR)
:
match_states (
Some (
normRTL (
entry ib))) (
RTL.State st f sp pcR rs m) (
State st'
f'
sp pcB rs m bc).
Proof.
Lemma match_states_entry_indirect dupmap st f sp pcX pcB pcR ib rs m bc st'
f'
indirect
(
STACKS :
list_forall2 match_stackframes st st')
(
TRANSF :
match_function dupmap f f')
(
FN : (
fn_code f') !
pcB =
Some ib)
(
MI :
match_iblock dupmap (
fn_code f') (
RTL.fn_code f)
indirect true pcR (
entry ib)
None)
(
MSN:
match_synthetic_node dupmap (
fn_code f')
indirect pcX pcB pcR)
:
match_states (
Some (
normRTL (
entry ib))) (
RTL.State st f sp pcR rs m) (
State st'
f'
sp pcX rs m bc).
Proof.
Lemma list_nth_z_rev_dupmap:
forall dupmap code indirect ln ln' (
pc pc':
node)
val,
list_nth_z ln val =
Some pc ->
list_forall2 (
fun n'
n =>
match_nodes dupmap code indirect n'
n)
ln'
ln ->
exists (
pc':
node),
list_nth_z ln'
val =
Some pc'
/\
match_nodes dupmap code indirect pc'
pc.
Proof.
induction ln;
intros until val;
intros LNZ LFA.
-
inv LNZ.
-
inv LNZ.
destruct (
zeq val 0)
eqn:
ZEQ.
+
inv H0.
destruct ln';
inv LFA.
simpl.
exists n.
split;
auto.
+
inv LFA.
simpl.
rewrite ZEQ.
exploit IHln. 2:
eapply H0.
all:
eauto.
Qed.
Match strong state property
Used when executing non-atomic instructions such as Bseq/Bcond(ib1,ib2).
Two possible executions:
**ib2 is a Bgoto (left side):**
RTL state MSS1 BTL state
[pcR1,rs1,m1] -------------------------- [ib1,pcX,rs0,m0]
| |
| | Either one or two
| | BTL_STEP for direct and
| | indirect cases, resp.
| |
RTL_STEP | *E0 [ib2,pc=(Bgoto succ),rs2,m2]
| / |
| MSS2 / |
| _________________/ | BTL_GOTO
| / |
| / GOAL: match_states |
[pcR2,rs2,m2] ------------------------ [ib?,pc=succ,rs2,m2]
**ib2 is any other instruction (right side):**
See explanations of opt_simu below.
pcB is always defined in the reverse mapping.
Remark match_synthetic_node_dupmap dupmap f'
indirect pcX pcB pcR0
(
MSN:
match_synthetic_node dupmap (
fn_code f')
indirect pcX pcB pcR0)
:
dupmap !
pcB =
Some pcR0.
Proof.
inv MSN; auto.
Qed.
Hint Resolve match_synthetic_node_dupmap:
core.
It always exists an iblock at pcX (which is either the real or the
synthetic node).
Remark match_synthetic_node_code dupmap f f'
indirect pcX pcB pcR0
(
TRANSF:
match_function dupmap f f')
(
MSN:
match_synthetic_node dupmap (
fn_code f')
indirect pcX pcB pcR0)
:
exists ib, (
fn_code f') !
pcX =
Some ib.
Proof.
inv MSN;
eauto.
exploit dupmap_correct;
eauto.
intros (
ib &
FNC &
MI);
eauto.
Qed.
Hint Resolve match_synthetic_node_dupmap:
core.
Main lemma for match_strong_state with both execution cases represented:
- left (last instruction): one or two BTL (big-)step(s) to execute the BTL
code that may start with a synthetic node;
- right (internal instruction): no step but a decrease in the measure.
Lemma match_strong_state_simu
dupmap st st'
f f'
sp rs2 m2 rs1 m1 rs0 m0 bc0 pcX pcB pcR0 pcR1 pcR2 isfst ib1 ib2 ib0 n t s1'
(
EQt:
t=
E0)
(
EQs1':
s1'=(
RTL.State st f sp pcR2 rs2 m2))
(
STEP :
RTL.step ge (
RTL.State st f sp pcR1 rs1 m1)
t s1')
(
MSS1 :
match_strong_state dupmap st st'
f f'
sp rs1 m1 rs0 m0 pcX pcB pcR0 pcR1 ib1 ib0 isfst)
(
MSS2 :
match_strong_state dupmap st st'
f f'
sp rs2 m2 rs0 m0 pcX pcB pcR0 pcR2 ib2 ib0 false)
(
MES :
measure ib2 <
n)
:
exists (
oib' :
option iblock),
(
exists s2',
plus (
step false)
tge (
State st'
f'
sp pcX rs0 m0 bc0)
E0 s2'
/\
match_states oib'
s1'
s2')
\/ (
omeasure oib' <
n /\
t=
E0
/\
match_states oib'
s1' (
State st'
f'
sp pcX rs0 m0 bc0)).
Proof.
Executing the BTL step corresponding to a synthetic node.
Lemma opt_simu_indirect
dupmap indirect st'
f'
sp rs0 m0 bc0 pcX pcB ibf (
fin:
final)
inst iinfo0
(
PC: (
fn_code f') !
pcX =
Some ibf)
(
BLK:
entry ibf =
Bgoto pcB iinfo0)
(
MFI:
match_final_inst dupmap (
fn_code f')
indirect fin inst)
:
step false tge (
State st'
f'
sp pcX rs0 m0 bc0)
E0 (
State st'
f'
sp pcB rs0 m0 bc0).
Proof.
inv MFI; econstructor; eauto.
all: rewrite BLK; repeat econstructor; eauto.
Qed.
Hint Resolve opt_simu_indirect:
core.
Lemma opt_simu_direct
dupmap indirect st st'
f f'
sp rs m rs0 m0 bc0 pcB pcR0 pcR1 ib0 s1'
t (
fin:
final)
inst iinfo
(
TRANSF:
match_function dupmap f f')
(
STACKS:
list_forall2 match_stackframes st st')
(
STEP:
RTL.step ge (
RTL.State st f sp pcR1 rs m)
t s1')
(
NGOTO:
is_goto (
fin iinfo) =
false)
(
DUP:
dupmap !
pcB =
Some pcR0)
(
MFI:
match_final_inst dupmap (
fn_code f')
indirect fin inst)
(
ATpcB : (
fn_code f') !
pcB =
Some ib0)
(
RTL_RUN :
star RTL.step ge (
RTL.State st f sp pcR0 rs0 m0)
E0
(
RTL.State st f sp pcR1 rs m))
(
BTL_RUN :
iblock_istep_run tge sp None (
entry ib0)
rs0 m0 =
iblock_istep_run tge sp None (
fin iinfo)
rs m)
(
PC: (
RTL.fn_code f) !
pcR1 =
Some inst)
:
exists oib'
s2',
step false tge (
State st'
f'
sp pcB rs0 m0 bc0)
t s2' /\
match_states oib'
s1'
s2'.
Proof.
opt_simu_intro combines the two lemmas above.
Lemma opt_simu_intro
dupmap st st'
f f'
sp rs m rs0 m0 bc0 pcX pcB pcR0 pcR1 ib ib0 isfst s1'
t
(
STEP:
RTL.step ge (
RTL.State st f sp pcR1 rs m)
t s1')
(
MSTRONG:
match_strong_state dupmap st st'
f f'
sp rs m rs0 m0 pcX pcB pcR0 pcR1 ib ib0 isfst)
(
NGOTO:
is_goto ib =
false)
:
exists (
oib' :
option iblock),
(
exists s2',
plus (
step false)
tge (
State st'
f'
sp pcX rs0 m0 bc0)
t s2' /\
match_states oib'
s1'
s2')
\/ (
omeasure oib' <
omeasure (
Some ib) /\
t=
E0 /\
match_states oib'
s1' (
State st'
f'
sp pcX rs0 m0 bc0)).
Proof.
inv MSTRONG;
subst.
inv MIB.
-
exploit opt_simu_direct;
eauto;
intros (
oib' &
s2' &
BSTEP &
MS).
inversion H0;
inversion STEP;
subst;
try_simplify_someHyps;
intros.
all:
inv MSN;
eexists;
left;
exists s2';
split;
[
apply plus_one |
idtac |
eapply plus_two |
idtac ];
eauto.
-
discriminate.
-
inv IS_EXPD;
try discriminate.
inv H;
simpl in *;
try congruence;
inv STEP;
try_simplify_someHyps;
intros;
eapply match_strong_state_simu;
eauto;
econstructor;
eauto.
{
erewrite eval_operation_preserved in H12.
erewrite H12 in BTL_RUN;
simpl in BTL_RUN;
auto.
intros;
rewrite <-
symbols_preserved;
trivial. }
inv H12; [
idtac |
destruct (
eval_addressing)
eqn:
EVAL in LOAD;[
specialize (
LOAD v) |] ];
rename LOAD into MEMT.
4:
rename H12 into EVAL;
rename H13 into MEMT.
all:
erewrite eval_addressing_preserved in EVAL;
try erewrite EVAL in BTL_RUN;
try erewrite MEMT in BTL_RUN;
simpl in BTL_RUN;
try destruct trap;
auto;
intros;
rewrite <-
symbols_preserved;
trivial.
-
inv IS_EXPD;
try discriminate.
inversion STEP;
subst;
try_simplify_someHyps;
intros.
destruct (
is_join_opt_None opc1 opc2);
eauto.
subst.
eapply match_strong_state_simu with (
ib1:=
Bcond c lr bso bnot iinfo) (
ib2:=(
if b then bso else bnot));
eauto.
+
intros;
rewrite H14 in BTL_RUN;
destruct b;
econstructor;
eauto.
+
assert (
measure (
if b then bnot else bso) > 0)
by apply measure_pos;
destruct b;
simpl;
lia.
Unshelve.
all:
eauto.
Qed.
Main RTL to BTL simulation theorem
Two possible executions:
**Last instruction (left side):**
RTL state match_states BTL state
s1 ------------------------------------ s2
| |
STEP | Classical (right) plus simu | +
| |
s1' ----------------------------------- s2'
**Middle instruction (right side):**
RTL state match_states [oib] BTL state
s1 ------------------------------------ s2
| _______/
STEP | *E0 ___________________/
| / match_states [oib']
s1' ______/
Where omeasure oib' < omeasure oib
Theorem opt_simu s1 t s1'
oib s2:
RTL.step ge s1 t s1' ->
match_states oib s1 s2 ->
exists (
oib' :
option iblock),
(
exists s2',
plus (
step false)
tge s2 t s2' /\
match_states oib'
s1'
s2')
\/ (
omeasure oib' <
omeasure oib /\
t=
E0 /\
match_states oib'
s1'
s2)
.
Proof.
Local Hint Resolve plus_one star_refl:
core.
Theorem transf_program_correct:
forward_simulation (
RTL.semantics prog) (
BTL.sem false tprog).
Proof.
End BTL_SIMULATES_RTL.
End RTLtoBTL_Translationproof.