Translation from Cminor to CFG.
Require Import Coqlib.
Require Errors.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Switch.
Require Import Cminor.
Require Import CFG.
Open Local Scope string_scope.
Translation environments and state
The translation functions modify a global state, comprising the
current state of the control-flow graph for the function being translated,
as well as sources of fresh CFG nodes.
Record state:
Type :=
mkstate {
st_nextnode:
positive;
st_code:
code;
st_wf:
forall (
pc:
positive),
Plt pc st_nextnode \/
st_code!
pc =
None
}.
Operations over the global state satisfy a crucial monotonicity property:
nodes are only added to the CFG, but are never removed nor their
instructions are changed; similarly, fresh nodes are only consumed,
but never reused. This property is captured by the following predicate over
states, which we show is a partial order.
Inductive state_incr:
state ->
state ->
Prop :=
state_incr_intro:
forall (
s1 s2:
state),
Ple s1.(
st_nextnode)
s2.(
st_nextnode) ->
(
forall pc,
s1.(
st_code)!
pc =
None \/
s2.(
st_code)!
pc =
s1.(
st_code)!
pc) ->
state_incr s1 s2.
Lemma state_incr_refl:
forall s,
state_incr s s.
Proof.
Lemma state_incr_trans:
forall s1 s2 s3,
state_incr s1 s2 ->
state_incr s2 s3 ->
state_incr s1 s3.
Proof.
The state and error monad
The translation functions can fail to produce CFG code. They must
also modify the global state, adding new nodes to the control-flow
graph and generating fresh temporary registers. In a language like
ML or Java, we would use exceptions to report errors and mutable data
structures to modify the global state. These luxuries are not
available in Coq, however. Instead, we use a monadic encoding of the
translation: translation functions take the current global state as
argument, and return either Error msg to denote an error,
or OK r s incr to denote success. s is the modified state, r
the result value of the translation function. and incr a proof
that the final state is in the state_incr relation with the
initial state. In the error case, msg is an error message (see
modules Errors) describing the problem.
We now define this monadic encoding -- the ``state and error'' monad --
as well as convenient syntax to express monadic computations.
Inductive res (
A:
Type) (
s:
state):
Type :=
|
Error:
Errors.errmsg ->
res A s
|
OK:
A ->
forall (
s':
state),
state_incr s s' ->
res A s.
Implicit Arguments OK [
A s].
Implicit Arguments Error [
A s].
Definition mon (
A:
Type) :
Type :=
forall (
s:
state),
res A s.
Definition ret (
A:
Type) (
x:
A) :
mon A :=
fun (
s:
state) =>
OK x s (
state_incr_refl s).
Implicit Arguments ret [
A].
Definition error (
A:
Type) (
msg:
Errors.errmsg) :
mon A :=
fun (
s:
state) =>
Error msg.
Implicit Arguments error [
A].
Definition bind (
A B:
Type) (
f:
mon A) (
g:
A ->
mon B) :
mon B :=
fun (
s:
state) =>
match f s with
|
Error msg =>
Error msg
|
OK a s'
i =>
match g a s'
with
|
Error msg =>
Error msg
|
OK b s''
i' =>
OK b s'' (
state_incr_trans s s'
s''
i i')
end
end.
Implicit Arguments bind [
A B].
Definition bind2 (
A B C:
Type) (
f:
mon (
A *
B)) (
g:
A ->
B ->
mon C) :
mon C :=
bind f (
fun xy =>
g (
fst xy) (
snd xy)).
Implicit Arguments bind2 [
A B C].
Notation "'
do'
X <-
A ;
B" := (
bind A (
fun X =>
B))
(
at level 200,
X ident,
A at level 100,
B at level 200).
Notation "'
do' (
X ,
Y ) <-
A ;
B" := (
bind2 A (
fun X Y =>
B))
(
at level 200,
X ident,
Y ident,
A at level 100,
B at level 200).
Definition handle_error (
A:
Type) (
f g:
mon A) :
mon A :=
fun (
s:
state) =>
match f s with
|
OK a s'
i =>
OK a s'
i
|
Error _ =>
g s
end.
Implicit Arguments handle_error [
A].
Operations on state
The initial state (empty CFG).
Remark init_state_wf:
forall pc,
Plt pc 1%
positive \/ (
PTree.empty instruction)!
pc =
None.
Proof.
Definition init_state :
state :=
mkstate 1%
positive (
PTree.empty instruction)
init_state_wf.
Adding a node with the given instruction to the CFG. Return the
label of the new node.
Remark add_instr_wf:
forall s i pc,
let n :=
s.(
st_nextnode)
in
Plt pc (
Psucc n) \/ (
PTree.set n i s.(
st_code))!
pc =
None.
Proof.
Remark add_instr_incr:
forall s i,
let n :=
s.(
st_nextnode)
in
state_incr s (
mkstate (
Psucc n) (
PTree.set n i s.(
st_code)) (
add_instr_wf s i)).
Proof.
Definition add_instr (
i:
instruction) :
mon node :=
fun s =>
let n :=
s.(
st_nextnode)
in
OK n
(
mkstate (
Psucc n) (
PTree.set n i s.(
st_code)) (
add_instr_wf s i))
(
add_instr_incr s i).
add_instr can be decomposed in two steps: reserving a fresh
CFG node, and filling it later with an instruction. This is needed
to compile loops.
Remark reserve_instr_wf:
forall s pc,
Plt pc (
Psucc s.(
st_nextnode)) \/
s.(
st_code)!
pc =
None.
Proof.
Remark reserve_instr_incr:
forall s,
let n :=
s.(
st_nextnode)
in
state_incr s (
mkstate (
Psucc n)
s.(
st_code) (
reserve_instr_wf s)).
Proof.
intros;
constructor;
simpl.
apply Ple_succ.
auto.
Qed.
Definition reserve_instr:
mon node :=
fun (
s:
state) =>
let n :=
s.(
st_nextnode)
in
OK n
(
mkstate (
Psucc n)
s.(
st_code) (
reserve_instr_wf s))
(
reserve_instr_incr s).
Remark update_instr_wf:
forall s n i,
Plt n s.(
st_nextnode) ->
forall pc,
Plt pc s.(
st_nextnode) \/ (
PTree.set n i s.(
st_code))!
pc =
None.
Proof.
intros.
case (
peq pc n);
intro.
subst pc;
left;
assumption.
rewrite PTree.gso;
auto.
exact (
st_wf s pc).
Qed.
Remark update_instr_incr:
forall s n i (
LT:
Plt n s.(
st_nextnode)),
s.(
st_code)!
n =
None ->
state_incr s
(
mkstate s.(
st_nextnode) (
PTree.set n i s.(
st_code)) (
update_instr_wf s n i LT)).
Proof.
intros.
constructor;
simpl;
intros.
apply Ple_refl.
rewrite PTree.gsspec.
destruct (
peq pc n).
left;
congruence.
right;
auto.
Qed.
Definition check_empty_node:
forall (
s:
state) (
n:
node), {
s.(
st_code)!
n =
None } + {
True }.
Proof.
intros.
case (
s.(
st_code)!
n);
intros.
right;
auto.
left;
auto.
Defined.
Definition update_instr (
n:
node) (
i:
instruction) :
mon unit :=
fun s =>
match plt n s.(
st_nextnode),
check_empty_node s n with
|
left LT,
left EMPTY =>
OK tt
(
mkstate s.(
st_nextnode) (
PTree.set n i s.(
st_code))
(
update_instr_wf s n i LT))
(
update_instr_incr s n i LT EMPTY)
|
_,
_ =>
Error (
Errors.msg "
CFGgen.update_instr")
end.
CFG generation *
Definition transl_exit (
nexits:
list node) (
n:
nat) :
mon node :=
match nth_error nexits n with
|
None =>
error (
Errors.msg "
CFGgen:
wrong exit")
|
Some ne =>
ret ne
end.
Fixpoint transl_cases (
nexits:
list node) (
tbl:
table nat) :
mon (
table node) :=
match tbl with
|
nil =>
ret nil
| (
v1,
x1) ::
tl =>
do n1 <-
transl_exit nexits x1;
do nl <-
transl_cases nexits tl;
ret ((
v1,
n1) ::
nl)
end.
Translation of statements. transl_stmt s nd nexits nret enriches
the current CFG with the instructions necessary to execute the Cminor
statement s, and returns the node of the first instruction in this
sequence. The generated instructions continue at node nd if the
statement terminates normally, and at the n-th node in the list nlist
if it terminates by an exit n construct.
Definition labelmap :
Type :=
PTree.t node.
Fixpoint transl_stmt (
s:
stmt) (
nd:
node) (
nexits:
list node) (
ngoto:
labelmap)
{
struct s} :
mon node :=
match s with
|
Sskip =>
ret nd
|
Sassign v b =>
add_instr (
Iassign v b nd)
|
Sstore chunk a b =>
add_instr (
Istore chunk a b nd)
|
Scall optid sig b cl =>
add_instr (
Icall optid sig b cl nd)
|
Stailcall sig b cl =>
add_instr (
Itailcall sig b cl)
|
Sbuiltin optid ef al =>
add_instr (
Ibuiltin optid ef al nd)
|
Sseq s1 s2 =>
do ns <-
transl_stmt s2 nd nexits ngoto;
transl_stmt s1 ns nexits ngoto
|
Sifthenelse a strue sfalse =>
do ntrue <-
transl_stmt strue nd nexits ngoto;
do nfalse <-
transl_stmt sfalse nd nexits ngoto;
add_instr (
Iifthenelse a ntrue nfalse)
|
Sloop sbody =>
do n1 <-
reserve_instr;
do n2 <-
transl_stmt sbody n1 nexits ngoto;
do xx <-
update_instr n1 (
Iskip n2);
add_instr (
Iskip n2)
|
Sblock sbody =>
transl_stmt sbody nd (
nd ::
nexits)
ngoto
|
Sexit n =>
transl_exit nexits n
|
Sswitch a cases default =>
do ncases <-
transl_cases nexits cases;
do ndefault <-
transl_exit nexits default;
add_instr (
Iswitch a ncases ndefault)
|
Sreturn optexpr =>
add_instr (
Ireturn optexpr)
|
Slabel lbl s' =>
do ns <-
transl_stmt s'
nd nexits ngoto;
match ngoto!
lbl with
|
None =>
error (
Errors.msg "
CFGgen:
unbound label")
|
Some n =>
do xx <-
(
handle_error (
update_instr n (
Iskip ns))
(
error (
Errors.MSG "
Multiply-
defined label " ::
Errors.CTX lbl ::
nil)));
ret ns
end
|
Sgoto lbl =>
match ngoto!
lbl with
|
None =>
error (
Errors.MSG "
Undefined defined label " ::
Errors.CTX lbl ::
nil)
|
Some n =>
ret n
end
end.
Preallocate CFG nodes for each label defined in the function body.
Definition alloc_label (
lbl:
Cminor.label) (
maps:
labelmap *
state) :
labelmap *
state :=
let (
map,
s) :=
maps in
let n :=
s.(
st_nextnode)
in
(
PTree.set lbl n map,
mkstate (
Psucc s.(
st_nextnode))
s.(
st_code) (
reserve_instr_wf s)).
Fixpoint reserve_labels (
s:
stmt) (
ms:
labelmap *
state)
{
struct s} :
labelmap *
state :=
match s with
|
Sseq s1 s2 =>
reserve_labels s1 (
reserve_labels s2 ms)
|
Sifthenelse c s1 s2 =>
reserve_labels s1 (
reserve_labels s2 ms)
|
Sloop s1 =>
reserve_labels s1 ms
|
Sblock s1 =>
reserve_labels s1 ms
|
Slabel lbl s1 =>
alloc_label lbl (
reserve_labels s1 ms)
|
_ =>
ms
end.
Translation of a Cminor function.
Definition transl_fun (
f:
Cminor.function) (
ngoto:
labelmap):
mon node :=
do nret <-
add_instr (
Ireturn None);
do nentry <-
transl_stmt f.(
Cminor.fn_body)
nret nil ngoto;
ret nentry.
Definition transl_function (
f:
Cminor.function) :
Errors.res CFG.function :=
let (
ngoto,
s0) :=
reserve_labels f.(
fn_body) (
PTree.empty node,
init_state)
in
match transl_fun f ngoto s0 with
|
Error msg =>
Errors.Error msg
|
OK nentry s i =>
Errors.OK (
CFG.mkfunction
f.(
Cminor.fn_sig)
f.(
Cminor.fn_params)
f.(
Cminor.fn_vars)
f.(
Cminor.fn_stackspace)
s.(
st_code)
nentry)
end.
Definition transl_fundef :=
transf_partial_fundef transl_function.
Translation of a whole program.
Definition transl_program (
p:
Cminor.program) :
Errors.res CFG.program :=
transform_partial_program transl_fundef p.