Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ ca88e660

History | View | Annotate | Download (18.3 KB)

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
open Horn_backend_collecting_sem
26

    
27
(*
28
TODO:
29
- gerer les traces. Ca merde pour l'instant dans le calcul des memoires sur les arrows
30
- gerer le reset --- DONE
31
- reconstruire les rechable states DONE
32
- reintroduire le cex/traces ... DONE
33
- 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 )
34
*)
35

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

    
42
(* Prints a constant value *)
43
let rec pp_horn_const fmt c =
44
  match c with
45
    | Const_int i    -> pp_print_int fmt i
46
    | Const_real (c,e,s)   -> assert false (* TODO rational pp_print_string fmt r *)
47
    (* | Const_float r  -> pp_print_float fmt r *)
48
    | Const_tag t    -> pp_horn_tag fmt t
49
    | _              -> assert false
50

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

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

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

    
85
let pp_instance_call
86
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
87
  try (* stateful node instance *)
88
    begin
89
      let (n,_) = List.assoc i m.minstances in
90
      match node_name n, inputs, outputs with
91
      | "_arrow", [i1; i2], [o] -> begin
92
        if init then
93
          pp_assign
94
   	    m
95
   	    self
96
   	    (pp_horn_var m)
97
	    fmt
98
   	    o.var_type (mk_val (LocalVar o) o.var_type) i1
99
        else
100
          pp_assign
101
   	    m self (pp_horn_var m) fmt
102
   	    o.var_type (mk_val (LocalVar o) o.var_type) i2
103
	    
104
      end
105
      | name, _, _ ->
106
	begin
107
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
108
	  if init then
109
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
110
	      pp_machine_init_name (node_name n)
111
	      (* inputs *)
112
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
113
	      inputs
114
	      (Utils.pp_final_char_if_non_empty " " inputs)
115
	      (* outputs *)
116
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
117
	      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
118
	      (Utils.pp_final_char_if_non_empty " " outputs)
119
	      (* memories (next) *)
120
	      (Utils.fprintf_list ~sep:" " pp_var) (
121
  		rename_machine_list
122
		  (concat m.mname.node_id i)
123
		  (rename_next_list (full_memory_vars machines target_machine)
124
		  )
125
	       )
126
	  else
127
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
128
	      pp_machine_step_name (node_name n)
129
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
130
	      (Utils.pp_final_char_if_non_empty " " inputs) 
131
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
132
	      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
133
	      (Utils.pp_final_char_if_non_empty " " outputs)
134
	      (Utils.fprintf_list ~sep:" " pp_var) (
135
		(rename_machine_list
136
		   (concat m.mname.node_id i)
137
		   (rename_current_list (full_memory_vars machines target_machine))
138
		) @
139
		  (rename_machine_list
140
		     (concat m.mname.node_id i)
141
		     (rename_next_list (full_memory_vars machines target_machine))
142
		  )
143
	       )
144

    
145
	end
146
    end
147
    with Not_found -> ( (* stateless node instance *)
148
      let (n,_) = List.assoc i m.mcalls in
149
      Format.fprintf fmt "(%s %a%t%a)"
150
	(node_name n)
151
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
152
	inputs
153
	(Utils.pp_final_char_if_non_empty " " inputs) 
154
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
155
	(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
156
    )
157

    
158
let pp_machine_init (m: machine_t) self fmt inst =
159
  let (node, static) = List.assoc inst m.minstances in
160
  fprintf fmt "(%a %a%t%s->%s)"
161
    pp_machine_init_name (node_name node)
162
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
163
    (Utils.pp_final_char_if_non_empty " " static)
164
    self inst
165

    
166
(* TODO *)
167
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
168
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
169
    (pp_horn_val self (pp_horn_var m)) c
170
    (Utils.pp_newline_if_non_empty tl)
171
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
172
    (Utils.pp_newline_if_non_empty el)
173
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
174

    
175
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
176
  match instr with
177
  | MReset i ->
178
    pp_machine_init m self fmt i
179
  | MLocalAssign (i,v) ->
180
    pp_assign
181
      m self (pp_horn_var m) fmt
182
      i.var_type (mk_val (LocalVar i) i.var_type) v
183
  | MStateAssign (i,v) ->
184
    pp_assign
185
      m self (pp_horn_var m) fmt
186
      i.var_type (mk_val (StateVar i) i.var_type) v
187
  | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  -> 
188
    assert false (* This should not happen anymore *)
189
  | MStep (il, i, vl) ->
190
    pp_instance_call machines ~init:init m self fmt i vl il
191
  | MBranch (g,hl) ->
192
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
193
    then (* boolean case, needs special treatment in C because truth value is not unique *)
194
      (* may disappear if we optimize code by replacing last branch test with default *)
195
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
196
      let el = try List.assoc tag_false hl with Not_found -> [] in
197
      pp_conditional machines ~init:init m self fmt g tl el
198
    else assert false (* enum type case *)
199
  | MComment _ -> ()
200

    
201

    
202
(**************************************************************)
203

    
204
let is_stateless m = m.minstances = [] && m.mmemory = []
205

    
206
(* Print the machine m:
207
   two functions: m_init and m_step
208
   - m_init is a predicate over m memories
209
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
210
   We first declare all variables then the two /rules/.
211
*)
212
let print_machine machines fmt m =
213
  let pp_instr init = pp_machine_instr machines ~init:init m in
214
  if m.mname.node_id = arrow_id then
215
    (* We don't print arrow function *)
216
    ()
217
  else
218
    begin
219
      Format.fprintf fmt "; %s@." m.mname.node_id;
220

    
221
   (* Printing variables *)
222
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt
223
     ((step_vars machines m)@
224
	 (rename_machine_list m.mname.node_id m.mstep.step_locals));
225
   Format.pp_print_newline fmt ();
226

    
227

    
228

    
229
   if is_stateless m then
230
     begin
231
       (* Declaring single predicate *)
232
       Format.fprintf fmt "(declare-rel %a (%a))@."
233
	 pp_machine_stateless_name m.mname.node_id
234
	 (Utils.fprintf_list ~sep:" " pp_type)
235
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
236

    
237
       (* Rule for single predicate *)
238
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
239
	 (pp_conj (pp_instr
240
		     true (* In this case, the boolean init can be set to true or false.
241
			     The node is stateless. *)
242
		     m.mname.node_id)
243
	 )
244
	 m.mstep.step_instrs
245
	 pp_machine_stateless_name m.mname.node_id
246
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
247
     end
248
   else
249
     begin
250
       (* Declaring predicate *)
251
       Format.fprintf fmt "(declare-rel %a (%a))@."
252
	 pp_machine_init_name m.mname.node_id
253
	 (Utils.fprintf_list ~sep:" " pp_type)
254
	 (List.map (fun v -> v.var_type) (init_vars machines m));
255

    
256
       Format.fprintf fmt "(declare-rel %a (%a))@."
257
	 pp_machine_step_name m.mname.node_id
258
	 (Utils.fprintf_list ~sep:" " pp_type)
259
	 (List.map (fun v -> v.var_type) (step_vars machines m));
260

    
261
       Format.pp_print_newline fmt ();
262

    
263
      (* Adding assertions *)
264
       (match m.mstep.step_asserts with
265
       | [] ->
266
          begin
267
            (* Rule for init *)
268
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
269
	                   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
270
	                   pp_machine_init_name m.mname.node_id
271
	                   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
272
            (* Rule for step*)
273
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
274
                           (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
275
                           pp_machine_step_name m.mname.node_id
276
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
277
          end
278
       | assertsl ->
279
          begin
280
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
281
            (* print_string pp_val; *)
282
            let instrs_concat = m.mstep.step_instrs in
283
            Format.fprintf fmt "; with Assertions @.";
284
            (*Rule for init*)
285
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
286
                           (pp_conj (pp_instr true m.mname.node_id)) instrs_concat
287
                           (pp_conj pp_val) assertsl
288
                           pp_machine_init_name m.mname.node_id
289
                           (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
290
            (*Rule for step*)
291
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
292
                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat
293
                           (pp_conj pp_val) assertsl
294
                           pp_machine_step_name m.mname.node_id
295
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
296
          end
297
       );
298
       
299
(*
300
       match m.mspec with
301
	 None -> () (* No node spec; we do nothing *)
302
       | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> 
303
	 ( 
304
       (* For the moment, we only deal with simple case: single ensures, no other parameters *)
305
	   ()
306
	     
307
	 )
308
       | _ -> () (* Other cases give nothing *)
309
*)      
310
     end
311
    end
312

    
313

    
314

    
315
let collecting_semantics machines fmt node machine =
316
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
317
    (* We print the types of the main node "memory tree" TODO: add the output *)
318
    let main_output =
319
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
320
    in
321
    let main_output_dummy =
322
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
323
    in
324
    let main_memory_next =
325
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
326
      main_output
327
    in
328
    let main_memory_current =
329
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
330
      main_output_dummy
331
    in
332

    
333
    (* Special case when the main node is stateless *)
334
    let init_name, step_name =
335
      if is_stateless machine then
336
	pp_machine_stateless_name, pp_machine_stateless_name
337
      else
338
	pp_machine_init_name, pp_machine_step_name
339
    in
340

    
341
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
342
      (Utils.fprintf_list ~sep:" " pp_type)
343
      (List.map (fun v -> v.var_type) main_memory_next);
344

    
345
    Format.fprintf fmt "; Initial set@.";
346
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
347
    Format.fprintf fmt "(rule INIT_STATE)@.";
348
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
349
      init_name node
350
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
351
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
352

    
353
    Format.fprintf fmt "; Inductive def@.";
354
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
355
    Format.fprintf fmt
356
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
357
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
358
      step_name node
359
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
360
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
361

    
362
let check_prop machines fmt node machine =
363
  let main_output =
364
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
365
  in
366
  let main_memory_next =
367
    (rename_next_list (full_memory_vars machines machine)) @ main_output
368
  in
369
  Format.fprintf fmt "; Property def@.";
370
  Format.fprintf fmt "(declare-rel ERR ())@.";
371
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
372
    (pp_conj pp_var) main_output
373
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
374
    ;
375
  if !Options.horn_queries then
376
    Format.fprintf fmt "(query ERR)@."
377

    
378

    
379
let cex_computation machines fmt node machine =
380
    Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
381
    (* We print the types of the cex node "memory tree" TODO: add the output *)
382
    let cex_input =
383
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
384
    in
385
    let cex_input_dummy =
386
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
387
    in
388
    let cex_output =
389
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
390
    in
391
    let cex_output_dummy =
392
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
393
    in
394
    let cex_memory_next =
395
      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
396
    in
397
    let cex_memory_current =
398
      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
399
    in
400

    
401
    (* Special case when the cex node is stateless *)
402
    let init_name, step_name =
403
      if is_stateless machine then
404
	pp_machine_stateless_name, pp_machine_stateless_name
405
      else
406
	pp_machine_init_name, pp_machine_step_name
407
    in
408

    
409
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
410
      (Utils.fprintf_list ~sep:" " pp_type)
411
      (List.map (fun v -> v.var_type) cex_memory_next);
412

    
413
    Format.fprintf fmt "; Initial set@.";
414
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
415
      init_name node
416
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
417
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
418

    
419
    Format.fprintf fmt "; Inductive def@.";
420
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
421
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
422
    Format.fprintf fmt "(declare-var cexcpt Int)@.";
423
    Format.fprintf fmt
424
      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
425
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
426
      step_name node
427
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
428
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
429

    
430
let get_cex machines fmt node machine =
431
    let cex_input =
432
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
433
    in
434
    let cex_output =
435
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
436
    in
437
  let cex_memory_next =
438
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
439
  in
440
  Format.fprintf fmt "; Property def@.";
441
  Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
442
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
443
    (pp_conj pp_var) cex_output
444
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
445
    ;
446
  Format.fprintf fmt "(query CEXTRACE)@."
447

    
448

    
449
************************************)
450
let main_print machines fmt =
451
if !Options.main_node <> "" then
452
  begin
453
    let node = !Options.main_node in
454
    let machine = get_machine machines node in
455
    collecting_semantics machines fmt node machine;
456
    check_prop machines fmt node machine;
457
    if !Options.horn_cex then(
458
      cex_computation machines fmt node machine;
459
      get_cex machines fmt node machine)
460
end
461

    
462
let print_type_definitions fmt =
463
  let cpt_type = ref 0 in
464
  Hashtbl.iter (fun typ decl ->
465
    match typ with
466
    | Tydec_const var ->
467
      (match decl.top_decl_desc with
468
      | TypeDef tdef -> (
469
	match tdef.tydef_desc with
470
	| Tydec_enum tl ->
471
	  incr cpt_type;
472
	  fprintf fmt "(declare-datatypes () ((%s %a)));@.@."
473
	    var
474
	    (Utils.fprintf_list ~sep:" " pp_print_string) tl
475
	| _ -> assert false
476
      )
477
      | _ -> assert false
478
      )
479
    | _        -> ()) type_table
480

    
481

    
482
let translate fmt basename prog machines =
483
  (* We print typedef *)
484
  print_type_definitions fmt;
485
  List.iter (print_machine machines fmt) (List.rev machines);
486
  main_print machines fmt
487

    
488
(* Local Variables: *)
489
(* compile-command:"make -C ../.." *)
490
(* End: *)