Project

General

Profile

Download (9.75 KB) Statistics
| Branch: | Tag: | Revision:
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
open Lustre_types
6
open Machine_code_types
7

    
8
(* open Machine_code_common *)
9
open Zustre_common
10
open Zustre_data
11

    
12
let get_conjuncts e =
13
  assert (Z3.Boolean.is_bool e);
14
  if Z3.Boolean.is_and e then Z3.Expr.get_args e else [ e ]
15

    
16
let build_cex machine machines _decl_err =
17
  (* Recovering associated top machine (to build full traces) and property *)
18
  (* TODO: for example extract top node and ok prop. We may have multiple
19
     MAIN/ERR loaded at the same time. Each of them should be assocaited with a
20
     CEX/Inv/Timeout.*)
21
  let node_id = machine.mname.node_id in
22

    
23
  let cex =
24
    match Z3.Fixedpoint.get_answer !fp with
25
    | Some e ->
26
      e
27
    | None ->
28
      raise Not_found
29
  in
30

    
31
  (* Original code used the function Z3.Fixedpoint.get_ground_sat_answer !fp *)
32
  let stats = Z3.Fixedpoint.get_statistics !fp in
33

    
34
  let conjuncts = List.rev (get_conjuncts cex) in
35

    
36
  Format.eprintf "cex: %s@.%i conjuncts: @[<v 0>%a@]@." (Z3.Expr.to_string cex)
37
    (List.length conjuncts)
38
    (Utils.fprintf_list ~sep:"@ " (fun fmt e ->
39
         Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
40
    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
51
      (fun (main, funs) conj ->
52
        (* Filtering out non MAIN decls *)
53
        let func_decl = Z3.Expr.get_func_decl conj in
54
        let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in
55
        (* Focusing only on MAIN_nodeid predicates *)
56
        if node_name = "MAIN_" ^ node_id then
57
          (* Extracting info *)
58
          (* Recall that MAIN args are in@mems@out *)
59
          let args = Z3.Expr.get_args conj in
60
          if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then
61
            (* Should be done with get_int but that function vanished from the
62
               opam Z3 API *)
63
            let id =
64
              Z.to_int (Z3.Arithmetic.Integer.get_big_int (List.hd args))
65
            in
66
            let input_values = Utils.List.extract args 1 (1 + nb_inputs) in
67
            let output_values =
68
              Utils.List.extract args
69
                (1 + nb_inputs + nb_mems)
70
                (1 + nb_inputs + nb_mems + nb_outputs)
71
            in
72
            (id, (input_values, output_values)) :: main, funs
73
          else assert false
74
        else
75
          let reg = Str.regexp_string "[a-z]*_step" in
76
          if Str.string_match reg node_name 0 then (
77
            let actual_name = Str.matched_group 0 node_name in
78
            Format.eprintf "Name %s@." actual_name;
79
            main, funs)
80
          else (
81
            Format.eprintf "pas matché %s@." node_name;
82
            main, funs))
83
      ((* main*)
84
       [], (* other functions *)
85
           [])
86
      conjuncts
87
  in
88
  let main = List.sort (fun (id1, _) (id2, _) -> compare id1 id2) main in
89
  List.iter
90
    (fun (id, expr) ->
91
      Format.eprintf "Id %i: %a@." id
92
        (Utils.fprintf_list ~sep:", " (fun fmt e ->
93
             Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
94
        (fst expr))
95
    main;
96

    
97
  (* let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args
98
     conj) in *)
99

    
100
  (* We recover the Zustre XML format, projecting each cex on each input/output
101
     signal *)
102
  let in_signals, _ =
103
    List.fold_right
104
      (fun (id, (sigs_in, sigs_out)) (res_sigs_in, res_sigs_out) ->
105
        let add l1 l2 =
106
          List.map2 (fun e1 e2 -> fst e2, (id, e1) :: snd e2) l1 l2
107
        in
108
        let sigs_in_id = add sigs_in res_sigs_in in
109
        let sigs_out_id = add sigs_out res_sigs_out in
110
        sigs_in_id, sigs_out_id)
111
      main
112
      (List.map (fun v -> v, []) inputs, List.map (fun v -> v, []) outputs)
113
  in
114

    
115
  (* let _ = List.mapi (fun k conj -> *)
116
  (*   (\* k-iterate *\) *)
117
  (* let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args
118
     conj) in *)
119
  (* let func_decl = Z3.Expr.get_func_decl conj in *)
120
  (* if !debug then Format.eprintf "FuncDecl %s@." (Z3.FuncDecl.to_string
121
     func_decl); *)
122
  (* let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in *)
123

    
124
  (* if !debug then Format.eprintf "Node %s, args %a@." node_name
125
     (Utils.fprintf_list ~sep:", " (Format.pp_print_string)) ground_val; *)
126

    
127
  (*   () *)
128
  (*   (\*  ground_pair = [] *)
129
  (*           try: *)
130
  (*               ground_vars = pred_dict[node_name] *)
131
  (*               ground_pair = zip(ground_vars,ground_val) *)
132
  (*               if "_reset" in node_name: *)
133
  (* # this condition is to remove the node nodename_reset added by lustrec *)
134
  (*                   continue *)
135
  (*                   # node = node_name.split("_reset")[0] *)
136
  (*                   # cex_dict.update({node:{k:ground_pair}}) *)
137
  (*               elif "_step" in node_name: *)
138
  (*                   node = node_name.split("_step")[0] *)
139
  (*                   try: *)
140
  (*                       # case in which we already have the node in dict *)
141
  (*                       d = cex_dict[node] *)
142
  (* max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key
143
     value and add 1 *)
144
  (*                       d.update({(max_key+1):ground_pair}) *)
145
  (*                   except Exception as e: *)
146
  (*                       self._log.warning("Adding a new node cex " + str(e)) *)
147
  (*                       cex_dict.update({node:{k:ground_pair}}) *)
148
  (*               else: *)
149
  (*                   node = node_name *)
150
  (*                   try: *)
151
  (*                       d = cex_dict[node] *)
152
  (* max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key
153
     value and add 1 *)
154
  (*                       d.update({(max_key+1):ground_pair}) *)
155
  (*                   except Exception as e: *)
156
  (*                       if node not in ["MAIN", "ERR"]: *)
157
  (* self._log.warning("Adding a new node cex " + str(e)) *)
158
  (*                           cex_dict.update({node:{k:ground_pair}}) *)
159
  (*           except Exception as e: *)
160
  (* self._log.warning("Problem with getting a node name: " + str(e)) *)
161
  (*   *\) *)
162
  (* ) conjuncts in *)
163
  (*   let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
164
  (*   if !debug then *)
165
  (*     Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
166
  (* 	(Utils.fprintf_list ~sep:"@ " *)
167
  (*   	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
168
  (* 	rules_expr; *)
169
  (*   if !debug then *)
170
  (*     Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp); *)
171

    
172
  (*  let _ (*stats_entries*) =   Z3.Statistics.get_entries stats in *)
173
  (* List.iter (fun e -> Format.eprintf "%s@.@?" *)
174
  (*   (Z3.Statistics.Entry.to_string e) *)
175

    
176
  (* ) stats_entries; *)
177
  let json : Yojson.t =
178
    `Assoc
179
      [
180
        ( "Results",
181
          `Assoc
182
            [
183
              ( "Property",
184
                `Assoc
185
                  [
186
                    "name", `String node_id;
187
                    "date", `String (Utils.get_date ());
188
                    ( "query",
189
                      `Assoc
190
                        [
191
                          "unit", `String "sec";
192
                          ( "value",
193
                            `Float
194
                              (let time_opt =
195
                                 Z3.Statistics.get stats "time.spacer.solve"
196
                               in
197
                               match time_opt with
198
                               | None ->
199
                                 -1.
200
                               | Some f ->
201
                                 Z3.Statistics.Entry.get_float f) );
202
                        ] );
203
                    "answer", `String "CEX";
204
                    ( "counterexample",
205
                      `Assoc
206
                        [
207
                          ( node_id,
208
                            `Assoc
209
                              (List.map
210
                                 (fun (vardecl, values) ->
211
                                   ( vardecl.var_id,
212
                                     `Assoc
213
                                       [
214
                                         ( "type",
215
                                           let _ =
216
                                             Format.fprintf Format.str_formatter
217
                                               "%a" Printers.pp_var_type vardecl
218
                                           in
219
                                           let s =
220
                                             Format.flush_str_formatter ()
221
                                           in
222
                                           `String s );
223
                                         ( "values",
224
                                           `Assoc
225
                                             (List.map
226
                                                (fun (id, v) ->
227
                                                  ( string_of_int id,
228
                                                    `String
229
                                                      (Z3.Expr.to_string v) ))
230
                                                values) );
231
                                       ] ))
232
                                 in_signals) );
233
                        ] );
234
                  ] );
235
            ] );
236
      ]
237
  in
238
  Format.eprintf "JSON: %s@." (Yojson.to_string json);
239
  ()
240
(* Results *)
241
(*   Property *)
242
(*   Date *)
243
(*   Query time *)
244
(*   Answer CEX *)
245
(*   Counterexample *)
246
(*     Node name="nodeid" *)
247
(*       Stream name="opt.x" type="unk" *)
248
(* 	  Value instant="0">xxx</Value>		       *)
249
(* () *)
250
(* ordered_by_signal = self.reorder(cex_dict) *)
251
(* return self.mk_cex_xml(ordered_by_signal) *)
252

    
253
(* Local Variables: *)
254
(* compile-command:"make -C ../.. lustrev" *)
255
(* End: *)
(3-3/7)