Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (26.8 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
module HBC = Horn_backend_common
10
let node_name = HBC.node_name
11

    
12
let concat = HBC.concat
13

    
14
let rename_machine = HBC.rename_machine
15
let rename_machine_list = HBC.rename_machine_list
16

    
17
let rename_next = HBC.rename_next
18
let rename_mid = HBC.rename_mid
19
let rename_current = HBC.rename_current
20

    
21
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

    
25
let full_memory_vars = HBC.full_memory_vars
26
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
let step_vars_m_x = HBC.step_vars_m_x
31
let step_vars_c_m_x = HBC.step_vars_c_m_x
32
  
33
let machine_reset_name = HBC.machine_reset_name 
34
let machine_step_name = HBC.machine_step_name 
35
let machine_stateless_name = HBC.machine_stateless_name 
36

    
37
let preprocess = Horn_backend.preprocess
38
  
39
  
40
(** Sorts
41

    
42
A sort is introduced for each basic type and each enumerated type.
43

    
44
A hashtbl records these and allow easy access to sort values, when
45
   provided with a enumerated type name. 
46

    
47
*)
48
        
49
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

    
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

    
59
  
60
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
          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
	| _ -> Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false
74
      )
75
      | _ -> assert false
76
      )
77
    | _        -> ()) Corelang.type_table
78

    
79
                 
80
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
(** Func decls
94

    
95
    Similarly fun_decls are registerd, by their name, into a hashtbl. The
96
    proposed encoding introduces a 0-ary fun_decl to model variables and
97
    fun_decl with arguments to declare reset and step predicates.
98

    
99

    
100

    
101
*)
102
let register_fdecl id fd = Hashtbl.add decls id fd
103
let get_fdecl id =
104
  try
105
    Hashtbl.find decls id
106
  with Not_found -> (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found)
107

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

    
112
    
113
let decl_var id =
114
  (* Format.eprintf "Declaring var %s@." id.var_id; *)
115
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
116
  register_fdecl id.var_id fdecl;
117
  fdecl
118

    
119
let decl_rel name args =
120
  (*verifier ce qui est construit. On veut un declare-rel *)
121
  let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in
122
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
123
  Z3.Fixedpoint.register_relation !fp fdecl;
124
  register_fdecl name fdecl;
125
  fdecl
126
  
127

    
128
(** Conversion functions
129

    
130
    The following is similar to the Horn backend. Each printing function is
131
    rephrased from pp_xx to xx_to_expr and produces a Z3 value.
132

    
133
*)
134

    
135

    
136
(* Returns the f_decl associated to the variable v *)
137
let horn_var_to_expr v =
138
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
139

    
140

    
141

    
142

    
143
  (* Used to print boolean constants *)
144
let horn_tag_to_expr t =
145
  if t = Corelang.tag_true then
146
    Z3.Boolean.mk_true !ctx
147
  else if t = Corelang.tag_false then
148
    Z3.Boolean.mk_false !ctx
149
  else
150
    (* Finding the associated sort *)
151
    let sort = get_tag_sort t in
152
    let elems = get_sort_elems sort in 
153
    let res : Z3.Expr.expr option =
154
      List.fold_left2 (fun res cst expr ->
155
          match res with
156
          | Some _ -> res
157
          | None -> if t = cst then Some (expr:Z3.Expr.expr) else None
158
        ) None elems (Z3.Enumeration.get_consts sort)
159
    in
160
    match res with None -> assert false | Some s -> s
161
    
162
(* Prints a constant value *)
163
let rec horn_const_to_expr c =
164
  match c with
165
    | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
166
    | Const_real (_,_,s)   -> Z3.Arithmetic.Real.mk_numeral_i !ctx 0
167
    | Const_tag t    -> horn_tag_to_expr t
168
    | _              -> assert false
169

    
170

    
171

    
172
(* Default value for each type, used when building arrays. Eg integer array
173
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
174
   for the type integer (arrays).
175
*)
176
let rec horn_default_val t =
177
  let t = Types.dynamic_type t in
178
  if Types.is_bool_type t  then Z3.Boolean.mk_true !ctx else
179
  if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
180
  if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
181
  (* match (Types.dynamic_type t).Types.tdesc with
182
   * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\)
183
   *    let valt = Types.array_element_type t in
184
   *    fprintf fmt "((as const (Array Int %a)) %a)"
185
   *      pp_type valt 
186
   *      pp_default_val valt
187
   * | Types.Tstruct(l) -> assert false
188
   * | Types.Ttuple(l) -> assert false
189
   * |_ -> *) assert false
190

    
191
(* Conversion of basic library functions *)
192
    
193
let horn_basic_app i val_to_expr vl =
194
  match i, vl with
195
  | "ite", [v1; v2; v3] ->
196
     Z3.Boolean.mk_ite
197
       !ctx
198
       (val_to_expr v1)
199
       (val_to_expr v2)
200
       (val_to_expr v3)
201

    
202
  | "uminus", [v] ->
203
     Z3.Arithmetic.mk_unary_minus
204
       !ctx
205
       (val_to_expr v)
206
  | "not", [v] ->
207
     Z3.Boolean.mk_not
208
       !ctx
209
       (val_to_expr v)
210
  | "=", [v1; v2] ->
211
     Z3.Boolean.mk_eq
212
       !ctx
213
       (val_to_expr v1)
214
       (val_to_expr v2)
215
  | "&&", [v1; v2] ->
216
     Z3.Boolean.mk_and
217
       !ctx
218
       [val_to_expr v1;
219
        val_to_expr v2]
220
  | "||", [v1; v2] ->
221
          Z3.Boolean.mk_or
222
       !ctx
223
       [val_to_expr v1;
224
        val_to_expr v2]
225

    
226
  | "impl", [v1; v2] ->
227
     Z3.Boolean.mk_implies
228
       !ctx
229
       (val_to_expr v1)
230
       (val_to_expr v2)
231
 | "mod", [v1; v2] ->
232
          Z3.Arithmetic.Integer.mk_mod
233
       !ctx
234
       (val_to_expr v1)
235
       (val_to_expr v2)
236
  | "equi", [v1; v2] ->
237
          Z3.Boolean.mk_eq
238
       !ctx
239
       (val_to_expr v1)
240
       (val_to_expr v2)
241
  | "xor", [v1; v2] ->
242
          Z3.Boolean.mk_xor
243
       !ctx
244
       (val_to_expr v1)
245
       (val_to_expr v2)
246
  | "!=", [v1; v2] ->
247
     Z3.Boolean.mk_not
248
       !ctx
249
       (
250
         Z3.Boolean.mk_eq
251
           !ctx
252
           (val_to_expr v1)
253
           (val_to_expr v2)
254
       )
255
  | "/", [v1; v2] ->
256
     Z3.Arithmetic.mk_div
257
       !ctx
258
       (val_to_expr v1)
259
       (val_to_expr v2)
260

    
261
  | "+", [v1; v2] ->
262
     Z3.Arithmetic.mk_add
263
       !ctx
264
       [val_to_expr v1; val_to_expr v2]
265

    
266
  | "-", [v1; v2] ->
267
     Z3.Arithmetic.mk_sub
268
       !ctx
269
       [val_to_expr v1 ; val_to_expr v2]
270
       
271
  | "*", [v1; v2] ->
272
     Z3.Arithmetic.mk_mul
273
       !ctx
274
       [val_to_expr v1; val_to_expr v2]
275

    
276

    
277
  | "<", [v1; v2] ->
278
     Z3.Arithmetic.mk_lt
279
       !ctx
280
       (val_to_expr v1)
281
       (val_to_expr v2)
282

    
283
  | "<=", [v1; v2] ->
284
     Z3.Arithmetic.mk_le
285
       !ctx
286
       (val_to_expr v1)
287
       (val_to_expr v2)
288

    
289
  | ">", [v1; v2] ->
290
     Z3.Arithmetic.mk_gt
291
       !ctx
292
       (val_to_expr v1)
293
       (val_to_expr v2)
294

    
295
  | ">=", [v1; v2] ->
296
     Z3.Arithmetic.mk_ge
297
       !ctx
298
       (val_to_expr v1)
299
       (val_to_expr v2)
300

    
301
       
302
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
303
   *      !ctx
304
   *      (val_to_expr v1)
305
   *      (val_to_expr v2)
306
   * 
307
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
308
  | _ -> (
309
    Format.eprintf
310
      "internal error: zustre unkown function %s@." i;
311
    assert false)
312

    
313
           
314
(* Convert a value expression [v], with internal function calls only.  [pp_var]
315
   is a printer for variables (typically [pp_c_var_read]), but an offset suffix
316
   may be added for array variables
317
*)
318
let rec horn_val_to_expr ?(is_lhs=false) self v =
319
  match v.value_desc with
320
  | Cst c       -> horn_const_to_expr c
321

    
322
  (* Code specific for arrays *)
323
  | Array il    ->
324
     (* An array definition: 
325
	(store (
326
	  ...
327
 	    (store (
328
	       store (
329
	          default_val
330
	       ) 
331
	       idx_n val_n
332
	    ) 
333
	    idx_n-1 val_n-1)
334
	  ... 
335
	  idx_1 val_1
336
	) *)
337
     let rec build_array (tab, x) =
338
       match tab with
339
       | [] -> horn_default_val v.value_type(* (get_type v) *)
340
       | h::t ->
341
	  Z3.Z3Array.mk_store
342
            !ctx
343
	    (build_array (t, (x+1)))
344
	    (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
345
	    (horn_val_to_expr ~is_lhs:is_lhs self h)
346
     in
347
     build_array (il, 0)
348
       
349
  | Access(tab,index) ->
350
     Z3.Z3Array.mk_select !ctx 
351
       (horn_val_to_expr ~is_lhs:is_lhs self tab)
352
       (horn_val_to_expr ~is_lhs:is_lhs self index)
353

    
354
  (* Code specific for arrays *)
355
    
356
  | Power (v, n)  -> assert false
357
  | LocalVar v    ->
358
     horn_var_to_expr
359
       (rename_machine
360
          self
361
          v)
362
  | StateVar v    ->
363
     if Types.is_array_type v.var_type
364
     then assert false
365
     else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
366
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr self) vl
367

    
368
let no_reset_to_exprs machines m i =
369
  let (n,_) = List.assoc i m.minstances in
370
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
371

    
372
  let m_list = 
373
    rename_machine_list
374
      (concat m.mname.node_id i)
375
      (rename_mid_list (full_memory_vars machines target_machine))
376
  in
377
  let c_list =
378
    rename_machine_list
379
      (concat m.mname.node_id i)
380
      (rename_current_list (full_memory_vars machines target_machine))
381
  in
382
  match c_list, m_list with
383
  | [chd], [mhd] ->
384
     let expr =
385
       Z3.Boolean.mk_eq !ctx 
386
         (horn_var_to_expr mhd)
387
         (horn_var_to_expr chd)
388
     in
389
     [expr]
390
  | _ -> (
391
    let exprs =
392
      List.map2 (fun mhd chd -> 
393
          Z3.Boolean.mk_eq !ctx 
394
            (horn_var_to_expr mhd)
395
            (horn_var_to_expr chd)
396
        )
397
        m_list
398
        c_list
399
    in
400
    exprs
401
  )
402

    
403
let instance_reset_to_exprs machines m i =
404
  let (n,_) = List.assoc i m.minstances in
405
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
406
  let vars =
407
    (
408
      (rename_machine_list
409
	 (concat m.mname.node_id i)
410
	 (rename_current_list (full_memory_vars machines target_machine))
411
      ) 
412
      @
413
	(rename_machine_list
414
	   (concat m.mname.node_id i)
415
	   (rename_mid_list (full_memory_vars machines target_machine))
416
	)
417
    )
418
  in
419
  let expr =
420
    Z3.Expr.mk_app
421
      !ctx
422
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
423
      (List.map (horn_var_to_expr) vars)
424
  in
425
  [expr]
426

    
427
let instance_call_to_exprs machines reset_instances m i inputs outputs =
428
  let self = m.mname.node_id in
429
  try (* stateful node instance *)
430
    begin
431
      let (n,_) = List.assoc i m.minstances in
432
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
433

    
434
      (* Checking whether this specific instances has been reset yet *)
435
      let reset_exprs = 
436
        if not (List.mem i reset_instances) then
437
	  (* If not, declare mem_m = mem_c *)
438
	  no_reset_to_exprs machines m i
439
        else
440
          [] (* Nothing to add yet *)
441
      in
442
      
443
      let mems = full_memory_vars machines target_machine in
444
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
445
      let mid_mems = rename_mems rename_mid_list in
446
      let next_mems = rename_mems rename_next_list in
447

    
448
      let call_expr = 
449
      match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
450
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
451
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
452
            Z3.Boolean.mk_eq !ctx
453
              ( (* output var *)
454
                horn_val_to_expr
455
                  ~is_lhs:true
456
                  self
457
                  (mk_val (LocalVar o) o.var_type)
458
              )
459
              (
460
                Z3.Boolean.mk_ite !ctx 
461
	          (horn_var_to_expr mem_m) 
462
	          (horn_val_to_expr self i1)
463
	          (horn_val_to_expr self i2)
464
              )
465
          in
466
          let stmt2 = (* mem_X = false *)
467
            Z3.Boolean.mk_eq !ctx
468
	      (horn_var_to_expr mem_x)
469
              (Z3.Boolean.mk_false !ctx)
470
          in
471
          [stmt1; stmt2]
472
      end
473

    
474
      | node_name_n ->
475
         let expr = 
476
           Z3.Expr.mk_app
477
             !ctx
478
             (get_fdecl (machine_step_name (node_name n)))
479
             ( (* Arguments are input, output, mid_mems, next_mems *)
480
               (
481
                 List.map (horn_val_to_expr self) (
482
                     inputs @
483
	               (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
484
                   )
485
               ) @ (
486
                 List.map (horn_var_to_expr) (mid_mems@next_mems)
487
	       )
488
             )
489
         in
490
         [expr]
491
      in
492

    
493
      reset_exprs@call_expr
494
    end
495
  with Not_found -> ( (* stateless node instance *)
496
    let (n,_) = List.assoc i m.mcalls in
497
    let expr = 
498
      Z3.Expr.mk_app
499
        !ctx
500
        (get_fdecl (machine_stateless_name (node_name n)))
501
        ((* Arguments are inputs, outputs *)
502
         List.map (horn_val_to_expr self)
503
           (
504
             inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
505
           )
506
        )
507
    in
508
    [expr]
509
  )
510

    
511

    
512
    
513
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
514
(* let rec value_suffix_to_expr self value = *)
515
(*  match value.value_desc with *)
516
(*  | Fun (n, vl)  ->  *)
517
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
518
    
519
(*  |  _            -> *)
520
(*    horn_val_to_expr self value *)
521

    
522

    
523
(* type_directed assignment: array vs. statically sized type
524
   - [var_type]: type of variable to be assigned
525
   - [var_name]: name of variable to be assigned
526
   - [value]: assigned value
527
   - [pp_var]: printer for variables
528
*)
529
let assign_to_exprs m var_name value =
530
  let self = m.mname.node_id in
531
  let e =
532
    Z3.Boolean.mk_eq
533
      !ctx
534
      (horn_val_to_expr ~is_lhs:true self var_name)
535
      (horn_val_to_expr self value)
536
  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
537
  in
538
  [e]
539

    
540
    
541
(* Convert instruction to Z3.Expr and update the set of reset instances *)
542
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
543
  match Corelang.get_instr_desc instr with
544
  | MComment _ -> [], reset_instances
545
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
546
    no_reset_to_exprs machines m i,
547
    i::reset_instances
548
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
549
    instance_reset_to_exprs machines m i,
550
    i::reset_instances
551
  | MLocalAssign (i,v) ->
552
    assign_to_exprs
553
      m  
554
      (mk_val (LocalVar i) i.var_type) v,
555
    reset_instances
556
  | MStateAssign (i,v) ->
557
    assign_to_exprs
558
      m 
559
      (mk_val (StateVar i) i.var_type) v,
560
    reset_instances
561
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
562
    assert false (* This should not happen anymore *)
563
  | MStep (il, i, vl) ->
564
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
565
       mem_c and print the call to mem_m *)
566
    instance_call_to_exprs machines reset_instances m i vl il,
567
    reset_instances (* Since this instance call will only happen once, we
568
		       don't have to update reset_instances *)
569

    
570
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
571
			 should not be produced yet. Later, we will have to
572
			 compare the reset_instances of each branch and
573
			 introduced the mem_m = mem_c for branches to do not
574
			 address it while other did. Am I clear ? *)
575
    (* For each branch we obtain the logical encoding, and the information
576
       whether a sub node has been reset or not. If a node has been reset in one
577
       of the branch, then all others have to have the mem_m = mem_c
578
       statement. *)
579
    let self = m.mname.node_id in
580
    let branch_to_expr (tag, instrs) =
581
      let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in
582
      let e =
583
	Z3.Boolean.mk_implies !ctx
584
          (Z3.Boolean.mk_eq !ctx 
585
             (horn_val_to_expr self g)
586
	     (horn_tag_to_expr tag))
587
          branch_def in
588

    
589
      [e], branch_resets
590
	  
591
    in
592
    List.fold_left (fun (instrs, resets) b ->
593
      let b_instrs, b_resets = branch_to_expr b in
594
      instrs@b_instrs, resets@b_resets 
595
    ) ([], reset_instances) hl 
596

    
597
and instrs_to_expr machines reset_instances m instrs = 
598
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
599
  let e_list, rs = 
600
    match instrs with
601
    | [x] -> instr_to_exprs reset_instances x 
602
    | _::_ -> (* 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 *)
603
       
604
       List.fold_left (fun (exprs, rs) i -> 
605
         let exprs_i, rs_i = instr_to_exprs rs i in
606
         exprs@exprs_i, rs@rs_i
607
       )
608
         ([], reset_instances) instrs 
609
	 
610
	 
611
    | [] -> [], reset_instances
612
  in
613
  let e = 
614
    match e_list with
615
    | [e] -> e
616
    | [] -> Z3.Boolean.mk_true !ctx
617
    | _ -> Z3.Boolean.mk_and !ctx e_list
618
  in
619
  e, rs
620

    
621

    
622
(*********************************************************)
623

    
624
(* Quantifiying universally all occuring variables *)
625
let add_rule ?(dont_touch=[]) vars  expr =
626
  (* let fds = Z3.Expr.get_args expr in *)
627
  (* Format.eprintf "Expr %s: args: [%a]@." *)
628
  (*   (Z3.Expr.to_string expr) *)
629
  (*   (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *)
630

    
631
  (* (\* Old code relying on provided vars *\) *)
632
  (* let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in *)
633
  (* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *)
634
  
635
  (* New code: we extract vars from expr *)
636
  let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl
637
				      let compare = compare
638
				      let hash = Hashtbl.hash
639
  end)
640
  in
641
  let rec get_expr_vars e =
642
    let open Utils in
643
    let nb_args = Z3.Expr.get_num_args e in
644
    if nb_args <= 0 then (
645
      let fdecl = Z3.Expr.get_func_decl e in
646
      (* let params = Z3.FuncDecl.get_parameters fdecl in *)
647
      (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *)
648
      let dkind = Z3.FuncDecl.get_decl_kind fdecl in
649
      match dkind with Z3enums.OP_UNINTERPRETED -> (
650
	(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
651
	(* let open Z3.FuncDecl.Parameter in *)
652
	(* List.iter (fun p -> *)
653
	(*   match p with *)
654
        (*     P_Int i -> Format.eprintf "int %i" i *)
655
	(*   | P_Dbl f -> Format.eprintf "dbl %f" f *)
656
	(*   | P_Sym s -> Format.eprintf "symb"  *)
657
	(*   | P_Srt s -> Format.eprintf "sort"  *)
658
	(*   | P_Ast _ ->Format.eprintf "ast"  *)
659
	(*   | P_Fdl f -> Format.eprintf "fundecl"  *)
660
	(*   | P_Rat s -> Format.eprintf "rat %s" s  *)
661
	     
662
	(* ) params; *)
663
	(* Format.eprintf "]@."; *)
664
	FDSet.singleton fdecl
665
      )
666
      | _ -> FDSet.empty
667
    )
668
    else (*if nb_args > 0 then*)
669
      List.fold_left
670
	(fun accu e ->  FDSet.union accu (get_expr_vars e))
671
	FDSet.empty (Z3.Expr.get_args e)
672
  in
673
  let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in
674
  let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
675
  let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
676

    
677
  (* Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @." *)
678
  (*   (Z3.Expr.to_string expr) *)
679
  (*   (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars) *)
680
  (*   ; *)
681
  let expr = Z3.Quantifier.mk_forall_const
682
    !ctx  (* context *)
683
    (List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *)
684
    (* sorts           (\* sort list*\) *)
685
    (* symbols (\* symbol list *\) *)
686
    expr (* expression *)
687
    None (* quantifier weight, None means 1 *)
688
    [] (* pattern list ? *)
689
    [] (* ? *)
690
    None (* ? *)
691
    None (* ? *)
692
  in
693
  (* Format.eprintf "OK@.@?"; *)
694

    
695
  (*
696
    TODO: bizarre la declaration de INIT tout seul semble poser pb.
697
  *) 
698
  Z3.Fixedpoint.add_rule !fp
699
    (Z3.Quantifier.expr_of_quantifier expr)
700
    None
701

    
702
 
703
(********************************************************)
704
    
705
let machine_reset machines m =
706
  let locals = local_memory_vars machines m in
707
  
708
  (* print "x_m = x_c" for each local memory *)
709
  let mid_mem_def =
710
    List.map (fun v ->
711
      Z3.Boolean.mk_eq !ctx
712
	(horn_var_to_expr (rename_mid v))
713
	(horn_var_to_expr (rename_current v))
714
    ) locals
715
  in
716

    
717
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
718
     Special treatment for _arrow: _first = true
719
  *)
720

    
721
  let reset_instances =
722
    
723
    List.map (fun (id, (n, _)) ->
724
      let name = node_name n in
725
      if name = "_arrow" then (
726
	Z3.Boolean.mk_eq !ctx
727
	  (
728
	    let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
729
	    Z3.Expr.mk_const_f !ctx vdecl
730
	  )
731
	  (Z3.Boolean.mk_true !ctx)
732
	  
733
      ) else (
734
	let machine_n = get_machine machines name in 
735
	
736
	Z3.Expr.mk_app
737
	  !ctx
738
	  (get_fdecl (name ^ "_reset"))
739
	  (List.map (horn_var_to_expr)
740
	     (rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
741
	  )
742
	  
743
      )
744
    ) m.minstances
745
      
746
      
747
  in
748
  
749
  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
750
    
751
        
752

    
753
(*  TODO: empty list means true statement *)
754
let decl_machine machines m =
755
  if m.mname.node_id = Arrow.arrow_id then
756
    (* We don't do arrow function *)
757
    ()
758
  else
759
    begin
760
      let _ =
761
        List.map decl_var
762
      	  (
763
      	    (inout_vars machines m)@
764
      	      (rename_current_list (full_memory_vars machines m)) @
765
      	      (rename_mid_list (full_memory_vars machines m)) @
766
      	      (rename_next_list (full_memory_vars machines m)) @
767
      	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
768
      	  )
769
      in
770
      
771
      if is_stateless m then
772
	begin
773
	  (* Declaring single predicate *)
774
	  let vars = inout_vars machines m in
775
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars in
776
	  let horn_body, _ (* don't care for reset here *) =
777
	    instrs_to_expr
778
	      machines
779
	      ([] (* No reset info for stateless nodes *) )
780
	      m
781
	      m.mstep.step_instrs
782
	  in
783
	  let horn_head = 
784
	    Z3.Expr.mk_app
785
	      !ctx
786
	      (get_fdecl (machine_stateless_name m.mname.node_id))
787
	      (List.map (horn_var_to_expr) vars)
788
	  in
789
	  let vars = vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
790
	  match m.mstep.step_asserts with
791
	  | [] ->
792
	     begin
793
	       (* Rule for single predicate : "; Stateless step rule @." *)
794
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
795
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
796
		 
797
	     end
798
	  | assertsl ->
799
	     begin
800
	       (*Rule for step "; Stateless step rule with Assertions @.";*)
801
	       let body_with_asserts =
802
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
803
	       in
804
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
805
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
806
	     end
807
	end
808
      else
809
	begin
810

    
811
	  (* Rule for reset *)
812

    
813
	  let vars = reset_vars machines m in
814
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars in
815
	  let horn_reset_body = machine_reset machines m in	    
816
	  let horn_reset_head = 
817
	    Z3.Expr.mk_app
818
	      !ctx
819
	      (get_fdecl (machine_reset_name m.mname.node_id))
820
	      (List.map (horn_var_to_expr) vars)
821
	  in
822

    
823
	  
824
	  let _ =
825
	    add_rule vars (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
826
	      
827
	  in
828

    
829
	  (* Rule for step*)
830
	  let vars = step_vars machines m in
831
          let _ = decl_rel (machine_step_name m.mname.node_id) vars in
832
	  let horn_step_body, _ (* don't care for reset here *) =
833
	    instrs_to_expr
834
	      machines
835
	      []
836
	      m
837
	      m.mstep.step_instrs
838
	  in
839
	  let horn_step_head = 
840
	    Z3.Expr.mk_app
841
	      !ctx
842
	      (get_fdecl (machine_step_name m.mname.node_id))
843
	      (List.map (horn_var_to_expr) vars)
844
	  in
845
	  match m.mstep.step_asserts with
846
	  | [] ->
847
	     begin
848
	       (* Rule for single predicate *) 
849
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
850
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
851
		 
852
	     end
853
	  | assertsl ->
854
	     begin
855
	       (* Rule for step Assertions @.; *)
856
	       let body_with_asserts =
857
		 Z3.Boolean.mk_and !ctx
858
		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
859
	       in
860
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
861
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
862
		 
863
	     end
864
     	       
865
	end
866
    end
867

    
868

    
869

    
870
(* Debug functions *)
871

    
872
let rec extract_expr_fds e =
873
  (* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *)
874
  (*   (Z3.Expr.to_string e); *)
875
  
876
  (* Removing quantifier is there are some *)
877
  let e = (* I didn't found a nicer way to do it than with an exception.  My
878
	     bad *)
879
    try
880
      let eq = Z3.Quantifier.quantifier_of_expr e in
881
      let e2 = Z3.Quantifier.get_body eq in
882
      (* Format.eprintf "Extracted quantifier body@ "; *)
883
      e2
884
	
885
    with _ -> Format.eprintf "No quantifier info@ "; e
886
  in
887
  let _ =
888
    try 
889
    (
890
      let fd = Z3.Expr.get_func_decl e in
891
      let fd_symbol = Z3.FuncDecl.get_name fd in
892
      let fd_name = Z3.Symbol.to_string fd_symbol in
893
      if not (Hashtbl.mem decls fd_name) then
894
	register_fdecl fd_name fd;
895
      (* Format.eprintf "fdecls (%s): %s@ " *)
896
      (* 	fd_name *)
897
      (* 	(Z3.FuncDecl.to_string fd); *)
898
      try
899
	(
900
	  let args = Z3.Expr.get_args e in
901
	  (* Format.eprintf "@[<v>@ "; *)
902
	  (* List.iter extract_expr_fds args; *)
903
	  (* Format.eprintf "@]@ "; *)
904
	  ()
905
	)
906
      with _ ->
907
	Format.eprintf "Impossible to extract fundecl args for expression %s@ "
908
	  (Z3.Expr.to_string e)
909
    )
910
  with _ ->
911
    Format.eprintf "Impossible to extract anything from expression %s@ "
912
      (Z3.Expr.to_string e)
913
  in
914
  (* Format.eprintf "@]@ " *)
915
  ()      
916

    
917
(* Local Variables: *)
918
(* compile-command:"make -C ../.." *)
919
(* End: *)