Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by Lélio Brun 8 months ago

reformatting

View differences:

src/tools/zustre/zustre_cex.ml
1 1
(* Rebuilding Cex *)
2 2
(* In order to properly rebuild the Cex, one needsthe unsliced model. Otherwise
3
   some input or state variables are removed.
4

  
5
*)
6

  
3
   some input or state variables are removed. *)
7 4

  
8 5
open Lustre_types
9 6
open Machine_code_types
7

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

  
13 10
open Zustre_data
14 11

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

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

  
30
  let cex = match Z3.Fixedpoint.get_answer !fp with Some e -> e | None -> raise Not_found in
31
  (* Original code used the function Z3.Fixedpoint.get_ground_sat_answer !fp *)
23
  let cex =
24
    match Z3.Fixedpoint.get_answer !fp with
25
    | Some e ->
26
      e
27
    | None ->
28
      raise Not_found
29
  in
32 30

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

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

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

  
42 42
  (* Checking size *)
43 43
  let inputs = machine.mstep.step_inputs in
......
45 45
  let outputs = machine.mstep.step_outputs in
46 46
  let nb_outputs = List.length inputs in
47 47
  let nb_mems = List.length (full_memory_vars machines machine) in
48
  
48

  
49 49
  let main, _ =
50
    List.fold_left (fun (main, funs) conj ->
51
    (* Filtering out non MAIN decls *)
52
    let func_decl = Z3.Expr.get_func_decl conj in
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 in@mems@out *)
58
      let args = Z3.Expr.get_args conj in
59
      if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then
60
        (* Should be done with get_int but that function vanished from the opam Z3 API *)
61
	let id = Z.to_int (Z3.Arithmetic.Integer.get_big_int (List.hd args)) in
62
	let input_values = Utils.List.extract args 1 (1 + nb_inputs) in
63
	let output_values = Utils.List.extract args (1+nb_inputs+nb_mems) (1 + nb_inputs + nb_mems + nb_outputs) in
64
	(id, (input_values, output_values))::main, funs
65
      else
66
	assert false
67
    else
68
      let reg = Str.regexp_string "[a-z]*_step" in
69
      if Str.string_match reg node_name 0 then (
70
	let actual_name = Str.matched_group 0 node_name in
71
	Format.eprintf "Name %s@." actual_name;
72
	main, funs
73
      )
74
      else (
75
	Format.eprintf "pas matché %s@." node_name;
76
	main, funs
77
      )
78
    ) ((* main*) [],(* other functions *) []) conjuncts
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
79 87
  in
80 88
  let main = List.sort (fun (id1, _) (id2, _) -> compare id1 id2) main in
81
  List.iter (
82
    fun (id, expr) ->
83
      Format.eprintf "Id %i: %a@."
84
	(id)
85
	(Utils.fprintf_list ~sep:", "
86
	   (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
87
	(fst expr)
88
  ) main;		    
89
   (* let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *)
90

  
91
   (* We recover the Zustre XML format, projecting each cex on each input/output
92
      signal *)
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 *)
93 102
  let in_signals, _ =
94
    List.fold_right (
95
      fun (id, (sigs_in, sigs_out)) (res_sigs_in, res_sigs_out) ->
96
	let add l1 l2 = List.map2 (fun e1 e2 -> fst e2, ((id, e1)::(snd e2))) l1 l2 in
97
	let sigs_in_id = add sigs_in res_sigs_in in
98
	let sigs_out_id = add sigs_out res_sigs_out in
99
	sigs_in_id, sigs_out_id
100
    ) main (List.map (fun v -> v, []) inputs, List.map (fun v -> v, []) outputs)
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)
101 113
  in
102 114

  
103 115
  (* let _ = List.mapi (fun k conj -> *)
104 116
  (*   (\* k-iterate *\) *)
105
  (*   let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in *)
106
  (*   let func_decl = Z3.Expr.get_func_decl conj in *)
107
  (*   if !debug then Format.eprintf "FuncDecl %s@." (Z3.FuncDecl.to_string func_decl); *)
108
  (*   let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in *)
109

  
110
   
111
  (*   if !debug then Format.eprintf "Node %s, args %a@." node_name  (Utils.fprintf_list ~sep:", " (Format.pp_print_string)) ground_val; *)
112
    
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

  
113 127
  (*   () *)
114 128
  (*   (\*  ground_pair = [] *)
115 129
  (*           try: *)
116 130
  (*               ground_vars = pred_dict[node_name] *)
117 131
  (*               ground_pair = zip(ground_vars,ground_val) *)
118 132
  (*               if "_reset" in node_name: *)
119
  (*                   # this condition is to remove the node nodename_reset added by lustrec *)
133
  (* # this condition is to remove the node nodename_reset added by lustrec *)
120 134
  (*                   continue *)
121 135
  (*                   # node = node_name.split("_reset")[0] *)
122 136
  (*                   # cex_dict.update({node:{k:ground_pair}}) *)
......
125 139
  (*                   try: *)
126 140
  (*                       # case in which we already have the node in dict *)
127 141
  (*                       d = cex_dict[node] *)
128
  (*                       max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *)
142
  (* max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key
143
     value and add 1 *)
129 144
  (*                       d.update({(max_key+1):ground_pair}) *)
130 145
  (*                   except Exception as e: *)
131 146
  (*                       self._log.warning("Adding a new node cex " + str(e)) *)
......
134 149
  (*                   node = node_name *)
135 150
  (*                   try: *)
136 151
  (*                       d = cex_dict[node] *)
137
  (*                       max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1 *)
152
  (* max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key
153
     value and add 1 *)
138 154
  (*                       d.update({(max_key+1):ground_pair}) *)
139 155
  (*                   except Exception as e: *)
140 156
  (*                       if node not in ["MAIN", "ERR"]: *)
141
  (*                           self._log.warning("Adding a new node cex " + str(e)) *)
157
  (* self._log.warning("Adding a new node cex " + str(e)) *)
142 158
  (*                           cex_dict.update({node:{k:ground_pair}}) *)
143 159
  (*           except Exception as e: *)
144
  (*               self._log.warning("Problem with getting a node name: " + str(e)) *)
160
  (* self._log.warning("Problem with getting a node name: " + str(e)) *)
145 161
  (*   *\) *)
146 162
  (* ) conjuncts in *)
147 163
  (*   let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
......
156 172
  (*  let _ (*stats_entries*) =   Z3.Statistics.get_entries stats in *)
157 173
  (* List.iter (fun e -> Format.eprintf "%s@.@?" *)
158 174
  (*   (Z3.Statistics.Entry.to_string e) *)
159
    
175

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

  
213 253
(* Local Variables: *)
214 254
(* compile-command:"make -C ../.. lustrev" *)
215 255
(* End: *)
216

  
217
	

Also available in: Unified diff