Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_analyze.ml @ 2f7c9195

History | View | Annotate | Download (6.94 KB)

1
(* This module takes a main node (reset and step) and a property. It assumes
2
   that the system is properly defined and check that the property is valid. 
3

    
4
   When valid, it returns a set of local invariants. Otherwise, it returns a cex
5
   expressed as a sequence of input values.
6

    
7
*)
8
open Lustre_types
9
open Machine_code_types
10
open Machine_code_common
11
open Zustre_common
12
open Zustre_data
13

    
14
let check machines node =
15

    
16
  let machine = get_machine machines node in
17
  let node_id = machine.mname.node_id in
18
  (* Declaring collecting semantics *)
19
  
20
  let main_output =
21
    rename_machine_list node_id machine.mstep.step_outputs
22
  in
23
  let main_output_dummy =
24
    rename_machine_list ("dummy" ^ node_id) machine.mstep.step_outputs
25
  in
26
  let main_input = 
27
    rename_machine_list node_id machine.mstep.step_inputs
28
  in  
29
  let main_input_dummy = 
30
    rename_machine_list ("dummy" ^ node_id) machine.mstep.step_inputs
31
  in  
32
  let main_memory_next =
33
    main_input @ (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
34
      main_output
35
  in
36
  let main_memory_current =
37
    main_input_dummy @ (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
38
      main_output_dummy
39
  in
40

    
41
  (* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ?
42
     Faut-il declarer les "rel" dans la hashtbl ?
43
  *)
44
  let decl_main =
45
    decl_rel
46
      ("MAIN" ^ "_" ^ node_id)
47
      (int_sort::(List.map (fun v -> type_to_sort v.var_type) (main_memory_next))) in
48

    
49
  
50
  
51
  (* Init case *)
52
  let decl_init = decl_rel "INIT_STATE" [] in
53

    
54
  (* (special) rule INIT_STATE *)
55
  let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
56
  Z3.Fixedpoint.add_rule !fp init_expr None;
57
  (* let _ = add_rule [] (Z3.Expr.mk_app *)
58
  (* 			 !ctx *)
59
  (* 			 decl_init *)
60
  (* 			 [] *)
61
  (* )  in *)
62

    
63
  (* Re-declaring variables *)
64
  let _ = List.map decl_var main_memory_next in
65

    
66
  let horn_head = 
67
    Z3.Expr.mk_app
68
      !ctx
69
      decl_main
70
      ((Z3.Arithmetic.Integer.mk_numeral_i !ctx 0)::(List.map horn_var_to_expr main_memory_next))
71
  in
72
  (* Special case when the main node is stateless *)
73
  let _ =
74
    if Machine_code_common.is_stateless machine then
75
      begin
76
	
77
	(* Initial set: One Step(m,x)  -- Stateless node  *)	
78
     	(* rule => (INIT_STATE and step(mid, next)) MAIN(next) *)
79

    
80
	(* Note that vars here contains main_memory_next *)
81
	let vars = step_vars_m_x machines machine in
82
	(* Re-declaring variables *)
83
	let _ = List.map decl_var vars in
84
	
85
	let horn_body =
86
	  Z3.Boolean.mk_and !ctx
87
	    [
88
	      Z3.Expr.mk_app !ctx decl_init [];
89
	      Z3.Expr.mk_app !ctx
90
		(get_fdecl (machine_stateless_name node))
91
		(List.map horn_var_to_expr vars) 
92
	    ]
93
	in
94
	add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
95
	  
96
	  
97
      end
98
    else
99
      begin
100
	(* Initial set: Reset(c,m) + One Step(m,x) @. *)
101

    
102
	(* Re-declaring variables *)
103
	let vars_reset = reset_vars machines machine in
104
	let vars_step = step_vars_m_x machines machine in
105
	let vars_step_all = step_vars_c_m_x machines machine in
106
	let _ = List.map decl_var (vars_reset @ vars_step @ vars_step_all ) in
107

    
108
	(* rule => (INIT_STATE and reset(mid) and step(mid, next)) MAIN(next) *)
109
	let horn_body =
110
	  Z3.Boolean.mk_and !ctx
111
	    [
112
	      Z3.Expr.mk_app !ctx decl_init [];
113
	      Z3.Expr.mk_app !ctx
114
		(get_fdecl (machine_reset_name node))
115
		(List.map horn_var_to_expr (reset_vars machines machine));
116
	      Z3.Expr.mk_app !ctx
117
		(get_fdecl (machine_step_name node))
118
		(List.map horn_var_to_expr (step_vars_m_x machines machine))
119
	    ]
120
	in
121

    
122
	(* Vars contains all vars: in_out, current, mid, neXt memories *)
123
	let vars = step_vars_c_m_x machines machine in
124
	add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
125
	  
126
	  
127
      end
128
  in
129
  
130
  let step_name = 
131
    if Machine_code_common.is_stateless machine then 
132
      machine_stateless_name
133
    else
134
      machine_step_name
135
  in
136
  
137
  (* ; Inductive def@. *)
138

    
139
  List.iter (fun x -> ignore (decl_var x)) (main_output_dummy @ main_input_dummy);
140
  
141
  (* (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; *)
142

    
143
  (* fprintf fmt *)
144
  (*   "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." *)
145
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *)
146
  (*   step_name node *)
147
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) *)
148

    
149
  let k = Corelang.dummy_var_decl "k" Type_predef.type_int (*Corelang.mktyp Location.dummy_loc Types.type_int*) in
150
  let k_var = decl_var k in
151
  
152
  let horn_head = 
153
    Z3.Expr.mk_app
154
      !ctx
155
      decl_main
156
      ((Z3.Arithmetic.mk_add
157
	  !ctx
158
	  [Z3.Expr.mk_const_f !ctx k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1]
159
       )::(List.map horn_var_to_expr main_memory_next))
160
  in
161
  let horn_body =
162
    Z3.Boolean.mk_and !ctx
163
      [
164
	Z3.Expr.mk_app !ctx decl_main (Z3.Expr.mk_const_f !ctx k_var::(List.map horn_var_to_expr main_memory_current));
165
	Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (List.map horn_var_to_expr (step_vars machines machine))
166
      ]
167
  in
168
  (* Vars contains all vars: in_out, current, mid, neXt memories *)
169
  let vars = (step_vars_c_m_x machines machine) @ main_output_dummy @ main_input_dummy  in
170
  let _ =
171
    add_rule ~dont_touch:[decl_main] (k::vars)  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
172
      
173
  in
174

    
175

    
176
  (* Property def *)
177
  let decl_err = decl_rel "ERR" [] in
178

    
179
  let prop =
180
    Z3.Boolean.mk_and !ctx (List.map horn_var_to_expr main_output)
181
  in
182
  let not_prop =
183
    Z3.Boolean.mk_not !ctx prop
184
  in
185
  add_rule (*~dont_touch:[decl_main;decl_err]*) (k::main_memory_next) (Z3.Boolean.mk_implies !ctx
186
	      (
187
		Z3.Boolean.mk_and !ctx
188
		  [not_prop;
189
		   Z3.Expr.mk_app !ctx decl_main (Z3.Expr.mk_const_f !ctx k_var::List.map horn_var_to_expr main_memory_next);
190
		  ]
191
	      )
192
	      (Z3.Expr.mk_app !ctx decl_err []))
193
  ;
194
  
195
      (* fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." *)
196
      (*   (pp_conj (pp_horn_var machine)) main_output *)
197
      (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next *)
198
      (*   ; *)
199
      (*  if !Options.horn_query then fprintf fmt "(query ERR)@." *)
200

    
201
      (* Debug instructions *)
202
  let rules_expr = Z3.Fixedpoint.get_rules !fp in
203
  if true then
204
    Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
205
    (Utils.fprintf_list ~sep:"@ "
206
       (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
207
    rules_expr;
208
  let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
209

    
210
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
211
  match res_status with
212
  | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex decl_err
213
  
214
  | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
215
       let expr_opt = Z3.Fixedpoint.get_answer !fp in
216
       match expr_opt with
217
	 None -> Format.eprintf "Unsat No feedback@."
218
       | Some e -> Format.eprintf "Unsat Result: %s@." (Z3.Expr.to_string e)
219
  )
220
  | Z3.Solver.UNKNOWN -> ()
221
      
222
(* Local Variables: *)
223
(* compile-command:"make -C ../.." *)
224
(* End: *)