Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_common.ml @ a0c92fa8

History | View | Annotate | Download (29.6 KB)

1
open Lustre_types
2
open Machine_code_types
3
open Machine_code_common
4
open Format
5
(* open Horn_backend_common
6
 * open Horn_backend *)
7
open Zustre_data
8
  
9
let report = Log.report ~plugin:"z3 interface"
10
           
11
module HBC = Horn_backend_common
12
let node_name = HBC.node_name
13

    
14
let concat = HBC.concat
15

    
16
let rename_machine = HBC.rename_machine
17
let rename_machine_list = HBC.rename_machine_list
18

    
19
let rename_next = HBC.rename_next
20
let rename_mid = HBC.rename_mid
21
let rename_current = HBC.rename_current
22

    
23
let rename_current_list = HBC.rename_current_list
24
let rename_mid_list = HBC.rename_mid_list
25
let rename_next_list = HBC.rename_next_list
26

    
27
let full_memory_vars = HBC.full_memory_vars
28
let inout_vars = HBC.inout_vars
29
let reset_vars = HBC.reset_vars
30
let step_vars = HBC.step_vars
31
let local_memory_vars = HBC.local_memory_vars
32
let step_vars_m_x = HBC.step_vars_m_x
33
let step_vars_c_m_x = HBC.step_vars_c_m_x
34
  
35
let machine_reset_name = HBC.machine_reset_name 
36
let machine_step_name = HBC.machine_step_name 
37
let machine_stateless_name = HBC.machine_stateless_name 
38

    
39
let preprocess = Horn_backend.preprocess
40
  
41

    
42
exception UnknownFunction of (string * (Format.formatter -> unit))
43
(** Sorts
44

    
45
A sort is introduced for each basic type and each enumerated type.
46

    
47
A hashtbl records these and allow easy access to sort values, when
48
   provided with a enumerated type name. 
49

    
50
*)
51
        
52
let bool_sort = Z3.Boolean.mk_sort !ctx
53
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
54
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
55

    
56

    
57
let get_const_sort = Hashtbl.find const_sorts  
58
let get_sort_elems = Hashtbl.find sort_elems
59
let get_tag_sort id = try Hashtbl.find const_tags id with _ -> Format.eprintf "Unable to find sort for tag=%s@." id; assert false
60
  
61

    
62
  
63
let decl_sorts () =
64
  Hashtbl.iter (fun typ decl ->
65
    match typ with
66
    | Tydec_const var ->
67
      (match decl.top_decl_desc with
68
      | TypeDef tdef -> (
69
	match tdef.tydef_desc with
70
	| Tydec_enum tl ->
71
	  let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
72
          Hashtbl.add const_sorts var new_sort;
73
          Hashtbl.add sort_elems new_sort tl;
74
          List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl
75
          
76
	| _ -> Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false
77
      )
78
      | _ -> assert false
79
      )
80
    | _        -> ()) Corelang.type_table
81

    
82
                 
83
let rec type_to_sort t =
84
  if Types.is_bool_type t  then bool_sort else
85
    if Types.is_int_type t then int_sort else 
86
  if Types.is_real_type t then real_sort else 
87
  match (Types.repr t).Types.tdesc with
88
  | Types.Tconst ty       -> get_const_sort ty
89
  | Types.Tclock t        -> type_to_sort t
90
  | Types.Tarray(dim,ty)   -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
91
  | Types.Tstatic(d, ty)-> type_to_sort ty
92
  | Types.Tarrow _
93
  | _                     -> Format.eprintf "internal error: pp_type %a@."
94
                               Types.print_ty t; assert false
95

    
96

    
97
(* let idx_var = *)
98
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort  *)
99
    
100
(* let uid_var = *)
101
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort  *)
102

    
103
(** Func decls
104

    
105
    Similarly fun_decls are registerd, by their name, into a hashtbl. The
106
    proposed encoding introduces a 0-ary fun_decl to model variables and
107
    fun_decl with arguments to declare reset and step predicates.
108

    
109

    
110

    
111
*)
112
let register_fdecl id fd = Hashtbl.add decls id fd
113
let get_fdecl id =
114
  try
115
    Hashtbl.find decls id
116
  with Not_found -> (report ~level:3 (fun fmt -> Format.fprintf fmt  "Unable to find func_decl %s@.@?" id); raise Not_found)
117

    
118
let pp_fdecls fmt =
119
  Format.fprintf fmt "Registered fdecls: @[%a@]@ "
120
    (Utils.fprintf_list ~sep:"@ " Format.pp_print_string)  (Hashtbl.fold (fun id _ accu -> id::accu) decls [])
121

    
122
    
123
let decl_var id =
124
  (* Format.eprintf "Declaring var %s@." id.var_id; *)
125
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
126
  register_fdecl id.var_id fdecl;
127
  fdecl
128

    
129
(* Declaring the function used in expr *) 
130
let decl_fun op args typ =
131
  let args = List.map type_to_sort args in
132
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in
133
  register_fdecl op fdecl;
134
  fdecl
135

    
136
let idx_sort = int_sort
137
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort
138
let uid_conc = 
139
  let fd = Z3.Z3List.get_cons_decl uid_sort in
140
  fun head tail -> Z3.FuncDecl.apply fd [head;tail]
141

    
142
let get_instance_uid =
143
  let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in
144
  let cpt = ref 0 in
145
  fun i ->
146
    let id =
147
      if Hashtbl.mem hash i then
148
	Hashtbl.find hash i
149
      else (
150
	incr cpt;
151
	Hashtbl.add hash i !cpt;
152
	!cpt
153
      )
154
    in
155
    Z3.Arithmetic.Integer.mk_numeral_i !ctx id
156
  
157

    
158
  
159
let decl_rel ?(no_additional_vars=false) name args_sorts =
160
  (* Enriching arg_sorts with two new variables: a counting index and an
161
     uid *)
162
  let args_sorts =
163
    if no_additional_vars then args_sorts else idx_sort::uid_sort::args_sorts in
164
  
165
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
166
  if !debug then
167
    Format.eprintf "Registering fdecl %s (%a)@."
168
      name
169
      (Utils.fprintf_list ~sep:"@ "
170
	 (fun fmt sort -> Format.fprintf fmt "%s" (Z3.Sort.to_string sort)))
171
      args_sorts
172
  ;
173
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
174
  Z3.Fixedpoint.register_relation !fp fdecl;
175
  register_fdecl name fdecl;
176
  fdecl
177
  
178

    
179

    
180
(* Shared variables to describe counter and uid *)
181

    
182
let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int
183
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) 
184
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int
185
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort 
186
let _ = register_fdecl "__uid__"  uid_fd  
187
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd 
188

    
189
(** Conversion functions
190

    
191
    The following is similar to the Horn backend. Each printing function is
192
    rephrased from pp_xx to xx_to_expr and produces a Z3 value.
193

    
194
*)
195

    
196

    
197
(* Returns the f_decl associated to the variable v *)
198
let horn_var_to_expr v =
199
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
200

    
201

    
202

    
203

    
204
  (* Used to print boolean constants *)
205
let horn_tag_to_expr t =
206
  if t = tag_true then
207
    Z3.Boolean.mk_true !ctx
208
  else if t = tag_false then
209
    Z3.Boolean.mk_false !ctx
210
  else
211
    (* Finding the associated sort *)
212
    let sort = get_tag_sort t in
213
    let elems = get_sort_elems sort in 
214
    let res : Z3.Expr.expr option =
215
      List.fold_left2 (fun res cst expr ->
216
          match res with
217
          | Some _ -> res
218
          | None -> if t = cst then Some (expr:Z3.Expr.expr) else None
219
        ) None elems (Z3.Enumeration.get_consts sort)
220
    in
221
    match res with None -> assert false | Some s -> s
222
    
223
(* Prints a constant value *)
224
let rec horn_const_to_expr c =
225
  match c with
226
    | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
227
    | Const_real r  -> Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r)
228
    | Const_tag t    -> horn_tag_to_expr t
229
    | _              -> assert false
230

    
231

    
232

    
233
(* Default value for each type, used when building arrays. Eg integer array
234
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
235
   for the type integer (arrays).
236
*)
237
let rec horn_default_val t =
238
  let t = Types.dynamic_type t in
239
  if Types.is_bool_type t  then Z3.Boolean.mk_true !ctx else
240
  if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
241
  if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
242
  (* match (Types.dynamic_type t).Types.tdesc with
243
   * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\)
244
   *    let valt = Types.array_element_type t in
245
   *    fprintf fmt "((as const (Array Int %a)) %a)"
246
   *      pp_type valt 
247
   *      pp_default_val valt
248
   * | Types.Tstruct(l) -> assert false
249
   * | Types.Ttuple(l) -> assert false
250
   * |_ -> *) assert false
251

    
252
(* Conversion of basic library functions *)
253
    
254
let horn_basic_app i vl (vltyp, typ) =
255
  match i, vl with
256
  | "ite", [v1; v2; v3] ->  Z3.Boolean.mk_ite !ctx v1 v2 v3
257
  | "uminus", [v] ->    Z3.Arithmetic.mk_unary_minus
258
       !ctx v
259
  | "not", [v] ->
260
     Z3.Boolean.mk_not
261
       !ctx v
262
  | "=", [v1; v2] ->
263
     Z3.Boolean.mk_eq
264
       !ctx v1 v2
265
  | "&&", [v1; v2] ->
266
     Z3.Boolean.mk_and
267
       !ctx
268
       [v1; v2]
269
  | "||", [v1; v2] ->
270
          Z3.Boolean.mk_or
271
       !ctx
272
       [v1;
273
         v2]
274

    
275
  | "impl", [v1; v2] ->
276
     Z3.Boolean.mk_implies
277
       !ctx v1 v2
278
 | "mod", [v1; v2] ->
279
          Z3.Arithmetic.Integer.mk_mod
280
       !ctx v1 v2
281
  | "equi", [v1; v2] ->
282
          Z3.Boolean.mk_eq
283
       !ctx
284
       v1 v2
285
  | "xor", [v1; v2] ->
286
          Z3.Boolean.mk_xor
287
       !ctx v1 v2
288
  | "!=", [v1; v2] ->
289
     Z3.Boolean.mk_not
290
       !ctx
291
       (
292
         Z3.Boolean.mk_eq
293
           !ctx v1 v2
294
       )
295
  | "/", [v1; v2] ->
296
     Z3.Arithmetic.mk_div
297
       !ctx v1 v2
298

    
299
  | "+", [v1; v2] ->
300
     Z3.Arithmetic.mk_add
301
       !ctx
302
       [v1; v2]
303
  | "-", [v1; v2] ->
304
     Z3.Arithmetic.mk_sub
305
       !ctx
306
       [v1 ;  v2]
307
       
308
  | "*", [v1; v2] ->
309
     Z3.Arithmetic.mk_mul
310
       !ctx
311
       [ v1;  v2]
312

    
313

    
314
  | "<", [v1; v2] ->
315
     Z3.Arithmetic.mk_lt
316
       !ctx v1 v2
317
  | "<=", [v1; v2] ->
318
     Z3.Arithmetic.mk_le
319
       !ctx v1 v2
320
  | ">", [v1; v2] ->
321
     Z3.Arithmetic.mk_gt
322
       !ctx v1 v2
323
  | ">=", [v1; v2] ->
324
     Z3.Arithmetic.mk_ge
325
       !ctx v1 v2
326
  | "int_to_real", [v1] ->
327
     Z3.Arithmetic.Integer.mk_int2real
328
       !ctx v1
329
  | _ ->
330
     let fd =
331
       try
332
         get_fdecl i
333
       with Not_found -> begin
334
           report ~level:3 (fun fmt -> Format.fprintf fmt "Registering function %s as uninterpreted function in Z3@.%s: (%a) -> %a" i i (Utils.fprintf_list ~sep:"," Types.print_ty) vltyp Types.print_ty typ); 
335
           decl_fun i vltyp typ
336
         end
337
     in
338
     Z3.FuncDecl.apply fd vl
339
    
340
     
341
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
342
   *      !ctx
343
   *      (val_to_expr v1)
344
   *      (val_to_expr v2)
345
   * 
346
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
347

    
348
(* | _ -> (
349
 *     let msg fmt = Format.fprintf fmt
350
 *                     "internal error: zustre unkown function %s (nb args = %i)@."
351
 *                     i (List.length vl)
352
 *     in
353
 *     raise (UnknownFunction(i, msg))
354
 *   ) *)
355

    
356
           
357
(* Convert a value expression [v], with internal function calls only.  [pp_var]
358
   is a printer for variables (typically [pp_c_var_read]), but an offset suffix
359
   may be added for array variables
360
*)
361
let rec horn_val_to_expr ?(is_lhs=false) m self v =
362
  (* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *)
363
  match v.value_desc with
364
  | Cst c       -> horn_const_to_expr c
365

    
366
  (* Code specific for arrays *)
367
  | Array il    ->
368
     (* An array definition: 
369
	(store (
370
	  ...
371
 	    (store (
372
	       store (
373
	          default_val
374
	       ) 
375
	       idx_n val_n
376
	    ) 
377
	    idx_n-1 val_n-1)
378
	  ... 
379
	  idx_1 val_1
380
	) *)
381
     let rec build_array (tab, x) =
382
       match tab with
383
       | [] -> horn_default_val v.value_type(* (get_type v) *)
384
       | h::t ->
385
	  Z3.Z3Array.mk_store
386
            !ctx
387
	    (build_array (t, (x+1)))
388
	    (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
389
	    (horn_val_to_expr ~is_lhs:is_lhs m self h)
390
     in
391
     build_array (il, 0)
392
     
393
  | Access(tab,index) ->
394
     Z3.Z3Array.mk_select !ctx 
395
       (horn_val_to_expr ~is_lhs:is_lhs m self tab)
396
       (horn_val_to_expr ~is_lhs:is_lhs m self index)
397

    
398
  (* Code specific for arrays *)
399
    
400
  | Power (v, n)  -> assert false
401
  | Var v    ->
402
     if is_memory m v then
403
       if Types.is_array_type v.var_type
404
       then assert false
405
       else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
406
     
407
     else 
408
       horn_var_to_expr
409
         (rename_machine
410
            self
411
            v)
412
  | Fun (n, vl)   -> horn_basic_app n (List.map (horn_val_to_expr m self) vl) (List.map (fun v -> v.value_type) vl, v.value_type)
413

    
414
let no_reset_to_exprs machines m i =
415
  let (n,_) = List.assoc i m.minstances in
416
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
417

    
418
  let m_list = 
419
    rename_machine_list
420
      (concat m.mname.node_id i)
421
      (rename_mid_list (full_memory_vars machines target_machine))
422
  in
423
  let c_list =
424
    rename_machine_list
425
      (concat m.mname.node_id i)
426
      (rename_current_list (full_memory_vars machines target_machine))
427
  in
428
  match c_list, m_list with
429
  | [chd], [mhd] ->
430
     let expr =
431
       Z3.Boolean.mk_eq !ctx 
432
         (horn_var_to_expr mhd)
433
         (horn_var_to_expr chd)
434
     in
435
     [expr]
436
  | _ -> (
437
    let exprs =
438
      List.map2 (fun mhd chd -> 
439
          Z3.Boolean.mk_eq !ctx 
440
            (horn_var_to_expr mhd)
441
            (horn_var_to_expr chd)
442
        )
443
        m_list
444
        c_list
445
    in
446
    exprs
447
  )
448

    
449
let instance_reset_to_exprs machines m i =
450
  let (n,_) = List.assoc i m.minstances in
451
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
452
  let vars =
453
    (rename_machine_list
454
       (concat m.mname.node_id i)
455
       (rename_current_list (full_memory_vars machines target_machine))@  (rename_mid_list (full_memory_vars machines target_machine))
456
    )
457
    
458
  in
459
  let expr =
460
    Z3.Expr.mk_app
461
      !ctx
462
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
463
      (List.map (horn_var_to_expr) (idx::uid::vars))
464
  in
465
  [expr]
466

    
467
let instance_call_to_exprs machines reset_instances m i inputs outputs =
468
  let self = m.mname.node_id in
469

    
470
  (* Building call args *)
471
  let idx_uid_inout =
472
    (* Additional input to register step counters, and uid *)
473
    let idx = horn_var_to_expr idx in
474
    let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in
475
    let inout = 
476
      List.map (horn_val_to_expr m self)
477
	(inputs @ (List.map (fun v -> mk_val (Var v) v.var_type) outputs))
478
    in
479
    idx::uid::inout
480
  in
481
    
482
  try (* stateful node instance *)
483
    begin
484
      let (n,_) = List.assoc i m.minstances in
485
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
486

    
487
      (* Checking whether this specific instances has been reset yet *)
488
      let reset_exprs = 
489
        if not (List.mem i reset_instances) then
490
	  (* If not, declare mem_m = mem_c *)
491
	  no_reset_to_exprs machines m i
492
        else
493
          [] (* Nothing to add yet *)
494
      in
495
      
496
      let mems = full_memory_vars machines target_machine in
497
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
498
      let mid_mems = rename_mems rename_mid_list in
499
      let next_mems = rename_mems rename_next_list in
500

    
501
      let call_expr = 
502
	match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
503
	| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
504
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
505
            Z3.Boolean.mk_eq !ctx
506
              ( (* output var *)
507
                horn_val_to_expr 
508
                  ~is_lhs:true
509
                  m self
510
                  (mk_val (Var o) o.var_type)
511
              )
512
              (
513
                Z3.Boolean.mk_ite !ctx 
514
	          (horn_var_to_expr mem_m) 
515
	          (horn_val_to_expr m self i1)
516
	          (horn_val_to_expr m self i2)
517
              )
518
          in
519
          let stmt2 = (* mem_X = false *)
520
            Z3.Boolean.mk_eq !ctx
521
	      (horn_var_to_expr mem_x)
522
              (Z3.Boolean.mk_false !ctx)
523
          in
524
          [stmt1; stmt2]
525
	end
526

    
527
	| node_name_n ->
528
           let expr = 
529
             Z3.Expr.mk_app
530
               !ctx
531
               (get_fdecl (machine_step_name (node_name n)))
532
               ( (* Arguments are input, output, mid_mems, next_mems *)
533
		 idx_uid_inout @ List.map (horn_var_to_expr) (mid_mems@next_mems)
534
		    
535
               )
536
           in
537
           [expr]
538
      in
539

    
540
      reset_exprs@call_expr
541
    end
542
  with Not_found -> ( (* stateless node instance *)
543
    let (n,_) = List.assoc i m.mcalls in
544
    let expr = 
545
      Z3.Expr.mk_app
546
        !ctx
547
        (get_fdecl (machine_stateless_name (node_name n)))
548
        idx_uid_inout 	  (* Arguments are inputs, outputs *)
549
    in
550
    [expr]
551
  )
552

    
553

    
554
    
555
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
556
(* let rec value_suffix_to_expr self value = *)
557
(*  match value.value_desc with *)
558
(*  | Fun (n, vl)  ->  *)
559
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
560
    
561
(*  |  _            -> *)
562
(*    horn_val_to_expr self value *)
563

    
564

    
565
(* type_directed assignment: array vs. statically sized type
566
   - [var_type]: type of variable to be assigned
567
   - [var_name]: name of variable to be assigned
568
   - [value]: assigned value
569
   - [pp_var]: printer for variables
570
*)
571
let assign_to_exprs m var_name value =
572
  let self = m.mname.node_id in
573
  let e =
574
    Z3.Boolean.mk_eq
575
      !ctx
576
      (horn_val_to_expr ~is_lhs:true m self var_name)
577
      (horn_val_to_expr m self value)
578
  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
579
  in
580
  [e]
581

    
582
    
583
(* Convert instruction to Z3.Expr and update the set of reset instances *)
584
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
585
  match Corelang.get_instr_desc instr with
586
  | MComment _ -> [], reset_instances
587
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
588
    no_reset_to_exprs machines m i,
589
    i::reset_instances
590
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
591
    instance_reset_to_exprs machines m i,
592
    i::reset_instances
593
  | MLocalAssign (i,v) ->
594
    assign_to_exprs
595
      m  
596
      (mk_val (Var i) i.var_type) v,
597
    reset_instances
598
  | MStateAssign (i,v) ->
599
    assign_to_exprs
600
      m 
601
      (mk_val (Var i) i.var_type) v,
602
    reset_instances
603
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
604
    assert false (* This should not happen anymore *)
605
  | MStep (il, i, vl) ->
606
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
607
       mem_c and print the call to mem_m *)
608
    instance_call_to_exprs machines reset_instances m i vl il,
609
    reset_instances (* Since this instance call will only happen once, we
610
		       don't have to update reset_instances *)
611

    
612
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
613
			 should not be produced yet. Later, we will have to
614
			 compare the reset_instances of each branch and
615
			 introduced the mem_m = mem_c for branches to do not
616
			 address it while other did. Am I clear ? *)
617
    (* For each branch we obtain the logical encoding, and the information
618
       whether a sub node has been reset or not. If a node has been reset in one
619
       of the branch, then all others have to have the mem_m = mem_c
620
       statement. *)
621
    let self = m.mname.node_id in
622
    let branch_to_expr (tag, instrs) =
623
      let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in
624
      let e =
625
	Z3.Boolean.mk_implies !ctx
626
          (Z3.Boolean.mk_eq !ctx 
627
             (horn_val_to_expr m self g)
628
	     (horn_tag_to_expr tag))
629
          branch_def in
630

    
631
      [e], branch_resets
632
	  
633
    in
634
    List.fold_left (fun (instrs, resets) b ->
635
      let b_instrs, b_resets = branch_to_expr b in
636
      instrs@b_instrs, resets@b_resets 
637
      ) ([], reset_instances) hl
638
  | MSpec _ -> assert false
639

    
640
and instrs_to_expr machines reset_instances m instrs = 
641
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
642
  let e_list, rs = 
643
    match instrs with
644
    | [x] -> instr_to_exprs reset_instances x 
645
    | _::_ -> (* 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 *)
646
       
647
       List.fold_left (fun (exprs, rs) i -> 
648
         let exprs_i, rs_i = instr_to_exprs rs i in
649
         exprs@exprs_i, rs@rs_i
650
       )
651
         ([], reset_instances) instrs 
652
	 
653
	 
654
    | [] -> [], reset_instances
655
  in
656
  let e = 
657
    match e_list with
658
    | [e] -> e
659
    | [] -> Z3.Boolean.mk_true !ctx
660
    | _ -> Z3.Boolean.mk_and !ctx e_list
661
  in
662
  e, rs
663

    
664

    
665
(*********************************************************)
666

    
667
(* Quantifiying universally all occuring variables *)
668
let add_rule ?(dont_touch=[]) vars  expr =
669
  (* let fds = Z3.Expr.get_args expr in *)
670
  (* Format.eprintf "Expr %s: args: [%a]@." *)
671
  (*   (Z3.Expr.to_string expr) *)
672
  (*   (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *)
673

    
674
  (* (\* Old code relying on provided vars *\) *)
675
  (* let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in *)
676
  (* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *)
677
  
678
  (* New code: we extract vars from expr *)
679
  let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl
680
				      let compare = compare
681
				      let hash = Hashtbl.hash
682
  end)
683
  in
684
(* Fonction seems unused 
685

    
686
  let rec get_expr_vars e =
687
    let open Utils in
688
    let nb_args = Z3.Expr.get_num_args e in
689
    if nb_args <= 0 then (
690
      let fdecl = Z3.Expr.get_func_decl e in
691
      (* let params = Z3.FuncDecl.get_parameters fdecl in *)
692
      (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *)
693
      let dkind = Z3.FuncDecl.get_decl_kind fdecl in
694
      match dkind with Z3enums.OP_UNINTERPRETED -> (
695
	(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
696
	(* let open Z3.FuncDecl.Parameter in *)
697
	(* List.iter (fun p -> *)
698
	(*   match p with *)
699
        (*     P_Int i -> Format.eprintf "int %i" i *)
700
	(*   | P_Dbl f -> Format.eprintf "dbl %f" f *)
701
	(*   | P_Sym s -> Format.eprintf "symb"  *)
702
	(*   | P_Srt s -> Format.eprintf "sort"  *)
703
	(*   | P_Ast _ ->Format.eprintf "ast"  *)
704
	(*   | P_Fdl f -> Format.eprintf "fundecl"  *)
705
	(*   | P_Rat s -> Format.eprintf "rat %s" s  *)
706
	     
707
	(* ) params; *)
708
	(* Format.eprintf "]@."; *)
709
	FDSet.singleton fdecl
710
      )
711
      | _ -> FDSet.empty
712
    )
713
    else (*if nb_args > 0 then*)
714
      List.fold_left
715
	(fun accu e ->  FDSet.union accu (get_expr_vars e))
716
	FDSet.empty (Z3.Expr.get_args e)
717
  in
718
 *)
719
  (* Unsed variable. Coul;d be reintroduced 
720
  let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in
721
  let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
722
  let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
723
   *)
724
  if !debug then (
725
    Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."
726
      (Z3.Expr.to_string expr)
727
      (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars)
728
  )
729
    ;
730
  let expr = Z3.Quantifier.mk_forall_const
731
    !ctx  (* context *)
732
    (List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *)
733
    (* sorts           (\* sort list*\) *)
734
    (* symbols (\* symbol list *\) *)
735
    expr (* expression *)
736
    None (* quantifier weight, None means 1 *)
737
    [] (* pattern list ? *)
738
    [] (* ? *)
739
    None (* ? *)
740
    None (* ? *)
741
  in
742
  (* Format.eprintf "OK@.@?"; *)
743

    
744
  (*
745
    TODO: bizarre la declaration de INIT tout seul semble poser pb.
746
  *) 
747
  Z3.Fixedpoint.add_rule !fp
748
    (Z3.Quantifier.expr_of_quantifier expr)
749
    None
750

    
751
 
752
(********************************************************)
753
    
754
let machine_reset machines m =
755
  let locals = local_memory_vars machines m in
756
  
757
  (* print "x_m = x_c" for each local memory *)
758
  let mid_mem_def =
759
    List.map (fun v ->
760
      Z3.Boolean.mk_eq !ctx
761
	(horn_var_to_expr (rename_mid v))
762
	(horn_var_to_expr (rename_current v))
763
    ) locals
764
  in
765

    
766
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
767
     Special treatment for _arrow: _first = true
768
  *)
769

    
770
  let reset_instances =
771
    
772
    List.map (fun (id, (n, _)) ->
773
      let name = node_name n in
774
      if name = "_arrow" then (
775
	Z3.Boolean.mk_eq !ctx
776
	  (
777
	    let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
778
	    Z3.Expr.mk_const_f !ctx vdecl
779
	  )
780
	  (Z3.Boolean.mk_true !ctx)
781
	  
782
      ) else (
783
	let machine_n = get_machine machines name in 
784
	
785
	Z3.Expr.mk_app
786
	  !ctx
787
	  (get_fdecl (name ^ "_reset"))
788
	  (List.map (horn_var_to_expr)
789
	     (idx::uid:: (* Additional vars: counters, uid *)
790
	      	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
791
	  ))
792
	  
793
      )
794
    ) m.minstances
795
      
796
      
797
  in
798
  
799
  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
800
    
801
        
802

    
803
(*  TODO: empty list means true statement *)
804
let decl_machine machines m =
805
  if m.mname.node_id = Arrow.arrow_id then
806
    (* We don't do arrow function *)
807
    ()
808
  else
809
    begin
810
      let _ =
811
        List.map decl_var
812
      	  (
813
      	    (inout_vars machines m)@
814
      	      (rename_current_list (full_memory_vars machines m)) @
815
      	      (rename_mid_list (full_memory_vars machines m)) @
816
      	      (rename_next_list (full_memory_vars machines m)) @
817
      	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
818
      	  )
819
      in
820
      if is_stateless m then
821
	begin
822
	  if !debug then 
823
	    Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id;
824

    
825
	  (* Declaring single predicate *)
826
	  let vars = inout_vars machines m in
827
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
828
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
829
	  
830
	  let horn_body, _ (* don't care for reset here *) =
831
	    instrs_to_expr
832
	      machines
833
	      ([] (* No reset info for stateless nodes *) )
834
	      m
835
	      m.mstep.step_instrs
836
	  in
837
	  let horn_head = 
838
	    Z3.Expr.mk_app
839
	      !ctx
840
	      (get_fdecl (machine_stateless_name m.mname.node_id))
841
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
842
	  in
843
	  (* this line seems useless *)
844
	  let vars = idx::uid::vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
845
	  (* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
846
	  match m.mstep.step_asserts with
847
	  | [] ->
848
	     begin
849
	       (* Rule for single predicate : "; Stateless step rule @." *)
850
	       (*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*)
851
	       (* TODO clean code *)
852
	       (* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
853
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
854
		 
855
	     end
856
	  | assertsl ->
857
	     begin
858
	       (*Rule for step "; Stateless step rule with Assertions @.";*)
859
	       let body_with_asserts =
860
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
861
	       in
862
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
863
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
864
	     end
865
	end
866
      else
867
	begin
868

    
869
	  (* Rule for reset *)
870

    
871
	  let vars = reset_vars machines m in
872
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
873
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in
874
	  let horn_reset_body = machine_reset machines m in	    
875
	  let horn_reset_head = 
876
	    Z3.Expr.mk_app
877
	      !ctx
878
	      (get_fdecl (machine_reset_name m.mname.node_id))
879
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
880
	  in
881

    
882
	  
883
	  let _ =
884
	    add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
885
	      
886
	  in
887

    
888
	  (* Rule for step*)
889
	  let vars = step_vars machines m in
890
  	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
891
          let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in
892
	  let horn_step_body, _ (* don't care for reset here *) =
893
	    instrs_to_expr
894
	      machines
895
	      []
896
	      m
897
	      m.mstep.step_instrs
898
	  in
899
	  let horn_step_head = 
900
	    Z3.Expr.mk_app
901
	      !ctx
902
	      (get_fdecl (machine_step_name m.mname.node_id))
903
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
904
	  in
905
	  match m.mstep.step_asserts with
906
	  | [] ->
907
	     begin
908
	       (* Rule for single predicate *) 
909
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
910
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
911
		 
912
	     end
913
	  | assertsl ->
914
	     begin
915
	       (* Rule for step Assertions @.; *)
916
	       let body_with_asserts =
917
		 Z3.Boolean.mk_and !ctx
918
		   (horn_step_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
919
	       in
920
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
921
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
922
		 
923
	     end
924
     	       
925
	end
926
    end
927

    
928

    
929

    
930
(* Debug functions *)
931
(*
932
let rec extract_expr_fds e =
933
  (* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *)
934
  (*   (Z3.Expr.to_string e); *)
935
  
936
  (* Removing quantifier is there are some *)
937
  let e = (* I didn't found a nicer way to do it than with an exception.  My
938
	     bad *)
939
    try
940
      let eq = Z3.Quantifier.quantifier_of_expr e in
941
      let e2 = Z3.Quantifier.get_body eq in
942
      (* Format.eprintf "Extracted quantifier body@ "; *)
943
      e2
944
	
945
    with _ -> Format.eprintf "No quantifier info@ "; e
946
  in
947
  let _ =
948
    try 
949
    (
950
      let fd = Z3.Expr.get_func_decl e in
951
      let fd_symbol = Z3.FuncDecl.get_name fd in
952
      let fd_name = Z3.Symbol.to_string fd_symbol in
953
      if not (Hashtbl.mem decls fd_name) then
954
	register_fdecl fd_name fd;
955
      (* Format.eprintf "fdecls (%s): %s@ " *)
956
      (* 	fd_name *)
957
      (* 	(Z3.FuncDecl.to_string fd); *)
958
      try
959
	(
960
	  let args = Z3.Expr.get_args e in
961
	  (* Format.eprintf "@[<v>@ "; *)
962
	  (* List.iter extract_expr_fds args; *)
963
	  (* Format.eprintf "@]@ "; *)
964
	  ()
965
	)
966
      with _ ->
967
	Format.eprintf "Impossible to extract fundecl args for expression %s@ "
968
	  (Z3.Expr.to_string e)
969
    )
970
  with _ ->
971
    Format.eprintf "Impossible to extract anything from expression %s@ "
972
      (Z3.Expr.to_string e)
973
  in
974
  (* Format.eprintf "@]@ " *)
975
  ()      
976
 *)
977
(* Local Variables: *)
978
(* compile-command:"make -C ../.." *)
979
(* End: *)