Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre_verifier.ml @ e4edf171

History | View | Annotate | Download (24.7 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
	| _ -> 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] ->      Z3.Boolean.mk_and
253
   *      !ctx
254
   *      (val_to_expr v1)
255
   *      (val_to_expr v2)
256
   * 
257
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
258
  | _ -> (
259
    Format.eprintf
260
      "internal error: zustre unkown function %s@." i;
261
    assert false)
262

    
263
           
264
(* Convert a value expression [v], with internal function calls only.
265
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
266
   but an offset suffix may be added for array variables
267
*)
268
let rec horn_val_to_expr ?(is_lhs=false) self v =
269
  match v.value_desc with
270
  | Cst c       -> horn_const_to_expr c
271

    
272
  (* Code specific for arrays *)
273
  | Array il    ->
274
     (* An array definition: 
275
	(store (
276
	  ...
277
 	    (store (
278
	       store (
279
	          default_val
280
	       ) 
281
	       idx_n val_n
282
	    ) 
283
	    idx_n-1 val_n-1)
284
	  ... 
285
	  idx_1 val_1
286
	) *)
287
     let rec build_array (tab, x) =
288
       match tab with
289
       | [] -> horn_default_val v.value_type(* (get_type v) *)
290
       | h::t ->
291
	  Z3.Z3Array.mk_store
292
            !ctx
293
	    (build_array (t, (x+1)))
294
	    (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
295
	    (horn_val_to_expr ~is_lhs:is_lhs self h)
296
     in
297
     build_array (il, 0)
298
       
299
  | Access(tab,index) ->
300
     Z3.Z3Array.mk_select !ctx 
301
       (horn_val_to_expr ~is_lhs:is_lhs self tab)
302
       (horn_val_to_expr ~is_lhs:is_lhs self index)
303

    
304
  (* Code specific for arrays *)
305
    
306
  | Power (v, n)  -> assert false
307
  | LocalVar v    ->
308
     horn_var_to_expr
309
       (rename_machine
310
          self
311
          v)
312
  | StateVar v    ->
313
     if Types.is_array_type v.var_type
314
     then assert false
315
     else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
316
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr self) vl
317

    
318
let no_reset_to_exprs machines m i =
319
  let (n,_) = List.assoc i m.minstances in
320
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
321

    
322
  let m_list = 
323
    rename_machine_list
324
      (concat m.mname.node_id i)
325
      (rename_mid_list (full_memory_vars machines target_machine))
326
  in
327
  let c_list =
328
    rename_machine_list
329
      (concat m.mname.node_id i)
330
      (rename_current_list (full_memory_vars machines target_machine))
331
  in
332
  match c_list, m_list with
333
  | [chd], [mhd] ->
334
     let expr =
335
       Z3.Boolean.mk_eq !ctx 
336
         (horn_var_to_expr mhd)
337
         (horn_var_to_expr chd)
338
     in
339
     [expr]
340
  | _ -> (
341
    let exprs =
342
      List.map2 (fun mhd chd -> 
343
          Z3.Boolean.mk_eq !ctx 
344
            (horn_var_to_expr mhd)
345
            (horn_var_to_expr chd)
346
        )
347
        m_list
348
        c_list
349
    in
350
    exprs
351
  )
352

    
353
let instance_reset_to_exprs machines m i =
354
  let (n,_) = List.assoc i m.minstances in
355
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
356
  let vars =
357
    (
358
      (rename_machine_list
359
	 (concat m.mname.node_id i)
360
	 (rename_current_list (full_memory_vars machines target_machine))
361
      ) 
362
      @
363
	(rename_machine_list
364
	   (concat m.mname.node_id i)
365
	   (rename_mid_list (full_memory_vars machines target_machine))
366
	)
367
    )
368
  in
369
  let expr =
370
    Z3.Expr.mk_app
371
      !ctx
372
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
373
      (List.map (horn_var_to_expr) vars)
374
  in
375
  [expr]
376

    
377
let instance_call_to_exprs machines reset_instances m i inputs outputs =
378
  let self = m.mname.node_id in
379
  try (* stateful node instance *)
380
    begin
381
      let (n,_) = List.assoc i m.minstances in
382
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
383

    
384
      (* Checking whether this specific instances has been reset yet *)
385
      let reset_exprs = 
386
        if not (List.mem i reset_instances) then
387
	  (* If not, declare mem_m = mem_c *)
388
	  no_reset_to_exprs machines m i
389
        else
390
          [] (* Nothing to add yet *)
391
      in
392
      
393
      let mems = full_memory_vars machines target_machine in
394
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
395
      let mid_mems = rename_mems rename_mid_list in
396
      let next_mems = rename_mems rename_next_list in
397

    
398
      let call_expr = 
399
      match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
400
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
401
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
402
            Z3.Boolean.mk_eq !ctx
403
              ( (* output var *)
404
                horn_val_to_expr
405
                  ~is_lhs:true
406
                  self
407
                  (mk_val (LocalVar o) o.var_type)
408
              )
409
              (
410
                Z3.Boolean.mk_ite !ctx 
411
	          (horn_var_to_expr mem_m) 
412
	          (horn_val_to_expr self i1)
413
	          (horn_val_to_expr self i2)
414
              )
415
          in
416
          let stmt2 = (* mem_X = false *)
417
            Z3.Boolean.mk_eq !ctx
418
	      (horn_var_to_expr mem_x)
419
              (Z3.Boolean.mk_false !ctx)
420
          in
421
          [stmt1; stmt2]
422
      end
423

    
424
      | node_name_n ->
425
         let expr = 
426
           Z3.Expr.mk_app
427
             !ctx
428
             (get_fdecl (machine_step_name (node_name n)))
429
             ( (* Arguments are input, output, mid_mems, next_mems *)
430
               (
431
                 List.map (horn_val_to_expr self) (
432
                     inputs @
433
	               (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
434
                   )
435
               ) @ (
436
                 List.map (horn_var_to_expr) (mid_mems@next_mems)
437
	       )
438
             )
439
         in
440
         [expr]
441
      in
442

    
443
      reset_exprs@call_expr
444
    end
445
  with Not_found -> ( (* stateless node instance *)
446
    let (n,_) = List.assoc i m.mcalls in
447
    let expr = 
448
      Z3.Expr.mk_app
449
        !ctx
450
        (get_fdecl (machine_stateless_name (node_name n)))
451
        ((* Arguments are inputs, outputs *)
452
         List.map (horn_val_to_expr self)
453
           (
454
             inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
455
           )
456
        )
457
    in
458
    [expr]
459
  )
460

    
461

    
462
    
463
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
464
(* let rec value_suffix_to_expr self value = *)
465
(*  match value.value_desc with *)
466
(*  | Fun (n, vl)  ->  *)
467
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
468
    
469
(*  |  _            -> *)
470
(*    horn_val_to_expr self value *)
471

    
472

    
473
(* type_directed assignment: array vs. statically sized type
474
   - [var_type]: type of variable to be assigned
475
   - [var_name]: name of variable to be assigned
476
   - [value]: assigned value
477
   - [pp_var]: printer for variables
478
*)
479
let assign_to_exprs m var_name value =
480
  let self = m.mname.node_id in
481
  let e =
482
    Z3.Boolean.mk_eq
483
      !ctx
484
      (horn_val_to_expr ~is_lhs:true self var_name)
485
      (horn_val_to_expr self value)
486
  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
487
  in
488
  [e]
489

    
490
    
491
(* Convert instruction to Z3.Expr and update the set of reset instances *)
492
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
493
  match Corelang.get_instr_desc instr with
494
  | MComment _ -> [], reset_instances
495
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
496
    no_reset_to_exprs machines m i,
497
    i::reset_instances
498
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
499
    instance_reset_to_exprs machines m i,
500
    i::reset_instances
501
  | MLocalAssign (i,v) ->
502
    assign_to_exprs
503
      m  
504
      (mk_val (LocalVar i) i.var_type) v,
505
    reset_instances
506
  | MStateAssign (i,v) ->
507
    assign_to_exprs
508
      m 
509
      (mk_val (StateVar i) i.var_type) v,
510
    reset_instances
511
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
512
    assert false (* This should not happen anymore *)
513
  | MStep (il, i, vl) ->
514
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
515
       mem_c and print the call to mem_m *)
516
    instance_call_to_exprs machines reset_instances m i vl il,
517
    reset_instances (* Since this instance call will only happen once, we
518
		       don't have to update reset_instances *)
519

    
520
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
521
			 should not be produced yet. Later, we will have to
522
			 compare the reset_instances of each branch and
523
			 introduced the mem_m = mem_c for branches to do not
524
			 address it while other did. Am I clear ? *)
525
    (* For each branch we obtain the logical encoding, and the information
526
       whether a sub node has been reset or not. If a node has been reset in one
527
       of the branch, then all others have to have the mem_m = mem_c
528
       statement. *)
529
    let self = m.mname.node_id in
530
    let branch_to_expr (tag, instrs) =
531
      let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in
532
      let e =
533
	Z3.Boolean.mk_implies !ctx
534
          (Z3.Boolean.mk_eq !ctx 
535
             (horn_val_to_expr self g)
536
	     (horn_tag_to_expr tag))
537
          branch_def in
538

    
539
      [e], branch_resets
540
	  
541
    in
542
    List.fold_left (fun (instrs, resets) b ->
543
      let b_instrs, b_resets = branch_to_expr b in
544
      instrs@b_instrs, resets@b_resets 
545
    ) ([], reset_instances) hl 
546

    
547
and instrs_to_expr machines reset_instances m instrs = 
548
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
549
  let e_list, rs = 
550
    match instrs with
551
    | [x] -> instr_to_exprs reset_instances x 
552
    | _::_ -> (* 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 *)
553
       
554
       List.fold_left (fun (exprs, rs) i -> 
555
         let exprs_i, rs_i = instr_to_exprs rs i in
556
         exprs@exprs_i, rs@rs_i
557
       )
558
         ([], reset_instances) instrs 
559
	 
560
	 
561
    | [] -> [], reset_instances
562
  in
563
  let e = 
564
    match e_list with
565
    | [e] -> e
566
    | [] -> Z3.Boolean.mk_true !ctx
567
    | _ -> Z3.Boolean.mk_and !ctx e_list
568
  in
569
  e, rs
570

    
571
        
572
let machine_reset machines m =
573
  let locals = local_memory_vars machines m in
574
  
575
  (* print "x_m = x_c" for each local memory *)
576
  let mid_mem_def =
577
    List.map (fun v ->
578
      Z3.Boolean.mk_eq !ctx
579
	(horn_var_to_expr (rename_mid v))
580
	(horn_var_to_expr (rename_current v))
581
    ) locals
582
  in
583

    
584
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
585
     Special treatment for _arrow: _first = true
586
  *)
587

    
588
  let reset_instances =
589
    
590
    List.map (fun (id, (n, _)) ->
591
      let name = node_name n in
592
      if name = "_arrow" then (
593
	Z3.Boolean.mk_eq !ctx
594
	  (
595
	    let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
596
	    Z3.Expr.mk_const_f !ctx vdecl
597
	  )
598
	  (Z3.Boolean.mk_true !ctx)
599
	  
600
      ) else (
601
	let machine_n = get_machine machines name in 
602
	
603
	Z3.Expr.mk_app
604
	  !ctx
605
	  (get_fdecl (name ^ "_reset"))
606
	  (List.map (horn_var_to_expr)
607
	     (rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
608
	  )
609
	  
610
      )
611
    ) m.minstances
612
      
613
      
614
  in
615
  
616
  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
617
    
618
        
619

    
620
(*  TODO: empty list means true statement *)
621
let decl_machine machines m =
622
  if m.mname.node_id = Arrow.arrow_id then
623
    (* We don't do arrow function *)
624
    ()
625
  else
626
    begin
627
      let vars =
628
        List.map decl_var 
629
      	  (
630
	    (inout_vars machines m)@
631
	      (rename_current_list (full_memory_vars machines m)) @
632
	      (rename_mid_list (full_memory_vars machines m)) @
633
	      (rename_next_list (full_memory_vars machines m)) @
634
	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
635
	  )
636
      in
637
      
638
      if is_stateless m then
639
	begin
640
	  (* Declaring single predicate *)
641
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in
642
	  let horn_body, _ (* don't care for reset here *) =
643
	    instrs_to_expr
644
	      machines
645
	      ([] (* No reset info for stateless nodes *) )
646
	      m
647
	      m.mstep.step_instrs
648
	  in
649
	  let horn_head = 
650
	    Z3.Expr.mk_app
651
	      !ctx
652
	      (get_fdecl (machine_stateless_name m.mname.node_id))
653
	      (List.map (horn_var_to_expr) (inout_vars machines m))
654
	  in
655
	  match m.mstep.step_asserts with
656
	  | [] ->
657
	     begin
658
	       (* Rule for single predicate : "; Stateless step rule @." *)
659
	       Z3.Fixedpoint.add_rule !fp
660
		 (Z3.Boolean.mk_implies !ctx horn_body horn_head)
661
		 None
662
	     end
663
	  | assertsl ->
664
	     begin
665
	       (*Rule for step "; Stateless step rule with Assertions @.";*)
666
	       let body_with_asserts =
667
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
668
	       in
669
	       Z3.Fixedpoint.add_rule !fp
670
		 (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
671
		 None
672
	     end
673
	end
674
      else
675
	begin
676
	  (* Declaring predicate *)
677
	  let _ = decl_rel (machine_reset_name m.mname.node_id) (reset_vars machines m) in
678
          let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in
679

    
680
	  (* Rule for reset *)
681

    
682
	  let horn_reset_body = machine_reset machines m in	    
683
	  let horn_reset_head = 
684
	    Z3.Expr.mk_app
685
	      !ctx
686
	      (get_fdecl (machine_reset_name m.mname.node_id))
687
	      (List.map (horn_var_to_expr) (reset_vars machines m))
688
	  in
689
	  
690
	  let _ =
691
	    Z3.Fixedpoint.add_rule !fp
692
	      (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
693
	      None
694
	  in
695

    
696
	  (* Rule for step*)
697
	  let horn_step_body, _ (* don't care for reset here *) =
698
	    instrs_to_expr
699
	      machines
700
	      []
701
	      m
702
	      m.mstep.step_instrs
703
	  in
704
	  let horn_step_head = 
705
	    Z3.Expr.mk_app
706
	      !ctx
707
	      (get_fdecl (machine_step_name m.mname.node_id))
708
	      (List.map (horn_var_to_expr) (step_vars machines m))
709
	  in
710
	  match m.mstep.step_asserts with
711
	  | [] ->
712
	     begin
713
	       (* Rule for single predicate *)
714
	       Z3.Fixedpoint.add_rule !fp
715
		 (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
716
		 None
717
	     end
718
	  | assertsl ->
719
	     begin
720
	       (* Rule for step Assertions @.; *)
721
	       let body_with_asserts =
722
		 Z3.Boolean.mk_and !ctx
723
		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
724
	       in
725
	       Z3.Fixedpoint.add_rule !fp
726
		 (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
727
		 None
728
	     end
729
     	       
730
	end
731
    end
732

    
733
let param_stat = ref false
734
let param_eldarica = ref false
735
let param_utvpi = ref false
736
let param_tosmt = ref false
737
let param_pp = ref false
738
             
739
module Verifier =
740
  (struct
741
    include VerifierType.Default
742
    let name = "zustre"
743
    let options = [
744
        "-stat", Arg.Set param_stat, "print statistics";
745
        "-eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules";
746
        "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
747
        "-tosmt", Arg.Set param_tosmt, "Print low-level (possibly unreadable) SMT2 statements";
748
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
749
      ]
750
                
751
    let activate () = (
752
        active := true;
753
        Options.output := "horn";
754
      )
755
    let is_active () = !active
756

    
757
    let get_normalization_params () =
758
      (* make sure the output is "Horn" *)
759
      assert(!Options.output = "horn");
760
      Backends.get_normalization_params ()
761

    
762
    let setup_solver () =
763
      fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
764
      (* let help = Z3.Fixedpoint.get_help fp in
765
       * Format.eprintf "Fp help : %s@." help;
766
       * 
767
       * let solver =Z3.Solver.mk_solver !ctx None in
768
       * let help = Z3.Solver.get_help solver in
769
       * Format.eprintf "Z3 help : %s@." help; *)
770
      
771
      let module P = Z3.Params in
772
      let module S = Z3.Symbol in
773
      let mks = S.mk_string !ctx in
774
      let params = P.mk_params !ctx in
775

    
776
      (* self.fp.set (engine='spacer') *)
777
      P.add_symbol params (mks "engine") (mks "spacer");
778
      
779
       (* #z3.set_option(rational_to_decimal=True) *)
780
       (* #self.fp.set('precision',30) *)
781
      if !param_stat then 
782
        (* self.fp.set('print_statistics',True) *)
783
        P.add_bool params (mks "print_statistics") true;
784

    
785
      (* Dont know where to find this parameter *)
786
      (* if !param_spacer_verbose then
787
         *   if self.args.spacer_verbose: 
788
         *        z3.set_option (verbose=1) *)
789

    
790
      (* The option is not recogined*)
791
      (* self.fp.set('use_heavy_mev',True) *)
792
      (* P.add_bool params (mks "use_heavy_mev") true; *)
793
      
794
      (* self.fp.set('pdr.flexible_trace',True) *)
795
      P.add_bool params (mks "pdr.flexible_trace") true;
796

    
797
      (* self.fp.set('reset_obligation_queue',False) *)
798
      P.add_bool params (mks "spacer.reset_obligation_queue") false;
799

    
800
      (* self.fp.set('spacer.elim_aux',False) *)
801
      P.add_bool params (mks "spacer.elim_aux") false;
802

    
803
      (* if self.args.eldarica:
804
        *     self.fp.set('print_fixedpoint_extensions', False) *)
805
      if !param_eldarica then
806
        P.add_bool params (mks "print_fixedpoint_extensions") false;
807
      
808
      (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
809
      if !param_utvpi then
810
        P.add_bool params (mks "pdr.utvpi") false;
811

    
812
      (* if self.args.tosmt:
813
       *        self.log.info("Setting low level printing")
814
       *        self.fp.set ('print.low_level_smt2',True) *)
815
      if !param_tosmt then
816
        P.add_bool params (mks "print.low_level_smt2") true;
817

    
818
      (* if not self.args.pp:
819
       *        self.log.info("No pre-processing")
820
       *        self.fp.set ('xform.slice', False)
821
       *        self.fp.set ('xform.inline_linear',False)
822
       *        self.fp.set ('xform.inline_eager',False) *\) *)
823
      if !param_pp then (
824
        P.add_bool params (mks "xform.slice") false;
825
        P.add_bool params (mks "xform.inline_linear") false;
826
        P.add_bool params (mks "xform.inline_eager") false
827
      );
828
      Z3.Fixedpoint.set_parameters !fp params
829
              
830
      
831
    let run basename prog machines =
832
      let machines = Machine_code_common.arrow_machine::machines in
833
      let machines = preprocess machines in
834
      setup_solver ();
835
      decl_sorts ();
836
      List.iter (decl_machine machines) (List.rev machines);
837
      ()
838
      
839
      
840

    
841
  end: VerifierType.S)
842