Require Import String.
Require Import Coqlib Maps Errors Integers Floats.
Require Archi.
Set Implicit Arguments.
Identifiers (names of local variables, of global symbols and functions,
etc) are represented by the type positive of positive integers.
Definition ident :=
positive.
Definition ident_eq :=
peq.
Additionally, function definitions and function calls are annotated
by function signatures indicating:
-
the number and types of arguments;
-
the type of the returned value, if any;
-
additional information on which calling convention to use.
These signatures are used in particular to determine appropriate
calling conventions for the function.
:
Type :=
mkcallconv {
cc_vararg:
bool;
(* variable-arity function *)
cc_unproto:
bool;
(* old-style unprototyped function *)
cc_structret:
bool (* function returning a struct *)
}.
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.
The intermediate languages are weakly typed, using the following types:
Inductive typ :
Type :=
|
Tint (* 32-bit integers or pointers *)
|
Tfloat (* 64-bit double-precision floats *)
|
Tlong (* 64-bit integers *)
|
Tsingle (* 32-bit single-precision floats *)
|
Tany32 (* any 32-bit value *)
|
Tany64.
(* any 64-bit value, i.e. any value *)
Record signature :
Type :=
mksignature {
sig_args:
list typ;
sig_res:
option typ;
sig_cc:
calling_convention
}.
Inductive memory_chunk :
Type :=
|
Mint8signed (* 8-bit signed integer *)
|
Mint8unsigned (* 8-bit unsigned integer *)
|
Mint16signed (* 16-bit signed integer *)
|
Mint16unsigned (* 16-bit unsigned integer *)
|
Mint32 (* 32-bit integer, or pointer *)
|
Mint64 (* 64-bit integer *)
|
Mfloat32 (* 32-bit single-precision float *)
|
Mfloat64 (* 64-bit double-precision float *)
|
Many32 (* any value that fits in 32 bits *)
|
Many64.
(* any value *)
For most languages, the functions composing the program are either
internal functions, defined within the language, or external functions,
defined outside. External functions include system calls but also
compiler built-in functions. We define a type for external functions
and associated operations.
Inductive external_function :
Type :=
|
EF_external (
name:
string) (
sg:
signature)
A system call or library function. Produces an event
in the trace.
|
EF_builtin (
name:
string) (
sg:
signature)
A compiler built-in function. Behaves like an external, but
can be inlined by the compiler.
|
EF_runtime (
name:
string) (
sg:
signature)
A function from the run-time library. Behaves like an
external, but must not be redefined.
|
EF_vload (
chunk:
memory_chunk)
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.
|
EF_vstore (
chunk:
memory_chunk)
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.
|
EF_malloc
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.
|
EF_memcpy (
sz:
Z) (
al:
Z)
Block copy, of sz bytes, between addresses that are al-aligned.
|
EF_annot (
kind:
positive) (
text:
string) (
targs:
list typ)
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.
|
EF_annot_val (
kind:
positive) (
text:
string) (
targ:
typ)
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.
|
EF_inline_asm (
text:
string) (
sg:
signature) (
clobbers:
list string)
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.
|
EF_debug (
kind:
positive) (
text:
ident) (
targs:
list typ).
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.
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].