Project

General

Profile

Download (7.85 KB) Statistics
| Branch: | Tag: | Revision:
1

    
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

    
38
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
        "-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
    let is_active () = !active
68

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

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

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

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

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

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

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

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

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

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

    
134
      (* if not self.args.pp:
135
       *        self.log.info("No pre-processing")
136
       *        self.fp.set ('xform.slice', False)
137
       *        self.fp.set ('xform.inline_linear',False)
138
       *        self.fp.set ('xform.inline_eager',False) *\) *)
139
      if !param_pp then (
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
143
      );
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
155
      
156
    let run basename prog machines =
157
      let machines = Machine_code_common.arrow_machine::machines in
158
      let machines = preprocess machines in
159
      setup_solver ();
160

    
161

    
162
      (* TODO
163
	 load deps: cf print_dep in horn_backend.ml
164

    
165
      *)
166
      if false then (
167
	
168
	let queries = Z3.Fixedpoint.parse_file !fp "mini.smt2" in
169

    
170
	(* Debug instructions *)
171
	
172

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

    
193
	(* No queries here *)
194
	let _ = Z3.Fixedpoint.parse_file !fp "mini_decl.smt2" in
195

    
196
	(* Debug instructions *)
197
	
198

    
199
	
200
	let rules_expr = Z3.Fixedpoint.get_rules !fp in
201
	Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
202
      	  (Utils.fprintf_list ~sep:"@ "
203
      	     (fun fmt e ->
204
	       (* let e2 = Z3.Quantifier.get_body eq in *)
205
	       (* let fd = Z3.Expr.get_func_decl e in *)
206
	       Format.fprintf fmt "Rule: %s@."
207
		 (Z3.Expr.to_string e);
208
	     )) rules_expr;
209
	
210
	let _ = List.map extract_expr_fds rules_expr in
211
	Format.eprintf "%t" pp_fdecls;
212

    
213
	if !Options.main_node <> "" then
214
      	  begin
215
      	    Zustre_analyze.check machines !Options.main_node
216

    
217
      	  end
218
	else
219
      	  failwith "Require main node";
220

    
221
	()	
222
      )
223
      else (
224
	
225
	
226
	decl_sorts ();
227
	
228
	List.iter (decl_machine machines) (List.rev machines);
229

    
230

    
231
	(* (\* Debug instructions *\) *)
232
	(* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
233
	(* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
234
	(* 	(Utils.fprintf_list ~sep:"@ " *)
235
	(* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
236
	(* 	rules_expr; *)
237

    
238
	if !Options.main_node <> "" then
239
      	  begin
240
      	    Zustre_analyze.check machines !Options.main_node
241

    
242
      	  end
243
	else
244
      	  failwith "Require main node";
245
	
246
	()
247
      )
248
	
249

    
250
	    end: VerifierType.S)
251
    
252
(* Local Variables: *)
253
(* compile-command:"make -C ../.." *)
254
(* End: *)
(5-5/5)