Project

General

Profile

« Previous | Next » 

Revision c1785a55

Added by Pierre-Loïc Garoche about 6 years ago

ongoing work on zustre backend

View differences:

src/backends/Horn/horn_backend_common.ml
14 14
open Corelang
15 15
open Machine_code
16 16

  
17
let machine_reset_name id = id ^ "_reset"
18
let machine_step_name id = id ^ "_step" 
19
let machine_stateless_name id = id ^ "_fun" 
17 20
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
18 21
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
19 22
let pp_machine_stateless_name fmt id = fprintf fmt "%s_fun" id
src/tools/zustre_verifier.ml
1 1
open LustreSpec
2 2
open Machine_code
3 3
open Format
4
open Horn_backend_common
5
open Horn_backend
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
6 19
   
7 20
let active = ref false
8 21
let ctx = ref (Z3.mk_context [])
22
let machine_reset_name = HBC.machine_reset_name 
23

  
24
(** Sorts
25

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

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

  
31
*)
32
        
10 33
let bool_sort = Z3.Boolean.mk_sort !ctx
11 34
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
12 35
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
13 36

  
14 37
let const_sorts = Hashtbl.create 13
15
let get_const_sort ty_name =
16
  Hashtbl.find const_sorts ty_name
38
let const_tags = Hashtbl.create 13
39
let sort_elems = Hashtbl.create 13
40

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

  
46
  
18 47
let decl_sorts () =
19 48
  Hashtbl.iter (fun typ decl ->
20 49
    match typ with
......
24 53
	match tdef.tydef_desc with
25 54
	| Tydec_enum tl ->
26 55
	  let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
27
          Hashtbl.add const_sorts var new_sort
56
          Hashtbl.add const_sorts var new_sort;
57
          Hashtbl.add sort_elems new_sort tl;
58
          List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl
59
          
28 60
	| _ -> assert false
29 61
      )
30 62
      | _ -> assert false
31 63
      )
32 64
    | _        -> ()) Corelang.type_table
33 65

  
34

  
66
                 
35 67
let rec type_to_sort t =
36 68
  if Types.is_bool_type t  then bool_sort else
37 69
    if Types.is_int_type t then int_sort else 
......
45 77
  | _                     -> Format.eprintf "internal error: pp_type %a@."
46 78
                               Types.print_ty t; assert false
47 79

  
48
  
80
(** Func decls
81

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

  
86

  
87

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

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

  
106

  
107
(** conversion functions
108

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

  
112
 *)
113

  
114

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

  
119

  
120

  
121

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

  
149

  
150

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

  
170

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

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

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

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

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

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

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

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

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

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

  
364
let instance_call_to_exprs machines reset_instances m i inputs outputs =
365
  let self = m.mname.node_id in
366
  try (* stateful node instance *)
367
    begin
368
      let (n,_) = List.assoc i m.minstances in
369
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
370

  
371
      (* Checking whether this specific instances has been reset yet *)
372
      let reset_exprs = 
373
        if not (List.mem i reset_instances) then
374
	  (* If not, declare mem_m = mem_c *)
375
	  no_reset_to_exprs machines m i
376
        else
377
          [] (* Nothing to add yet *)
378
      in
379
      
380
      let mems = full_memory_vars machines target_machine in
381
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
382
      let mid_mems = rename_mems rename_mid_list in
383
      let next_mems = rename_mems rename_next_list in
384

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

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

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

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

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

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

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

  
513

  
514
(*                TODO: empty list means true statement *)
52 515
let decl_machine machines m =
53 516
  if m.Machine_code.mname.node_id = Machine_code.arrow_id then
54 517
    (* We don't print arrow function *)
55 518
    ()
56 519
  else
57 520
    begin
58
      let _ = List.map decl_var 
59
      	(
60
	  (inout_vars machines m)@
61
	    (rename_current_list (full_memory_vars machines m)) @
62
	    (rename_mid_list (full_memory_vars machines m)) @
63
	    (rename_next_list (full_memory_vars machines m)) @
64
	    (rename_machine_list m.mname.node_id m.mstep.step_locals)
65
	)
521
      let vars =
522
        List.map decl_var 
523
      	  (
524
	    (inout_vars machines m)@
525
	      (rename_current_list (full_memory_vars machines m)) @
526
	        (rename_mid_list (full_memory_vars machines m)) @
527
	          (rename_next_list (full_memory_vars machines m)) @
528
	            (rename_machine_list m.mname.node_id m.mstep.step_locals)
529
	  )
66 530
      in
67
      ()
68
     (*
531
      
69 532
      if is_stateless m then
70 533
	begin
71 534
	  (* Declaring single predicate *)
72
	  fprintf fmt "(declare-rel %a (%a))@."
73
	    pp_machine_stateless_name m.mname.node_id
74
	    (Utils.fprintf_list ~sep:" " pp_type)
75
	    (List.map (fun v -> v.var_type) (inout_vars machines m));
76

  
535
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in          
77 536
          match m.mstep.step_asserts with
78 537
	  | [] ->
79 538
	     begin
......
84 543
	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
85 544
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
86 545
		 pp_machine_stateless_name m.mname.node_id
87
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
546
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (inout_vars machines m);
88 547
	     end
89 548
	  | assertsl ->
90 549
	     begin
91
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
550
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
92 551
	       
93 552
	       fprintf fmt "; Stateless step rule with Assertions @.";
94 553
	       (*Rule for step*)
......
96 555
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
97 556
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
98 557
		 pp_machine_stateless_name m.mname.node_id
99
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
558
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
100 559
	  
101 560
	     end
102 561
	       
......
104 563
      else
105 564
	begin
106 565
	  (* Declaring predicate *)
107
	  fprintf fmt "(declare-rel %a (%a))@."
108
	    pp_machine_reset_name m.mname.node_id
109
	    (Utils.fprintf_list ~sep:" " pp_type)
110
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
111

  
112
	  fprintf fmt "(declare-rel %a (%a))@."
113
	    pp_machine_step_name m.mname.node_id
114
	    (Utils.fprintf_list ~sep:" " pp_type)
115
	    (List.map (fun v -> v.var_type) (step_vars machines m));
116

  
117
	  pp_print_newline fmt ();
566
	  let _ = decl_rel (machine_reset_name m.mname.node_id) (reset_vars machines m) in
567
          let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in
118 568

  
119 569
	  (* Rule for reset *)
120 570
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
121 571
	    (pp_machine_reset machines) m 
122 572
	    pp_machine_reset_name m.mname.node_id
123
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
573
	    (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (reset_vars machines m);
124 574

  
125 575
          match m.mstep.step_asserts with
126 576
	  | [] ->
......
131 581
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
132 582
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
133 583
		 pp_machine_step_name m.mname.node_id
134
		 (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
584
		 (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (step_vars machines m);
135 585
	     end
136 586
	  | assertsl -> 
137 587
	     begin
138
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
588
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
139 589
	       (* print_string pp_val; *)
140 590
	       fprintf fmt "; Step rule with Assertions @.";
141 591
	       
......
144 594
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
145 595
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
146 596
		 pp_machine_step_name m.mname.node_id
147
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
597
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
148 598
	     end
149 599
	       
150 600
     	       
151 601
	end
152
      *)  end
602
    end
153 603

  
154
           
604
let param_stat = ref false
605
let param_eldarica = ref false
606
let param_utvpi = ref false
607
let param_tosmt = ref false
608
let param_pp = ref false
609
             
155 610
module Verifier =
156 611
  (struct
157 612
    include VerifierType.Default
158 613
    let name = "zustre"
159
    let options = []
614
    let options = [
615
        "-stat", Arg.Set param_stat, "print statistics";
616
        "-eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules";
617
        "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
618
        "-tosmt", Arg.Set param_tosmt, "Print low-level (possibly unreadable) SMT2 statements";
619
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
620
      ]
621
                
160 622
    let activate () = (
161 623
        active := true;
162 624
        Options.output := "horn";
......
168 630
      assert(!Options.output = "horn");
169 631
      Backends.get_normalization_params ()
170 632

  
633
    let setup_solver () =
634
      let fp = Z3.Fixedpoint.mk_fixedpoint !ctx in
635
      (* let help = Z3.Fixedpoint.get_help fp in
636
       * Format.eprintf "Fp help : %s@." help;
637
       * 
638
       * let solver =Z3.Solver.mk_solver !ctx None in
639
       * let help = Z3.Solver.get_help solver in
640
       * Format.eprintf "Z3 help : %s@." help; *)
641
      
642
      let module P = Z3.Params in
643
      let module S = Z3.Symbol in
644
      let mks = S.mk_string !ctx in
645
      let params = P.mk_params !ctx in
646

  
647
      (* self.fp.set (engine='spacer') *)
648
      P.add_symbol params (mks "engine") (mks "spacer");
649
      
650
       (* #z3.set_option(rational_to_decimal=True) *)
651
       (* #self.fp.set('precision',30) *)
652
      if !param_stat then 
653
        (* self.fp.set('print_statistics',True) *)
654
        P.add_bool params (mks "print_statistics") true;
655

  
656
      (* Dont know where to find this parameter *)
657
      (* if !param_spacer_verbose then
658
         *   if self.args.spacer_verbose: 
659
         *        z3.set_option (verbose=1) *)
660

  
661
      (* The option is not recogined*)
662
      (* self.fp.set('use_heavy_mev',True) *)
663
      (* P.add_bool params (mks "use_heavy_mev") true; *)
664
      
665
      (* self.fp.set('pdr.flexible_trace',True) *)
666
      P.add_bool params (mks "pdr.flexible_trace") true;
667

  
668
      (* self.fp.set('reset_obligation_queue',False) *)
669
      P.add_bool params (mks "spacer.reset_obligation_queue") false;
670

  
671
      (* self.fp.set('spacer.elim_aux',False) *)
672
      P.add_bool params (mks "spacer.elim_aux") false;
673

  
674
      (* if self.args.eldarica:
675
        *     self.fp.set('print_fixedpoint_extensions', False) *)
676
      if !param_eldarica then
677
        P.add_bool params (mks "print_fixedpoint_extensions") false;
678
      
679
      (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
680
      if !param_utvpi then
681
        P.add_bool params (mks "pdr.utvpi") false;
682

  
683
      (* if self.args.tosmt:
684
       *        self.log.info("Setting low level printing")
685
       *        self.fp.set ('print.low_level_smt2',True) *)
686
      if !param_tosmt then
687
        P.add_bool params (mks "print.low_level_smt2") true;
688

  
689
      (* if not self.args.pp:
690
       *        self.log.info("No pre-processing")
691
       *        self.fp.set ('xform.slice', False)
692
       *        self.fp.set ('xform.inline_linear',False)
693
       *        self.fp.set ('xform.inline_eager',False) *\) *)
694
      if !param_pp then (
695
        P.add_bool params (mks "xform.slice") false;
696
        P.add_bool params (mks "xform.inline_linear") false;
697
        P.add_bool params (mks "xform.inline_eager") false
698
      );
699
      Z3.Fixedpoint.set_parameters fp params
700
        
701
      
171 702
    let run basename prog machines =
172 703
      let machines = Machine_code.arrow_machine::machines in
173 704
      let machines = preprocess machines in
705
      setup_solver ();
174 706
      decl_sorts ();
175 707
      List.iter (decl_machine machines) (List.rev machines);
176 708

  

Also available in: Unified diff