Project

General

Profile

Download (16.7 KB) Statistics
| Branch: | Tag: | Revision:
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 Types
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
let rec get_type_cst c =
51
  match c with
52
  | Const_int(n) -> new_ty Tint
53
  | Const_real(x) -> new_ty Treal
54
  | Const_float(f) -> new_ty Treal
55
  | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type_cst (List.hd l)))
56
  | Const_tag(tag) -> new_ty Tbool
57
  | Const_string(str) ->  assert false(* used only for annotations *)
58
  | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l))
59

    
60
let rec get_type v = 
61
  match v with
62
  | Cst c -> get_type_cst c             
63
  | Access(tab, index) -> begin
64
                           let rec remove_link ltype = match (dynamic_type ltype).tdesc with 
65
                             | Tlink t -> t
66
                             | _ -> ltype
67
                           in
68
                            match (dynamic_type (remove_link (get_type tab))).tdesc with
69
                            | Tarray(size, t) -> remove_link t
70
                            | Tvar -> Format.eprintf "Type of access is a variable... "; assert false
71
                            | Tunivar -> Format.eprintf "Type of access is a variable... "; assert false
72
                            | _ -> Format.eprintf "Type of access is not an array "; assert false
73
                          end
74
  | Power(v, n) -> assert false
75
  | LocalVar v -> v.var_type
76
  | StateVar v -> v.var_type
77
  | Fun(n, vl) -> begin match n with
78
                  | "+" 
79
                  | "-" 
80
                  | "*" -> get_type (List.hd vl)
81
                  | _ -> Format.eprintf "Function undealt with : %s" n ;assert false
82
                  end
83
  | Array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type (List.hd l)))
84
  | _ -> assert false
85

    
86

    
87
let rec default_val fmt t =
88
  match (dynamic_type t).tdesc with
89
  | Tint -> fprintf fmt "0"
90
  | Treal -> fprintf fmt "0"
91
  | Tbool -> fprintf fmt "true"
92
  | Tarray(dim, l) -> let valt = array_element_type t in
93
                      fprintf fmt "((as const (Array Int ";
94
                      begin try
95
                        pp_type fmt valt
96
                      with
97
                      | _ -> fprintf fmt "failed"; end;
98
                      fprintf fmt ")) ";
99
                      begin try
100
                        default_val fmt valt
101
                      with
102
                      | _ -> fprintf fmt "failed"; end;
103
                      fprintf fmt ")"
104
  | Tstruct(l) -> assert false
105
  | Ttuple(l) -> assert false
106
  |_ -> assert false
107

    
108

    
109
(* Prints a value expression [v], with internal function calls only.
110
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
111
   but an offset suffix may be added for array variables
112
*)
113
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
114
  match v with
115
    | Cst c         -> pp_horn_const fmt c
116
    | Array initlist       -> (*Format.fprintf err_formatter "init %a" (pp_horn_val ~is_lhs:is_lhs self pp_var) (List.hd initlist);*)
117
                              let rec print tab x =
118
                                match tab with
119
                                | [] -> default_val fmt (get_type v)(*fprintf fmt "YAY"*)
120
                                | h::t -> fprintf fmt "(store "; print t (x+1); fprintf fmt " %i " x; pp_horn_val ~is_lhs:is_lhs self pp_var fmt h; fprintf fmt ")" 
121
                              in
122
                              print initlist 0
123
    | Access(tab,index)      -> fprintf fmt "(select "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt tab; fprintf fmt " "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt index; fprintf fmt ")"
124
    | Power (v, n)  -> assert false
125
    | LocalVar v    -> pp_var fmt (rename_machine self v)
126
    | StateVar v    ->
127
      if Types.is_array_type v.var_type
128
      then begin assert false; eprintf "toto called\n";fprintf fmt "TOTO" end
129
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
130
    | Fun (n, vl)   -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
131

    
132
(* Prints a [value] indexed by the suffix list [loop_vars] *)
133
let rec pp_value_suffix self pp_value fmt value =
134
 match value with
135
 | Fun (n, vl)  ->
136
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
137
 |  _            ->
138
   pp_horn_val self pp_value fmt value
139

    
140
(* type_directed assignment: array vs. statically sized type
141
   - [var_type]: type of variable to be assigned
142
   - [var_name]: name of variable to be assigned
143
   - [value]: assigned value
144
   - [pp_var]: printer for variables
145
*)
146
let pp_assign m pp_var fmt var_type var_name value =
147
  let self = m.mname.node_id in
148
  fprintf fmt "(= %a %a)" 
149
    (pp_horn_val ~is_lhs:true self pp_var) var_name
150
    (pp_value_suffix self pp_var) value
151
    
152

    
153
(* In case of no reset call, we define mid_mem = current_mem *)
154
let pp_no_reset machines m fmt i =
155
  let (n,_) = List.assoc i m.minstances in
156
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
157

    
158
  let m_list = 
159
    rename_machine_list
160
      (concat m.mname.node_id i)
161
      (rename_mid_list (full_memory_vars machines target_machine))
162
  in
163
  let c_list =
164
    rename_machine_list
165
      (concat m.mname.node_id i)
166
      (rename_current_list (full_memory_vars machines target_machine))
167
  in
168
  match c_list, m_list with
169
  | [chd], [mhd] ->
170
    fprintf fmt "(= %a %a)"
171
      (pp_horn_var m) mhd
172
      (pp_horn_var m) chd
173
  
174
  | _ -> (
175
    fprintf fmt "@[<v 0>(and @[<v 0>";
176
    List.iter2 (fun mhd chd -> 
177
      fprintf fmt "(= %a %a)@ "
178
      (pp_horn_var m) mhd
179
      (pp_horn_var m) chd
180
    )
181
      m_list
182
      c_list      ;
183
    fprintf fmt ")@]@ @]"
184
  )
185

    
186
let pp_instance_reset machines m fmt i =
187
  let (n,_) = List.assoc i m.minstances in
188
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
189
  
190
  fprintf fmt "(%a @[<v 0>%a)@]"
191
    pp_machine_reset_name (node_name n)
192
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
193
    (
194
      (rename_machine_list
195
	 (concat m.mname.node_id i)
196
	 (rename_current_list (full_memory_vars machines target_machine))
197
      ) 
198
      @
199
	(rename_machine_list
200
	   (concat m.mname.node_id i)
201
	   (rename_mid_list (full_memory_vars machines target_machine))
202
	)
203
    )
204

    
205
let pp_instance_call machines reset_instances m fmt i inputs outputs =
206
  let self = m.mname.node_id in
207
  try (* stateful node instance *)
208
    begin
209
      let (n,_) = List.assoc i m.minstances in
210
      let target_machine = List.find (fun m  -> m.mname.node_id = node_name n) machines in
211
      (* Checking whether this specific instances has been reset yet *)
212
      if not (List.mem i reset_instances) then
213
	(* If not, declare mem_m = mem_c *)
214
	pp_no_reset machines m fmt i;
215
      
216
      let mems = full_memory_vars machines target_machine in
217
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
218
      let mid_mems = rename_mems rename_mid_list in
219
      let next_mems = rename_mems rename_next_list in
220

    
221
      match node_name n, inputs, outputs, mid_mems, next_mems with
222
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
223
	fprintf fmt "@[<v 5>(and ";
224
	fprintf fmt "(= %a (ite %a %a %a))"
225
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (LocalVar o) (* output var *)
226
	  (pp_horn_var m) mem_m 
227
	  (pp_horn_val self (pp_horn_var m)) i1
228
	  (pp_horn_val self (pp_horn_var m)) i2
229
	;
230
	fprintf fmt "@ ";
231
	fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
232
	fprintf fmt ")@]"
233
      end
234

    
235
      | node_name_n -> begin
236
	fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]"
237
	  pp_machine_step_name (node_name n)
238
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
239
	  (Utils.pp_final_char_if_non_empty "@ " inputs)
240
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
241
	  (List.map (fun v -> LocalVar v) outputs)
242
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
243
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
244
	
245
      end
246
    end
247
  with Not_found -> ( (* stateless node instance *)
248
    let (n,_) = List.assoc i m.mcalls in
249
    fprintf fmt "(%s @[<v 0>%a%t%a)@]"
250
      (node_name n)
251
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
252
      inputs
253
      (Utils.pp_final_char_if_non_empty "@ " inputs)
254
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
255
      (List.map (fun v -> LocalVar v) outputs)
256
  )
257
    
258
    
259
(* Print the instruction and update the set of reset instances *)
260
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
261
  match instr with
262
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
263
    pp_no_reset machines m fmt i;
264
    i::reset_instances
265
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
266
    pp_instance_reset machines m fmt i;
267
    i::reset_instances
268
  | MLocalAssign (i,v) ->
269
    pp_assign
270
      m (pp_horn_var m) fmt
271
      i.var_type (LocalVar i) v;
272
    reset_instances
273
  | MStateAssign (i,v) ->
274
    pp_assign
275
      m (pp_horn_var m) fmt
276
      i.var_type (StateVar i) v;
277
    reset_instances
278
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
279
    assert false (* This should not happen anymore *)
280
  | MStep (il, i, vl) ->
281
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
282
       mem_c and print the call to mem_m *)
283
    pp_instance_call machines reset_instances m fmt i vl il;
284
    reset_instances (* Since this instance call will only happen once, we
285
		       don't have to update reset_instances *)
286

    
287
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
288
			 should not be produced yet. Later, we will have to
289
			 compare the reset_instances of each branch and
290
			 introduced the mem_m = mem_c for branches to do not
291
			 address it while other did. Am I clear ? *)
292
    (* For each branch we obtain the logical encoding, and the information
293
       whether a sub node has been reset or not. If a node has been reset in one
294
       of the branch, then all others have to have the mem_m = mem_c
295
       statement. *)
296
    let self = m.mname.node_id in
297
    let pp_branch fmt (tag, instrs) =
298
      fprintf fmt 
299
	"@[<v 3>(or (not (= %a %s))@ " 
300
	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It
301
					  seems that => within Horn predicate
302
					  may cause trouble. I have hard time
303
					  producing a MWE, so I'll just keep the
304
					  fix here as (not a) or b *)
305
	(pp_horn_val self (pp_horn_var m)) g
306
	tag;
307
      let rs = pp_machine_instrs machines reset_instances m fmt instrs in
308
      fprintf fmt "@])";
309
      () (* rs *)
310
    in
311
    pp_conj pp_branch fmt hl;
312
    reset_instances 
313

    
314
and pp_machine_instrs machines reset_instances m fmt instrs = 
315
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
316
  match instrs with
317
  | [x] -> ppi reset_instances fmt x 
318
  | _::_ ->
319
    fprintf fmt "(and @[<v 0>";
320
    let rs = List.fold_left (fun rs i -> 
321
      let rs = ppi rs fmt i in
322
      fprintf fmt "@ ";
323
      rs
324
    )
325
      reset_instances instrs 
326
    in
327
    fprintf fmt "@])";
328
    rs
329

    
330
  | [] -> fprintf fmt "true"; reset_instances
331

    
332
let pp_machine_reset machines fmt m =
333
  let locals = local_memory_vars machines m in
334
  fprintf fmt "@[<v 5>(and @ ";
335

    
336
  (* print "x_m = x_c" for each local memory *)
337
  (Utils.fprintf_list ~sep:"@ " (fun fmt v -> 
338
    fprintf fmt "(= %a %a)"
339
      (pp_horn_var m) (rename_mid v)
340
      (pp_horn_var m) (rename_current v)
341
   )) fmt locals;
342
  fprintf fmt "@ ";
343

    
344
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
345
     Special treatment for _arrow: _first = true
346
  *)
347
  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
348
    let name = node_name n in
349
    if name = "_arrow" then ( 
350
      fprintf fmt "(= %s._arrow._first_m true)"
351
	(concat m.mname.node_id id)  
352
    ) else (
353
      let machine_n = get_machine machines name in 
354
      fprintf fmt "(%s_reset @[<hov 0>%a@])" 
355
	name
356
	(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
357
	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
358
    )
359
   )) fmt m.minstances;
360

    
361
  fprintf fmt "@]@ )"
362

    
363

    
364

    
365
(**************************************************************)
366

    
367
let is_stateless m = m.minstances = [] && m.mmemory = []
368

    
369
(* Print the machine m:
370
   two functions: m_init and m_step
371
   - m_init is a predicate over m memories
372
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
373
   We first declare all variables then the two /rules/.
374
*)
375
let print_machine machines fmt m =
376
  if m.mname.node_id = arrow_id then
377
    (* We don't print arrow function *)
378
    ()
379
  else
380
    begin
381
      fprintf fmt "; %s@." m.mname.node_id;
382
      
383
      (* Printing variables *)
384
      Utils.fprintf_list ~sep:"@." pp_decl_var fmt
385
	(
386
	  (inout_vars machines m)@
387
	    (rename_current_list (full_memory_vars machines m)) @
388
	    (rename_mid_list (full_memory_vars machines m)) @
389
	    (rename_next_list (full_memory_vars machines m)) @
390
	    (rename_machine_list m.mname.node_id m.mstep.step_locals)
391
	);
392
      pp_print_newline fmt ();
393

    
394
      if is_stateless m then
395
	begin
396
	  (* Declaring single predicate *)
397
	  fprintf fmt "(declare-rel %a (%a))@."
398
	    pp_machine_stateless_name m.mname.node_id
399
	    (Utils.fprintf_list ~sep:" " pp_type)
400
	    (List.map (fun v -> v.var_type) (inout_vars machines m));
401

    
402
	  (* Rule for single predicate *)
403
	  fprintf fmt "@[<v 2>(rule (=> @ ";
404
	  ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
405
	  fprintf fmt "@ (%a %a)@]@.))@.@."
406
	    pp_machine_stateless_name m.mname.node_id
407
	    (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
408
	end
409
      else
410
	begin
411
	  (* Declaring predicate *)
412
	  fprintf fmt "(declare-rel %a (%a))@."
413
	    pp_machine_reset_name m.mname.node_id
414
	    (Utils.fprintf_list ~sep:" " pp_type)
415
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
416

    
417
	  fprintf fmt "(declare-rel %a (%a))@."
418
	    pp_machine_step_name m.mname.node_id
419
	    (Utils.fprintf_list ~sep:" " pp_type)
420
	    (List.map (fun v -> v.var_type) (step_vars machines m));
421

    
422
	  pp_print_newline fmt ();
423

    
424
	  (* Rule for reset *)
425
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
426
	    (pp_machine_reset machines) m 
427
	    pp_machine_reset_name m.mname.node_id
428
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
429

    
430
          match m.mstep.step_asserts with
431
	  | [] ->
432
	    begin
433

    
434
	      (* Rule for step*)
435
	      fprintf fmt "@[<v 2>(rule (=> @ ";
436
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
437
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
438
		pp_machine_step_name m.mname.node_id
439
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
440
	    end
441
	  | assertsl -> 
442
	    begin
443
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
444
	      (* print_string pp_val; *)
445
	      fprintf fmt "; with Assertions @.";
446
	      
447
	      (*Rule for step*)
448
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
449
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
450
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
451
		pp_machine_step_name m.mname.node_id
452
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
453
	    end
454
	      
455
	      
456
	end
457
    end
458

    
459

    
460
(* Local Variables: *)
461
(* compile-command:"make -C ../../.." *)
462
(* End: *)
(4-4/5)