Project

General

Profile

« Previous | Next » 

Revision c226a3ba

Added by LĂ©lio Brun over 2 years ago

start generating ACSL spec

View differences:

src/backends/C/c_backend.ml
117 117

  
118 118
    | "acsl" ->
119 119
      C_backend_header.(module EmptyMod : MODIFIERS_HDR),
120
      C_backend_src.(module EmptyMod : MODIFIERS_SRC),
120
      (module C_backend_spec.SrcMod : C_backend_src.MODIFIERS_SRC),
121 121
      C_backend_main.(module EmptyMod : MODIFIERS_MAINSRC),
122 122
      (module C_backend_spec.MakefileMod : C_backend_makefile.MODIFIERS_MKF),
123 123
      C_backend_spec.preprocess_acsl
src/backends/C/c_backend_common.ml
40 40
let var_is name v =
41 41
  v.var_id = name
42 42

  
43
(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *)
44
let mk_self m =
43
let mk_local n m =
45 44
  let used name =
46 45
    let open List in
47 46
    exists (var_is name) m.mstep.step_inputs
48 47
    || exists (var_is name) m.mstep.step_outputs
49 48
    || exists (var_is name) m.mstep.step_locals
50 49
    || exists (var_is name) m.mmemory in
51
  mk_new_name used "self"
50
  mk_new_name used n
51

  
52
(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *)
53
let mk_self = mk_local "self"
54

  
55
let mk_mem = mk_local "mem"
56
let mk_mem_in = mk_local "mem_in"
57
let mk_mem_out = mk_local "mem_out"
52 58

  
53 59
(* Generation of a non-clashing name for the instance variable of static allocation macro *)
54 60
let mk_instance m =
......
110 116
*)
111 117
let pp_global_init_name fmt id = fprintf fmt "%s_INIT" id
112 118
let pp_global_clear_name fmt id = fprintf fmt "%s_CLEAR" id
113
let pp_machine_memtype_name fmt id = fprintf fmt "struct %s_mem" id
119
let pp_machine_memtype_name ?(ghost=false) fmt id =
120
  fprintf fmt "struct %s_mem%s" id (if ghost then "_ghost" else "")
114 121
let pp_machine_regtype_name fmt id = fprintf fmt "struct %s_reg" id
115 122
let pp_machine_alloc_name fmt id = fprintf fmt "%s_alloc" id
116 123
let pp_machine_dealloc_name fmt id = fprintf fmt "%s_dealloc" id
......
216 223
  | _ ->
217 224
     fprintf fmt "%s" (pp_c_basic_type_desc t)
218 225

  
219
let pp_c_type ?(var_opt=None) var_id fmt t =
226
let pp_c_type ?var_opt var_id fmt t =
220 227
  let rec aux t pp_suffix =
221 228
    if is_basic_c_type  t then
222 229
       fprintf fmt "%a %s%a"
......
352 359
let pp_c_decl_input_var fmt id =
353 360
  if !Options.ansi && Types.is_address_type id.var_type
354 361
  then
355
    pp_c_type ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt
362
    pp_c_type ~var_opt:id (sprintf "(*%s)" id.var_id) fmt
356 363
      (Types.array_base_type id.var_type)
357 364
  else
358
    pp_c_type ~var_opt:(Some id) id.var_id fmt id.var_type
365
    pp_c_type ~var_opt:id id.var_id fmt id.var_type
359 366

  
360 367
(* Declaration of an output variable:
361 368
   - if its type is scalar, then pass its address
......
366 373
let pp_c_decl_output_var fmt id =
367 374
  if (not !Options.ansi) && Types.is_address_type id.var_type
368 375
  then
369
    pp_c_type ~var_opt:(Some id) id.var_id fmt id.var_type
376
    pp_c_type ~var_opt:id id.var_id fmt id.var_type
370 377
  else
371
    pp_c_type ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt
378
    pp_c_type ~var_opt:id (sprintf "(*%s)" id.var_id) fmt
372 379
      (Types.array_base_type id.var_type)
373 380

  
374 381
(* Declaration of a local/mem variable:
......
380 387
  if id.var_dec_const
381 388
  then
382 389
    fprintf fmt "%a = %a"
383
      (pp_c_type ~var_opt:(Some id) id.var_id)
390
      (pp_c_type ~var_opt:id id.var_id)
384 391
      id.var_type
385 392
      (pp_c_val m "" (pp_c_var_read m))
386 393
      (Machine_code_common.get_const_assign m id)
387 394
  else
388 395
    fprintf fmt "%a"
389
      (pp_c_type ~var_opt:(Some id) id.var_id) id.var_type
396
      (pp_c_type ~var_opt:id id.var_id) id.var_type
390 397

  
391 398
(* Declaration of a struct variable:
392 399
   - if it's an array/matrix/etc, we declare it as a pointer
......
399 406
  else
400 407
    pp_c_type id.var_id  fmt id.var_type
401 408

  
402
let pp_c_decl_instance_var fmt (name, (node, _)) =
403
  fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
409
let pp_c_decl_instance_var ?(ghost=false) fmt (name, (node, _)) =
410
  fprintf fmt "%a %s%s"
411
    (pp_machine_memtype_name ~ghost) (node_name node)
412
    (if ghost then "" else "*")
413
    name
404 414

  
405 415
(* let pp_c_checks self fmt m =
406 416
 *   pp_print_list
......
412 422
 *     fmt
413 423
 *     m.mstep.step_checks *)
414 424

  
425
let has_c_prototype funname dependencies =
426
  (* We select the last imported node with the name funname.
427
     The order of evaluation of dependencies should be
428
     compatible with overloading. (Not checked yet) *)
429
  let imported_node_opt =
430
    List.fold_left
431
      (fun res dep ->
432
         match res with
433
         | Some _ -> res
434
         | None ->
435
           let decls = dep.content in
436
           let matched = fun t -> match t.top_decl_desc with
437
             | ImportedNode nd -> nd.nodei_id = funname
438
             | _ -> false
439
           in
440
           if List.exists matched decls then
441
             match (List.find matched decls).top_decl_desc with
442
             | ImportedNode nd -> Some nd
443
             | _ -> assert false
444
           else
445
             None) None dependencies in
446
  match imported_node_opt with
447
  | None -> false
448
  | Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)
449

  
415 450
(********************************************************************************************)
416 451
(*                       Struct Printing functions                                          *)
417 452
(********************************************************************************************)
......
427 462
 *     pp_c_decl_struct_var
428 463
 *     fmt m.mmemory *)
429 464

  
430
let print_machine_struct fmt m =
465
let print_machine_struct ?(ghost=false) fmt m =
431 466
  if not (fst (Machine_code_common.get_stateless_status m)) then
432 467
    (* Define struct *)
433 468
    fprintf fmt "@[<v 2>%a {%a%a@]@,};"
434
      pp_machine_memtype_name m.mname.node_id
435
      (pp_print_list
436
         ~pp_open_box:pp_open_vbox0
437
         ~pp_prologue:(fun fmt () ->
438
             fprintf fmt "@,@[%a {" pp_machine_regtype_name m.mname.node_id)
439
         ~pp_sep:pp_print_semicolon
440
         ~pp_eol:pp_print_semicolon'
441
         ~pp_epilogue:(fun fmt () -> fprintf fmt "}@] _reg;")
442
         pp_c_decl_struct_var)
469
      (pp_machine_memtype_name ~ghost) m.mname.node_id
470
      (if ghost then
471
         (fun fmt -> function
472
            | [] -> pp_print_nothing fmt ()
473
            | _ -> fprintf fmt "@,%a _reg;"
474
                     pp_machine_regtype_name m.mname.node_id)
475
       else
476
         pp_print_list
477
           ~pp_open_box:pp_open_vbox0
478
           ~pp_prologue:(fun fmt () ->
479
               fprintf fmt "@,@[%a {" pp_machine_regtype_name m.mname.node_id)
480
           ~pp_sep:pp_print_semicolon
481
           ~pp_eol:pp_print_semicolon'
482
           ~pp_epilogue:(fun fmt () -> fprintf fmt "}@] _reg;")
483
           pp_c_decl_struct_var)
443 484
      m.mmemory
444 485
      (pp_print_list
486
         ~pp_open_box:pp_open_vbox0
445 487
         ~pp_prologue:pp_print_cut
446 488
         ~pp_sep:pp_print_semicolon
447 489
         ~pp_eol:pp_print_semicolon'
448
         pp_c_decl_instance_var)
490
         (pp_c_decl_instance_var ~ghost))
449 491
      m.minstances
450 492

  
451 493
(********************************************************************************************)
......
462 504

  
463 505
let print_alloc_prototype fmt (name, static) =
464 506
  fprintf fmt "%a * %a %a"
465
    pp_machine_memtype_name name
507
    (pp_machine_memtype_name ~ghost:false) name
466 508
    pp_machine_alloc_name name
467 509
    (pp_print_parenthesized pp_c_decl_input_var) static
468 510

  
469 511
let print_dealloc_prototype fmt name =
470 512
  fprintf fmt "void %a (%a * _alloc)"
471 513
    pp_machine_dealloc_name name
472
    pp_machine_memtype_name name
473
    
514
    (pp_machine_memtype_name ~ghost:false) name
515

  
474 516
let print_reset_prototype self fmt (name, static) =
475 517
  fprintf fmt "void %a (%a%a *%s)"
476 518
    pp_machine_reset_name name
477 519
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
478 520
       pp_c_decl_input_var) static
479
    pp_machine_memtype_name name
521
    (pp_machine_memtype_name ~ghost:false) name
480 522
    self
481 523

  
482 524
let print_init_prototype self fmt (name, static) =
......
484 526
    pp_machine_init_name name
485 527
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
486 528
       pp_c_decl_input_var) static
487
    pp_machine_memtype_name name
529
    (pp_machine_memtype_name ~ghost:false) name
488 530
    self
489 531

  
490 532
let print_clear_prototype self fmt (name, static) =
......
492 534
    pp_machine_clear_name name
493 535
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
494 536
       pp_c_decl_input_var) static
495
    pp_machine_memtype_name name
537
    (pp_machine_memtype_name ~ghost:false) name
496 538
    self
497 539

  
498 540
let print_stateless_prototype fmt (name, inputs, outputs) =
......
509 551
       ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs
510 552
    (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
511 553
       ~pp_epilogue:pp_print_cut pp_c_decl_output_var) outputs
512
    pp_machine_memtype_name name
554
    (pp_machine_memtype_name ~ghost:false) name
513 555
    self
514 556

  
515 557
let print_import_prototype fmt dep =
src/backends/C/c_backend_header.ml
105 105
      (* constants *)
106 106
      (print_static_constant_decl macro) const_locals
107 107
      attr
108
      pp_machine_memtype_name m.mname.node_id
108
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
109 109
      inst
110 110
      (pp_print_list ~pp_open_box:pp_open_vbox0
111 111
         ~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\")
......
201 201
    if not inode.nodei_stateless then
202 202
      (* Declare struct *)
203 203
      fprintf fmt "%a;"
204
        pp_machine_memtype_name inode.nodei_id
204
        (pp_machine_memtype_name ~ghost:false) inode.nodei_id
205 205

  
206 206
  let print_stateless_C_prototype fmt (name, inputs, outputs) =
207 207
    let output =
src/backends/C/c_backend_main.ml
85 85
               pp_machine_static_alloc_name mname
86 86
           else
87 87
             fprintf fmt "%a *main_mem = %a();"
88
               pp_machine_memtype_name mname
88
               (pp_machine_memtype_name ~ghost:false) mname
89 89
               pp_machine_alloc_name mname) ()
90 90
        pp_machine_reset_name mname
91 91
        main_mem
src/backends/C/c_backend_spec.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
open Format
12
open Utils.Format
13 13
open Lustre_types
14
open Machine_code_types
15
open C_backend_common
16
open Machine_code_common
17
open Corelang
14 18

  
15 19
(**************************************************************************)
16 20
(*     Printing spec for c *)
......
126 130

  
127 131
  *)
128 132

  
129
(* TODO ACSL
130
   mspec are function body annotations, sush as loop invariants, acsl asserts ... *) 
131
let pp_mspec _ _ = ()
132

  
133
   (* TODO ACSL 
133
   (* TODO ACSL
134 134
   Return updates machines (eg with local annotations) and acsl preamble *)
135 135
let preprocess_acsl machines = machines, []
136 136
                          
......
138 138
let pp_acsl_preamble fmt preamble =
139 139
  Format.fprintf fmt "";
140 140
  ()
141

  
142
let pp_spec pp fmt =
143
  fprintf fmt "@[<v>/*%@@[<v>@,%a@]@,*/@]" pp
144

  
145
let pp_spec_cut pp fmt =
146
  fprintf fmt "%a@," (pp_spec pp)
147

  
148
let pp_spec_line pp fmt =
149
  fprintf fmt "//%@ %a@," pp
150

  
151
let pp_requires pp_req fmt =
152
  fprintf fmt "requires %a;" pp_req
153

  
154
let pp_ensures pp_ens fmt =
155
  fprintf fmt "ensures %a;" pp_ens
156

  
157
let pp_assigns pp_asg fmt =
158
  fprintf fmt "assigns %a;" pp_asg
159

  
160
let pp_ghost pp_gho fmt =
161
  fprintf fmt "ghost %a" pp_gho
162

  
163
let pp_assert pp_ast fmt =
164
  fprintf fmt "assert %a;" pp_ast
165

  
166
let pp_mem_valid pp_var fmt (name, var) =
167
  fprintf fmt "%s_valid(%a)" name pp_var var
168

  
169
let pp_mem_valid' = pp_mem_valid pp_print_string
170

  
171
let pp_indirect pp_field fmt (ptr, field) =
172
  fprintf fmt "%s->%a" ptr pp_field field
173

  
174
let pp_indirect' = pp_indirect pp_print_string
175

  
176
let pp_access pp_field fmt (stru, field) =
177
  fprintf fmt "%s.%a" stru pp_field field
178

  
179
let pp_access' = pp_access pp_print_string
180

  
181
let pp_inst self fmt (name, _) =
182
  pp_indirect' fmt (self, name)
183

  
184
let pp_true fmt () =
185
  pp_print_string fmt "\\true"
186

  
187
let pp_separated self fmt =
188
  fprintf fmt "\\separated(@[<h>%s%a@])"
189
    self
190
    (pp_print_list
191
       ~pp_prologue:pp_print_comma
192
       ~pp_sep:pp_print_comma
193
       (pp_inst self))
194

  
195
let pp_forall pp_l pp_r fmt (l, r) =
196
  fprintf fmt "@[<v 2>\\forall %a;@,%a@]"
197
    pp_l l
198
    pp_r r
199

  
200
let pp_valid =
201
  pp_print_parenthesized
202
    ~pp_nil:pp_true
203
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\valid")
204

  
205
let pp_equal pp_l pp_r fmt (l, r) =
206
  fprintf fmt "%a == %a"
207
    pp_l l
208
    pp_r r
209

  
210
let pp_implies pp_l pp_r fmt (l, r) =
211
  fprintf fmt "%a ==>@ %a"
212
    pp_l l
213
    pp_r r
214

  
215
let pp_and pp_l pp_r fmt (l, r) =
216
  fprintf fmt "%a @ && %a"
217
    pp_l l
218
    pp_r r
219

  
220
let pp_and_l pp_v fmt =
221
  pp_print_list
222
    ~pp_open_box:pp_open_vbox0
223
    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")
224
    pp_v
225
    fmt
226

  
227
let pp_machine_decl fmt (id, mem_type, var) =
228
  fprintf fmt "struct %s_%s %s" id mem_type var
229

  
230
let pp_mem_ghost pp_mem pp_self ?i fmt (name, mem, self) =
231
  fprintf fmt "%s_ghost%a(%a, %a)"
232
    name
233
    (pp_print_option pp_print_int) i
234
    pp_mem mem
235
    pp_self self
236

  
237
let pp_mem_ghost' = pp_mem_ghost pp_print_string pp_print_string
238

  
239
let pp_mem_init fmt (name, mem) =
240
  fprintf fmt "%s_init(%s)" name mem
241

  
242
let pp_var_decl fmt v =
243
  pp_print_string fmt v.var_id
244

  
245
let pp_ptr_decl fmt v =
246
  fprintf fmt "*%s" v.var_id
247

  
248
let pp_mem_trans ?i fmt (m, mem_in, mem_out) =
249
  fprintf fmt "%s_trans%a(@[<h>%s, %a%s%a@])"
250
    m.mname.node_id
251
    (pp_print_option pp_print_int) i
252
    mem_in
253
    (pp_print_list
254
       ~pp_epilogue:pp_print_comma
255
       ~pp_sep:pp_print_comma
256
       pp_var_decl) m.mstep.step_inputs
257
    mem_out
258
    (pp_print_list
259
       ~pp_prologue:pp_print_comma
260
       ~pp_sep:pp_print_comma
261
       pp_ptr_decl) m.mstep.step_outputs
262

  
263
let pp_nothing fmt () =
264
  pp_print_string fmt "\\nothing"
265

  
266
let pp_predicate pp_l pp_r fmt (l, r) =
267
  fprintf fmt "@[<v 2>predicate %a =@,%a;@]"
268
    pp_l l
269
    pp_r r
270

  
271
let print_machine_valid_predicate fmt m =
272
  if not (fst (Machine_code_common.get_stateless_status m)) then
273
    let name = m.mname.node_id in
274
    let self = mk_self m in
275
    pp_spec
276
      (pp_predicate
277
         (pp_mem_valid pp_machine_decl)
278
         (pp_and
279
            (pp_and_l (fun fmt (_, (td, _) as inst) ->
280
                 pp_mem_valid (pp_inst self) fmt (node_name td, inst)))
281
            (pp_valid pp_print_string)))
282
      fmt
283
      ((name, (name, "mem", "*" ^ self)),
284
       (m.minstances, [self]))
285

  
286
let print_machine_ghost_simulation_aux ?i m pp fmt v =
287
  let name = m.mname.node_id in
288
  let self = mk_self m in
289
  let mem = mk_mem m in
290
  pp_spec
291
    (pp_predicate
292
       (pp_mem_ghost pp_machine_decl pp_machine_decl ?i)
293
       pp)
294
    fmt
295
    ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
296
     v)
297

  
298
let print_machine_ghost_simulation dependencies m fmt i instr =
299
  let name = m.mname.node_id in
300
  let self = mk_self m in
301
  let mem = mk_mem m in
302
  let prev_ghost fmt () = pp_mem_ghost' ~i fmt (name, mem, self) in
303
  let pred pp v = pp_and prev_ghost pp fmt ((), v) in
304
  print_machine_ghost_simulation_aux m
305
    (fun fmt -> function
306
       | MStateAssign (m, _) ->
307
         pred
308
           (pp_equal
309
              (pp_access (pp_access pp_var_decl))
310
              (pp_indirect (pp_access pp_var_decl)))
311
           ((mem, ("_reg", m)),
312
            (self, ("_reg", m)))
313
       | MStep ([i0], i, vl)
314
         when Basic_library.is_value_internal_fun
315
             (mk_val (Fun (i, vl)) i0.var_type)  ->
316
         prev_ghost fmt ()
317
       | MStep (_, i, _) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
318
         prev_ghost fmt ()
319
       | MStep ([_], i, _) when has_c_prototype i dependencies ->
320
         prev_ghost fmt ()
321
       | MStep (_, i, _)
322
       | MReset i ->
323
         begin try
324
             let n, _ = List.assoc i m.minstances in
325
             pred
326
               (pp_mem_ghost pp_access' pp_indirect')
327
               (node_name n, (mem, i), (self, i))
328
           with Not_found -> prev_ghost fmt ()
329
         end
330
       | _ -> prev_ghost fmt ())
331
    ~i:(i+1) fmt instr.instr_desc
332

  
333
let print_machine_ghost_struct fmt m =
334
  pp_spec (pp_ghost (print_machine_struct ~ghost:true)) fmt m
335

  
336
let print_machine_ghost_simulations dependencies fmt m =
337
  if not (fst (Machine_code_common.get_stateless_status m)) then
338
    let name = m.mname.node_id in
339
    let self = mk_self m in
340
    let mem = mk_mem m in
341
    fprintf fmt "%a@,%a@,%a%a"
342
      print_machine_ghost_struct m
343
      (print_machine_ghost_simulation_aux m pp_true ~i:0) ()
344
      (pp_print_list_i
345
        ~pp_epilogue:pp_print_cut
346
        ~pp_open_box:pp_open_vbox0
347
        (print_machine_ghost_simulation dependencies m))
348
      m.mstep.step_instrs
349
      (print_machine_ghost_simulation_aux m
350
         (pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self)
351

  
352
let pp_at pp_p fmt (p, l) =
353
  fprintf fmt "\\at(%a, %s)" pp_p p l
354

  
355
let label_pre = "Pre"
356

  
357
let pp_at_pre pp_p fmt p =
358
  pp_at pp_p fmt (p, label_pre)
359

  
360
module SrcMod = struct
361

  
362
  let pp_predicates dependencies fmt machines =
363
    fprintf fmt
364
      "%a%a"
365
      (pp_print_list
366
         ~pp_open_box:pp_open_vbox0
367
         ~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")
368
         print_machine_valid_predicate
369
         ~pp_epilogue:pp_print_cutcut) machines
370
      (pp_print_list
371
         ~pp_open_box:pp_open_vbox0
372
         ~pp_sep:pp_print_cutcut
373
         ~pp_prologue:(fun fmt () -> fprintf fmt
374
                          "/* ACSL ghost simulations */@,%a"
375
                          (pp_spec_line (pp_ghost pp_print_string))
376
                          "struct _arrow_mem_ghost {struct _arrow_reg _reg;};")
377
         (print_machine_ghost_simulations dependencies)
378
         ~pp_epilogue:pp_print_cutcut) machines
379

  
380
  let pp_reset_spec fmt self m =
381
    let name = m.mname.node_id in
382
    let mem = mk_mem m in
383
    pp_spec_cut (fun fmt () ->
384
        fprintf fmt
385
          "%a@,%a@,%a@,%a"
386
          (pp_requires pp_mem_valid') (name, self)
387
          (pp_requires (pp_separated self)) m.minstances
388
          (pp_assigns
389
             (pp_print_list
390
                ~pp_sep:pp_print_comma
391
                ~pp_nil:pp_nothing
392
                (pp_inst self))) m.minstances
393
          (pp_ensures
394
             (pp_forall
395
                pp_machine_decl
396
                (pp_implies
397
                   pp_mem_ghost'
398
                   pp_mem_init)))
399
          ((name, "mem_ghost", mem),
400
           ((name, mem, self), (name, mem))))
401
      fmt ()
402

  
403
  let pp_step_spec fmt self m =
404
    let name = m.mname.node_id in
405
    let mem_in = mk_mem_in m in
406
    let mem_out = mk_mem_out m in
407
    pp_spec_cut (fun fmt () ->
408
        fprintf fmt
409
          "%a@,%a@,%a@,%a@,%a"
410
          (pp_requires (pp_valid pp_var_decl)) m.mstep.step_outputs
411
          (pp_requires pp_mem_valid') (name, self)
412
          (pp_requires (pp_separated self)) m.minstances
413
          (pp_assigns
414
             (if m.mstep.step_outputs = [] && m.minstances = [] then
415
                pp_nothing
416
              else
417
                fun fmt () ->
418
                  fprintf fmt "@[<h>%a%a@]"
419
                    (pp_print_list
420
                       ~pp_sep:pp_print_comma
421
                       ~pp_epilogue:pp_print_comma
422
                       pp_ptr_decl) m.mstep.step_outputs
423
                    (pp_print_list
424
                       ~pp_sep:pp_print_comma
425
                       (pp_inst self)) m.minstances)) ()
426
          (pp_ensures
427
             (pp_forall
428
                (fun fmt () ->
429
                   fprintf fmt "%a, %s"
430
                     pp_machine_decl (name, "mem_ghost", mem_in)
431
                     mem_out)
432
                (pp_implies
433
                   (pp_at_pre pp_mem_ghost')
434
                   (pp_implies
435
                      pp_mem_ghost'
436
                      pp_mem_trans))))
437
          ((),
438
           ((name, mem_in, self),
439
            ((name, mem_out, self),
440
             (m, mem_in, mem_out)))))
441
      fmt ()
442

  
443
  let pp_step_instr_spec m self fmt (i, instr) =
444
    let name = m.mname.node_id in
445
    let mem_in = mk_mem_in m in
446
    let mem_out = mk_mem_out m in
447
    fprintf fmt "@,%a"
448
      (pp_spec
449
         (pp_assert
450
            (pp_forall
451
               (fun fmt () ->
452
                  fprintf fmt "%a, %s"
453
                    pp_machine_decl (name, "mem_ghost", mem_in)
454
                    mem_out)
455
               (pp_implies
456
                  (pp_at_pre pp_mem_ghost')
457
                  (pp_implies
458
                     (pp_mem_ghost' ~i:(i+1))
459
                     (pp_mem_trans ~i:(i+1)))))))
460
      ((),
461
       ((name, mem_in, self),
462
        ((name, mem_out, self),
463
         (m, mem_in, mem_out))))
464

  
465
end
466

  
141 467
(**************************************************************************)
142 468
(*                              MAKEFILE                                  *)
143 469
(**************************************************************************)
144 470

  
145
let makefile_targets fmt basename _nodename dependencies =
146
  fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
147
  (* EACSL version of library file . c *)
148
  fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
149
  fprintf fmt 
150
    "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@." 
151
    basename basename; 
152
  fprintf fmt "@.";
153
  fprintf fmt "@.";
154

  
155
  (* EACSL version of library file . c + main .c  *)
156
  fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;
157
  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@." 
158
    basename basename basename; 
159
  (* Ugly hack to deal with eacsl bugs *)
160
  fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;
161
  fprintf fmt "@.";
162
  fprintf fmt "@.";
163

  
164
  (* EACSL version of binary *)
165
  fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
166
  fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)
167
  C_backend_makefile.fprintf_dependencies fmt dependencies; 
168
  fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@." 
169
    basename 
170
    (Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name)) 
171
    (C_backend_makefile.compiled_dependencies dependencies)
172
    ("${FRAMACEACSL}/e_acsl.c " 
173
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c " 
174
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
175
    basename 
176
    (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib)) 
177
    (C_backend_makefile.lib_dependencies dependencies)
178
  ;
179
  fprintf fmt "@.";
180

  
181
module MakefileMod =
182
struct
183
  let other_targets = makefile_targets
184
    
471
module MakefileMod = struct
472

  
473
  let other_targets fmt basename _nodename dependencies =
474
    fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
475
    (* EACSL version of library file . c *)
476
    fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
477
    fprintf fmt
478
      "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@."
479
      basename basename;
480
    fprintf fmt "@.";
481
    fprintf fmt "@.";
482

  
483
    (* EACSL version of library file . c + main .c  *)
484
    fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;
485
    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@."
486
      basename basename basename;
487
    (* Ugly hack to deal with eacsl bugs *)
488
    fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;
489
    fprintf fmt "@.";
490
    fprintf fmt "@.";
491

  
492
    (* EACSL version of binary *)
493
    fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
494
    fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)
495
    C_backend_makefile.fprintf_dependencies fmt dependencies;
496
    fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@."
497
      basename
498
      (Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name))
499
      (C_backend_makefile.compiled_dependencies dependencies)
500
      ("${FRAMACEACSL}/e_acsl.c "
501
       ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
502
       ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
503
      basename
504
      (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib))
505
      (C_backend_makefile.lib_dependencies dependencies)
506
    ;
507
    fprintf fmt "@."
508

  
185 509
end
186 510

  
187 511
(* Local Variables: *)
src/backends/C/c_backend_src.ml
17 17
open C_backend_common
18 18

  
19 19
module type MODIFIERS_SRC = sig
20
  val pp_predicates: dep_t list -> formatter -> machine_t list -> unit
21
  val pp_reset_spec: formatter -> ident -> machine_t -> unit
22
  val pp_step_spec: formatter -> ident -> machine_t -> unit
23
  val pp_step_instr_spec: machine_t -> ident -> formatter -> (int * instr_t) -> unit
20 24
end
21 25

  
22 26
module EmptyMod = struct
27
  let pp_predicates _ _ _ = ()
28
  let pp_reset_spec _ _ _ = ()
29
  let pp_step_spec _ _ _ = ()
30
  let pp_step_instr_spec _ _ _ _ = ()
23 31
end
24 32

  
25 33
module Main = functor (Mod: MODIFIERS_SRC) -> struct
......
274 282
  let pp_machine_clear =
275 283
    pp_machine_ pp_machine_clear_name "pp_machine_clear"
276 284

  
277
  let has_c_prototype funname dependencies =
278
    (* We select the last imported node with the name funname.
279
       The order of evaluation of dependencies should be
280
       compatible with overloading. (Not checked yet) *)
281
    let imported_node_opt =
282
      List.fold_left
283
        (fun res dep ->
284
           match res with
285
           | Some _ -> res
286
           | None ->
287
             let decls = dep.content in
288
             let matched = fun t -> match t.top_decl_desc with
289
               | ImportedNode nd -> nd.nodei_id = funname
290
               | _ -> false
291
             in
292
             if List.exists matched decls then
293
               match (List.find matched decls).top_decl_desc with
294
               | ImportedNode nd -> Some nd
295
               | _ -> assert false
296
             else
297
               None) None dependencies in
298
    match imported_node_opt with
299
    | None -> false
300
    | Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)
301

  
302 285
  let pp_call m self pp_read pp_write fmt i
303 286
      (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
304 287
    try (* stateful node instance *)
......
406 389
      (pp_print_list ~pp_open_box:pp_open_vbox0
407 390
         (pp_machine_instr dependencies m self)) h
408 391

  
392
  let pp_machine_nospec_instr dependencies m self fmt _i instr =
393
    pp_machine_instr dependencies m self fmt instr
394

  
395
  let pp_machine_step_instr dependencies m self fmt i instr =
396
    fprintf fmt "%a%a%a"
397
      (if i = 0 then
398
         (fun fmt () -> Mod.pp_step_instr_spec m self fmt (i-1, instr))
399
       else
400
         pp_print_nothing) ()
401
      (pp_machine_instr dependencies m self) instr
402
      (Mod.pp_step_instr_spec m self) (i, instr)
409 403

  
410 404
  (********************************************************************************************)
411 405
  (*                         C file Printing functions                                        *)
......
474 468
       _alloc = (%a *) malloc(sizeof(%a));@,\
475 469
       assert(_alloc);@,\
476 470
       %a%areturn _alloc;"
477
      pp_machine_memtype_name m.mname.node_id
478
      pp_machine_memtype_name m.mname.node_id
479
      pp_machine_memtype_name m.mname.node_id
471
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
472
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
473
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
480 474
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m)
481 475
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances
482 476

  
......
524 518

  
525 519
  let pp_print_function
526 520
      ~pp_prototype ~prototype
521
      ?(pp_spec=pp_print_nothing)
527 522
      ?(pp_local=pp_print_nothing) ?(base_locals=[])
528 523
      ?(pp_array_mem=pp_print_nothing) ?(array_mems=[])
529 524
      ?(pp_init_mpfr_local=pp_print_nothing)
......
531 526
      ?(mpfr_locals=[])
532 527
      ?(pp_check=pp_print_nothing) ?(checks=[])
533 528
      ?(pp_extra=pp_print_nothing)
534
      ?(pp_instr=pp_print_nothing) ?(instrs=[])
529
      ?(pp_instr=fun fmt _ _ -> pp_print_nothing fmt ()) ?(instrs=[])
535 530
      fmt =
536 531
    fprintf fmt
537
      "@[<v 2>%a {@,\
532
      "%a@[<v 2>%a {@,\
538 533
       %a%a\
539 534
       %a%a%a%a%areturn;@]@,\
540 535
       }"
536
      pp_spec ()
541 537
      pp_prototype prototype
542 538
      (* locals *)
543 539
      (pp_print_list
......
560 556
      (* check assertions *)
561 557
      (pp_print_list pp_check) checks
562 558
      (* instrs *)
563
      (pp_print_list
559
      (pp_print_list_i
564 560
         ~pp_open_box:pp_open_vbox0
565 561
         ~pp_epilogue:pp_print_cut
566 562
         pp_instr) instrs
......
593 589
        ~mpfr_locals:m.mstep.step_locals
594 590
        ~pp_check:(pp_c_check m self)
595 591
        ~checks:m.mstep.step_checks
596
        ~pp_instr:(pp_machine_instr dependencies m self)
592
        ~pp_instr:(pp_machine_nospec_instr dependencies m self)
597 593
        ~instrs:m.mstep.step_instrs
598 594
        fmt
599 595
    else
......
615 611
        ~mpfr_locals:m.mstep.step_locals
616 612
        ~pp_check:(pp_c_check m self)
617 613
        ~checks:m.mstep.step_checks
618
        ~pp_instr:(pp_machine_instr dependencies m self)
614
        ~pp_instr:(pp_machine_nospec_instr dependencies m self)
619 615
        ~instrs:m.mstep.step_instrs
620 616
        fmt
621 617

  
622 618
  let print_reset_code dependencies self fmt m =
623 619
    pp_print_function
620
      ~pp_spec:(fun fmt () -> Mod.pp_reset_spec fmt self m)
624 621
      ~pp_prototype:(print_reset_prototype self)
625 622
      ~prototype:(m.mname.node_id, m.mstatic)
626 623
      ~pp_local:(pp_c_decl_local_var m)
627 624
      ~base_locals:(const_locals m)
628
      ~pp_instr:(pp_machine_instr dependencies m self)
625
      ~pp_instr:(pp_machine_nospec_instr dependencies m self)
629 626
      ~instrs:m.minit
630 627
      fmt
631 628

  
......
670 667
    then
671 668
      (* C99 code *)
672 669
      pp_print_function
670
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m)
673 671
        ~pp_prototype:(print_step_prototype self)
674 672
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
675 673
        ~pp_local:(pp_c_decl_local_var m)
......
681 679
        ~mpfr_locals:m.mstep.step_locals
682 680
        ~pp_check:(pp_c_check m self)
683 681
        ~checks:m.mstep.step_checks
684
        ~pp_instr:(pp_machine_instr dependencies m self)
682
        ~pp_instr:(pp_machine_step_instr dependencies m self)
685 683
        ~instrs:m.mstep.step_instrs
686 684
        fmt
687 685
    else
......
692 690
          let id, _, _ = call_of_expr e in
693 691
          mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
694 692
      pp_print_function
693
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m)
695 694
        ~pp_prototype:(print_step_prototype self)
696 695
        ~prototype:(m.mname.node_id,
697 696
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
......
703 702
        ~mpfr_locals:m.mstep.step_locals
704 703
        ~pp_check:(pp_c_check m self)
705 704
        ~checks:m.mstep.step_checks
706
        ~pp_instr:(pp_machine_instr dependencies m self)
705
        ~pp_instr:(pp_machine_step_instr dependencies m self)
707 706
        ~instrs:m.mstep.step_instrs
708 707
        fmt
709 708

  
......
834 833
        (* Clear function *)
835 834
        (print_clear_code self) m
836 835

  
837

  
838 836
  (* TODO: ACSL
839 837
     - a contract machine shall not be directly printed in the C source
840 838
     - but a regular machine associated to a contract machine shall integrate
......
849 847
      print_stateless_code dependencies fmt m
850 848
    else
851 849
      let self = mk_self m in
852
      fprintf fmt "@[<v>%a%a@,%a%a@]"
850
      fprintf fmt "@[<v>%a%a@,@,%a%a@]"
853 851
        print_alloc_function m
854 852
        (* Reset function *)
855 853
        (print_reset_code dependencies self) m
......
889 887
       %a\
890 888
       %a\
891 889
       %a\
890
       %a\
892 891
       @]@."
893 892
      print_import_standard ()
894 893
      print_import_prototype
......
967 966
         print_machine_struct
968 967
         ~pp_epilogue:pp_print_cutcut) machines
969 968

  
969
      (* Print the spec predicates *)
970
      (Mod.pp_predicates dependencies) machines
971

  
970 972
      (* Print nodes one by one (in the previous order) *)
971 973
      (pp_print_list
972 974
         ~pp_open_box:pp_open_vbox0
src/lusic.ml
10 10
(*                                                                  *)
11 11
(********************************************************************)
12 12

  
13
open Format 
14 13
open Lustre_types
15 14

  
16 15
(********************************************************************************************)
src/utils/utils.ml
290 290
      ?(pp_prologue=pp_print_nothing) ?(pp_epilogue=pp_print_nothing)
291 291
      ?(pp_op=pp_print_nothing) ?(pp_cl=pp_print_nothing)
292 292
      ?(pp_open_box=fun fmt () -> pp_open_box fmt 0)
293
      ?(pp_eol=pp_print_nothing) ?pp_sep pp_v fmt l =
293
      ?(pp_eol=pp_print_nothing)
294
      ?(pp_nil=pp_print_nothing)
295
      ?pp_sep pp_v fmt l =
294 296
    fprintf fmt "%a%a%a%a%a@]%a%a"
295 297
      (fun fmt l -> if l <> [] then pp_prologue fmt ()) l
296 298
      pp_op ()
297 299
      pp_open_box ()
298
      (pp_print_list ?pp_sep pp_v) l
300
      (fun fmt () ->
301
         if l = [] then pp_nil fmt () else pp_print_list ?pp_sep pp_v fmt l) ()
299 302
      (fun fmt l -> if l <> [] then pp_eol fmt ()) l
300 303
      pp_cl ()
301 304
      (fun fmt l -> if l <> [] then pp_epilogue fmt ()) l

Also available in: Unified diff