Project

General

Profile

Download (31.8 KB) Statistics
| Branch: | Tag: | Revision:
1
open Format
2
open LustreSpec
3
open Machine_code
4
open C_backend_common
5
open Utils
6

    
7

    
8
module type SPECARG = 
9
sig
10
  val prog : program 
11
  val machines : machine_t list
12
end
13
  
14
  (**************************************************************************)
15
  (*                              SPEC DATATYPES                            *)
16
  (**************************************************************************)
17
    
18
    
19
  type eexpr_minimachine_t = {
20
  muid: tag;
21
  mquantifiers: (quantifier_type * var_decl list) list;
22
  mmmemory: var_decl list;
23
  mmcalls: (ident * static_call) list;     (* map from stateful/stateless instance to node, 
24
					      no internals *)
25
  mminstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *)
26
  mminit: instr_t list;
27
  mmstep_logic: step_t;  
28
  mmstep_effects: step_t;  
29
  (* mmlogic: step_t;   *)
30
}
31

    
32
type spec_machine_t = {
33
  m_requires: eexpr_minimachine_t list;
34
  m_ensures: eexpr_minimachine_t list;
35
  m_behaviors: (string * eexpr_minimachine_t list * eexpr_minimachine_t list) list;
36
}
37

    
38

    
39
let machine_from_minimachine_effects m mm =
40
{
41
  mname = m.mname;
42
  mmemory = mm.mmmemory;
43
  mcalls = mm.mmcalls;
44
  minstances = mm.mminstances;
45
  minit = []; (* ??? *)
46
  mstatic = [] ; (* ??? *)
47
  mstep = mm.mmstep_effects;
48
  mspec = None;
49
  mannot = [];
50
}
51

    
52
let machine_from_minimachine_logics m mm =
53
{
54
  mname = m.mname;
55
  mmemory = mm.mmmemory;
56
  mcalls = mm.mmcalls;
57
  minstances = mm.mminstances;
58
  minit = []; (* ??? *)
59
  mstatic = [] ; (* ??? *)
60
  mstep = mm.mmstep_logic;
61
  mspec = None;
62
  mannot = [];
63
}
64

    
65
(**************************************************************************)
66
(*                       DATATYPES PRINTERS                               *)
67
(**************************************************************************)
68

    
69

    
70

    
71
let pp_acsl_type var fmt t =
72
  let rec aux t pp_suffix =
73
  match (Types.repr t).Types.tdesc with
74
  | Types.Tclock t'       -> aux t' pp_suffix
75
  | Types.Tbool           -> fprintf fmt "boolean %s%a" var pp_suffix ()
76
  | Types.Treal           -> fprintf fmt "real %s%a" var pp_suffix ()
77
  | Types.Tint            -> fprintf fmt "integer %s%a" var pp_suffix ()
78
  | Types.Tarray (d, t')  ->
79
    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
80
    aux t' pp_suffix'
81
  (* | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix *)
82
  (* | Types.Tconst ty       -> fprintf fmt "%s %s" ty var *)
83
  (* | Types.Tarrow (_, _)   -> fprintf fmt "void (\*%s)()" var *)
84
  | _                     -> 
85
    (eprintf "internal error: pp_acsl_type %a@." Types.print_ty t; assert false)
86
  in aux t (fun fmt () -> ())
87

    
88
let pp_acsl_var_decl fmt id =
89
  pp_acsl_type id.var_id fmt id.var_type
90

    
91

    
92
let pp_quantifiers fmt (q, vars) =
93
  let pp_var fmt id = 
94
    fprintf fmt "%s: %a" id.var_id Types.print_ty id.var_type
95
  in
96
  match q with
97
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
98
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
99

    
100
(*
101
let pp_eexpr fmt ee =
102
  Format.fprintf fmt 
103
    "%a%t @[<v 2>mem      : %a@;instances: %a@;init     : %a@;logic step     :@;  @[<v 2>%a@]@;effects step     :@;  @[<v 2>%a@]@;@]@;"
104
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) ee.mquantifiers
105
    (fun fmt -> match ee.mquantifiers with [] -> () | _ -> Format.fprintf fmt ";")
106
    (Utils.fprintf_list ~sep:", " Printers.pp_var) ee.mmmemory
107
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) ee.mminstances
108
    (Utils.fprintf_list ~sep:"@ " pp_instr) ee.mminit
109
    pp_step ee.mmstep_logic
110
    pp_step ee.mmstep_effects
111

    
112

    
113
let pp_spec fmt spec =
114
  Format.fprintf fmt "@[<hov 2>(*@@ ";
115
  Utils.fprintf_list ~sep:"@;@@ " (fun fmt r -> Format.fprintf fmt "requires %a;" pp_eexpr r) fmt spec.m_requires;
116
  Utils.fprintf_list ~sep:"@;@@ " (fun fmt r -> Format.fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.m_ensures;
117
  Utils.fprintf_list ~sep:"@;" (fun fmt (name, assumes, ensures) -> 
118
    Format.fprintf fmt "behavior %s:@[@ %a@ %a@]" 
119
      name
120
      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> Format.fprintf fmt "assumes %a;" pp_eexpr r)) assumes
121
      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> Format.fprintf fmt "ensures %a;" pp_eexpr r)) ensures
122
  ) fmt spec.m_behaviors;
123
  Format.fprintf fmt "@]*)";
124
  ()
125
*)
126

    
127

    
128
(**************************************************************************)
129
(*                            CONVERTER                                   *)
130
(**************************************************************************)
131
(* The eexpr shoud have been normalized, ie. its eexpr_normalized field updated
132
   We add a new boolean output var and bound it to the main expression
133
   characterizing the eexpr.   
134
*)
135

    
136
let save_var v =
137
  { v with var_id = v.var_id^"_save" }
138

    
139
let rec postTransformLogicValue x = match x with
140
  | StateVar v -> StateVar (save_var v)
141
  | Fun (i, vl) -> Fun (i, List.map postTransformLogicValue vl)
142
  | Array vl -> Array (List.map postTransformLogicValue vl)
143
  | Access (x, y) -> Access (postTransformLogicValue x, postTransformLogicValue y)
144
  | Power (x, y) -> Power (postTransformLogicValue x, postTransformLogicValue y)
145
  | x -> x
146

    
147
let rec postTransformLogic x = List.map (function
148
    | MLocalAssign (x, y) -> MLocalAssign (x, postTransformLogicValue y)
149
    | MStateAssign (x, y) -> MStateAssign (x, postTransformLogicValue y)
150
    | MStep (x, y, z) -> MStep (x, y, List.map postTransformLogicValue z)
151
    | MBranch (x, y) -> MBranch (postTransformLogicValue x, List.map (function (x, y)-> (x, postTransformLogic y)) y)
152
    | MReset x -> MReset x
153
    ) x
154

    
155
let rec postTransformSide = function
156
    | MStateAssign (i, v)::q -> (MStateAssign (save_var i, StateVar i))::(MStateAssign (i, v))::(postTransformSide q)
157
    | t::q -> t::(postTransformSide q)
158
    | [] -> []
159

    
160
let rec postTranformMemory = function
161
    | t::q -> t::(save_var t)::(postTranformMemory q)
162
    | [] -> []
163

    
164
let translate_eexpr nd eexpr =
165
  (* Format.eprintf "Translating eexpr: %a" Printers.pp_eexpr eexpr; *)
166
  let output_var, eqs, locals = 
167
    match eexpr.eexpr_normalized with None -> assert false | Some x -> x 
168
  in 
169
  (* both inputs and outputs are considered here as inputs for the specification *) 
170
  let inputs = nd.node_inputs @ nd.node_outputs in
171
  let inputs_quantifiers = inputs @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in 
172
  
173
  let eexpr_local_vars = output_var :: locals @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in
174
  let visible_vars = eexpr_local_vars @ inputs in
175
  
176
  let sort_eqs inputs eqs = 
177
    let eqs_logic, new_locals_logic, sch_logic = Scheduling.schedule_eqs inputs visible_vars eqs in
178
    (* Format.eprintf "sch: [%a]@;new locals: [%a]@;locals:[%a]@.eexpr local vars: [%a]@.@?"  *)
179
    (*   (Utils.fprintf_list ~sep:", " Format.pp_print_string) sch_logic *)
180
    (*   (Utils.fprintf_list ~sep:", " Printers.pp_var) new_locals_logic *)
181
    (*   (Utils.fprintf_list ~sep:", " Printers.pp_var) locals *)
182
    (*   (Utils.fprintf_list ~sep:", " Printers.pp_var) eexpr_local_vars;  *)
183
    let locals = eexpr_local_vars @ new_locals_logic @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in
184
    let sorted_eqs_rev_logic, remainder_logic = 
185
      List.fold_left 
186
	(fun (accu, eqs_remainder) v -> 
187
	  if List.exists (fun eq -> List.mem v eq.eq_lhs) accu
188
	  then (* The variable was already handled by a previous selected eq. 
189
		  Typically it is part of a tuple *)
190
	    ((* Format.eprintf "Case 1 for variable %s@." v; *)
191
	     (accu, eqs_remainder)
192
	    )
193
	  else if List.exists (fun vdecl -> vdecl.var_id = v) locals || output_var.var_id = v
194
	  then ((* Select the eq associated to v. *) 
195
	    (* Format.eprintf "Case 2 for variable %s@." v; *)
196
	    let eq_v, remainder = find_eq v eqs_remainder in
197
	    eq_v::accu, remainder
198
	  )
199
	  else ((* else it is a constant value, checked during typing phase *)
200
	    (* Format.eprintf "Case 3 for variable %s@." v; *)
201
	    accu, eqs_remainder
202
	  )
203
	) 
204
	([], eqs_logic) 
205
	sch_logic 
206
    in
207
    if List.length remainder_logic > 0 then (
208
      Format.eprintf "Spec equations not used are@.%a@.Full equation set is:@.%a@.@?"
209
	Printers.pp_node_eqs remainder_logic
210
	Printers.pp_node_eqs eqs_logic;
211
      assert false );
212
    List.rev sorted_eqs_rev_logic, locals  
213
  in
214

    
215
  
216
  (* Generating logic definition instructions *)
217
  let sorted_eqs, locals = sort_eqs inputs_quantifiers eqs in
218

    
219
  let init_args = 
220
    VDSet.empty, 
221
    [], 
222
    Utils.IMap.empty, 
223
    List.fold_right (fun l -> VDSet.add l) locals VDSet.empty,
224
    [] 
225
  in
226

    
227
  let m, init, j, locals, s_logic = 
228
    translate_eqs 
229
      nd
230
      true (* keep_ite *)  
231
      eexpr_local_vars
232
      init_args
233
      (sorted_eqs) 
234
  in
235

    
236
  (* We remove side effects *)
237
  let s_logic = List.filter (fun i -> match i with MStateAssign _ -> false | _ -> true) s_logic in 
238
  (* and put the output var as the last instr *)
239
  let s_logic =
240
    let output_assign, others = 
241
      List.partition 
242
	(fun i -> match i with | MStep([v], _, _) | MLocalAssign(v,_) -> v.var_id = output_var.var_id | _ -> false)
243
	s_logic 
244
    in
245
    (* Format.eprintf "output instr: @.%a@.others:@.%a@." *)
246
    (*   (Utils.fprintf_list ~sep:"@." pp_instr) output_assign *)
247
    (*   (Utils.fprintf_list ~sep:"@." pp_instr) others; *)
248
    others @ output_assign
249
  in
250
  let _,_,_,_, s_side_effects = 
251
    translate_eqs nd true (*TODO: explose ite *)  eexpr_local_vars init_args (sorted_eqs) 
252
  in
253
  let rec filter_side_effects instrs =
254
    List.fold_right (
255
      fun i accu ->
256
	match i with
257
      | MStep([v], _, _) 
258
      | MLocalAssign(v,_) -> 
259
	if v.var_id <> output_var.var_id then
260
	  i::accu
261
	else
262
	  accu
263
      | MBranch (g, cases) -> 
264
	let filtered_cases = 
265
	  List.map (fun (l, l_instrs) -> l, filter_side_effects l_instrs) cases in
266
	MBranch(g, filtered_cases) :: accu
267
      | _ -> i::accu
268
	  
269
    ) instrs []
270
  in
271

    
272
  let s_side_effects = filter_side_effects s_side_effects in 
273
  
274
  {
275
    muid = eexpr.eexpr_tag;
276
    mquantifiers = eexpr.eexpr_quantifiers;
277
    mmmemory = postTranformMemory (VDSet.elements m);
278
    mmcalls = []; (* no calls *)
279
    mminstances = []; (* no calls *)
280
    mminit = init;
281
    mmstep_logic = {
282
      step_inputs = inputs;
283
      step_outputs = [output_var];
284
      step_locals = VDSet.elements (VDSet.remove output_var (VDSet.diff locals m));
285
      step_checks = [] (* Not handled yet *);
286
      step_instrs = (
287
	(* special treatment depending on the active backend. For horn backend,
288
	   common branches are not merged while they are in C or Java
289
	   backends. *)
290
	match !Options.output with
291
	| "horn" -> s_logic
292
	| "C" | "java" | _ -> (*TODO: check that this is correct to remove : join_guards_list*) (postTransformLogic s_logic)
293
      );
294
      step_asserts = [];
295
    };
296
    mmstep_effects = {
297
      step_inputs = inputs; (* contains nd.node_inputs + nd.node_outputs *)
298
      step_outputs = nd.node_outputs; (* used by the printer to print correctly the names *)
299
      step_locals = VDSet.elements (VDSet.remove output_var (VDSet.diff locals m));
300
      step_checks = [] (* Not handled yet *);
301
      step_instrs = (
302
	(* special treatment depending on the active backend. For horn backend,
303
	   common branches are not merged while they are in C or Java
304
	   backends. *)
305
	match !Options.output with
306
	| "horn" -> s_side_effects
307
	| "C" | "java" | _ -> (*TODO: check that this is correct to remove : join_guards_list*) (postTransformSide s_side_effects)
308
      );
309
      step_asserts = [];
310
    }
311
  }    
312

    
313
let translate_spec nd spec = 
314
  (* Each eexpr of the spec is expressed as a minimachine: 
315
     instrs (to update memory and set local vars) 
316
     + expr (to compute the output
317
     + memory defs 
318
     + instances (for callee nodes)
319
  *)
320
  let transl = List.map (translate_eexpr nd) in
321
  {
322
    m_requires = transl spec.requires;
323
    m_ensures = transl spec.ensures;
324
    m_behaviors =
325
      List.map
326
	(fun (beh_id, req, ens, _) -> beh_id, transl req, transl ens) 
327
	spec.behaviors
328
  }
329
    
330

    
331
(*
332

    
333
mspec = Utils.option_map (translate_spec nd) nd.node_spec;
334
    mannot = List.flatten (
335
      List.map (fun ann -> List.map (fun (kwd, eexpr) -> kwd, (translate_eexpr nd eexpr)) ann.annots) nd.node_annot);
336
*)
337

    
338

    
339
(**************************************************************************)
340
(*                              HEADER                                    *)
341
(**************************************************************************)
342
    
343
  (* Print basic library function as ACSL functions *)
344
  let basic_lib_pp_acsl i get_val_type pp_val fmt vl =
345
    match i, vl with
346
    | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 
347
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
348
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
349
    | "impl", [v1; v2] -> Format.fprintf fmt "((!%a) ||  %a)" pp_val v1 pp_val v2 
350
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
351
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
352
    | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
353
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2
354
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
355
    | _ -> raise (Failure ("No ACSL printer for function " ^ i))
356
      
357

    
358
  let rec pp_acsl_val ?(is_lhs=false) self pp_var fmt v =
359
    match v with
360
    | Cst c         -> pp_c_const fmt c
361
    | Array _      
362
    | Access _       -> assert false (* no arrays *)
363
    | Power (v, n)  -> assert false
364
    | LocalVar v    -> pp_var fmt v
365
    | StateVar v    ->     
366
      if Types.is_array_type v.var_type
367
      then assert false
368
      else fprintf fmt "%s%s_reg.%s" self 
369
     (if !Options.no_pointer then "." else "->") v.var_id
370
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (basic_lib_pp_acsl n Machine_code.get_val_type (pp_acsl_val self pp_var)) vl
371
      
372

    
373
  let rec pp_eexpr_logic_instr m eem fmt instr =
374
    let self = mk_self m in
375
    let conv_m =  machine_from_minimachine_logics m eem in
376
    match instr with 
377
    | MReset i -> assert false (* should not happen, calls were inlined *)
378
    | MLocalAssign (i,v) -> (
379
      match conv_m.mstep.step_outputs with 
380
      | [o] -> if i = o then
381
	  fprintf fmt "%a;" (pp_acsl_val self (pp_c_var_read conv_m)) v
382
	else
383
	  fprintf fmt "\\let %a = %a;" 
384
	    (pp_c_var_read conv_m (* TODO no variable shold be treated as output *)) i
385
	    (pp_acsl_val self (pp_c_var_read conv_m)) v
386

    
387
      | _ -> 
388
	assert false (* should not happen: only a single output *)
389
    )
390
    | MStateAssign (i,v) -> 
391
      assert false (* should not happen, no side effects in logical predicates *)
392
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
393
      pp_eexpr_logic_instr m eem fmt (MLocalAssign (i0, Fun (i, vl)))
394
  | MStep ([i0], "ite", vl) ->
395
    pp_eexpr_logic_instr m eem fmt (MLocalAssign (i0, Fun ("ite", vl)))
396
  | MStep (il, i, vl) ->
397
    Format.eprintf "Illegal function call %s@.%a@.@?" i pp_instr instr; 
398
    assert false (* should not happen, calls were inlined *)
399
  | MBranch (g,hl) -> assert false (* should not happen. Oder ??? TODO *)
400
    
401

    
402
let pp_logic_eexpr m fmt ee =
403
  fprintf fmt "%a%t%a"
404
    (Utils.fprintf_list ~sep:"@ " pp_quantifiers) ee.mquantifiers
405
    (Utils.pp_final_char_if_non_empty " " ee.mquantifiers) 
406
    (Utils.fprintf_list ~sep:"@;" 
407
       (pp_eexpr_logic_instr m ee)) ee.mmstep_logic.step_instrs
408
    
409

    
410
let pp_acsl_spec_logics stateless m fmt spec = 
411
  let self = mk_self m in
412
  let pp_expr_def fmt ee =
413
    match ee.mmstep_logic.step_instrs with
414
    | [MStep([o], i, vl)] -> () (* We do nothing, the expression is simple and 
415
				   was introduced directly in the contract *)
416
    | _ -> ((* We define a new ACSL predicate *)
417
      fprintf fmt "/*@@ @[<v 3>predicate spec_%i(%a%t) =@;%a@]@;*/@." 
418
	ee.muid   
419
	(Utils.fprintf_list ~sep:", " pp_acsl_var_decl) ee.mmstep_logic.step_inputs
420
  (fun fmt -> if stateless then fprintf fmt "" else fprintf fmt "%t%a %s%s"
421
  (Utils.pp_final_char_if_non_empty ", " ee.mmstep_logic.step_inputs)
422
	pp_machine_memtype_name m.mname.node_id
423
  (if !Options.no_pointer then "" else "*")
424
	self)
425
	(pp_logic_eexpr m) ee
426
    )
427

    
428
  in
429
  List.iter (pp_expr_def fmt) 
430
    (spec.m_requires@
431
       spec.m_ensures@
432
       (List.fold_left 
433
	  (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
434
	  [] spec.m_behaviors)
435
    )
436

    
437
(* Access to the value of a variable:
438
   - if it's not a scalar output, then its name is enough
439
   - otherwise, dereference it (it has been declared as a pointer,
440
     despite its scalar Lustre type)
441
   - moreover, cast arrays variables into their original array type.
442
*)
443
let pp_acsl_var_read suffix outputs fmt id =
444
  if Types.is_array_type id.var_type
445
  then
446
    assert false (* no array *)
447
  else (
448
    (if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
449
    then fprintf fmt "(*%s%s" id.var_id suffix
450
    else fprintf fmt "(%s%s" id.var_id suffix);
451
      match (Types.repr id.var_type).Types.tdesc with
452
      | Types.Tbool           -> fprintf fmt "?\\true:\\false)"
453
      | _ -> fprintf fmt ")"
454
  )
455

    
456
    
457
let pp_requires_mem stateless machines fmt m =
458
  let self = mk_self m in
459
  List.iter (fun v -> fprintf fmt "requires \\valid(%s);@;" v.var_id) m.mstep.step_outputs;
460
  let mems = Machine_code.get_mems m machines in
461
  (if not !Options.no_pointer then
462
    List.iter (fun prefix -> fprintf fmt "requires \\valid(%s%a);@;" self
463
      (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix
464
    )
465
      (Machine_code.get_instances m machines)
466
  );
467
  if not stateless then fprintf fmt "requires \\valid(%s);@;" self;
468
  if List.length mems + List.length m.mstep.step_outputs > 1 then
469
    fprintf fmt "requires \\separated(@[<hov>%a%t%a@]);@;" 
470
      (Utils.fprintf_list ~sep:",@ " 
471
	      (fun fmt v -> pp_print_string fmt v.var_id))
472
      m.mstep.step_outputs 
473
      (Utils.pp_final_char_if_non_empty ",@ " mems)
474
      (if !Options.no_pointer then
475
        fun fmt x -> fprintf fmt "%s" (if stateless then "" else self) (*maybe we want to add more pointers here like arrays *)
476
      else
477
        Utils.fprintf_list ~sep:",@ " (fun fmt (prefix, var) -> fprintf fmt "&%s%a->_reg.%s"
478
	        self 
479
	        (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix
480
	        var.var_id))
481
      mems
482

    
483
let pp_assigns more stateless machines fmt m =
484
  let self = mk_self m in
485
  let mems = Machine_code.get_mems m machines in
486
  fprintf fmt "assigns @[<hov>%a%a%t%a@];@;"
487
    (Utils.fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "*%s" v.var_id))
488
    m.mstep.step_outputs
489
    (if !Options.no_pointer then
490
        fun fmt mems -> fprintf fmt "%s" (if stateless then "" else (", *"^self)) (*maybe we want to keep some memory like array *)
491
     else Utils.fprintf_list ~sep:",@ "
492
       (fun fmt (prefix, var) -> fprintf fmt "%t%s%a->_reg.%s"
493
         (Utils.pp_final_char_if_non_empty ",@ " mems)
494
         self
495
         (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix
496
         var.var_id)
497
    )
498
    mems
499
    (Utils.pp_final_char_if_non_empty ",@ " more)
500
    (Utils.fprintf_list ~sep:",@ " (fun fmt v -> v fmt))
501
    more
502

    
503

    
504
let pp_acsl_mem_valid stateless pre post machines fmt m =
505
  fprintf fmt "@[<v 2>/*@@ ";
506
  pp_requires_mem stateless machines fmt m;
507
  pre fmt;
508
  post fmt;
509
  pp_assigns [] stateless machines fmt m;
510
  fprintf fmt "@]*/@.";
511
  ()
512

    
513
(* Seems to be a simplification of pp_assign (in c_backend_src *)
514
let pp_expr_rhs m pp_var fmt var_type value =
515
  let self = mk_self m in
516
  let depth = C_backend_src.expansion_depth value in
517
(*eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*)
518
  let loop_vars = C_backend_src.mk_loop_variables m var_type depth in
519
  let reordered_loop_vars = C_backend_src.reorder_loop_variables loop_vars in
520
  let rec aux fmt vars =
521
    match vars with
522
    | [] ->
523
      fprintf fmt "%a;" 
524
	(C_backend_src.pp_value_suffix self loop_vars pp_var) value
525
    | _ -> assert false
526
  in
527
  begin
528
    reset_loop_counter ();
529
    (*reset_addr_counter ();*)
530
    aux fmt reordered_loop_vars
531
  end
532

    
533
let pp_acsl_spec_contracts stateless pre post machines m outputs fmt spec = 
534
  let self = mk_self m in
535
    (* let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in *)
536
  let pp_eexpr_expr fmt ee = 
537
      (* If the eexpr contains a single definition we use it directly. Otherwise,
538
	 we rely on an external predicate *)
539
    let conv_m =  machine_from_minimachine_logics m ee in
540
    match ee.mmstep_logic.step_instrs with
541
    | [MStep([o], i, vl)] -> 
542
      fprintf fmt "%a %t"
543
	(Utils.fprintf_list ~sep:" " pp_quantifiers) ee.mquantifiers
544
	(fun fmt ->
545
	  let value = Fun (i, vl) in
546
       	  pp_expr_rhs
547
	    conv_m
548
	    (pp_c_var_read conv_m) 
549
	    fmt
550
	    o.var_type value 
551
	)
552
    | _ -> fprintf fmt "spec_%i(%a%t);" 
553
      ee.muid   
554
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read "" outputs)) ee.mmstep_logic.step_inputs
555
      (fun fmt -> if stateless then fprintf fmt "" else fprintf fmt ", %s%s" (if !Options.no_pointer then "*" else "") self)
556
  in
557
  fprintf fmt "@[<v 2>/*@@ ";
558
  (* Valid pointers *)
559
  pp_requires_mem stateless machines fmt m;
560
  
561
  (* Spec requires *)
562
  Utils.fprintf_list ~sep:"" 
563
    (fun fmt r -> fprintf fmt "requires %a@ " pp_eexpr_expr r) 
564
    fmt 
565
    spec.m_requires;
566
  pre fmt;
567
  Utils.fprintf_list ~sep:"" 
568
    (fun fmt r -> fprintf fmt "ensures %a@ " pp_eexpr_expr r) 
569
    fmt 
570
    spec.m_ensures;
571
  post fmt;
572
  fprintf fmt "@ ";
573
    (* TODO assigns + separated *)
574
    (* fprintf fmt "assigns *self%t%a;@ "  *)
575
    (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
576
    (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
577
    Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, ensures) -> 
578
      fprintf fmt "behavior %s:@[@ %a@ %a@]" 
579
	name
580
	(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a" pp_eexpr_expr r)) assumes
581
	(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a" pp_eexpr_expr r)) ensures
582
    ) fmt spec.m_behaviors;
583
    (* Assings *)
584
    pp_assigns [] stateless machines fmt m;
585
    fprintf fmt "@]@ */@.";
586
    ()
587

    
588

    
589
let pp_c_decl_struct_spec_var fmt id =
590
  if !Options.ghost_mode then
591
    fprintf fmt "/*@@ ghost %a */" pp_c_decl_struct_var id
592
 else 
593
    fprintf fmt "%a" pp_c_decl_struct_var id
594
  
595
module Make = 
596
  functor (SpecArg: SPECARG) -> 
597
struct
598
  
599
  open SpecArg
600

    
601
(**************************************************************************)
602
(*                              INITIALIZE DATA                           *)
603
(**************************************************************************)
604
(* Map each machine uid to its compiled spec (and TODO later annot) *)
605
let compiled_contracts : (node_desc * spec_machine_t) list ref = ref []
606
let compiled_ee : eexpr_minimachine_t list ref = ref []
607

    
608
let init machines =
609
  
610
  List.iter (
611
    fun m -> (* iterate through spec eexpr and register them *)
612
      let nd = m.mname in
613
      let translate_eexpr ee = 
614
	        let eem = translate_eexpr nd ee in
615
	        compiled_ee := eem::!compiled_ee;
616
	        eem
617
      in
618
      let tl = List.map translate_eexpr in
619
      match m.mspec with
620
      | None -> ()
621
      | Some spec ->
622
	let compiled_spec =
623
	  { m_requires = tl spec.requires;
624
	    m_ensures =  tl spec.ensures;
625
	    m_behaviors = List.map 
626
	      (fun (s, eel1, eel2, _) -> (s, tl eel1, tl eel2))
627
	      spec.behaviors
628
	  }
629
	in
630
	compiled_contracts := (nd, compiled_spec)::!compiled_contracts
631
  ) machines
632

    
633
let get_ee_minimachine ee = 
634
  List.find (fun eem -> eem.muid = ee.eexpr_tag) !compiled_ee 
635

    
636
let get_spec nd = List.assoc nd !compiled_contracts
637

    
638
(**************************************************************************)
639
(*                              HEADER                                    *)
640
(**************************************************************************)
641

    
642
module HdrMod = struct
643

    
644
let get_spec_memories m =
645
  match m.mspec with
646
    None -> []
647
  | Some _ -> 
648
    let spec = get_spec m.mname in
649
    List.flatten (
650
    List.map (fun ee -> ee.mmmemory) 
651
      (spec.m_requires@
652
	 spec.m_ensures@
653
	 (List.fold_left 
654
	    (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
655
	    [] spec.m_behaviors)
656
      ))
657

    
658
let _print_machine_decl_init_fun_prefix pre post fmt m =
659
      let self = mk_self m in
660
	    fprintf fmt "/*@@requires \\valid(%s);@." self;
661
      pre fmt;
662
      post fmt;
663
	    fprintf fmt "assigns *%s;*/@." self
664

    
665

    
666
let _print_machine_decl_step_fun_prefix stateless pre post fmt m =
667
(* Print specification contracts if any *)
668
      (match m.mspec with
669
      | None -> pp_acsl_mem_valid stateless pre post machines fmt m
670
      | Some _ -> 
671
	let spec = get_spec m.mname in
672
    	pp_acsl_spec_contracts stateless pre post machines m m.mstep.step_outputs fmt spec
673
      )
674

    
675
let has_spec_mem m = (get_spec_memories m) <> []
676

    
677
let pp_registers_struct fmt m = 
678
  let spec_memories = get_spec_memories m in
679
  (Utils.fprintf_list ~sep:"@;" pp_c_decl_struct_spec_var) fmt spec_memories
680

    
681
let print_machine_decl_prefix fmt m =
682
  (* Print specification if any *)
683
  let mems = Machine_code.get_mems m machines in  
684
  (match m.mspec with
685
  | None -> ()
686
  | Some _ ->
687
    let spec = get_spec m.mname in
688
    pp_acsl_spec_logics (List.length mems == 0) m fmt spec
689
  )
690

    
691
let print_machine_decl_step_fun_prefix fmt m = _print_machine_decl_step_fun_prefix false (fun fmt -> ()) (fun fmt -> ()) fmt m
692

    
693
let print_machine_decl_init_fun_prefix fmt m = _print_machine_decl_init_fun_prefix (fun fmt -> ()) (fun fmt -> ()) fmt m
694
	
695
let print_machine_decl_stateless_fun_prefix fmt m = _print_machine_decl_step_fun_prefix true (fun fmt -> ()) (fun fmt -> ()) fmt m
696

    
697
let print_global_decl = fun fmt -> ()
698

    
699
end
700

    
701
(**************************************************************************)
702
(*                              CODE                                      *)
703
(**************************************************************************)
704

    
705
module SrcMod =
706
struct
707

    
708

    
709
(**************************************************************************)
710
(*                              CODE                                      *)
711
(**************************************************************************)
712

    
713
  let pp_instr_debug m (eem: eexpr_minimachine_t) fmt instrs =
714
    let self = mk_self m in
715
    let conv_m = machine_from_minimachine_effects m eem in
716
    Utils.fprintf_list ~sep:"@;" 
717
      (C_backend_src.pp_machine_instr_internal 
718
	 [] (* no dependencies considered *)
719
	 conv_m
720
	 (* (m.mname.node_id,  *)
721
	 (*  ee.mmstep_effects.step_inputs,  *)
722
	 (*  ee.mmstep_effects.step_outputs,  *)
723
	 (*  ee.mmstep_effects.step_locals,  *)
724
	 (*  ee.mmmemory,  *)
725
	 (*  ee.mminstances,  *)
726
	 (*  ee.mmcalls) *)
727
	 self)
728
      fmt 
729
      instrs
730

    
731
  (* Print instructions *)
732
  let pp_instr pp_machine_instr m (eem: eexpr_minimachine_t) fmt instrs =
733
    let self = mk_self m in
734
    let conv_m = machine_from_minimachine_effects m eem in
735
    Utils.fprintf_list ~sep:"@;" 
736
      (pp_machine_instr 
737
	 [] (* no dependencies considered *)
738
	 conv_m
739
	 (* (m.mname.node_id,  *)
740
	 (*  ee.mmstep_effects.step_inputs,  *)
741
	 (*  ee.mmstep_effects.step_outputs,  *)
742
	 (*  ee.mmstep_effects.step_locals,  *)
743
	 (*  ee.mmmemory,  *)
744
	 (*  ee.mminstances,  *)
745
	 (*  ee.mmcalls) *)
746
	 self)
747
      fmt 
748
      instrs
749

    
750
  let pp_acsl_spec_side_effects pp_machine_instr m fmt spec = 
751
    let pp_side_effects fmt ee =  
752
      (* Declare local vars *)
753
      let locals = 
754
	List.filter 
755
	  (fun l -> not (List.mem l m.mstep.step_locals)) 
756
	  ee.mmstep_effects.step_locals 
757
      in
758
      (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) fmt locals;
759
      Utils.pp_final_char_if_non_empty ";@," locals fmt ;
760
      pp_instr pp_machine_instr m ee fmt ee.mmstep_effects.step_instrs
761
    in
762
    let effects = spec.m_requires@spec.m_ensures@
763
      (List.fold_left 
764
	 (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
765
	 [] spec.m_behaviors)
766
    in
767
    let effects = List.filter (fun ee -> ee.mmstep_effects.step_instrs <> []) effects in
768
    let all_instrs = List.flatten (List.map (fun e -> e.mmstep_effects.step_instrs) effects) in
769
    if all_instrs <> [] then (
770
      fprintf fmt "// Begin of specification memory update block@;";
771
      if !Options.ghost_mode then
772
	fprintf fmt "@[<v 3>/*@@ ghost %a@]@;*/@;" 
773
	  (Utils.fprintf_list ~sep:"@;" pp_side_effects)
774
	  effects
775
      else (
776
	Utils.fprintf_list ~sep:"@;" pp_side_effects fmt effects;
777
	fprintf fmt "@;"
778
      )
779
      ;
780
      fprintf fmt "// End of specification memory update block@."
781
    )
782

    
783
let pp_acsl_spec_init_side_effects pp_machine_instr m fmt spec = 
784
   let pp_side_effects fmt ee =  
785
    (* Print instructions *)
786
    pp_instr pp_machine_instr m ee fmt ee.mminit
787
  in
788
  
789
  let effects = spec.m_requires@spec.m_ensures@
790
    (List.fold_left 
791
       (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
792
       [] spec.m_behaviors)
793
  in
794
  
795
  let effects = List.filter (fun ee -> ee.mminit <> []) effects in
796
  let all_instrs = List.flatten (List.map (fun e -> e.mminit) effects) in
797
  if all_instrs <> [] then (
798
    fprintf fmt "// Begin of specification memory init block@;";
799
    if !Options.ghost_mode then
800
      fprintf fmt "@[<v 3>/*@@ ghost %a@]@;*/@;" 
801
	(Utils.fprintf_list ~sep:"@;" pp_side_effects)
802
	effects
803
    else (
804
      Utils.fprintf_list ~sep:"@;" pp_side_effects fmt effects;
805
      fprintf fmt "@;"
806
    )
807
    ;
808
    fprintf fmt "// End of specification memory init block@."
809
  )
810

    
811
let print_step_code_postfix pp_machine_instr stateless fmt m =
812
  (* Print specification if any: insert side effect at the end of the function body  *)
813
  match m.mspec with
814
  | None -> ()
815
  | Some _ -> (* the node contain a spec. It has been compiled in the init phase *)
816
    let spec = get_spec m.mname in
817
    pp_acsl_spec_side_effects pp_machine_instr m fmt spec
818

    
819
let print_step_code_prefix pp_machine_instr x fmt m = ()
820
let print_step_code_midfix pp_machine_instr x fmt m = ()
821

    
822
  let print_instr_prefix m fmt x = ()
823
  let print_instr_postfix m fmt x = ()
824
    
825
let print_init_code_postfix pp_machine_instr fmt m =
826
  (* Print specification if any: insert side effect at the end of the function body  *)
827
  match m.mspec with
828
  | None -> ()
829
  | Some _ -> (* the node contain a spec. It has been compiled in the init phase *)
830
    let spec = get_spec m.mname in
831
    pp_acsl_spec_init_side_effects pp_machine_instr m fmt spec
832
    
833
end
834

    
835
(**************************************************************************)
836
(*                              MAKEFILE                                  *)
837
(**************************************************************************)
838

    
839
let makefile_targets fmt basename nodename dependencies =
840
  fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
841
  (* EACSL version of library file . c *)
842
  fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
843
  fprintf fmt 
844
    "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@." 
845
    basename basename; 
846
  fprintf fmt "@.";
847
  fprintf fmt "@.";
848

    
849
  (* EACSL version of library file . c + main .c  *)
850
  fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;
851
  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@." 
852
    basename basename basename; 
853
  (* Ugly hack to deal with eacsl bugs *)
854
  fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;
855
  fprintf fmt "@.";
856
  fprintf fmt "@.";
857

    
858
  (* EACSL version of binary *)
859
  fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
860
  fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)
861
  C_backend_makefile.fprintf_dependencies fmt dependencies; 
862
  fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@." 
863
    basename 
864
    (Utils.fprintf_list ~sep:" " (fun fmt (s, _, _) -> Format.fprintf fmt "%s.o" s)) 
865
    (C_backend_makefile.compiled_dependencies dependencies)
866
    ("${FRAMACEACSL}/e_acsl.c " 
867
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c " 
868
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
869
    basename 
870
    (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib)) 
871
    (C_backend_makefile.lib_dependencies dependencies)
872
  ;
873
  fprintf fmt "@.";
874

    
875
module MakefileMod =
876
struct
877
  let other_targets = makefile_targets
878
    
879
end
880

    
881
module MainMod = C_backend_main.EmptyMod
882

    
883
module CoqMod = C_backend_coq.EmptyMod
884

    
885
end
886
(* Local Variables: *)
887
(* compile-command:"make -C ../../.." *)
888
(* End: *)
(8-8/9)