Library Tunnelingproof
Correctness proof for the branch tunneling optimization.
Require Import Coqlib.
Require Import Maps.
Require Import UnionFind.
Require Import AST.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Locations.
Require Import LTL.
Require Import Tunneling.
A variant of
record_goto that also incrementally computes a measure f: node -> nat
counting the number of Lnop instructions starting at a given pc that were eliminated.
Definition measure_edge (u: U.t) (pc s: node) (f: node -> nat) : node -> nat :=
fun x => if peq (U.repr u s) pc then f x
else if peq (U.repr u x) pc then (f x + f s + 1)%nat
else f x.
Definition record_goto' (uf: U.t * (node -> nat)) (pc: node) (i: instruction) : U.t * (node -> nat) :=
match i with
| Lnop s => let (u, f) := uf in (U.union u pc s, measure_edge u pc s f)
| _ => uf
end.
Definition branch_map_correct (c: code) (uf: U.t * (node -> nat)): Prop :=
forall pc,
match c!pc with
| Some(Lnop s) =>
U.repr (fst uf) pc = pc \/ (U.repr (fst uf) pc = U.repr (fst uf) s /\ snd uf s < snd uf pc)%nat
| _ =>
U.repr (fst uf) pc = pc
end.
Lemma record_gotos'_correct:
forall c,
branch_map_correct c (PTree.fold record_goto' c (U.empty, fun (x: node) => O)).
Definition record_gotos' (f: function) :=
PTree.fold record_goto' f.(fn_code) (U.empty, fun (x: node) => O).
Lemma record_gotos_gotos':
forall f, fst (record_gotos' f) = record_gotos f.
Definition branch_target (f: function) (pc: node) : node :=
U.repr (record_gotos f) pc.
Definition count_gotos (f: function) (pc: node) : nat :=
snd (record_gotos' f) pc.
Theorem record_gotos_correct:
forall f pc,
match f.(fn_code)!pc with
| Some(Lnop s) =>
branch_target f pc = pc \/
(branch_target f pc = branch_target f s /\ count_gotos f s < count_gotos f pc)%nat
| _ => branch_target f pc = pc
end.
Section PRESERVATION.
Variable p: program.
Let tp := tunnel_program p.
Let ge := Genv.globalenv p.
Let tge := Genv.globalenv tp.
Lemma functions_translated:
forall v f,
Genv.find_funct ge v = Some f ->
Genv.find_funct tge v = Some (tunnel_fundef f).
Proof (@Genv.find_funct_transf _ _ _ tunnel_fundef p).
Lemma function_ptr_translated:
forall v f,
Genv.find_funct_ptr ge v = Some f ->
Genv.find_funct_ptr tge v = Some (tunnel_fundef f).
Proof (@Genv.find_funct_ptr_transf _ _ _ tunnel_fundef p).
Lemma symbols_preserved:
forall id,
Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef p).
Lemma sig_preserved:
forall f, funsig (tunnel_fundef f) = funsig f.
Lemma find_function_translated:
forall ros ls f,
find_function ge ros ls = Some f ->
find_function tge ros ls = Some (tunnel_fundef f).
The proof of semantic preservation is a simulation argument
based on diagrams of the following form:
The
In the definition of
st1 --------------- st2
| |
t| ?|t
| |
v v
st1'--------------- st2'
The
match_states predicate, defined below, captures the precondition
between states st1 and st2, as well as the postcondition between
st1' and st2'. One transition in the source code (left) can correspond
to zero or one transition in the transformed code (right). The
"zero transition" case occurs when executing a Lgoto instruction
in the source code that has been removed by tunneling.
In the definition of
match_states, note that only the control-flow
(in particular, the current program point pc) is changed:
the values of locations and the memory states are identical in the
original and transformed codes.
Definition tunneled_code (f: function) :=
PTree.map (fun pc b => tunnel_instr (record_gotos f) b) (fn_code f).
Inductive match_stackframes: stackframe -> stackframe -> Prop :=
| match_stackframes_intro:
forall res f sp ls0 pc,
match_stackframes
(Stackframe res f sp ls0 pc)
(Stackframe res (tunnel_function f) sp ls0 (branch_target f pc)).
Inductive match_states: state -> state -> Prop :=
| match_states_intro:
forall s f sp pc ls m ts,
list_forall2 match_stackframes s ts ->
match_states (State s f sp pc ls m)
(State ts (tunnel_function f) sp (branch_target f pc) ls m)
| match_states_call:
forall s f ls m ts,
list_forall2 match_stackframes s ts ->
match_states (Callstate s f ls m)
(Callstate ts (tunnel_fundef f) ls m)
| match_states_return:
forall s ls m ts,
list_forall2 match_stackframes s ts ->
match_states (Returnstate s ls m)
(Returnstate ts ls m).
To preserve non-terminating behaviours, we show that the transformed
code cannot take an infinity of "zero transition" cases.
We use the following
measure function over source states,
which decreases strictly in the "zero transition" case.
Definition measure (st: state) : nat :=
match st with
| State s f sp pc ls m => count_gotos f pc
| Callstate s f ls m => 0%nat
| Returnstate s ls m => 0%nat
end.
Lemma tunnel_function_lookup:
forall f pc i,
f.(fn_code)!pc = Some i ->
(tunnel_function f).(fn_code)!pc = Some (tunnel_instr (record_gotos f) i).
Lemma tunnel_step_correct:
forall st1 t st2, step ge st1 t st2 ->
forall st1' (MS: match_states st1 st1'),
(exists st2', step tge st1' t st2' /\ match_states st2 st2')
\/ (measure st2 < measure st1 /\ t = E0 /\ match_states st2 st1')%nat.
Lemma transf_initial_states:
forall st1, initial_state p st1 ->
exists st2, initial_state tp st2 /\ match_states st1 st2.
Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2 -> final_state st1 r -> final_state st2 r.
Theorem transf_program_correct:
forall (beh: program_behavior), not_wrong beh ->
exec_program p beh -> exec_program tp beh.
End PRESERVATION.