Project

General

Profile

Download (7.62 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
open Lustre_types
7
open Machine_code_types
8
open Machine_code_common
9
open Zustre_common
10
open Zustre_data
11

    
12
let idx_0 = Z3.Arithmetic.Integer.mk_numeral_i !ctx 0
13

    
14
let uid_0 = Z3.Z3List.nil uid_sort
15

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

    
20
  (* Declaring collecting semantics *)
21
  let main_output = rename_machine_list node_id machine.mstep.step_outputs in
22
  let main_output_dummy =
23
    rename_machine_list ("dummy" ^ node_id) machine.mstep.step_outputs
24
  in
25
  let main_input = rename_machine_list node_id machine.mstep.step_inputs in
26
  let main_input_dummy =
27
    rename_machine_list ("dummy" ^ node_id) machine.mstep.step_inputs
28
  in
29
  let main_memory_next =
30
    main_input
31
    @ rename_next_list
32
        (* machine.mname.node_id *)
33
        (full_memory_vars machines machine)
34
    @ main_output
35
  in
36
  let main_memory_current =
37
    main_input_dummy
38
    @ rename_current_list
39
        (* machine.mname.node_id *)
40
        (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
45
     le buffer ? Faut-il declarer les "rel" dans la hashtbl ? *)
46
  let main_name node_id = "MAIN" ^ "_" ^ node_id in
47

    
48
  let decl_main =
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
52

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

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

    
60
  (* let _ = add_rule [] (Z3.Expr.mk_app *)
61
  (* 			 !ctx *)
62
  (* 			 decl_init *)
63
  (* 			 [] *)
64
  (* )  in *)
65

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

    
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)
73
  in
74
  (* Special case when the main node is stateless *)
75
  let _ =
76
    if Machine_code_common.is_stateless machine then
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)
95
    else
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)
126
  in
127

    
128
  let step_name =
129
    if Machine_code_common.is_stateless machine then machine_stateless_name
130
    else machine_step_name
131
  in
132

    
133
  (* ; Inductive def@. *)
134
  List.iter (fun x -> ignore (decl_var x)) (main_output_dummy @ main_input_dummy);
135

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

    
139
  (* fprintf fmt *)
140
  (* "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN
141
     %a)@]@.))@.@." *)
142
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *)
143
  (*   step_name node *)
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
150
  let k_var = Z3.Expr.mk_const_f !ctx (decl_var k) in
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)
157
  in
158
  let horn_body =
159
    Z3.Boolean.mk_and !ctx
160
      [
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));
167
      ]
168
  in
169
  (* Vars contains all vars: in_out, current, mid, neXt memories *)
170
  let vars =
171
    step_vars_c_m_x machines machine @ main_output_dummy @ main_input_dummy
172
  in
173
  let _ =
174
    add_rule ~dont_touch:[ decl_main ] (k :: vars)
175
      (Z3.Boolean.mk_implies !ctx horn_body horn_head)
176
  in
177

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

    
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 *)
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:"@ " (fun fmt e ->
207
           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 ->
215
      Zustre_cex.build_cex machine machines decl_err
216
    | Z3.Solver.UNSATISFIABLE -> (
217
      (*build_inv*)
218
      let expr_opt = Z3.Fixedpoint.get_answer !fp in
219
      match expr_opt with
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
    ()
230
(* Local Variables: *)
231
(* compile-command:"make -C ../.. lustrev" *)
232
(* End: *)
(2-2/7)