The BTL intermediate language: abstract syntax and semantics.
BTL stands for "Block Transfer Language".
Informally, a block is a piece of "loop-free" code, with a single entry-point,
hence, such that transformation preserving locally the semantics of each block,
preserve also globally the semantics of the function.
A BTL function is a CFG where each node is such a block, represented by structured code.
BTL gives a structured view of RTL code.
It is dedicated to optimizations validated by "symbolic simulation" over blocks.
Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import RTL Op Registers OptionMonad.
Require Import BTL_Invariants.
Require Import ValueDomain IntPromotionCommon IntPromotion.
Import ListNotations.
Abstract syntax
Definition exit :=
node.
Parameter inst_info_shadow :
Set.
Extract Constant inst_info_shadow =>
"BTLtypes.inst_info_shadow".
Inductive inst_promotion_info :=
|
IPromNone
|
IPromotableOp (
prom :
op_promotion_ceq)
|
IPromotableCond (
prom :
cond_promotion_ceq)
|
IPromotedOp (
op0 :
operation) (
prom :
op_promotion_ceq) (
sgn ret_sgn :
bool)
|
IPromotedCond (
cond0 :
condition) (
prom :
cond_promotion_ceq) (
sgn :
bool).
Definition meminv_annot_t :=
option (
list store_num_t).
Record inst_info :=
mk_iinfo {
addr_aval :
option aval;
istore_num :
store_num_t;
inst_promotion :
inst_promotion_info;
meminv_annot :
meminv_annot_t;
iinfo_shadow :
inst_info_shadow;
}.
Definition make_def_inst_info (
gh :
inst_info_shadow) :
inst_info :=
mk_iinfo None SNumNone IPromNone None gh.
Definition set_addr_aval (
a :
option aval) (
ii :
inst_info) :=
mk_iinfo a ii.(
istore_num)
ii.(
inst_promotion)
ii.(
meminv_annot)
ii.(
iinfo_shadow).
Definition set_inst_promotion (
prom :
inst_promotion_info) (
ii :
inst_info) :=
mk_iinfo ii.(
addr_aval)
ii.(
istore_num)
prom ii.(
meminv_annot)
ii.(
iinfo_shadow).
Definition copy_inst_info (
ii :
inst_info) (
gh :
inst_info_shadow) :
inst_info :=
mk_iinfo ii.(
addr_aval)
ii.(
istore_num)
ii.(
inst_promotion)
ii.(
meminv_annot)
gh.
Definition store_info_of_iinfo (
ii :
inst_info) :
store_info :=
{|
store_num :=
ii.(
istore_num);
store_aaddr :=
ii.(
addr_aval) |}.
Parameter block_info:
Set.
Extract Constant block_info =>
"BTLtypes.block_info".
Parameter function_info:
Set.
Extract Constant function_info =>
"BTLtypes.function_info".
final instructions (that stops block execution)
Inductive finalA (
A :
Type):
Type :=
|
Bgoto (
succ:
exit)
|
Breturn (
res:
option A)
terminates the execution of the current function. It returns the value of the given
register, or Vundef if none is given.
|
Bcall (
sig:
signature) (
fn:
A +
qualident) (
args:
list A) (
dest:
reg) (
succ:
exit)
invokes the function determined by fn (either a function pointer found in a register or a
function name), giving it the values of registers args as arguments.
It stores the return value in dest and branches to succ.
|
Btailcall (
sig:
signature) (
fn:
A +
qualident) (
args:
list A)
performs a function invocation in tail-call position
(the current function terminates after the call, returning the result of the callee)
|
Bbuiltin (
ef:
external_function) (
args:
list (
builtin_arg A)) (
dest:
builtin_res reg) (
succ:
exit)
calls the built-in function identified by ef, giving it the values of args as arguments.
It stores the return value in dest and branches to succ.
|
Bjumptable (
arg:
A) (
tbl:
list exit)
Bjumptable arg tbl transitions to the node that is the n-th
element of the list tbl, where n is the unsigned integer value of register arg.
.
Global Arguments Bgoto [_].
Global Arguments Breturn [_].
Global Arguments Bcall [_].
Global Arguments Btailcall [_].
Global Arguments Bbuiltin [_].
Global Arguments Bjumptable [_].
Definition final :=
finalA reg.
Inductive iblock:
Type :=
|
BF (
fi:
final) (
iinfo:
inst_info)
|
Bnop (
oiinfo:
option inst_info)
|
Bop (
op:
operation) (
args:
list reg) (
dest:
reg) (
iinfo:
inst_info)
performs the arithmetic operation op over the values of registers args, stores the result in dest
|
Bload (
trap:
trapping_mode) (
chunk:
memory_chunk) (
addr:
addressing) (
args:
list reg)
(
dest:
reg) (
iinfo:
inst_info)
loads a chunk quantity from the address determined by the addressing mode addr
and the values of the args registers, stores the quantity just read into dest.
If trap=NOTRAP, then failures lead to a default value written to dest.
|
Bstore (
chunk:
memory_chunk) (
addr:
addressing) (
args:
list reg) (
src:
reg) (
iinfo:
inst_info)
stores the value of register src in the chunk quantity at the
the address determined by the addressing mode addr and the
values of the args registers.
|
Bseq (
b1 b2:
iblock)
starts by running b1 and stops here if execution of b1 has reached a final instruction or aborted
or continue with b2 otherwise
|
Bcond (
cond:
condition) (
args:
list reg) (
ifso ifnot:
iblock) (
iinfo:
inst_info)
evaluates the boolean condition cond over the values of registers args.
If the condition is true, it continues on ifso.
If the condition is false, it continues on ifnot.
info is a shadow field there to provide information relative to branch prediction.
.
Coercion BF:
final >->
Funclass.
NB: - a RTL (Inop pc) ending a branch of block is encoded by (Bseq Bnop (Bgoto pc)).
- a RTL (Inop pc) in the middle of a branch is simply encoded by Bnop.
- the same trick appears for all "basic" instructions and Icond.
Record iblock_info :=
mk_ibinfo {
entry:
iblock;
binfo:
block_info
}.
Definition code:
Type :=
PTree.t iblock_info.
Record function:
Type :=
mkfunction {
fn_sig:
signature;
fn_params:
list reg;
fn_stacksize:
Z;
fn_code:
code;
fn_entrypoint:
node;
fn_gm:
gluemap;
fn_info:
function_info
}.
A function description comprises a control-flow graph (CFG) fn_code
(a partial finite mapping from nodes to instructions). As in Cminor,
fn_sig is the function signature and fn_stacksize the number of bytes
for its stack-allocated activation record. fn_params is the list
of registers that are bound to the values of arguments at call time.
fn_entrypoint is the node of the first instruction of the function
in the CFG.
Definition fundef :=
AST.fundef function.
Definition program :=
AST.program fundef unit.
Definition funsig (
fd:
fundef) :=
match fd with
|
Internal f =>
fn_sig f
|
External ef =>
ef_sig ef
end.
Operational semantics
Definition genv :=
Genv.t fundef unit.
The dynamic semantics of BTL is similar to RTL,
except that the step of one instruction is generalized into the run of one iblock.
Moreover, we maintain a shadow block_classification used to define the semantics of
the abstract values annotated on the addresses.
Inductive stackframe :
Type :=
|
Stackframe:
forall (
res:
reg)
(* where to store the result *)
(
f:
function)
(* calling function *)
(
sp:
val)
(* stack pointer in calling function *)
(
succ:
exit)
(* program point in calling function *)
(
rs:
regset),
(* register state in calling function *)
stackframe.
Inductive state :
Type :=
|
State:
forall (
stack:
list stackframe)
(* call stack *)
(
f:
function)
(* current function *)
(
sp:
val)
(* stack pointer *)
(
pc:
node)
(* current program point in c *)
(
rs:
regset)
(* register state *)
(
m:
mem)
(* memory state *)
(
bc:
block_classification),
state
|
Callstate:
forall (
stack:
list stackframe)
(* call stack *)
(
f:
fundef)
(* function to call *)
(
args:
list val)
(* arguments to the call *)
(
m:
mem)
(* memory state *)
(
bc:
block_classification),
state
|
Returnstate:
forall (
stack:
list stackframe)
(* call stack *)
(
v:
val)
(* return value for the call *)
(
m:
mem)
(* memory state *)
(
bc:
block_classification),
state.
Definition dummy_block_classification :
block_classification.
Proof.
exists (
fun _ =>
BCother);
discriminate 1.
Qed.
Definition reg_builtin_res (
res:
builtin_res reg):
option reg :=
match res with
|
BR r =>
Some r
| _ =>
None
end.
Inductive annot_sem :=
|
AnnotNone
|
AnnotUndef
|
AnnotTrap.
Section RELSEM.
Variable annot :
annot_sem.
Variable ge:
genv.
Definition find_function (
ros:
reg +
qualident) (
rs:
regset) :
option fundef :=
match ros with
|
inl r =>
Genv.find_funct ge rs#
r
|
inr symb =>
match Genv.find_symbol ge symb with
|
None =>
None
|
Some b =>
Genv.find_funct_ptr ge b
end
end.
Section AdditionnalProperties.
Inductive assert_prop (
p :
Prop) :
annot_sem ->
Prop :=
|
AssertLax :
assert_prop p AnnotNone
|
AssertTrue an (
A_TRUE :
p) :
assert_prop p an.
Inductive may_undef_prop (
p :
Prop) (
x :
val) :
annot_sem ->
val ->
Prop :=
|
MayUndefLax :
may_undef_prop p x AnnotNone x
|
MayUndefTrue an (
U_TRUE :
p):
may_undef_prop p x an x
|
MayUndefUndef (
U_FALSE : ~
p):
may_undef_prop p x AnnotUndef Vundef.
Lemma may_undef_prop_lax p x x':
may_undef_prop p x AnnotNone x' <->
x' =
x.
Proof.
split.
- inversion 1; reflexivity.
- intros ->; constructor.
Qed.
Lemma may_undef_morph p0 p1 x an y
(
F_EQ :
p0 <->
p1):
may_undef_prop p0 x an y <->
may_undef_prop p1 x an y.
Proof.
split; inversion 1; solve [constructor; rewrite F_EQ in *; assumption].
Qed.
Definition adp_op_promotable (
sp :
val) (
m :
mem) (
op :
operation) (
prom :
op_promotion_ceq) (
args :
list val)
:
Prop :=
sound_op_promotion (
promotable_op_strong ge sp m)
op prom args /\
list_val_promotes_eq prom.(
op_prom_args_eq)
args /\
if prom.(
op_prom_res_eq)
then if_Some (
eval_operation ge sp op args m)
val_promotes_eq else True.
Definition is_promotable_op (
iprom :
inst_promotion_info) :
option op_promotion_ceq :=
match iprom with
|
IPromotableOp prom =>
Some prom
| _ =>
None
end.
Definition adp_op (
sp :
val) (
m :
mem) (
op :
operation) (
args :
list val) (
iinfo :
inst_info) :
Prop :=
if_Some (
is_promotable_op iinfo.(
inst_promotion)) (
fun prom =>
adp_op_promotable sp m op prom args).
Definition adp_addr_match (
bc :
block_classification) (
sp :
val) (
addr :
addressing) (
args :
list val)
(
aa :
aval) :
Prop :=
if_Some (
eval_addressing ge sp addr args) (
fun va =>
vmatch bc va aa).
Definition udp_load (
bc :
block_classification) (
sp :
val) (
addr:
addressing) (
args:
list val)
(
iinfo:
inst_info) :
Prop :=
if_Some iinfo.(
addr_aval) (
adp_addr_match bc sp addr args).
Definition adp_store (
bc :
block_classification) (
sp :
val) (
addr :
addressing) (
args :
list val)
(
iinfo:
inst_info) :
Prop :=
if_Some iinfo.(
addr_aval) (
adp_addr_match bc sp addr args).
Definition adp_cond_promotable (
m :
mem) (
cond :
condition) (
prom :
cond_promotion_ceq) (
args :
list val) :
Prop :=
sound_cond_promotion (
promotable_cond_strong m)
cond prom args /\
list_val_promotes_eq prom.(
cond_prom_args_eq)
args.
Definition is_promotable_cond (
iprom :
inst_promotion_info) :
option cond_promotion_ceq :=
match iprom with
|
IPromotableCond prom =>
Some prom
| _ =>
None
end.
Definition adp_cond (
m :
mem) (
cond :
condition) (
args :
list val) (
iinfo :
inst_info) :
Prop :=
if_Some (
is_promotable_cond iinfo.(
inst_promotion)) (
fun prom =>
adp_cond_promotable m cond prom args).
Section Decidability.
Lemma rew_proj_sumbool_dec [
P Q :
Prop] (
p : {
P}+{~
P}) (
q : {
Q}+{~
Q})
(
EQ :
P <->
Q):
proj_sumbool p =
proj_sumbool q.
Proof.
destruct p, q; solve [reflexivity | exfalso; tauto].
Qed.
Definition if_Some_dec [
A P] (
x :
option A) (
p :
forall x :
A, {
P x}+{~
P x})
: {
if_Some x P }+{~
if_Some x P} :=
match x with
|
Some x =>
p x
|
None =>
left Logic.I
end.
Definition ex_Some_dec [
A P] (
x :
option A) (
p :
forall x :
A, {
P x}+{~
P x})
: {
ex_Some x P }+{~
ex_Some x P} :=
match x with
|
Some x =>
p x
|
None =>
right (
fun q =>
q)
end.
Definition alive_dec [
A] (
x :
option A)
:
let P :=
x <>
None in {
P}+{~
P}.
Proof.
case x as [x|]; [left|right]; congruence.
Defined.
Lemma forall_bool_decidable [
P :
bool ->
Prop] (
p :
forall b, {
P b}+{~
P b}):
{
forall b,
P b}+{~
forall b,
P b}.
Proof.
case (
p false); [
case (
p true)|];
intros.
1:
left;
intros [|];
assumption.
all:
right;
auto.
Defined.
Lemma and_decidable [
P Q]: {
P}+{~
P} -> {
Q}+{~
Q} -> {
P /\
Q}+{~(
P /\
Q)}.
Proof.
intros [|]; [intros [|]|intro]; (left + right); tauto.
Defined.
Lemma list_forall2_decidable [
A B] [
P :
A ->
B ->
Prop]
(
p :
forall (
x :
A) (
y :
B), {
P x y}+{~
P x y}) (
u :
list A) (
v :
list B):
let R :=
list_forall2 P u v in {
R}+{~
R}.
Proof.
revert v; induction u as [|x xs REC]; intros [|y ys]; try solve [right; inversion 1].
- left; constructor.
- case (p x y). 2:right; inversion 1; tauto.
case (REC ys). 2:right; inversion 1; tauto.
left; constructor; assumption.
Qed.
Lemma Z_bounded_dec (
lb :
Z) (
ub :
Z) (
P :
Z ->
Prop) (
dec :
forall m, {
P m}+{~
P m}):
let PI :=
forall m,
lb <=
m <
ub ->
P m in
{
PI}+{~
PI}.
Proof.
Lemma is_uns_dec (
n :
Z) (
i :
int):
{
is_uns n i}+{~
is_uns n i}.
Proof.
apply Z_bounded_dec;
intro m.
case (
Z_ge_dec m n)
as [|].
case (
Int.testbit i m)
as [|].
1:
right;
discriminate 1;
auto.
all:
left;
intros;
try reflexivity;
exfalso;
auto.
Qed.
Lemma is_sgn_dec (
n :
Z) (
i :
int):
{
is_sgn n i}+{~
is_sgn n i}.
Proof.
Lemma pmatch_dec bc b ofs a:
{
pmatch bc b ofs a}+{~
pmatch bc b ofs a}.
Proof.
case (
bc b)
eqn:
BC,
a;
try solve [
right;
inversion 1;
congruence |
left;
constructor;
auto];
try (
case (
Ptrofs.eq_dec ofs ofs0)
as [|]; [
subst ofs0|]);
try (
case (
QualIdent.eq id id0)
as [|]; [
subst id0|]);
try solve [
right;
inversion 1;
congruence |
left;
econstructor;
eauto;
congruence].
Qed.
Lemma vmatch_dec bc v a:
{
vmatch bc v a}+{~
vmatch bc v a}.
Proof.
case v,
a;
try solve [
right;
inversion 1 |
left;
constructor].
1,2:
case (
Int.eq_dec i n)
as [<-|]; [
left;
constructor |
right;
inversion 1;
congruence].
-
case (
Z_le_dec 0
n)
as [|].
case (
is_uns_dec n i)
as [|].
1:
left;
constructor;
auto.
all:
right;
inversion 1;
auto.
-
case (
Z_lt_dec 0
n)
as [|].
case (
is_sgn_dec n i)
as [|].
1:
left;
constructor;
auto.
all:
right;
inversion 1;
auto.
-
case (
Int64.eq_dec i n)
as [<-|]; [
left;
constructor |
right;
inversion 1;
congruence].
-
case (
Floats.Float.eq_dec f f0)
as [<-|]; [
left;
constructor |
right;
inversion 1;
congruence].
-
case (
Floats.Float32.eq_dec f f0)
as [<-|]; [
left;
constructor |
right;
inversion 1;
congruence].
-
case (
pmatch_dec bc b i p)
as [|]; [
left;
constructor |
right;
inversion 1];
auto.
-
case (
pmatch_dec bc b i p)
as [|]; [
left;
constructor |
right;
inversion 1];
auto.
Qed.
Lemma promotable_op_strong_dec sp m sgn op op' pargs pres args:
let P :=
promotable_op_strong ge sp m sgn op op' pargs pres args in
{
P}+{~
P}.
Proof.
Lemma list_val_promotes_eq_dec es vs:
let P :=
list_val_promotes_eq es vs in {
P}+{~
P}.
Proof.
Lemma adp_op_promotable_dec sp m op prom args:
let P :=
adp_op_promotable sp m op prom args in
{
P}+{~
P}.
Proof.
Lemma adp_op_dec sp m op args iinfo
: {
adp_op sp m op args iinfo}+{~
adp_op sp m op args iinfo}.
Proof.
Lemma promotable_cond_strong_dec m sgn cond cond' args:
let P :=
promotable_cond_strong m sgn cond cond' args in
{
P}+{~
P}.
Proof.
Lemma adp_cond_promotable_dec m cond prom args:
let P :=
adp_cond_promotable m cond prom args in
{
P}+{~
P}.
Proof.
Lemma adp_cond_dec m cond args iinfo
: {
adp_cond m cond args iinfo}+{~
adp_cond m cond args iinfo}.
Proof.
Definition adp_addr_match_dec bc sp addr args aa:
let P :=
adp_addr_match bc sp addr args aa in {
P}+{~
P}.
Proof.
Lemma udp_load_dec bc sp addr args iinfo:
let P :=
udp_load bc sp addr args iinfo in {
P}+{~
P}.
Proof.
Lemma adp_store_dec bc sp addr args iinfo:
let P :=
adp_store bc sp addr args iinfo in {
P}+{~
P}.
Proof.
End Decidability.
Section ValidPointerPreservation.
Variables m1 m2 :
mem.
Hypothesis VPE :
forall b z,
Mem.valid_pointer m1 b z =
Mem.valid_pointer m2 b z.
Lemma adp_op_promotable_valid_pointer_eq sp op prom args:
adp_op_promotable sp m1 op prom args <->
adp_op_promotable sp m2 op prom args.
Proof.
Lemma adp_op_valid_pointer_eq sp op args iinfo:
adp_op sp m1 op args iinfo <->
adp_op sp m2 op args iinfo.
Proof.
Lemma adp_cond_promotable_valid_pointer_eq cond prom args:
adp_cond_promotable m1 cond prom args <->
adp_cond_promotable m2 cond prom args.
Proof.
Lemma adp_cond_valid_pointer_eq cond args iinfo:
adp_cond m1 cond args iinfo <->
adp_cond m2 cond args iinfo.
Proof.
End ValidPointerPreservation.
End AdditionnalProperties.
internal big-step execution of one iblock
Inductive iblock_istep sp (
bc :
block_classification):
regset ->
mem ->
iblock ->
regset ->
mem ->
option final ->
Prop :=
|
exec_final rs m fin iinfo:
iblock_istep sp bc rs m (
BF fin iinfo)
rs m (
Some fin)
|
exec_nop rs m oiinfo:
iblock_istep sp bc rs m (
Bnop oiinfo)
rs m None
|
exec_op rs m op args res v iinfo
(
EVAL:
eval_operation ge sp op rs##
args m =
Some v)
(
ADP :
assert_prop (
adp_op sp m op rs##
args iinfo)
annot)
:
iblock_istep sp bc rs m (
Bop op args res iinfo) (
rs#
res <-
v)
m None
|
exec_load rs m trap chunk addr args dst v v' (
iinfo :
inst_info)
(
LOAD:
has_loaded ge sp rs m chunk addr args v trap)
(
UDP :
may_undef_prop (
udp_load bc sp addr rs##
args iinfo)
v annot v')
:
iblock_istep sp bc rs m (
Bload trap chunk addr args dst iinfo) (
rs#
dst <-
v')
m None
|
exec_store rs m chunk addr args src a m' (
iinfo :
inst_info)
(
EVAL:
eval_addressing ge sp addr rs##
args =
Some a)
(
ADP :
assert_prop (
adp_store bc sp addr rs##
args iinfo)
annot)
(
STORE:
Mem.storev chunk m a rs#
src =
Some m')
:
iblock_istep sp bc rs m (
Bstore chunk addr args src iinfo)
rs m' None
|
exec_seq_stop rs m b1 b2 rs' m' fin
(
EXEC:
iblock_istep sp bc rs m b1 rs' m' (
Some fin))
:
iblock_istep sp bc rs m (
Bseq b1 b2)
rs' m' (
Some fin)
|
exec_seq_continue rs m b1 b2 rs1 m1 rs' m' ofin
(
EXEC1:
iblock_istep sp bc rs m b1 rs1 m1 None)
(
EXEC2:
iblock_istep sp bc rs1 m1 b2 rs' m' ofin)
:
iblock_istep sp bc rs m (
Bseq b1 b2)
rs' m' ofin
|
exec_cond rs m cond args ifso ifnot b rs' m' ofin iinfo
(
EVAL:
eval_condition cond rs##
args m =
Some b)
(
ADP :
assert_prop (
adp_cond m cond rs##
args iinfo)
annot)
(
EXEC:
iblock_istep sp bc rs m (
if b then ifso else ifnot)
rs' m' ofin)
:
iblock_istep sp bc rs m (
Bcond cond args ifso ifnot iinfo)
rs' m' ofin
.
Local Open Scope list_scope.
Inductive final_step stack f sp rs m bc:
final ->
trace ->
state ->
Prop :=
|
exec_Bgoto pc:
final_step stack f sp rs m bc (
Bgoto pc)
E0
(
State stack f sp pc rs m bc)
|
exec_Breturn or stk m' bc':
sp = (
Vptr stk Ptrofs.zero) ->
Mem.free m stk 0
f.(
fn_stacksize) =
Some m' ->
final_step stack f sp rs m bc (
Breturn or)
E0 (
Returnstate stack (
regmap_optget or Vundef rs)
m' bc')
|
exec_Bcall sig ros args res pc' fd bc':
find_function ros rs =
Some fd ->
funsig fd =
sig ->
final_step stack f sp rs m bc (
Bcall sig ros args res pc')
E0 (
Callstate (
Stackframe res f sp pc' rs ::
stack)
fd rs##
args m bc')
|
exec_Btailcall sig ros args stk m' bc' fd:
find_function ros rs =
Some fd ->
funsig fd =
sig ->
sp = (
Vptr stk Ptrofs.zero) ->
Mem.free m stk 0
f.(
fn_stacksize) =
Some m' ->
final_step stack f sp rs m bc (
Btailcall sig ros args)
E0 (
Callstate stack fd rs##
args m' bc')
|
exec_Bbuiltin ef args res pc' vargs t vres m' bc':
eval_builtin_args ge (
fun r =>
rs#
r)
sp m args vargs ->
external_call ef ge vargs m t vres m' ->
final_step stack f sp rs m bc (
Bbuiltin ef args res pc')
t (
State stack f sp pc' (
regmap_setres res vres rs)
m' bc')
|
exec_Bjumptable arg tbl n pc':
rs#
arg =
Vint n ->
list_nth_z tbl (
Int.unsigned n) =
Some pc' ->
final_step stack f sp rs m bc (
Bjumptable arg tbl)
E0 (
State stack f sp pc' rs m bc)
.
big-step execution of one iblock
Definition iblock_step stack f sp rs m bc ib t s:
Prop :=
exists rs' m' fin,
iblock_istep sp bc rs m ib rs' m' (
Some fin) /\
final_step stack f sp rs' m' bc fin t s.
The transitions are presented as an inductive predicate
step ge st1 t st2, where ge is the global environment,
st1 the initial state, st2 the final state, and t the trace
of system calls performed during this transition.
Inductive step:
state ->
trace ->
state ->
Prop :=
|
exec_iblock stack ib f sp pc rs m bc t s
(
PC: (
fn_code f)!
pc =
Some ib)
(
STEP:
iblock_step stack f sp rs m bc ib.(
entry)
t s)
:
step (
State stack f sp pc rs m bc)
t s
|
exec_function_internal stack f args m bc m' bc' stk
(
ARGS:
Val.has_argtype_list args f.(
fn_sig).(
sig_args))
(
ALLOC:
Mem.alloc m 0
f.(
fn_stacksize) = (
m',
stk))
:
step (
Callstate stack (
Internal f)
args m bc)
E0 (
State stack
f
(
Vptr stk Ptrofs.zero)
f.(
fn_entrypoint)
(
init_regs args f.(
fn_params))
m' bc')
|
exec_function_external stack ef args res t m bc m' bc'
(
EXTCALL:
external_call ef ge args m t res m')
:
step (
Callstate stack (
External ef)
args m bc)
t (
Returnstate stack res m' bc')
|
exec_return stack res f sp pc rs vres m bc bc'
:
step (
Returnstate (
Stackframe res f sp pc rs ::
stack)
vres m bc)
E0 (
State stack f sp pc (
rs#
res <-
vres)
m bc')
.
End RELSEM.
Section RUNSEM.
A functional variant iblock_istep_run of iblock_istep AnnotNone.
Lemma iblock_istep_run_equiv below provides a proof that "relation" iblock_istep is a "partial function".
Local Open Scope option_monad_scope.
Local Hint Constructors iblock_istep:
core.
Local Hint Resolve AssertLax MayUndefLax:
core.
outcome of a block execution
Record outcome :=
out {
_rs:
regset;
_m:
mem;
_fin:
option final
}.
Fixpoint iblock_istep_run (
ge :
genv)
sp ib rs m:
option outcome :=
match ib with
|
BF fin _ =>
Some {|
_rs :=
rs;
_m :=
m;
_fin :=
Some fin |}
|
Bnop _ =>
Some {|
_rs :=
rs;
_m:=
m;
_fin :=
None |}
|
Bop op args res iinfo =>
SOME v <-
eval_operation ge sp op rs##
args m IN
Some {|
_rs :=
rs#
res <-
v;
_m:=
m;
_fin :=
None |}
|
Bload TRAP chunk addr args dst iinfo =>
SOME a <-
eval_addressing ge sp addr rs##
args IN
SOME v <-
Mem.loadv chunk m a IN
Some {|
_rs :=
rs#
dst <-
v;
_m:=
m;
_fin :=
None |}
|
Bload NOTRAP chunk addr args dst iinfo =>
let v :=
match eval_addressing ge sp addr rs##
args with
|
Some a =>
match Mem.loadv chunk m a with
|
Some v =>
v
|
None =>
Vundef
end
|
None =>
Vundef
end in
Some {|
_rs :=
rs#
dst <-
v;
_m:=
m;
_fin :=
None |}
|
Bstore chunk addr args src iinfo =>
SOME a <-
eval_addressing ge sp addr rs##
args IN
SOME m' <-
Mem.storev chunk m a rs#
src IN
Some {|
_rs :=
rs;
_m:=
m';
_fin :=
None |}
|
Bseq b1 b2 =>
SOME out1 <-
iblock_istep_run ge sp b1 rs m IN
match out1.(
_fin)
with
|
None =>
iblock_istep_run ge sp b2 out1.(
_rs)
out1.(
_m)
| _ =>
Some out1
end
|
Bcond cond args ifso ifnot iinfo =>
SOME b <-
eval_condition cond rs##
args m IN
iblock_istep_run ge sp (
if b then ifso else ifnot)
rs m
end.
Lemma iblock_istep_run_equiv_load ge sp bc ib v v' rs rs' m trap chunk addr args dst iinfo ofin
(
IB:
ib =
Bload trap chunk addr args dst iinfo)
(
RS':
rs' =
rs #
dst <-
v')
(
LOAD:
has_loaded ge sp rs m chunk addr args v trap)
(
UDP :
may_undef_prop (
udp_load ge bc sp addr rs##
args iinfo)
v AnnotNone v'):
iblock_istep AnnotNone ge sp bc rs m ib rs' m ofin <->
iblock_istep_run ge sp ib rs m =
Some {|
_rs :=
rs';
_m :=
m;
_fin :=
ofin |}.
Proof.
rewrite may_undef_prop_lax in UDP;
subst v'.
subst;
split;
intro H.
-
inv H;
clear LOAD0.
simpl;
inv LOAD.
+
rewrite EVAL,
LOAD0;
repeat autodestruct.
+
repeat autodestruct.
intro LOAD;
exfalso.
rewrite (
LOAD0 _
eq_refl)
in LOAD;
congruence.
-
replace ofin with (@
None final)
by (
revert H;
simpl;
repeat autodestruct).
eauto.
Qed.
Local Hint Resolve iblock_istep_run_equiv_load:
core.
Lemma iblock_istep_run_equiv ge sp bc rs m ib rs' m' ofin:
iblock_istep AnnotNone ge sp bc rs m ib rs' m' ofin <->
iblock_istep_run ge sp ib rs m =
Some {|
_rs :=
rs';
_m:=
m';
_fin :=
ofin |}.
Proof.
split.
-
induction 1;
try solve [
eapply iblock_istep_run_equiv_load;
eauto];
simpl;
repeat autodestruct;
try_simplify_someHyps.
-
revert rs m rs' m' ofin.
induction ib;
intros until ofin;
intro R;
generalize R;
simpl;
repeat autodestruct;
try solve [
try_simplify_someHyps];
intros;
try (
injection R0 as ?;
subst).
all:
try solve [
eapply exec_load; [
eapply has_loaded_normal|];
eauto
|
eapply iblock_istep_run_equiv_load;
eauto;
apply has_loaded_default;
congruence].
+
destruct o;
try_simplify_someHyps;
subst;
eauto.
Qed.
End RUNSEM.
Execution of whole programs are described as sequences of transitions
from an initial state to a final state. An initial state is a Callstate
corresponding to the invocation of the ``main'' function of the program
without arguments and with an empty call stack.
Inductive initial_state (
p:
program):
state ->
Prop :=
|
initial_state_intro:
forall b f m0 bc0,
let ge :=
Genv.globalenv p in
Genv.init_mem p =
Some m0 ->
Genv.find_symbol ge p.(
prog_main) =
Some b ->
Genv.find_funct_ptr ge b =
Some f ->
funsig f =
signature_main ->
initial_state p (
Callstate nil f nil m0 bc0).
A final state is a Returnstate with an empty call stack.
Inductive final_state:
state ->
int ->
Prop :=
|
final_state_intro:
forall r m bc,
final_state (
Returnstate nil (
Vint r)
m bc)
r.
Definition sem (
annot :
annot_sem) (
p:
program) :=
Semantics (
step annot) (
initial_state p)
final_state (
Genv.globalenv p).
Auxiliary general purpose functions on BTL
Definition is_goto (
ib:
iblock):
bool :=
match ib with
|
BF (
Bgoto _) _ =>
true
| _ =>
false
end.
Simulation of the AnnotTrap semantics by the AnnotUndef one
Module Trap_to_Undef.
Lemma transf_assert_prop P:
assert_prop P AnnotTrap ->
assert_prop P AnnotUndef.
Proof.
inversion 1; constructor; auto.
Qed.
Lemma transf_may_undef_prop P v v':
may_undef_prop P v AnnotTrap v' ->
may_undef_prop P v AnnotUndef v'.
Proof.
inversion 1; constructor; auto.
Qed.
Lemma transf_iblock_istep ge sp bc rs0 m0 ib rs1 m1 fin:
iblock_istep AnnotTrap ge sp bc rs0 m0 ib rs1 m1 fin ->
iblock_istep AnnotUndef ge sp bc rs0 m0 ib rs1 m1 fin.
Proof.
Lemma transf_step ge s0 t s1:
step AnnotTrap ge s0 t s1 ->
step AnnotUndef ge s0 t s1.
Proof.
inversion 1;
econstructor;
eauto.
case STEP as (
rs1 &
m1 &
fin &
ISTEP &
FIN).
eapply transf_iblock_istep in ISTEP.
repeat (
esplit;
try eassumption).
Qed.
Lemma transf_program p:
forward_simulation (
sem AnnotTrap p) (
sem AnnotUndef p).
Proof.
End Trap_to_Undef.
Simulation of the AnnotUndef semantics by the AnnotNone one
Additional lessdef lemmas
Lemma has_loaded_lessdef (
ge :
genv)
sp rs rs' m m' chk addr args v trap
(
LD_RS:
regs_lessdef rs rs')
(
LD_M:
Mem.extends m m')
(
LOAD:
has_loaded ge sp rs m chk addr args v trap):
exists v',
has_loaded ge sp rs' m' chk addr args v' trap /\
Val.lessdef v v'.
Proof.
Lemma regmap_optget_lessdef r d d' rs rs'
(
LD_D :
Val.lessdef d d')
(
LD_RS :
regs_lessdef rs rs'):
Val.lessdef (
regmap_optget r d rs) (
regmap_optget r d' rs').
Proof.
case r as [r|]; simpl; eauto.
Qed.
Lemma find_function_lessdef ge ros rs rs' fd
(
LD_RS :
regs_lessdef rs rs'):
find_function ge ros rs =
Some fd ->
find_function ge ros rs' =
Some fd.
Proof.
Lemma init_regs_lessdef vs vs' rs
(
LD_VS :
Val.lessdef_list vs vs'):
regs_lessdef (
init_regs vs rs) (
init_regs vs' rs).
Proof.
revert vs vs' LD_VS;
induction rs;
intros ? ?;
simpl.
-
constructor.
-
case vs;
inversion 1; [
constructor|].
intro r;
rewrite !
Regmap.gsspec;
case peq as [|];
auto.
apply IHrs;
assumption.
Qed.
Lemma may_undef_prop_lessdef P v bc v':
may_undef_prop P v bc v' ->
Val.lessdef v' v.
Proof.
inversion 1; constructor.
Qed.
Module Undef_to_Lax.
Local Hint Resolve AssertLax MayUndefLax :
core.
Lemma transf_iblock_istep ge sp bc rs0 rs0' m0 m0' ib rs1 m1 fin
(
STEP :
iblock_istep AnnotUndef ge sp bc rs0 m0 ib rs1 m1 fin)
(
M_RS :
regs_lessdef rs0 rs0')
(
M_M :
Mem.extends m0 m0'):
exists rs1' m1',
iblock_istep AnnotNone ge sp bc rs0' m0' ib rs1' m1' fin /\
regs_lessdef rs1 rs1' /\
Mem.extends m1 m1'.
Proof.
Inductive match_stackframe:
stackframe ->
stackframe ->
Prop :=
|
match_stackframe_intro
sp res f pc rs rs'
(
M_RS:
regs_lessdef rs rs')
:
match_stackframe (
Stackframe res f sp pc rs)
(
Stackframe res f sp pc rs').
Definition match_stackframes :
list stackframe ->
list stackframe ->
Prop :=
list_forall2 match_stackframe.
Inductive match_states:
state ->
state ->
Prop :=
|
match_states_norm stk stk' f pc sp rs rs' m m' bc
(
STACK :
match_stackframes stk stk')
(
M_RS :
regs_lessdef rs rs')
(
M_M :
Mem.extends m m')
:
match_states (
State stk f sp pc rs m bc)
(
State stk' f sp pc rs' m' bc)
|
match_states_call stk stk' f args args' m m' bc
(
STACK :
match_stackframes stk stk')
(
M_ARGS :
Val.lessdef_list args args')
(
M_M :
Mem.extends m m')
:
match_states (
Callstate stk f args m bc)
(
Callstate stk' f args' m' bc)
|
match_states_return stk stk' v v' m m' bc
(
STACK :
match_stackframes stk stk')
(
M_V :
Val.lessdef v v')
(
M_M :
Mem.extends m m')
:
match_states (
Returnstate stk v m bc)
(
Returnstate stk' v' m' bc).
Lemma transf_final_step ge stk stk' f sp rs rs' m m' bc fin t s
(
STEP :
final_step ge stk f sp rs m bc fin t s)
(
M_STK :
match_stackframes stk stk')
(
M_RS :
regs_lessdef rs rs')
(
M_M :
Mem.extends m m'):
exists s',
final_step ge stk' f sp rs' m' bc fin t s' /\
match_states s s'.
Proof.
Lemma transf_step ge s0 s0' t s1
(
STEP :
step AnnotUndef ge s0 t s1)
(
MATCH :
match_states s0 s0'):
exists s1',
step AnnotNone ge s0' t s1' /\
match_states s1 s1'.
Proof.
Lemma transf_program p:
forward_simulation (
sem AnnotUndef p) (
sem AnnotNone p).
Proof.
End Undef_to_Lax.
Other lemmas
Lemma find_function_match [
match_fundef match_varinfo ctx p tp]
(
TRANSL: @
Linking.match_program_gen program fundef unit fundef unit _
match_fundef match_varinfo ctx p tp)
(
fp :
reg +
qualident)
rs f:
find_function (
Genv.globalenv p)
fp rs =
Some f ->
exists (
cunit :
program) (
tf :
fundef),
find_function (
Genv.globalenv tp)
fp rs =
Some tf /\
match_fundef cunit f tf /\
Linking.linkorder cunit ctx.
Proof.
Lemma has_loaded_preserved [
F1 F2 V1 V2 :
Type] (
ge1 :
Genv.t F1 V1) (
ge2 :
Genv.t F2 V2)
(
agree_on_symbols :
forall s,
Genv.find_symbol ge2 s =
Genv.find_symbol ge1 s)
sp rs m chk addr args v trap:
has_loaded ge2 sp rs m chk addr args v trap <->
has_loaded ge1 sp rs m chk addr args v trap.
Proof.
Section Preservation.
Variables ge1 ge2 :
genv.
Hypothesis agree_on_symbols:
forall s,
Genv.find_symbol ge2 s =
Genv.find_symbol ge1 s.
Lemma adp_op_promotable_preserved sp m op prom args:
adp_op_promotable ge2 sp m op prom args <->
adp_op_promotable ge1 sp m op prom args.
Proof.
Lemma adp_op_preserved sp m op args iinfo:
adp_op ge2 sp m op args iinfo <->
adp_op ge1 sp m op args iinfo.
Proof.
Lemma adp_addr_match_preserved bc sp addr args av:
adp_addr_match ge2 bc sp addr args av <->
adp_addr_match ge1 bc sp addr args av.
Proof.
Lemma udp_load_preserved bc sp addr args iinfo:
udp_load ge2 bc sp addr args iinfo <->
udp_load ge1 bc sp addr args iinfo.
Proof.
Lemma adp_store_preserved bc sp addr args iinfo:
adp_store ge2 bc sp addr args iinfo <->
adp_store ge1 bc sp addr args iinfo.
Proof.
End Preservation.