Project

General

Profile

Revision fea041c5

View differences:

src/backends/Horn/horn_backend.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
(* The compilation presented here is defined in Garoche, Gurfinkel, Kahsai,
13
   HCSV'14 *)
12
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14

  
15
   This is a modified version that handles reset and automaton
16
*)
14 17

  
15 18
open Format
16 19
open LustreSpec
17 20
open Corelang
18 21
open Machine_code
19 22

  
23
open Horn_backend_common
24
open Horn_backend_printers
25
open Horn_backend_collecting_sem
20 26

  
21
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
22
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
23
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id
24

  
25
let pp_type fmt t =
26
  match (Types.repr t).Types.tdesc with
27
  | Types.Tbool           -> Format.fprintf fmt "Bool"
28
  | Types.Tint            -> Format.fprintf fmt "Int"
29
  | Types.Treal           -> Format.fprintf fmt "Real"
30
  | Types.Tclock _
31
  | Types.Tarray _
32
  | Types.Tstatic _
33
  | Types.Tconst _
34
  | Types.Tarrow _
35
  | _                     -> Format.eprintf "internal error: pp_type %a@."
36
    Types.print_ty t; assert false
37

  
38
let pp_decl_var fmt id =
39
  Format.fprintf fmt "(declare-var %s %a)"
40
    id.var_id
41
    pp_type id.var_type
42

  
43
let pp_var fmt id = Format.pp_print_string fmt id.var_id
44

  
45

  
46
let pp_conj pp fmt l =
47
  match l with
48
    [] -> assert false
49
  | [x] -> pp fmt x
50
  | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
51

  
52

  
53
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
54
let rename f = (fun v -> {v with var_id = f v.var_id } )
55
let rename_machine p = rename (fun n -> concat p n)
56
let rename_machine_list p = List.map (rename_machine p)
57

  
58
let rename_current =  rename (fun n -> n ^ "_c")
59
let rename_current_list = List.map rename_current
60
let rename_next = rename (fun n -> n ^ "_x")
61
let rename_next_list = List.map rename_next
62

  
27
(*
28
TODO:
29
- gerer les traces. Ca merde pour l'instant dans le calcul des memoires sur les arrows
63 30

  
64
let get_machine machines node_name =
65
  try
66
    List.find (fun m  -> m.mname.node_id = node_name) machines
67
  with Not_found ->
68
    begin
69
      Format.eprintf "internal error: get_machine %s@." node_name;
70
      assert false
71
    end
72

  
73
let full_memory_vars machines machine =
74
  let rec aux fst prefix m =
75
    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
76
      List.fold_left (fun accu (id, (n, _)) ->
77
	let name = node_name n in
78
	if name = "_arrow" then accu else
79
	  let machine_n = get_machine machines name in
80
	  ( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
81
      ) [] (m.minstances)
82
  in
83
  aux true machine.mname.node_id machine
84

  
85
let stateless_vars machines m =
86
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
87
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)
88

  
89
let step_vars machines m =
90
  (stateless_vars machines m)@
91
    (rename_current_list (full_memory_vars machines m)) @
92
    (rename_next_list (full_memory_vars machines m))
93

  
94
let init_vars machines m =
95
  (stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m))
96

  
97
(********************************************************************************************)
98
(*                    Instruction Printing functions                                        *)
99
(********************************************************************************************)
100

  
101
let pp_horn_var m fmt id =
102
  if Types.is_array_type id.var_type
103
  then
104
    assert false (* no arrays in Horn output *)
105
  else
106
    Format.fprintf fmt "%s" id.var_id
107

  
108

  
109
(* Used to print boolean constants *)
110
let pp_horn_tag fmt t =
111
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
112

  
113
(* Prints a constant value *)
114
let rec pp_horn_const fmt c =
115
  match c with
116
    | Const_int i    -> pp_print_int fmt i
117
    | Const_real (c,e,s)   -> assert false (* TODO rational pp_print_string fmt r *)
118
    (* | Const_float r  -> pp_print_float fmt r *)
119
    | Const_tag t    -> pp_horn_tag fmt t
120
    | _              -> assert false
121

  
122
(* Prints a value expression [v], with internal function calls only.
123
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
124
   but an offset suffix may be added for array variables
31
- gerer le reset --- DONE
32
- reconstruire les rechable states DONE
33
- reintroduire le cex/traces ... DONE
34
- traiter les types enum et les branchements sur ces types enum (en particulier les traitements des resets qui ont lieu dans certaines branches et pas dans d'autres )
125 35
*)
126
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
127
  match v.value_desc with
128
    | Cst c         -> pp_horn_const fmt c
129
    | Array _
130
    | Access _ -> assert false (* no arrays *)
131
    | Power (v, n)  -> assert false
132
    | LocalVar v    -> pp_var fmt (rename_machine self v)
133
    | StateVar v    ->
134
      if Types.is_array_type v.var_type
135
      then assert false
136
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
137
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
138

  
139
(* Prints a [value] indexed by the suffix list [loop_vars] *)
140
let rec pp_value_suffix self pp_value fmt value =
141
 match value.value_desc with
142
 | Fun (n, vl)  ->
143
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
144
 |  _            ->
145
   pp_horn_val self pp_value fmt value
146

  
147
(* type_directed assignment: array vs. statically sized type
148
   - [var_type]: type of variable to be assigned
149
   - [var_name]: name of variable to be assigned
150
   - [value]: assigned value
151
   - [pp_var]: printer for variables
152
*)
153
let pp_assign m self pp_var fmt var_type var_name value =
154
  fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
155

  
156
let pp_instance_call
157
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
158
  try (* stateful node instance *)
159
    begin
160
      let (n,_) = List.assoc i m.minstances in
161
      match node_name n, inputs, outputs with
162
      | "_arrow", [i1; i2], [o] -> begin
163
        if init then
164
          pp_assign
165
   	    m
166
   	    self
167
   	    (pp_horn_var m)
168
	    fmt
169
   	    o.var_type (mk_val (LocalVar o) o.var_type) i1
170
        else
171
          pp_assign
172
   	    m self (pp_horn_var m) fmt
173
   	    o.var_type (mk_val (LocalVar o) o.var_type) i2
174
	    
175
      end
176
      | name, _, _ ->
177
	begin
178
	  let target_machine = get_machine machines name in
179
	  if init then
180
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
181
	      pp_machine_init_name (node_name n)
182
	      (* inputs *)
183
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
184
	      inputs
185
	      (Utils.pp_final_char_if_non_empty " " inputs)
186
	      (* outputs *)
187
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
188
	      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
189
	      (Utils.pp_final_char_if_non_empty " " outputs)
190
	      (* memories (next) *)
191
	      (Utils.fprintf_list ~sep:" " pp_var) (
192
  		rename_machine_list
193
		  (concat m.mname.node_id i)
194
		  (rename_next_list (full_memory_vars machines target_machine)
195
		  )
196
	       )
197
	  else
198
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
199
	      pp_machine_step_name (node_name n)
200
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
201
	      (Utils.pp_final_char_if_non_empty " " inputs)
202
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
203
	      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
204
	      (Utils.pp_final_char_if_non_empty " " outputs)
205
	      (Utils.fprintf_list ~sep:" " pp_var) (
206
		(rename_machine_list
207
		   (concat m.mname.node_id i)
208
		   (rename_current_list (full_memory_vars machines target_machine))
209
		) @
210
		  (rename_machine_list
211
		     (concat m.mname.node_id i)
212
		     (rename_next_list (full_memory_vars machines target_machine))
213
		  )
214
	       )
215

  
216
	end
217
    end
218
    with Not_found -> ( (* stateless node instance *)
219
      let (n,_) = List.assoc i m.mcalls in
220
      Format.fprintf fmt "(%s %a%t%a)"
221
	(node_name n)
222
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
223
	inputs
224
	(Utils.pp_final_char_if_non_empty " " inputs)
225
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
226
	(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
227
    )
228

  
229
let pp_machine_init (m: machine_t) self fmt inst =
230
  let (node, static) = List.assoc inst m.minstances in
231
  fprintf fmt "(%a %a%t%s->%s)"
232
    pp_machine_init_name (node_name node)
233
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
234
    (Utils.pp_final_char_if_non_empty " " static)
235
    self inst
236

  
237
(* TODO *)
238
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
239
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
240
    (pp_horn_val self (pp_horn_var m)) c
241
    (Utils.pp_newline_if_non_empty tl)
242
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
243
    (Utils.pp_newline_if_non_empty el)
244
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
245

  
246
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
247
  match instr with
248
  | MReset i ->
249
    pp_machine_init m self fmt i
250
  | MLocalAssign (i,v) ->
251
    pp_assign
252
      m self (pp_horn_var m) fmt
253
      i.var_type (mk_val (LocalVar i) i.var_type) v
254
  | MStateAssign (i,v) ->
255
    pp_assign
256
      m self (pp_horn_var m) fmt
257
      i.var_type (mk_val (StateVar i) i.var_type) v
258
  | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  -> 
259
    assert false (* This should not happen anymore *)
260
  | MStep (il, i, vl) ->
261
    pp_instance_call machines ~init:init m self fmt i vl il
262
  | MBranch (g,hl) ->
263
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
264
    then (* boolean case, needs special treatment in C because truth value is not unique *)
265
      (* may disappear if we optimize code by replacing last branch test with default *)
266
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
267
      let el = try List.assoc tag_false hl with Not_found -> [] in
268
      pp_conditional machines ~init:init m self fmt g tl el
269
    else assert false (* enum type case *)
270
  | MComment _ -> ()
271

  
272

  
273
(**************************************************************)
274

  
275
let is_stateless m = m.minstances = [] && m.mmemory = []
276

  
277
(* Print the machine m:
278
   two functions: m_init and m_step
279
   - m_init is a predicate over m memories
280
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
281
   We first declare all variables then the two /rules/.
282
*)
283
let print_machine machines fmt m =
284
  let pp_instr init = pp_machine_instr machines ~init:init m in
285
  if m.mname.node_id = arrow_id then
286
    (* We don't print arrow function *)
287
    ()
288
  else
289
    begin
290
      Format.fprintf fmt "; %s@." m.mname.node_id;
291

  
292
   (* Printing variables *)
293
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt
294
     ((step_vars machines m)@
295
	 (rename_machine_list m.mname.node_id m.mstep.step_locals));
296
   Format.pp_print_newline fmt ();
297

  
298

  
299

  
300
   if is_stateless m then
301
     begin
302
       (* Declaring single predicate *)
303
       Format.fprintf fmt "(declare-rel %a (%a))@."
304
	 pp_machine_stateless_name m.mname.node_id
305
	 (Utils.fprintf_list ~sep:" " pp_type)
306
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
307

  
308
       (* Rule for single predicate *)
309
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
310
	 (pp_conj (pp_instr
311
		     true (* In this case, the boolean init can be set to true or false.
312
			     The node is stateless. *)
313
		     m.mname.node_id)
314
	 )
315
	 m.mstep.step_instrs
316
	 pp_machine_stateless_name m.mname.node_id
317
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
318
     end
319
   else
320
     begin
321
       (* Declaring predicate *)
322
       Format.fprintf fmt "(declare-rel %a (%a))@."
323
	 pp_machine_init_name m.mname.node_id
324
	 (Utils.fprintf_list ~sep:" " pp_type)
325
	 (List.map (fun v -> v.var_type) (init_vars machines m));
326

  
327
       Format.fprintf fmt "(declare-rel %a (%a))@."
328
	 pp_machine_step_name m.mname.node_id
329
	 (Utils.fprintf_list ~sep:" " pp_type)
330
	 (List.map (fun v -> v.var_type) (step_vars machines m));
331

  
332
       Format.pp_print_newline fmt ();
333

  
334
      (* Adding assertions *)
335
       (match m.mstep.step_asserts with
336
       | [] ->
337
          begin
338
            (* Rule for init *)
339
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
340
	                   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
341
	                   pp_machine_init_name m.mname.node_id
342
	                   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
343
            (* Rule for step*)
344
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
345
                           (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
346
                           pp_machine_step_name m.mname.node_id
347
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
348
          end
349
       | assertsl ->
350
          begin
351
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
352
            (* print_string pp_val; *)
353
            let instrs_concat = m.mstep.step_instrs in
354
            Format.fprintf fmt "; with Assertions @.";
355
            (*Rule for init*)
356
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
357
                           (pp_conj (pp_instr true m.mname.node_id)) instrs_concat
358
                           (pp_conj pp_val) assertsl
359
                           pp_machine_init_name m.mname.node_id
360
                           (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
361
            (*Rule for step*)
362
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
363
                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat
364
                           (pp_conj pp_val) assertsl
365
                           pp_machine_step_name m.mname.node_id
366
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
367
          end
368
       );
369
     end
370
    end
371

  
372

  
373

  
374
let collecting_semantics machines fmt node machine =
375
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
376
    (* We print the types of the main node "memory tree" TODO: add the output *)
377
    let main_output =
378
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
379
    in
380
    let main_output_dummy =
381
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
382
    in
383
    let main_memory_next =
384
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
385
      main_output
386
    in
387
    let main_memory_current =
388
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
389
      main_output_dummy
390
    in
391

  
392
    (* Special case when the main node is stateless *)
393
    let init_name, step_name =
394
      if is_stateless machine then
395
	pp_machine_stateless_name, pp_machine_stateless_name
396
      else
397
	pp_machine_init_name, pp_machine_step_name
398
    in
399

  
400
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
401
      (Utils.fprintf_list ~sep:" " pp_type)
402
      (List.map (fun v -> v.var_type) main_memory_next);
403

  
404
    Format.fprintf fmt "; Initial set@.";
405
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
406
    Format.fprintf fmt "(rule INIT_STATE)@.";
407
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
408
      init_name node
409
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
410
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
411

  
412
    Format.fprintf fmt "; Inductive def@.";
413
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
414
    Format.fprintf fmt
415
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
416
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
417
      step_name node
418
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
419
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
420

  
421
let check_prop machines fmt node machine =
422
  let main_output =
423
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
424
  in
425
  let main_memory_next =
426
    (rename_next_list (full_memory_vars machines machine)) @ main_output
427
  in
428
  Format.fprintf fmt "; Property def@.";
429
  Format.fprintf fmt "(declare-rel ERR ())@.";
430
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
431
    (pp_conj pp_var) main_output
432
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
433
    ;
434
   if !Options.horn_query then Format.fprintf fmt "(query ERR)@."
435

  
436

  
437
let cex_computation machines fmt node machine =
438
    Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
439
    (* We print the types of the cex node "memory tree" TODO: add the output *)
440
    let cex_input =
441
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
442
    in
443
    let cex_input_dummy =
444
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
445
    in
446
    let cex_output =
447
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
448
    in
449
    let cex_output_dummy =
450
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
451
    in
452
    let cex_memory_next =
453
      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
454
    in
455
    let cex_memory_current =
456
      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
457
    in
458

  
459
    (* Special case when the cex node is stateless *)
460
    let init_name, step_name =
461
      if is_stateless machine then
462
	pp_machine_stateless_name, pp_machine_stateless_name
463
      else
464
	pp_machine_init_name, pp_machine_step_name
465
    in
466

  
467
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
468
      (Utils.fprintf_list ~sep:" " pp_type)
469
      (List.map (fun v -> v.var_type) cex_memory_next);
470

  
471
    Format.fprintf fmt "; Initial set@.";
472
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
473
      init_name node
474
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
475
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
476

  
477
    Format.fprintf fmt "; Inductive def@.";
478
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
479
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
480
    Format.fprintf fmt "(declare-var cexcpt Int)@.";
481
    Format.fprintf fmt
482
      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
483
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
484
      step_name node
485
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
486
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
487

  
488
let get_cex machines fmt node machine =
489
    let cex_input =
490
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
491
    in
492
    let cex_output =
493
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
494
    in
495
  let cex_memory_next =
496
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
497
  in
498
  Format.fprintf fmt "; Property def@.";
499
  Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
500
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
501
    (pp_conj pp_var) cex_output
502
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
503
    ;
504
  Format.fprintf fmt "(query CEXTRACE)@."
505

  
506 36

  
507 37
let main_print machines fmt =
508 38
if !Options.main_node <> "" then
509 39
  begin
510 40
    let node = !Options.main_node in
511 41
    let machine = get_machine machines node in
512

  
513

  
514
    collecting_semantics machines fmt node machine;
515
    check_prop machines fmt node machine;
516 42
    if !Options.horn_cex then(
517 43
      cex_computation machines fmt node machine;
518 44
      get_cex machines fmt node machine)
45
    else (
46
      collecting_semantics machines fmt node machine;
47
      check_prop machines fmt node machine;
48
    )
519 49
end
520 50

  
51
let print_type_definitions fmt =
52
  let cpt_type = ref 0 in
53
  Hashtbl.iter (fun typ decl ->
54
    match typ with
55
    | Tydec_const var ->
56
      (match decl.top_decl_desc with
57
      | TypeDef tdef -> (
58
	match tdef.tydef_desc with
59
	| Tydec_enum tl ->
60
	  incr cpt_type;
61
	  fprintf fmt "(declare-datatypes () ((%s %a)));@.@."
62
	    var
63
	    (Utils.fprintf_list ~sep:" " pp_print_string) tl
64
	| _ -> assert false
65
      )
66
      | _ -> assert false
67
      )
68
    | _        -> ()) type_table
69

  
521 70

  
522 71
let translate fmt basename prog machines =
72
  (* We print typedef *)
73
  print_type_definitions fmt;
523 74
  List.iter (print_machine machines fmt) (List.rev machines);
524 75
  main_print machines fmt
525 76

  
526

  
527
let traces_file fmt basename prog machines =
528

  
529
  Format.fprintf fmt
530
  "<?xml version=\"1.0\"?>\n<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">\n";
531

  
532
  (* We extract the annotation dealing with traceability *)
533
  let machines_traces = List.map (fun m ->
534
    let traces : (ident * expr) list=
535
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
536
      let filtered =
537
	List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
538
      in
539
      let content = List.map snd filtered in
540
      (* Elements are supposed to be a pair (tuple): variable, expression *)
541
      List.map (fun ee ->
542
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
543
	| [], Expr_tuple [v;e] -> (
544
	  match v.expr_desc with
545
	  | Expr_ident vid -> vid, e
546
	  | _ -> assert false )
547
	| _ -> assert false)
548
	content
549
    in
550

  
551
    m, traces
552

  
553
  ) machines
554
  in
555

  
556
  (* Compute memories associated to each machine *)
557
  let compute_mems m =
558
    let rec aux fst prefix m =
559
      (List.map (fun mem -> (prefix, mem)) m.mmemory) @
560
	List.fold_left (fun accu (id, (n, _)) ->
561
	  let name = node_name n in
562
	  if name = "_arrow" then accu else
563
	    let machine_n = get_machine machines name in
564
	    ( aux false ((id,machine_n)::prefix) machine_n )
565
	    @ accu
566
	) [] m.minstances
567
    in
568
    aux true [] m
569
  in
570

  
571
  List.iter (fun m ->
572
    (* Format.fprintf fmt "; Node %s@." m.mname.node_id; *)
573
    Format.fprintf fmt "    <Node name=\"%s\">@." m.mname.node_id;
574

  
575
    let memories_old =
576
      List.map (fun (p, v) ->
577
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
578
	let traces = List.assoc machine machines_traces in
579
	if List.mem_assoc v.var_id traces then (
580
	  (* We take the expression associated to variable v in the trace info *)
581
	  (* Format.eprintf "Found variable %a in traces: %a@."  pp_var v Printers.pp_expr (List.assoc v.var_id traces); *)
582
	  p, List.assoc v.var_id traces
583
      )
584
	else (
585
	  (* We keep the variable as is: we create an expression v *)
586
	  (* Format.eprintf "Unable to found variable %a in traces (%a)@."  pp_var v (Utils.fprintf_list ~sep:", " Format.pp_print_string) (List.map fst traces); *)
587
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
588
	)
589

  
590
      ) (compute_mems m)
591
    in
592
    let memories_next = (* We remove the topest pre in each expression *)
593
      List.map
594
      	(fun (prefix, ee) ->
595
      	  match ee.expr_desc with
596
      	  | Expr_pre e -> prefix, e
597
      	  | _ -> Format.eprintf
598
      	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
599
      	    (Utils.fprintf_list ~sep:","
600
      	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
601
      	    (List.rev prefix)
602
      	    Printers.pp_expr ee;
603
      	    assert false)
604
	memories_old
605
    in
606

  
607
    let pp_prefix_rev fmt prefix =
608
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
609
    in
610

  
611
    let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in
612
    let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in
613
     Format.fprintf fmt "     <input name=\"%a\" type=\"%a\">%a</input> @."
614
                   (Utils.fprintf_list ~sep:" | " pp_var) input_vars
615
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) input_vars
616
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_inputs);
617

  
618
    Format.fprintf fmt "      <output name=\"%a\" type=\"%a\">%a</output> @."
619
                   (Utils.fprintf_list ~sep:" | " pp_var)  output_vars
620
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) output_vars
621
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
622

  
623
    let init_local_vars = (rename_next_list (full_memory_vars machines m)) in
624
    let step_local_vars = (rename_current_list (full_memory_vars machines m)) in
625

  
626
    Format.fprintf fmt "      <localInit name=\"%a\" type=\"%a\">%t%a</localInit> @."
627
                   (Utils.fprintf_list ~sep:" | " pp_var) init_local_vars
628
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) init_local_vars
629
                   (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "")
630
                   (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" Printers.pp_expr ee)) memories_next;
631

  
632
    Format.fprintf fmt "      <localStep name=\"%a\" type=\"%a\">%t%a</localStep> @."
633
                   (Utils.fprintf_list ~sep:" | " pp_var) step_local_vars
634
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) step_local_vars
635
                   (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
636
                     (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "(%a)"
637
                                    Printers.pp_expr ee)) (memories_old);
638

  
639
     Format.fprintf fmt "    </Node>@.";
640

  
641
  ) (List.rev machines);
642
  Format.fprintf fmt "</Traces>@.";
643

  
644
          (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)
645
   (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" *)
646
   (*                                  pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old); *)
647

  
648 77
(* Local Variables: *)
649 78
(* compile-command:"make -C ../.." *)
650 79
(* End: *)
src/backends/Horn/horn_backend_collecting_sem.ml
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
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14

  
15
   This is a modified version that handle reset
16
*)
17

  
18
open Format
19
open LustreSpec
20
open Corelang
21
open Machine_code
22

  
23
open Horn_backend_common
24
open Horn_backend_printers
25

  
26
let collecting_semantics machines fmt node machine =
27
  fprintf fmt "; Collecting semantics for node %s@.@." node;
28
  (* We print the types of the main node "memory tree" TODO: add the output *)
29
  let main_output =
30
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
31
  in
32
  let main_output_dummy =
33
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
34
  in
35
  let main_memory_next =
36
    (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
37
      main_output
38
  in
39
  let main_memory_current =
40
    (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
41
      main_output_dummy
42
  in
43

  
44
  (* Special case when the main node is stateless *)
45
  let reset_name, step_name =
46
    if is_stateless machine then
47
      pp_machine_stateless_name, pp_machine_stateless_name
48
    else
49
      pp_machine_reset_name, pp_machine_step_name
50
  in
51

  
52
  fprintf fmt "(declare-rel MAIN (%a))@."
53
    (Utils.fprintf_list ~sep:" " pp_type)
54
    (List.map (fun v -> v.var_type) main_memory_next);
55

  
56
  fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
57
  fprintf fmt "(declare-rel INIT_STATE ())@.";
58
  fprintf fmt "(rule INIT_STATE)@.";
59
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
60
  fprintf fmt "INIT_STATE@ ";
61
  fprintf fmt "(@[<v 0>%a %a@])@ "
62
    reset_name node
63
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine);
64
  fprintf fmt "(@[<v 0>%a %a@])"
65
    step_name node
66
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
67
    
68
  fprintf fmt "@]@ )@ ";
69
  fprintf fmt "(MAIN %a)@]@.))@.@."
70
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ;
71

  
72
  fprintf fmt "; Inductive def@.";
73
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
74
  fprintf fmt
75
    "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
76
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current
77
    step_name node
78
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine)
79
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
80

  
81

  
82
let check_prop machines fmt node machine =
83
  let main_output =
84
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
85
  in
86
  let main_memory_next =
87
    (rename_next_list (full_memory_vars machines machine)) @ main_output
88
  in
89
  fprintf fmt "; Property def@.";
90
  fprintf fmt "(declare-rel ERR ())@.";
91
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
92
    (pp_conj (pp_horn_var machine)) main_output
93
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
94
    ;
95
   if !Options.horn_query then fprintf fmt "(query ERR)@."
96

  
97

  
98
let cex_computation machines fmt node machine =
99
  fprintf fmt "; CounterExample computation for node %s@.@." node;
100
    (* We print the types of the cex node "memory tree" TODO: add the output *)
101
  let cex_input =
102
    rename_machine_list machine.mname.node_id machine.mstep.step_inputs
103
  in
104
  let cex_input_dummy =
105
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
106
  in
107
  let cex_output =
108
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
109
  in
110
  let cex_output_dummy =
111
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
112
  in
113
  let cex_memory_next =
114
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
115
  in
116
  let cex_memory_current =
117
    cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
118
  in
119

  
120
    (* Special case when the cex node is stateless *)
121
  let reset_name, step_name =
122
    if is_stateless machine then
123
      pp_machine_stateless_name, pp_machine_stateless_name
124
    else
125
      pp_machine_reset_name, pp_machine_step_name
126
  in
127

  
128
  fprintf fmt "(declare-rel CEX (Int %a))@.@."
129
    (Utils.fprintf_list ~sep:" " pp_type)
130
    (List.map (fun v -> v.var_type) cex_memory_next);
131

  
132
  fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
133
  fprintf fmt "(declare-rel INIT_STATE_CEX ())@.";
134
  fprintf fmt "(rule INIT_STATE_CEX)@.";
135
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
136
  fprintf fmt "INIT_STATE_CEX@ ";
137
  fprintf fmt "(@[<v 0>%a %a@])@ "
138
    reset_name node
139
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine);
140
  fprintf fmt "(@[<v 0>%a %a@])"
141
    step_name node
142
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
143
  
144
  fprintf fmt "@]@ )@ ";
145
  fprintf fmt "(CEX 0 %a)@]@.))@.@."
146
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next ;
147

  
148
  fprintf fmt "; Inductive def@.";
149
  (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
150
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt cex_output_dummy;
151
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
152
  fprintf fmt "(declare-var cexcpt Int)@.";
153
  fprintf fmt
154
    "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
155
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_current
156
    step_name node
157
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine)
158
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next
159

  
160
let get_cex machines fmt node machine =
161
    let cex_input =
162
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
163
    in
164
    let cex_output =
165
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
166
    in
167
  let cex_memory_next =
168
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
169
  in
170
  fprintf fmt "; Property def@.";
171
  fprintf fmt "(declare-rel CEXTRACE ())@.";
172
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
173
    (pp_conj (pp_horn_var machine)) cex_output
174
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next
175
    ;
176
  fprintf fmt "(query CEXTRACE)@."
177

  
178
(* Local Variables: *)
179
(* compile-command:"make -C ../.." *)
180
(* End: *)
src/backends/Horn/horn_backend_common.ml
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 Format
13
open LustreSpec
14
open Corelang
15
open Machine_code
16

  
17
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
18
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
19
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id
20

  
21
let rec pp_type fmt t =
22
  match (Types.repr t).Types.tdesc with
23
  | Types.Tbool           -> fprintf fmt "Bool"
24
  | Types.Tint            -> fprintf fmt "Int"
25
  | Types.Treal           -> fprintf fmt "Real"
26
  | Types.Tconst ty       -> pp_print_string fmt ty
27
  | Types.Tclock t        -> pp_type fmt t
28
  | Types.Tarray _
29
  | Types.Tstatic _
30
  | Types.Tarrow _
31
  | _                     -> eprintf "internal error: pp_type %a@."
32
    Types.print_ty t; assert false
33

  
34
let pp_decl_var fmt id =
35
  fprintf fmt "(declare-var %s %a)"
36
    id.var_id
37
    pp_type id.var_type
38

  
39
(* let pp_var fmt id = pp_print_string fmt id.var_id  *)
40

  
41

  
42
let pp_conj pp fmt l =
43
  match l with
44
    [] -> assert false
45
  | [x] -> pp fmt x
46
  | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:"@ " pp) l
47

  
48

  
49

  
50
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
51
let rename f = (fun v -> {v with var_id = f v.var_id } )
52
let rename_machine p = rename (fun n -> concat p n)
53
let rename_machine_list p = List.map (rename_machine p)
54

  
55
let rename_current =  rename (fun n -> n ^ "_c")
56
let rename_current_list = List.map rename_current
57
let rename_mid =  rename (fun n -> n ^ "_m")
58
let rename_mid_list = List.map rename_mid
59
let rename_next = rename (fun n -> n ^ "_x")
60
let rename_next_list = List.map rename_next
61

  
62
let get_machine machines node_name =
63
(*  try *)
64
  List.find (fun m  -> m.mname.node_id = node_name) machines
65
(* with Not_found -> Format.eprintf "Unable to find machine %s in machines %a@.@?"  *)
66
(*   node_name *)
67
(*   (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines *)
68
(*   ; assert false *)
69

  
70
let local_memory_vars machines machine =
71
  rename_machine_list machine.mname.node_id machine.mmemory
72
    
73
let instances_memory_vars ?(without_arrow=false) machines machine =
74
  let rec aux fst prefix m =
75
    (
76
      if not fst then (
77
	(rename_machine_list (concat prefix m.mname.node_id) m.mmemory)
78
      )
79
      else []
80
    ) @
81
      List.fold_left (fun accu (id, (n, _)) ->
82
	let name = node_name n in
83
	if without_arrow && name = "_arrow" then
84
	  accu 
85
	else
86
	  let machine_n = get_machine machines name in
87
	  ( aux false (concat prefix 
88
			 (if fst then id else concat m.mname.node_id id))
89
	      machine_n ) @ accu
90
      ) [] (m.minstances)
91
  in
92
  aux true machine.mname.node_id machine
93

  
94
let full_memory_vars ?(without_arrow=false) machines machine =
95
  (local_memory_vars machines machine)
96
  @ (instances_memory_vars ~without_arrow machines machine)
97

  
98
let inout_vars machines m =
99
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)
100
  @ (rename_machine_list m.mname.node_id m.mstep.step_outputs)
101

  
102
let step_vars machines m =
103
  (inout_vars machines m)
104
  @ (rename_current_list (full_memory_vars machines m)) 
105
  @ (rename_next_list (full_memory_vars machines m))
106

  
107
let step_vars_m_x machines m =
108
  (inout_vars machines m)
109
  @ (rename_mid_list (full_memory_vars machines m)) 
110
  @ (rename_next_list (full_memory_vars machines m))
111

  
112
let reset_vars machines m =
113
  (rename_current_list (full_memory_vars machines m)) 
114
  @ (rename_mid_list (full_memory_vars machines m))
115

  
116

  
117
(* Local Variables: *)
118
(* compile-command:"make -C ../.." *)
119
(* End: *)
src/backends/Horn/horn_backend_printers.ml
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
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14

  
15
   This is a modified version that handle reset
16
*)
17

  
18
open Format
19
open LustreSpec
20
open Corelang
21
open Machine_code
22

  
23
open Horn_backend_common
24

  
25

  
26
(********************************************************************************************)
27
(*                    Instruction Printing functions                                        *)
28
(********************************************************************************************)
29

  
30
let pp_horn_var m fmt id =
31
  if Types.is_array_type id.var_type
32
  then
33
    assert false (* no arrays in Horn output *)
34
  else
35
    fprintf fmt "%s" id.var_id
36

  
37
(* Used to print boolean constants *)
38
let pp_horn_tag fmt t =
39
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
40

  
41
(* Prints a constant value *)
42
let rec pp_horn_const fmt c =
43
  match c with
44
    | Const_int i    -> pp_print_int fmt i
45
    | Const_real (_,_s)   -> pp_print_string fmt s
46
    | Const_tag t    -> pp_horn_tag fmt t
47
    | _              -> assert false
48

  
49
(* Prints a value expression [v], with internal function calls only.
50
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
51
   but an offset suffix may be added for array variables
52
*)
53
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
54
  match v with
55
    | Cst c         -> pp_horn_const fmt c
56
    | Array _
57
    | Access _ -> assert false (* no arrays *)
58
    | Power (v, n)  -> assert false
59
    | LocalVar v    -> pp_var fmt (rename_machine self v)
60
    | StateVar v    ->
61
      if Types.is_array_type v.var_type
62
      then assert false
63
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
64
    | Fun (n, vl)   -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
65

  
66
(* Prints a [value] indexed by the suffix list [loop_vars] *)
67
let rec pp_value_suffix self pp_value fmt value =
68
 match value with
69
 | Fun (n, vl)  ->
70
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
71
 |  _            ->
72
   pp_horn_val self pp_value fmt value
73

  
74
(* type_directed assignment: array vs. statically sized type
75
   - [var_type]: type of variable to be assigned
76
   - [var_name]: name of variable to be assigned
77
   - [value]: assigned value
78
   - [pp_var]: printer for variables
79
*)
80
let pp_assign m pp_var fmt var_type var_name value =
81
  let self = m.mname.node_id in
82
  fprintf fmt "(= %a %a)" 
83
    (pp_horn_val ~is_lhs:true self pp_var) var_name
84
    (pp_value_suffix self pp_var) value
85
    
86

  
87
(* In case of no reset call, we define mid_mem = current_mem *)
88
let pp_no_reset machines m fmt i =
89
  let (n,_) = List.assoc i m.minstances in
90
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
91

  
92
  let m_list = 
93
    rename_machine_list
94
      (concat m.mname.node_id i)
95
      (rename_mid_list (full_memory_vars machines target_machine))
96
  in
97
  let c_list =
98
    rename_machine_list
99
      (concat m.mname.node_id i)
100
      (rename_current_list (full_memory_vars machines target_machine))
101
  in
102
  match c_list, m_list with
103
  | [chd], [mhd] ->
104
    fprintf fmt "(= %a %a)"
105
      (pp_horn_var m) mhd
106
      (pp_horn_var m) chd
107
  
108
  | _ -> (
109
    fprintf fmt "@[<v 0>(and @[<v 0>";
110
    List.iter2 (fun mhd chd -> 
111
      fprintf fmt "(= %a %a)@ "
112
      (pp_horn_var m) mhd
113
      (pp_horn_var m) chd
114
    )
115
      m_list
116
      c_list      ;
117
    fprintf fmt ")@]@ @]"
118
  )
119

  
120
let pp_instance_reset machines m fmt i =
121
  let (n,_) = List.assoc i m.minstances in
122
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
123
  
124
  fprintf fmt "(%a @[<v 0>%a)@]"
125
    pp_machine_reset_name (node_name n)
126
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
127
    (
128
      (rename_machine_list
129
	 (concat m.mname.node_id i)
130
	 (rename_current_list (full_memory_vars machines target_machine))
131
      ) 
132
      @
133
	(rename_machine_list
134
	   (concat m.mname.node_id i)
135
	   (rename_mid_list (full_memory_vars machines target_machine))
136
	)
137
    )
138

  
139
let pp_instance_call machines reset_instances m fmt i inputs outputs =
140
  let self = m.mname.node_id in
141
  try (* stateful node instance *)
142
    begin
143
      let (n,_) = List.assoc i m.minstances in
144
      let target_machine = List.find (fun m  -> m.mname.node_id = node_name n) machines in
145
      (* Checking whether this specific instances has been reset yet *)
146
      if not (List.mem i reset_instances) then
147
	(* If not, declare mem_m = mem_c *)
148
	pp_no_reset machines m fmt i;
149
      
150
      let mems = full_memory_vars machines target_machine in
151
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
152
      let mid_mems = rename_mems rename_mid_list in
153
      let next_mems = rename_mems rename_next_list in
154

  
155
      match node_name n, inputs, outputs, mid_mems, next_mems with
156
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
157
	fprintf fmt "@[<v 5>(and ";
158
	fprintf fmt "(= %a (ite %a %a %a))"
159
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (LocalVar o) (* output var *)
160
	  (pp_horn_var m) mem_m 
161
	  (pp_horn_val self (pp_horn_var m)) i1
162
	  (pp_horn_val self (pp_horn_var m)) i2
163
	;
164
	fprintf fmt "@ ";
165
	fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
166
	fprintf fmt ")@]"
167
      end
168

  
169
      | node_name_n -> begin
170
	fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]"
171
	  pp_machine_step_name (node_name n)
172
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
173
	  (Utils.pp_final_char_if_non_empty "@ " inputs)
174
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
175
	  (List.map (fun v -> LocalVar v) outputs)
176
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
177
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
178
	
179
      end
180
    end
181
  with Not_found -> ( (* stateless node instance *)
182
    let (n,_) = List.assoc i m.mcalls in
183
    fprintf fmt "(%s @[<v 0>%a%t%a)@]"
184
      (node_name n)
185
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
186
      inputs
187
      (Utils.pp_final_char_if_non_empty "@ " inputs)
188
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
189
      (List.map (fun v -> LocalVar v) outputs)
190
  )
191
    
192
    
193
(* Print the instruction and update the set of reset instances *)
194
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
195
  match instr with
196
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
197
    pp_no_reset machines m fmt i;
198
    i::reset_instances
199
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
200
    pp_instance_reset machines m fmt i;
201
    i::reset_instances
202
  | MLocalAssign (i,v) ->
203
    pp_assign
204
      m (pp_horn_var m) fmt
205
      i.var_type (LocalVar i) v;
206
    reset_instances
207
  | MStateAssign (i,v) ->
208
    pp_assign
209
      m (pp_horn_var m) fmt
210
      i.var_type (StateVar i) v;
211
    reset_instances
212
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
213
    assert false (* This should not happen anymore *)
214
  | MStep (il, i, vl) ->
215
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
216
       mem_c and print the call to mem_m *)
217
    pp_instance_call machines reset_instances m fmt i vl il;
218
    reset_instances (* Since this instance call will only happen once, we
219
		       don't have to update reset_instances *)
220

  
221
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
222
			 should not be produced yet. Later, we will have to
223
			 compare the reset_instances of each branch and
224
			 introduced the mem_m = mem_c for branches to do not
225
			 address it while other did. Am I clear ? *)
226
    (* For each branch we obtain the logical encoding, and the information
227
       whether a sub node has been reset or not. If a node has been reset in one
228
       of the branch, then all others have to have the mem_m = mem_c
229
       statement. *)
230
    let self = m.mname.node_id in
231
    let pp_branch fmt (tag, instrs) =
232
      fprintf fmt 
233
	"@[<v 3>(or (not (= %a %s))@ " 
234
	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It
235
					  seems that => within Horn predicate
236
					  may cause trouble. I have hard time
237
					  producing a MWE, so I'll just keep the
238
					  fix here as (not a) or b *)
239
	(pp_horn_val self (pp_horn_var m)) g
240
	tag;
241
      let rs = pp_machine_instrs machines reset_instances m fmt instrs in
242
      fprintf fmt "@])";
243
      () (* rs *)
244
    in
245
    pp_conj pp_branch fmt hl;
246
    reset_instances 
247

  
248
and pp_machine_instrs machines reset_instances m fmt instrs = 
249
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
250
  match instrs with
251
  | [x] -> ppi reset_instances fmt x 
252
  | _::_ ->
253
    fprintf fmt "(and @[<v 0>";
254
    let rs = List.fold_left (fun rs i -> 
255
      let rs = ppi rs fmt i in
256
      fprintf fmt "@ ";
257
      rs
258
    )
259
      reset_instances instrs 
260
    in
261
    fprintf fmt "@])";
262
    rs
263

  
264
  | [] -> fprintf fmt "true"; reset_instances
265

  
266
let pp_machine_reset machines fmt m =
267
  let locals = local_memory_vars machines m in
268
  fprintf fmt "@[<v 5>(and @ ";
269

  
270
  (* print "x_m = x_c" for each local memory *)
271
  (Utils.fprintf_list ~sep:"@ " (fun fmt v -> 
272
    fprintf fmt "(= %a %a)"
273
      (pp_horn_var m) (rename_mid v)
274
      (pp_horn_var m) (rename_current v)
275
   )) fmt locals;
276
  fprintf fmt "@ ";
277

  
278
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
279
     Special treatment for _arrow: _first = true
280
  *)
281
  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
282
    let name = node_name n in
283
    if name = "_arrow" then ( 
284
      fprintf fmt "(= %s._arrow._first_m true)"
285
	(concat m.mname.node_id id)  
286
    ) else (
287
      let machine_n = get_machine machines name in 
288
      fprintf fmt "(%s_reset @[<hov 0>%a@])" 
289
	name
290
	(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
291
	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
292
    )
293
   )) fmt m.minstances;
294

  
295
  fprintf fmt "@]@ )"
296

  
297

  
298

  
299
(**************************************************************)
300

  
301
let is_stateless m = m.minstances = [] && m.mmemory = []
302

  
303
(* Print the machine m:
304
   two functions: m_init and m_step
305
   - m_init is a predicate over m memories
306
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
307
   We first declare all variables then the two /rules/.
308
*)
309
let print_machine machines fmt m =
310
  if m.mname.node_id = arrow_id then
311
    (* We don't print arrow function *)
312
    ()
313
  else
314
    begin
315
      fprintf fmt "; %s@." m.mname.node_id;
316
      
317
      (* Printing variables *)
318
      Utils.fprintf_list ~sep:"@." pp_decl_var fmt
319
	(
320
	  (inout_vars machines m)@
321
	    (rename_current_list (full_memory_vars machines m)) @
322
	    (rename_mid_list (full_memory_vars machines m)) @
323
	    (rename_next_list (full_memory_vars machines m)) @
324
	    (rename_machine_list m.mname.node_id m.mstep.step_locals)
325
	);
326
      pp_print_newline fmt ();
327

  
328
      if is_stateless m then
329
	begin
330
	  (* Declaring single predicate *)
331
	  fprintf fmt "(declare-rel %a (%a))@."
332
	    pp_machine_stateless_name m.mname.node_id
333
	    (Utils.fprintf_list ~sep:" " pp_type)
334
	    (List.map (fun v -> v.var_type) (inout_vars machines m));
335

  
336
	  (* Rule for single predicate *)
337
	  fprintf fmt "@[<v 2>(rule (=> @ ";
338
	  ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
339
	  fprintf fmt "@ (%a %a)@]@.))@.@."
340
	    pp_machine_stateless_name m.mname.node_id
341
	    (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
342
	end
343
      else
344
	begin
345
	  (* Declaring predicate *)
346
	  fprintf fmt "(declare-rel %a (%a))@."
347
	    pp_machine_reset_name m.mname.node_id
348
	    (Utils.fprintf_list ~sep:" " pp_type)
349
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
350

  
351
	  fprintf fmt "(declare-rel %a (%a))@."
352
	    pp_machine_step_name m.mname.node_id
353
	    (Utils.fprintf_list ~sep:" " pp_type)
354
	    (List.map (fun v -> v.var_type) (step_vars machines m));
355

  
356
	  pp_print_newline fmt ();
357

  
358
	  (* Rule for reset *)
359
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
360
	    (pp_machine_reset machines) m 
361
	    pp_machine_reset_name m.mname.node_id
362
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
363

  
364
          match m.mstep.step_asserts with
365
	  | [] ->
366
	    begin
367

  
368
	      (* Rule for step*)
369
	      fprintf fmt "@[<v 2>(rule (=> @ ";
370
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
371
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
372
		pp_machine_step_name m.mname.node_id
373
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
374
	    end
375
	  | assertsl -> 
376
	    begin
377
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
378
	      (* print_string pp_val; *)
379
	      fprintf fmt "; with Assertions @.";
380
	      
381
	      (*Rule for step*)
382
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
383
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
384
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
385
		pp_machine_step_name m.mname.node_id
386
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
387
	    end
388
	      
389
	      
390
	end
391
    end
392

  
393

  
394
(* Local Variables: *)
395
(* compile-command:"make -C ../../.." *)
396
(* End: *)
src/backends/Horn/horn_backend_traces.ml
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
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14

  
15
   This is a modified version that handle reset
16
*)
17

  
18
open Format
19
open LustreSpec
20
open Corelang
21
open Machine_code
22

  
23
open Horn_backend_common
24
open Horn_backend_printers
25

  
26
(* Compute memories associated to each machine *)
27
let compute_mems machines m =
28
  let rec aux fst prefix m =
29
    (List.map (fun mem -> (prefix, mem)) m.mmemory) @
30
      List.fold_left (fun accu (id, (n, _)) ->
31
	let name = node_name n in
32
	if name = "_arrow" then accu else
33
	  let machine_n = get_machine machines name in
34
	  ( aux false ((id,machine_n)::prefix) machine_n )
35
	  @ accu
36
      ) [] m.minstances
37
  in
38
  aux true [] m
39

  
40

  
41
(* We extract the annotation dealing with traceability *)
42
let machines_traces machines = 
43
  List.map (fun m ->
44
    let traces : (ident * expr) list=
45
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
46
      let filtered =
47
	List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
48
      in
49
      let content = List.map snd filtered in
50
      (* Elements are supposed to be a pair (tuple): variable, expression *)
51
      List.map (fun ee ->
52
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
53
	| [], Expr_tuple [v;e] -> (
54
	  match v.expr_desc with
55
	  | Expr_ident vid -> vid, e
56
	  | _ -> assert false )
57
	| _ -> assert false)
58
	content
59
    in
60

  
61
    m, traces
62

  
63
  ) machines
64
  
65
let memories_old machines m =
66
  List.map (fun (p, v) ->
67
    let machine = match p with | [] -> m | (_,m')::_ -> m' in
68
    let traces = List.assoc machine (machines_traces machines) in
69
    if List.mem_assoc v.var_id traces then 
70
      (
71
	(* We take the expression associated to variable v in the trace
72
	   info *)
73

  
74
	(* eprintf "Found variable %a in traces: %a@."  pp_var v
75
	   Printers.pp_expr (List.assoc v.var_id traces); *)
76
	p, List.assoc v.var_id traces
77
      )
78
    else 
79
      begin
80

  
81
	(* We keep the variable as is: we create an expression v *)
82

  
83
	(* eprintf "Unable to found variable %a in traces (%a)@."  pp_var v
84
	   (Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst
85
	   traces); *)	    
86

  
87
	p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
88
      end
89

  
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff