Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend_printers.ml @ f3d244c1

History | View | Annotate | Download (13.7 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 (_,_,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.value_desc 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.value_desc 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_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)) (mk_val (LocalVar o) o.var_type) (* 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 -> mk_val (LocalVar v) v.var_type) 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 -> mk_val (LocalVar v) v.var_type) 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
  | MComment _ -> reset_instances
197
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
198
    pp_no_reset machines m fmt i;
199
    i::reset_instances
200
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
201
    pp_instance_reset machines m fmt i;
202
    i::reset_instances
203
  | MLocalAssign (i,v) ->
204
    pp_assign
205
      m (pp_horn_var m) fmt
206
      (mk_val (LocalVar i) i.var_type) v;
207
    reset_instances
208
  | MStateAssign (i,v) ->
209
    pp_assign
210
      m (pp_horn_var m) fmt
211
      (mk_val (StateVar i) i.var_type) v;
212
    reset_instances
213
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
214
    assert false (* This should not happen anymore *)
215
  | MStep (il, i, vl) ->
216
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
217
       mem_c and print the call to mem_m *)
218
    pp_instance_call machines reset_instances m fmt i vl il;
219
    reset_instances (* Since this instance call will only happen once, we
220
		       don't have to update reset_instances *)
221

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

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

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

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

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

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

    
296
  fprintf fmt "@]@ )"
297

    
298

    
299

    
300
(**************************************************************)
301

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

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

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

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

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

    
357
	  pp_print_newline fmt ();
358

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

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

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

    
394

    
395
(* Local Variables: *)
396
(* compile-command:"make -C ../../.." *)
397
(* End: *)