Project

General

Profile

Revision 7d77632f

View differences:

src/tools/zustre/zustre_analyze.ml
11 11
open Zustre_common
12 12
open Zustre_data
13 13

  
14
let idx_0 = Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 
15
let uid_0 = Z3.Z3List.nil uid_sort 
16
	    
14 17
let check machines node =
15 18

  
16 19
  let machine = get_machine machines node in
......
41 44
  (* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ?
42 45
     Faut-il declarer les "rel" dans la hashtbl ?
43 46
  *)
44
  
47

  
48
  let main_name node_id = "MAIN" ^ "_" ^ node_id in
49
    
45 50
  let decl_main =
46
    decl_rel
47
      ("MAIN" ^ "_" ^ node_id)
51
    decl_rel ~no_additional_vars:true
52
      (main_name node_id)
48 53
      (int_sort::(List.map (fun v -> type_to_sort v.var_type) (main_memory_next))) in
49 54

  
50 55
  
51 56
  
52 57
  (* Init case *)
53
  let decl_init = decl_rel "INIT_STATE" [] in
58
  let decl_init = decl_rel ~no_additional_vars:true "INIT_STATE" [] in
54 59

  
55 60
  (* (special) rule INIT_STATE *)
56 61
  let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
......
68 73
    Z3.Expr.mk_app
69 74
      !ctx
70 75
      decl_main
71
      ((Z3.Arithmetic.Integer.mk_numeral_i !ctx 0)::(List.map horn_var_to_expr main_memory_next))
76
      (idx_0::(* uid_0:: *)(List.map horn_var_to_expr main_memory_next))
72 77
  in
73 78
  (* Special case when the main node is stateless *)
74 79
  let _ =
......
89 94
	      Z3.Expr.mk_app !ctx decl_init [];
90 95
	      Z3.Expr.mk_app !ctx
91 96
		(get_fdecl (machine_stateless_name node))
92
		(List.map horn_var_to_expr vars) 
97
		(idx_0::uid_0::(List.map horn_var_to_expr vars))
93 98
	    ]
94 99
	in
95 100
	add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
......
113 118
	      Z3.Expr.mk_app !ctx decl_init [];
114 119
	      Z3.Expr.mk_app !ctx
115 120
		(get_fdecl (machine_reset_name node))
116
		(List.map horn_var_to_expr (reset_vars machines machine));
121
		(idx_0::uid_0::List.map horn_var_to_expr (reset_vars machines machine));
117 122
	      Z3.Expr.mk_app !ctx
118 123
		(get_fdecl (machine_step_name node))
119
		(List.map horn_var_to_expr (step_vars_m_x machines machine))
124
		(idx_0::uid_0::List.map horn_var_to_expr (step_vars_m_x machines machine))
120 125
	    ]
121 126
	in
122 127

  
......
148 153
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) *)
149 154

  
150 155
  let k = Corelang.dummy_var_decl "k" Type_predef.type_int (*Corelang.mktyp Location.dummy_loc Types.type_int*) in
151
  let k_var = decl_var k in
156
  let k_var = Z3.Expr.mk_const_f !ctx (decl_var k) in
152 157
  
153 158
  let horn_head = 
154 159
    Z3.Expr.mk_app
......
156 161
      decl_main
157 162
      ((Z3.Arithmetic.mk_add
158 163
	  !ctx
159
	  [Z3.Expr.mk_const_f !ctx k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1]
164
	  [k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1]
160 165
       )::(List.map horn_var_to_expr main_memory_next))
161 166
  in
162 167
  let horn_body =
163 168
    Z3.Boolean.mk_and !ctx
164 169
      [
165
	Z3.Expr.mk_app !ctx decl_main (Z3.Expr.mk_const_f !ctx k_var::(List.map horn_var_to_expr main_memory_current));
166
	Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (List.map horn_var_to_expr (step_vars machines machine))
170
	Z3.Expr.mk_app !ctx decl_main (k_var::(List.map horn_var_to_expr main_memory_current));
171
	Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (k_var::uid_0::List.map horn_var_to_expr (step_vars machines machine))
167 172
      ]
168 173
  in
169 174
  (* Vars contains all vars: in_out, current, mid, neXt memories *)
......
175 180

  
176 181

  
177 182
  (* Property def *)
178
  let decl_err = decl_rel "ERR" [] in
183
  let decl_err = decl_rel ~no_additional_vars:true "ERR" [] in
179 184

  
180 185
  let prop =
181 186
    Z3.Boolean.mk_and !ctx (List.map horn_var_to_expr main_output)
......
187 192
	      (
188 193
		Z3.Boolean.mk_and !ctx
189 194
		  [not_prop;
190
		   Z3.Expr.mk_app !ctx decl_main (Z3.Expr.mk_const_f !ctx k_var::List.map horn_var_to_expr main_memory_next);
195
		   Z3.Expr.mk_app !ctx decl_main (k_var::List.map horn_var_to_expr main_memory_next);
191 196
		  ]
192 197
	      )
193 198
	      (Z3.Expr.mk_app !ctx decl_err []))
src/tools/zustre/zustre_cex.ml
46 46
  let nb_outputs = List.length inputs in
47 47
  let nb_mems = List.length (full_memory_vars machines machine) in
48 48
  
49
  let main =
50
    List.fold_left (fun accu conj ->
49
  let main, funs =
50
    List.fold_left (fun (main, funs) conj ->
51 51
    (* Filtering out non MAIN decls *)
52 52
    let func_decl = Z3.Expr.get_func_decl conj in
53 53
    let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in
54 54
    (* Focusing only on MAIN_nodeid predicates *)
55 55
    if node_name = "MAIN_" ^ node_id then
56 56
      (* Extracting info *)
57
      (* Recall that MAIN args are 
58
	 main_input @ 
59
	 (full_memory_vars machines machine) @
60
	 main_output   *)
57
      (* Recall that MAIN args are in@mems@out *)
61 58
      let args = Z3.Expr.get_args conj in
62 59
      if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then
63 60
	let id = Z3.Arithmetic.Integer.get_int (List.hd args) in
64 61
	let input_values = Utils.List.extract args 1 (1 + nb_inputs) in
65 62
	let output_values = Utils.List.extract args (1+nb_inputs+nb_mems) (1 + nb_inputs + nb_mems + nb_outputs) in
66
	(id, (input_values, output_values))::accu
63
	(id, (input_values, output_values))::main, funs
67 64
      else
68 65
	assert false
69 66
    else
70
      accu 
71
  ) [] conjuncts
67
      let reg = Str.regexp_string "[a-z]*_step" in
68
      if Str.string_match reg node_name 0 then (
69
	let actual_name = Str.matched_group 0 node_name in
70
	Format.eprintf "Name %s@." actual_name;
71
	main, funs
72
      )
73
      else (
74
	Format.eprintf "pas matché %s@." node_name;
75
	main, funs
76
      )
77
    ) ((* main*) [],(* other functions *) []) conjuncts
72 78
  in
73 79
  let main = List.sort (fun (id1, _) (id2, _) -> compare id1 id2) main in
74 80
  List.iter (
......
147 153
  (*     Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp); *)
148 154

  
149 155
  let stats_entries =   Z3.Statistics.get_entries stats in
150
  List.iter (fun e -> Format.eprintf "%s@.@?"
151
    (Z3.Statistics.Entry.to_string e)
156
  (* List.iter (fun e -> Format.eprintf "%s@.@?" *)
157
  (*   (Z3.Statistics.Entry.to_string e) *)
152 158
    
153
  ) stats_entries;
159
  (* ) stats_entries; *)
154 160
  let json : Yojson.json =
155 161
    `Assoc [
156 162
      "Results",
src/tools/zustre/zustre_common.ml
90 90
  | _                     -> Format.eprintf "internal error: pp_type %a@."
91 91
                               Types.print_ty t; assert false
92 92

  
93

  
94
(* let idx_var = *)
95
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort  *)
96
    
97
(* let uid_var = *)
98
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort  *)
99

  
93 100
(** Func decls
94 101

  
95 102
    Similarly fun_decls are registerd, by their name, into a hashtbl. The
......
116 123
  register_fdecl id.var_id fdecl;
117 124
  fdecl
118 125

  
119
let decl_rel name args_sorts =
120
  (*verifier ce qui est construit. On veut un declare-rel *)
126
let idx_sort = int_sort
127
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort
128
let uid_conc = 
129
  let fd = Z3.Z3List.get_cons_decl uid_sort in
130
  fun head tail -> Z3.FuncDecl.apply fd [head;tail]
131

  
132
let get_instance_uid =
133
  let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in
134
  let cpt = ref 0 in
135
  fun i ->
136
    let id =
137
      if Hashtbl.mem hash i then
138
	Hashtbl.find hash i
139
      else (
140
	incr cpt;
141
	Hashtbl.add hash i !cpt;
142
	!cpt
143
      )
144
    in
145
    Z3.Arithmetic.Integer.mk_numeral_i !ctx id
146
  
147

  
148
  
149
let decl_rel ?(no_additional_vars=false) name args_sorts =
150
  (* Enriching arg_sorts with two new variables: a counting index and an
151
     uid *)
152
  let args_sorts =
153
    if no_additional_vars then args_sorts else idx_sort::uid_sort::args_sorts in
121 154
  
122 155
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
123 156
  if !debug then
......
133 166
  fdecl
134 167
  
135 168

  
169

  
170
(* Shared variables to describe counter and uid *)
171

  
172
let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int
173
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) 
174
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int
175
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort 
176
let _ = register_fdecl "__uid__"  uid_fd  
177
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd 
178

  
136 179
(** Conversion functions
137 180

  
138 181
    The following is similar to the Horn backend. Each printing function is
......
412 455
  let (n,_) = List.assoc i m.minstances in
413 456
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
414 457
  let vars =
415
    (
416
      (rename_machine_list
417
	 (concat m.mname.node_id i)
418
	 (rename_current_list (full_memory_vars machines target_machine))
419
      ) 
420
      @
421
	(rename_machine_list
422
	   (concat m.mname.node_id i)
423
	   (rename_mid_list (full_memory_vars machines target_machine))
424
	)
458
    (rename_machine_list
459
       (concat m.mname.node_id i)
460
       (rename_current_list (full_memory_vars machines target_machine))@  (rename_mid_list (full_memory_vars machines target_machine))
425 461
    )
462
    
426 463
  in
427 464
  let expr =
428 465
    Z3.Expr.mk_app
429 466
      !ctx
430 467
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
431
      (List.map (horn_var_to_expr) vars)
468
      (List.map (horn_var_to_expr) (idx::uid::vars))
432 469
  in
433 470
  [expr]
434 471

  
435 472
let instance_call_to_exprs machines reset_instances m i inputs outputs =
436 473
  let self = m.mname.node_id in
474

  
475
  (* Building call args *)
476
  let idx_uid_inout =
477
    (* Additional input to register step counters, and uid *)
478
    let idx = horn_var_to_expr idx in
479
    let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in
480
    let inout = 
481
      List.map (horn_val_to_expr self)
482
	(inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs))
483
    in
484
    idx::uid::inout
485
  in
486
    
437 487
  try (* stateful node instance *)
438 488
    begin
439 489
      let (n,_) = List.assoc i m.minstances in
......
454 504
      let next_mems = rename_mems rename_next_list in
455 505

  
456 506
      let call_expr = 
457
      match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
458
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
507
	match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
508
	| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
459 509
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
460 510
            Z3.Boolean.mk_eq !ctx
461 511
              ( (* output var *)
......
477 527
              (Z3.Boolean.mk_false !ctx)
478 528
          in
479 529
          [stmt1; stmt2]
480
      end
481

  
482
      | node_name_n ->
483
         let expr = 
484
           Z3.Expr.mk_app
485
             !ctx
486
             (get_fdecl (machine_step_name (node_name n)))
487
             ( (* Arguments are input, output, mid_mems, next_mems *)
488
               (
489
                 List.map (horn_val_to_expr self) (
490
                     inputs @
491
	               (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
492
                   )
493
               ) @ (
494
                 List.map (horn_var_to_expr) (mid_mems@next_mems)
495
	       )
496
             )
497
         in
498
         [expr]
530
	end
531

  
532
	| node_name_n ->
533
           let expr = 
534
             Z3.Expr.mk_app
535
               !ctx
536
               (get_fdecl (machine_step_name (node_name n)))
537
               ( (* Arguments are input, output, mid_mems, next_mems *)
538
		 idx_uid_inout @ List.map (horn_var_to_expr) (mid_mems@next_mems)
539
		    
540
               )
541
           in
542
           [expr]
499 543
      in
500 544

  
501 545
      reset_exprs@call_expr
......
506 550
      Z3.Expr.mk_app
507 551
        !ctx
508 552
        (get_fdecl (machine_stateless_name (node_name n)))
509
        ((* Arguments are inputs, outputs *)
510
         List.map (horn_val_to_expr self)
511
           (
512
             inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
513
           )
514
        )
553
        idx_uid_inout 	  (* Arguments are inputs, outputs *)
515 554
    in
516 555
    [expr]
517 556
  )
......
747 786
	  !ctx
748 787
	  (get_fdecl (name ^ "_reset"))
749 788
	  (List.map (horn_var_to_expr)
750
	     (rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
751
	  )
789
	     (idx::uid:: (* Additional vars: counters, uid *)
790
	      	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
791
	  ))
752 792
	  
753 793
      )
754 794
    ) m.minstances
......
798 838
	    Z3.Expr.mk_app
799 839
	      !ctx
800 840
	      (get_fdecl (machine_stateless_name m.mname.node_id))
801
	      (List.map (horn_var_to_expr) vars)
841
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
802 842
	  in
803 843
	  (* this line seems useless *)
804
	  let vars = vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
844
	  let vars = idx::uid::vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
805 845
	  (* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
806 846
	  match m.mstep.step_asserts with
807 847
	  | [] ->
......
836 876
	    Z3.Expr.mk_app
837 877
	      !ctx
838 878
	      (get_fdecl (machine_reset_name m.mname.node_id))
839
	      (List.map (horn_var_to_expr) vars)
879
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
840 880
	  in
841 881

  
842 882
	  
843 883
	  let _ =
844
	    add_rule vars (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
884
	    add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
845 885
	      
846 886
	  in
847 887

  
......
860 900
	    Z3.Expr.mk_app
861 901
	      !ctx
862 902
	      (get_fdecl (machine_step_name m.mname.node_id))
863
	      (List.map (horn_var_to_expr) vars)
903
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
864 904
	  in
865 905
	  match m.mstep.step_asserts with
866 906
	  | [] ->
867 907
	     begin
868 908
	       (* Rule for single predicate *) 
869 909
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
870
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
910
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
871 911
		 
872 912
	     end
873 913
	  | assertsl ->
......
878 918
		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
879 919
	       in
880 920
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
881
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
921
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
882 922
		 
883 923
	     end
884 924
     	       
src/utils.ml
392 392
end
393 393

  
394 394
let get_date () =
395
  let tm = Unix.localtime (Unix.time ()) in
395
  let tm = Unix.localtime (Unix.time ()) in 
396 396
  let fmt = Format.str_formatter in
397
  let open Unix in
398
  let _ =
399
    Format.fprintf fmt
400
      "%i/%i/%i %ih%i:%i"
401
      tm.tm_year
402
      tm.tm_mon
403
      tm.tm_mday
404
      tm.tm_hour
405
      tm.tm_min
406
      tm.tm_sec
407
  in
397
  pp_date fmt tm;
398
  (* let open Unix in *)
399
  (* let _ = *)
400
  (*   Format.fprintf fmt *)
401
  (*     "%i/%i/%i %ih%i:%i" *)
402
  (*     tm.tm_year *)
403
  (*     tm.tm_mon *)
404
  (*     tm.tm_mday *)
405
  (*     tm.tm_hour *)
406
  (*     tm.tm_min *)
407
  (*     tm.tm_sec *)
408
  (* in *)
408 409
  Format.flush_str_formatter ()
409 410

  
410 411
(* Local Variables: *)

Also available in: Unified diff