Project

General

Profile

« Previous | Next » 

Revision 4300981b

Added by Pierre-Loïc Garoche over 3 years ago

Zustre: timeout and slicing

View differences:

src/tools/zustre/zustre_analyze.ml
200 200

  
201 201
      (* Debug instructions *)
202 202
  let rules_expr = Z3.Fixedpoint.get_rules !fp in
203
  if true then
203
  if !debug then
204 204
    Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
205 205
    (Utils.fprintf_list ~sep:"@ "
206 206
       (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
207
    rules_expr;
208
  let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
209

  
210
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
211
  match res_status with
212
  | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex decl_err
213
  
214
  | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
215
       let expr_opt = Z3.Fixedpoint.get_answer !fp in
216
       match expr_opt with
217
	 None -> Format.eprintf "Unsat No feedback@."
218
       | Some e -> Format.eprintf "Unsat Result: %s@." (Z3.Expr.to_string e)
219
  )
220
  | Z3.Solver.UNKNOWN -> ()
221
      
207
      rules_expr;
208
  try
209
    let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
210
    
211
    Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
212
    match res_status with
213
    | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex decl_err
214
       
215
    | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
216
      let expr_opt = Z3.Fixedpoint.get_answer !fp in
217
      match expr_opt with
218
	None -> if !debug then Format.eprintf "Unsat No feedback@."
219
      | Some e -> if !debug then Format.eprintf "Unsat Result: %s@." (Z3.Expr.to_string e)
220
    )
221
    | Z3.Solver.UNKNOWN -> ()
222
  with Z3.Error msg -> Format.eprintf "Z3 failure: %s@." msg; () 
222 223
(* Local Variables: *)
223 224
(* compile-command:"make -C ../.." *)
224 225
(* End: *)
src/tools/zustre/zustre_common.ml
120 120
  (*verifier ce qui est construit. On veut un declare-rel *)
121 121
  
122 122
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
123
  if !debug then
124
    Format.eprintf "Registering fdecl %s (%a)@."
125
      name
126
      (Utils.fprintf_list ~sep:"@ "
127
	 (fun fmt sort -> Format.fprintf fmt "%s" (Z3.Sort.to_string sort)))
128
      args_sorts
129
  ;
123 130
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
124 131
  Z3.Fixedpoint.register_relation !fp fdecl;
125 132
  register_fdecl name fdecl;
......
675 682
  let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
676 683
  let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
677 684

  
678
  (* Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @." *)
679
  (*   (Z3.Expr.to_string expr) *)
680
  (*   (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars) *)
681
  (*   ; *)
685
  if !debug then (
686
    Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."
687
      (Z3.Expr.to_string expr)
688
      (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars)
689
  )
690
    ;
682 691
  let expr = Z3.Quantifier.mk_forall_const
683 692
    !ctx  (* context *)
684 693
    (List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *)
......
768 777
      	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
769 778
      	  )
770 779
      in
771
      
772 780
      if is_stateless m then
773 781
	begin
782
	  if !debug then 
783
	    Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id;
784

  
774 785
	  (* Declaring single predicate *)
775 786
	  let vars = inout_vars machines m in
776 787
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
777 788
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
789
	  
778 790
	  let horn_body, _ (* don't care for reset here *) =
779 791
	    instrs_to_expr
780 792
	      machines
......
788 800
	      (get_fdecl (machine_stateless_name m.mname.node_id))
789 801
	      (List.map (horn_var_to_expr) vars)
790 802
	  in
803
	  (* this line seems useless *)
791 804
	  let vars = vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
805
	  (* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
792 806
	  match m.mstep.step_asserts with
793 807
	  | [] ->
794 808
	     begin
795 809
	       (* Rule for single predicate : "; Stateless step rule @." *)
796
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
810
	       (*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*)
811
	       (* TODO clean code *)
812
	       (* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
797 813
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
798 814
		 
799 815
	     end
src/tools/zustre/zustre_data.ml
9 9

  
10 10
let decls: (Lustre_types.ident, Z3.FuncDecl.func_decl) Hashtbl.t = Hashtbl.create 13
11 11

  
12
let debug = ref false
13
let timeout = ref 10000 (* default : 10 s = 10 000 ms *)
12 14

  
13 15
(* Local Variables: *)
14 16
(* compile-command:"make -C ../.." *)
src/tools/zustre/zustre_verifier.ml
55 55
        "-eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules";
56 56
        "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
57 57
        "-tosmt", Arg.Set param_tosmt, "Print low-level (possibly unreadable) SMT2 statements";
58
        "-timeout", Arg.Set_int timeout, "Set timeout in ms (default 10000 = 10 s)";
58 59
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
60
        "-debug", Arg.Set debug, "Debug mode";
59 61
      ]
60 62
                
61 63
    let activate () = (
......
77 79
       * let solver =Z3.Solver.mk_solver !ctx None in
78 80
       * let help = Z3.Solver.get_help solver in
79 81
       * Format.eprintf "Z3 help : %s@." help; *)
80
      
82

  
81 83
      let module P = Z3.Params in
82 84
      let module S = Z3.Symbol in
83 85
      let mks = S.mk_string !ctx in
84
      let params = P.mk_params !ctx in
86
      
87
      (* Fixpoint Engine parameters *)
88
      
89
      let fp_params = P.mk_params !ctx in
85 90

  
86 91
      (* (\* self.fp.set (engine='spacer') *\) *)
87
      P.add_symbol params (mks "engine") (mks "spacer");
88
      (* P.add_symbol params (mks "engine") (mks "pdr");  *)
92
      P.add_symbol fp_params (mks "engine") (mks "spacer");
93
      (* P.add_symbol fp_params (mks "engine") (mks "pdr");  *)
89 94
      
90 95
       (* #z3.set_option(rational_to_decimal=True) *)
91 96
       (* #self.fp.set('precision',30) *)
92 97
      if !param_stat then 
93 98
        (* self.fp.set('print_statistics',True) *)
94
        P.add_bool params (mks "print_statistics") true;
99
        P.add_bool fp_params (mks "print_statistics") true;
95 100

  
96 101
      (* Dont know where to find this parameter *)
97 102
      (* if !param_spacer_verbose then
......
100 105

  
101 106
      (* The option is not recogined*)
102 107
      (* self.fp.set('use_heavy_mev',True) *)
103
      (* P.add_bool params (mks "use_heavy_mev") true; *)
108
      (* P.add_bool fp_params (mks "use_heavy_mev") true; *)
104 109
      
105 110
      (* self.fp.set('pdr.flexible_trace',True) *)
106
      P.add_bool params (mks "pdr.flexible_trace") true;
111
      P.add_bool fp_params (mks "pdr.flexible_trace") true;
107 112

  
108 113
      (* self.fp.set('reset_obligation_queue',False) *)
109
      P.add_bool params (mks "spacer.reset_obligation_queue") false;
114
      P.add_bool fp_params (mks "spacer.reset_obligation_queue") false;
110 115

  
111 116
      (* self.fp.set('spacer.elim_aux',False) *)
112
      P.add_bool params (mks "spacer.elim_aux") false;
117
      P.add_bool fp_params (mks "spacer.elim_aux") false;
113 118

  
114 119
      (* if self.args.eldarica:
115 120
        *     self.fp.set('print_fixedpoint_extensions', False) *)
116 121
      if !param_eldarica then
117
        P.add_bool params (mks "print_fixedpoint_extensions") false;
122
        P.add_bool fp_params (mks "print_fixedpoint_extensions") false;
118 123
      
119 124
      (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
120 125
      if !param_utvpi then
121
        P.add_bool params (mks "pdr.utvpi") false;
126
        P.add_bool fp_params (mks "pdr.utvpi") false;
122 127

  
123 128
      (* if self.args.tosmt:
124 129
       *        self.log.info("Setting low level printing")
125 130
       *        self.fp.set ('print.low_level_smt2',True) *)
126 131
      if !param_tosmt then
127
        P.add_bool params (mks "print.low_level_smt2") true;
132
        P.add_bool fp_params (mks "print.low_level_smt2") true;
128 133

  
129 134
      (* if not self.args.pp:
130 135
       *        self.log.info("No pre-processing")
......
132 137
       *        self.fp.set ('xform.inline_linear',False)
133 138
       *        self.fp.set ('xform.inline_eager',False) *\) *)
134 139
      if !param_pp then (
135
        P.add_bool params (mks "xform.slice") false;
136
        P.add_bool params (mks "xform.inline_linear") false;
137
        P.add_bool params (mks "xform.inline_eager") false
140
        P.add_bool fp_params (mks "xform.slice") false;
141
        P.add_bool fp_params (mks "xform.inline_linear") false;
142
        P.add_bool fp_params (mks "xform.inline_eager") false
138 143
      );
139
      Z3.Fixedpoint.set_parameters !fp params
140
              
144

  
145

  
146
      (* Ploc's options. Do not seem to have any effect yet *)
147
      P.add_bool fp_params (mks "print_answer") true;
148
      P.add_bool fp_params (mks "print_certificate") true;
149
      P.add_bool fp_params (mks "xform.slice") false;
150

  
151
      (* Adding a timeout *)
152
      P.add_int fp_params (mks "timeout") !timeout;
153

  
154
      Z3.Fixedpoint.set_parameters !fp fp_params
141 155
      
142 156
    let run basename prog machines =
143 157
      let machines = Machine_code_common.arrow_machine::machines in

Also available in: Unified diff