|
1
|
(********************************************************************)
|
|
2
|
(* *)
|
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
|
|
5
|
(* *)
|
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
|
8
|
(* version 2.1. *)
|
|
9
|
(* *)
|
|
10
|
(********************************************************************)
|
|
11
|
|
|
12
|
open Utils.Format
|
|
13
|
open Lustre_types
|
|
14
|
open Machine_code_types
|
|
15
|
open C_backend_common
|
|
16
|
open Machine_code_common
|
|
17
|
open Corelang
|
|
18
|
|
|
19
|
(**************************************************************************)
|
|
20
|
(* Printing spec for c *)
|
|
21
|
|
|
22
|
(**************************************************************************)
|
|
23
|
(* OLD STUFF ???
|
|
24
|
|
|
25
|
|
|
26
|
let pp_acsl_type var fmt t =
|
|
27
|
let rec aux t pp_suffix =
|
|
28
|
match (Types.repr t).Types.tdesc with
|
|
29
|
| Types.Tclock t' -> aux t' pp_suffix
|
|
30
|
| Types.Tbool -> fprintf fmt "int %s%a" var pp_suffix ()
|
|
31
|
| Types.Treal -> fprintf fmt "real %s%a" var pp_suffix ()
|
|
32
|
| Types.Tint -> fprintf fmt "int %s%a" var pp_suffix ()
|
|
33
|
| Types.Tarray (d, t') ->
|
|
34
|
let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
|
|
35
|
aux t' pp_suffix'
|
|
36
|
(* | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix *)
|
|
37
|
(* | Types.Tconst ty -> fprintf fmt "%s %s" ty var *)
|
|
38
|
(* | Types.Tarrow (_, _) -> fprintf fmt "void (\*%s)()" var *)
|
|
39
|
| _ -> eprintf "internal error: pp_acsl_type %a@." Types.print_ty t; assert false
|
|
40
|
in aux t (fun fmt () -> ())
|
|
41
|
|
|
42
|
let pp_acsl_var_decl fmt id =
|
|
43
|
pp_acsl_type id.var_id fmt id.var_type
|
|
44
|
|
|
45
|
|
|
46
|
let rec pp_eexpr is_output fmt eexpr =
|
|
47
|
let pp_eexpr = pp_eexpr is_output in
|
|
48
|
match eexpr.eexpr_desc with
|
|
49
|
| EExpr_const c -> Printers.pp_econst fmt c
|
|
50
|
| EExpr_ident id ->
|
|
51
|
if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
|
|
52
|
| EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el
|
|
53
|
| EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
|
|
54
|
| EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
|
|
55
|
(* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
|
|
56
|
(* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
|
|
57
|
| EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
|
|
58
|
| EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
|
|
59
|
| EExpr_merge (id, e1, e2) ->
|
|
60
|
fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
|
|
61
|
| EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r
|
|
62
|
| EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e
|
|
63
|
| EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e
|
|
64
|
|
|
65
|
|
|
66
|
(* | EExpr_whennot _ *)
|
|
67
|
(* | EExpr_uclock _ *)
|
|
68
|
(* | EExpr_dclock _ *)
|
|
69
|
(* | EExpr_phclock _ -> assert false *)
|
|
70
|
and pp_eapp is_output fmt id e r =
|
|
71
|
let pp_eexpr = pp_eexpr is_output in
|
|
72
|
match r with
|
|
73
|
| None ->
|
|
74
|
(match id, e.eexpr_desc with
|
|
75
|
| "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
|
|
76
|
| "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
|
|
77
|
| "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
|
|
78
|
| "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
|
|
79
|
| "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
|
|
80
|
| "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
|
|
81
|
| "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
|
|
82
|
| "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
|
|
83
|
| "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
|
|
84
|
| "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
|
|
85
|
| "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
|
|
86
|
| "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
|
|
87
|
| ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
|
|
88
|
| ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
|
|
89
|
| "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
|
|
90
|
| "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
|
|
91
|
| "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
|
|
92
|
| "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
|
|
93
|
| _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
|
|
94
|
| Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x
|
|
95
|
|
|
96
|
let pp_ensures is_output fmt e =
|
|
97
|
match e with
|
|
98
|
| EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e
|
|
99
|
| SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args
|
|
100
|
|
|
101
|
let pp_acsl_spec outputs fmt spec =
|
|
102
|
let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
|
|
103
|
let pp_eexpr = pp_eexpr is_output in
|
|
104
|
fprintf fmt "@[<v 2>/*@@ ";
|
|
105
|
Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
|
|
106
|
Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;
|
|
107
|
fprintf fmt "@ ";
|
|
108
|
(* fprintf fmt "assigns *self%t%a;@ " *)
|
|
109
|
(* (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
|
|
110
|
(* (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
|
|
111
|
Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) ->
|
|
112
|
fprintf fmt "behavior %s:@[@ %a@ %a@]"
|
|
113
|
name
|
|
114
|
(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
|
|
115
|
(Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires
|
|
116
|
) fmt spec.behaviors;
|
|
117
|
fprintf fmt "@]@ */@.";
|
|
118
|
()
|
|
119
|
|
|
120
|
|
|
121
|
|
|
122
|
|
|
123
|
let print_machine_decl_prefix fmt m =
|
|
124
|
(* Print specification if any *)
|
|
125
|
(match m.mspec with
|
|
126
|
| None -> ()
|
|
127
|
| Some spec ->
|
|
128
|
pp_acsl_spec m.mstep.step_outputs fmt spec
|
|
129
|
)
|
|
130
|
|
|
131
|
*)
|
|
132
|
|
|
133
|
(* TODO ACSL
|
|
134
|
Return updates machines (eg with local annotations) and acsl preamble *)
|
|
135
|
let preprocess_acsl machines = machines, []
|
|
136
|
|
|
137
|
(* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *)
|
|
138
|
let pp_acsl_preamble fmt _preamble =
|
|
139
|
Format.fprintf fmt "";
|
|
140
|
()
|
|
141
|
|
|
142
|
let pp_acsl_basic_type_desc t_desc =
|
|
143
|
if Types.is_bool_type t_desc then
|
|
144
|
(* if !Options.cpp then "bool" else "_Bool" *)
|
|
145
|
"integer"
|
|
146
|
else if Types.is_int_type t_desc then
|
|
147
|
(* !Options.int_type *)
|
|
148
|
"integer"
|
|
149
|
else if Types.is_real_type t_desc then
|
|
150
|
if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
|
|
151
|
else
|
|
152
|
assert false (* Not a basic C type. Do not handle arrays or pointers *)
|
|
153
|
|
|
154
|
module VarDecl = struct
|
|
155
|
type t = var_decl
|
|
156
|
let compare v1 v2 = compare v1.var_id v2.var_id
|
|
157
|
end
|
|
158
|
module VDSet = Set.Make(VarDecl)
|
|
159
|
|
|
160
|
module Live = Map.Make(Int)
|
|
161
|
|
|
162
|
let pp_spec pp fmt =
|
|
163
|
fprintf fmt "@[<v>/*%@@[<v>@,%a@]@,*/@]" pp
|
|
164
|
|
|
165
|
let pp_spec_cut pp fmt =
|
|
166
|
fprintf fmt "%a@," (pp_spec pp)
|
|
167
|
|
|
168
|
let pp_spec_line pp fmt =
|
|
169
|
fprintf fmt "//%@ %a@," pp
|
|
170
|
|
|
171
|
let pp_requires pp_req fmt =
|
|
172
|
fprintf fmt "requires %a;" pp_req
|
|
173
|
|
|
174
|
let pp_ensures pp_ens fmt =
|
|
175
|
fprintf fmt "ensures %a;" pp_ens
|
|
176
|
|
|
177
|
let pp_assigns pp_asg fmt =
|
|
178
|
fprintf fmt "assigns %a;" pp_asg
|
|
179
|
|
|
180
|
let pp_ghost pp_gho fmt =
|
|
181
|
fprintf fmt "ghost %a" pp_gho
|
|
182
|
|
|
183
|
let pp_assert pp_ast fmt =
|
|
184
|
fprintf fmt "assert %a;" pp_ast
|
|
185
|
|
|
186
|
let pp_mem_valid pp_var fmt (name, var) =
|
|
187
|
fprintf fmt "%s_valid(%a)" name pp_var var
|
|
188
|
|
|
189
|
let pp_mem_valid' = pp_mem_valid pp_print_string
|
|
190
|
|
|
191
|
let pp_indirect pp_field fmt (ptr, field) =
|
|
192
|
fprintf fmt "%s->%a" ptr pp_field field
|
|
193
|
|
|
194
|
let pp_indirect' = pp_indirect pp_print_string
|
|
195
|
|
|
196
|
let pp_access pp_field fmt (stru, field) =
|
|
197
|
fprintf fmt "%s.%a" stru pp_field field
|
|
198
|
|
|
199
|
let pp_access' = pp_access pp_print_string
|
|
200
|
|
|
201
|
let pp_inst self fmt (name, _) =
|
|
202
|
pp_indirect' fmt (self, name)
|
|
203
|
|
|
204
|
let pp_true fmt () =
|
|
205
|
pp_print_string fmt "\\true"
|
|
206
|
|
|
207
|
let pp_separated self fmt =
|
|
208
|
fprintf fmt "\\separated(@[<h>%s%a@])"
|
|
209
|
self
|
|
210
|
(pp_print_list
|
|
211
|
~pp_prologue:pp_print_comma
|
|
212
|
~pp_sep:pp_print_comma
|
|
213
|
(pp_inst self))
|
|
214
|
|
|
215
|
let pp_forall pp_l pp_r fmt (l, r) =
|
|
216
|
fprintf fmt "@[<v 2>\\forall %a;@,%a@]"
|
|
217
|
pp_l l
|
|
218
|
pp_r r
|
|
219
|
|
|
220
|
let pp_exists pp_l pp_r fmt (l, r) =
|
|
221
|
fprintf fmt "@[<v 2>\\exists %a;@,%a@]"
|
|
222
|
pp_l l
|
|
223
|
pp_r r
|
|
224
|
|
|
225
|
let pp_valid =
|
|
226
|
pp_print_braced
|
|
227
|
~pp_nil:pp_true
|
|
228
|
~pp_prologue:(fun fmt () -> pp_print_string fmt "\\valid(")
|
|
229
|
~pp_epilogue:pp_print_cpar
|
|
230
|
|
|
231
|
let pp_equal pp_l pp_r fmt (l, r) =
|
|
232
|
fprintf fmt "%a == %a"
|
|
233
|
pp_l l
|
|
234
|
pp_r r
|
|
235
|
|
|
236
|
let pp_different pp_l pp_r fmt (l, r) =
|
|
237
|
fprintf fmt "%a != %a"
|
|
238
|
pp_l l
|
|
239
|
pp_r r
|
|
240
|
|
|
241
|
let pp_implies pp_l pp_r fmt (l, r) =
|
|
242
|
fprintf fmt "@[<v>%a ==>@ %a@]"
|
|
243
|
pp_l l
|
|
244
|
pp_r r
|
|
245
|
|
|
246
|
let pp_and pp_l pp_r fmt (l, r) =
|
|
247
|
fprintf fmt "@[<v>%a @ && %a@]"
|
|
248
|
pp_l l
|
|
249
|
pp_r r
|
|
250
|
|
|
251
|
let pp_and_l pp_v fmt =
|
|
252
|
pp_print_list
|
|
253
|
~pp_open_box:pp_open_vbox0
|
|
254
|
~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
|
|
255
|
pp_v
|
|
256
|
fmt
|
|
257
|
|
|
258
|
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
|
|
259
|
fprintf fmt "%a @[<hov>? %a@ : %a@]"
|
|
260
|
pp_c c
|
|
261
|
pp_t t
|
|
262
|
pp_f f
|
|
263
|
|
|
264
|
let pp_paren pp fmt v =
|
|
265
|
fprintf fmt "(%a)" pp v
|
|
266
|
|
|
267
|
let pp_machine_decl fmt (id, mem_type, var) =
|
|
268
|
fprintf fmt "struct %s_%s %s" id mem_type var
|
|
269
|
|
|
270
|
let pp_mem_ghost pp_mem pp_self ?i fmt (name, mem, self) =
|
|
271
|
fprintf fmt "%s_ghost%a(@[<hov>%a,@ %a@])"
|
|
272
|
name
|
|
273
|
(pp_print_option pp_print_int) i
|
|
274
|
pp_mem mem
|
|
275
|
pp_self self
|
|
276
|
|
|
277
|
let pp_mem_ghost' = pp_mem_ghost pp_print_string pp_print_string
|
|
278
|
|
|
279
|
let pp_mem_init pp_mem fmt (name, mem) =
|
|
280
|
fprintf fmt "%s_initialization(%a)" name pp_mem mem
|
|
281
|
|
|
282
|
let pp_mem_init' = pp_mem_init pp_print_string
|
|
283
|
|
|
284
|
let pp_var_decl fmt v =
|
|
285
|
pp_print_string fmt v.var_id
|
|
286
|
|
|
287
|
let pp_locals m fmt vs =
|
|
288
|
pp_print_list
|
|
289
|
~pp_open_box:pp_open_hbox
|
|
290
|
~pp_sep:pp_print_comma
|
|
291
|
(pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m) fmt vs
|
|
292
|
|
|
293
|
let pp_ptr_decl fmt v =
|
|
294
|
fprintf fmt "*%s" v.var_id
|
|
295
|
|
|
296
|
let pp_basic_assign_spec pp_var fmt typ var_name value =
|
|
297
|
if Types.is_real_type typ && !Options.mpfr
|
|
298
|
then
|
|
299
|
assert false
|
|
300
|
(* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
|
|
301
|
else
|
|
302
|
pp_equal pp_var pp_var fmt (var_name, value)
|
|
303
|
|
|
304
|
let pp_assign_spec m self pp_var fmt (var_type, var_name, value) =
|
|
305
|
let depth = expansion_depth value in
|
|
306
|
let loop_vars = mk_loop_variables m var_type depth in
|
|
307
|
let reordered_loop_vars = reorder_loop_variables loop_vars in
|
|
308
|
let rec aux typ fmt vars =
|
|
309
|
match vars with
|
|
310
|
| [] ->
|
|
311
|
pp_basic_assign_spec
|
|
312
|
(pp_value_suffix ~indirect:false m self var_type loop_vars pp_var)
|
|
313
|
fmt typ var_name value
|
|
314
|
| (d, LVar i) :: q ->
|
|
315
|
assert false
|
|
316
|
(* let typ' = Types.array_element_type typ in
|
|
317
|
* fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
|
|
318
|
* i i i pp_c_dimension d i
|
|
319
|
* (aux typ') q *)
|
|
320
|
| (d, LInt r) :: q ->
|
|
321
|
assert false
|
|
322
|
(* let typ' = Types.array_element_type typ in
|
|
323
|
* let szl = Utils.enumerate (Dimension.size_const_dimension d) in
|
|
324
|
* fprintf fmt "@[<v 2>{@,%a@]@,}"
|
|
325
|
* (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)
|
|
326
|
| _ -> assert false
|
|
327
|
in
|
|
328
|
begin
|
|
329
|
reset_loop_counter ();
|
|
330
|
aux var_type fmt reordered_loop_vars;
|
|
331
|
end
|
|
332
|
|
|
333
|
let pp_c_var_read m fmt id =
|
|
334
|
(* mpfr_t is a static array, not treated as general arrays *)
|
|
335
|
if Types.is_address_type id.var_type
|
|
336
|
then
|
|
337
|
if Machine_code_common.is_memory m id
|
|
338
|
&& not (Types.is_real_type id.var_type && !Options.mpfr)
|
|
339
|
then fprintf fmt "(*%s)" id.var_id
|
|
340
|
else fprintf fmt "%s" id.var_id
|
|
341
|
else
|
|
342
|
fprintf fmt "%s" id.var_id
|
|
343
|
|
|
344
|
let rec assigned s instr =
|
|
345
|
let open VDSet in
|
|
346
|
match instr.instr_desc with
|
|
347
|
| MLocalAssign (x, _) ->
|
|
348
|
add x s
|
|
349
|
| MStep (xs, _, _) ->
|
|
350
|
union s (of_list xs)
|
|
351
|
| MBranch (_, brs) ->
|
|
352
|
List.(fold_left (fun s (_, instrs) -> fold_left assigned s instrs) s brs)
|
|
353
|
| _ -> s
|
|
354
|
|
|
355
|
let rec occur_val s v =
|
|
356
|
let open VDSet in
|
|
357
|
match v.value_desc with
|
|
358
|
| Var x ->
|
|
359
|
add x s
|
|
360
|
| Fun (_, vs)
|
|
361
|
| Array vs ->
|
|
362
|
List.fold_left occur_val s vs
|
|
363
|
| Access (v1, v2)
|
|
364
|
| Power (v1, v2) ->
|
|
365
|
occur_val (occur_val s v1) v2
|
|
366
|
| _ -> s
|
|
367
|
|
|
368
|
let rec occur s instr =
|
|
369
|
let open VDSet in
|
|
370
|
match instr.instr_desc with
|
|
371
|
| MLocalAssign (_, v)
|
|
372
|
| MStateAssign (_, v) ->
|
|
373
|
occur_val s v
|
|
374
|
| MStep (_, _, vs) ->
|
|
375
|
List.fold_left occur_val s vs
|
|
376
|
| MBranch (v, brs) ->
|
|
377
|
List.(fold_left (fun s (_, instrs) -> fold_left occur s instrs)
|
|
378
|
(occur_val s v) brs)
|
|
379
|
| _ -> s
|
|
380
|
|
|
381
|
let live = Hashtbl.create 32
|
|
382
|
|
|
383
|
let set_live_of m =
|
|
384
|
let open VDSet in
|
|
385
|
let locals = of_list m.mstep.step_locals in
|
|
386
|
let outputs = of_list m.mstep.step_outputs in
|
|
387
|
let vars = union locals outputs in
|
|
388
|
let no_occur_after i =
|
|
389
|
let occ, _ = List.fold_left (fun (s, j) instr ->
|
|
390
|
if j <= i then (s, j+1) else (occur s instr, j+1))
|
|
391
|
(empty, 0) m.mstep.step_instrs in
|
|
392
|
diff locals occ
|
|
393
|
in
|
|
394
|
let l, _, _ = List.fold_left (fun (l, asg, i) instr ->
|
|
395
|
let asg = inter (assigned asg instr) vars in
|
|
396
|
Live.add (i + 1) (diff asg (no_occur_after i)) l, asg, i + 1)
|
|
397
|
(Live.empty, empty, 0) m.mstep.step_instrs in
|
|
398
|
Hashtbl.add live m.mname.node_id (Live.add 0 empty l)
|
|
399
|
|
|
400
|
let live_i m i =
|
|
401
|
Live.find i (Hashtbl.find live m.mname.node_id)
|
|
402
|
|
|
403
|
let pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_input pp_output fmt
|
|
404
|
(name, inputs, locals, outputs, mem_in, mem_out) =
|
|
405
|
fprintf fmt "%s_transition%a(@[<hov>%a,@ %a%a%a%a@])"
|
|
406
|
name
|
|
407
|
(pp_print_option pp_print_int) i
|
|
408
|
pp_mem_in mem_in
|
|
409
|
(pp_print_list
|
|
410
|
~pp_epilogue:pp_print_comma
|
|
411
|
~pp_sep:pp_print_comma
|
|
412
|
pp_input) inputs
|
|
413
|
(pp_print_option
|
|
414
|
(fun fmt _ ->
|
|
415
|
pp_print_list
|
|
416
|
~pp_epilogue:pp_print_comma
|
|
417
|
~pp_sep:pp_print_comma
|
|
418
|
pp_input fmt locals))
|
|
419
|
i
|
|
420
|
pp_mem_out mem_out
|
|
421
|
(pp_print_list
|
|
422
|
~pp_prologue:pp_print_comma
|
|
423
|
~pp_sep:pp_print_comma
|
|
424
|
pp_output) outputs
|
|
425
|
|
|
426
|
let pp_mem_trans ?i pp_mem_in pp_mem_out pp_input pp_output fmt
|
|
427
|
(m, mem_in, mem_out) =
|
|
428
|
let locals, outputs = match i with
|
|
429
|
| Some 0 ->
|
|
430
|
[], []
|
|
431
|
| Some i when i < List.length m.mstep.step_instrs ->
|
|
432
|
let li = live_i m i in
|
|
433
|
VDSet.(inter (of_list m.mstep.step_locals) li |> elements,
|
|
434
|
inter (of_list m.mstep.step_outputs) li |> elements)
|
|
435
|
| Some _ ->
|
|
436
|
[], m.mstep.step_outputs
|
|
437
|
| _ ->
|
|
438
|
m.mstep.step_locals, m.mstep.step_outputs
|
|
439
|
in
|
|
440
|
pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_input pp_output fmt
|
|
441
|
(m.mname.node_id,
|
|
442
|
m.mstep.step_inputs,
|
|
443
|
locals,
|
|
444
|
outputs,
|
|
445
|
mem_in,
|
|
446
|
mem_out)
|
|
447
|
|
|
448
|
let pp_mem_trans' ?i fmt =
|
|
449
|
pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_var_decl fmt
|
|
450
|
let pp_mem_trans'' ?i fmt =
|
|
451
|
pp_mem_trans ?i pp_print_string pp_print_string pp_var_decl pp_ptr_decl fmt
|
|
452
|
|
|
453
|
let pp_nothing fmt () =
|
|
454
|
pp_print_string fmt "\\nothing"
|
|
455
|
|
|
456
|
let pp_predicate pp_l pp_r fmt (l, r) =
|
|
457
|
fprintf fmt "@[<v 2>predicate %a =@,%a;@]"
|
|
458
|
pp_l l
|
|
459
|
pp_r r
|
|
460
|
|
|
461
|
let print_machine_valid_predicate fmt m =
|
|
462
|
if not (fst (Machine_code_common.get_stateless_status m)) then
|
|
463
|
let name = m.mname.node_id in
|
|
464
|
let self = mk_self m in
|
|
465
|
pp_spec
|
|
466
|
(pp_predicate
|
|
467
|
(pp_mem_valid pp_machine_decl)
|
|
468
|
(pp_and
|
|
469
|
(pp_and_l (fun fmt (_, (td, _) as inst) ->
|
|
470
|
pp_mem_valid (pp_inst self) fmt (node_name td, inst)))
|
|
471
|
(pp_valid pp_print_string)))
|
|
472
|
fmt
|
|
473
|
((name, (name, "mem", "*" ^ self)),
|
|
474
|
(m.minstances, [self]))
|
|
475
|
|
|
476
|
let print_machine_ghost_simulation_aux ?i m pp fmt v =
|
|
477
|
let name = m.mname.node_id in
|
|
478
|
let self = mk_self m in
|
|
479
|
let mem = mk_mem m in
|
|
480
|
pp_spec
|
|
481
|
(pp_predicate
|
|
482
|
(pp_mem_ghost pp_machine_decl pp_machine_decl ?i)
|
|
483
|
pp)
|
|
484
|
fmt
|
|
485
|
((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
|
|
486
|
v)
|
|
487
|
|
|
488
|
let print_ghost_simulation dependencies m fmt (i, instr) =
|
|
489
|
let name = m.mname.node_id in
|
|
490
|
let self = mk_self m in
|
|
491
|
let mem = mk_mem m in
|
|
492
|
let prev_ghost fmt () = pp_mem_ghost' ~i fmt (name, mem, self) in
|
|
493
|
let pred pp v = pp_and prev_ghost pp fmt ((), v) in
|
|
494
|
let rec aux fmt instr =
|
|
495
|
match instr.instr_desc with
|
|
496
|
| MStateAssign (m, _) ->
|
|
497
|
pp_equal
|
|
498
|
(pp_access (pp_access pp_var_decl))
|
|
499
|
(pp_indirect (pp_access pp_var_decl))
|
|
500
|
fmt
|
|
501
|
((mem, ("_reg", m)), (self, ("_reg", m)))
|
|
502
|
| MStep ([i0], i, vl)
|
|
503
|
when Basic_library.is_value_internal_fun
|
|
504
|
(mk_val (Fun (i, vl)) i0.var_type) ->
|
|
505
|
pp_true fmt ()
|
|
506
|
| MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
|
|
507
|
pp_true fmt ()
|
|
508
|
| MStep ([_], i, _) when has_c_prototype i dependencies ->
|
|
509
|
pp_true fmt ()
|
|
510
|
| MStep (_, i, _)
|
|
511
|
| MReset i ->
|
|
512
|
begin try
|
|
513
|
let n, _ = List.assoc i m.minstances in
|
|
514
|
pp_mem_ghost pp_access' pp_indirect' fmt
|
|
515
|
(node_name n, (mem, i), (self, i))
|
|
516
|
with Not_found -> pp_true fmt ()
|
|
517
|
end
|
|
518
|
| MBranch (_, brs) ->
|
|
519
|
(* TODO: handle branches *)
|
|
520
|
pp_and_l aux fmt List.(flatten (map snd brs))
|
|
521
|
| _ -> pp_true fmt ()
|
|
522
|
in
|
|
523
|
pred aux instr
|
|
524
|
|
|
525
|
let print_machine_ghost_simulation dependencies m fmt i instr =
|
|
526
|
print_machine_ghost_simulation_aux m
|
|
527
|
(print_ghost_simulation dependencies m)
|
|
528
|
~i:(i+1)
|
|
529
|
fmt (i, instr)
|
|
530
|
|
|
531
|
let print_machine_ghost_struct fmt m =
|
|
532
|
pp_spec (pp_ghost (print_machine_struct ~ghost:true)) fmt m
|
|
533
|
|
|
534
|
let print_machine_ghost_simulations dependencies fmt m =
|
|
535
|
if not (fst (Machine_code_common.get_stateless_status m)) then
|
|
536
|
let name = m.mname.node_id in
|
|
537
|
let self = mk_self m in
|
|
538
|
let mem = mk_mem m in
|
|
539
|
fprintf fmt "%a@,%a@,%a%a"
|
|
540
|
print_machine_ghost_struct m
|
|
541
|
(print_machine_ghost_simulation_aux m pp_true ~i:0) ()
|
|
542
|
(pp_print_list_i
|
|
543
|
~pp_epilogue:pp_print_cut
|
|
544
|
~pp_open_box:pp_open_vbox0
|
|
545
|
(print_machine_ghost_simulation dependencies m))
|
|
546
|
m.mstep.step_instrs
|
|
547
|
(print_machine_ghost_simulation_aux m
|
|
548
|
(pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
|
|
549
|
|
|
550
|
let print_machine_trans_simulation_aux ?i m pp fmt v =
|
|
551
|
let name = m.mname.node_id in
|
|
552
|
let mem_in = mk_mem_in m in
|
|
553
|
let mem_out = mk_mem_out m in
|
|
554
|
pp_spec
|
|
555
|
(pp_predicate
|
|
556
|
(pp_mem_trans pp_machine_decl pp_machine_decl
|
|
557
|
(pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
|
|
558
|
(pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m)
|
|
559
|
?i)
|
|
560
|
pp)
|
|
561
|
fmt
|
|
562
|
((m, (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
|
|
563
|
v)
|
|
564
|
|
|
565
|
let print_trans_simulation machines dependencies m fmt (i, instr) =
|
|
566
|
let mem_in = mk_mem_in m in
|
|
567
|
let mem_out = mk_mem_out m in
|
|
568
|
let d = VDSet.(diff (union (live_i m i) (assigned empty instr))
|
|
569
|
(live_i m (i+1))) in
|
|
570
|
(* XXX *)
|
|
571
|
printf "%d : %a\n%d : %a\nocc: %a\n\n"
|
|
572
|
i
|
|
573
|
(pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i))
|
|
574
|
(i+1)
|
|
575
|
(pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)))
|
|
576
|
(pp_print_parenthesized pp_var_decl) VDSet.(elements (assigned empty instr));
|
|
577
|
let prev_trans fmt () = pp_mem_trans' ~i fmt (m, mem_in, mem_out) in
|
|
578
|
let pred pp v =
|
|
579
|
let vars = VDSet.(union (of_list m.mstep.step_locals)
|
|
580
|
(of_list m.mstep.step_outputs)) in
|
|
581
|
let locals = VDSet.(inter vars d |> elements) in
|
|
582
|
if locals = []
|
|
583
|
then pp_and prev_trans pp fmt ((), v)
|
|
584
|
else pp_exists (pp_locals m) (pp_and prev_trans pp) fmt (locals, ((), v))
|
|
585
|
in
|
|
586
|
let rec aux fmt instr = match instr.instr_desc with
|
|
587
|
| MLocalAssign (x, v)
|
|
588
|
| MStateAssign (x, v) ->
|
|
589
|
pp_assign_spec m mem_in (pp_c_var_read m) fmt
|
|
590
|
(x.var_type, mk_val (Var x) x.var_type, v)
|
|
591
|
| MStep ([i0], i, vl)
|
|
592
|
when Basic_library.is_value_internal_fun
|
|
593
|
(mk_val (Fun (i, vl)) i0.var_type) ->
|
|
594
|
pp_true fmt ()
|
|
595
|
| MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
|
|
596
|
pp_true fmt ()
|
|
597
|
| MStep ([_], i, _) when has_c_prototype i dependencies ->
|
|
598
|
pp_true fmt ()
|
|
599
|
| MStep (xs, f, ys) ->
|
|
600
|
begin try
|
|
601
|
let n, _ = List.assoc f m.minstances in
|
|
602
|
pp_mem_trans_aux
|
|
603
|
pp_access' pp_access'
|
|
604
|
(pp_c_val m mem_in (pp_c_var_read m))
|
|
605
|
pp_var_decl
|
|
606
|
fmt
|
|
607
|
(node_name n, ys, [], xs, (mem_in, f), (mem_out, f))
|
|
608
|
with Not_found -> pp_true fmt ()
|
|
609
|
end
|
|
610
|
| MReset f ->
|
|
611
|
begin try
|
|
612
|
let n, _ = List.assoc f m.minstances in
|
|
613
|
pp_mem_init' fmt (node_name n, mem_out)
|
|
614
|
with Not_found -> pp_true fmt ()
|
|
615
|
end
|
|
616
|
| MBranch (v, brs) ->
|
|
617
|
(* if let t = fst (List.hd brs) in t = tag_true || t = tag_false
|
|
618
|
* then (\* boolean case *\)
|
|
619
|
* let tl = try List.assoc tag_true brs with Not_found -> [] in
|
|
620
|
* let el = try List.assoc tag_false brs with Not_found -> [] in
|
|
621
|
* pp_ite (pp_c_val m mem_in (pp_c_var_read m))
|
|
622
|
* (pp_paren (pp_and_l aux)) (pp_paren (pp_and_l aux))
|
|
623
|
* fmt (v, tl, el)
|
|
624
|
* else (\* enum type case *\) *)
|
|
625
|
pp_and_l (fun fmt (l, instrs) ->
|
|
626
|
let pp_val = pp_c_val m mem_in (pp_c_var_read m) in
|
|
627
|
if l = tag_false then
|
|
628
|
pp_paren (pp_implies
|
|
629
|
(pp_different pp_val pp_c_tag)
|
|
630
|
(pp_and_l aux))
|
|
631
|
fmt
|
|
632
|
((v, tag_true), instrs)
|
|
633
|
else
|
|
634
|
pp_paren (pp_implies
|
|
635
|
(pp_equal pp_val pp_c_tag)
|
|
636
|
(pp_and_l aux))
|
|
637
|
fmt
|
|
638
|
((v, l), instrs))
|
|
639
|
fmt brs
|
|
640
|
| _ -> pp_true fmt ()
|
|
641
|
in
|
|
642
|
pred aux instr
|
|
643
|
|
|
644
|
let print_machine_trans_simulation machines dependencies m fmt i instr =
|
|
645
|
print_machine_trans_simulation_aux m
|
|
646
|
(print_trans_simulation machines dependencies m)
|
|
647
|
~i:(i+1)
|
|
648
|
fmt (i, instr)
|
|
649
|
|
|
650
|
let print_machine_trans_annotations machines dependencies fmt m =
|
|
651
|
if not (fst (Machine_code_common.get_stateless_status m)) then begin
|
|
652
|
set_live_of m;
|
|
653
|
let i = List.length m.mstep.step_instrs in
|
|
654
|
let mem_in = mk_mem_in m in
|
|
655
|
let mem_out = mk_mem_out m in
|
|
656
|
let last_trans fmt () =
|
|
657
|
let locals = VDSet.(inter
|
|
658
|
(of_list m.mstep.step_locals)
|
|
659
|
(live_i m i)
|
|
660
|
|> elements) in
|
|
661
|
if locals = []
|
|
662
|
then pp_mem_trans' ~i fmt (m, mem_in, mem_out)
|
|
663
|
else pp_exists (pp_locals m) (pp_mem_trans' ~i) fmt
|
|
664
|
(locals, (m, mem_in, mem_out))
|
|
665
|
in
|
|
666
|
fprintf fmt "%a@,%a%a"
|
|
667
|
(print_machine_trans_simulation_aux m pp_true ~i:0) ()
|
|
668
|
(pp_print_list_i
|
|
669
|
~pp_epilogue:pp_print_cut
|
|
670
|
~pp_open_box:pp_open_vbox0
|
|
671
|
(print_machine_trans_simulation machines dependencies m))
|
|
672
|
m.mstep.step_instrs
|
|
673
|
(print_machine_trans_simulation_aux m last_trans) ()
|
|
674
|
end
|
|
675
|
|
|
676
|
let print_machine_init_predicate fmt m =
|
|
677
|
if not (fst (Machine_code_common.get_stateless_status m)) then
|
|
678
|
let name = m.mname.node_id in
|
|
679
|
let mem_in = mk_mem_in m in
|
|
680
|
pp_spec
|
|
681
|
(pp_predicate
|
|
682
|
(pp_mem_init pp_machine_decl)
|
|
683
|
(pp_and_l (fun fmt (i, (td, _)) ->
|
|
684
|
pp_mem_init pp_access' fmt (node_name td, (mem_in, i)))))
|
|
685
|
fmt
|
|
686
|
((name, (name, "mem_ghost", mem_in)), m.minstances)
|
|
687
|
|
|
688
|
let pp_at pp_p fmt (p, l) =
|
|
689
|
fprintf fmt "\\at(%a, %s)" pp_p p l
|
|
690
|
|
|
691
|
let label_pre = "Pre"
|
|
692
|
|
|
693
|
let pp_at_pre pp_p fmt p =
|
|
694
|
pp_at pp_p fmt (p, label_pre)
|
|
695
|
|
|
696
|
let pp_arrow_spec fmt () =
|
|
697
|
let name = "_arrow" in
|
|
698
|
let mem_in = "mem_in" in
|
|
699
|
let mem_out = "mem_out" in
|
|
700
|
let reg_first = "_reg", "_first" in
|
|
701
|
let mem_in_first = mem_in, reg_first in
|
|
702
|
let mem_out_first = mem_out, reg_first in
|
|
703
|
let mem = "mem" in
|
|
704
|
let self = "self" in
|
|
705
|
fprintf fmt "/* ACSL arrow spec */@,%a%a%a%a%a"
|
|
706
|
|
|
707
|
(pp_spec_line (pp_ghost pp_print_string))
|
|
708
|
"struct _arrow_mem_ghost {struct _arrow_reg _reg;};"
|
|
709
|
|
|
710
|
(pp_spec_cut
|
|
711
|
(pp_predicate
|
|
712
|
(pp_mem_valid pp_machine_decl)
|
|
713
|
(pp_valid pp_print_string)))
|
|
714
|
((name, (name, "mem", "*" ^ self)), [self])
|
|
715
|
|
|
716
|
(pp_spec_cut
|
|
717
|
(pp_predicate
|
|
718
|
(pp_mem_init pp_machine_decl)
|
|
719
|
(pp_equal
|
|
720
|
(pp_access pp_access')
|
|
721
|
pp_print_int)))
|
|
722
|
((name, (name, "mem_ghost", mem_in)),
|
|
723
|
(mem_in_first, 1))
|
|
724
|
|
|
725
|
(pp_spec_cut
|
|
726
|
(pp_predicate
|
|
727
|
(pp_mem_trans_aux
|
|
728
|
pp_machine_decl pp_machine_decl pp_print_string pp_print_string)
|
|
729
|
(pp_ite
|
|
730
|
(pp_access pp_access')
|
|
731
|
(pp_paren
|
|
732
|
(pp_and
|
|
733
|
(pp_equal
|
|
734
|
(pp_access pp_access')
|
|
735
|
pp_print_int)
|
|
736
|
(pp_equal pp_print_string pp_print_string)))
|
|
737
|
(pp_paren
|
|
738
|
(pp_and
|
|
739
|
(pp_equal
|
|
740
|
(pp_access pp_access')
|
|
741
|
(pp_access pp_access'))
|
|
742
|
(pp_equal pp_print_string pp_print_string))))))
|
|
743
|
((name, ["integer x"; "integer y"], [], ["integer out"],
|
|
744
|
(name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
|
|
745
|
(* (("out", mem_in_first), *)
|
|
746
|
(mem_in_first, ((mem_out_first, 0), ("out", "x")),
|
|
747
|
((mem_out_first, mem_in_first), ("out", "y"))))
|
|
748
|
|
|
749
|
(pp_spec_cut
|
|
750
|
(pp_predicate
|
|
751
|
(pp_mem_ghost pp_machine_decl pp_machine_decl)
|
|
752
|
(pp_equal
|
|
753
|
(pp_access pp_access')
|
|
754
|
(pp_indirect pp_access'))))
|
|
755
|
((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
|
|
756
|
((mem, reg_first), (self, reg_first)))
|
|
757
|
|
|
758
|
module SrcMod = struct
|
|
759
|
|
|
760
|
let pp_predicates dependencies fmt machines =
|
|
761
|
fprintf fmt
|
|
762
|
"%a@,%a%a%a%a"
|
|
763
|
pp_arrow_spec ()
|
|
764
|
(pp_print_list
|
|
765
|
~pp_open_box:pp_open_vbox0
|
|
766
|
~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")
|
|
767
|
print_machine_valid_predicate
|
|
768
|
~pp_epilogue:pp_print_cutcut) machines
|
|
769
|
(pp_print_list
|
|
770
|
~pp_open_box:pp_open_vbox0
|
|
771
|
~pp_sep:pp_print_cutcut
|
|
772
|
~pp_prologue:(pp_print_endcut "/* ACSL ghost simulations */")
|
|
773
|
(print_machine_ghost_simulations dependencies)
|
|
774
|
~pp_epilogue:pp_print_cutcut) machines
|
|
775
|
(pp_print_list
|
|
776
|
~pp_open_box:pp_open_vbox0
|
|
777
|
~pp_sep:pp_print_cutcut
|
|
778
|
~pp_prologue:(pp_print_endcut "/* ACSL initialization annotations */")
|
|
779
|
print_machine_init_predicate
|
|
780
|
~pp_epilogue:pp_print_cutcut) machines
|
|
781
|
(pp_print_list
|
|
782
|
~pp_open_box:pp_open_vbox0
|
|
783
|
~pp_sep:pp_print_cutcut
|
|
784
|
~pp_prologue:(pp_print_endcut "/* ACSL transition annotations */")
|
|
785
|
(print_machine_trans_annotations machines dependencies)
|
|
786
|
~pp_epilogue:pp_print_cutcut) machines
|
|
787
|
|
|
788
|
let pp_reset_spec fmt self m =
|
|
789
|
let name = m.mname.node_id in
|
|
790
|
let mem = mk_mem m in
|
|
791
|
pp_spec_cut (fun fmt () ->
|
|
792
|
fprintf fmt
|
|
793
|
"%a@,%a@,%a@,%a"
|
|
794
|
(pp_requires pp_mem_valid') (name, self)
|
|
795
|
(pp_requires (pp_separated self)) m.minstances
|
|
796
|
(pp_assigns
|
|
797
|
(pp_print_list
|
|
798
|
~pp_sep:pp_print_comma
|
|
799
|
~pp_nil:pp_nothing
|
|
800
|
(pp_inst self))) m.minstances
|
|
801
|
(pp_ensures
|
|
802
|
(pp_forall
|
|
803
|
pp_machine_decl
|
|
804
|
(pp_implies
|
|
805
|
pp_mem_ghost'
|
|
806
|
pp_mem_init')))
|
|
807
|
((name, "mem_ghost", mem),
|
|
808
|
((name, mem, self), (name, mem))))
|
|
809
|
fmt ()
|
|
810
|
|
|
811
|
let pp_step_spec fmt self m =
|
|
812
|
let name = m.mname.node_id in
|
|
813
|
let mem_in = mk_mem_in m in
|
|
814
|
let mem_out = mk_mem_out m in
|
|
815
|
pp_spec_cut (fun fmt () ->
|
|
816
|
fprintf fmt
|
|
817
|
"%a@,%a@,%a@,%a@,%a"
|
|
818
|
(pp_requires (pp_valid pp_var_decl)) m.mstep.step_outputs
|
|
819
|
(pp_requires pp_mem_valid') (name, self)
|
|
820
|
(pp_requires (pp_separated self)) m.minstances
|
|
821
|
(pp_assigns
|
|
822
|
(if m.mstep.step_outputs = [] && m.minstances = [] then
|
|
823
|
pp_nothing
|
|
824
|
else
|
|
825
|
fun fmt () ->
|
|
826
|
fprintf fmt "@[<h>%a%a@]"
|
|
827
|
(pp_print_list
|
|
828
|
~pp_sep:pp_print_comma
|
|
829
|
~pp_epilogue:pp_print_comma
|
|
830
|
pp_ptr_decl) m.mstep.step_outputs
|
|
831
|
(pp_print_list
|
|
832
|
~pp_sep:pp_print_comma
|
|
833
|
(pp_inst self)) m.minstances)) ()
|
|
834
|
(pp_ensures
|
|
835
|
(pp_forall
|
|
836
|
(fun fmt () ->
|
|
837
|
fprintf fmt "%a, %s"
|
|
838
|
pp_machine_decl (name, "mem_ghost", mem_in)
|
|
839
|
mem_out)
|
|
840
|
(pp_implies
|
|
841
|
(pp_at_pre pp_mem_ghost')
|
|
842
|
(pp_implies
|
|
843
|
pp_mem_ghost'
|
|
844
|
pp_mem_trans''))))
|
|
845
|
((),
|
|
846
|
((name, mem_in, self),
|
|
847
|
((name, mem_out, self),
|
|
848
|
(m, mem_in, mem_out)))))
|
|
849
|
fmt ()
|
|
850
|
|
|
851
|
let pp_step_instr_spec m self fmt (i, _instr) =
|
|
852
|
let name = m.mname.node_id in
|
|
853
|
let mem_in = mk_mem_in m in
|
|
854
|
let mem_out = mk_mem_out m in
|
|
855
|
fprintf fmt "@,%a"
|
|
856
|
(pp_spec
|
|
857
|
(pp_assert
|
|
858
|
(pp_forall
|
|
859
|
(fun fmt () ->
|
|
860
|
fprintf fmt "%a, %s"
|
|
861
|
pp_machine_decl (name, "mem_ghost", mem_in)
|
|
862
|
mem_out)
|
|
863
|
(pp_implies
|
|
864
|
(pp_at_pre pp_mem_ghost')
|
|
865
|
(pp_implies
|
|
866
|
(pp_mem_ghost' ~i)
|
|
867
|
(pp_mem_trans'' ~i))))))
|
|
868
|
((),
|
|
869
|
((name, mem_in, self),
|
|
870
|
((name, mem_out, self),
|
|
871
|
(m, mem_in, mem_out))))
|
|
872
|
|
|
873
|
end
|
|
874
|
|
|
875
|
(**************************************************************************)
|
|
876
|
(* MAKEFILE *)
|
|
877
|
(**************************************************************************)
|
|
878
|
|
|
879
|
module MakefileMod = struct
|
|
880
|
|
|
881
|
let other_targets fmt basename _nodename dependencies =
|
|
882
|
fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
|
|
883
|
(* EACSL version of library file . c *)
|
|
884
|
fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
|
|
885
|
fprintf fmt
|
|
886
|
"\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@."
|
|
887
|
basename basename;
|
|
888
|
fprintf fmt "@.";
|
|
889
|
fprintf fmt "@.";
|
|
890
|
|
|
891
|
(* EACSL version of library file . c + main .c *)
|
|
892
|
fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;
|
|
893
|
fprintf fmt "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c -then-on e-acsl -print -ocode %s_main_eacsl.i@."
|
|
894
|
basename basename basename;
|
|
895
|
(* Ugly hack to deal with eacsl bugs *)
|
|
896
|
fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;
|
|
897
|
fprintf fmt "@.";
|
|
898
|
fprintf fmt "@.";
|
|
899
|
|
|
900
|
(* EACSL version of binary *)
|
|
901
|
fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
|
|
902
|
fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)
|
|
903
|
C_backend_makefile.fprintf_dependencies fmt dependencies;
|
|
904
|
fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@."
|
|
905
|
basename
|
|
906
|
(Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name))
|
|
907
|
(C_backend_makefile.compiled_dependencies dependencies)
|
|
908
|
("${FRAMACEACSL}/e_acsl.c "
|
|
909
|
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
|
|
910
|
^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
|
|
911
|
basename
|
|
912
|
(Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
|
|
913
|
(C_backend_makefile.lib_dependencies dependencies)
|
|
914
|
;
|
|
915
|
fprintf fmt "@."
|
|
916
|
|
|
917
|
end
|
|
918
|
|
|
919
|
(* Local Variables: *)
|
|
920
|
(* compile-command:"make -C ../../.." *)
|
|
921
|
(* End: *)
|