blob: cb755e55651fc473b2f3ba19472d6e7d84bb0d87 (
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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
(*
* Vericert: Verified high-level synthesis.
* Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
From compcert Require Import Coqlib Maps.
From compcert Require Import AST Integers Values Events Memory Globalenvs Smallstep.
From compcert Require Import Op Registers.
Definition node := positive.
Inductive instruction : Type :=
| RPnop : instruction
| RPop : operation -> list reg -> reg -> instruction
| RPload : memory_chunk -> addressing -> list reg -> reg -> instruction
| RPstore : memory_chunk -> addressing -> list reg -> reg -> instruction.
Definition bblock_body : Type := list (list instruction).
Inductive control_flow_inst : Type :=
| RPcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst
| RPtailcall : signature -> reg + ident -> list reg -> control_flow_inst
| RPbuiltin : external_function -> list (builtin_arg reg) ->
builtin_res reg -> node -> control_flow_inst
| RPcond : condition -> list reg -> node -> node -> control_flow_inst
| RPjumptable : reg -> list node -> control_flow_inst
| RPreturn : option reg -> control_flow_inst
| RPgoto : node -> control_flow_inst.
Record bblock : Type := mk_bblock {
bb_body: bblock_body;
bb_exit: option control_flow_inst
}.
Definition code : Type := PTree.t bblock.
Record function: Type := mkfunction {
fn_sig: signature;
fn_params: list reg;
fn_stacksize: Z;
fn_code: code;
fn_entrypoint: node
}.
Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.
Definition funsig (fd: fundef) :=
match fd with
| Internal f => fn_sig f
| External ef => ef_sig ef
end.
Definition successors_instr (i : control_flow_inst) : list node :=
match i with
| RPcall sig ros args res s => s :: nil
| RPtailcall sig ros args => nil
| RPbuiltin ef args res s => s :: nil
| RPcond cond args ifso ifnot => ifso :: ifnot :: nil
| RPjumptable arg tbl => tbl
| RPreturn optarg => nil
| RPgoto n => n :: nil
end.
Definition max_reg_instr (m: positive) (i: instruction) :=
match i with
| RPnop => m
| RPop op args res => fold_left Pos.max args (Pos.max res m)
| RPload chunk addr args dst => fold_left Pos.max args (Pos.max dst m)
| RPstore chunk addr args src => fold_left Pos.max args (Pos.max src m)
end.
Definition max_reg_cfi (m : positive) (i : control_flow_inst) :=
match i with
| RPcall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m))
| RPcall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m)
| RPtailcall sig (inl r) args => fold_left Pos.max args (Pos.max r m)
| RPtailcall sig (inr id) args => fold_left Pos.max args m
| RPbuiltin ef args res s =>
fold_left Pos.max (params_of_builtin_args args)
(fold_left Pos.max (params_of_builtin_res res) m)
| RPcond cond args ifso ifnot => fold_left Pos.max args m
| RPjumptable arg tbl => Pos.max arg m
| RPreturn None => m
| RPreturn (Some arg) => Pos.max arg m
| RPgoto n => m
end.
Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) :=
let max_body := fold_left (fun x l => fold_left max_reg_instr l x) bb.(bb_body) m in
match bb.(bb_exit) with
| Some e => max_reg_cfi max_body e
| None => max_body
end.
Definition max_reg_function (f: function) :=
Pos.max
(PTree.fold max_reg_bblock f.(fn_code) 1%positive)
(fold_left Pos.max f.(fn_params) 1%positive).
Definition max_pc_function (f: function) : positive :=
PTree.fold (fun m pc i => (Pos.max m
(pc + match Zlength i.(bb_body)
with Z.pos p => p | _ => 1 end))%positive)
f.(fn_code) 1%positive.
(*Inductive state : Type :=
| State:
forall (stack: list stackframe) (**r call stack *)
(f: function) (**r current function *)
(sp: val) (**r stack pointer *)
(pc: node) (**r current program point in [c] *)
(rs: regset) (**r register state *)
(m: mem), (**r memory state *)
state
| Callstate:
forall (stack: list stackframe) (**r call stack *)
(f: fundef) (**r function to call *)
(args: list val) (**r arguments to the call *)
(m: mem), (**r memory state *)
state
| Returnstate:
forall (stack: list stackframe) (**r call stack *)
(v: val) (**r return value for the call *)
(m: mem), (**r memory state *)
state.
*)
|
