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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
|
open InterpreterStatements
open Interpreter
module L = Logging
module T = Types
module A = CfimAst
module M = Modules
module SA = SymbolicAst
(** The local logger *)
let log = L.translate_log
type trans_ctx = { type_context : C.type_context; fun_context : C.fun_context }
let type_def_to_string (ctx : trans_ctx) (def : Pure.type_def) : string =
let type_params = def.type_params in
let type_defs = ctx.type_context.type_defs in
let fmt = PrintPure.mk_type_formatter type_defs type_params in
PrintPure.type_def_to_string fmt def
let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
let type_params = sg.type_params in
let type_defs = ctx.type_context.type_defs in
let fun_defs = ctx.fun_context.fun_defs in
let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
PrintPure.fun_sig_to_string fmt sg
let fun_def_to_string (ctx : trans_ctx) (def : Pure.fun_def) : string =
let type_params = def.signature.type_params in
let type_defs = ctx.type_context.type_defs in
let fun_defs = ctx.fun_context.fun_defs in
let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
PrintPure.fun_def_to_string fmt def
type symbolic_fun_translation = V.symbolic_value list * SA.expression
(** The result of running the symbolic interpreter on a function:
- the list of symbolic values used for the input values
- the generated symbolic AST
*)
type pure_fun_translation = Pure.fun_def * Pure.fun_def list
(** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs,
for the forward function and the backward functions.
*)
let translate_function_to_symbolics (config : C.partial_config)
(type_context : C.type_context) (fun_context : C.fun_context)
(fdef : A.fun_def) :
symbolic_fun_translation * symbolic_fun_translation list =
(* Debug *)
log#ldebug
(lazy
("translate_function_to_symbolics: " ^ Print.name_to_string fdef.A.name));
(* Evaluate *)
let synthesize = true in
let evaluate gid =
let inputs, symb =
evaluate_function_symbolic config synthesize type_context fun_context fdef
gid
in
(inputs, Option.get symb)
in
(* Execute the forward function *)
let forward = evaluate None in
(* Execute the backward functions *)
let backwards =
T.RegionGroupId.mapi
(fun gid _ -> evaluate (Some gid))
fdef.signature.regions_hierarchy
in
(* Return *)
(forward, backwards)
(** Translate a function, by generating its forward and backward translations. *)
let translate_function_to_pure (config : C.partial_config)
(type_context : C.type_context) (fun_context : C.fun_context)
(fun_sigs : Pure.fun_sig SymbolicToPure.RegularFunIdMap.t)
(fdef : A.fun_def) : pure_fun_translation =
(* Debug *)
log#ldebug
(lazy ("translate_function_to_pure: " ^ Print.name_to_string fdef.A.name));
let def_id = fdef.def_id in
(* Compute the symbolic ASTs *)
let symbolic_forward, symbolic_backwards =
translate_function_to_symbolics config type_context fun_context fdef
in
(* Convert the symbolic ASTs to pure ASTs: *)
(* Initialize the context *)
let sv_to_var = V.SymbolicValueId.Map.empty in
let var_counter = Pure.VarId.generator_zero in
let calls = V.FunCallId.Map.empty in
let abstractions = V.AbstractionId.Map.empty in
let type_context =
{
SymbolicToPure.types_infos = type_context.type_infos;
cfim_type_defs = type_context.type_defs;
}
in
let fun_context =
{ SymbolicToPure.cfim_fun_defs = fun_context.fun_defs; fun_sigs }
in
let ctx =
{
SymbolicToPure.bid = None;
(* Dummy for now *)
sv_to_var;
var_counter;
type_context;
fun_context;
fun_def = fdef;
forward_inputs = [];
(* Empty for now *)
backward_inputs = T.RegionGroupId.Map.empty;
(* Empty for now *)
backward_outputs = T.RegionGroupId.Map.empty;
(* Empty for now *)
calls;
abstractions;
}
in
(* We need to initialize the input/output variables *)
let module RegularFunIdMap = SymbolicToPure.RegularFunIdMap in
let forward_sg = RegularFunIdMap.find (A.Local def_id, None) fun_sigs in
let add_forward_inputs input_svs ctx =
let ctx, forward_inputs =
SymbolicToPure.fresh_vars_for_symbolic_values input_svs ctx
in
{ ctx with forward_inputs }
in
let ctx, forward_inputs = SymbolicToPure.fresh_vars forward_sg.inputs ctx in
let ctx = { ctx with forward_inputs } in
(* Translate the forward function *)
let pure_forward =
SymbolicToPure.translate_fun_def
(add_forward_inputs (fst symbolic_forward) ctx)
(snd symbolic_forward)
in
(* Translate the backward functions *)
let translate_backward (rg : T.region_var_group) : Pure.fun_def =
(* For the backward inputs/outputs initialization: we use the fact that
* there are no nested borrows for now, and so that the region groups
* can't have parents *)
assert (rg.parents = []);
let back_id = rg.id in
let input_svs, symbolic = T.RegionGroupId.nth symbolic_backwards back_id in
let ctx = add_forward_inputs input_svs ctx in
(* TODO: the computation of the backward inputs is a bit awckward... *)
let backward_sg =
RegularFunIdMap.find (A.Local def_id, Some back_id) fun_sigs
in
let _, backward_inputs =
Collections.List.split_at backward_sg.inputs (List.length forward_inputs)
in
let ctx, backward_inputs = SymbolicToPure.fresh_vars backward_inputs ctx in
let backward_outputs = backward_sg.outputs in
let ctx, backward_outputs =
SymbolicToPure.fresh_vars backward_outputs ctx
in
let backward_inputs =
T.RegionGroupId.Map.singleton back_id backward_inputs
in
let backward_outputs =
T.RegionGroupId.Map.singleton back_id backward_outputs
in
(* Put everything in the context *)
let ctx =
{ ctx with bid = Some back_id; backward_inputs; backward_outputs }
in
(* Translate *)
SymbolicToPure.translate_fun_def ctx symbolic
in
let pure_backwards =
List.map translate_backward fdef.signature.regions_hierarchy
in
(* Return *)
(pure_forward, pure_backwards)
let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
Pure.type_def T.TypeDefId.Map.t * pure_fun_translation A.FunDefId.Map.t =
(* Debug *)
log#ldebug (lazy "translate_module_to_pure");
(* Compute the type and function contexts *)
let type_context, fun_context = compute_type_fun_contexts m in
(* Translate all the type definitions *)
let type_defs = SymbolicToPure.translate_type_defs m.types in
(* Translate all the function *signatures* *)
let assumed_sigs =
List.map (fun (id, sg) -> (A.Assumed id, sg)) Assumed.assumed_sigs
in
let local_sigs =
List.map
(fun (fdef : A.fun_def) -> (A.Local fdef.def_id, fdef.signature))
m.functions
in
let sigs = List.append assumed_sigs local_sigs in
let fun_sigs =
SymbolicToPure.translate_fun_signatures type_context.type_infos sigs
in
(* Translate all the functions *)
let pure_translations =
List.map
(fun (fdef : A.fun_def) ->
( fdef.def_id,
translate_function_to_pure config type_context fun_context fun_sigs
fdef ))
m.functions
in
(* Put the translated functions in a map *)
let fun_defs =
List.fold_left
(fun m (def_id, trans) -> A.FunDefId.Map.add def_id trans m)
A.FunDefId.Map.empty pure_translations
in
(* Return *)
(type_defs, fun_defs)
|
