Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre_verifier.ml @ ff2d7a82

History | View | Annotate | Download (24.1 KB)

1
open LustreSpec
2
open Machine_code
3
open Format
4
(* open Horn_backend_common
5
 * open Horn_backend *)
6

    
7
module HBC = Horn_backend_common
8
let machine_step_name = HBC.machine_step_name
9
let node_name = HBC.node_name
10
let concat = HBC.concat
11
let rename_machine = HBC.rename_machine
12
let rename_machine_list = HBC.rename_machine_list
13
let rename_next = HBC.rename_next
14
let rename_current = HBC.rename_current
15
let rename_current_list = HBC.rename_current_list
16
let rename_mid_list = HBC.rename_mid_list
17
let rename_next_list = HBC.rename_next_list
18
let full_memory_vars = HBC.full_memory_vars
19
   
20
let active = ref false
21
let ctx = ref (Z3.mk_context [])
22
let machine_reset_name = HBC.machine_reset_name 
23
let machine_stateless_name = HBC.machine_stateless_name 
24

    
25
(** Sorts
26

    
27
A sort is introduced for each basic type and each enumerated type.
28

    
29
A hashtbl records these and allow easy access to sort values, when
30
   provided with a enumerated type name. 
31

    
32
*)
33
        
34
let bool_sort = Z3.Boolean.mk_sort !ctx
35
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
36
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
37

    
38
let const_sorts = Hashtbl.create 13
39
let const_tags = Hashtbl.create 13
40
let sort_elems = Hashtbl.create 13
41

    
42
let get_const_sort = Hashtbl.find const_sorts 
43
let get_sort_elems = Hashtbl.find sort_elems
44
let get_tag_sort = Hashtbl.find const_tags
45
  
46

    
47
  
48
let decl_sorts () =
49
  Hashtbl.iter (fun typ decl ->
50
    match typ with
51
    | Tydec_const var ->
52
      (match decl.top_decl_desc with
53
      | TypeDef tdef -> (
54
	match tdef.tydef_desc with
55
	| Tydec_enum tl ->
56
	  let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
57
          Hashtbl.add const_sorts var new_sort;
58
          Hashtbl.add sort_elems new_sort tl;
59
          List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl
60
          
61
	| _ -> assert false
62
      )
63
      | _ -> assert false
64
      )
65
    | _        -> ()) Corelang.type_table
66

    
67
                 
68
let rec type_to_sort t =
69
  if Types.is_bool_type t  then bool_sort else
70
    if Types.is_int_type t then int_sort else 
71
  if Types.is_real_type t then real_sort else 
72
  match (Types.repr t).Types.tdesc with
73
  | Types.Tconst ty       -> get_const_sort ty
74
  | Types.Tclock t        -> type_to_sort t
75
  | Types.Tarray(dim,ty)   -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
76
  | Types.Tstatic(d, ty)-> type_to_sort ty
77
  | Types.Tarrow _
78
  | _                     -> Format.eprintf "internal error: pp_type %a@."
79
                               Types.print_ty t; assert false
80

    
81
(** Func decls
82

    
83
Similarly fun_decls are registerd, by their name, into a hashtbl. The
84
   proposed encoding introduces a 0-ary fun_decl to model variables
85
   and fun_decl with arguments to declare reset and step predicates.
86

    
87

    
88

    
89
 *)
90
let decls = Hashtbl.create 13
91
let register_fdecl id fd = Hashtbl.add decls id fd
92
let get_fdecl id = Hashtbl.find decls id
93
                 
94
let decl_var id =
95
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
96
  register_fdecl id.var_id fdecl;
97
  fdecl
98

    
99
let decl_rel name args =
100
  (*verifier ce qui est construit. On veut un declare-rel *)
101
  let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in
102
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
103
  register_fdecl name fdecl;
104
  fdecl
105
  
106

    
107

    
108
(** conversion functions
109

    
110
The following is similar to the Horn backend. Each printing function
111
   is rephrased from pp_xx to xx_to_expr and produces a Z3 value.
112

    
113
 *)
114

    
115

    
116
(* Returns the f_decl associated to the variable v *)
117
let horn_var_to_expr v =
118
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
119

    
120

    
121

    
122

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

    
150

    
151

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

    
171

    
172
let horn_basic_app i val_to_expr vl =
173
  match i, vl with
174
  | "ite", [v1; v2; v3] ->
175
     Z3.Boolean.mk_ite
176
       !ctx
177
       (val_to_expr v1)
178
       (val_to_expr v2)
179
       (val_to_expr v3)
180

    
181
  | "uminus", [v] ->
182
     Z3.Arithmetic.mk_unary_minus
183
       !ctx
184
       (val_to_expr v)
185
  | "not", [v] ->
186
     Z3.Boolean.mk_not
187
       !ctx
188
       (val_to_expr v)
189
  | "=", [v1; v2] ->
190
     Z3.Boolean.mk_eq
191
       !ctx
192
       (val_to_expr v1)
193
       (val_to_expr v2)
194
  | "&&", [v1; v2] ->
195
     Z3.Boolean.mk_and
196
       !ctx
197
       [val_to_expr v1;
198
        val_to_expr v2]
199
  | "||", [v1; v2] ->
200
          Z3.Boolean.mk_or
201
       !ctx
202
       [val_to_expr v1;
203
        val_to_expr v2]
204

    
205
  | "impl", [v1; v2] ->
206
     Z3.Boolean.mk_implies
207
       !ctx
208
       (val_to_expr v1)
209
       (val_to_expr v2)
210
 | "mod", [v1; v2] ->
211
          Z3.Arithmetic.Integer.mk_mod
212
       !ctx
213
       (val_to_expr v1)
214
       (val_to_expr v2)
215
  | "equi", [v1; v2] ->
216
          Z3.Boolean.mk_eq
217
       !ctx
218
       (val_to_expr v1)
219
       (val_to_expr v2)
220
  | "xor", [v1; v2] ->
221
          Z3.Boolean.mk_xor
222
       !ctx
223
       (val_to_expr v1)
224
       (val_to_expr v2)
225
  | "!=", [v1; v2] ->
226
     Z3.Boolean.mk_not
227
       !ctx
228
       (
229
         Z3.Boolean.mk_eq
230
           !ctx
231
           (val_to_expr v1)
232
           (val_to_expr v2)
233
       )
234
  | "/", [v1; v2] ->
235
     Z3.Arithmetic.mk_div
236
       !ctx
237
       (val_to_expr v1)
238
       (val_to_expr v2)
239

    
240
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
241
   *      !ctx
242
   *      (val_to_expr v1)
243
   *      (val_to_expr v2)
244
   * 
245
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
246
  | _ -> (
247
    Format.eprintf
248
      "internal error: zustre unkown function %s@." i;
249
    assert false)
250

    
251
           
252
(* Convert a value expression [v], with internal function calls only.
253
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
254
   but an offset suffix may be added for array variables
255
*)
256
let rec horn_val_to_expr ?(is_lhs=false) self v =
257
  match v.value_desc with
258
  | Cst c       -> horn_const_to_expr c
259

    
260
  (* Code specific for arrays *)
261
  | Array il    ->
262
     (* An array definition: 
263
	(store (
264
	  ...
265
 	    (store (
266
	       store (
267
	          default_val
268
	       ) 
269
	       idx_n val_n
270
	    ) 
271
	    idx_n-1 val_n-1)
272
	  ... 
273
	  idx_1 val_1
274
	) *)
275
     let rec build_array (tab, x) =
276
       match tab with
277
       | [] -> horn_default_val v.value_type(* (get_type v) *)
278
       | h::t ->
279
	  Z3.Z3Array.mk_store
280
            !ctx
281
	    (build_array (t, (x+1)))
282
	    (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
283
	    (horn_val_to_expr ~is_lhs:is_lhs self h)
284
     in
285
     build_array (il, 0)
286
       
287
  | Access(tab,index) ->
288
     Z3.Z3Array.mk_select !ctx 
289
       (horn_val_to_expr ~is_lhs:is_lhs self tab)
290
       (horn_val_to_expr ~is_lhs:is_lhs self index)
291

    
292
  (* Code specific for arrays *)
293
    
294
  | Power (v, n)  -> assert false
295
  | LocalVar v    ->
296
     horn_var_to_expr
297
       (rename_machine
298
          self
299
          v)
300
  | StateVar v    ->
301
     if Types.is_array_type v.var_type
302
     then assert false
303
     else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
304
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr self) vl
305

    
306
let no_reset_to_exprs machines m i =
307
  let (n,_) = List.assoc i m.minstances in
308
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
309

    
310
  let m_list = 
311
    rename_machine_list
312
      (concat m.mname.node_id i)
313
      (rename_mid_list (full_memory_vars machines target_machine))
314
  in
315
  let c_list =
316
    rename_machine_list
317
      (concat m.mname.node_id i)
318
      (rename_current_list (full_memory_vars machines target_machine))
319
  in
320
  match c_list, m_list with
321
  | [chd], [mhd] ->
322
     let expr =
323
       Z3.Boolean.mk_eq !ctx 
324
         (horn_var_to_expr mhd)
325
         (horn_var_to_expr chd)
326
     in
327
     [expr]
328
  | _ -> (
329
    let exprs =
330
      List.map2 (fun mhd chd -> 
331
          Z3.Boolean.mk_eq !ctx 
332
            (horn_var_to_expr mhd)
333
            (horn_var_to_expr chd)
334
        )
335
        m_list
336
        c_list
337
    in
338
    exprs
339
  )
340

    
341
let instance_reset_to_exprs machines m i =
342
  let (n,_) = List.assoc i m.minstances in
343
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
344
  let vars =
345
    (
346
      (rename_machine_list
347
	 (concat m.mname.node_id i)
348
	 (rename_current_list (full_memory_vars machines target_machine))
349
      ) 
350
      @
351
	(rename_machine_list
352
	   (concat m.mname.node_id i)
353
	   (rename_mid_list (full_memory_vars machines target_machine))
354
	)
355
    )
356
  in
357
  let expr =
358
    Z3.Expr.mk_app
359
      !ctx
360
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
361
      (List.map (horn_var_to_expr) vars)
362
  in
363
  [expr]
364

    
365
let instance_call_to_exprs machines reset_instances m i inputs outputs =
366
  let self = m.mname.node_id in
367
  try (* stateful node instance *)
368
    begin
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
      (* Checking whether this specific instances has been reset yet *)
373
      let reset_exprs = 
374
        if not (List.mem i reset_instances) then
375
	  (* If not, declare mem_m = mem_c *)
376
	  no_reset_to_exprs machines m i
377
        else
378
          [] (* Nothing to add yet *)
379
      in
380
      
381
      let mems = full_memory_vars machines target_machine in
382
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
383
      let mid_mems = rename_mems rename_mid_list in
384
      let next_mems = rename_mems rename_next_list in
385

    
386
      let call_expr = 
387
      match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
388
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
389
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
390
            Z3.Boolean.mk_eq !ctx
391
              ( (* output var *)
392
                horn_val_to_expr
393
                  ~is_lhs:true
394
                  self
395
                  (mk_val (LocalVar o) o.var_type)
396
              )
397
              (
398
                Z3.Boolean.mk_ite !ctx 
399
	          (horn_var_to_expr mem_m) 
400
	          (horn_val_to_expr self i1)
401
	          (horn_val_to_expr self i2)
402
              )
403
          in
404
          let stmt2 = (* mem_X = false *)
405
            Z3.Boolean.mk_eq !ctx
406
	      (horn_var_to_expr mem_x)
407
              (Z3.Boolean.mk_false !ctx)
408
          in
409
          [stmt1; stmt2]
410
      end
411

    
412
      | node_name_n ->
413
         let expr = 
414
           Z3.Expr.mk_app
415
             !ctx
416
             (get_fdecl (machine_step_name (node_name n)))
417
             ( (* Arguments are input, output, mid_mems, next_mems *)
418
               (
419
                 List.map (horn_val_to_expr self) (
420
                     inputs @
421
	               (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
422
                   )
423
               ) @ (
424
                 List.map (horn_var_to_expr) (mid_mems@next_mems)
425
	       )
426
             )
427
         in
428
         [expr]
429
      in
430

    
431
      reset_exprs@call_expr
432
    end
433
  with Not_found -> ( (* stateless node instance *)
434
    let (n,_) = List.assoc i m.mcalls in
435
    let expr = 
436
      Z3.Expr.mk_app
437
        !ctx
438
        (get_fdecl (machine_stateless_name (node_name n)))
439
        ((* Arguments are inputs, outputs *)
440
         List.map (horn_val_to_expr self)
441
           (
442
             inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
443
           )
444
        )
445
    in
446
    [expr]
447
  )
448
    
449

    
450
(* Convert instruction to Z3.Expr and update the set of reset instances *)
451
let rec instr_to_expr machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
452
  match Corelang.get_instr_desc instr with
453
  | MComment _ -> [], reset_instances
454
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
455
    no_reset_to_exprs machines m i,
456
    i::reset_instances
457
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
458
    instance_reset_to_exprs machines m i,
459
    i::reset_instances
460
  | MLocalAssign (i,v) ->
461
    assign_to_exprs
462
      m (horn_var_to_expr) 
463
      (mk_val (LocalVar i) i.var_type) v,
464
    reset_instances
465
  | MStateAssign (i,v) ->
466
    assign_to_exprs
467
      m (horn_var_to_expr) 
468
      (mk_val (StateVar i) i.var_type) v,
469
    reset_instances
470
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
471
    assert false (* This should not happen anymore *)
472
  | MStep (il, i, vl) ->
473
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
474
       mem_c and print the call to mem_m *)
475
    instance_call_to_exprs machines reset_instances m i vl il,
476
    reset_instances (* Since this instance call will only happen once, we
477
		       don't have to update reset_instances *)
478

    
479
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
480
			 should not be produced yet. Later, we will have to
481
			 compare the reset_instances of each branch and
482
			 introduced the mem_m = mem_c for branches to do not
483
			 address it while other did. Am I clear ? *)
484
    (* For each branch we obtain the logical encoding, and the information
485
       whether a sub node has been reset or not. If a node has been reset in one
486
       of the branch, then all others have to have the mem_m = mem_c
487
       statement. *)
488
    let self = m.mname.node_id in
489
    let branch_to_expr (tag, instrs) =
490
      Z3.Boolean.mk_implies
491
        (Z3.Boolean.mk_eq !ctx 
492
           (horn_val_to_expr self g)
493
	   (horn_tag_to_expr tag))
494
        (machine_instrs_to_exprs machines reset_instances m instrs)
495
    in
496
    List.map branch_to_expr hl,
497
    reset_instances 
498

    
499
and instrs_to_expr machines reset_instances m instrs = 
500
  let instr_to_expr rs i = instr_to_expr machines rs m i in
501
  match instrs with
502
  | [x] -> instr_to_expres reset_instances x 
503
  | _::_ -> (* 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 *)
504

    
505
      List.fold_left (fun (exprs, rs) i -> 
506
          let exprs_i, rs = ppi rs i in
507
          expr@exprs_i, rs
508
        )
509
        ([], reset_instances) instrs 
510
    
511
    
512
  | [] -> [], reset_instances
513

    
514

    
515
let basic_library_to_horn_expr i vl =
516
  match i, vl with
517
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
518

    
519
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
520
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
521
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
522
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
523
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
524
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
525
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
526
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
527
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
528
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
529
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
530
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
531
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
532
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
533

    
534
*)
535

    
536
        
537
(* Prints a [value] indexed by the suffix list [loop_vars] *)
538
let rec value_suffix_to_expr self value =
539
 match value.value_desc with
540
 | Fun (n, vl)  -> 
541
   basic_library_to_horn_expr n (value_suffix_to_expr self vl)
542
 |  _            ->
543
   horn_val_to_expr self value
544

    
545
        
546
(* type_directed assignment: array vs. statically sized type
547
   - [var_type]: type of variable to be assigned
548
   - [var_name]: name of variable to be assigned
549
   - [value]: assigned value
550
   - [pp_var]: printer for variables
551
*)
552
let assign_to_exprs m var_name value =
553
  let self = m.mname.node_id in
554
  let e =
555
    Z3.Boolean.mk_eq
556
      !ctx
557
      (horn_val_to_expr ~is_lhs:true self var_name)
558
      (value_suffix_to_expr self value)
559
  in
560
  [e]
561

    
562
(*                TODO: empty list means true statement *)
563
let decl_machine machines m =
564
  if m.Machine_code.mname.node_id = Machine_code.arrow_id then
565
    (* We don't print arrow function *)
566
    ()
567
  else
568
    begin
569
      let vars =
570
        List.map decl_var 
571
      	  (
572
	    (inout_vars machines m)@
573
	      (rename_current_list (full_memory_vars machines m)) @
574
	        (rename_mid_list (full_memory_vars machines m)) @
575
	          (rename_next_list (full_memory_vars machines m)) @
576
	            (rename_machine_list m.mname.node_id m.mstep.step_locals)
577
	  )
578
      in
579
      
580
      if is_stateless m then
581
	begin
582
	  (* Declaring single predicate *)
583
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in          
584
          match m.mstep.step_asserts with
585
	  | [] ->
586
	     begin
587

    
588
	       (* Rule for single predicate *)
589
	       fprintf fmt "; Stateless step rule @.";
590
	       fprintf fmt "@[<v 2>(rule (=> @ ";
591
	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
592
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
593
		 pp_machine_stateless_name m.mname.node_id
594
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (inout_vars machines m);
595
	     end
596
	  | assertsl ->
597
	     begin
598
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
599
	       
600
	       fprintf fmt "; Stateless step rule with Assertions @.";
601
	       (*Rule for step*)
602
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
603
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
604
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
605
		 pp_machine_stateless_name m.mname.node_id
606
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
607
	  
608
	     end
609
	       
610
	end
611
      else
612
	begin
613
	  (* Declaring predicate *)
614
	  let _ = decl_rel (machine_reset_name m.mname.node_id) (reset_vars machines m) in
615
          let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in
616

    
617
	  (* Rule for reset *)
618
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
619
	    (pp_machine_reset machines) m 
620
	    pp_machine_reset_name m.mname.node_id
621
	    (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (reset_vars machines m);
622

    
623
          match m.mstep.step_asserts with
624
	  | [] ->
625
	     begin
626
	       fprintf fmt "; Step rule @.";
627
	       (* Rule for step*)
628
	       fprintf fmt "@[<v 2>(rule (=> @ ";
629
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
630
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
631
		 pp_machine_step_name m.mname.node_id
632
		 (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (step_vars machines m);
633
	     end
634
	  | assertsl -> 
635
	     begin
636
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
637
	       (* print_string pp_val; *)
638
	       fprintf fmt "; Step rule with Assertions @.";
639
	       
640
	       (*Rule for step*)
641
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
642
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
643
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
644
		 pp_machine_step_name m.mname.node_id
645
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
646
	     end
647
	       
648
     	       
649
	end
650
    end
651

    
652
let param_stat = ref false
653
let param_eldarica = ref false
654
let param_utvpi = ref false
655
let param_tosmt = ref false
656
let param_pp = ref false
657
             
658
module Verifier =
659
  (struct
660
    include VerifierType.Default
661
    let name = "zustre"
662
    let options = [
663
        "-stat", Arg.Set param_stat, "print statistics";
664
        "-eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules";
665
        "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
666
        "-tosmt", Arg.Set param_tosmt, "Print low-level (possibly unreadable) SMT2 statements";
667
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
668
      ]
669
                
670
    let activate () = (
671
        active := true;
672
        Options.output := "horn";
673
      )
674
    let is_active () = !active
675

    
676
    let get_normalization_params () =
677
      (* make sure the output is "Horn" *)
678
      assert(!Options.output = "horn");
679
      Backends.get_normalization_params ()
680

    
681
    let setup_solver () =
682
      let fp = Z3.Fixedpoint.mk_fixedpoint !ctx in
683
      (* let help = Z3.Fixedpoint.get_help fp in
684
       * Format.eprintf "Fp help : %s@." help;
685
       * 
686
       * let solver =Z3.Solver.mk_solver !ctx None in
687
       * let help = Z3.Solver.get_help solver in
688
       * Format.eprintf "Z3 help : %s@." help; *)
689
      
690
      let module P = Z3.Params in
691
      let module S = Z3.Symbol in
692
      let mks = S.mk_string !ctx in
693
      let params = P.mk_params !ctx in
694

    
695
      (* self.fp.set (engine='spacer') *)
696
      P.add_symbol params (mks "engine") (mks "spacer");
697
      
698
       (* #z3.set_option(rational_to_decimal=True) *)
699
       (* #self.fp.set('precision',30) *)
700
      if !param_stat then 
701
        (* self.fp.set('print_statistics',True) *)
702
        P.add_bool params (mks "print_statistics") true;
703

    
704
      (* Dont know where to find this parameter *)
705
      (* if !param_spacer_verbose then
706
         *   if self.args.spacer_verbose: 
707
         *        z3.set_option (verbose=1) *)
708

    
709
      (* The option is not recogined*)
710
      (* self.fp.set('use_heavy_mev',True) *)
711
      (* P.add_bool params (mks "use_heavy_mev") true; *)
712
      
713
      (* self.fp.set('pdr.flexible_trace',True) *)
714
      P.add_bool params (mks "pdr.flexible_trace") true;
715

    
716
      (* self.fp.set('reset_obligation_queue',False) *)
717
      P.add_bool params (mks "spacer.reset_obligation_queue") false;
718

    
719
      (* self.fp.set('spacer.elim_aux',False) *)
720
      P.add_bool params (mks "spacer.elim_aux") false;
721

    
722
      (* if self.args.eldarica:
723
        *     self.fp.set('print_fixedpoint_extensions', False) *)
724
      if !param_eldarica then
725
        P.add_bool params (mks "print_fixedpoint_extensions") false;
726
      
727
      (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
728
      if !param_utvpi then
729
        P.add_bool params (mks "pdr.utvpi") false;
730

    
731
      (* if self.args.tosmt:
732
       *        self.log.info("Setting low level printing")
733
       *        self.fp.set ('print.low_level_smt2',True) *)
734
      if !param_tosmt then
735
        P.add_bool params (mks "print.low_level_smt2") true;
736

    
737
      (* if not self.args.pp:
738
       *        self.log.info("No pre-processing")
739
       *        self.fp.set ('xform.slice', False)
740
       *        self.fp.set ('xform.inline_linear',False)
741
       *        self.fp.set ('xform.inline_eager',False) *\) *)
742
      if !param_pp then (
743
        P.add_bool params (mks "xform.slice") false;
744
        P.add_bool params (mks "xform.inline_linear") false;
745
        P.add_bool params (mks "xform.inline_eager") false
746
      );
747
      Z3.Fixedpoint.set_parameters fp params
748
        
749
      
750
    let run basename prog machines =
751
      let machines = Machine_code.arrow_machine::machines in
752
      let machines = preprocess machines in
753
      setup_solver ();
754
      decl_sorts ();
755
      List.iter (decl_machine machines) (List.rev machines);
756

    
757
      
758
      ()
759

    
760
  end: VerifierType.S)
761