Project

General

Profile

Download (7.08 KB) Statistics
| Branch: | Tag: | Revision:
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
  
45
  let decl_main =
46
    decl_rel
47
      ("MAIN" ^ "_" ^ node_id)
48
      (int_sort::(List.map (fun v -> type_to_sort v.var_type) (main_memory_next))) in
49

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

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

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

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

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

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

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

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

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

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

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

    
176

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

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

    
202
      (* Debug instructions *)
203
  let rules_expr = Z3.Fixedpoint.get_rules !fp in
204
  if !debug then
205
    Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
206
    (Utils.fprintf_list ~sep:"@ "
207
       (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
208
      rules_expr;
209
  try
210
    let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
211
    
212
    Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
213
    match res_status with
214
    | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err
215
       
216
    | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
217
      let expr_opt = Z3.Fixedpoint.get_answer !fp in
218
      match expr_opt with
219
	None -> if !debug then Format.eprintf "Unsat No feedback@."
220
      | Some e -> if !debug then Format.eprintf "Unsat Result: %s@." (Z3.Expr.to_string e)
221
    )
222
    | Z3.Solver.UNKNOWN -> ()
223
  with Z3.Error msg -> Format.eprintf "Z3 failure: %s@." msg; () 
224
(* Local Variables: *)
225
(* compile-command:"make -C ../.. lustrev" *)
226
(* End: *)
(1-1/6)