Library compcert.common.AST
This file defines a number of data types and operations used in
the abstract syntax trees of many of the intermediate languages.
Require Import String.
Require Import Coqlib Maps Errors Integers Floats.
Require Archi.
Set Implicit Arguments.
Syntactic elements
The intermediate languages are weakly typed, using the following types:
Inductive typ : Type :=
| Tint
| Tfloat
| Tlong
| Tsingle
| Tany32
| Tany64.
Lemma typ_eq: ∀ (t1 t2: typ), {t1=t2} + {t1≠t2}.
Proof. decide equality. Defined.
Global Opaque typ_eq.
Definition opt_typ_eq: ∀ (t1 t2: option typ), {t1=t2} + {t1≠t2}
:= option_eq typ_eq.
Definition list_typ_eq: ∀ (l1 l2: list typ), {l1=l2} + {l1≠l2}
:= list_eq_dec typ_eq.
Definition Tptr : typ := if Archi.ptr64 then Tlong else Tint.
Definition typesize (ty: typ) : Z :=
match ty with
| Tint ⇒ 4
| Tfloat ⇒ 8
| Tlong ⇒ 8
| Tsingle ⇒ 4
| Tany32 ⇒ 4
| Tany64 ⇒ 8
end.
Lemma typesize_pos: ∀ ty, typesize ty > 0.
Proof. destruct ty; simpl; omega. Qed.
Lemma typesize_Tptr: typesize Tptr = if Archi.ptr64 then 8 else 4.
Proof. unfold Tptr; destruct Archi.ptr64; auto. Qed.
All values of size 32 bits are also of type Tany32. All values
are of type Tany64. This corresponds to the following subtyping
relation over types.
Definition subtype (ty1 ty2: typ) : bool :=
match ty1, ty2 with
| Tint, Tint ⇒ true
| Tlong, Tlong ⇒ true
| Tfloat, Tfloat ⇒ true
| Tsingle, Tsingle ⇒ true
| (Tint | Tsingle | Tany32), Tany32 ⇒ true
| _, Tany64 ⇒ true
| _, _ ⇒ false
end.
Fixpoint subtype_list (tyl1 tyl2: list typ) : bool :=
match tyl1, tyl2 with
| nil, nil ⇒ true
| ty1::tys1, ty2::tys2 ⇒ subtype ty1 ty2 && subtype_list tys1 tys2
| _, _ ⇒ false
end.
Additionally, function definitions and function calls are annotated
by function signatures indicating:
These signatures are used in particular to determine appropriate
calling conventions for the function.
- the number and types of arguments;
- the type of the returned value, if any;
- additional information on which calling convention to use.
Record calling_convention : Type := mkcallconv {
cc_vararg: bool;
cc_unproto: bool;
cc_structret: bool
}.
Definition cc_default :=
{| cc_vararg := false; cc_unproto := false; cc_structret := false |}.
Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x≠y}.
Proof.
decide equality; apply bool_dec.
Defined.
Global Opaque calling_convention_eq.
Record signature : Type := mksignature {
sig_args: list typ;
sig_res: option typ;
sig_cc: calling_convention
}.
Definition proj_sig_res (s: signature) : typ :=
match s.(sig_res) with
| None ⇒ Tint
| Some t ⇒ t
end.
Definition signature_eq: ∀ (s1 s2: signature), {s1=s2} + {s1≠s2}.
Proof.
generalize opt_typ_eq, list_typ_eq, calling_convention_eq; decide equality.
Defined.
Global Opaque signature_eq.
Definition signature_main :=
{| sig_args := nil; sig_res := Some Tint; sig_cc := cc_default |}.
Memory accesses (load and store instructions) are annotated by
a ``memory chunk'' indicating the type, size and signedness of the
chunk of memory being accessed.
Inductive memory_chunk : Type :=
| Mint8signed
| Mint8unsigned
| Mint16signed
| Mint16unsigned
| Mint32
| Mint64
| Mfloat32
| Mfloat64
| Many32
| Many64.
Definition chunk_eq: ∀ (c1 c2: memory_chunk), {c1=c2} + {c1≠c2}.
Proof. decide equality. Defined.
Global Opaque chunk_eq.
Definition Mptr : memory_chunk := if Archi.ptr64 then Mint64 else Mint32.
The type (integer/pointer or float) of a chunk.
Definition type_of_chunk (c: memory_chunk) : typ :=
match c with
| Mint8signed ⇒ Tint
| Mint8unsigned ⇒ Tint
| Mint16signed ⇒ Tint
| Mint16unsigned ⇒ Tint
| Mint32 ⇒ Tint
| Mint64 ⇒ Tlong
| Mfloat32 ⇒ Tsingle
| Mfloat64 ⇒ Tfloat
| Many32 ⇒ Tany32
| Many64 ⇒ Tany64
end.
Lemma type_of_Mptr: type_of_chunk Mptr = Tptr.
Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed.
The chunk that is appropriate to store and reload a value of
the given type, without losing information.
Definition chunk_of_type (ty: typ) :=
match ty with
| Tint ⇒ Mint32
| Tfloat ⇒ Mfloat64
| Tlong ⇒ Mint64
| Tsingle ⇒ Mfloat32
| Tany32 ⇒ Many32
| Tany64 ⇒ Many64
end.
Lemma chunk_of_Tptr: chunk_of_type Tptr = Mptr.
Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed.
Initialization data for global variables.
Inductive init_data: Type :=
| Init_int8: int → init_data
| Init_int16: int → init_data
| Init_int32: int → init_data
| Init_int64: int64 → init_data
| Init_float32: float32 → init_data
| Init_float64: float → init_data
| Init_space: Z → init_data
| Init_addrof: ident → ptrofs → init_data.
Definition init_data_size (i: init_data) : Z :=
match i with
| Init_int8 _ ⇒ 1
| Init_int16 _ ⇒ 2
| Init_int32 _ ⇒ 4
| Init_int64 _ ⇒ 8
| Init_float32 _ ⇒ 4
| Init_float64 _ ⇒ 8
| Init_addrof _ _ ⇒ if Archi.ptr64 then 8 else 4
| Init_space n ⇒ Zmax n 0
end.
Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
match il with
| nil ⇒ 0
| i :: il' ⇒ init_data_size i + init_data_list_size il'
end.
Lemma init_data_size_pos:
∀ i, init_data_size i ≥ 0.
Proof.
destruct i; simpl; try xomega. destruct Archi.ptr64; omega.
Qed.
Lemma init_data_list_size_pos:
∀ il, init_data_list_size il ≥ 0.
Proof.
induction il; simpl. omega. generalize (init_data_size_pos a); omega.
Qed.
Information attached to global variables.
Record globvar (V: Type) : Type := mkglobvar {
gvar_info: V;
gvar_init: list init_data;
gvar_readonly: bool;
gvar_volatile: bool
}.
Whole programs consist of:
A global definition is either a global function or a global variable.
The type of function descriptions and that of additional information
for variables vary among the various intermediate languages and are
taken as parameters to the program type. The other parts of whole
programs are common to all languages.
- a collection of global definitions (name and description);
- a set of public names (the names that are visible outside this compilation unit);
- the name of the ``main'' function that serves as entry point in the program.
Inductive globdef (F V: Type) : Type :=
| Gfun (f: F)
| Gvar (v: globvar V).
Arguments Gfun [F V].
Arguments Gvar [F V].
Record program (F V: Type) : Type := mkprogram {
prog_defs: list (ident × option (globdef F V));
prog_public: list ident;
prog_main: ident
}.
Definition prog_defs_names (F V: Type) (p: program F V) : list ident :=
List.map fst p.(prog_defs).
The "definition map" of a program maps names of globals to their definitions.
If several definitions have the same name, the one appearing last in p.(prog_defs) wins.
Definition prog_defmap (F V: Type) (p: program F V) : PTree.t (globdef F V) :=
PTree_Properties.of_list_option p.(prog_defs).
Definition prog_option_defmap (F V: Type) (p: program F V) : PTree.t (option (globdef F V)) :=
PTree_Properties.of_list p.(prog_defs).
Section DEFMAP.
Variables F V: Type.
Variable p: program F V.
Lemma in_prog_defmap:
∀ id g, (prog_defmap p)!id = Some g → In (id, Some g) (prog_defs p).
Proof.
apply PTree_Properties.in_of_list_option.
Qed.
Lemma prog_defmap_unique:
∀ defs1 id g defs2,
prog_defs p = defs1 ++ (id, Some g) :: defs2 →
¬In id (map fst defs2) →
(prog_defmap p)!id = Some g.
Proof.
unfold prog_defmap; intros. rewrite H. apply PTree_Properties.of_list_option_unique; auto.
Qed.
Lemma prog_defmap_norepet:
∀ id g,
list_norepet (prog_defs_names p) →
In (id, Some g) (prog_defs p) →
(prog_defmap p)!id = Some g.
Proof.
apply PTree_Properties.of_list_option_norepet.
Qed.
End DEFMAP.
Section OPTION_DEFMAP.
Variables F V: Type.
Variable p: program F V.
Lemma in_prog_option_defmap:
∀ id g, (prog_option_defmap p)!id = Some g → In (id, g) (prog_defs p).
Proof.
apply PTree_Properties.in_of_list.
Qed.
Lemma prog_option_defmap_dom:
∀ id, In id (prog_defs_names p) → ∃ g, (prog_option_defmap p)!id = Some g.
Proof.
apply PTree_Properties.of_list_dom.
Qed.
Lemma prog_option_defmap_unique:
∀ defs1 id g defs2,
prog_defs p = defs1 ++ (id, g) :: defs2 →
¬In id (map fst defs2) →
(prog_option_defmap p)!id = Some g.
Proof.
unfold prog_option_defmap; intros. rewrite H. apply PTree_Properties.of_list_unique; auto.
Qed.
Lemma prog_option_defmap_norepet:
∀ id g,
list_norepet (prog_defs_names p) →
In (id, g) (prog_defs p) →
(prog_option_defmap p)!id = Some g.
Proof.
apply PTree_Properties.of_list_norepet.
Qed.
Lemma prog_defmap_option_defmap:
∀ id g,
(prog_option_defmap p) ! id = Some (Some g) ↔
(prog_defmap p)!id = Some g.
Proof.
apply PTree_Properties.of_list_option_of_list.
Qed.
End OPTION_DEFMAP.
Generic transformations over programs
Section TRANSF_PROGRAM.
Variable A B V: Type.
Variable transf: A → B.
Definition transform_program_globdef (idg: ident × option (globdef A V)) : ident × option (globdef B V) :=
match idg with
| (id, None) ⇒ (id, None)
| (id, Some (Gfun f)) ⇒ (id, Some (Gfun (transf f)))
| (id, Some (Gvar v)) ⇒ (id, Some (Gvar v))
end.
Definition transform_program (p: program A V) : program B V :=
mkprogram
(List.map transform_program_globdef p.(prog_defs))
p.(prog_public)
p.(prog_main).
End TRANSF_PROGRAM.
The following is a more general presentation of transform_program:
- Global variable information can be transformed, in addition to function definitions.
- The transformation functions can fail and return an error message.
- The transformation for function definitions receives a global context (derived from the compilation unit being transformed) as additiona argument.
- The transformation functions receive the name of the global as additional argument.
Local Open Scope error_monad_scope.
Section TRANSF_PROGRAM_GEN.
Variables A B V W: Type.
Variable transf_fun: ident → A → res B.
Variable transf_var: ident → V → res W.
Definition transf_globvar (i: ident) (g: globvar V) : res (globvar W) :=
do info' <- transf_var i g.(gvar_info);
OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)).
Fixpoint transf_globdefs (l: list (ident × option (globdef A V))) : res (list (ident × option (globdef B W))) :=
match l with
| nil ⇒ OK nil
| (id, None) :: l' ⇒
do tl' <- transf_globdefs l';
OK ((id, None) :: tl')
| (id, Some (Gfun f)) :: l' ⇒
match transf_fun id f with
| Error msg ⇒ Error (MSG "In function " :: CTX id :: MSG ": " :: msg)
| OK tf ⇒
do tl' <- transf_globdefs l'; OK ((id, Some (Gfun tf)) :: tl')
end
| (id, Some (Gvar v)) :: l' ⇒
match transf_globvar id v with
| Error msg ⇒ Error (MSG "In variable " :: CTX id :: MSG ": " :: msg)
| OK tv ⇒
do tl' <- transf_globdefs l'; OK ((id, Some (Gvar tv)) :: tl')
end
end.
Definition transform_partial_program2 (p: program A V) : res (program B W) :=
do gl' <- transf_globdefs p.(prog_defs);
OK (mkprogram gl' p.(prog_public) p.(prog_main)).
End TRANSF_PROGRAM_GEN.
The following is a special case of transform_partial_program2,
where only function definitions are transformed, but not variable definitions.
Section TRANSF_PARTIAL_PROGRAM.
Variable A B V: Type.
Variable transf_fun: A → res B.
Definition transform_partial_program (p: program A V) : res (program B V) :=
transform_partial_program2 (fun i f ⇒ transf_fun f) (fun i v ⇒ OK v) p.
End TRANSF_PARTIAL_PROGRAM.
Lemma transform_program_partial_program:
∀ (A B V: Type) (transf_fun: A → B) (p: program A V),
transform_partial_program (fun f ⇒ OK (transf_fun f)) p = OK (transform_program transf_fun p).
Proof.
intros. unfold transform_partial_program, transform_partial_program2.
assert (EQ: ∀ l,
transf_globdefs (fun i f ⇒ OK (transf_fun f)) (fun i (v: V) ⇒ OK v) l =
OK (List.map (transform_program_globdef transf_fun) l)).
{ induction l as [ | [id g] l]; simpl.
- auto.
- destruct g as [ [ | ] | ] ; simpl; rewrite IHl; simpl; auto. destruct v; auto.
}
rewrite EQ; simpl. auto.
Qed.
External functions
A system call or library function. Produces an event
in the trace.
A compiler built-in function. Behaves like an external, but
can be inlined by the compiler.
A function from the run-time library. Behaves like an
external, but must not be redefined.
A volatile read operation. If the adress given as first argument
points within a volatile global variable, generate an
event and return the value found in this event. Otherwise,
produce no event and behave like a regular memory load.
A volatile store operation. If the adress given as first argument
points within a volatile global variable, generate an event.
Otherwise, produce no event and behave like a regular memory store.
Dynamic memory allocation. Takes the requested size in bytes
as argument; returns a pointer to a fresh block of the given size.
Produces no observable event.
| EF_free
Dynamic memory deallocation. Takes a pointer to a block
allocated by an EF_malloc external call and frees the
corresponding block.
Produces no observable event.
A programmer-supplied annotation. Takes zero, one or several arguments,
produces an event carrying the text and the values of these arguments,
and returns no value.
Another form of annotation that takes one argument, produces
an event carrying the text and the value of this argument,
and returns the value of the argument.
Inline asm statements. Semantically, treated like an
annotation with no parameters (EF_annot text nil). To be
used with caution, as it can invalidate the semantic
preservation theorem. Generated only if -finline-asm is
given.
Transport debugging information from the front-end to the generated
assembly. Takes zero, one or several arguments like EF_annot.
Unlike EF_annot, produces no observable event.
The type signature of an external function.
Definition ef_sig (ef: external_function): signature :=
match ef with
| EF_external name sg ⇒ sg
| EF_builtin name sg ⇒ sg
| EF_runtime name sg ⇒ sg
| EF_vload chunk ⇒ mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default
| EF_vstore chunk ⇒ mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default
| EF_malloc ⇒ mksignature (Tptr :: nil) (Some Tptr) cc_default
| EF_free ⇒ mksignature (Tptr :: nil) None cc_default
| EF_memcpy sz al ⇒ mksignature (Tptr :: Tptr :: nil) None cc_default
| EF_annot text targs ⇒ mksignature targs None cc_default
| EF_annot_val text targ ⇒ mksignature (targ :: nil) (Some targ) cc_default
| EF_inline_asm text sg clob ⇒ sg
| EF_debug kind text targs ⇒ mksignature targs None cc_default
end.
Whether an external function should be inlined by the compiler.
Definition ef_inline (ef: external_function) : bool :=
match ef with
| EF_external name sg ⇒ false
| EF_builtin name sg ⇒ true
| EF_runtime name sg ⇒ false
| EF_vload chunk ⇒ true
| EF_vstore chunk ⇒ true
| EF_malloc ⇒ false
| EF_free ⇒ false
| EF_memcpy sz al ⇒ true
| EF_annot text targs ⇒ true
| EF_annot_val text targ ⇒ true
| EF_inline_asm text sg clob ⇒ true
| EF_debug kind text targs ⇒ true
end.
Whether an external function must reload its arguments.
Definition ef_reloads (ef: external_function) : bool :=
match ef with
| EF_annot text targs ⇒ false
| EF_debug kind text targs ⇒ false
| _ ⇒ true
end.
Equality between external functions. Used in module Allocation.
Definition external_function_eq: ∀ (ef1 ef2: external_function), {ef1=ef2} + {ef1≠ef2}.
Proof.
generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros.
decide equality.
Defined.
Global Opaque external_function_eq.
Function definitions are the union of internal and external functions.
Inductive fundef (F: Type): Type :=
| Internal: F → fundef F
| External: external_function → fundef F.
Arguments External [F].
Section TRANSF_FUNDEF.
Variable A B: Type.
Variable transf: A → B.
Definition transf_fundef (fd: fundef A): fundef B :=
match fd with
| Internal f ⇒ Internal (transf f)
| External ef ⇒ External ef
end.
End TRANSF_FUNDEF.
Section TRANSF_PARTIAL_FUNDEF.
Variable A B: Type.
Variable transf_partial: A → res B.
Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
match fd with
| Internal f ⇒ do f' <- transf_partial f; OK (Internal f')
| External ef ⇒ OK (External ef)
end.
End TRANSF_PARTIAL_FUNDEF.
Set Contextual Implicit.
In some intermediate languages (LTL, Mach), 64-bit integers can be
split into two 32-bit halves and held in a pair of registers.
Syntactically, this is captured by the type rpair below.
Inductive rpair (A: Type) : Type :=
| One (r: A)
| Twolong (rhi rlo: A).
Definition typ_rpair (A: Type) (typ_of: A → typ) (p: rpair A): typ :=
match p with
| One r ⇒ typ_of r
| Twolong rhi rlo ⇒ Tlong
end.
Definition map_rpair (A B: Type) (f: A → B) (p: rpair A): rpair B :=
match p with
| One r ⇒ One (f r)
| Twolong rhi rlo ⇒ Twolong (f rhi) (f rlo)
end.
Definition regs_of_rpair (A: Type) (p: rpair A): list A :=
match p with
| One r ⇒ r :: nil
| Twolong rhi rlo ⇒ rhi :: rlo :: nil
end.
Fixpoint regs_of_rpairs (A: Type) (l: list (rpair A)): list A :=
match l with
| nil ⇒ nil
| p :: l ⇒ regs_of_rpair p ++ regs_of_rpairs l
end.
Lemma in_regs_of_rpairs:
∀ (A: Type) (x: A) p, In x (regs_of_rpair p) → ∀ l, In p l → In x (regs_of_rpairs l).
Proof.
induction l; simpl; intros. auto. apply in_app. destruct H0; auto. subst a. auto.
Qed.
Lemma in_regs_of_rpairs_inv:
∀ (A: Type) (x: A) l, In x (regs_of_rpairs l) → ∃ p, In p l ∧ In x (regs_of_rpair p).
Proof.
induction l; simpl; intros. contradiction.
rewrite in_app_iff in H; destruct H.
∃ a; auto.
apply IHl in H. firstorder auto.
Qed.
Definition forall_rpair (A: Type) (P: A → Prop) (p: rpair A): Prop :=
match p with
| One r ⇒ P r
| Twolong rhi rlo ⇒ P rhi ∧ P rlo
end.
Inductive builtin_arg (A: Type) : Type :=
| BA (x: A)
| BA_int (n: int)
| BA_long (n: int64)
| BA_float (f: float)
| BA_single (f: float32)
| BA_loadstack (chunk: memory_chunk) (ofs: ptrofs)
| BA_addrstack (ofs: ptrofs)
| BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: ptrofs)
| BA_addrglobal (id: ident) (ofs: ptrofs)
| BA_splitlong (hi lo: builtin_arg A).
Inductive builtin_res (A: Type) : Type :=
| BR (x: A)
| BR_none
| BR_splitlong (hi lo: builtin_res A).
Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident :=
match a with
| BA_loadglobal chunk id ofs ⇒ id :: nil
| BA_addrglobal id ofs ⇒ id :: nil
| BA_splitlong hi lo ⇒ globals_of_builtin_arg hi ++ globals_of_builtin_arg lo
| _ ⇒ nil
end.
Definition globals_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list ident :=
List.fold_right (fun a l ⇒ globals_of_builtin_arg a ++ l) nil al.
Fixpoint params_of_builtin_arg (A: Type) (a: builtin_arg A) : list A :=
match a with
| BA x ⇒ x :: nil
| BA_splitlong hi lo ⇒ params_of_builtin_arg hi ++ params_of_builtin_arg lo
| _ ⇒ nil
end.
Definition params_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list A :=
List.fold_right (fun a l ⇒ params_of_builtin_arg a ++ l) nil al.
Fixpoint params_of_builtin_res (A: Type) (a: builtin_res A) : list A :=
match a with
| BR x ⇒ x :: nil
| BR_none ⇒ nil
| BR_splitlong hi lo ⇒ params_of_builtin_res hi ++ params_of_builtin_res lo
end.
Fixpoint map_builtin_arg (A B: Type) (f: A → B) (a: builtin_arg A) : builtin_arg B :=
match a with
| BA x ⇒ BA (f x)
| BA_int n ⇒ BA_int n
| BA_long n ⇒ BA_long n
| BA_float n ⇒ BA_float n
| BA_single n ⇒ BA_single n
| BA_loadstack chunk ofs ⇒ BA_loadstack chunk ofs
| BA_addrstack ofs ⇒ BA_addrstack ofs
| BA_loadglobal chunk id ofs ⇒ BA_loadglobal chunk id ofs
| BA_addrglobal id ofs ⇒ BA_addrglobal id ofs
| BA_splitlong hi lo ⇒
BA_splitlong (map_builtin_arg f hi) (map_builtin_arg f lo)
end.
Fixpoint map_builtin_res (A B: Type) (f: A → B) (a: builtin_res A) : builtin_res B :=
match a with
| BR x ⇒ BR (f x)
| BR_none ⇒ BR_none
| BR_splitlong hi lo ⇒
BR_splitlong (map_builtin_res f hi) (map_builtin_res f lo)
end.
Which kinds of builtin arguments are supported by which external function.
Inductive builtin_arg_constraint : Type :=
| OK_default
| OK_const
| OK_addrstack
| OK_addrglobal
| OK_addrany
| OK_all.
Definition builtin_arg_ok
(A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
match ba, c with
| (BA _ | BA_splitlong (BA _) (BA _)), _ ⇒ true
| (BA_int _ | BA_long _ | BA_float _ | BA_single _), OK_const ⇒ true
| BA_addrstack _, (OK_addrstack | OK_addrany) ⇒ true
| BA_addrglobal _ _, (OK_addrglobal | OK_addrany) ⇒ true
| _, OK_all ⇒ true
| _, _ ⇒ false
end.