Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/tools/zustre/zustre_verifier.ml
1

  
2 1
(*
3 2
TODO
4 3

  
......
34 33

  
35 34
*)
36 35

  
37

  
38 36
open Zustre_common
39 37
open Zustre_data
40 38

  
41 39
let param_stat = ref false
40

  
42 41
let param_eldarica = ref false
42

  
43 43
let param_utvpi = ref false
44

  
44 45
let param_tosmt = ref false
46

  
45 47
let param_pp = ref false
46 48

  
47 49
let active = ref false
48 50

  
49
module Verifier =
50
  (struct
51
    include VerifierType.Default
52
    let name = "zustre"
53
    let options = [
54
        "-stat", Arg.Set param_stat, "print statistics";
55
        "-eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules";
56
        "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
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)";
59
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
60
        "-debug", Arg.Set debug, "Debug mode";
61
      ]
62
                
63
    let activate () = (
64
        active := true;
65
        Options.output := "horn";
66
      )
67

  
68
    let is_active () = !active
69

  
70
    let get_normalization_params () =
71
      (* make sure the output is "Horn" *)
72
      assert(!Options.output = "horn");
73
      Backends.get_normalization_params ()
74

  
75
    let setup_solver () =
76
      fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
77
      (* let help = Z3.Fixedpoint.get_help fp in
78
       * Format.eprintf "Fp help : %s@." help;
79
       * 
80
       * let solver =Z3.Solver.mk_solver !ctx None in
81
       * let help = Z3.Solver.get_help solver in
82
       * Format.eprintf "Z3 help : %s@." help; *)
83

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

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

  
102
      (* Dont know where to find this parameter *)
103
      (* if !param_spacer_verbose then
104
         *   if self.args.spacer_verbose: 
105
         *        z3.set_option (verbose=1) *)
106

  
107
      (* The option is not recogined*)
108
      (* self.fp.set('use_heavy_mev',True) *)
109
      (* P.add_bool fp_params (mks "use_heavy_mev") true; *)
110
      
111
      (* self.fp.set('pdr.flexible_trace',True) *)
112
      P.add_bool fp_params (mks "pdr.flexible_trace") true;
113

  
114
      (* self.fp.set('reset_obligation_queue',False) *)
115
      P.add_bool fp_params (mks "spacer.reset_obligation_queue") false;
116

  
117
      (* self.fp.set('spacer.elim_aux',False) *)
118
      P.add_bool fp_params (mks "spacer.elim_aux") false;
119

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

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

  
135
      (* if not self.args.pp:
136
       *        self.log.info("No pre-processing")
137
       *        self.fp.set ('xform.slice', False)
138
       *        self.fp.set ('xform.inline_linear',False)
139
       *        self.fp.set ('xform.inline_eager',False) *\) *)
140
      if not !param_pp then (
141
	(* Mandatory to print all steps and recover cex *)
142
        P.add_bool fp_params (mks "xform.slice") false;
143
        P.add_bool fp_params (mks "xform.inline_linear") false;
144
        P.add_bool fp_params (mks "xform.inline_eager") false
145
      );
146

  
147

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

  
153
      (* P.add_bool fp_params (mks "print_statistics") true; *)
154
      (* P.add_bool fp_params (mks "print_certificate") true;  *)
155

  
156
      (* Adding a timeout *)
157
      P.add_int fp_params (mks "timeout") !timeout;
158

  
159
      Z3.Fixedpoint.set_parameters !fp fp_params
160
      
161
    let run ~basename _prog machines =
162
      let machines = Machine_code_common.arrow_machine::machines in
163
      let machines = preprocess machines in
164
      setup_solver ();
165

  
166

  
167
      (* TODO
168
	 load deps: cf print_dep in horn_backend.ml
169

  
170
      
171
      if false then (
172
	
173
	let queries = Z3.Fixedpoint.parse_file !fp "nstep.smt2" in
174

  
175
	(* Debug instructions *)
176
	
177

  
178
	
179
	let rules_expr = Z3.Fixedpoint.get_rules !fp in
180
	Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
181
      	  (Utils.fprintf_list ~sep:"@ "
182
      	     (fun fmt e ->
183
	       (* let e2 = Z3.Quantifier.get_body eq in *)
184
	       (* let fd = Z3.Expr.get_func_decl e in *)
185
	       Format.fprintf fmt "Rule: %s@."
186
		 (Z3.Expr.to_string e);
187
	     )) rules_expr;
188
	
189
	let _ = List.map extract_expr_fds rules_expr in
190
	Format.eprintf "%t" pp_fdecls;
191

  
192
	let decl_err = List.hd queries in
193
      	let res_status = Z3.Fixedpoint.query !fp decl_err in
194
	
195
	Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
196
	(* let _ =  *)
197
	(*   match res_status with *)
198
	(*   | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err *)
199
	(*   | _ -> () *)
200
	(* in *)
201
	exit 0
202
      )
203
      else if false then (
204

  
205
	(* No queries here *)
206
	let _ = Z3.Fixedpoint.parse_file !fp "mini_decl.smt2" in
207

  
208
	(* Debug instructions *)
209
	
210

  
211
	
212
	let rules_expr = Z3.Fixedpoint.get_rules !fp in
213
	Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
214
      	  (Utils.fprintf_list ~sep:"@ "
215
      	     (fun fmt e ->
216
	       (* let e2 = Z3.Quantifier.get_body eq in *)
217
	       (* let fd = Z3.Expr.get_func_decl e in *)
218
	       Format.fprintf fmt "Rule: %s@."
219
		 (Z3.Expr.to_string e);
220
	     )) rules_expr;
221
	
222
	let _ = List.map extract_expr_fds rules_expr in
223
	Format.eprintf "%t" pp_fdecls;
224

  
225
	if !Options.main_node <> "" then
226
      	  begin
227
      	    Zustre_analyze.check machines !Options.main_node
228

  
229
      	  end
230
	else
231
      	  failwith "Require main node";
232

  
233
	()	
234
      )
235
      else 
236

  
237
       *)
238

  
239
      (
240
	
241
	
242
	decl_sorts ();
243
	
244
	List.iter (decl_machine machines) (List.rev machines);
245

  
246

  
247
	(* (\* Debug instructions *\) *)
248
	(* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
249
	(* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
250
	(* 	(Utils.fprintf_list ~sep:"@ " *)
251
	(* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
252
	(* 	rules_expr; *)
253

  
254
	if !Options.main_node <> "" then
255
      	  begin
256
      	    Zustre_analyze.check machines !Options.main_node
257

  
258
      	  end
259
	else
260
      	  failwith "Require main node";
261
	
262
	()
263
      )
264
	
265

  
266
	    end: VerifierType.S)
51
module Verifier : VerifierType.S = struct
52
  include VerifierType.Default
53

  
54
  let name = "zustre"
55

  
56
  let options =
57
    [
58
      "-stat", Arg.Set param_stat, "print statistics";
59
      ( "-eldarica",
60
        Arg.Set param_eldarica,
61
        "deactivate fixedpoint extensions when printing rules" );
62
      "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
63
      ( "-tosmt",
64
        Arg.Set param_tosmt,
65
        "Print low-level (possibly unreadable) SMT2 statements" );
66
      ( "-timeout",
67
        Arg.Set_int timeout,
68
        "Set timeout in ms (default 10000 = 10 s)" );
69
      "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
70
      "-debug", Arg.Set debug, "Debug mode";
71
    ]
72

  
73
  let activate () =
74
    active := true;
75
    Options.output := "horn"
76

  
77
  let is_active () = !active
78

  
79
  let get_normalization_params () =
80
    (* make sure the output is "Horn" *)
81
    assert (!Options.output = "horn");
82
    Backends.get_normalization_params ()
83

  
84
  let setup_solver () =
85
    fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
86

  
87
    (* let help = Z3.Fixedpoint.get_help fp in
88
     * Format.eprintf "Fp help : %s@." help;
89
     * 
90
     * let solver =Z3.Solver.mk_solver !ctx None in
91
     * let help = Z3.Solver.get_help solver in
92
     * Format.eprintf "Z3 help : %s@." help; *)
93
    let module P = Z3.Params in
94
    let module S = Z3.Symbol in
95
    let mks = S.mk_string !ctx in
96

  
97
    (* Fixpoint Engine parameters *)
98
    let fp_params = P.mk_params !ctx in
99

  
100
    (* (\* self.fp.set (engine='spacer') *\) *)
101
    P.add_symbol fp_params (mks "engine") (mks "spacer");
102

  
103
    (* P.add_symbol fp_params (mks "engine") (mks "pdr");  *)
104

  
105
    (* #z3.set_option(rational_to_decimal=True) *)
106
    (* #self.fp.set('precision',30) *)
107
    if !param_stat then
108
      (* self.fp.set('print_statistics',True) *)
109
      P.add_bool fp_params (mks "print_statistics") true;
110

  
111
    (* Dont know where to find this parameter *)
112
    (* if !param_spacer_verbose then
113
       *   if self.args.spacer_verbose:
114
       *        z3.set_option (verbose=1) *)
115

  
116
    (* The option is not recogined*)
117
    (* self.fp.set('use_heavy_mev',True) *)
118
    (* P.add_bool fp_params (mks "use_heavy_mev") true; *)
119

  
120
    (* self.fp.set('pdr.flexible_trace',True) *)
121
    P.add_bool fp_params (mks "pdr.flexible_trace") true;
122

  
123
    (* self.fp.set('reset_obligation_queue',False) *)
124
    P.add_bool fp_params (mks "spacer.reset_obligation_queue") false;
125

  
126
    (* self.fp.set('spacer.elim_aux',False) *)
127
    P.add_bool fp_params (mks "spacer.elim_aux") false;
128

  
129
    (* if self.args.eldarica:
130
       *     self.fp.set('print_fixedpoint_extensions', False) *)
131
    if !param_eldarica then
132
      P.add_bool fp_params (mks "print_fixedpoint_extensions") false;
133

  
134
    (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
135
    if !param_utvpi then P.add_bool fp_params (mks "pdr.utvpi") false;
136

  
137
    (* if self.args.tosmt:
138
     *        self.log.info("Setting low level printing")
139
     *        self.fp.set ('print.low_level_smt2',True) *)
140
    if !param_tosmt then P.add_bool fp_params (mks "print.low_level_smt2") true;
141

  
142
    (* if not self.args.pp:
143
     *        self.log.info("No pre-processing")
144
     *        self.fp.set ('xform.slice', False)
145
     *        self.fp.set ('xform.inline_linear',False)
146
     *        self.fp.set ('xform.inline_eager',False) *\) *)
147
    if not !param_pp then (
148
      (* Mandatory to print all steps and recover cex *)
149
      P.add_bool fp_params (mks "xform.slice") false;
150
      P.add_bool fp_params (mks "xform.inline_linear") false;
151
      P.add_bool fp_params (mks "xform.inline_eager") false);
152

  
153
    (* Ploc's options. Do not seem to have any effect yet *)
154
    P.add_bool fp_params (mks "print_answer") true;
155
    (* P.add_bool fp_params (mks "print_certificate") true; *)
156
    P.add_bool fp_params (mks "xform.slice") false;
157

  
158
    (* required to preserve signatures *)
159

  
160
    (* P.add_bool fp_params (mks "print_statistics") true; *)
161
    (* P.add_bool fp_params (mks "print_certificate") true;  *)
162

  
163
    (* Adding a timeout *)
164
    P.add_int fp_params (mks "timeout") !timeout;
165

  
166
    Z3.Fixedpoint.set_parameters !fp fp_params
167

  
168
  let run ~basename _prog machines =
169
    let machines = Machine_code_common.arrow_machine :: machines in
170
    let machines = preprocess machines in
171
    setup_solver ();
172

  
173
    (* TODO
174
        load deps: cf print_dep in horn_backend.ml
175

  
176

  
177
            if false then (
178

  
179
       let queries = Z3.Fixedpoint.parse_file !fp "nstep.smt2" in
180

  
181
       (* Debug instructions *)
182

  
183

  
184

  
185
       let rules_expr = Z3.Fixedpoint.get_rules !fp in
186
       Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
187
            	  (Utils.fprintf_list ~sep:"@ "
188
            	     (fun fmt e ->
189
              (* let e2 = Z3.Quantifier.get_body eq in *)
190
              (* let fd = Z3.Expr.get_func_decl e in *)
191
              Format.fprintf fmt "Rule: %s@."
192
       	 (Z3.Expr.to_string e);
193
            )) rules_expr;
194

  
195
       let _ = List.map extract_expr_fds rules_expr in
196
       Format.eprintf "%t" pp_fdecls;
197

  
198
       let decl_err = List.hd queries in
199
            	let res_status = Z3.Fixedpoint.query !fp decl_err in
200

  
201
       Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
202
       (* let _ =  *)
203
       (*   match res_status with *)
204
       (*   | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err *)
205
       (*   | _ -> () *)
206
       (* in *)
207
       exit 0
208
            )
209
            else if false then (
210

  
211
       (* No queries here *)
212
       let _ = Z3.Fixedpoint.parse_file !fp "mini_decl.smt2" in
213

  
214
       (* Debug instructions *)
215

  
216

  
217

  
218
       let rules_expr = Z3.Fixedpoint.get_rules !fp in
219
       Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
220
            	  (Utils.fprintf_list ~sep:"@ "
221
            	     (fun fmt e ->
222
              (* let e2 = Z3.Quantifier.get_body eq in *)
223
              (* let fd = Z3.Expr.get_func_decl e in *)
224
              Format.fprintf fmt "Rule: %s@."
225
       	 (Z3.Expr.to_string e);
226
            )) rules_expr;
227

  
228
       let _ = List.map extract_expr_fds rules_expr in
229
       Format.eprintf "%t" pp_fdecls;
230

  
231
       if !Options.main_node <> "" then
232
            	  begin
233
            	    Zustre_analyze.check machines !Options.main_node
234

  
235
            	  end
236
       else
237
            	  failwith "Require main node";
238

  
239
       ()
240
            )
241
            else
242
    *)
243
    decl_sorts ();
244

  
245
    List.iter (decl_machine machines) (List.rev machines);
246

  
247
    (* (\* Debug instructions *\) *)
248
    (* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
249
    (* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
250
    (* 	(Utils.fprintf_list ~sep:"@ " *)
251
    (* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
252
    (* 	rules_expr; *)
253
    if !Options.main_node <> "" then
254
      Zustre_analyze.check machines !Options.main_node
255
    else failwith "Require main node";
267 256

  
257
    ()
258
end
268 259

  
269 260
let () =
270
  VerifierList.registered := (module Verifier : VerifierType.S) ::
271
                             !VerifierList.registered
261
  VerifierList.registered :=
262
    (module Verifier : VerifierType.S) :: !VerifierList.registered
272 263

  
273 264
(* Local Variables: *)
274 265
(* compile-command:"make -C ../.. lustrev" *)

Also available in: Unified diff