The RTL intermediate language: abstract syntax and semantics.
RTL stands for "Register Transfer Language". This is the first
intermediate language after Cminor and CminorSel.
Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Abstract syntax
RTL is organized as instructions, functions and programs.
Instructions correspond roughly to elementary instructions of the
target processor, but take their arguments and leave their results
in pseudo-registers (also called temporaries in textbooks).
Infinitely many pseudo-registers are available, and each function
has its own set of pseudo-registers, unaffected by function calls.
Instructions are organized as a control-flow graph: a function is
a finite map from ``nodes'' (abstract program points) to instructions,
and each instruction lists explicitly the nodes of its successors.
Definition node :=
positive.
Inductive assert_arg:
Type :=
|
AA_reg (
r:
reg)
|
AA_load (
chk:
memory_chunk) (
addr:
addressing) (
args:
list reg).
Inductive instruction:
Type :=
|
Inop:
node ->
instruction
No operation -- just branch to the successor.
|
Iop:
operation ->
list reg ->
reg ->
node ->
instruction
Iop op args dest succ performs the arithmetic operation op
over the values of registers args, stores the result in dest,
and branches to succ.
|
Iload:
trapping_mode ->
memory_chunk ->
addressing ->
list reg ->
reg ->
node ->
instruction
Iload trap chunk addr args dest succ 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, and branches to succ.
If trap=NOTRAP, then failures lead to a default value written to dest.
|
Istore:
memory_chunk ->
addressing ->
list reg ->
reg ->
node ->
instruction
Istore chunk addr args src succ 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, then branches to succ.
|
Icall:
signature ->
reg +
qualident ->
list reg ->
reg ->
node ->
instruction
Icall sig fn args dest succ 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.
|
Itailcall:
signature ->
reg +
qualident ->
list reg ->
instruction
Itailcall sig fn args performs a function invocation
in tail-call position.
|
Ibuiltin:
external_function ->
list (
builtin_arg reg) ->
builtin_res reg ->
node ->
instruction
Ibuiltin ef args dest succ 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.
|
Icond:
condition ->
list reg ->
node ->
node ->
option bool ->
instruction
Icond cond args ifso ifnot info evaluates the boolean condition
cond over the values of registers args. If the condition
is true, it transitions to ifso. If the condition is false,
it transitions to ifnot. info is a shadow field there to provide
information relative to branch prediction.
|
Ijumptable:
reg ->
list node ->
instruction
Ijumptable 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.
|
Ireturn:
option reg ->
instruction
Ireturn terminates the execution of the current function
(it has no successor). It returns the value of the given
register, or Vundef if none is given.
|
Iassert:
condition ->
list assert_arg ->
node ->
instruction.
Iassert cond args succ is a ghost instruction that ensures
that condition cond evaluates to true on args, and branches to succ.
It is used to propagate information from forward correctness proof
to backward robustness proofs
Definition eq_ros :
forall ros1 ros2 :
reg+
qualident,
{
ros1 =
ros2 } + {
ros1 <>
ros2 }.
Proof.
Definition eq_builtin_res :
forall br1 br2 : (
builtin_res reg),
{
br1 =
br2 } + {
br1 <>
br2 }.
Proof.
generalize peq.
induction br1;
decide equality.
Defined.
Definition eq_builtin_arg :
forall ba1 ba2 : (
builtin_arg reg),
{
ba1 =
ba2 } + {
ba1 <>
ba2 }.
Proof.
Definition eq_assert_arg :
forall ba1 ba2 :
assert_arg,
{
ba1 =
ba2 } + {
ba1 <>
ba2 }.
Proof.
generalize peq.
generalize eq_addressing.
induction ba1;
repeat decide equality.
Defined.
Definition bool_eq_dec:
forall a b:
bool, {
a=
b}+{
a<>
b}.
Proof.
decide equality.
Defined.
Definition option_eq_dec:
forall {
T :
Type}
(
T_eq_dec :
forall a b :
T, {
a=
b}+{
a<>
b}),
forall x y :
option T, {
x=
y}+{
x<>
y}.
Proof.
decide equality.
Defined.
Definition eq_instruction :
forall i1 i2 :
instruction,
{
i1 =
i2 } + {
i1 <>
i2 }.
Proof.
Definition code:
Type :=
PTree.t instruction.
Definition eq_code:
forall (
c1 c2 :
code) , {
c1 =
c2} + {
c1 <>
c2}.
Proof.
intros.
destruct (
PTree.beq_correct eq_instruction c1 c2)
as (
CORRECT1 &
CORRECT2).
destruct (
PTree.beq eq_instruction c1 c2).
-
left.
apply PTree.extensionality.
intro.
clear CORRECT2.
pose proof (
CORRECT1 eq_refl i)
as CORRECT.
clear CORRECT1.
destruct (
c1 !
i)
as [
c1o | ];
destruct (
c2 !
i)
as [
c2o | ].
+
destruct (
eq_instruction c1o c2o);
cbn in CORRECT;
congruence.
+
contradiction.
+
contradiction.
+
reflexivity.
-
right.
intro EQ.
clear CORRECT1.
subst c2.
assert (
false =
true)
as ZZ. 2:
congruence.
apply CORRECT2.
intro.
destruct (
c1 !
x). 2: (
trivial;
fail).
destruct (
eq_instruction i i);
cbn;
congruence.
Defined.
Record function:
Type :=
mkfunction {
fn_sig:
signature;
fn_params:
list reg;
fn_stacksize:
Z;
fn_code:
code;
fn_entrypoint:
node
}.
Definition eq_function:
forall f1 f2 :
function, {
f1=
f2} + {
f1<>
f2}.
Proof.
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 eq_fundef (
fd1 fd2 :
fundef) : {
fd1=
fd2} + {
fd1<>
fd2}.
Proof.
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.
Definition regset :=
Regmap.t val.
Fixpoint init_regs (
vl:
list val) (
rl:
list reg) {
struct rl} :
regset :=
match rl,
vl with
|
r1 ::
rs,
v1 ::
vs =>
Regmap.set r1 v1 (
init_regs vs rs)
| _, _ =>
Regmap.init Vundef
end.
The dynamic semantics of RTL is given in small-step style, as a
set of transitions between states. A state captures the current
point in the execution. Three kinds of states appear in the transitions:
-
State cs f sp pc rs m describes an execution point within a function.
f is the current function.
sp is the pointer to the stack block for its current activation
(as in Cminor).
pc is the current program point (CFG node) within the code c.
rs gives the current values for the pseudo-registers.
m is the current memory state.
-
Callstate cs f args m is an intermediate state that appears during
function calls.
f is the function definition that we are calling.
args (a list of values) are the arguments for this call.
m is the current memory state.
-
Returnstate cs v m is an intermediate state that appears when a
function terminates and returns to its caller.
v is the return value and m the current memory state.
In all three kinds of states, the
cs parameter represents the call stack.
It is a list of frames
Stackframe res f sp pc rs. Each frame represents
a function call in progress.
res is the pseudo-register that will receive the result of the call.
f is the calling function.
sp is its stack pointer.
pc is the program point for the instruction that follows the call.
rs is the state of registers in the calling function.
Inductive stackframe :
Type :=
|
Stackframe:
forall (
res:
reg)
(* where to store the result *)
(
f:
function)
(* calling function *)
(
sp:
val)
(* stack pointer in calling function *)
(
pc:
node)
(* 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 *)
state
|
Callstate:
forall (
stack:
list stackframe)
(* call stack *)
(
f:
fundef)
(* function to call *)
(
args:
list val)
(* arguments to the call *)
(
m:
mem),
(* memory state *)
state
|
Returnstate:
forall (
stack:
list stackframe)
(* call stack *)
(
v:
val)
(* return value for the call *)
(
m:
mem),
(* memory state *)
state.
Inductive has_loaded {
F V:
Type} (
genv:
Genv.t F V)
sp rs m chunk addr args v:
trapping_mode ->
Prop :=
|
has_loaded_normal a trap
(
EVAL:
eval_addressing genv sp addr rs##
args =
Some a)
(
LOAD:
Mem.loadv chunk m a =
Some v)
:
has_loaded genv sp rs m chunk addr args v trap
|
has_loaded_default
(
LOAD:
forall a,
eval_addressing genv sp addr rs##
args =
Some a ->
Mem.loadv chunk m a =
None)
(
DEFAULT:
v =
Vundef)
:
has_loaded genv sp rs m chunk addr args v NOTRAP
.
Local Hint Constructors has_loaded:
core.
Inductive eval_assert_arg {
F V:
Type} (
ge:
Genv.t F V) (
sp:
val) (
rs:
regset) (
m:
mem) :
assert_arg ->
val ->
Prop :=
|
eval_AA_reg:
forall r,
eval_assert_arg ge sp rs m (
AA_reg r) (
rs #
r)
|
eval_AA_load:
forall chk addr args a v
(
EVAL:
eval_addressing ge sp addr rs##
args =
Some a)
(
LOAD:
Mem.loadv chk m a =
Some v),
eval_assert_arg ge sp rs m (
AA_load chk addr args)
v.
Definition eval_assert_args {
F V:
Type} (
ge:
Genv.t F V)
sp rs m al vl :=
list_forall2 (
eval_assert_arg ge sp rs m)
al vl.
Section RELSEM.
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.
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_Inop:
forall s f sp pc rs m pc',
(
fn_code f)!
pc =
Some(
Inop pc') ->
step (
State s f sp pc rs m)
E0 (
State s f sp pc' rs m)
|
exec_Iop:
forall s f sp pc rs m op args res pc' v,
(
fn_code f)!
pc =
Some(
Iop op args res pc') ->
eval_operation ge sp op rs##
args m =
Some v ->
step (
State s f sp pc rs m)
E0 (
State s f sp pc' (
rs#
res <-
v)
m)
|
exec_Iload:
forall s f sp pc rs m trap chunk addr args dst pc' v,
(
fn_code f)!
pc =
Some(
Iload trap chunk addr args dst pc') ->
has_loaded ge sp rs m chunk addr args v trap ->
step (
State s f sp pc rs m)
E0 (
State s f sp pc' (
rs#
dst <-
v)
m)
|
exec_Istore:
forall s f sp pc rs m chunk addr args src pc' a m',
(
fn_code f)!
pc =
Some(
Istore chunk addr args src pc') ->
eval_addressing ge sp addr rs##
args =
Some a ->
Mem.storev chunk m a rs#
src =
Some m' ->
step (
State s f sp pc rs m)
E0 (
State s f sp pc' rs m')
|
exec_Icall:
forall s f sp pc rs m sig ros args res pc' fd,
(
fn_code f)!
pc =
Some(
Icall sig ros args res pc') ->
find_function ros rs =
Some fd ->
funsig fd =
sig ->
step (
State s f sp pc rs m)
E0 (
Callstate (
Stackframe res f sp pc' rs ::
s)
fd rs##
args m)
|
exec_Itailcall:
forall s f stk pc rs m sig ros args fd m',
(
fn_code f)!
pc =
Some(
Itailcall sig ros args) ->
find_function ros rs =
Some fd ->
funsig fd =
sig ->
Mem.free m stk 0
f.(
fn_stacksize) =
Some m' ->
step (
State s f (
Vptr stk Ptrofs.zero)
pc rs m)
E0 (
Callstate s fd rs##
args m')
|
exec_Ibuiltin:
forall s f sp pc rs m ef args res pc' vargs t vres m',
(
fn_code f)!
pc =
Some(
Ibuiltin ef args res pc') ->
eval_builtin_args ge (
fun r =>
rs#
r)
sp m args vargs ->
external_call ef ge vargs m t vres m' ->
step (
State s f sp pc rs m)
t (
State s f sp pc' (
regmap_setres res vres rs)
m')
|
exec_Icond:
forall s f sp pc rs m cond args ifso ifnot b pc' predb,
(
fn_code f)!
pc =
Some(
Icond cond args ifso ifnot predb) ->
eval_condition cond rs##
args m =
Some b ->
pc' = (
if b then ifso else ifnot) ->
step (
State s f sp pc rs m)
E0 (
State s f sp pc' rs m)
|
exec_Ijumptable:
forall s f sp pc rs m arg tbl n pc',
(
fn_code f)!
pc =
Some(
Ijumptable arg tbl) ->
rs#
arg =
Vint n ->
list_nth_z tbl (
Int.unsigned n) =
Some pc' ->
step (
State s f sp pc rs m)
E0 (
State s f sp pc' rs m)
|
exec_Ireturn:
forall s f stk pc rs m or m',
(
fn_code f)!
pc =
Some(
Ireturn or) ->
Mem.free m stk 0
f.(
fn_stacksize) =
Some m' ->
step (
State s f (
Vptr stk Ptrofs.zero)
pc rs m)
E0 (
Returnstate s (
regmap_optget or Vundef rs)
m')
|
exec_Iassert:
forall s f sp pc rs m cond args pc' vargs,
(
fn_code f)!
pc =
Some(
Iassert cond args pc') ->
eval_assert_args ge sp rs m args vargs ->
eval_condition cond vargs m =
Some true ->
step (
State s f sp pc rs m)
E0 (
State s f sp pc' rs m)
|
exec_function_internal:
forall s f args m m' stk,
Val.has_argtype_list args f.(
fn_sig).(
sig_args) ->
Mem.alloc m 0
f.(
fn_stacksize) = (
m',
stk) ->
step (
Callstate s (
Internal f)
args m)
E0 (
State s
f
(
Vptr stk Ptrofs.zero)
f.(
fn_entrypoint)
(
init_regs args f.(
fn_params))
m')
|
exec_function_external:
forall s ef args res t m m',
external_call ef ge args m t res m' ->
step (
Callstate s (
External ef)
args m)
t (
Returnstate s res m')
|
exec_return:
forall res f sp pc rs s vres m,
step (
Returnstate (
Stackframe res f sp pc rs ::
s)
vres m)
E0 (
State s f sp pc (
rs#
res <-
vres)
m).
Lemma exec_Iop':
forall s f sp pc rs m op args res pc' rs' v,
(
fn_code f)!
pc =
Some(
Iop op args res pc') ->
eval_operation ge sp op rs##
args m =
Some v ->
rs' = (
rs#
res <-
v) ->
step (
State s f sp pc rs m)
E0 (
State s f sp pc' rs' m).
Proof.
intros.
subst rs'.
eapply exec_Iop;
eauto.
Qed.
Lemma exec_Iload':
forall s f sp pc rs m trap chunk addr args dst pc' rs' a v,
(
fn_code f)!
pc =
Some(
Iload trap chunk addr args dst pc') ->
eval_addressing ge sp addr rs##
args =
Some a ->
Mem.loadv chunk m a =
Some v ->
rs' = (
rs#
dst <-
v) ->
step (
State s f sp pc rs m)
E0 (
State s f sp pc' rs' m).
Proof.
End RELSEM.
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,
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).
A final state is a Returnstate with an empty call stack.
Inductive final_state:
state ->
int ->
Prop :=
|
final_state_intro:
forall r m,
final_state (
Returnstate nil (
Vint r)
m)
r.
The small-step semantics for a program.
Definition semantics (
p:
program) :=
Semantics step (
initial_state p)
final_state (
Genv.globalenv p).
This semantics is receptive to changes in events.
Lemma semantics_receptive:
forall (
p:
program),
receptive (
semantics p).
Proof.
Operations on RTL abstract syntax
Transformation of a RTL function instruction by instruction.
This applies a given transformation function to all instructions
of a function and constructs a transformed function from that.
Section TRANSF.
Variable transf:
node ->
instruction ->
instruction.
Definition transf_function (
f:
function) :
function :=
mkfunction
f.(
fn_sig)
f.(
fn_params)
f.(
fn_stacksize)
(
PTree.map transf f.(
fn_code))
f.(
fn_entrypoint).
End TRANSF.
Computation of the possible successors of an instruction.
This is used in particular for dataflow analyses.
Definition successors_instr (
i:
instruction) :
list node :=
match i with
|
Inop s =>
s ::
nil
|
Iop op args res s =>
s ::
nil
|
Iload trap chunk addr args dst s =>
s ::
nil
|
Istore chunk addr args src s =>
s ::
nil
|
Icall sig ros args res s =>
s ::
nil
|
Itailcall sig ros args =>
nil
|
Ibuiltin ef args res s =>
s ::
nil
|
Icond cond args ifso ifnot _ =>
ifso ::
ifnot ::
nil
|
Ijumptable arg tbl =>
tbl
|
Ireturn optarg =>
nil
|
Iassert _ _
s =>
s ::
nil
end.
Definition successors_map (
f:
function) :
PTree.t (
list node) :=
PTree.map1 successors_instr f.(
fn_code).
The registers used by an instruction
Fixpoint params_of_assert_arg (
a:
assert_arg) :
list reg :=
match a with
|
AA_reg x =>
x ::
nil
|
AA_load _ _
args =>
args
end.
Definition params_of_assert_args (
al:
list assert_arg) :
list reg :=
List.flat_map params_of_assert_arg al.
Definition instr_uses (
i:
instruction) :
list reg :=
match i with
|
Inop s =>
nil
|
Iop op args res s =>
args
|
Iload trap chunk addr args dst s =>
args
|
Istore chunk addr args src s =>
src ::
args
|
Icall sig (
inl r)
args res s =>
r ::
args
|
Icall sig (
inr id)
args res s =>
args
|
Itailcall sig (
inl r)
args =>
r ::
args
|
Itailcall sig (
inr id)
args =>
args
|
Ibuiltin ef args res s =>
params_of_builtin_args args
|
Icond cond args ifso ifnot _ =>
args
|
Ijumptable arg tbl =>
arg ::
nil
|
Ireturn None =>
nil
|
Ireturn (
Some arg) =>
arg ::
nil
|
Iassert _
args _ =>
params_of_assert_args args
end.
The register defined by an instruction, if any
Definition instr_defs (
i:
instruction) :
option reg :=
match i with
|
Inop s =>
None
|
Iop op args res s =>
Some res
|
Iload trap chunk addr args dst s =>
Some dst
|
Istore chunk addr args src s =>
None
|
Icall sig ros args res s =>
Some res
|
Itailcall sig ros args =>
None
|
Ibuiltin ef args res s =>
match res with BR r =>
Some r | _ =>
None end
|
Icond cond args ifso ifnot _ =>
None
|
Ijumptable arg tbl =>
None
|
Ireturn optarg =>
None
|
Iassert _ _ _ =>
None
end.
Maximum PC (node number) in the CFG of a function. All nodes of
the CFG of f are between 1 and max_pc_function f (inclusive).
Definition max_pc_function (
f:
function) :=
PTree.fold (
fun m pc i =>
Pos.max m pc)
f.(
fn_code) 1%
positive.
Lemma max_pc_function_sound:
forall f pc i,
f.(
fn_code)!
pc =
Some i ->
Ple pc (
max_pc_function f).
Proof.
Maximum pseudo-register mentioned in a function. All results or arguments
of an instruction of f, as well as all parameters of f, are between
1 and max_reg_function (inclusive).
Definition max_reg_instr (
m:
positive) (
pc:
node) (
i:
instruction) :=
match i with
|
Inop s =>
m
|
Iop op args res s =>
fold_left Pos.max args (
Pos.max res m)
|
Iload trap chunk addr args dst s =>
fold_left Pos.max args (
Pos.max dst m)
|
Istore chunk addr args src s =>
fold_left Pos.max args (
Pos.max src m)
|
Icall sig (
inl r)
args res s =>
fold_left Pos.max args (
Pos.max r (
Pos.max res m))
|
Icall sig (
inr id)
args res s =>
fold_left Pos.max args (
Pos.max res m)
|
Itailcall sig (
inl r)
args =>
fold_left Pos.max args (
Pos.max r m)
|
Itailcall sig (
inr id)
args =>
fold_left Pos.max args m
|
Ibuiltin ef args res s =>
fold_left Pos.max (
params_of_builtin_args args)
(
fold_left Pos.max (
params_of_builtin_res res)
m)
|
Icond cond args ifso ifnot _ =>
fold_left Pos.max args m
|
Ijumptable arg tbl =>
Pos.max arg m
|
Ireturn None =>
m
|
Ireturn (
Some arg) =>
Pos.max arg m
|
Iassert _
args s =>
fold_left Pos.max (
params_of_assert_args args)
m
end.
Definition max_reg_function (
f:
function) :=
Pos.max
(
PTree.fold max_reg_instr f.(
fn_code) 1%
positive)
(
fold_left Pos.max f.(
fn_params) 1%
positive).
Remark max_reg_instr_ge:
forall m pc i,
Ple m (
max_reg_instr m pc i).
Proof.
intros.
assert (
X:
forall l n,
Ple m n ->
Ple m (
fold_left Pos.max l n)).
{
induction l;
simpl;
intros.
auto.
apply IHl.
extlia. }
destruct i;
simpl;
try (
destruct s0);
repeat (
apply X);
try extlia.
destruct o;
extlia.
Qed.
Remark max_reg_instr_def:
forall m pc i r,
instr_defs i =
Some r ->
Ple r (
max_reg_instr m pc i).
Proof.
intros.
assert (
X:
forall l n,
Ple r n ->
Ple r (
fold_left Pos.max l n)).
{
induction l;
simpl;
intros.
extlia.
apply IHl.
extlia. }
destruct i;
simpl in *;
inv H.
-
apply X.
extlia.
-
apply X.
extlia.
-
destruct s0;
apply X;
extlia.
-
destruct b;
inv H1.
apply X.
simpl.
extlia.
Qed.
Remark max_reg_instr_uses:
forall m pc i r,
In r (
instr_uses i) ->
Ple r (
max_reg_instr m pc i).
Proof.
intros.
assert (
X:
forall l n,
In r l \/
Ple r n ->
Ple r (
fold_left Pos.max l n)).
{
induction l;
simpl;
intros.
tauto.
apply IHl.
destruct H0 as [[
A|
A]|
A].
right;
subst;
extlia.
auto.
right;
extlia. }
destruct i;
simpl in *;
try (
destruct s0);
try (
apply X;
auto).
-
contradiction.
-
destruct H.
right;
subst;
extlia.
auto.
-
destruct H.
right;
subst;
extlia.
auto.
-
destruct H.
right;
subst;
extlia.
auto.
-
intuition.
subst;
extlia.
-
destruct o;
simpl in H;
intuition.
subst;
extlia.
Qed.
Lemma max_reg_function_def:
forall f pc i r,
f.(
fn_code)!
pc =
Some i ->
instr_defs i =
Some r ->
Ple r (
max_reg_function f).
Proof.
Lemma max_reg_function_use:
forall f pc i r,
f.(
fn_code)!
pc =
Some i ->
In r (
instr_uses i) ->
Ple r (
max_reg_function f).
Proof.
Lemma max_reg_function_params:
forall f r,
In r f.(
fn_params) ->
Ple r (
max_reg_function f).
Proof.
Section EVAL_ASSERT_ARG_PRESERVED.
Variables F1 V1 F2 V2:
Type.
Variable ge1:
Genv.t F1 V1.
Variable ge2:
Genv.t F2 V2.
Variable sp:
val.
Variable rs:
regset.
Variable m:
mem.
Hypothesis symbols_preserved:
forall id,
Genv.find_symbol ge2 id =
Genv.find_symbol ge1 id.
Lemma eval_assert_arg_preserved:
forall a v,
eval_assert_arg ge1 sp rs m a v ->
eval_assert_arg ge2 sp rs m a v.
Proof.
Lemma eval_assert_args_preserved:
forall al vl,
eval_assert_args ge1 sp rs m al vl ->
eval_assert_args ge2 sp rs m al vl.
Proof.
End EVAL_ASSERT_ARG_PRESERVED.
Section EVAL_ASSERT_ARG_LESSDEF.
Variable F V:
Type.
Variable ge:
Genv.t F V.
Variable sp:
val.
Variable rs1 rs2:
regset.
Variables m1 m2:
mem.
Hypothesis mem_extends:
Mem.extends m1 m2.
Lemma eval_assert_arg_lessdef:
forall a v1,
eval_assert_arg ge sp rs1 m1 a v1 ->
(
forall x,
In x (
params_of_assert_arg a) ->
Val.lessdef rs1#
x rs2#
x) ->
exists v2,
eval_assert_arg ge sp rs2 m2 a v2 /\
Val.lessdef v1 v2.
Proof.
induction 1;
intros IN;
simpl in IN.
-
do 2
esplit.
econstructor.
eauto.
-
eapply eval_addressing_lessdef with (
vl2:=
rs2 ##
args)
in EVAL as (?&
EVAL'&
INJ);
eauto.
2:{
clear EVAL.
induction args;
constructor;
eauto with datatypes. }
eapply Mem.loadv_extends in LOAD as (?&?&?);
eauto.
do 2
esplit;
eauto.
econstructor;
eauto.
Qed.
Lemma eval_assert_args_lessdef:
forall al vl1,
eval_assert_args ge sp rs1 m1 al vl1 ->
(
forall x,
In x (
params_of_assert_args al) ->
Val.lessdef rs1#
x rs2#
x) ->
exists vl2,
eval_assert_args ge sp rs2 m2 al vl2 /\
Val.lessdef_list vl1 vl2.
Proof.
induction 1;
intros IN;
simpl in IN.
-
econstructor;
split.
constructor.
auto.
-
exploit eval_assert_arg_lessdef;
eauto with datatypes.
intros (
v1' &
P &
Q).
destruct IHlist_forall2 as (
vl' &
U & ?
V);
eauto with datatypes.
exists (
v1'::
vl');
split;
constructor;
auto.
Qed.
End EVAL_ASSERT_ARG_LESSDEF.