blob: 202a8b795e0a8478b6acd31bc661478019fd3a3f (
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
74
75
76
77
78
79
|
From coqup.common Require Import Coquplib.
From compcert Require Import Maps.
From compcert Require Op AST Memory Registers.
Definition node := positive.
Definition reg := Registers.reg.
Definition ident := AST.ident.
Inductive instruction : Type :=
| Hnop : node -> instruction
| Hnonblock : Op.operation -> list reg -> reg -> node -> instruction
(** [Hnonblock op args res next] Defines a nonblocking assignment to a
register, using the operation defined in Op.v. *)
| Hload : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
| Hstore : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
| Hinst : AST.signature -> ident -> reg -> node -> instruction
(** [Hinst sig fun args rst strt end res next] Defines the start of a
module instantiation, meaning the function will run until the result is
returned. *)
| Htailcall : AST.signature -> ident -> list reg -> instruction
| Hcond : Op.condition -> list reg -> node -> node -> instruction
| Hjumptable : reg -> list node -> instruction
| Hfinish : option reg -> instruction.
Record inst : Type :=
mkinst {
inst_moddecl : ident;
inst_args : list reg
}.
Definition code : Type := PTree.t instruction.
Definition instances : Type := PTree.t inst.
Definition empty_instances : instances := PTree.empty 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 : instances;
mod_entrypoint : node
}.
Definition moddecl := AST.fundef module.
Definition design := AST.program moddecl unit.
Definition modsig (md : moddecl) :=
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 (m : module) : module :=
mkmodule
m.(mod_sig)
m.(mod_params)
m.(mod_stacksize)
(PTree.map transf m.(mod_code))
m.(mod_insts)
m.(mod_entrypoint).
End TRANSF.
|
