Project

General

Profile

Download (29.3 KB) Statistics
| Branch: | Tag: | Revision:
1
open Lustre_types
2
open Machine_code_types
3
open Machine_code_common
4

    
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

    
13
let node_name = HBC.node_name
14

    
15
let concat = HBC.concat
16

    
17
let rename_machine = HBC.rename_machine
18

    
19
let rename_machine_list = HBC.rename_machine_list
20

    
21
let rename_next = HBC.rename_next
22

    
23
let rename_mid = HBC.rename_mid
24

    
25
let rename_current = HBC.rename_current
26

    
27
let rename_current_list = HBC.rename_current_list
28

    
29
let rename_mid_list = HBC.rename_mid_list
30

    
31
let rename_next_list = HBC.rename_next_list
32

    
33
let full_memory_vars = HBC.full_memory_vars
34

    
35
let inout_vars = HBC.inout_vars
36

    
37
let reset_vars = HBC.reset_vars
38

    
39
let step_vars = HBC.step_vars
40

    
41
let local_memory_vars = HBC.local_memory_vars
42

    
43
let step_vars_m_x = HBC.step_vars_m_x
44

    
45
let step_vars_c_m_x = HBC.step_vars_c_m_x
46

    
47
let machine_reset_name = HBC.machine_reset_name
48

    
49
let machine_step_name = HBC.machine_step_name
50

    
51
let machine_stateless_name = HBC.machine_stateless_name
52

    
53
let preprocess = Horn_backend.preprocess
54

    
55
exception UnknownFunction of (string * (Format.formatter -> unit))
56
(** Sorts
57

    
58
    A sort is introduced for each basic type and each enumerated type.
59

    
60
    A hashtbl records these and allow easy access to sort values, when provided
61
    with a enumerated type name. *)
62

    
63
let bool_sort = Z3.Boolean.mk_sort !ctx
64

    
65
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
66

    
67
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
68

    
69
let get_const_sort = Hashtbl.find const_sorts
70

    
71
let get_sort_elems = Hashtbl.find sort_elems
72

    
73
let get_tag_sort id =
74
  try Hashtbl.find const_tags id
75
  with _ ->
76
    Format.eprintf "Unable to find sort for tag=%s@." id;
77
    assert false
78

    
79
let decl_sorts () =
80
  Hashtbl.iter
81
    (fun typ decl ->
82
      match typ with
83
      | Tydec_const var -> (
84
        match decl.top_decl_desc with
85
        | TypeDef tdef -> (
86
          match tdef.tydef_desc with
87
          | Tydec_enum tl ->
88
            let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
89
            Hashtbl.add const_sorts var new_sort;
90
            Hashtbl.add sort_elems new_sort tl;
91
            List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl
92
          | _ ->
93
            Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc
94
              typ;
95
            assert false)
96
        | _ ->
97
          assert false)
98
      | _ ->
99
        ())
100
    Corelang.type_table
101

    
102
let rec type_to_sort t =
103
  if Types.is_bool_type t then bool_sort
104
  else if Types.is_int_type t then int_sort
105
  else if Types.is_real_type t then real_sort
106
  else
107
    match (Types.repr t).Types.tdesc with
108
    | Types.Tconst ty ->
109
      get_const_sort ty
110
    | Types.Tclock t ->
111
      type_to_sort t
112
    | Types.Tarray (_, ty) ->
113
      Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
114
    | Types.Tstatic (_, ty) ->
115
      type_to_sort ty
116
    | Types.Tarrow _ | _ ->
117
      Format.eprintf "internal error: pp_type %a@." Types.print_ty t;
118
      assert false
119

    
120
(* let idx_var = *)
121
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort  *)
122

    
123
(* let uid_var = *)
124
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort  *)
125

    
126
(** Func decls
127

    
128
    Similarly fun_decls are registerd, by their name, into a hashtbl. The
129
    proposed encoding introduces a 0-ary fun_decl to model variables and
130
    fun_decl with arguments to declare reset and step predicates. *)
131
let register_fdecl id fd = Hashtbl.add decls id fd
132

    
133
let get_fdecl id =
134
  try Hashtbl.find decls id
135
  with Not_found ->
136
    report ~level:3 (fun fmt ->
137
        Format.fprintf fmt "Unable to find func_decl %s@.@?" id);
138
    raise Not_found
139

    
140
let pp_fdecls fmt =
141
  Format.fprintf fmt "Registered fdecls: @[%a@]@ "
142
    (Utils.fprintf_list ~sep:"@ " Format.pp_print_string)
143
    (Hashtbl.fold (fun id _ accu -> id :: accu) decls [])
144

    
145
let decl_var id =
146
  (* Format.eprintf "Declaring var %s@." id.var_id; *)
147
  let fdecl =
148
    Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type)
149
  in
150
  register_fdecl id.var_id fdecl;
151
  fdecl
152

    
153
(* Declaring the function used in expr *)
154
let decl_fun op args typ =
155
  let args = List.map type_to_sort args in
156
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in
157
  register_fdecl op fdecl;
158
  fdecl
159

    
160
let idx_sort = int_sort
161

    
162
let uid_sort =
163
  Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort
164

    
165
let uid_conc =
166
  let fd = Z3.Z3List.get_cons_decl uid_sort in
167
  fun head tail -> Z3.FuncDecl.apply fd [ head; tail ]
168

    
169
let get_instance_uid =
170
  let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in
171
  let cpt = ref 0 in
172
  fun i ->
173
    let id =
174
      if Hashtbl.mem hash i then Hashtbl.find hash i
175
      else (
176
        incr cpt;
177
        Hashtbl.add hash i !cpt;
178
        !cpt)
179
    in
180
    Z3.Arithmetic.Integer.mk_numeral_i !ctx id
181

    
182
let decl_rel ?(no_additional_vars = false) name args_sorts =
183
  (* Enriching arg_sorts with two new variables: a counting index and an uid *)
184
  let args_sorts =
185
    if no_additional_vars then args_sorts
186
    else idx_sort :: uid_sort :: args_sorts
187
  in
188

    
189
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
190
  if !debug then
191
    Format.eprintf "Registering fdecl %s (%a)@." name
192
      (Utils.fprintf_list ~sep:"@ " (fun fmt sort ->
193
           Format.fprintf fmt "%s" (Z3.Sort.to_string sort)))
194
      args_sorts;
195
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
196
  Z3.Fixedpoint.register_relation !fp fdecl;
197
  register_fdecl name fdecl;
198
  fdecl
199

    
200
(* Shared variables to describe counter and uid *)
201

    
202
let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int
203

    
204
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx)
205

    
206
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int
207

    
208
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort
209

    
210
let _ = register_fdecl "__uid__" uid_fd
211

    
212
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd
213

    
214
(** Conversion functions
215

    
216
    The following is similar to the Horn backend. Each printing function is
217
    rephrased from pp_xx to xx_to_expr and produces a Z3 value. *)
218

    
219
(* Returns the f_decl associated to the variable v *)
220
let horn_var_to_expr v = Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
221

    
222
(* Used to print boolean constants *)
223
let horn_tag_to_expr t =
224
  if t = tag_true then Z3.Boolean.mk_true !ctx
225
  else if t = tag_false then Z3.Boolean.mk_false !ctx
226
  else
227
    (* Finding the associated sort *)
228
    let sort = get_tag_sort t in
229
    let elems = get_sort_elems sort in
230
    let res : Z3.Expr.expr option =
231
      List.fold_left2
232
        (fun res cst expr ->
233
          match res with
234
          | Some _ ->
235
            res
236
          | None ->
237
            if t = cst then Some (expr : Z3.Expr.expr) else None)
238
        None elems
239
        (Z3.Enumeration.get_consts sort)
240
    in
241
    match res with None -> assert false | Some s -> s
242

    
243
(* Prints a constant value *)
244
let horn_const_to_expr c =
245
  match c with
246
  | Const_int i ->
247
    Z3.Arithmetic.Integer.mk_numeral_i !ctx i
248
  | Const_real r ->
249
    Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r)
250
  | Const_tag t ->
251
    horn_tag_to_expr t
252
  | _ ->
253
    assert false
254

    
255
(* Default value for each type, used when building arrays. Eg integer array
256
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
257
   for the type integer (arrays). *)
258
let horn_default_val t =
259
  let t = Types.dynamic_type t in
260
  if Types.is_bool_type t then Z3.Boolean.mk_true !ctx
261
  else if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0
262
  else if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0
263
  else
264
    (* match (Types.dynamic_type t).Types.tdesc with
265
     * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\)
266
     *    let valt = Types.array_element_type t in
267
     *    fprintf fmt "((as const (Array Int %a)) %a)"
268
     *      pp_type valt 
269
     *      pp_default_val valt
270
     * | Types.Tstruct(l) -> assert false
271
     * | Types.Ttuple(l) -> assert false
272
     * |_ -> *)
273
    assert false
274

    
275
(* Conversion of basic library functions *)
276

    
277
let horn_basic_app i vl (vltyp, typ) =
278
  match i, vl with
279
  | "ite", [ v1; v2; v3 ] ->
280
    Z3.Boolean.mk_ite !ctx v1 v2 v3
281
  | "uminus", [ v ] ->
282
    Z3.Arithmetic.mk_unary_minus !ctx v
283
  | "not", [ v ] ->
284
    Z3.Boolean.mk_not !ctx v
285
  | "=", [ v1; v2 ] ->
286
    Z3.Boolean.mk_eq !ctx v1 v2
287
  | "&&", [ v1; v2 ] ->
288
    Z3.Boolean.mk_and !ctx [ v1; v2 ]
289
  | "||", [ v1; v2 ] ->
290
    Z3.Boolean.mk_or !ctx [ v1; v2 ]
291
  | "impl", [ v1; v2 ] ->
292
    Z3.Boolean.mk_implies !ctx v1 v2
293
  | "mod", [ v1; v2 ] ->
294
    Z3.Arithmetic.Integer.mk_mod !ctx v1 v2
295
  | "equi", [ v1; v2 ] ->
296
    Z3.Boolean.mk_eq !ctx v1 v2
297
  | "xor", [ v1; v2 ] ->
298
    Z3.Boolean.mk_xor !ctx v1 v2
299
  | "!=", [ v1; v2 ] ->
300
    Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_eq !ctx v1 v2)
301
  | "/", [ v1; v2 ] ->
302
    Z3.Arithmetic.mk_div !ctx v1 v2
303
  | "+", [ v1; v2 ] ->
304
    Z3.Arithmetic.mk_add !ctx [ v1; v2 ]
305
  | "-", [ v1; v2 ] ->
306
    Z3.Arithmetic.mk_sub !ctx [ v1; v2 ]
307
  | "*", [ v1; v2 ] ->
308
    Z3.Arithmetic.mk_mul !ctx [ v1; v2 ]
309
  | "<", [ v1; v2 ] ->
310
    Z3.Arithmetic.mk_lt !ctx v1 v2
311
  | "<=", [ v1; v2 ] ->
312
    Z3.Arithmetic.mk_le !ctx v1 v2
313
  | ">", [ v1; v2 ] ->
314
    Z3.Arithmetic.mk_gt !ctx v1 v2
315
  | ">=", [ v1; v2 ] ->
316
    Z3.Arithmetic.mk_ge !ctx v1 v2
317
  | "int_to_real", [ v1 ] ->
318
    Z3.Arithmetic.Integer.mk_int2real !ctx v1
319
  | _ ->
320
    let fd =
321
      try get_fdecl i
322
      with Not_found ->
323
        report ~level:3 (fun fmt ->
324
            Format.fprintf fmt
325
              "Registering function %s as uninterpreted function in Z3@.%s: \
326
               (%a) -> %a"
327
              i i
328
              (Utils.fprintf_list ~sep:"," Types.print_ty)
329
              vltyp Types.print_ty typ);
330
        decl_fun i vltyp typ
331
    in
332
    Z3.FuncDecl.apply fd vl
333

    
334
(* | _, [v1; v2] ->      Z3.Boolean.mk_and
335
 *      !ctx
336
 *      (val_to_expr v1)
337
 *      (val_to_expr v2)
338
 * 
339
 *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
340

    
341
(* | _ -> (
342
 *     let msg fmt = Format.fprintf fmt
343
 *                     "internal error: zustre unkown function %s (nb args = %i)@."
344
 *                     i (List.length vl)
345
 *     in
346
 *     raise (UnknownFunction(i, msg))
347
 *   ) *)
348

    
349
(* Convert a value expression [v], with internal function calls only. [pp_var]
350
   is a printer for variables (typically [pp_c_var_read]), but an offset suffix
351
   may be added for array variables *)
352
let rec horn_val_to_expr ?(is_lhs = false) m self v =
353
  (* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *)
354
  match v.value_desc with
355
  | Cst c ->
356
    horn_const_to_expr c
357
  (* Code specific for arrays *)
358
  | Array il ->
359
    (* An array definition: (store ( ... (store ( store ( default_val ) idx_n
360
       val_n ) idx_n-1 val_n-1) ... idx_1 val_1 ) *)
361
    let rec build_array (tab, x) =
362
      match tab with
363
      | [] ->
364
        horn_default_val v.value_type (* (get_type v) *)
365
      | h :: t ->
366
        Z3.Z3Array.mk_store !ctx
367
          (build_array (t, x + 1))
368
          (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
369
          (horn_val_to_expr ~is_lhs m self h)
370
    in
371
    build_array (il, 0)
372
  | Access (tab, index) ->
373
    Z3.Z3Array.mk_select !ctx
374
      (horn_val_to_expr ~is_lhs m self tab)
375
      (horn_val_to_expr ~is_lhs m self index)
376
  (* Code specific for arrays *)
377
  | Power _ ->
378
    assert false
379
  | Var v ->
380
    if is_memory m v then
381
      if Types.is_array_type v.var_type then assert false
382
      else
383
        horn_var_to_expr
384
          (rename_machine self
385
             ((if is_lhs then rename_next else rename_current (* self *)) v))
386
    else horn_var_to_expr (rename_machine self v)
387
  | Fun (n, vl) ->
388
    horn_basic_app n
389
      (List.map (horn_val_to_expr m self) vl)
390
      (List.map (fun v -> v.value_type) vl, v.value_type)
391

    
392
let no_reset_to_exprs machines m i =
393
  let n, _ = List.assoc i m.minstances in
394
  let target_machine =
395
    List.find (fun m -> m.mname.node_id = Corelang.node_name n) machines
396
  in
397

    
398
  let m_list =
399
    rename_machine_list (concat m.mname.node_id i)
400
      (rename_mid_list (full_memory_vars machines target_machine))
401
  in
402
  let c_list =
403
    rename_machine_list (concat m.mname.node_id i)
404
      (rename_current_list (full_memory_vars machines target_machine))
405
  in
406
  match c_list, m_list with
407
  | [ chd ], [ mhd ] ->
408
    let expr =
409
      Z3.Boolean.mk_eq !ctx (horn_var_to_expr mhd) (horn_var_to_expr chd)
410
    in
411
    [ expr ]
412
  | _ ->
413
    let exprs =
414
      List.map2
415
        (fun mhd chd ->
416
          Z3.Boolean.mk_eq !ctx (horn_var_to_expr mhd) (horn_var_to_expr chd))
417
        m_list c_list
418
    in
419
    exprs
420

    
421
let instance_reset_to_exprs machines m i =
422
  let n, _ = List.assoc i m.minstances in
423
  let target_machine =
424
    List.find (fun m -> m.mname.node_id = Corelang.node_name n) machines
425
  in
426
  let vars =
427
    rename_machine_list (concat m.mname.node_id i)
428
      (rename_current_list (full_memory_vars machines target_machine))
429
    @ rename_mid_list (full_memory_vars machines target_machine)
430
  in
431

    
432
  let expr =
433
    Z3.Expr.mk_app !ctx
434
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
435
      (List.map horn_var_to_expr (idx :: uid :: vars))
436
  in
437
  [ expr ]
438

    
439
let instance_call_to_exprs machines reset_instances m i inputs outputs =
440
  let self = m.mname.node_id in
441

    
442
  (* Building call args *)
443
  let idx_uid_inout =
444
    (* Additional input to register step counters, and uid *)
445
    let idx = horn_var_to_expr idx in
446
    let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in
447
    let inout =
448
      List.map (horn_val_to_expr m self)
449
        (inputs @ List.map (fun v -> mk_val (Var v) v.var_type) outputs)
450
    in
451
    idx :: uid :: inout
452
  in
453

    
454
  try
455
    (* stateful node instance *)
456
    let n, _ = List.assoc i m.minstances in
457
    let target_machine =
458
      List.find (fun m -> m.mname.node_id = Corelang.node_name n) machines
459
    in
460

    
461
    (* Checking whether this specific instances has been reset yet *)
462
    let reset_exprs =
463
      if not (List.mem i reset_instances) then
464
        (* If not, declare mem_m = mem_c *)
465
        no_reset_to_exprs machines m i
466
      else []
467
      (* Nothing to add yet *)
468
    in
469

    
470
    let mems = full_memory_vars machines target_machine in
471
    let rename_mems f =
472
      rename_machine_list (concat m.mname.node_id i) (f mems)
473
    in
474
    let mid_mems = rename_mems rename_mid_list in
475
    let next_mems = rename_mems rename_next_list in
476

    
477
    let call_expr =
478
      match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
479
      | "_arrow", [ i1; i2 ], [ o ], [ mem_m ], [ mem_x ] ->
480
        let stmt1 =
481
          (* out = ite mem_m then i1 else i2 *)
482
          Z3.Boolean.mk_eq !ctx
483
            ((* output var *)
484
             horn_val_to_expr ~is_lhs:true m self
485
               (mk_val (Var o) o.var_type))
486
            (Z3.Boolean.mk_ite !ctx (horn_var_to_expr mem_m)
487
               (horn_val_to_expr m self i1)
488
               (horn_val_to_expr m self i2))
489
        in
490
        let stmt2 =
491
          (* mem_X = false *)
492
          Z3.Boolean.mk_eq !ctx (horn_var_to_expr mem_x)
493
            (Z3.Boolean.mk_false !ctx)
494
        in
495
        [ stmt1; stmt2 ]
496
      | _ ->
497
        let expr =
498
          Z3.Expr.mk_app !ctx
499
            (get_fdecl (machine_step_name (node_name n)))
500
            ((* Arguments are input, output, mid_mems, next_mems *)
501
             idx_uid_inout
502
            @ List.map horn_var_to_expr (mid_mems @ next_mems))
503
        in
504
        [ expr ]
505
    in
506

    
507
    reset_exprs @ call_expr
508
  with Not_found ->
509
    (* stateless node instance *)
510
    let n, _ = List.assoc i m.mcalls in
511
    let expr =
512
      Z3.Expr.mk_app !ctx
513
        (get_fdecl (machine_stateless_name (node_name n)))
514
        idx_uid_inout
515
      (* Arguments are inputs, outputs *)
516
    in
517
    [ expr ]
518

    
519
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
520
(* let rec value_suffix_to_expr self value = *)
521
(*  match value.value_desc with *)
522
(*  | Fun (n, vl)  ->  *)
523
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
524

    
525
(*  |  _            -> *)
526
(*    horn_val_to_expr self value *)
527

    
528
(* type_directed assignment: array vs. statically sized type - [var_type]: type
529
   of variable to be assigned - [var_name]: name of variable to be assigned -
530
   [value]: assigned value - [pp_var]: printer for variables *)
531
let assign_to_exprs m var_name value =
532
  let self = m.mname.node_id in
533
  let e =
534
    Z3.Boolean.mk_eq !ctx
535
      (horn_val_to_expr ~is_lhs:true m self var_name)
536
      (horn_val_to_expr m self value)
537
    (* was: TODO deal with array accesses (value_suffix_to_expr self value) *)
538
  in
539
  [ e ]
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 :
543
    Z3.Expr.expr list * ident list =
544
  match Corelang.get_instr_desc instr with
545
  | MComment _ ->
546
    [], reset_instances
547
  | MNoReset i ->
548
    (* we assign middle_mem with mem_m. And declare i as reset *)
549
    no_reset_to_exprs machines m i, i :: reset_instances
550
  | MReset i ->
551
    (* we assign middle_mem with reset: reset(mem_m) *)
552
    instance_reset_to_exprs machines m i, i :: reset_instances
553
  | MLocalAssign (i, v) ->
554
    assign_to_exprs m (mk_val (Var i) i.var_type) v, reset_instances
555
  | MStateAssign (i, v) ->
556
    assign_to_exprs m (mk_val (Var i) i.var_type) v, reset_instances
557
  | MStep ([ _ ], i, vl)
558
    when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl)
559
    ->
560
    assert false (* This should not happen anymore *)
561
  | MStep (il, i, vl) ->
562
    (* if reset instance, just print the call over mem_m , otherwise declare
563
       mem_m = mem_c and print the call to mem_m *)
564
    instance_call_to_exprs machines reset_instances m i vl il, reset_instances
565
  (* Since this instance call will only happen once, we don't have to update
566
     reset_instances *)
567
  | MBranch (g, hl) ->
568
    (* (g = tag1 => expr1) and (g = tag2 => expr2) ... should not be produced
569
       yet. Later, we will have to compare the reset_instances of each branch
570
       and introduced the mem_m = mem_c for branches to do not address it while
571
       other did. Am I clear ? *)
572
    (* For each branch we obtain the logical encoding, and the information
573
       whether a sub node has been reset or not. If a node has been reset in one
574
       of the branch, then all others have to have the mem_m = mem_c statement. *)
575
    let self = m.mname.node_id in
576
    let branch_to_expr (tag, instrs) =
577
      let branch_def, branch_resets =
578
        instrs_to_expr machines reset_instances m instrs
579
      in
580
      let e =
581
        Z3.Boolean.mk_implies !ctx
582
          (Z3.Boolean.mk_eq !ctx
583
             (horn_val_to_expr m self g)
584
             (horn_tag_to_expr tag))
585
          branch_def
586
      in
587

    
588
      [ e ], branch_resets
589
    in
590

    
591
    List.fold_left
592
      (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
  | MSpec _ ->
597
    assert false
598

    
599
and instrs_to_expr machines reset_instances m instrs =
600
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
601
  let e_list, rs =
602
    match instrs with
603
    | [ x ] ->
604
      instr_to_exprs reset_instances x
605
    | _ :: _ ->
606
      (* TODO: check whether we should compuyte a AND on the exprs (expr list)
607
         built here. It was performed in the printer setting but seems to be
608
         useless here since the output is a list of exprs *)
609
      List.fold_left
610
        (fun (exprs, rs) i ->
611
          let exprs_i, rs_i = instr_to_exprs rs i in
612
          exprs @ exprs_i, rs @ rs_i)
613
        ([], reset_instances) instrs
614
    | [] ->
615
      [], reset_instances
616
  in
617
  let e =
618
    match e_list with
619
    | [ e ] ->
620
      e
621
    | [] ->
622
      Z3.Boolean.mk_true !ctx
623
    | _ ->
624
      Z3.Boolean.mk_and !ctx e_list
625
  in
626
  e, rs
627

    
628
(*********************************************************)
629

    
630
(* Quantifiying universally all occuring variables *)
631
let add_rule ?(dont_touch = []) vars expr =
632
  (* let fds = Z3.Expr.get_args expr in *)
633
  (* Format.eprintf "Expr %s: args: [%a]@." *)
634
  (*   (Z3.Expr.to_string expr) *)
635
  (* (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt
636
     (Z3.Expr.to_string e))) fds; *)
637

    
638
  (* (\* Old code relying on provided vars *\) *)
639
  (* let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in *)
640
  (* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl
641
     id.var_id)) vars) in *)
642

    
643
  (* New code: we extract vars from expr *)
644
  let module FDSet = Set.Make (struct
645
    type t = Z3.FuncDecl.func_decl
646

    
647
    let compare = compare
648
    (* let hash = Hashtbl.hash *)
649
  end) in
650
  (* Fonction seems unused
651

    
652
     let rec get_expr_vars e = let open Utils in let nb_args =
653
     Z3.Expr.get_num_args e in if nb_args <= 0 then ( let fdecl =
654
     Z3.Expr.get_func_decl e in (* let params = Z3.FuncDecl.get_parameters fdecl
655
     in *) (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string
656
     e); *) let dkind = Z3.FuncDecl.get_decl_kind fdecl in match dkind with
657
     Z3enums.OP_UNINTERPRETED -> ( (* Format.eprintf "kind = %s, " (match dkind
658
     with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
659
     (* let open Z3.FuncDecl.Parameter in *) (* List.iter (fun p -> *) (* match
660
     p with *) (* P_Int i -> Format.eprintf "int %i" i *) (* | P_Dbl f ->
661
     Format.eprintf "dbl %f" f *) (* | P_Sym s -> Format.eprintf "symb" *) (* |
662
     P_Srt s -> Format.eprintf "sort" *) (* | P_Ast _ ->Format.eprintf "ast" *)
663
     (* | P_Fdl f -> Format.eprintf "fundecl" *) (* | P_Rat s -> Format.eprintf
664
     "rat %s" s *)
665

    
666
     (* ) params; *) (* Format.eprintf "]@."; *) FDSet.singleton fdecl ) | _ ->
667
     FDSet.empty ) else (*if nb_args > 0 then*) List.fold_left (fun accu e ->
668
     FDSet.union accu (get_expr_vars e)) FDSet.empty (Z3.Expr.get_args e) in *)
669
  (* Unsed variable. Coul;d be reintroduced let extracted_vars = FDSet.elements
670
     (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in let
671
     extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in let
672
     extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in *)
673
  if !debug then
674
    Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."
675
      (Z3.Expr.to_string expr)
676
      (Utils.fprintf_list ~sep:",@ " (fun fmt e ->
677
           Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
678
      (List.map horn_var_to_expr vars);
679
  let expr =
680
    Z3.Quantifier.mk_forall_const !ctx
681
      (* context *)
682
      (List.map horn_var_to_expr vars)
683
      (* TODO provide bounded variables as expr *)
684
      (* sorts           (\* sort list*\) *)
685
      (* symbols (\* symbol list *\) *)
686
      expr (* expression *) None (* quantifier weight, None means 1 *) []
687
      (* pattern list ? *) [] (* ? *) None (* ? *) None
688
    (* ? *)
689
  in
690

    
691
  (* Format.eprintf "OK@.@?"; *)
692

    
693
  (* TODO: bizarre la declaration de INIT tout seul semble poser pb. *)
694
  Z3.Fixedpoint.add_rule !fp (Z3.Quantifier.expr_of_quantifier expr) None
695

    
696
(********************************************************)
697

    
698
let machine_reset machines m =
699
  let locals = local_memory_vars m in
700

    
701
  (* print "x_m = x_c" for each local memory *)
702
  let mid_mem_def =
703
    List.map
704
      (fun v ->
705
        Z3.Boolean.mk_eq !ctx
706
          (horn_var_to_expr (rename_mid v))
707
          (horn_var_to_expr (rename_current v)))
708
      locals
709
  in
710

    
711
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode. Special
712
     treatment for _arrow: _first = true *)
713
  let reset_instances =
714
    List.map
715
      (fun (id, (n, _)) ->
716
        let name = node_name n in
717
        if name = "_arrow" then
718
          Z3.Boolean.mk_eq !ctx
719
            (let vdecl =
720
               get_fdecl (concat m.mname.node_id id ^ "._arrow._first_m")
721
             in
722
             Z3.Expr.mk_const_f !ctx vdecl)
723
            (Z3.Boolean.mk_true !ctx)
724
        else
725
          let machine_n = get_machine machines name in
726

    
727
          Z3.Expr.mk_app !ctx
728
            (get_fdecl (name ^ "_reset"))
729
            (List.map horn_var_to_expr
730
               (idx
731
                ::
732
                uid
733
                ::
734
                (* Additional vars: counters, uid *)
735
                rename_machine_list
736
                  (concat m.mname.node_id id)
737
                  (reset_vars machines machine_n))))
738
      m.minstances
739
  in
740

    
741
  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
742

    
743
(* TODO: empty list means true statement *)
744
let decl_machine machines m =
745
  if m.mname.node_id = Arrow.arrow_id then (* We don't do arrow function *)
746
    ()
747
  else
748
    let _ =
749
      List.map decl_var
750
        (inout_vars m
751
        @ rename_current_list (full_memory_vars machines m)
752
        @ rename_mid_list (full_memory_vars machines m)
753
        @ rename_next_list (full_memory_vars machines m)
754
        @ rename_machine_list m.mname.node_id m.mstep.step_locals)
755
    in
756
    if is_stateless m then (
757
      if !debug then
758
        Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id;
759

    
760
      (* Declaring single predicate *)
761
      let vars = inout_vars m in
762
      let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
763
      let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
764

    
765
      let horn_body, _ (* don't care for reset here *) =
766
        instrs_to_expr machines [] (* No reset info for stateless nodes *) m
767
          m.mstep.step_instrs
768
      in
769
      let horn_head =
770
        Z3.Expr.mk_app !ctx
771
          (get_fdecl (machine_stateless_name m.mname.node_id))
772
          (List.map horn_var_to_expr
773
             (idx :: uid :: (* Additional vars: counters, uid *)
774
                            vars))
775
      in
776
      (* this line seems useless *)
777
      let vars =
778
        idx :: uid :: vars
779
        @ rename_machine_list m.mname.node_id m.mstep.step_locals
780
      in
781
      (* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ "
782
         Printers.pp_var) vars; *)
783
      match m.mstep.step_asserts with
784
      | [] ->
785
        (* Rule for single predicate : "; Stateless step rule @." *)
786
        (*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*)
787
        (* TODO clean code *)
788
        (* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ "
789
           Printers.pp_var) vars; *)
790
        add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
791
      | assertsl ->
792
        (*Rule for step "; Stateless step rule with Assertions @.";*)
793
        let body_with_asserts =
794
          Z3.Boolean.mk_and !ctx
795
            (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
796
        in
797
        let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
798
        add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head))
799
    else
800
      (* Rule for reset *)
801
      let vars = reset_vars machines m in
802
      let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
803
      let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in
804
      let horn_reset_body = machine_reset machines m in
805
      let horn_reset_head =
806
        Z3.Expr.mk_app !ctx
807
          (get_fdecl (machine_reset_name m.mname.node_id))
808
          (List.map horn_var_to_expr
809
             (idx :: uid :: (* Additional vars: counters, uid *)
810
                            vars))
811
      in
812

    
813
      let _ =
814
        add_rule (idx :: uid :: vars)
815
          (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
816
      in
817

    
818
      (* Rule for step*)
819
      let vars = step_vars machines m in
820
      let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
821
      let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in
822
      let horn_step_body, _ (* don't care for reset here *) =
823
        instrs_to_expr machines [] m m.mstep.step_instrs
824
      in
825
      let horn_step_head =
826
        Z3.Expr.mk_app !ctx
827
          (get_fdecl (machine_step_name m.mname.node_id))
828
          (List.map horn_var_to_expr
829
             (idx :: uid :: (* Additional vars: counters, uid *)
830
                            vars))
831
      in
832
      match m.mstep.step_asserts with
833
      | [] ->
834
        (* Rule for single predicate *)
835
        let vars =
836
          step_vars_c_m_x machines m
837
          @ rename_machine_list m.mname.node_id m.mstep.step_locals
838
        in
839
        add_rule (idx :: uid :: vars)
840
          (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
841
      | assertsl ->
842
        (* Rule for step Assertions @.; *)
843
        let body_with_asserts =
844
          Z3.Boolean.mk_and !ctx
845
            (horn_step_body
846
             :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
847
        in
848
        let vars =
849
          step_vars_c_m_x machines m
850
          @ rename_machine_list m.mname.node_id m.mstep.step_locals
851
        in
852
        add_rule (idx :: uid :: vars)
853
          (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
854

    
855
(* Debug functions *)
856
(* let rec extract_expr_fds e = (* Format.eprintf "@[<v 2>Extracting fundecls
857
   from expr %s@ " *) (* (Z3.Expr.to_string e); *)
858

    
859
   (* Removing quantifier is there are some *) let e = (* I didn't found a nicer
860
   way to do it than with an exception. My bad *) try let eq =
861
   Z3.Quantifier.quantifier_of_expr e in let e2 = Z3.Quantifier.get_body eq in
862
   (* Format.eprintf "Extracted quantifier body@ "; *) e2
863

    
864
   with _ -> Format.eprintf "No quantifier info@ "; e in let _ = try ( let fd =
865
   Z3.Expr.get_func_decl e in let fd_symbol = Z3.FuncDecl.get_name fd in let
866
   fd_name = Z3.Symbol.to_string fd_symbol in if not (Hashtbl.mem decls fd_name)
867
   then register_fdecl fd_name fd; (* Format.eprintf "fdecls (%s): %s@ " *) (*
868
   fd_name *) (* (Z3.FuncDecl.to_string fd); *) try ( let args =
869
   Z3.Expr.get_args e in (* Format.eprintf "@[<v>@ "; *) (* List.iter
870
   extract_expr_fds args; *) (* Format.eprintf "@]@ "; *) () ) with _ ->
871
   Format.eprintf "Impossible to extract fundecl args for expression %s@ "
872
   (Z3.Expr.to_string e) ) with _ -> Format.eprintf "Impossible to extract
873
   anything from expression %s@ " (Z3.Expr.to_string e) in (* Format.eprintf
874
   "@]@ " *) () *)
875
(* Local Variables: *)
876
(* compile-command:"make -C ../.." *)
877
(* End: *)
(4-4/7)