General notions about the bisimulation BTL <-> RTL.
Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Duplicate RTL Op OptionMonad.
Require Export BTL.
Matching BTL and RTL code
We define a single verifier able to prove a bisimulation between BTL and RTL code.
Hence, in a sense, our verifier imitates the approach of Duplicate, where dupmap maps the BTL nodes to the RTL nodes.
The match_function definition gives a "relational" specification of the verifier...
Require Import Errors.
Inductive match_synthetic_node (
dupmap:
PTree.t node) (
cfg:
BTL.code):
bool ->
node ->
node ->
node ->
Prop :=
|
mn_direct pcB pcR indirect:
dupmap !
pcB =
Some pcR ->
match_synthetic_node dupmap cfg indirect pcB pcB pcR
|
mn_indirect pcX pcB pcR ibf iinfo:
dupmap !
pcX =
None ->
cfg !
pcX =
Some ibf ->
ibf.(
entry) =
BF (
Bgoto pcB)
iinfo ->
dupmap !
pcB =
Some pcR ->
match_synthetic_node dupmap cfg true pcX pcB pcR
.
Global Hint Constructors match_synthetic_node:
core.
Definition match_nodes dupmap cfg indirect pcX pcR :=
exists pcB,
match_synthetic_node dupmap cfg indirect pcX pcB pcR.
Inductive match_final_inst (
dupmap:
PTree.t node) (
cfg:
BTL.code) (
indirect:
bool):
final ->
instruction ->
Prop :=
|
mfi_return or:
match_final_inst dupmap cfg indirect (
Breturn or) (
Ireturn or)
|
mfi_call pcX pcR s ri lr r:
match_nodes dupmap cfg indirect pcX pcR ->
match_final_inst dupmap cfg indirect (
Bcall s ri lr r pcX) (
Icall s ri lr r pcR)
|
mfi_tailcall s ri lr:
match_final_inst dupmap cfg indirect (
Btailcall s ri lr) (
Itailcall s ri lr)
|
mfi_builtin pcX pcR ef la br:
match_nodes dupmap cfg indirect pcX pcR ->
match_final_inst dupmap cfg indirect (
Bbuiltin ef la br pcX) (
Ibuiltin ef la br pcR)
|
mfi_jumptable ln ln' r:
list_forall2 (
fun pcX pcR =>
match_nodes dupmap cfg indirect pcX pcR)
ln ln' ->
match_final_inst dupmap cfg indirect (
Bjumptable r ln) (
Ijumptable r ln')
.
Inductive is_join_opt {
A}: (
option A) -> (
option A) -> (
option A) ->
Prop :=
|
ijo_None_left o:
is_join_opt None o o
|
ijo_None_right o:
is_join_opt o None o
|
ijo_Some x:
is_join_opt (
Some x) (
Some x) (
Some x)
.
Inductive match_iblock (
dupmap:
PTree.t node) (
cfg:
BTL.code) (
cfg':
RTL.code) (
indirect:
bool):
bool ->
node ->
iblock -> (
option node) ->
Prop :=
|
mib_BF isfst fi pc i iinfo:
cfg'!
pc =
Some i ->
match_final_inst dupmap cfg indirect fi i ->
match_iblock dupmap cfg cfg' indirect isfst pc (
BF fi iinfo)
None
|
mib_nop_on_rtl isfst pc pc' iinfo:
cfg'!
pc =
Some (
Inop pc') ->
match_iblock dupmap cfg cfg' indirect isfst pc (
Bnop (
Some iinfo)) (
Some pc')
|
mib_nop_skip pc:
match_iblock dupmap cfg cfg' indirect false pc (
Bnop None) (
Some pc)
|
mib_op isfst pc pc' op lr r iinfo:
cfg'!
pc =
Some (
Iop op lr r pc') ->
match_iblock dupmap cfg cfg' indirect isfst pc (
Bop op lr r iinfo) (
Some pc')
|
mib_load isfst pc pc' trap m a lr r iinfo:
cfg'!
pc =
Some (
Iload trap m a lr r pc') ->
match_iblock dupmap cfg cfg' indirect isfst pc (
Bload trap m a lr r iinfo) (
Some pc')
|
mib_store isfst pc pc' m a lr r iinfo:
cfg'!
pc =
Some (
Istore m a lr r pc') ->
match_iblock dupmap cfg cfg' indirect isfst pc (
Bstore m a lr r iinfo) (
Some pc')
|
mib_exit pc pc' iinfo:
match_nodes dupmap cfg indirect pc pc' ->
match_iblock dupmap cfg cfg' indirect false pc' (
BF (
Bgoto pc)
iinfo)
None
|
mib_seq_Some isfst b1 b2 pc1 pc2 opc:
match_iblock dupmap cfg cfg' indirect isfst pc1 b1 (
Some pc2) ->
match_iblock dupmap cfg cfg' indirect false pc2 b2 opc ->
match_iblock dupmap cfg cfg' indirect isfst pc1 (
Bseq b1 b2)
opc
|
mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i iinfo:
cfg'!
pc =
Some (
Icond c lr pcso pcnot i) ->
match_iblock dupmap cfg cfg' indirect false pcso bso opc1 ->
match_iblock dupmap cfg cfg' indirect false pcnot bnot opc2 ->
is_join_opt opc1 opc2 opc ->
match_iblock dupmap cfg cfg' indirect isfst pc (
Bcond c lr bso bnot iinfo)
opc
.
Definition match_cfg dupmap (
cfg:
BTL.code) (
cfg':
RTL.code) (
indirect:
bool):
Prop :=
forall pc pc',
dupmap!
pc =
Some pc' ->
exists ib,
cfg!
pc =
Some ib /\
match_iblock dupmap cfg cfg' indirect true pc' ib.(
entry)
None.
Record match_function dupmap f f' indirect:
Prop := {
dupmap_correct:
match_cfg dupmap (
BTL.fn_code f) (
RTL.fn_code f')
indirect;
dupmap_entrypoint:
match_nodes dupmap (
BTL.fn_code f)
indirect (
fn_entrypoint f) (
RTL.fn_entrypoint f');
preserv_fnsig:
fn_sig f =
RTL.fn_sig f';
preserv_fnparams:
fn_params f =
RTL.fn_params f';
preserv_fnstacksize:
fn_stacksize f =
RTL.fn_stacksize f'
}.
Shared verifier between RTL -> BTL and BTL -> RTL
Local Open Scope error_monad_scope.
Definition verify_node_eq n n' :=
match (
Pos.compare n n')
with Eq =>
OK tt | _ =>
Error(
msg "BTL.verify_node_eq: comparison failed")
end.
Definition verify_indirection dupmap cfg n n' :=
match cfg!
n with
|
None =>
Error(
msg "BTL.verify_indirection: missing synthetic node")
|
Some ibf =>
match ibf.(
entry)
with
|
BF (
Bgoto pc1) _ =>
match dupmap!
pc1 with
|
None =>
Error(
msg "BTL.verify_indirection: invalid map")
|
Some revn =>
verify_node_eq n' revn
end
| _ =>
Error(
msg "BTL.verify_indirection: invalid synthetic node")
end
end.
Definition verify_is_copy dupmap cfg (
indirect:
bool)
n n' :=
match dupmap!
n with
|
None =>
if indirect then verify_indirection dupmap cfg n n'
else Error(
msg "BTL.verify_is_copy: invalid map")
|
Some revn =>
verify_node_eq n' revn
end.
Fixpoint verify_is_copy_list dupmap cfg indirect ln ln' :=
match ln with
|
n::
ln =>
match ln' with
|
n'::
ln' =>
do dummy <-
verify_is_copy dupmap cfg indirect n n';
verify_is_copy_list dupmap cfg indirect ln ln'
|
nil =>
Error (
msg "BTL.verify_is_copy_list: ln' bigger than ln")
end
|
nil =>
match ln' with
|
n ::
ln' =>
Error (
msg "BTL.verify_is_copy_list: ln bigger than ln'")
|
nil =>
OK tt end
end.
Lemma verify_is_copy_correct dupmap cfg indirect pc pc' tt:
verify_is_copy dupmap cfg indirect pc pc' =
OK tt ->
match_nodes dupmap cfg indirect pc pc'.
Proof.
Local Hint Resolve verify_is_copy_correct:
core.
Lemma verify_is_copy_list_correct dupmap cfg indirect ln:
forall ln' tt,
verify_is_copy_list dupmap cfg indirect ln ln' =
OK tt ->
list_forall2 (
fun pc pc' =>
match_nodes dupmap cfg indirect pc pc')
ln ln'.
Proof.
induction ln.
- intros. destruct ln'; monadInv H. constructor.
- intros. destruct ln'; monadInv H. constructor; eauto.
Qed.
Fixpoint verify_block (
dupmap:
PTree.t node) (
cfg:
code) (
cfg':
RTL.code)
indirect isfst pc ib :
res (
option node) :=
match ib with
|
BF fi _ =>
match fi with
|
Bgoto pc1 =>
do u <-
verify_is_copy dupmap cfg indirect pc1 pc;
if negb isfst then
OK None
else Error (
msg "BTL.verify_block: isfst is true Bgoto")
|
Breturn or =>
match cfg'!
pc with
|
Some (
Ireturn or') =>
if option_eq Pos.eq_dec or or' then OK None
else Error (
msg "BTL.verify_block: different opt reg in Breturn")
| _ =>
Error (
msg "BTL.verify_block: incorrect cfg Breturn")
end
|
Bcall s ri lr r pc1 =>
match cfg'!
pc with
|
Some (
Icall s' ri' lr' r' pc2) =>
do u <-
verify_is_copy dupmap cfg indirect pc1 pc2;
if (
signature_eq s s')
then
if (
product_eq Pos.eq_dec QualIdent.eq ri ri')
then
if (
list_eq_dec Pos.eq_dec lr lr')
then
if (
Pos.eq_dec r r')
then OK None
else Error (
msg "BTL.verify_block: different r r' in Bcall")
else Error (
msg "BTL.verify_block: different lr in Bcall")
else Error (
msg "BTL.verify_block: different ri in Bcall")
else Error (
msg "BTL.verify_block: different signatures in Bcall")
| _ =>
Error (
msg "BTL.verify_block: incorrect cfg Bcall")
end
|
Btailcall s ri lr =>
match cfg'!
pc with
|
Some (
Itailcall s' ri' lr') =>
if (
signature_eq s s')
then
if (
product_eq Pos.eq_dec QualIdent.eq ri ri')
then
if (
list_eq_dec Pos.eq_dec lr lr')
then OK None
else Error (
msg "BTL.verify_block: different lr in Btailcall")
else Error (
msg "BTL.verify_block: different ri in Btailcall")
else Error (
msg "BTL.verify_block: different signatures in Btailcall")
| _ =>
Error (
msg "BTL.verify_block: incorrect cfg Btailcall")
end
|
Bbuiltin ef la br pc1 =>
match cfg'!
pc with
|
Some (
Ibuiltin ef' la' br' pc2) =>
do u <-
verify_is_copy dupmap cfg indirect pc1 pc2;
if (
external_function_eq ef ef')
then
if (
list_eq_dec builtin_arg_eq_pos la la')
then
if (
builtin_res_eq_pos br br')
then OK None
else Error (
msg "BTL.verify_block: different brr in Bbuiltin")
else Error (
msg "BTL.verify_block: different lbar in Bbuiltin")
else Error (
msg "BTL.verify_block: different ef in Bbuiltin")
| _ =>
Error (
msg "BTL.verify_block: incorrect cfg Bbuiltin")
end
|
Bjumptable r ln =>
match cfg'!
pc with
|
Some (
Ijumptable r' ln') =>
do u <-
verify_is_copy_list dupmap cfg indirect ln ln';
if (
Pos.eq_dec r r')
then OK None
else Error (
msg "BTL.verify_block: different r in Bjumptable")
| _ =>
Error (
msg "BTL.verify_block: incorrect cfg Bjumptable")
end
end
|
Bnop oiinfo =>
match oiinfo with
|
Some _ =>
match cfg'!
pc with
|
Some (
Inop pc') =>
OK (
Some pc')
| _ =>
Error (
msg "BTL.verify_block: incorrect cfg Bnop")
end
|
None =>
if negb isfst then OK (
Some pc)
else Error (
msg "BTL.verify_block: isfst is true Bnop (on_rtl is false)")
end
|
Bop op lr r _ =>
match cfg'!
pc with
|
Some (
Iop op' lr' r' pc') =>
if (
eq_operation op op')
then
if (
list_eq_dec Pos.eq_dec lr lr')
then
if (
Pos.eq_dec r r')
then
OK (
Some pc')
else Error (
msg "BTL.verify_block: different r in Bop")
else Error (
msg "BTL.verify_block: different lr in Bop")
else Error (
msg "BTL.verify_block: different operations in Bop")
| _ =>
Error (
msg "BTL.verify_block: incorrect cfg Bop")
end
|
Bload tm m a lr r _ =>
match cfg'!
pc with
|
Some (
Iload tm' m' a' lr' r' pc') =>
if (
trapping_mode_eq tm tm')
then
if (
chunk_eq m m')
then
if (
eq_addressing a a')
then
if (
list_eq_dec Pos.eq_dec lr lr')
then
if (
Pos.eq_dec r r')
then
OK (
Some pc')
else Error (
msg "BTL.verify_block: different r in Bload")
else Error (
msg "BTL.verify_block: different lr in Bload")
else Error (
msg "BTL.verify_block: different addressing in Bload")
else Error (
msg "BTL.verify_block: different chunk in Bload")
else Error (
msg "BTL.verify_block: different trapping_mode in Bload")
| _ =>
Error (
msg "BTL.verify_block: incorrect cfg Bload")
end
|
Bstore m a lr r _ =>
match cfg'!
pc with
|
Some (
Istore m' a' lr' r' pc') =>
if (
chunk_eq m m')
then
if (
eq_addressing a a')
then
if (
list_eq_dec Pos.eq_dec lr lr')
then
if (
Pos.eq_dec r r')
then OK (
Some pc')
else Error (
msg "BTL.verify_block: different r in Bstore")
else Error (
msg "BTL.verify_block: different lr in Bstore")
else Error (
msg "BTL.verify_block: different addressing in Bstore")
else Error (
msg "BTL.verify_block: different chunk in Bstore")
| _ =>
Error (
msg "BTL.verify_block: incorrect cfg Bstore")
end
|
Bseq b1 b2 =>
do opc <-
verify_block dupmap cfg cfg' indirect isfst pc b1;
match opc with
|
Some pc' =>
verify_block dupmap cfg cfg' indirect false pc' b2
|
None =>
Error (
msg "BTL.verify_block: None next pc in Bseq (deadcode)")
end
|
Bcond c lr bso bnot _ =>
match cfg'!
pc with
|
Some (
Icond c' lr' pcso pcnot i') =>
if (
list_eq_dec Pos.eq_dec lr lr')
then
if (
eq_condition c c')
then
do opc1 <-
verify_block dupmap cfg cfg' indirect false pcso bso;
do opc2 <-
verify_block dupmap cfg cfg' indirect false pcnot bnot;
match opc1,
opc2 with
|
None,
o =>
OK o
|
o,
None =>
OK o
|
Some x,
Some x' =>
if Pos.eq_dec x x' then OK (
Some x)
else Error (
msg "BTL.verify_block: is_join_opt incorrect for Bcond")
end
else Error (
msg "BTL.verify_block: incompatible conditions in Bcond")
else Error (
msg "BTL.verify_block: different lr in Bcond")
| _ =>
Error (
msg "BTL.verify_block: incorrect cfg Bcond")
end
end.
Lemma verify_block_correct dupmap cfg cfg' indirect ib:
forall pc isfst fin,
verify_block dupmap cfg cfg' indirect isfst pc ib = (
OK fin) ->
match_iblock dupmap cfg cfg' indirect isfst pc ib fin.
Proof.
induction ib;
intros;
try (
unfold verify_block in H;
destruct (
cfg'!
pc)
eqn:
EQCFG; [
idtac |
discriminate;
fail ]).
-
destruct fi;
unfold verify_block in H.
+
monadInv H.
destruct (
isfst);
simpl in EQ0;
inv EQ0.
eapply verify_is_copy_correct in EQ.
constructor;
assumption.
+
destruct (
cfg'!
pc)
eqn:
EQCFG;
try destruct i;
try discriminate.
destruct (
option_eq _ _ _);
try discriminate.
inv H.
eapply mib_BF;
eauto.
constructor.
+
destruct (
cfg'!
pc)
eqn:
EQCFG;
try destruct i;
try discriminate.
monadInv H.
eapply verify_is_copy_correct in EQ.
destruct (
signature_eq _ _);
try discriminate.
destruct (
product_eq _ _ _ _);
try discriminate.
destruct (
list_eq_dec _ _ _);
try discriminate.
destruct (
Pos.eq_dec _ _);
try discriminate.
subst.
inv EQ0.
eapply mib_BF;
eauto.
constructor;
assumption.
+
destruct (
cfg'!
pc)
eqn:
EQCFG;
try destruct i;
try discriminate.
destruct (
signature_eq _ _);
try discriminate.
destruct (
product_eq _ _ _ _);
try discriminate.
destruct (
list_eq_dec _ _ _);
try discriminate.
subst.
inv H.
eapply mib_BF;
eauto.
constructor.
+
destruct (
cfg'!
pc)
eqn:
EQCFG;
try destruct i;
try discriminate.
monadInv H.
eapply verify_is_copy_correct in EQ.
destruct (
external_function_eq _ _);
try discriminate.
destruct (
list_eq_dec _ _ _);
try discriminate.
destruct (
builtin_res_eq_pos _ _);
try discriminate.
subst.
inv EQ0.
eapply mib_BF;
eauto.
constructor;
assumption.
+
destruct (
cfg'!
pc)
eqn:
EQCFG;
try destruct i;
try discriminate.
monadInv H.
eapply verify_is_copy_list_correct in EQ.
destruct (
Pos.eq_dec _ _);
try discriminate.
subst.
inv EQ0.
eapply mib_BF;
eauto.
constructor;
assumption.
-
destruct oiinfo;
simpl in *.
+
destruct (
cfg'!
pc)
eqn:
EQCFG;
try discriminate.
destruct i0;
inv H.
constructor;
assumption.
+
destruct isfst;
try discriminate.
inv H.
constructor;
assumption.
-
destruct i;
try discriminate.
destruct (
eq_operation _ _);
try discriminate.
destruct (
list_eq_dec _ _ _);
try discriminate.
destruct (
Pos.eq_dec _ _);
try discriminate.
inv H.
constructor;
assumption.
-
destruct i;
try discriminate.
destruct (
trapping_mode_eq _ _);
try discriminate.
destruct (
chunk_eq _ _);
try discriminate.
destruct (
eq_addressing _ _);
try discriminate.
destruct (
list_eq_dec _ _ _);
try discriminate.
destruct (
Pos.eq_dec _ _);
try discriminate.
inv H.
constructor;
assumption.
-
destruct i;
try discriminate.
destruct (
chunk_eq _ _);
try discriminate.
destruct (
eq_addressing _ _);
try discriminate.
destruct (
list_eq_dec _ _ _);
try discriminate.
destruct (
Pos.eq_dec _ _);
try discriminate.
inv H.
constructor;
assumption.
-
monadInv H.
destruct x;
try discriminate.
eapply mib_seq_Some.
eapply IHib1;
eauto.
eapply IHib2;
eauto.
-
destruct i;
try discriminate.
destruct (
list_eq_dec _ _ _);
try discriminate.
destruct (
eq_condition _ _);
try discriminate.
fold (
verify_block dupmap cfg cfg' indirect false n ib1)
in H.
fold (
verify_block dupmap cfg cfg' indirect false n0 ib2)
in H.
monadInv H.
destruct x,
x0;
try destruct (
Pos.eq_dec _ _);
try discriminate.
all:
inv EQ2;
eapply mib_cond;
eauto;
econstructor.
Qed.
Local Hint Resolve verify_block_correct:
core.
Fixpoint verify_blocks dupmap (
cfg:
code) (
cfg':
RTL.code)
indirect l:
res unit :=
match l with
|
nil =>
OK tt
| (
pc,
pc')::
l =>
match cfg!
pc with
|
Some ib =>
do o <-
verify_block dupmap cfg cfg' indirect true pc' ib.(
entry);
match o with
|
None =>
verify_blocks dupmap cfg cfg' indirect l
| _ =>
Error(
msg "BTL.verify_blocks.end")
end
| _ =>
Error(
msg "BTL.verify_blocks.entry")
end
end.
Definition verify_cfg dupmap (
cfg:
code) (
cfg':
RTL.code)
indirect:
res unit :=
verify_blocks dupmap cfg cfg' indirect (
PTree.elements dupmap).
Lemma verify_cfg_correct dupmap cfg cfg' indirect tt:
verify_cfg dupmap cfg cfg' indirect =
OK tt ->
match_cfg dupmap cfg cfg' indirect.
Proof.
unfold verify_cfg.
intros X pc pc' H;
generalize X;
clear X.
exploit PTree.elements_correct;
eauto.
generalize tt pc pc' H;
clear pc pc' H.
generalize (
PTree.elements dupmap).
induction l as [|[
pc1 pc1']
l];
simpl.
-
tauto.
-
intros u pc pc' DUP H.
unfold bind.
repeat autodestruct.
intros;
subst.
destruct H as [
H|
H];
eauto.
inversion H;
subst.
eexists;
split;
eauto.
Qed.
Definition verify_function dupmap f f' indirect:
res unit :=
do dst <-
verify_is_copy dupmap (
fn_code f)
indirect (
fn_entrypoint f) (
RTL.fn_entrypoint f');
verify_cfg dupmap (
fn_code f) (
RTL.fn_code f')
indirect.
Lemma verify_function_correct dupmap f f' indirect tt:
verify_function dupmap f f' indirect =
OK tt ->
fn_sig f =
RTL.fn_sig f' ->
fn_params f =
RTL.fn_params f' ->
fn_stacksize f =
RTL.fn_stacksize f' ->
match_function dupmap f f' indirect.
Proof.