Project

General

Profile

Download (7.28 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 idx_0 = Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 
15
let uid_0 = Z3.Z3List.nil uid_sort 
16
	    
17
let check machines node =
18

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

    
44
  (* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ?
45
     Faut-il declarer les "rel" dans la hashtbl ?
46
  *)
47

    
48
  let main_name node_id = "MAIN" ^ "_" ^ node_id in
49
    
50
  let decl_main =
51
    decl_rel ~no_additional_vars:true
52
      (main_name node_id)
53
      (int_sort::(List.map (fun v -> type_to_sort v.var_type) (main_memory_next))) in
54

    
55
  
56
  
57
  (* Init case *)
58
  let decl_init = decl_rel ~no_additional_vars:true "INIT_STATE" [] in
59

    
60
  (* (special) rule INIT_STATE *)
61
  let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
62
  Z3.Fixedpoint.add_rule !fp init_expr None;
63
  (* let _ = add_rule [] (Z3.Expr.mk_app *)
64
  (* 			 !ctx *)
65
  (* 			 decl_init *)
66
  (* 			 [] *)
67
  (* )  in *)
68

    
69
  (* Re-declaring variables *)
70
  let _ = List.map decl_var main_memory_next in
71

    
72
  let horn_head = 
73
    Z3.Expr.mk_app
74
      !ctx
75
      decl_main
76
      (idx_0::(* uid_0:: *)(List.map horn_var_to_expr main_memory_next))
77
  in
78
  (* Special case when the main node is stateless *)
79
  let _ =
80
    if Machine_code_common.is_stateless machine then
81
      begin
82
	
83
	(* Initial set: One Step(m,x)  -- Stateless node  *)	
84
     	(* rule => (INIT_STATE and step(mid, next)) MAIN(next) *)
85

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

    
108
	(* Re-declaring variables *)
109
	let vars_reset = reset_vars machines machine in
110
	let vars_step = step_vars_m_x machines machine in
111
	let vars_step_all = step_vars_c_m_x machines machine in
112
	let _ = List.map decl_var (vars_reset @ vars_step @ vars_step_all ) in
113

    
114
	(* rule => (INIT_STATE and reset(mid) and step(mid, next)) MAIN(next) *)
115
	let horn_body =
116
	  Z3.Boolean.mk_and !ctx
117
	    [
118
	      Z3.Expr.mk_app !ctx decl_init [];
119
	      Z3.Expr.mk_app !ctx
120
		(get_fdecl (machine_reset_name node))
121
		(idx_0::uid_0::List.map horn_var_to_expr (reset_vars machines machine));
122
	      Z3.Expr.mk_app !ctx
123
		(get_fdecl (machine_step_name node))
124
		(idx_0::uid_0::List.map horn_var_to_expr (step_vars_m_x machines machine))
125
	    ]
126
	in
127

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

    
145
  List.iter (fun x -> ignore (decl_var x)) (main_output_dummy @ main_input_dummy);
146
  
147
  (* (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; *)
148

    
149
  (* fprintf fmt *)
150
  (*   "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." *)
151
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *)
152
  (*   step_name node *)
153
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) *)
154

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

    
181

    
182
  (* Property def *)
183
  let decl_err = decl_rel ~no_additional_vars:true "ERR" [] in
184

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

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