Project

General

Profile

Download (8.38 KB) Statistics
| Branch: | Tag: | Revision:
1 5778dd5e ploc
2
(*
3
TODO
4
5
A property/contract is attached to a node foo and could be analyzed
6
- while considering the exact semantics
7
- while substituting some callee by their definition (doing it incrementaly ?)
8
- the returned cex could be given at node level
9
- or while considering a main node and producing the output at the main node level
10
11
One can consider the following algorithm:
12
- main node foo, local node bar, with a target property/contract
13
- declare bar using only the contract of its subnodes (callee)
14
- if the property is valid, 
15
  - check the validity status of the subnode contracts used
16
    - if one is not proved, perform the analysis again (of bar contract) using
17
      the actual definition of the unproven contract
18
  - return the computed invariants with the dependencies (subcontracts assumed, subcontracts proved)
19
- if the property is invalid
20
  - check invalidity wrt to full definition of the node bar (with the actual definition of its subnodes)
21
  - return the cex
22
  - try to see if the cex (or a similar violation of the contract) is reachable from its parents 
23
    (up to main node foo)
24
    
25
26
Other features:
27
- check equivalence btw two nodes, provided an equivalence map on some callee
28
  (A equiv B) with map (A id equiv B id) 
29
  - substitute each callee appearing B nodes 
30
31
Analysis:
32
  - take a main definition, a boolean proposition, and build the collecting semantics
33
  - then check that the proposition remains valid
34
35
*)
36
37 9c4cc944 Corentin Lauverjat
open Lustrec
38 5778dd5e ploc
open Zustre_common
39
open Zustre_data
40
41
let param_stat = ref false
42
let param_eldarica = ref false
43
let param_utvpi = ref false
44
let param_tosmt = ref false
45
let param_pp = ref false
46
47
let active = ref false
48
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 4300981b ploc
        "-timeout", Arg.Set_int timeout, "Set timeout in ms (default 10000 = 10 s)";
59 5778dd5e ploc
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
60 4300981b ploc
        "-debug", Arg.Set debug, "Debug mode";
61 5778dd5e ploc
      ]
62
                
63
    let activate () = (
64
        active := true;
65 9c4cc944 Corentin Lauverjat
        Lustrec.Options.output := "horn";
66 5778dd5e ploc
      )
67 57d61d67 ploc
68 5778dd5e ploc
    let is_active () = !active
69
70
    let get_normalization_params () =
71
      (* make sure the output is "Horn" *)
72 9c4cc944 Corentin Lauverjat
      assert(!Lustrec.Options.output = "horn");
73 5778dd5e ploc
      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 4300981b ploc
84 5778dd5e ploc
      let module P = Z3.Params in
85
      let module S = Z3.Symbol in
86
      let mks = S.mk_string !ctx in
87 4300981b ploc
      
88
      (* Fixpoint Engine parameters *)
89
      
90
      let fp_params = P.mk_params !ctx in
91 5778dd5e ploc
92 51ec4e8c ploc
      (* (\* self.fp.set (engine='spacer') *\) *)
93 4300981b ploc
      P.add_symbol fp_params (mks "engine") (mks "spacer");
94
      (* P.add_symbol fp_params (mks "engine") (mks "pdr");  *)
95 5778dd5e ploc
      
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 4300981b ploc
        P.add_bool fp_params (mks "print_statistics") true;
101 5778dd5e ploc
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 4300981b ploc
      (* P.add_bool fp_params (mks "use_heavy_mev") true; *)
110 5778dd5e ploc
      
111
      (* self.fp.set('pdr.flexible_trace',True) *)
112 4300981b ploc
      P.add_bool fp_params (mks "pdr.flexible_trace") true;
113 5778dd5e ploc
114
      (* self.fp.set('reset_obligation_queue',False) *)
115 4300981b ploc
      P.add_bool fp_params (mks "spacer.reset_obligation_queue") false;
116 5778dd5e ploc
117
      (* self.fp.set('spacer.elim_aux',False) *)
118 4300981b ploc
      P.add_bool fp_params (mks "spacer.elim_aux") false;
119 5778dd5e ploc
120
      (* if self.args.eldarica:
121
        *     self.fp.set('print_fixedpoint_extensions', False) *)
122
      if !param_eldarica then
123 4300981b ploc
        P.add_bool fp_params (mks "print_fixedpoint_extensions") false;
124 5778dd5e ploc
      
125
      (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
126
      if !param_utvpi then
127 4300981b ploc
        P.add_bool fp_params (mks "pdr.utvpi") false;
128 5778dd5e ploc
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 4300981b ploc
        P.add_bool fp_params (mks "print.low_level_smt2") true;
134 5778dd5e ploc
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 57d61d67 ploc
      if not !param_pp then (
141
	(* Mandatory to print all steps and recover cex *)
142 4300981b ploc
        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 5778dd5e ploc
      );
146 4300981b ploc
147
148
      (* Ploc's options. Do not seem to have any effect yet *)
149
      P.add_bool fp_params (mks "print_answer") true;
150 57d61d67 ploc
      (* 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 4300981b ploc
156
      (* Adding a timeout *)
157
      P.add_int fp_params (mks "timeout") !timeout;
158
159
      Z3.Fixedpoint.set_parameters !fp fp_params
160 5778dd5e ploc
      
161 7a4fd94d ploc
    let run ~basename prog machines =
162 9c4cc944 Corentin Lauverjat
      let machines = Lustrec.Machine_code_common.arrow_machine::machines in
163 5778dd5e ploc
      let machines = preprocess machines in
164
      setup_solver ();
165
166
167
      (* TODO
168
	 load deps: cf print_dep in horn_backend.ml
169
170 ea758c12 ploc
      
171 5778dd5e ploc
      if false then (
172
	
173 57d61d67 ploc
	let queries = Z3.Fixedpoint.parse_file !fp "nstep.smt2" in
174 5778dd5e ploc
175 51ec4e8c ploc
	(* Debug instructions *)
176
	
177 5778dd5e ploc
178 51ec4e8c ploc
	
179
	let rules_expr = Z3.Fixedpoint.get_rules !fp in
180
	Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
181 9c4cc944 Corentin Lauverjat
      	  (Lustrec.Utils.fprintf_list ~sep:"@ "
182 51ec4e8c ploc
      	     (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 57d61d67 ploc
192
	let decl_err = List.hd queries in
193
      	let res_status = Z3.Fixedpoint.query !fp decl_err in
194 51ec4e8c ploc
	
195 57d61d67 ploc
	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 5778dd5e ploc
      )
203 51ec4e8c ploc
      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 9c4cc944 Corentin Lauverjat
      	  (Lustrec.Utils.fprintf_list ~sep:"@ "
215 51ec4e8c ploc
      	     (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 9c4cc944 Corentin Lauverjat
	if !Lustrec.Options.main_node <> "" then
226 51ec4e8c ploc
      	  begin
227 9c4cc944 Corentin Lauverjat
      	    Zustre_analyze.check machines !Lustrec.Options.main_node
228 51ec4e8c ploc
229
      	  end
230
	else
231
      	  failwith "Require main node";
232
233
	()	
234
      )
235 ea758c12 ploc
      else 
236
237
       *)
238
239
      (
240 5778dd5e ploc
	
241
	
242 51ec4e8c ploc
	decl_sorts ();
243
	
244
	List.iter (decl_machine machines) (List.rev machines);
245 5778dd5e ploc
246
247 51ec4e8c ploc
	(* (\* Debug instructions *\) *)
248
	(* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
249
	(* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
250 9c4cc944 Corentin Lauverjat
	(* 	(Lustrec.Utils.fprintf_list ~sep:"@ " *)
251 51ec4e8c ploc
	(* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
252
	(* 	rules_expr; *)
253 5778dd5e ploc
254 9c4cc944 Corentin Lauverjat
	if !Lustrec.Options.main_node <> "" then
255 51ec4e8c ploc
      	  begin
256 9c4cc944 Corentin Lauverjat
      	    Zustre_analyze.check machines !Lustrec.Options.main_node
257 5778dd5e ploc
258 51ec4e8c ploc
      	  end
259
	else
260
      	  failwith "Require main node";
261
	
262
	()
263 5778dd5e ploc
      )
264
	
265
266 51ec4e8c ploc
	    end: VerifierType.S)
267 5778dd5e ploc
    
268
(* Local Variables: *)
269 57d61d67 ploc
(* compile-command:"make -C ../.. lustrev" *)
270 5778dd5e ploc
(* End: *)