Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend_printers.ml @ 8d0c1f8e

History | View | Annotate | Download (15.4 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

    
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 r   -> pp_print_string fmt r
46
    | Const_float r  -> pp_print_float fmt r
47
    | Const_tag t    -> pp_horn_tag fmt t
48
    | _              -> assert false
49

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

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

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

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

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

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

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

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

    
170
      | node_name_n -> begin
171
	fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]"
172
	  pp_machine_step_name (node_name n)
173
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
174
	  (Utils.pp_final_char_if_non_empty "@ " inputs)
175
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
176
	  (List.map (fun v -> LocalVar v) outputs)
177
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
178
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
179
	
180
      end
181
    end
182
  with Not_found -> ( (* stateless node instance *)
183
    let (n,_) = List.assoc i m.mcalls in
184
    fprintf fmt "(%s @[<v 0>%a%t%a)@]"
185
      (node_name n)
186
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
187
      inputs
188
      (Utils.pp_final_char_if_non_empty "@ " inputs)
189
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
190
      (List.map (fun v -> LocalVar v) outputs)
191
  )
192

    
193

    
194
(* let rec pp_bool_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el = *)
195
(*   fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}" *)
196
(*     (pp_horn_val self (pp_horn_var m)) c *)
197
(*     (Utils.pp_newline_if_non_empty tl) *)
198
(*     (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl *)
199
(*     (Utils.pp_newline_if_non_empty el) *)
200
(*     (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el *)
201

    
202
(* and pp_enum_conditional machines ?(init=false)  (m: machine_t) self fmt g hl = *)
203
(* (\* TODO: check that the enum has all its constructor defined: Xavier how have you handled that, could we have partial definition? *\) *)
204
(*   match hl with *)
205
(*   | [] -> assert false *)
206
(*   | [el] -> Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self) fmt el *)
207
(*   | hd::tl -> *)
208
(*   fprintf fmt "@[<v 2>if (= %a %a) {%t%a@]@,@[<v 2>} else {@.(%a)xxxx@]@,}" *)
209
(*     (pp_horn_val self (pp_horn_var m)) c *)
210
(*     TODOg *)
211
(*     (Utils.pp_newline_if_non_empty tl) *)
212
(*     (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) hd *)
213
(*     pp_print_newline fmt; *)
214
    
215
    
216
(* Print the instruction and update the set of reset instances *)
217
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
218
  match instr with
219
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
220
    pp_no_reset machines m fmt i;
221
    i::reset_instances
222
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
223
    pp_instance_reset machines m fmt i;
224
    i::reset_instances
225
  | MLocalAssign (i,v) ->
226
    pp_assign
227
      m (pp_horn_var m) fmt
228
      i.var_type (LocalVar i) v;
229
    reset_instances
230
  | MStateAssign (i,v) ->
231
    pp_assign
232
      m (pp_horn_var m) fmt
233
      i.var_type (StateVar i) v;
234
    reset_instances
235
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
236
    assert false (* This should not happen anymore *)
237
  | MStep (il, i, vl) ->
238
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
239
       mem_c and print the call to mem_m *)
240
    pp_instance_call machines reset_instances m fmt i vl il;
241
    reset_instances (* Since this instance call will only happen once, we
242
		       don't have to update reset_instances *)
243

    
244
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
245
			 should not be produced yet. Later, we will have to
246
			 compare the reset_instances of each branch and
247
			 introduced the mem_m = mem_c for branches to do not
248
			 address it while other did. Am I clear ? *)
249
    (* For each branch we obtain the logical encoding, and the information
250
       whether a sub node has been reset or not. If a node has been reset in one
251
       of the branch, then all others have to have the mem_m = mem_c
252
       statement. *)
253
    let self = m.mname.node_id in
254
    let pp_branch fmt (tag, instrs) =
255
      fprintf fmt 
256
	"@[<v 3>(or (not (= %a %s))@ " 
257
	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It
258
					  seems that => within Horn predicate
259
					  may cause trouble. I have hard time
260
					  producing a MWE, so I'll just keep the
261
					  fix here as (not a) or b *)
262
	(pp_horn_val self (pp_horn_var m)) g
263
	tag;
264
      let rs = pp_machine_instrs machines reset_instances m fmt instrs in
265
      fprintf fmt "@])";
266
      () (* rs *)
267
    in
268
    pp_conj pp_branch fmt hl;
269
    reset_instances (* TODO: le code est faux en ce qui concerne les resets. Il
270
		       faut calculer ce qui se passe sur chaque branche et rajouter les instructions
271
		       adequates *)
272
	     
273
(* if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false *)
274
(* then (\* boolean case, needs special treatment in C because truth value is not unique *\) *)
275
(*   (\* may disappear if we optimize code by replacing last branch test with default *\) *)
276
(*   let tl = try List.assoc tag_true  hl with Not_found -> [] in *)
277
(*   let el = try List.assoc tag_false hl with Not_found -> [] in *)
278
(*   pp_bool_conditional machines ~init:init m self fmt g tl el *)
279
(* else (\* enum type case *\) *)
280

    
281
(*   pp_enum_conditional machines ~init:init m self fmt g hl  *)
282
and pp_machine_instrs machines reset_instances m fmt instrs = 
283
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
284
  match instrs with
285
  | [x] -> ppi reset_instances fmt x 
286
  | _::_ ->
287
    fprintf fmt "(and @[<v 0>";
288
    let rs = List.fold_left (fun rs i -> 
289
      let rs = ppi rs fmt i in
290
      fprintf fmt "@ ";
291
      rs
292
    )
293
      reset_instances instrs 
294
    in
295
    fprintf fmt "@])";
296
    rs
297

    
298
  | [] -> fprintf fmt "true"; reset_instances
299

    
300
let pp_machine_reset machines fmt m =
301
  let locals = local_memory_vars machines m in
302
  fprintf fmt "@[<v 5>(and @ ";
303

    
304
  (* print "x_m = x_c" for each local memory *)
305
  (Utils.fprintf_list ~sep:"@ " (fun fmt v -> 
306
    fprintf fmt "(= %a %a)"
307
      (pp_horn_var m) (rename_mid v)
308
      (pp_horn_var m) (rename_current v)
309
   )) fmt locals;
310
  fprintf fmt "@ ";
311

    
312
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
313
     Special treatment for _arrow: _first = true
314
  *)
315
  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
316
    let name = node_name n in
317
    if name = "_arrow" then ( 
318
      fprintf fmt "(= %s._arrow._first_m true)"
319
	(concat m.mname.node_id id)  
320
    ) else (
321
      let machine_n = get_machine machines name in 
322
      fprintf fmt "(%s_reset @[<hov 0>%a@])" 
323
	name
324
	(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
325
	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
326
    )
327
   )) fmt m.minstances;
328

    
329
  fprintf fmt "@]@ )"
330

    
331

    
332

    
333
(**************************************************************)
334

    
335
let is_stateless m = m.minstances = [] && m.mmemory = []
336

    
337
(* Print the machine m:
338
   two functions: m_init and m_step
339
   - m_init is a predicate over m memories
340
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
341
   We first declare all variables then the two /rules/.
342
*)
343
let print_machine machines fmt m =
344
  if m.mname.node_id = arrow_id then
345
    (* We don't print arrow function *)
346
    ()
347
  else
348
    begin
349
      fprintf fmt "; %s@." m.mname.node_id;
350
      
351
      (* Printing variables *)
352
      Utils.fprintf_list ~sep:"@." pp_decl_var fmt
353
	(
354
	  (inout_vars machines m)@
355
	    (rename_current_list (full_memory_vars machines m)) @
356
	    (rename_mid_list (full_memory_vars machines m)) @
357
	    (rename_next_list (full_memory_vars machines m)) @
358
	    (rename_machine_list m.mname.node_id m.mstep.step_locals)
359
	);
360
      pp_print_newline fmt ();
361

    
362
      if is_stateless m then
363
	begin
364
	  (* Declaring single predicate *)
365
	  fprintf fmt "(declare-rel %a (%a))@."
366
	    pp_machine_stateless_name m.mname.node_id
367
	    (Utils.fprintf_list ~sep:" " pp_type)
368
	    (List.map (fun v -> v.var_type) (inout_vars machines m));
369

    
370
	  (* Rule for single predicate *)
371
	  fprintf fmt "@[<v 2>(rule (=> @ ";
372
	  ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
373
	  fprintf fmt "@ (%a %a)@]@.))@.@."
374
	    pp_machine_stateless_name m.mname.node_id
375
	    (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
376
	end
377
      else
378
	begin
379
	  (* Declaring predicate *)
380
	  fprintf fmt "(declare-rel %a (%a))@."
381
	    pp_machine_reset_name m.mname.node_id
382
	    (Utils.fprintf_list ~sep:" " pp_type)
383
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
384

    
385
	  fprintf fmt "(declare-rel %a (%a))@."
386
	    pp_machine_step_name m.mname.node_id
387
	    (Utils.fprintf_list ~sep:" " pp_type)
388
	    (List.map (fun v -> v.var_type) (step_vars machines m));
389

    
390
	  pp_print_newline fmt ();
391

    
392
	  (* Rule for reset *)
393
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
394
	    (pp_machine_reset machines) m 
395
	    pp_machine_reset_name m.mname.node_id
396
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
397

    
398
          match m.mstep.step_asserts with
399
	  | [] ->
400
	    begin
401

    
402
	      (* Rule for step*)
403
	      fprintf fmt "@[<v 2>(rule (=> @ ";
404
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
405
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
406
		pp_machine_step_name m.mname.node_id
407
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
408
	    end
409
	  | assertsl -> 
410
	    begin
411
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
412
	      (* print_string pp_val; *)
413
	      fprintf fmt "; with Assertions @.";
414
	      
415
	      (*Rule for step*)
416
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
417
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
418
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
419
		pp_machine_step_name m.mname.node_id
420
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
421
	    end
422
	      
423
	      
424
	end
425
    end
426

    
427

    
428
(* Local Variables: *)
429
(* compile-command:"make -C ../../.." *)
430
(* End: *)