Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/tools/zustre/zustre_analyze.ml
1 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. 
2
   that the system is properly defined and check that the property is valid.
3 3

  
4 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
*)
5
   expressed as a sequence of input values. *)
8 6
open Lustre_types
9 7
open Machine_code_types
10 8
open Machine_code_common
11 9
open Zustre_common
12 10
open Zustre_data
13 11

  
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 =
12
let idx_0 = Z3.Arithmetic.Integer.mk_numeral_i !ctx 0
13

  
14
let uid_0 = Z3.Z3List.nil uid_sort
18 15

  
16
let check machines node =
19 17
  let machine = get_machine machines node in
20 18
  let node_id = machine.mname.node_id in
19

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

  
44
  (* TODO: push/pop? donner un nom different par instance pour les garder dans
45
     le buffer ? Faut-il declarer les "rel" dans la hashtbl ? *)
48 46
  let main_name node_id = "MAIN" ^ "_" ^ node_id in
49
    
47

  
50 48
  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
49
    decl_rel ~no_additional_vars:true (main_name node_id)
50
      (int_sort :: List.map (fun v -> type_to_sort v.var_type) main_memory_next)
51
  in
54 52

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

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

  
63 60
  (* let _ = add_rule [] (Z3.Expr.mk_app *)
64 61
  (* 			 !ctx *)
65 62
  (* 			 decl_init *)
......
69 66
  (* Re-declaring variables *)
70 67
  let _ = List.map decl_var main_memory_next in
71 68

  
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))
69
  let horn_head =
70
    Z3.Expr.mk_app !ctx decl_main
71
      (idx_0 :: (* uid_0:: *)
72
                List.map horn_var_to_expr main_memory_next)
77 73
  in
78 74
  (* Special case when the main node is stateless *)
79 75
  let _ =
80 76
    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
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
              (idx_0 :: uid_0 :: List.map horn_var_to_expr vars);
92
          ]
93
      in
94
      add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
104 95
    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
96
      (* Initial set: Reset(c,m) + One Step(m,x) @. *)
97

  
98
      (* Re-declaring variables *)
99
      let vars_reset = reset_vars machines machine in
100
      let vars_step = step_vars_m_x machines machine in
101
      let vars_step_all = step_vars_c_m_x machines machine in
102
      let _ = List.map decl_var (vars_reset @ vars_step @ vars_step_all) in
103

  
104
      (* rule => (INIT_STATE and reset(mid) and step(mid, next)) MAIN(next) *)
105
      let horn_body =
106
        Z3.Boolean.mk_and !ctx
107
          [
108
            Z3.Expr.mk_app !ctx decl_init [];
109
            Z3.Expr.mk_app !ctx
110
              (get_fdecl (machine_reset_name node))
111
              (idx_0
112
               ::
113
               uid_0 :: List.map horn_var_to_expr (reset_vars machines machine));
114
            Z3.Expr.mk_app !ctx
115
              (get_fdecl (machine_step_name node))
116
              (idx_0
117
               ::
118
               uid_0
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)
134 126
  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
127

  
128
  let step_name =
129
    if Machine_code_common.is_stateless machine then machine_stateless_name
130
    else machine_step_name
141 131
  in
142
  
143
  (* ; Inductive def@. *)
144 132

  
133
  (* ; Inductive def@. *)
145 134
  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; *)
135

  
136
  (* (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var
137
     v)) fmt main_output_dummy; *)
148 138

  
149 139
  (* fprintf fmt *)
150
  (*   "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." *)
140
  (* "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN
141
     %a)@]@.))@.@." *)
151 142
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *)
152 143
  (*   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
144
  (* (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines
145
     machine) *)
146
  let k =
147
    Corelang.dummy_var_decl "k" Type_predef.type_int
148
    (*Corelang.mktyp Location.dummy_loc Types.type_int*)
149
  in
156 150
  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))
151

  
152
  let horn_head =
153
    Z3.Expr.mk_app !ctx decl_main
154
      (Z3.Arithmetic.mk_add !ctx
155
         [ k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1 ]
156
       :: List.map horn_var_to_expr main_memory_next)
166 157
  in
167 158
  let horn_body =
168 159
    Z3.Boolean.mk_and !ctx
169 160
      [
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))
161
        Z3.Expr.mk_app !ctx decl_main
162
          (k_var :: List.map horn_var_to_expr main_memory_current);
163
        Z3.Expr.mk_app !ctx
164
          (get_fdecl (step_name node))
165
          (k_var
166
           :: uid_0 :: List.map horn_var_to_expr (step_vars machines machine));
172 167
      ]
173 168
  in
174 169
  (* 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
170
  let vars =
171
    step_vars_c_m_x machines machine @ main_output_dummy @ main_input_dummy
172
  in
176 173
  let _ =
177
    add_rule ~dont_touch:[decl_main] (k::vars)  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
178
      
174
    add_rule ~dont_touch:[ decl_main ] (k :: vars)
175
      (Z3.Boolean.mk_implies !ctx horn_body horn_head)
179 176
  in
180 177

  
181

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

  
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 *)
181
  let prop = Z3.Boolean.mk_and !ctx (List.map horn_var_to_expr main_output) in
182
  let not_prop = Z3.Boolean.mk_not !ctx prop in
183
  add_rule
184
    (*~dont_touch:[decl_main;decl_err]*)
185
    (k :: main_memory_next)
186
    (Z3.Boolean.mk_implies !ctx
187
       (Z3.Boolean.mk_and !ctx
188
          [
189
            not_prop;
190
            Z3.Expr.mk_app !ctx decl_main
191
              (k_var :: List.map horn_var_to_expr main_memory_next);
192
          ])
193
       (Z3.Expr.mk_app !ctx decl_err []));
194

  
195
  (* fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@
196
     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 *)
208 203
  let rules_expr = Z3.Fixedpoint.get_rules !fp in
209 204
  if !debug then
210 205
    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)) )
206
      (Utils.fprintf_list ~sep:"@ " (fun fmt e ->
207
           Format.pp_print_string fmt (Z3.Expr.to_string e)))
213 208
      rules_expr;
214 209
  try
215
    let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
216
    
210
    let res_status = Z3.Fixedpoint.query_r !fp [ decl_err ] in
211

  
217 212
    Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
218 213
    match res_status with
219
    | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err
220
       
221
    | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
214
    | Z3.Solver.SATISFIABLE ->
215
      Zustre_cex.build_cex machine machines decl_err
216
    | Z3.Solver.UNSATISFIABLE -> (
217
      (*build_inv*)
222 218
      let expr_opt = Z3.Fixedpoint.get_answer !fp in
223 219
      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; () 
220
      | None ->
221
        if !debug then Format.eprintf "Unsat No feedback@."
222
      | Some e ->
223
        if !debug then Format.eprintf "Unsat Result: %s@." (Z3.Expr.to_string e)
224
      )
225
    | Z3.Solver.UNKNOWN ->
226
      ()
227
  with Z3.Error msg ->
228
    Format.eprintf "Z3 failure: %s@." msg;
229
    ()
229 230
(* Local Variables: *)
230 231
(* compile-command:"make -C ../.. lustrev" *)
231 232
(* End: *)

Also available in: Unified diff