Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre_verifier.ml @ 46cb4020

History | View | Annotate | Download (25.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

    
8
module HBC = Horn_backend_common
9
let machine_step_name = HBC.machine_step_name
10
let node_name = HBC.node_name
11
let concat = HBC.concat
12
let rename_machine = HBC.rename_machine
13
let rename_machine_list = HBC.rename_machine_list
14
let rename_next = HBC.rename_next
15
let rename_current = HBC.rename_current
16
let rename_current_list = HBC.rename_current_list
17
let rename_mid_list = HBC.rename_mid_list
18
let rename_next_list = HBC.rename_next_list
19
let full_memory_vars = HBC.full_memory_vars
20
let inout_vars = HBC.inout_vars
21
let reset_vars = HBC.reset_vars
22
let step_vars = HBC.step_vars
23
let local_memory_vars = HBC.local_memory_vars
24
  
25
let machine_reset_name = HBC.machine_reset_name 
26
let machine_stateless_name = HBC.machine_stateless_name 
27

    
28
let rename_mid = HBC.rename_mid
29

    
30
let preprocess = Horn_backend.preprocess
31
  
32
let active = ref false
33
let ctx = ref (Z3.mk_context [])
34
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx)
35

    
36
(** Sorts
37

    
38
A sort is introduced for each basic type and each enumerated type.
39

    
40
A hashtbl records these and allow easy access to sort values, when
41
   provided with a enumerated type name. 
42

    
43
*)
44
        
45
let bool_sort = Z3.Boolean.mk_sort !ctx
46
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
47
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
48

    
49
let const_sorts = Hashtbl.create 13
50
let const_tags = Hashtbl.create 13
51
let sort_elems = Hashtbl.create 13
52

    
53
let get_const_sort = Hashtbl.find const_sorts 
54
let get_sort_elems = Hashtbl.find sort_elems
55
let get_tag_sort = Hashtbl.find const_tags
56
  
57

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

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

    
92
(** Func decls
93

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

    
98

    
99

    
100
 *)
101
let decls = Hashtbl.create 13
102
let register_fdecl id fd = Hashtbl.add decls id fd
103
let get_fdecl id = Hashtbl.find decls id
104
                 
105
let decl_var id =
106
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
107
  register_fdecl id.var_id fdecl;
108
  fdecl
109

    
110
let decl_rel name args =
111
  (*verifier ce qui est construit. On veut un declare-rel *)
112
  let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in
113
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
114
  register_fdecl name fdecl;
115
  fdecl
116
  
117

    
118

    
119
(** Conversion functions
120

    
121
The following is similar to the Horn backend. Each printing function
122
   is rephrased from pp_xx to xx_to_expr and produces a Z3 value.
123

    
124
 *)
125

    
126

    
127
(* Returns the f_decl associated to the variable v *)
128
let horn_var_to_expr v =
129
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
130

    
131

    
132

    
133

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

    
161

    
162

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

    
182
(* Conversion of basic library functions *)
183
    
184
let horn_basic_app i val_to_expr vl =
185
  match i, vl with
186
  | "ite", [v1; v2; v3] ->
187
     Z3.Boolean.mk_ite
188
       !ctx
189
       (val_to_expr v1)
190
       (val_to_expr v2)
191
       (val_to_expr v3)
192

    
193
  | "uminus", [v] ->
194
     Z3.Arithmetic.mk_unary_minus
195
       !ctx
196
       (val_to_expr v)
197
  | "not", [v] ->
198
     Z3.Boolean.mk_not
199
       !ctx
200
       (val_to_expr v)
201
  | "=", [v1; v2] ->
202
     Z3.Boolean.mk_eq
203
       !ctx
204
       (val_to_expr v1)
205
       (val_to_expr v2)
206
  | "&&", [v1; v2] ->
207
     Z3.Boolean.mk_and
208
       !ctx
209
       [val_to_expr v1;
210
        val_to_expr v2]
211
  | "||", [v1; v2] ->
212
          Z3.Boolean.mk_or
213
       !ctx
214
       [val_to_expr v1;
215
        val_to_expr v2]
216

    
217
  | "impl", [v1; v2] ->
218
     Z3.Boolean.mk_implies
219
       !ctx
220
       (val_to_expr v1)
221
       (val_to_expr v2)
222
 | "mod", [v1; v2] ->
223
          Z3.Arithmetic.Integer.mk_mod
224
       !ctx
225
       (val_to_expr v1)
226
       (val_to_expr v2)
227
  | "equi", [v1; v2] ->
228
          Z3.Boolean.mk_eq
229
       !ctx
230
       (val_to_expr v1)
231
       (val_to_expr v2)
232
  | "xor", [v1; v2] ->
233
          Z3.Boolean.mk_xor
234
       !ctx
235
       (val_to_expr v1)
236
       (val_to_expr v2)
237
  | "!=", [v1; v2] ->
238
     Z3.Boolean.mk_not
239
       !ctx
240
       (
241
         Z3.Boolean.mk_eq
242
           !ctx
243
           (val_to_expr v1)
244
           (val_to_expr v2)
245
       )
246
  | "/", [v1; v2] ->
247
     Z3.Arithmetic.mk_div
248
       !ctx
249
       (val_to_expr v1)
250
       (val_to_expr v2)
251

    
252
  | "+", [v1; v2] ->
253
     Z3.Arithmetic.mk_add
254
       !ctx
255
       [val_to_expr v1; val_to_expr v2]
256

    
257
  | "-", [v1; v2] ->
258
     Z3.Arithmetic.mk_sub
259
       !ctx
260
       [val_to_expr v1 ; val_to_expr v2]
261
       
262
  | "*", [v1; v2] ->
263
     Z3.Arithmetic.mk_mul
264
       !ctx
265
       [val_to_expr v1; val_to_expr v2]
266

    
267

    
268
  | "<", [v1; v2] ->
269
     Z3.Arithmetic.mk_lt
270
       !ctx
271
       (val_to_expr v1)
272
       (val_to_expr v2)
273

    
274
  | "<=", [v1; v2] ->
275
     Z3.Arithmetic.mk_le
276
       !ctx
277
       (val_to_expr v1)
278
       (val_to_expr v2)
279

    
280
  | ">", [v1; v2] ->
281
     Z3.Arithmetic.mk_gt
282
       !ctx
283
       (val_to_expr v1)
284
       (val_to_expr v2)
285

    
286
  | ">=", [v1; v2] ->
287
     Z3.Arithmetic.mk_ge
288
       !ctx
289
       (val_to_expr v1)
290
       (val_to_expr v2)
291

    
292
       
293
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
294
   *      !ctx
295
   *      (val_to_expr v1)
296
   *      (val_to_expr v2)
297
   * 
298
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
299
  | _ -> (
300
    Format.eprintf
301
      "internal error: zustre unkown function %s@." i;
302
    assert false)
303

    
304
           
305
(* Convert a value expression [v], with internal function calls only.
306
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
307
   but an offset suffix may be added for array variables
308
*)
309
let rec horn_val_to_expr ?(is_lhs=false) self v =
310
  match v.value_desc with
311
  | Cst c       -> horn_const_to_expr c
312

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

    
345
  (* Code specific for arrays *)
346
    
347
  | Power (v, n)  -> assert false
348
  | LocalVar v    ->
349
     horn_var_to_expr
350
       (rename_machine
351
          self
352
          v)
353
  | StateVar v    ->
354
     if Types.is_array_type v.var_type
355
     then assert false
356
     else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
357
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr self) vl
358

    
359
let no_reset_to_exprs machines m i =
360
  let (n,_) = List.assoc i m.minstances in
361
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
362

    
363
  let m_list = 
364
    rename_machine_list
365
      (concat m.mname.node_id i)
366
      (rename_mid_list (full_memory_vars machines target_machine))
367
  in
368
  let c_list =
369
    rename_machine_list
370
      (concat m.mname.node_id i)
371
      (rename_current_list (full_memory_vars machines target_machine))
372
  in
373
  match c_list, m_list with
374
  | [chd], [mhd] ->
375
     let expr =
376
       Z3.Boolean.mk_eq !ctx 
377
         (horn_var_to_expr mhd)
378
         (horn_var_to_expr chd)
379
     in
380
     [expr]
381
  | _ -> (
382
    let exprs =
383
      List.map2 (fun mhd chd -> 
384
          Z3.Boolean.mk_eq !ctx 
385
            (horn_var_to_expr mhd)
386
            (horn_var_to_expr chd)
387
        )
388
        m_list
389
        c_list
390
    in
391
    exprs
392
  )
393

    
394
let instance_reset_to_exprs machines m i =
395
  let (n,_) = List.assoc i m.minstances in
396
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
397
  let vars =
398
    (
399
      (rename_machine_list
400
	 (concat m.mname.node_id i)
401
	 (rename_current_list (full_memory_vars machines target_machine))
402
      ) 
403
      @
404
	(rename_machine_list
405
	   (concat m.mname.node_id i)
406
	   (rename_mid_list (full_memory_vars machines target_machine))
407
	)
408
    )
409
  in
410
  let expr =
411
    Z3.Expr.mk_app
412
      !ctx
413
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
414
      (List.map (horn_var_to_expr) vars)
415
  in
416
  [expr]
417

    
418
let instance_call_to_exprs machines reset_instances m i inputs outputs =
419
  let self = m.mname.node_id in
420
  try (* stateful node instance *)
421
    begin
422
      let (n,_) = List.assoc i m.minstances in
423
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
424

    
425
      (* Checking whether this specific instances has been reset yet *)
426
      let reset_exprs = 
427
        if not (List.mem i reset_instances) then
428
	  (* If not, declare mem_m = mem_c *)
429
	  no_reset_to_exprs machines m i
430
        else
431
          [] (* Nothing to add yet *)
432
      in
433
      
434
      let mems = full_memory_vars machines target_machine in
435
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
436
      let mid_mems = rename_mems rename_mid_list in
437
      let next_mems = rename_mems rename_next_list in
438

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

    
465
      | node_name_n ->
466
         let expr = 
467
           Z3.Expr.mk_app
468
             !ctx
469
             (get_fdecl (machine_step_name (node_name n)))
470
             ( (* Arguments are input, output, mid_mems, next_mems *)
471
               (
472
                 List.map (horn_val_to_expr self) (
473
                     inputs @
474
	               (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
475
                   )
476
               ) @ (
477
                 List.map (horn_var_to_expr) (mid_mems@next_mems)
478
	       )
479
             )
480
         in
481
         [expr]
482
      in
483

    
484
      reset_exprs@call_expr
485
    end
486
  with Not_found -> ( (* stateless node instance *)
487
    let (n,_) = List.assoc i m.mcalls in
488
    let expr = 
489
      Z3.Expr.mk_app
490
        !ctx
491
        (get_fdecl (machine_stateless_name (node_name n)))
492
        ((* Arguments are inputs, outputs *)
493
         List.map (horn_val_to_expr self)
494
           (
495
             inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
496
           )
497
        )
498
    in
499
    [expr]
500
  )
501

    
502

    
503
    
504
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
505
(* let rec value_suffix_to_expr self value = *)
506
(*  match value.value_desc with *)
507
(*  | Fun (n, vl)  ->  *)
508
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
509
    
510
(*  |  _            -> *)
511
(*    horn_val_to_expr self value *)
512

    
513

    
514
(* type_directed assignment: array vs. statically sized type
515
   - [var_type]: type of variable to be assigned
516
   - [var_name]: name of variable to be assigned
517
   - [value]: assigned value
518
   - [pp_var]: printer for variables
519
*)
520
let assign_to_exprs m var_name value =
521
  let self = m.mname.node_id in
522
  let e =
523
    Z3.Boolean.mk_eq
524
      !ctx
525
      (horn_val_to_expr ~is_lhs:true self var_name)
526
      (horn_val_to_expr self value)
527
  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
528
  in
529
  [e]
530

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

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

    
580
      [e], branch_resets
581
	  
582
    in
583
    List.fold_left (fun (instrs, resets) b ->
584
      let b_instrs, b_resets = branch_to_expr b in
585
      instrs@b_instrs, resets@b_resets 
586
    ) ([], reset_instances) hl 
587

    
588
and instrs_to_expr machines reset_instances m instrs = 
589
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
590
  let e_list, rs = 
591
    match instrs with
592
    | [x] -> instr_to_exprs reset_instances x 
593
    | _::_ -> (* 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 *)
594
       
595
       List.fold_left (fun (exprs, rs) i -> 
596
         let exprs_i, rs_i = instr_to_exprs rs i in
597
         exprs@exprs_i, rs@rs_i
598
       )
599
         ([], reset_instances) instrs 
600
	 
601
	 
602
    | [] -> [], reset_instances
603
  in
604
  let e = 
605
    match e_list with
606
    | [e] -> e
607
    | [] -> Z3.Boolean.mk_true !ctx
608
    | _ -> Z3.Boolean.mk_and !ctx e_list
609
  in
610
  e, rs
611

    
612
        
613
let machine_reset machines m =
614
  let locals = local_memory_vars machines m in
615
  
616
  (* print "x_m = x_c" for each local memory *)
617
  let mid_mem_def =
618
    List.map (fun v ->
619
      Z3.Boolean.mk_eq !ctx
620
	(horn_var_to_expr (rename_mid v))
621
	(horn_var_to_expr (rename_current v))
622
    ) locals
623
  in
624

    
625
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
626
     Special treatment for _arrow: _first = true
627
  *)
628

    
629
  let reset_instances =
630
    
631
    List.map (fun (id, (n, _)) ->
632
      let name = node_name n in
633
      if name = "_arrow" then (
634
	Z3.Boolean.mk_eq !ctx
635
	  (
636
	    let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
637
	    Z3.Expr.mk_const_f !ctx vdecl
638
	  )
639
	  (Z3.Boolean.mk_true !ctx)
640
	  
641
      ) else (
642
	let machine_n = get_machine machines name in 
643
	
644
	Z3.Expr.mk_app
645
	  !ctx
646
	  (get_fdecl (name ^ "_reset"))
647
	  (List.map (horn_var_to_expr)
648
	     (rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
649
	  )
650
	  
651
      )
652
    ) m.minstances
653
      
654
      
655
  in
656
  
657
  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
658
    
659
        
660

    
661
(*  TODO: empty list means true statement *)
662
let decl_machine machines m =
663
  if m.mname.node_id = Arrow.arrow_id then
664
    (* We don't do arrow function *)
665
    ()
666
  else
667
    begin
668
      let vars =
669
        List.map decl_var 
670
      	  (
671
	    (inout_vars machines m)@
672
	      (rename_current_list (full_memory_vars machines m)) @
673
	      (rename_mid_list (full_memory_vars machines m)) @
674
	      (rename_next_list (full_memory_vars machines m)) @
675
	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
676
	  )
677
      in
678
      
679
      if is_stateless m then
680
	begin
681
	  (* Declaring single predicate *)
682
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in
683
	  let horn_body, _ (* don't care for reset here *) =
684
	    instrs_to_expr
685
	      machines
686
	      ([] (* No reset info for stateless nodes *) )
687
	      m
688
	      m.mstep.step_instrs
689
	  in
690
	  let horn_head = 
691
	    Z3.Expr.mk_app
692
	      !ctx
693
	      (get_fdecl (machine_stateless_name m.mname.node_id))
694
	      (List.map (horn_var_to_expr) (inout_vars machines m))
695
	  in
696
	  match m.mstep.step_asserts with
697
	  | [] ->
698
	     begin
699
	       (* Rule for single predicate : "; Stateless step rule @." *)
700
	       Z3.Fixedpoint.add_rule !fp
701
		 (Z3.Boolean.mk_implies !ctx horn_body horn_head)
702
		 None
703
	     end
704
	  | assertsl ->
705
	     begin
706
	       (*Rule for step "; Stateless step rule with Assertions @.";*)
707
	       let body_with_asserts =
708
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
709
	       in
710
	       Z3.Fixedpoint.add_rule !fp
711
		 (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
712
		 None
713
	     end
714
	end
715
      else
716
	begin
717
	  (* Declaring predicate *)
718
	  let _ = decl_rel (machine_reset_name m.mname.node_id) (reset_vars machines m) in
719
          let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in
720

    
721
	  (* Rule for reset *)
722

    
723
	  let horn_reset_body = machine_reset machines m in	    
724
	  let horn_reset_head = 
725
	    Z3.Expr.mk_app
726
	      !ctx
727
	      (get_fdecl (machine_reset_name m.mname.node_id))
728
	      (List.map (horn_var_to_expr) (reset_vars machines m))
729
	  in
730
	  
731
	  let _ =
732
	    Z3.Fixedpoint.add_rule !fp
733
	      (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
734
	      None
735
	  in
736

    
737
	  (* Rule for step*)
738
	  let horn_step_body, _ (* don't care for reset here *) =
739
	    instrs_to_expr
740
	      machines
741
	      []
742
	      m
743
	      m.mstep.step_instrs
744
	  in
745
	  let horn_step_head = 
746
	    Z3.Expr.mk_app
747
	      !ctx
748
	      (get_fdecl (machine_step_name m.mname.node_id))
749
	      (List.map (horn_var_to_expr) (step_vars machines m))
750
	  in
751
	  match m.mstep.step_asserts with
752
	  | [] ->
753
	     begin
754
	       (* Rule for single predicate *)
755
	       Z3.Fixedpoint.add_rule !fp
756
		 (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
757
		 None
758
	     end
759
	  | assertsl ->
760
	     begin
761
	       (* Rule for step Assertions @.; *)
762
	       let body_with_asserts =
763
		 Z3.Boolean.mk_and !ctx
764
		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
765
	       in
766
	       Z3.Fixedpoint.add_rule !fp
767
		 (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
768
		 None
769
	     end
770
     	       
771
	end
772
    end
773

    
774
let param_stat = ref false
775
let param_eldarica = ref false
776
let param_utvpi = ref false
777
let param_tosmt = ref false
778
let param_pp = ref false
779
             
780
module Verifier =
781
  (struct
782
    include VerifierType.Default
783
    let name = "zustre"
784
    let options = [
785
        "-stat", Arg.Set param_stat, "print statistics";
786
        "-eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules";
787
        "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
788
        "-tosmt", Arg.Set param_tosmt, "Print low-level (possibly unreadable) SMT2 statements";
789
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
790
      ]
791
                
792
    let activate () = (
793
        active := true;
794
        Options.output := "horn";
795
      )
796
    let is_active () = !active
797

    
798
    let get_normalization_params () =
799
      (* make sure the output is "Horn" *)
800
      assert(!Options.output = "horn");
801
      Backends.get_normalization_params ()
802

    
803
    let setup_solver () =
804
      fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
805
      (* let help = Z3.Fixedpoint.get_help fp in
806
       * Format.eprintf "Fp help : %s@." help;
807
       * 
808
       * let solver =Z3.Solver.mk_solver !ctx None in
809
       * let help = Z3.Solver.get_help solver in
810
       * Format.eprintf "Z3 help : %s@." help; *)
811
      
812
      let module P = Z3.Params in
813
      let module S = Z3.Symbol in
814
      let mks = S.mk_string !ctx in
815
      let params = P.mk_params !ctx in
816

    
817
      (* self.fp.set (engine='spacer') *)
818
      P.add_symbol params (mks "engine") (mks "spacer");
819
      
820
       (* #z3.set_option(rational_to_decimal=True) *)
821
       (* #self.fp.set('precision',30) *)
822
      if !param_stat then 
823
        (* self.fp.set('print_statistics',True) *)
824
        P.add_bool params (mks "print_statistics") true;
825

    
826
      (* Dont know where to find this parameter *)
827
      (* if !param_spacer_verbose then
828
         *   if self.args.spacer_verbose: 
829
         *        z3.set_option (verbose=1) *)
830

    
831
      (* The option is not recogined*)
832
      (* self.fp.set('use_heavy_mev',True) *)
833
      (* P.add_bool params (mks "use_heavy_mev") true; *)
834
      
835
      (* self.fp.set('pdr.flexible_trace',True) *)
836
      P.add_bool params (mks "pdr.flexible_trace") true;
837

    
838
      (* self.fp.set('reset_obligation_queue',False) *)
839
      P.add_bool params (mks "spacer.reset_obligation_queue") false;
840

    
841
      (* self.fp.set('spacer.elim_aux',False) *)
842
      P.add_bool params (mks "spacer.elim_aux") false;
843

    
844
      (* if self.args.eldarica:
845
        *     self.fp.set('print_fixedpoint_extensions', False) *)
846
      if !param_eldarica then
847
        P.add_bool params (mks "print_fixedpoint_extensions") false;
848
      
849
      (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
850
      if !param_utvpi then
851
        P.add_bool params (mks "pdr.utvpi") false;
852

    
853
      (* if self.args.tosmt:
854
       *        self.log.info("Setting low level printing")
855
       *        self.fp.set ('print.low_level_smt2',True) *)
856
      if !param_tosmt then
857
        P.add_bool params (mks "print.low_level_smt2") true;
858

    
859
      (* if not self.args.pp:
860
       *        self.log.info("No pre-processing")
861
       *        self.fp.set ('xform.slice', False)
862
       *        self.fp.set ('xform.inline_linear',False)
863
       *        self.fp.set ('xform.inline_eager',False) *\) *)
864
      if !param_pp then (
865
        P.add_bool params (mks "xform.slice") false;
866
        P.add_bool params (mks "xform.inline_linear") false;
867
        P.add_bool params (mks "xform.inline_eager") false
868
      );
869
      Z3.Fixedpoint.set_parameters !fp params
870
              
871
      
872
    let run basename prog machines =
873
      let machines = Machine_code_common.arrow_machine::machines in
874
      let machines = preprocess machines in
875
      setup_solver ();
876
      decl_sorts ();
877
      List.iter (decl_machine machines) (List.rev machines);
878

    
879

    
880
      (* Debug instructions *)
881
      let rules_expr = Z3.Fixedpoint.get_rules !fp in
882
      Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
883
	(Utils.fprintf_list ~sep:"@ "
884
	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
885
	rules_expr;
886
      
887
      ()
888
      
889
      
890

    
891
  end: VerifierType.S)
892