Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_verifier.ml @ 5778dd5e

History | View | Annotate | Download (6.38 KB)

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
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
59
      ]
60
                
61
    let activate () = (
62
        active := true;
63
        Options.output := "horn";
64
      )
65
    let is_active () = !active
66

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

    
72
    let setup_solver () =
73
      fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
74
      (* let help = Z3.Fixedpoint.get_help fp in
75
       * Format.eprintf "Fp help : %s@." help;
76
       * 
77
       * let solver =Z3.Solver.mk_solver !ctx None in
78
       * let help = Z3.Solver.get_help solver in
79
       * Format.eprintf "Z3 help : %s@." help; *)
80
      
81
      let module P = Z3.Params in
82
      let module S = Z3.Symbol in
83
      let mks = S.mk_string !ctx in
84
      let params = P.mk_params !ctx in
85

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

    
95
      (* Dont know where to find this parameter *)
96
      (* if !param_spacer_verbose then
97
         *   if self.args.spacer_verbose: 
98
         *        z3.set_option (verbose=1) *)
99

    
100
      (* The option is not recogined*)
101
      (* self.fp.set('use_heavy_mev',True) *)
102
      (* P.add_bool params (mks "use_heavy_mev") true; *)
103
      
104
      (* self.fp.set('pdr.flexible_trace',True) *)
105
      P.add_bool params (mks "pdr.flexible_trace") true;
106

    
107
      (* self.fp.set('reset_obligation_queue',False) *)
108
      P.add_bool params (mks "spacer.reset_obligation_queue") false;
109

    
110
      (* self.fp.set('spacer.elim_aux',False) *)
111
      P.add_bool params (mks "spacer.elim_aux") false;
112

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

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

    
128
      (* if not self.args.pp:
129
       *        self.log.info("No pre-processing")
130
       *        self.fp.set ('xform.slice', False)
131
       *        self.fp.set ('xform.inline_linear',False)
132
       *        self.fp.set ('xform.inline_eager',False) *\) *)
133
      if !param_pp then (
134
        P.add_bool params (mks "xform.slice") false;
135
        P.add_bool params (mks "xform.inline_linear") false;
136
        P.add_bool params (mks "xform.inline_eager") false
137
      );
138
      Z3.Fixedpoint.set_parameters !fp params
139
              
140
      
141
    let run basename prog machines =
142
      let machines = Machine_code_common.arrow_machine::machines in
143
      let machines = preprocess machines in
144
      setup_solver ();
145

    
146

    
147
      (* TODO
148
	 load deps: cf print_dep in horn_backend.ml
149

    
150
      *)
151
      if false then (
152
	
153
	let queries = Z3.Fixedpoint.parse_file !fp "mini.smt2" in
154

    
155
      (* Debug instructions *)
156
      let rules_expr = Z3.Fixedpoint.get_rules !fp in
157
      Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
158
      	(Utils.fprintf_list ~sep:"@ "
159
      	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
160
      	rules_expr;
161

    
162
	let res_status = Z3.Fixedpoint.query !fp (List.hd queries )in
163
	
164
	Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)
165
      )
166
      else (
167
	
168
	
169
      decl_sorts ();
170
      
171
      List.iter (decl_machine machines) (List.rev machines);
172

    
173

    
174
      (* (\* Debug instructions *\) *)
175
      (* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
176
      (* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
177
      (* 	(Utils.fprintf_list ~sep:"@ " *)
178
      (* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
179
      (* 	rules_expr; *)
180

    
181
      if !Options.main_node <> "" then
182
      	begin
183
      	  Zustre_analyze.check machines !Options.main_node
184

    
185
      	end
186
      else
187
      	failwith "Require main node";
188
      
189
      ()
190
      )
191
	
192

    
193
  end: VerifierType.S)
194
    
195
(* Local Variables: *)
196
(* compile-command:"make -C ../.." *)
197
(* End: *)