Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_common.ml @ 51106b7e

History | View | Annotate | Download (29 KB)

1 e4edf171 ploc
open Lustre_types
2
open Machine_code_types
3
open Machine_code_common
4 ad4774b0 ploc
open Format
5 c1785a55 ploc
(* open Horn_backend_common
6
 * open Horn_backend *)
7 5778dd5e ploc
open Zustre_data
8 c1785a55 ploc
9
module HBC = Horn_backend_common
10
let node_name = HBC.node_name
11 5778dd5e ploc
12 c1785a55 ploc
let concat = HBC.concat
13 5778dd5e ploc
14 c1785a55 ploc
let rename_machine = HBC.rename_machine
15
let rename_machine_list = HBC.rename_machine_list
16 5778dd5e ploc
17 c1785a55 ploc
let rename_next = HBC.rename_next
18 5778dd5e ploc
let rename_mid = HBC.rename_mid
19 c1785a55 ploc
let rename_current = HBC.rename_current
20 5778dd5e ploc
21 c1785a55 ploc
let rename_current_list = HBC.rename_current_list
22
let rename_mid_list = HBC.rename_mid_list
23
let rename_next_list = HBC.rename_next_list
24 5778dd5e ploc
25 c1785a55 ploc
let full_memory_vars = HBC.full_memory_vars
26 e4edf171 ploc
let inout_vars = HBC.inout_vars
27
let reset_vars = HBC.reset_vars
28
let step_vars = HBC.step_vars
29
let local_memory_vars = HBC.local_memory_vars
30 5778dd5e ploc
let step_vars_m_x = HBC.step_vars_m_x
31
let step_vars_c_m_x = HBC.step_vars_c_m_x
32 e4edf171 ploc
  
33 c1785a55 ploc
let machine_reset_name = HBC.machine_reset_name 
34 5778dd5e ploc
let machine_step_name = HBC.machine_step_name 
35 ff2d7a82 ploc
let machine_stateless_name = HBC.machine_stateless_name 
36 c1785a55 ploc
37 e4edf171 ploc
let preprocess = Horn_backend.preprocess
38
  
39 5778dd5e ploc
  
40 c1785a55 ploc
(** Sorts
41
42
A sort is introduced for each basic type and each enumerated type.
43 ad4774b0 ploc
44 c1785a55 ploc
A hashtbl records these and allow easy access to sort values, when
45
   provided with a enumerated type name. 
46
47
*)
48
        
49 ad4774b0 ploc
let bool_sort = Z3.Boolean.mk_sort !ctx
50
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
51
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
52
53 c1785a55 ploc
54
let get_const_sort = Hashtbl.find const_sorts 
55
let get_sort_elems = Hashtbl.find sort_elems
56
let get_tag_sort = Hashtbl.find const_tags
57
  
58 ad4774b0 ploc
59 c1785a55 ploc
  
60 ad4774b0 ploc
let decl_sorts () =
61
  Hashtbl.iter (fun typ decl ->
62
    match typ with
63
    | Tydec_const var ->
64
      (match decl.top_decl_desc with
65
      | TypeDef tdef -> (
66
	match tdef.tydef_desc with
67
	| Tydec_enum tl ->
68
	  let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
69 c1785a55 ploc
          Hashtbl.add const_sorts var new_sort;
70
          Hashtbl.add sort_elems new_sort tl;
71
          List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl
72
          
73 46cb4020 ploc
	| _ -> Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false
74 ad4774b0 ploc
      )
75
      | _ -> assert false
76
      )
77
    | _        -> ()) Corelang.type_table
78
79 c1785a55 ploc
                 
80 ad4774b0 ploc
let rec type_to_sort t =
81
  if Types.is_bool_type t  then bool_sort else
82
    if Types.is_int_type t then int_sort else 
83
  if Types.is_real_type t then real_sort else 
84
  match (Types.repr t).Types.tdesc with
85
  | Types.Tconst ty       -> get_const_sort ty
86
  | Types.Tclock t        -> type_to_sort t
87
  | Types.Tarray(dim,ty)   -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
88
  | Types.Tstatic(d, ty)-> type_to_sort ty
89
  | Types.Tarrow _
90
  | _                     -> Format.eprintf "internal error: pp_type %a@."
91
                               Types.print_ty t; assert false
92
93 7d77632f ploc
94
(* let idx_var = *)
95
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort  *)
96
    
97
(* let uid_var = *)
98
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort  *)
99
100 c1785a55 ploc
(** Func decls
101
102 9f3de818 ploc
    Similarly fun_decls are registerd, by their name, into a hashtbl. The
103
    proposed encoding introduces a 0-ary fun_decl to model variables and
104
    fun_decl with arguments to declare reset and step predicates.
105 c1785a55 ploc
106
107
108 9f3de818 ploc
*)
109 c1785a55 ploc
let register_fdecl id fd = Hashtbl.add decls id fd
110 5778dd5e ploc
let get_fdecl id =
111
  try
112
    Hashtbl.find decls id
113
  with Not_found -> (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found)
114 51ec4e8c ploc
115
let pp_fdecls fmt =
116
  Format.fprintf fmt "Registered fdecls: @[%a@]@ "
117
    (Utils.fprintf_list ~sep:"@ " Format.pp_print_string)  (Hashtbl.fold (fun id _ accu -> id::accu) decls [])
118
119 5778dd5e ploc
    
120 ad4774b0 ploc
let decl_var id =
121 dbab1fe5 ploc
  (* Format.eprintf "Declaring var %s@." id.var_id; *)
122 c1785a55 ploc
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
123
  register_fdecl id.var_id fdecl;
124
  fdecl
125
126 7d77632f ploc
let idx_sort = int_sort
127
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort
128
let uid_conc = 
129
  let fd = Z3.Z3List.get_cons_decl uid_sort in
130
  fun head tail -> Z3.FuncDecl.apply fd [head;tail]
131
132
let get_instance_uid =
133
  let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in
134
  let cpt = ref 0 in
135
  fun i ->
136
    let id =
137
      if Hashtbl.mem hash i then
138
	Hashtbl.find hash i
139
      else (
140
	incr cpt;
141
	Hashtbl.add hash i !cpt;
142
	!cpt
143
      )
144
    in
145
    Z3.Arithmetic.Integer.mk_numeral_i !ctx id
146
  
147
148
  
149
let decl_rel ?(no_additional_vars=false) name args_sorts =
150
  (* Enriching arg_sorts with two new variables: a counting index and an
151
     uid *)
152
  let args_sorts =
153
    if no_additional_vars then args_sorts else idx_sort::uid_sort::args_sorts in
154 2f7c9195 ploc
  
155
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
156 4300981b ploc
  if !debug then
157
    Format.eprintf "Registering fdecl %s (%a)@."
158
      name
159
      (Utils.fprintf_list ~sep:"@ "
160
	 (fun fmt sort -> Format.fprintf fmt "%s" (Z3.Sort.to_string sort)))
161
      args_sorts
162
  ;
163 c1785a55 ploc
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
164 5778dd5e ploc
  Z3.Fixedpoint.register_relation !fp fdecl;
165 c1785a55 ploc
  register_fdecl name fdecl;
166
  fdecl
167
  
168
169 7d77632f ploc
170
(* Shared variables to describe counter and uid *)
171
172
let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int
173
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) 
174
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int
175
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort 
176
let _ = register_fdecl "__uid__"  uid_fd  
177
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd 
178
179 e4edf171 ploc
(** Conversion functions
180 c1785a55 ploc
181 9f3de818 ploc
    The following is similar to the Horn backend. Each printing function is
182
    rephrased from pp_xx to xx_to_expr and produces a Z3 value.
183 c1785a55 ploc
184 9f3de818 ploc
*)
185 c1785a55 ploc
186
187
(* Returns the f_decl associated to the variable v *)
188
let horn_var_to_expr v =
189
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
190
191
192
193
194
  (* Used to print boolean constants *)
195
let horn_tag_to_expr t =
196
  if t = Corelang.tag_true then
197
    Z3.Boolean.mk_true !ctx
198
  else if t = Corelang.tag_false then
199
    Z3.Boolean.mk_false !ctx
200
  else
201
    (* Finding the associated sort *)
202
    let sort = get_tag_sort t in
203
    let elems = get_sort_elems sort in 
204
    let res : Z3.Expr.expr option =
205
      List.fold_left2 (fun res cst expr ->
206
          match res with
207
          | Some _ -> res
208
          | None -> if t = cst then Some (expr:Z3.Expr.expr) else None
209
        ) None elems (Z3.Enumeration.get_consts sort)
210
    in
211
    match res with None -> assert false | Some s -> s
212
    
213
(* Prints a constant value *)
214
let rec horn_const_to_expr c =
215
  match c with
216
    | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
217
    | Const_real (_,_,s)   -> Z3.Arithmetic.Real.mk_numeral_i !ctx 0
218
    | Const_tag t    -> horn_tag_to_expr t
219
    | _              -> assert false
220
221
222
223
(* Default value for each type, used when building arrays. Eg integer array
224
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
225
   for the type integer (arrays).
226
*)
227
let rec horn_default_val t =
228
  let t = Types.dynamic_type t in
229
  if Types.is_bool_type t  then Z3.Boolean.mk_true !ctx else
230
  if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
231
  if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
232
  (* match (Types.dynamic_type t).Types.tdesc with
233
   * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\)
234
   *    let valt = Types.array_element_type t in
235
   *    fprintf fmt "((as const (Array Int %a)) %a)"
236
   *      pp_type valt 
237
   *      pp_default_val valt
238
   * | Types.Tstruct(l) -> assert false
239
   * | Types.Ttuple(l) -> assert false
240
   * |_ -> *) assert false
241
242 e4edf171 ploc
(* Conversion of basic library functions *)
243
    
244 c1785a55 ploc
let horn_basic_app i val_to_expr vl =
245
  match i, vl with
246
  | "ite", [v1; v2; v3] ->
247
     Z3.Boolean.mk_ite
248
       !ctx
249
       (val_to_expr v1)
250
       (val_to_expr v2)
251
       (val_to_expr v3)
252
253
  | "uminus", [v] ->
254
     Z3.Arithmetic.mk_unary_minus
255
       !ctx
256
       (val_to_expr v)
257
  | "not", [v] ->
258
     Z3.Boolean.mk_not
259
       !ctx
260
       (val_to_expr v)
261
  | "=", [v1; v2] ->
262
     Z3.Boolean.mk_eq
263
       !ctx
264
       (val_to_expr v1)
265
       (val_to_expr v2)
266
  | "&&", [v1; v2] ->
267
     Z3.Boolean.mk_and
268
       !ctx
269
       [val_to_expr v1;
270
        val_to_expr v2]
271
  | "||", [v1; v2] ->
272
          Z3.Boolean.mk_or
273
       !ctx
274
       [val_to_expr v1;
275
        val_to_expr v2]
276
277
  | "impl", [v1; v2] ->
278
     Z3.Boolean.mk_implies
279
       !ctx
280
       (val_to_expr v1)
281
       (val_to_expr v2)
282
 | "mod", [v1; v2] ->
283
          Z3.Arithmetic.Integer.mk_mod
284
       !ctx
285
       (val_to_expr v1)
286
       (val_to_expr v2)
287
  | "equi", [v1; v2] ->
288
          Z3.Boolean.mk_eq
289
       !ctx
290
       (val_to_expr v1)
291
       (val_to_expr v2)
292
  | "xor", [v1; v2] ->
293
          Z3.Boolean.mk_xor
294
       !ctx
295
       (val_to_expr v1)
296
       (val_to_expr v2)
297
  | "!=", [v1; v2] ->
298
     Z3.Boolean.mk_not
299
       !ctx
300
       (
301
         Z3.Boolean.mk_eq
302
           !ctx
303
           (val_to_expr v1)
304
           (val_to_expr v2)
305
       )
306
  | "/", [v1; v2] ->
307
     Z3.Arithmetic.mk_div
308
       !ctx
309
       (val_to_expr v1)
310
       (val_to_expr v2)
311
312 46cb4020 ploc
  | "+", [v1; v2] ->
313
     Z3.Arithmetic.mk_add
314
       !ctx
315
       [val_to_expr v1; val_to_expr v2]
316
317
  | "-", [v1; v2] ->
318
     Z3.Arithmetic.mk_sub
319
       !ctx
320
       [val_to_expr v1 ; val_to_expr v2]
321
       
322
  | "*", [v1; v2] ->
323
     Z3.Arithmetic.mk_mul
324
       !ctx
325
       [val_to_expr v1; val_to_expr v2]
326
327
328
  | "<", [v1; v2] ->
329
     Z3.Arithmetic.mk_lt
330
       !ctx
331
       (val_to_expr v1)
332
       (val_to_expr v2)
333
334
  | "<=", [v1; v2] ->
335
     Z3.Arithmetic.mk_le
336
       !ctx
337
       (val_to_expr v1)
338
       (val_to_expr v2)
339
340
  | ">", [v1; v2] ->
341
     Z3.Arithmetic.mk_gt
342
       !ctx
343
       (val_to_expr v1)
344
       (val_to_expr v2)
345
346
  | ">=", [v1; v2] ->
347
     Z3.Arithmetic.mk_ge
348
       !ctx
349
       (val_to_expr v1)
350
       (val_to_expr v2)
351
352
       
353 c1785a55 ploc
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
354
   *      !ctx
355
   *      (val_to_expr v1)
356
   *      (val_to_expr v2)
357
   * 
358
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
359
  | _ -> (
360
    Format.eprintf
361
      "internal error: zustre unkown function %s@." i;
362
    assert false)
363
364
           
365 9f3de818 ploc
(* Convert a value expression [v], with internal function calls only.  [pp_var]
366
   is a printer for variables (typically [pp_c_var_read]), but an offset suffix
367
   may be added for array variables
368 c1785a55 ploc
*)
369 51106b7e ploc
let rec horn_val_to_expr ?(is_lhs=false) m self v =
370 c1785a55 ploc
  match v.value_desc with
371
  | Cst c       -> horn_const_to_expr c
372
373
  (* Code specific for arrays *)
374
  | Array il    ->
375
     (* An array definition: 
376
	(store (
377
	  ...
378
 	    (store (
379
	       store (
380
	          default_val
381
	       ) 
382
	       idx_n val_n
383
	    ) 
384
	    idx_n-1 val_n-1)
385
	  ... 
386
	  idx_1 val_1
387
	) *)
388
     let rec build_array (tab, x) =
389
       match tab with
390
       | [] -> horn_default_val v.value_type(* (get_type v) *)
391
       | h::t ->
392
	  Z3.Z3Array.mk_store
393
            !ctx
394
	    (build_array (t, (x+1)))
395
	    (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
396 51106b7e ploc
	    (horn_val_to_expr ~is_lhs:is_lhs m self h)
397 c1785a55 ploc
     in
398
     build_array (il, 0)
399 51106b7e ploc
     
400 c1785a55 ploc
  | Access(tab,index) ->
401
     Z3.Z3Array.mk_select !ctx 
402 51106b7e ploc
       (horn_val_to_expr ~is_lhs:is_lhs m self tab)
403
       (horn_val_to_expr ~is_lhs:is_lhs m self index)
404 c1785a55 ploc
405
  (* Code specific for arrays *)
406
    
407
  | Power (v, n)  -> assert false
408 51106b7e ploc
  | Var v    ->
409
     if is_memory m v then
410
       if Types.is_array_type v.var_type
411
       then assert false
412
       else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
413
     
414
     else 
415
       horn_var_to_expr
416
         (rename_machine
417
            self
418
            v)
419
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr m self) vl
420 c1785a55 ploc
421
let no_reset_to_exprs machines m i =
422
  let (n,_) = List.assoc i m.minstances in
423
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
424 ad4774b0 ploc
425 c1785a55 ploc
  let m_list = 
426
    rename_machine_list
427
      (concat m.mname.node_id i)
428
      (rename_mid_list (full_memory_vars machines target_machine))
429
  in
430
  let c_list =
431
    rename_machine_list
432
      (concat m.mname.node_id i)
433
      (rename_current_list (full_memory_vars machines target_machine))
434
  in
435
  match c_list, m_list with
436
  | [chd], [mhd] ->
437
     let expr =
438
       Z3.Boolean.mk_eq !ctx 
439
         (horn_var_to_expr mhd)
440
         (horn_var_to_expr chd)
441
     in
442
     [expr]
443
  | _ -> (
444
    let exprs =
445
      List.map2 (fun mhd chd -> 
446
          Z3.Boolean.mk_eq !ctx 
447
            (horn_var_to_expr mhd)
448
            (horn_var_to_expr chd)
449
        )
450
        m_list
451
        c_list
452
    in
453
    exprs
454
  )
455
456
let instance_reset_to_exprs machines m i =
457
  let (n,_) = List.assoc i m.minstances in
458
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
459
  let vars =
460 7d77632f ploc
    (rename_machine_list
461
       (concat m.mname.node_id i)
462
       (rename_current_list (full_memory_vars machines target_machine))@  (rename_mid_list (full_memory_vars machines target_machine))
463 c1785a55 ploc
    )
464 7d77632f ploc
    
465 c1785a55 ploc
  in
466
  let expr =
467
    Z3.Expr.mk_app
468
      !ctx
469
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
470 7d77632f ploc
      (List.map (horn_var_to_expr) (idx::uid::vars))
471 c1785a55 ploc
  in
472
  [expr]
473
474
let instance_call_to_exprs machines reset_instances m i inputs outputs =
475
  let self = m.mname.node_id in
476 7d77632f ploc
477
  (* Building call args *)
478
  let idx_uid_inout =
479
    (* Additional input to register step counters, and uid *)
480
    let idx = horn_var_to_expr idx in
481
    let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in
482
    let inout = 
483 51106b7e ploc
      List.map (horn_val_to_expr m self)
484
	(inputs @ (List.map (fun v -> mk_val (Var v) v.var_type) outputs))
485 7d77632f ploc
    in
486
    idx::uid::inout
487
  in
488
    
489 c1785a55 ploc
  try (* stateful node instance *)
490
    begin
491
      let (n,_) = List.assoc i m.minstances in
492
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
493
494
      (* Checking whether this specific instances has been reset yet *)
495
      let reset_exprs = 
496
        if not (List.mem i reset_instances) then
497
	  (* If not, declare mem_m = mem_c *)
498
	  no_reset_to_exprs machines m i
499
        else
500
          [] (* Nothing to add yet *)
501
      in
502
      
503
      let mems = full_memory_vars machines target_machine in
504
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
505
      let mid_mems = rename_mems rename_mid_list in
506
      let next_mems = rename_mems rename_next_list in
507
508
      let call_expr = 
509 7d77632f ploc
	match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
510
	| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
511 c1785a55 ploc
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
512
            Z3.Boolean.mk_eq !ctx
513
              ( (* output var *)
514 51106b7e ploc
                horn_val_to_expr 
515 c1785a55 ploc
                  ~is_lhs:true
516 51106b7e ploc
                  m self
517
                  (mk_val (Var o) o.var_type)
518 c1785a55 ploc
              )
519
              (
520
                Z3.Boolean.mk_ite !ctx 
521
	          (horn_var_to_expr mem_m) 
522 51106b7e ploc
	          (horn_val_to_expr m self i1)
523
	          (horn_val_to_expr m self i2)
524 c1785a55 ploc
              )
525
          in
526
          let stmt2 = (* mem_X = false *)
527
            Z3.Boolean.mk_eq !ctx
528
	      (horn_var_to_expr mem_x)
529
              (Z3.Boolean.mk_false !ctx)
530
          in
531
          [stmt1; stmt2]
532 7d77632f ploc
	end
533
534
	| node_name_n ->
535
           let expr = 
536
             Z3.Expr.mk_app
537
               !ctx
538
               (get_fdecl (machine_step_name (node_name n)))
539
               ( (* Arguments are input, output, mid_mems, next_mems *)
540
		 idx_uid_inout @ List.map (horn_var_to_expr) (mid_mems@next_mems)
541
		    
542
               )
543
           in
544
           [expr]
545 c1785a55 ploc
      in
546
547
      reset_exprs@call_expr
548
    end
549
  with Not_found -> ( (* stateless node instance *)
550
    let (n,_) = List.assoc i m.mcalls in
551
    let expr = 
552
      Z3.Expr.mk_app
553
        !ctx
554
        (get_fdecl (machine_stateless_name (node_name n)))
555 7d77632f ploc
        idx_uid_inout 	  (* Arguments are inputs, outputs *)
556 c1785a55 ploc
    in
557
    [expr]
558
  )
559 e4edf171 ploc
560
561
    
562
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
563
(* let rec value_suffix_to_expr self value = *)
564
(*  match value.value_desc with *)
565
(*  | Fun (n, vl)  ->  *)
566
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
567 c1785a55 ploc
    
568 e4edf171 ploc
(*  |  _            -> *)
569
(*    horn_val_to_expr self value *)
570
571 c1785a55 ploc
572 e4edf171 ploc
(* type_directed assignment: array vs. statically sized type
573
   - [var_type]: type of variable to be assigned
574
   - [var_name]: name of variable to be assigned
575
   - [value]: assigned value
576
   - [pp_var]: printer for variables
577
*)
578
let assign_to_exprs m var_name value =
579
  let self = m.mname.node_id in
580
  let e =
581
    Z3.Boolean.mk_eq
582
      !ctx
583 51106b7e ploc
      (horn_val_to_expr ~is_lhs:true m self var_name)
584
      (horn_val_to_expr m self value)
585 e4edf171 ploc
  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
586
  in
587
  [e]
588
589
    
590 c1785a55 ploc
(* Convert instruction to Z3.Expr and update the set of reset instances *)
591 e4edf171 ploc
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
592 ff2d7a82 ploc
  match Corelang.get_instr_desc instr with
593 c1785a55 ploc
  | MComment _ -> [], reset_instances
594
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
595
    no_reset_to_exprs machines m i,
596
    i::reset_instances
597
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
598
    instance_reset_to_exprs machines m i,
599
    i::reset_instances
600
  | MLocalAssign (i,v) ->
601
    assign_to_exprs
602 e4edf171 ploc
      m  
603 51106b7e ploc
      (mk_val (Var i) i.var_type) v,
604 c1785a55 ploc
    reset_instances
605
  | MStateAssign (i,v) ->
606
    assign_to_exprs
607 e4edf171 ploc
      m 
608 51106b7e ploc
      (mk_val (Var i) i.var_type) v,
609 c1785a55 ploc
    reset_instances
610
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
611
    assert false (* This should not happen anymore *)
612
  | MStep (il, i, vl) ->
613
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
614
       mem_c and print the call to mem_m *)
615
    instance_call_to_exprs machines reset_instances m i vl il,
616
    reset_instances (* Since this instance call will only happen once, we
617
		       don't have to update reset_instances *)
618
619
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
620
			 should not be produced yet. Later, we will have to
621
			 compare the reset_instances of each branch and
622
			 introduced the mem_m = mem_c for branches to do not
623
			 address it while other did. Am I clear ? *)
624
    (* For each branch we obtain the logical encoding, and the information
625
       whether a sub node has been reset or not. If a node has been reset in one
626
       of the branch, then all others have to have the mem_m = mem_c
627
       statement. *)
628
    let self = m.mname.node_id in
629
    let branch_to_expr (tag, instrs) =
630 e4edf171 ploc
      let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in
631
      let e =
632
	Z3.Boolean.mk_implies !ctx
633
          (Z3.Boolean.mk_eq !ctx 
634 51106b7e ploc
             (horn_val_to_expr m self g)
635 e4edf171 ploc
	     (horn_tag_to_expr tag))
636
          branch_def in
637
638
      [e], branch_resets
639
	  
640 c1785a55 ploc
    in
641 e4edf171 ploc
    List.fold_left (fun (instrs, resets) b ->
642
      let b_instrs, b_resets = branch_to_expr b in
643
      instrs@b_instrs, resets@b_resets 
644
    ) ([], reset_instances) hl 
645 c1785a55 ploc
646
and instrs_to_expr machines reset_instances m instrs = 
647 e4edf171 ploc
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
648
  let e_list, rs = 
649
    match instrs with
650
    | [x] -> instr_to_exprs reset_instances x 
651
    | _::_ -> (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *)
652
       
653
       List.fold_left (fun (exprs, rs) i -> 
654
         let exprs_i, rs_i = instr_to_exprs rs i in
655
         exprs@exprs_i, rs@rs_i
656
       )
657
         ([], reset_instances) instrs 
658
	 
659
	 
660
    | [] -> [], reset_instances
661
  in
662
  let e = 
663
    match e_list with
664
    | [e] -> e
665
    | [] -> Z3.Boolean.mk_true !ctx
666
    | _ -> Z3.Boolean.mk_and !ctx e_list
667
  in
668
  e, rs
669 ff2d7a82 ploc
670 51ec4e8c ploc
671
(*********************************************************)
672
673
(* Quantifiying universally all occuring variables *)
674
let add_rule ?(dont_touch=[]) vars  expr =
675
  (* let fds = Z3.Expr.get_args expr in *)
676
  (* Format.eprintf "Expr %s: args: [%a]@." *)
677
  (*   (Z3.Expr.to_string expr) *)
678
  (*   (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *)
679
680
  (* (\* Old code relying on provided vars *\) *)
681
  (* let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in *)
682
  (* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *)
683
  
684
  (* New code: we extract vars from expr *)
685
  let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl
686
				      let compare = compare
687
				      let hash = Hashtbl.hash
688
  end)
689
  in
690
  let rec get_expr_vars e =
691
    let open Utils in
692
    let nb_args = Z3.Expr.get_num_args e in
693
    if nb_args <= 0 then (
694
      let fdecl = Z3.Expr.get_func_decl e in
695
      (* let params = Z3.FuncDecl.get_parameters fdecl in *)
696 dbab1fe5 ploc
      (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *)
697 51ec4e8c ploc
      let dkind = Z3.FuncDecl.get_decl_kind fdecl in
698
      match dkind with Z3enums.OP_UNINTERPRETED -> (
699
	(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
700
	(* let open Z3.FuncDecl.Parameter in *)
701
	(* List.iter (fun p -> *)
702
	(*   match p with *)
703
        (*     P_Int i -> Format.eprintf "int %i" i *)
704
	(*   | P_Dbl f -> Format.eprintf "dbl %f" f *)
705
	(*   | P_Sym s -> Format.eprintf "symb"  *)
706
	(*   | P_Srt s -> Format.eprintf "sort"  *)
707
	(*   | P_Ast _ ->Format.eprintf "ast"  *)
708
	(*   | P_Fdl f -> Format.eprintf "fundecl"  *)
709
	(*   | P_Rat s -> Format.eprintf "rat %s" s  *)
710
	     
711
	(* ) params; *)
712
	(* Format.eprintf "]@."; *)
713
	FDSet.singleton fdecl
714
      )
715
      | _ -> FDSet.empty
716
    )
717
    else (*if nb_args > 0 then*)
718
      List.fold_left
719
	(fun accu e ->  FDSet.union accu (get_expr_vars e))
720
	FDSet.empty (Z3.Expr.get_args e)
721
  in
722
  let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in
723
  let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
724
  let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
725
726 4300981b ploc
  if !debug then (
727
    Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."
728
      (Z3.Expr.to_string expr)
729
      (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars)
730
  )
731
    ;
732 51ec4e8c ploc
  let expr = Z3.Quantifier.mk_forall_const
733
    !ctx  (* context *)
734
    (List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *)
735
    (* sorts           (\* sort list*\) *)
736
    (* symbols (\* symbol list *\) *)
737
    expr (* expression *)
738
    None (* quantifier weight, None means 1 *)
739
    [] (* pattern list ? *)
740
    [] (* ? *)
741
    None (* ? *)
742
    None (* ? *)
743
  in
744 dbab1fe5 ploc
  (* Format.eprintf "OK@.@?"; *)
745 51ec4e8c ploc
746 9f3de818 ploc
  (*
747
    TODO: bizarre la declaration de INIT tout seul semble poser pb.
748
  *) 
749 51ec4e8c ploc
  Z3.Fixedpoint.add_rule !fp
750
    (Z3.Quantifier.expr_of_quantifier expr)
751
    None
752
753 9f3de818 ploc
 
754 51ec4e8c ploc
(********************************************************)
755
    
756 e4edf171 ploc
let machine_reset machines m =
757
  let locals = local_memory_vars machines m in
758
  
759
  (* print "x_m = x_c" for each local memory *)
760
  let mid_mem_def =
761
    List.map (fun v ->
762
      Z3.Boolean.mk_eq !ctx
763
	(horn_var_to_expr (rename_mid v))
764
	(horn_var_to_expr (rename_current v))
765
    ) locals
766
  in
767 ff2d7a82 ploc
768 e4edf171 ploc
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
769
     Special treatment for _arrow: _first = true
770
  *)
771
772
  let reset_instances =
773
    
774
    List.map (fun (id, (n, _)) ->
775
      let name = node_name n in
776
      if name = "_arrow" then (
777
	Z3.Boolean.mk_eq !ctx
778
	  (
779
	    let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
780
	    Z3.Expr.mk_const_f !ctx vdecl
781
	  )
782
	  (Z3.Boolean.mk_true !ctx)
783
	  
784
      ) else (
785
	let machine_n = get_machine machines name in 
786
	
787
	Z3.Expr.mk_app
788
	  !ctx
789
	  (get_fdecl (name ^ "_reset"))
790
	  (List.map (horn_var_to_expr)
791 7d77632f ploc
	     (idx::uid:: (* Additional vars: counters, uid *)
792
	      	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
793
	  ))
794 e4edf171 ploc
	  
795
      )
796
    ) m.minstances
797
      
798
      
799 ff2d7a82 ploc
  in
800 e4edf171 ploc
  
801
  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
802
    
803
        
804 ff2d7a82 ploc
805 e4edf171 ploc
(*  TODO: empty list means true statement *)
806 ad4774b0 ploc
let decl_machine machines m =
807 e4edf171 ploc
  if m.mname.node_id = Arrow.arrow_id then
808
    (* We don't do arrow function *)
809 ad4774b0 ploc
    ()
810
  else
811
    begin
812 5778dd5e ploc
      let _ =
813
        List.map decl_var
814 c1785a55 ploc
      	  (
815 5778dd5e ploc
      	    (inout_vars machines m)@
816
      	      (rename_current_list (full_memory_vars machines m)) @
817
      	      (rename_mid_list (full_memory_vars machines m)) @
818
      	      (rename_next_list (full_memory_vars machines m)) @
819
      	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
820
      	  )
821 ad4774b0 ploc
      in
822
      if is_stateless m then
823
	begin
824 4300981b ploc
	  if !debug then 
825
	    Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id;
826
827 ad4774b0 ploc
	  (* Declaring single predicate *)
828 5778dd5e ploc
	  let vars = inout_vars machines m in
829 2f7c9195 ploc
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
830
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
831 4300981b ploc
	  
832 e4edf171 ploc
	  let horn_body, _ (* don't care for reset here *) =
833
	    instrs_to_expr
834
	      machines
835
	      ([] (* No reset info for stateless nodes *) )
836
	      m
837
	      m.mstep.step_instrs
838
	  in
839
	  let horn_head = 
840
	    Z3.Expr.mk_app
841
	      !ctx
842
	      (get_fdecl (machine_stateless_name m.mname.node_id))
843 7d77632f ploc
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
844 e4edf171 ploc
	  in
845 4300981b ploc
	  (* this line seems useless *)
846 7d77632f ploc
	  let vars = idx::uid::vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
847 4300981b ploc
	  (* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
848 e4edf171 ploc
	  match m.mstep.step_asserts with
849 ad4774b0 ploc
	  | [] ->
850
	     begin
851 e4edf171 ploc
	       (* Rule for single predicate : "; Stateless step rule @." *)
852 4300981b ploc
	       (*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*)
853
	       (* TODO clean code *)
854
	       (* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
855 5778dd5e ploc
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
856
		 
857 ad4774b0 ploc
	     end
858
	  | assertsl ->
859
	     begin
860 e4edf171 ploc
	       (*Rule for step "; Stateless step rule with Assertions @.";*)
861
	       let body_with_asserts =
862 51106b7e ploc
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
863 e4edf171 ploc
	       in
864 51ec4e8c ploc
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
865 5778dd5e ploc
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
866 ad4774b0 ploc
	     end
867
	end
868
      else
869
	begin
870
871
	  (* Rule for reset *)
872
873 5778dd5e ploc
	  let vars = reset_vars machines m in
874 2f7c9195 ploc
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
875
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in
876 e4edf171 ploc
	  let horn_reset_body = machine_reset machines m in	    
877
	  let horn_reset_head = 
878
	    Z3.Expr.mk_app
879
	      !ctx
880
	      (get_fdecl (machine_reset_name m.mname.node_id))
881 7d77632f ploc
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
882 e4edf171 ploc
	  in
883 51ec4e8c ploc
884 e4edf171 ploc
	  
885
	  let _ =
886 7d77632f ploc
	    add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
887 5778dd5e ploc
	      
888 e4edf171 ploc
	  in
889
890
	  (* Rule for step*)
891 5778dd5e ploc
	  let vars = step_vars machines m in
892 2f7c9195 ploc
  	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
893
          let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in
894 e4edf171 ploc
	  let horn_step_body, _ (* don't care for reset here *) =
895
	    instrs_to_expr
896
	      machines
897
	      []
898
	      m
899
	      m.mstep.step_instrs
900
	  in
901
	  let horn_step_head = 
902
	    Z3.Expr.mk_app
903
	      !ctx
904
	      (get_fdecl (machine_step_name m.mname.node_id))
905 7d77632f ploc
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
906 e4edf171 ploc
	  in
907
	  match m.mstep.step_asserts with
908 ad4774b0 ploc
	  | [] ->
909
	     begin
910 dbab1fe5 ploc
	       (* Rule for single predicate *) 
911
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
912 7d77632f ploc
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
913 5778dd5e ploc
		 
914 ad4774b0 ploc
	     end
915 e4edf171 ploc
	  | assertsl ->
916 ad4774b0 ploc
	     begin
917 e4edf171 ploc
	       (* Rule for step Assertions @.; *)
918
	       let body_with_asserts =
919
		 Z3.Boolean.mk_and !ctx
920 51106b7e ploc
		   (horn_step_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
921 e4edf171 ploc
	       in
922 dbab1fe5 ploc
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
923 7d77632f ploc
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
924 5778dd5e ploc
		 
925 ad4774b0 ploc
	     end
926
     	       
927
	end
928 c1785a55 ploc
    end
929 ad4774b0 ploc
930 c1785a55 ploc
931 51ec4e8c ploc
932
(* Debug functions *)
933
934
let rec extract_expr_fds e =
935 dbab1fe5 ploc
  (* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *)
936
  (*   (Z3.Expr.to_string e); *)
937 51ec4e8c ploc
  
938
  (* Removing quantifier is there are some *)
939
  let e = (* I didn't found a nicer way to do it than with an exception.  My
940
	     bad *)
941
    try
942
      let eq = Z3.Quantifier.quantifier_of_expr e in
943
      let e2 = Z3.Quantifier.get_body eq in
944 dbab1fe5 ploc
      (* Format.eprintf "Extracted quantifier body@ "; *)
945 51ec4e8c ploc
      e2
946
	
947
    with _ -> Format.eprintf "No quantifier info@ "; e
948
  in
949
  let _ =
950
    try 
951
    (
952
      let fd = Z3.Expr.get_func_decl e in
953
      let fd_symbol = Z3.FuncDecl.get_name fd in
954
      let fd_name = Z3.Symbol.to_string fd_symbol in
955
      if not (Hashtbl.mem decls fd_name) then
956
	register_fdecl fd_name fd;
957 dbab1fe5 ploc
      (* Format.eprintf "fdecls (%s): %s@ " *)
958
      (* 	fd_name *)
959
      (* 	(Z3.FuncDecl.to_string fd); *)
960 51ec4e8c ploc
      try
961
	(
962
	  let args = Z3.Expr.get_args e in
963 dbab1fe5 ploc
	  (* Format.eprintf "@[<v>@ "; *)
964
	  (* List.iter extract_expr_fds args; *)
965
	  (* Format.eprintf "@]@ "; *)
966
	  ()
967 51ec4e8c ploc
	)
968
      with _ ->
969
	Format.eprintf "Impossible to extract fundecl args for expression %s@ "
970
	  (Z3.Expr.to_string e)
971
    )
972
  with _ ->
973
    Format.eprintf "Impossible to extract anything from expression %s@ "
974
      (Z3.Expr.to_string e)
975
  in
976 dbab1fe5 ploc
  (* Format.eprintf "@]@ " *)
977
  ()      
978 51ec4e8c ploc
979 5778dd5e ploc
(* Local Variables: *)
980
(* compile-command:"make -C ../.." *)
981
(* End: *)