blob: 1fc69320e340771c44e300d200b2b97640388fca (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
From coqup.common Require Import Coquplib.
From compcert Require Op Maps.
From compcert Require AST Memory Registers.
Definition node := positive.
Definition reg := Registers.reg.
Definition ident := AST.ident.
Inductive instruction : Type :=
| Vnop : node -> instruction
| Vnonblock : Op.operation -> list reg -> reg -> node -> instruction
| Vload : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
| Vstore : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
| Vinst : AST.signature -> ident -> list reg -> reg -> node -> instruction
| Vtailinst : AST.signature -> ident -> list reg -> instruction
| Vcond : Op.condition -> list reg -> node -> node -> instruction
| Vjumptable : reg -> list node -> instruction
| Vfinish : option reg -> instruction.
Record inst : Type :=
mkinst {
inst_start : reg;
inst_finish : reg;
inst_result : reg;
inst_args : list reg
}.
Definition code : Type := Maps.PTree.t instruction.
Definition instantiations : Type := Maps.PTree.t inst.
(** Function declaration for VTL also contain a construction which describes the
functions that are called in the current function. This information is used
to print out *)
Record module : Type :=
mkmodule {
mod_sig : AST.signature;
mod_params : list reg;
mod_stacksize : Z;
mod_code : code;
mod_insts : inst;
mod_entrypoint : node
}.
Definition moddef := AST.fundef module.
Definition design := AST.program moddef unit.
Definition modsig (md : moddef) :=
match md with
| AST.Internal m => mod_sig m
| AST.External ef => AST.ef_sig ef
end.
(** Describes the transformation of VTL instruction by instruction. This applies
the transformation to each instruction in the function and returns the new
function with the modified instructions. *)
Section TRANSF.
Variable transf : node -> instruction -> instruction.
Definition transf_function (f : function) : function :=
mkfunction
f.(fn_sig)
f.(fn_params)
f.(fn_stacksize)
(Maps.PTree.map transf f.(fn_code))
f.(fn_entrypoint).
End TRANSF.
|
