Project

General

Profile

Revision 57d61d67

View differences:

configure.ac
77 77
   AC_SUBST(LUSTREV_SEAL_TAG, "<**/*>: package(seal)")
78 78
])
79 79

  
80
# z3
81
AC_MSG_CHECKING(z3 library (optional))
82
define([z3path], esyscmd([ocamlfind query Z3 | tr -d '\n']))
80
# z3 (optional)
81

  
82
# option to rely on github version if installed
83
AC_ARG_WITH(z3_github, [AS_HELP_STRING([--with-z3-github],
84
              [Rely on Z3 as distributed by the official github
85
	       repo rather then the opam distribution. Disabled by default.])])
86

  
87
AS_IF([test "x$with_z3_github" != "xyes"],
88
      [z3name=z3],
89
      [z3name=Z3]
90
      )
91
	
92
AC_MSG_CHECKING(z3 library)
93

  
94

  
95
#define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
83 96
#define([z3path], esyscmd([opam config var Z3:lib | tr -d '\n']))
84 97

  
85
AS_IF([ocamlfind query Z3 >/dev/null 2>&1],
86
    [z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
98
AS_IF([ocamlfind query $z3name >/dev/null 2>&1],
99
    [z3=yes; AC_MSG_RESULT([yes])],[seal=no; AC_MSG_RESULT(no)],
87 100
)
88 101
AS_IF([test "x$z3" = "xyes"], [
89 102
   AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")
90
   AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package(Z3)")
91
   AC_SUBST(Z3LIBPATH, "z3path")
103
   AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package($z3name)")
104
   AS_IF([test "x$z3name" = "xZ3"],
105
   	       [define([Z3path], esyscmd([ocamlfind query Z3 | tr -d '\n']))
106
	        AC_SUBST(Z3LIBPATH, "Z3path")],
107
 	       [define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
108
	        AC_SUBST(Z3LIBPATH, "z3path")]
109
		)
92 110
])
93 111

  
94 112

  
......
244 262
  if (test "x$z3" = xyes); then
245 263
      AC_MSG_NOTICE([Zustre enabled])
246 264
      AC_MSG_WARN(Z3 shared lib (libz3.so) has to be available in the LD_LIBRARY_PATH.)
247
      AC_MSG_WARN(It is currently located in "z3path")
265
      dnl AC_MSG_WARN(It is currently located in "z3path")
248 266
      AC_MSG_WARN(If not already available run "source ${prefix}/include/lustrec/z3librc")
249 267
      AC_MSG_WARN(or add that line to your ~/.profile or ~/.bashrc)
250 268
else
src/_tags.in
28 28
<**/*.native>                   : package(ocamlgraph)
29 29
<**/*.native>                   : use_str
30 30
<**/*.native>                   : use_unix
31
<utils.*>                       : use_unix
31 32
<**/*.native>                   : package(num)
32 33
<**/*.ml>                       : package(logs)
33 34
<**/*.native>                   : package(logs)
35
<**/*.native>                   : package(yojson)
36
<tools/zustre/zustre_cex.*>                   : package(yojson)
34 37
<**/json_parser.ml>             : package(yojson)
35 38
<**/main_parse_json_file.*>     : package(cmdliner)
36 39
<**/main_parse_json_file.*>     : package(fmt.tty)
src/tools/zustre/zustre_analyze.ml
41 41
  (* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ?
42 42
     Faut-il declarer les "rel" dans la hashtbl ?
43 43
  *)
44
  
44 45
  let decl_main =
45 46
    decl_rel
46 47
      ("MAIN" ^ "_" ^ node_id)
......
210 211
    
211 212
    Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
212 213
    match res_status with
213
    | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex decl_err
214
    | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err
214 215
       
215 216
    | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
216 217
      let expr_opt = Z3.Fixedpoint.get_answer !fp in
......
221 222
    | Z3.Solver.UNKNOWN -> ()
222 223
  with Z3.Error msg -> Format.eprintf "Z3 failure: %s@." msg; () 
223 224
(* Local Variables: *)
224
(* compile-command:"make -C ../.." *)
225
(* compile-command:"make -C ../.. lustrev" *)
225 226
(* End: *)
src/tools/zustre/zustre_cex.ml
1
(* Rebuilding Cex *)
2
(* In order to properly rebuild the Cex, one needsthe unsliced model. Otherwise
3
   some input or state variables are removed.
4

  
5
*)
6

  
7

  
8
open Lustre_types
9
open Machine_code_types
10
(* open Machine_code_common *)
11
open Zustre_common
12

  
1 13
open Zustre_data
2 14

  
3 15
let get_conjuncts e =
......
7 19
  else
8 20
    [e]
9 21

  
10
let build_cex decl_err =
22
let build_cex machine machines decl_err =
23
  (* Recovering associated top machine (to build full traces) and property *) 
24
  (* TODO: for example extract top node and ok prop. We may have multiple
25
     MAIN/ERR loaded at the same time. Each of them should be assocaited with a
26
     CEX/Inv/Timeout.*)
27
  
28
  let node_id = machine.mname.node_id in
11 29

  
12 30
  let cex = match Z3.Fixedpoint.get_answer !fp with Some e -> e | None -> raise Not_found in
13
       (* Original code used the function Z3.Fixedpoint.get_ground_sat_answer !fp *)
31
  (* Original code used the function Z3.Fixedpoint.get_ground_sat_answer !fp *)
32

  
33
  let stats = Z3.Fixedpoint.get_statistics !fp in
34
  
14 35
  let conjuncts = List.rev (get_conjuncts cex) in
15
  (* Predicates are renamed according to the naming scheme of LustreC*)
16
  (*      pred_dict = {}
17
        cex_dict = {} #store the cex in order
18
        for p in self.preds:
19
            lus_pred = z3.substitute(p, *self.coco.z3MapVar)
20
            lus_arg = [str(x) for x in lus_pred.children()]
21
            pred_dict.update({str(lus_pred.decl()):lus_arg})
22
  *)
23
  (* Building a cex_dict, a map of maps ! node name -> (k -> value)  *)
24
  let _ = List.mapi (fun k conj ->
25
    (* k-iterate *)
26
    let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in
36

  
37
  Format.eprintf "cex: %s@.%i conjuncts: @[<v 0>%a@]@."
38
    (Z3.Expr.to_string cex)
39
    (List.length conjuncts)
40
    (Utils.fprintf_list ~sep:"@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) conjuncts;
41

  
42
  (* Checking size *)
43
  let inputs = machine.mstep.step_inputs in
44
  let nb_inputs = List.length inputs in
45
  let outputs = machine.mstep.step_outputs in
46
  let nb_outputs = List.length inputs in
47
  let nb_mems = List.length (full_memory_vars machines machine) in
48
  
49
  let main =
50
    List.fold_left (fun accu conj ->
51
    (* Filtering out non MAIN decls *)
27 52
    let func_decl = Z3.Expr.get_func_decl conj in
28
    if !debug then Format.eprintf "FuncDecl %s@." (Z3.FuncDecl.to_string func_decl);
29 53
    let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in
54
    (* Focusing only on MAIN_nodeid predicates *)
55
    if node_name = "MAIN_" ^ node_id then
56
      (* Extracting info *)
57
      (* Recall that MAIN args are 
58
	 main_input @ 
59
	 (full_memory_vars machines machine) @
60
	 main_output   *)
61
      let args = Z3.Expr.get_args conj in
62
      if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then
63
	let id = Z3.Arithmetic.Integer.get_int (List.hd args) in
64
	let input_values = Utils.List.extract args 1 (1 + nb_inputs) in
65
	let output_values = Utils.List.extract args (1+nb_inputs+nb_mems) (1 + nb_inputs + nb_mems + nb_outputs) in
66
	(id, (input_values, output_values))::accu
67
      else
68
	assert false
69
    else
70
      accu 
71
  ) [] conjuncts
72
  in
73
  let main = List.sort (fun (id1, _) (id2, _) -> compare id1 id2) main in
74
  List.iter (
75
    fun (id, expr) ->
76
      Format.eprintf "Id %i: %a@."
77
	(id)
78
	(Utils.fprintf_list ~sep:", "
79
	   (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
80
	(fst expr)
81
  ) main;		    
82
   (* let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *)
83

  
84
   (* We recover the Zustre XML format, projecting each cex on each input/output
85
      signal *)
86
  let in_signals, out_signals =
87
    List.fold_right (
88
      fun (id, (sigs_in, sigs_out)) (res_sigs_in, res_sigs_out) ->
89
	let add l1 l2 = List.map2 (fun e1 e2 -> fst e2, ((id, e1)::(snd e2))) l1 l2 in
90
	let sigs_in_id = add sigs_in res_sigs_in in
91
	let sigs_out_id = add sigs_out res_sigs_out in
92
	sigs_in_id, sigs_out_id
93
    ) main (List.map (fun v -> v, []) inputs, List.map (fun v -> v, []) outputs)
94
  in
95

  
96
  (* let _ = List.mapi (fun k conj -> *)
97
  (*   (\* k-iterate *\) *)
98
  (*   let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *)
99
  (*   let func_decl = Z3.Expr.get_func_decl conj in *)
100
  (*   if !debug then Format.eprintf "FuncDecl %s@." (Z3.FuncDecl.to_string func_decl); *)
101
  (*   let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in *)
102

  
103
   
104
  (*   if !debug then Format.eprintf "Node %s, args %a@." node_name  (Utils.fprintf_list ~sep:", " (Format.pp_print_string)) ground_val; *)
30 105
    
31
    if !debug then Format.eprintf "Node %s, args %a@." node_name  (Utils.fprintf_list ~sep:", " (Format.pp_print_string)) ground_val;
32
    
33
    ()
34
    (*  ground_pair = []
35
            try:
36
                ground_vars = pred_dict[node_name]
37
                ground_pair = zip(ground_vars,ground_val)
38
                if "_reset" in node_name:
39
                    # this condition is to remove the node nodename_reset added by lustrec
40
                    continue
41
                    # node = node_name.split("_reset")[0]
42
                    # cex_dict.update({node:{k:ground_pair}})
43
                elif "_step" in node_name:
44
                    node = node_name.split("_step")[0]
45
                    try:
46
                        # case in which we already have the node in dict
47
                        d = cex_dict[node]
48
                        max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1
49
                        d.update({(max_key+1):ground_pair})
50
                    except Exception as e:
51
                        self._log.warning("Adding a new node cex " + str(e))
52
                        cex_dict.update({node:{k:ground_pair}})
53
                else:
54
                    node = node_name
55
                    try:
56
                        d = cex_dict[node]
57
                        max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1
58
                        d.update({(max_key+1):ground_pair})
59
                    except Exception as e:
60
                        if node not in ["MAIN", "ERR"]:
61
                            self._log.warning("Adding a new node cex " + str(e))
62
                            cex_dict.update({node:{k:ground_pair}})
63
            except Exception as e:
64
                self._log.warning("Problem with getting a node name: " + str(e))
65
    *)
66
  ) conjuncts in
67
    let rules_expr = Z3.Fixedpoint.get_rules !fp in
68
    if !debug then
69
      Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
70
	(Utils.fprintf_list ~sep:"@ "
71
    	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
72
	rules_expr;
73
    if !debug then
74
      Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp);
106
  (*   () *)
107
  (*   (\*  ground_pair = [] *)
108
  (*           try: *)
109
  (*               ground_vars = pred_dict[node_name] *)
110
  (*               ground_pair = zip(ground_vars,ground_val) *)
111
  (*               if "_reset" in node_name: *)
112
  (*                   # this condition is to remove the node nodename_reset added by lustrec *)
113
  (*                   continue *)
114
  (*                   # node = node_name.split("_reset")[0] *)
115
  (*                   # cex_dict.update({node:{k:ground_pair}}) *)
116
  (*               elif "_step" in node_name: *)
117
  (*                   node = node_name.split("_step")[0] *)
118
  (*                   try: *)
119
  (*                       # case in which we already have the node in dict *)
120
  (*                       d = cex_dict[node] *)
121
  (*                       max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *)
122
  (*                       d.update({(max_key+1):ground_pair}) *)
123
  (*                   except Exception as e: *)
124
  (*                       self._log.warning("Adding a new node cex " + str(e)) *)
125
  (*                       cex_dict.update({node:{k:ground_pair}}) *)
126
  (*               else: *)
127
  (*                   node = node_name *)
128
  (*                   try: *)
129
  (*                       d = cex_dict[node] *)
130
  (*                       max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *)
131
  (*                       d.update({(max_key+1):ground_pair}) *)
132
  (*                   except Exception as e: *)
133
  (*                       if node not in ["MAIN", "ERR"]: *)
134
  (*                           self._log.warning("Adding a new node cex " + str(e)) *)
135
  (*                           cex_dict.update({node:{k:ground_pair}}) *)
136
  (*           except Exception as e: *)
137
  (*               self._log.warning("Problem with getting a node name: " + str(e)) *)
138
  (*   *\) *)
139
  (* ) conjuncts in *)
140
  (*   let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
141
  (*   if !debug then *)
142
  (*     Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
143
  (* 	(Utils.fprintf_list ~sep:"@ " *)
144
  (*   	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
145
  (* 	rules_expr; *)
146
  (*   if !debug then *)
147
  (*     Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp); *)
75 148

  
149
  let stats_entries =   Z3.Statistics.get_entries stats in
150
  List.iter (fun e -> Format.eprintf "%s@.@?"
151
    (Z3.Statistics.Entry.to_string e)
152
    
153
  ) stats_entries;
154
  let json : Yojson.json =
155
    `Assoc [
156
      "Results",
157
      `Assoc [
158
	"Property",
159
	`Assoc [
160
	  "name", `String node_id;
161
	  "date", `String (Utils.get_date ());
162
	  "query", `Assoc ["unit", `String "sec";
163
			   "value", `Float (
164
			     let time_opt = Z3.Statistics.get stats "time.spacer.solve" in
165
			     match time_opt with None -> -1.
166
			     | Some f -> Z3.Statistics.Entry.get_float f)
167
			  ];
168
	  "answer", `String "CEX";
169
	  "counterexample",
170
	  `Assoc [
171
	    node_id, `Assoc
172
	      (
173
		List.map (fun (vardecl, values) ->
174
		  vardecl.var_id,
175
		  `Assoc [
176
		    "type", (let _ = Format.fprintf Format.str_formatter "%a" Printers.pp_var_type vardecl in
177
			    let s = Format.flush_str_formatter () in
178
			    `String s);
179
		    "values", `Assoc (List.map (fun (id, v) ->
180
		      string_of_int id, `String (Z3.Expr.to_string v))
181
					values)
182
		  ]   
183
		) in_signals
184
	      )
185
	  ]
186
	]
187
      ]
188
     ]
189
  in
190
  Format.eprintf "JSON: %s@."
191
    (Yojson.to_string json);
76 192
  ()
193
  (* Results *)
194
  (*   Property *)
195
  (*   Date *)
196
  (*   Query time *)
197
  (*   Answer CEX *)
198
  (*   Counterexample *)
199
  (*     Node name="nodeid" *)
200
  (*       Stream name="opt.x" type="unk" *)
201
  (* 	  Value instant="0">xxx</Value>		       *)
202
  (* () *)
77 203
	(* ordered_by_signal = self.reorder(cex_dict) *)
78 204
        (* return self.mk_cex_xml(ordered_by_signal) *)
79 205

  
206
(* Local Variables: *)
207
(* compile-command:"make -C ../.. lustrev" *)
208
(* End: *)
80 209

  
81 210
	
src/tools/zustre/zustre_verifier.ml
64 64
        active := true;
65 65
        Options.output := "horn";
66 66
      )
67

  
67 68
    let is_active () = !active
68 69

  
69 70
    let get_normalization_params () =
......
136 137
       *        self.fp.set ('xform.slice', False)
137 138
       *        self.fp.set ('xform.inline_linear',False)
138 139
       *        self.fp.set ('xform.inline_eager',False) *\) *)
139
      if !param_pp then (
140
      if not !param_pp then (
141
	(* Mandatory to print all steps and recover cex *)
140 142
        P.add_bool fp_params (mks "xform.slice") false;
141 143
        P.add_bool fp_params (mks "xform.inline_linear") false;
142 144
        P.add_bool fp_params (mks "xform.inline_eager") false
......
145 147

  
146 148
      (* Ploc's options. Do not seem to have any effect yet *)
147 149
      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
      (* 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;  *)
150 155

  
151 156
      (* Adding a timeout *)
152 157
      P.add_int fp_params (mks "timeout") !timeout;
......
165 170
      *)
166 171
      if false then (
167 172
	
168
	let queries = Z3.Fixedpoint.parse_file !fp "mini.smt2" in
173
	let queries = Z3.Fixedpoint.parse_file !fp "nstep.smt2" in
169 174

  
170 175
	(* Debug instructions *)
171 176
	
......
183 188
	
184 189
	let _ = List.map extract_expr_fds rules_expr in
185 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
186 194
	
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)
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
190 202
      )
191 203
      else if false then (
192 204

  
......
250 262
	    end: VerifierType.S)
251 263
    
252 264
(* Local Variables: *)
253
(* compile-command:"make -C ../.." *)
265
(* compile-command:"make -C ../.. lustrev" *)
254 266
(* End: *)
src/utils.ml
380 380
	| _ -> assert false
381 381
      in
382 382
      run 0 l1 l2
383

  
384
  let rec extract l fst last =
385
    if last < fst then assert false else
386
      match l, fst with
387
      | hd::tl, 0 -> if last = 0 then [] else hd::(extract tl 0 (last-1))
388
      | _::tl, _ -> extract tl (fst-1) (last-1)
389
      | [], 0 -> if last=0 then [] else assert false (* List too short *)
390
      | _ -> assert false 
391
		 
383 392
end
384 393

  
385
  
394
let get_date () =
395
  let tm = Unix.localtime (Unix.time ()) in
396
  let fmt = Format.str_formatter in
397
  let open Unix in
398
  let _ =
399
    Format.fprintf fmt
400
      "%i/%i/%i %ih%i:%i"
401
      tm.tm_year
402
      tm.tm_mon
403
      tm.tm_mday
404
      tm.tm_hour
405
      tm.tm_min
406
      tm.tm_sec
407
  in
408
  Format.flush_str_formatter ()
409

  
386 410
(* Local Variables: *)
387 411
(* compile-command:"make -C .." *)
388 412
(* End: *)

Also available in: Unified diff