Project

General

Profile

Revision 5778dd5e

View differences:

src/_tags.in
11 11
"plugins/mpfr": include
12 12
"features/machine_types": include
13 13
"tools": include
14
"tools/zustre": include
14 15
"tools/stateflow": include
15 16
"tools/stateflow/common": include
16 17
"tools/stateflow/semantics": include
src/backends/Horn/horn_backend_common.ml
147 147
  (rename_current_list (full_memory_vars machines m)) 
148 148
  @ (rename_mid_list (full_memory_vars machines m))
149 149

  
150
let step_vars_c_m_x machines m =
151
  (inout_vars machines m) 
152
  @ (rename_current_list (full_memory_vars machines m)) 
153
  @ (rename_mid_list (full_memory_vars machines m)) 
154
  @ (rename_next_list (full_memory_vars machines m))
150 155

  
151 156

  
152 157
(* Local Variables: *)
src/tools/zustre/zustre_analyze.ml
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

  
18
  (* Declaring collecting semantics *)
19
  
20
  let main_output =
21
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
22
  in
23
  let main_output_dummy =
24
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
25
  in
26
  let main_memory_next =
27
    (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
28
      main_output
29
  in
30
  let main_memory_current =
31
    (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
32
      main_output_dummy
33
  in
34

  
35
  (* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ?
36
     Faut-il declarer les "rel" dans la hashtbl ?
37
  *)
38
  let decl_main = decl_rel "MAIN" main_memory_next in
39

  
40
  
41
  
42
  (* Init case *)
43
  let decl_init = decl_rel "INIT_STATE" [] in
44

  
45
  (* rule INIT_STATE *)
46
  let _ = add_rule [] (Z3.Expr.mk_app
47
			 !ctx
48
			 decl_init
49
			 []
50
  )  in
51
  
52
  let horn_head = 
53
    Z3.Expr.mk_app
54
      !ctx
55
      decl_main
56
      (List.map horn_var_to_expr main_memory_next)
57
  in
58
  (* Special case when the main node is stateless *)
59
  let _ =
60
    if Machine_code_common.is_stateless machine then
61
      begin
62
	
63
	(* Initial set: One Step(m,x)  -- Stateless node  *)	
64
     	(* rule => (INIT_STATE and step(mid, next)) MAIN(next) *)
65

  
66
	(* Note that vars here contains main_memory_next *)
67
	let vars = step_vars_m_x machines machine in
68
	
69
	let horn_body =
70
	  Z3.Boolean.mk_and !ctx
71
	    [
72
	      Z3.Expr.mk_app !ctx decl_init [];
73
	      Z3.Expr.mk_app !ctx
74
		(get_fdecl (machine_stateless_name node))
75
		(List.map horn_var_to_expr vars) 
76
	    ]
77
	in
78
	add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
79
	  
80
	  
81
      end
82
    else
83
      begin
84
	(* Initial set: Reset(c,m) + One Step(m,x) @. *)
85
	(* rule => (INIT_STATE and reset(mid) and step(mid, next)) MAIN(next) *)
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_reset_name node))
92
		(List.map horn_var_to_expr (reset_vars machines machine));
93
	      Z3.Expr.mk_app !ctx
94
		(get_fdecl (machine_step_name node))
95
		(List.map horn_var_to_expr (step_vars_m_x machines machine))
96
	    ]
97
	in
98

  
99
	(* Vars contains all vars: in_out, current, mid, neXt memories *)
100
	let vars = step_vars_c_m_x machines machine in
101
	add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
102
	  
103
	  
104
      end
105
  in
106
  
107
  let step_name = 
108
    if Machine_code_common.is_stateless machine then 
109
      machine_stateless_name
110
    else
111
      machine_step_name
112
  in
113
  
114
  (* ; Inductive def@. *)
115

  
116
  List.iter (fun x -> ignore (decl_var x)) main_output_dummy;
117
  
118
  (* (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; *)
119

  
120
  (* fprintf fmt *)
121
  (*   "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." *)
122
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *)
123
  (*   step_name node *)
124
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) *)
125
  
126
  
127
  let horn_head = 
128
    Z3.Expr.mk_app
129
      !ctx
130
      decl_main
131
      (List.map horn_var_to_expr main_memory_next)
132
  in
133
  let horn_body =
134
    Z3.Boolean.mk_and !ctx
135
      [
136
	Z3.Expr.mk_app !ctx decl_main (List.map horn_var_to_expr main_memory_current);
137
	Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (List.map horn_var_to_expr (step_vars machines machine))
138
      ]
139
  in
140
  let _ =
141
    add_rule []  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
142
      
143
  in
144

  
145

  
146
  (* Property def *)
147
  let decl_err = decl_rel "ERR" [] in
148

  
149
  let prop =
150
    Z3.Boolean.mk_and !ctx (List.map horn_var_to_expr main_output)
151
  in
152
  let not_prop =
153
    Z3.Boolean.mk_not !ctx prop
154
  in
155
  add_rule main_memory_next (Z3.Boolean.mk_implies !ctx
156
	      (
157
		Z3.Boolean.mk_and !ctx
158
		  [not_prop;
159
		   Z3.Expr.mk_app !ctx decl_main (List.map horn_var_to_expr main_memory_next);
160
		  ]
161
	      )
162
	      (Z3.Expr.mk_app !ctx decl_err []))
163
  ;
164
  
165
      (* fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." *)
166
      (*   (pp_conj (pp_horn_var machine)) main_output *)
167
      (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next *)
168
      (*   ; *)
169
      (*  if !Options.horn_query then fprintf fmt "(query ERR)@." *)
170

  
171
      (* Debug instructions *)
172
  let rules_expr = Z3.Fixedpoint.get_rules !fp in
173
  Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
174
    (Utils.fprintf_list ~sep:"@ "
175
       (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
176
    rules_expr;
177

  
178
  
179
  let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
180

  
181
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)
182
  
183
(* Local Variables: *)
184
(* compile-command:"make -C ../.." *)
185
(* End: *)
src/tools/zustre/zustre_common.ml
1
open Lustre_types
2
open Machine_code_types
3
open Machine_code_common
4
open Format
5
(* open Horn_backend_common
6
 * open Horn_backend *)
7
open Zustre_data
8

  
9
module HBC = Horn_backend_common
10
let node_name = HBC.node_name
11

  
12
let concat = HBC.concat
13

  
14
let rename_machine = HBC.rename_machine
15
let rename_machine_list = HBC.rename_machine_list
16

  
17
let rename_next = HBC.rename_next
18
let rename_mid = HBC.rename_mid
19
let rename_current = HBC.rename_current
20

  
21
let rename_current_list = HBC.rename_current_list
22
let rename_mid_list = HBC.rename_mid_list
23
let rename_next_list = HBC.rename_next_list
24

  
25
let full_memory_vars = HBC.full_memory_vars
26
let inout_vars = HBC.inout_vars
27
let reset_vars = HBC.reset_vars
28
let step_vars = HBC.step_vars
29
let local_memory_vars = HBC.local_memory_vars
30
let step_vars_m_x = HBC.step_vars_m_x
31
let step_vars_c_m_x = HBC.step_vars_c_m_x
32
  
33
let machine_reset_name = HBC.machine_reset_name 
34
let machine_step_name = HBC.machine_step_name 
35
let machine_stateless_name = HBC.machine_stateless_name 
36

  
37
let preprocess = Horn_backend.preprocess
38
  
39
  
40
(** Sorts
41

  
42
A sort is introduced for each basic type and each enumerated type.
43

  
44
A hashtbl records these and allow easy access to sort values, when
45
   provided with a enumerated type name. 
46

  
47
*)
48
        
49
let bool_sort = Z3.Boolean.mk_sort !ctx
50
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
51
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
52

  
53

  
54
let get_const_sort = Hashtbl.find const_sorts 
55
let get_sort_elems = Hashtbl.find sort_elems
56
let get_tag_sort = Hashtbl.find const_tags
57
  
58

  
59
  
60
let decl_sorts () =
61
  Hashtbl.iter (fun typ decl ->
62
    match typ with
63
    | Tydec_const var ->
64
      (match decl.top_decl_desc with
65
      | TypeDef tdef -> (
66
	match tdef.tydef_desc with
67
	| Tydec_enum tl ->
68
	  let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
69
          Hashtbl.add const_sorts var new_sort;
70
          Hashtbl.add sort_elems new_sort tl;
71
          List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl
72
          
73
	| _ -> Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false
74
      )
75
      | _ -> assert false
76
      )
77
    | _        -> ()) Corelang.type_table
78

  
79
                 
80
let rec type_to_sort t =
81
  if Types.is_bool_type t  then bool_sort else
82
    if Types.is_int_type t then int_sort else 
83
  if Types.is_real_type t then real_sort else 
84
  match (Types.repr t).Types.tdesc with
85
  | Types.Tconst ty       -> get_const_sort ty
86
  | Types.Tclock t        -> type_to_sort t
87
  | Types.Tarray(dim,ty)   -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
88
  | Types.Tstatic(d, ty)-> type_to_sort ty
89
  | Types.Tarrow _
90
  | _                     -> Format.eprintf "internal error: pp_type %a@."
91
                               Types.print_ty t; assert false
92

  
93
(** Func decls
94

  
95
Similarly fun_decls are registerd, by their name, into a hashtbl. The
96
   proposed encoding introduces a 0-ary fun_decl to model variables
97
   and fun_decl with arguments to declare reset and step predicates.
98

  
99

  
100

  
101
 *)
102
let register_fdecl id fd = Hashtbl.add decls id fd
103
let get_fdecl id =
104
  try
105
    Hashtbl.find decls id
106
  with Not_found -> (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found)
107
    
108
let decl_var id =
109
  Format.eprintf "Declaring var %s@." id.var_id;
110
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
111
  Z3.Fixedpoint.register_relation !fp fdecl;
112
  register_fdecl id.var_id fdecl;
113
  fdecl
114

  
115
let decl_rel name args =
116
  (*verifier ce qui est construit. On veut un declare-rel *)
117
  let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in
118
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
119
  Z3.Fixedpoint.register_relation !fp fdecl;
120
  register_fdecl name fdecl;
121
  fdecl
122
  
123

  
124
(* Quantifiying universally all occuring variables *)
125
let add_rule vars expr =
126
  (* let fds = Z3.Expr.get_args expr in *)
127
  (* Format.eprintf "Expr %s: args: [%a]@." *)
128
  (*   (Z3.Expr.to_string expr) *)
129
  (*   (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *)
130

  
131
  (* Old code relying on provided vars *)
132
  let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in
133
  let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in
134
  
135
  (* New code: we extract vars from expr *)
136
  let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl
137
				      let compare = compare
138
				      let hash = Hashtbl.hash
139
  end)
140
  in
141
  let rec get_expr_vars e =
142
    let open Utils in
143
    let nb_args = Z3.Expr.get_num_args e in
144
    if nb_args <= 0 then (
145
      let fdecl = Z3.Expr.get_func_decl e in
146
      let params = Z3.FuncDecl.get_parameters fdecl in
147
      Format.eprintf "Extracting info about %s: [@?" (Z3.Expr.to_string e);
148
      let dkind = Z3.FuncDecl.get_decl_kind fdecl in
149
      match dkind with Z3enums.OP_UNINTERPRETED -> (
150
	Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | OP_UNINTERPRETED -> "uninter");
151
	let open Z3.FuncDecl.Parameter in
152
	List.iter (fun p ->
153
	  match p with
154
            P_Int i -> Format.eprintf "int %i" i
155
	  | P_Dbl f -> Format.eprintf "dbl %f" f
156
	  | P_Sym s -> Format.eprintf "symb" 
157
	  | P_Srt s -> Format.eprintf "sort" 
158
	  | P_Ast _ ->Format.eprintf "ast" 
159
	  | P_Fdl f -> Format.eprintf "fundecl" 
160
	  | P_Rat s -> Format.eprintf "rat %s" s 
161
	     
162
	) params;
163
	Format.eprintf "]@.";
164
	FDSet.singleton fdecl
165
      )
166
      | _ -> FDSet.empty
167
    )
168
    else (*if nb_args > 0 then*)
169
      List.fold_left
170
	(fun accu e ->  FDSet.union accu (get_expr_vars e))
171
	FDSet.empty (Z3.Expr.get_args e)
172
  in
173
  let vars = FDSet.elements (get_expr_vars expr) in
174
  let sorts = List.map Z3.FuncDecl.get_range vars in
175
  let symbols = List.map Z3.FuncDecl.get_name vars in
176
  
177
  let expr = Z3.Quantifier.mk_forall
178
    !ctx  (* context *)
179
    sorts           (* sort list*)
180
    symbols (* symbol list *)
181
    expr (* expression *)
182
    None (* quantifier weight, None means 1 *)
183
    [] (* pattern list ? *)
184
    [] (* ? *)
185
    None (* ? *)
186
    None (* ? *)
187
  in
188
  Z3.Fixedpoint.add_rule !fp
189
    (Z3.Quantifier.expr_of_quantifier expr)
190
    None
191

  
192

  
193
(** Conversion functions
194

  
195
The following is similar to the Horn backend. Each printing function
196
   is rephrased from pp_xx to xx_to_expr and produces a Z3 value.
197

  
198
 *)
199

  
200

  
201
(* Returns the f_decl associated to the variable v *)
202
let horn_var_to_expr v =
203
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
204

  
205

  
206

  
207

  
208
  (* Used to print boolean constants *)
209
let horn_tag_to_expr t =
210
  if t = Corelang.tag_true then
211
    Z3.Boolean.mk_true !ctx
212
  else if t = Corelang.tag_false then
213
    Z3.Boolean.mk_false !ctx
214
  else
215
    (* Finding the associated sort *)
216
    let sort = get_tag_sort t in
217
    let elems = get_sort_elems sort in 
218
    let res : Z3.Expr.expr option =
219
      List.fold_left2 (fun res cst expr ->
220
          match res with
221
          | Some _ -> res
222
          | None -> if t = cst then Some (expr:Z3.Expr.expr) else None
223
        ) None elems (Z3.Enumeration.get_consts sort)
224
    in
225
    match res with None -> assert false | Some s -> s
226
    
227
(* Prints a constant value *)
228
let rec horn_const_to_expr c =
229
  match c with
230
    | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
231
    | Const_real (_,_,s)   -> Z3.Arithmetic.Real.mk_numeral_i !ctx 0
232
    | Const_tag t    -> horn_tag_to_expr t
233
    | _              -> assert false
234

  
235

  
236

  
237
(* Default value for each type, used when building arrays. Eg integer array
238
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
239
   for the type integer (arrays).
240
*)
241
let rec horn_default_val t =
242
  let t = Types.dynamic_type t in
243
  if Types.is_bool_type t  then Z3.Boolean.mk_true !ctx else
244
  if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
245
  if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
246
  (* match (Types.dynamic_type t).Types.tdesc with
247
   * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\)
248
   *    let valt = Types.array_element_type t in
249
   *    fprintf fmt "((as const (Array Int %a)) %a)"
250
   *      pp_type valt 
251
   *      pp_default_val valt
252
   * | Types.Tstruct(l) -> assert false
253
   * | Types.Ttuple(l) -> assert false
254
   * |_ -> *) assert false
255

  
256
(* Conversion of basic library functions *)
257
    
258
let horn_basic_app i val_to_expr vl =
259
  match i, vl with
260
  | "ite", [v1; v2; v3] ->
261
     Z3.Boolean.mk_ite
262
       !ctx
263
       (val_to_expr v1)
264
       (val_to_expr v2)
265
       (val_to_expr v3)
266

  
267
  | "uminus", [v] ->
268
     Z3.Arithmetic.mk_unary_minus
269
       !ctx
270
       (val_to_expr v)
271
  | "not", [v] ->
272
     Z3.Boolean.mk_not
273
       !ctx
274
       (val_to_expr v)
275
  | "=", [v1; v2] ->
276
     Z3.Boolean.mk_eq
277
       !ctx
278
       (val_to_expr v1)
279
       (val_to_expr v2)
280
  | "&&", [v1; v2] ->
281
     Z3.Boolean.mk_and
282
       !ctx
283
       [val_to_expr v1;
284
        val_to_expr v2]
285
  | "||", [v1; v2] ->
286
          Z3.Boolean.mk_or
287
       !ctx
288
       [val_to_expr v1;
289
        val_to_expr v2]
290

  
291
  | "impl", [v1; v2] ->
292
     Z3.Boolean.mk_implies
293
       !ctx
294
       (val_to_expr v1)
295
       (val_to_expr v2)
296
 | "mod", [v1; v2] ->
297
          Z3.Arithmetic.Integer.mk_mod
298
       !ctx
299
       (val_to_expr v1)
300
       (val_to_expr v2)
301
  | "equi", [v1; v2] ->
302
          Z3.Boolean.mk_eq
303
       !ctx
304
       (val_to_expr v1)
305
       (val_to_expr v2)
306
  | "xor", [v1; v2] ->
307
          Z3.Boolean.mk_xor
308
       !ctx
309
       (val_to_expr v1)
310
       (val_to_expr v2)
311
  | "!=", [v1; v2] ->
312
     Z3.Boolean.mk_not
313
       !ctx
314
       (
315
         Z3.Boolean.mk_eq
316
           !ctx
317
           (val_to_expr v1)
318
           (val_to_expr v2)
319
       )
320
  | "/", [v1; v2] ->
321
     Z3.Arithmetic.mk_div
322
       !ctx
323
       (val_to_expr v1)
324
       (val_to_expr v2)
325

  
326
  | "+", [v1; v2] ->
327
     Z3.Arithmetic.mk_add
328
       !ctx
329
       [val_to_expr v1; val_to_expr v2]
330

  
331
  | "-", [v1; v2] ->
332
     Z3.Arithmetic.mk_sub
333
       !ctx
334
       [val_to_expr v1 ; val_to_expr v2]
335
       
336
  | "*", [v1; v2] ->
337
     Z3.Arithmetic.mk_mul
338
       !ctx
339
       [val_to_expr v1; val_to_expr v2]
340

  
341

  
342
  | "<", [v1; v2] ->
343
     Z3.Arithmetic.mk_lt
344
       !ctx
345
       (val_to_expr v1)
346
       (val_to_expr v2)
347

  
348
  | "<=", [v1; v2] ->
349
     Z3.Arithmetic.mk_le
350
       !ctx
351
       (val_to_expr v1)
352
       (val_to_expr v2)
353

  
354
  | ">", [v1; v2] ->
355
     Z3.Arithmetic.mk_gt
356
       !ctx
357
       (val_to_expr v1)
358
       (val_to_expr v2)
359

  
360
  | ">=", [v1; v2] ->
361
     Z3.Arithmetic.mk_ge
362
       !ctx
363
       (val_to_expr v1)
364
       (val_to_expr v2)
365

  
366
       
367
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
368
   *      !ctx
369
   *      (val_to_expr v1)
370
   *      (val_to_expr v2)
371
   * 
372
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
373
  | _ -> (
374
    Format.eprintf
375
      "internal error: zustre unkown function %s@." i;
376
    assert false)
377

  
378
           
379
(* Convert a value expression [v], with internal function calls only.
380
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
381
   but an offset suffix may be added for array variables
382
*)
383
let rec horn_val_to_expr ?(is_lhs=false) self v =
384
  match v.value_desc with
385
  | Cst c       -> horn_const_to_expr c
386

  
387
  (* Code specific for arrays *)
388
  | Array il    ->
389
     (* An array definition: 
390
	(store (
391
	  ...
392
 	    (store (
393
	       store (
394
	          default_val
395
	       ) 
396
	       idx_n val_n
397
	    ) 
398
	    idx_n-1 val_n-1)
399
	  ... 
400
	  idx_1 val_1
401
	) *)
402
     let rec build_array (tab, x) =
403
       match tab with
404
       | [] -> horn_default_val v.value_type(* (get_type v) *)
405
       | h::t ->
406
	  Z3.Z3Array.mk_store
407
            !ctx
408
	    (build_array (t, (x+1)))
409
	    (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
410
	    (horn_val_to_expr ~is_lhs:is_lhs self h)
411
     in
412
     build_array (il, 0)
413
       
414
  | Access(tab,index) ->
415
     Z3.Z3Array.mk_select !ctx 
416
       (horn_val_to_expr ~is_lhs:is_lhs self tab)
417
       (horn_val_to_expr ~is_lhs:is_lhs self index)
418

  
419
  (* Code specific for arrays *)
420
    
421
  | Power (v, n)  -> assert false
422
  | LocalVar v    ->
423
     horn_var_to_expr
424
       (rename_machine
425
          self
426
          v)
427
  | StateVar v    ->
428
     if Types.is_array_type v.var_type
429
     then assert false
430
     else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
431
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr self) vl
432

  
433
let no_reset_to_exprs machines m i =
434
  let (n,_) = List.assoc i m.minstances in
435
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
436

  
437
  let m_list = 
438
    rename_machine_list
439
      (concat m.mname.node_id i)
440
      (rename_mid_list (full_memory_vars machines target_machine))
441
  in
442
  let c_list =
443
    rename_machine_list
444
      (concat m.mname.node_id i)
445
      (rename_current_list (full_memory_vars machines target_machine))
446
  in
447
  match c_list, m_list with
448
  | [chd], [mhd] ->
449
     let expr =
450
       Z3.Boolean.mk_eq !ctx 
451
         (horn_var_to_expr mhd)
452
         (horn_var_to_expr chd)
453
     in
454
     [expr]
455
  | _ -> (
456
    let exprs =
457
      List.map2 (fun mhd chd -> 
458
          Z3.Boolean.mk_eq !ctx 
459
            (horn_var_to_expr mhd)
460
            (horn_var_to_expr chd)
461
        )
462
        m_list
463
        c_list
464
    in
465
    exprs
466
  )
467

  
468
let instance_reset_to_exprs machines m i =
469
  let (n,_) = List.assoc i m.minstances in
470
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
471
  let vars =
472
    (
473
      (rename_machine_list
474
	 (concat m.mname.node_id i)
475
	 (rename_current_list (full_memory_vars machines target_machine))
476
      ) 
477
      @
478
	(rename_machine_list
479
	   (concat m.mname.node_id i)
480
	   (rename_mid_list (full_memory_vars machines target_machine))
481
	)
482
    )
483
  in
484
  let expr =
485
    Z3.Expr.mk_app
486
      !ctx
487
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
488
      (List.map (horn_var_to_expr) vars)
489
  in
490
  [expr]
491

  
492
let instance_call_to_exprs machines reset_instances m i inputs outputs =
493
  let self = m.mname.node_id in
494
  try (* stateful node instance *)
495
    begin
496
      let (n,_) = List.assoc i m.minstances in
497
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
498

  
499
      (* Checking whether this specific instances has been reset yet *)
500
      let reset_exprs = 
501
        if not (List.mem i reset_instances) then
502
	  (* If not, declare mem_m = mem_c *)
503
	  no_reset_to_exprs machines m i
504
        else
505
          [] (* Nothing to add yet *)
506
      in
507
      
508
      let mems = full_memory_vars machines target_machine in
509
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
510
      let mid_mems = rename_mems rename_mid_list in
511
      let next_mems = rename_mems rename_next_list in
512

  
513
      let call_expr = 
514
      match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
515
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
516
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
517
            Z3.Boolean.mk_eq !ctx
518
              ( (* output var *)
519
                horn_val_to_expr
520
                  ~is_lhs:true
521
                  self
522
                  (mk_val (LocalVar o) o.var_type)
523
              )
524
              (
525
                Z3.Boolean.mk_ite !ctx 
526
	          (horn_var_to_expr mem_m) 
527
	          (horn_val_to_expr self i1)
528
	          (horn_val_to_expr self i2)
529
              )
530
          in
531
          let stmt2 = (* mem_X = false *)
532
            Z3.Boolean.mk_eq !ctx
533
	      (horn_var_to_expr mem_x)
534
              (Z3.Boolean.mk_false !ctx)
535
          in
536
          [stmt1; stmt2]
537
      end
538

  
539
      | node_name_n ->
540
         let expr = 
541
           Z3.Expr.mk_app
542
             !ctx
543
             (get_fdecl (machine_step_name (node_name n)))
544
             ( (* Arguments are input, output, mid_mems, next_mems *)
545
               (
546
                 List.map (horn_val_to_expr self) (
547
                     inputs @
548
	               (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
549
                   )
550
               ) @ (
551
                 List.map (horn_var_to_expr) (mid_mems@next_mems)
552
	       )
553
             )
554
         in
555
         [expr]
556
      in
557

  
558
      reset_exprs@call_expr
559
    end
560
  with Not_found -> ( (* stateless node instance *)
561
    let (n,_) = List.assoc i m.mcalls in
562
    let expr = 
563
      Z3.Expr.mk_app
564
        !ctx
565
        (get_fdecl (machine_stateless_name (node_name n)))
566
        ((* Arguments are inputs, outputs *)
567
         List.map (horn_val_to_expr self)
568
           (
569
             inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
570
           )
571
        )
572
    in
573
    [expr]
574
  )
575

  
576

  
577
    
578
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
579
(* let rec value_suffix_to_expr self value = *)
580
(*  match value.value_desc with *)
581
(*  | Fun (n, vl)  ->  *)
582
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
583
    
584
(*  |  _            -> *)
585
(*    horn_val_to_expr self value *)
586

  
587

  
588
(* type_directed assignment: array vs. statically sized type
589
   - [var_type]: type of variable to be assigned
590
   - [var_name]: name of variable to be assigned
591
   - [value]: assigned value
592
   - [pp_var]: printer for variables
593
*)
594
let assign_to_exprs m var_name value =
595
  let self = m.mname.node_id in
596
  let e =
597
    Z3.Boolean.mk_eq
598
      !ctx
599
      (horn_val_to_expr ~is_lhs:true self var_name)
600
      (horn_val_to_expr self value)
601
  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
602
  in
603
  [e]
604

  
605
    
606
(* Convert instruction to Z3.Expr and update the set of reset instances *)
607
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
608
  match Corelang.get_instr_desc instr with
609
  | MComment _ -> [], reset_instances
610
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
611
    no_reset_to_exprs machines m i,
612
    i::reset_instances
613
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
614
    instance_reset_to_exprs machines m i,
615
    i::reset_instances
616
  | MLocalAssign (i,v) ->
617
    assign_to_exprs
618
      m  
619
      (mk_val (LocalVar i) i.var_type) v,
620
    reset_instances
621
  | MStateAssign (i,v) ->
622
    assign_to_exprs
623
      m 
624
      (mk_val (StateVar i) i.var_type) v,
625
    reset_instances
626
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
627
    assert false (* This should not happen anymore *)
628
  | MStep (il, i, vl) ->
629
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
630
       mem_c and print the call to mem_m *)
631
    instance_call_to_exprs machines reset_instances m i vl il,
632
    reset_instances (* Since this instance call will only happen once, we
633
		       don't have to update reset_instances *)
634

  
635
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
636
			 should not be produced yet. Later, we will have to
637
			 compare the reset_instances of each branch and
638
			 introduced the mem_m = mem_c for branches to do not
639
			 address it while other did. Am I clear ? *)
640
    (* For each branch we obtain the logical encoding, and the information
641
       whether a sub node has been reset or not. If a node has been reset in one
642
       of the branch, then all others have to have the mem_m = mem_c
643
       statement. *)
644
    let self = m.mname.node_id in
645
    let branch_to_expr (tag, instrs) =
646
      let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in
647
      let e =
648
	Z3.Boolean.mk_implies !ctx
649
          (Z3.Boolean.mk_eq !ctx 
650
             (horn_val_to_expr self g)
651
	     (horn_tag_to_expr tag))
652
          branch_def in
653

  
654
      [e], branch_resets
655
	  
656
    in
657
    List.fold_left (fun (instrs, resets) b ->
658
      let b_instrs, b_resets = branch_to_expr b in
659
      instrs@b_instrs, resets@b_resets 
660
    ) ([], reset_instances) hl 
661

  
662
and instrs_to_expr machines reset_instances m instrs = 
663
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
664
  let e_list, rs = 
665
    match instrs with
666
    | [x] -> instr_to_exprs reset_instances x 
667
    | _::_ -> (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *)
668
       
669
       List.fold_left (fun (exprs, rs) i -> 
670
         let exprs_i, rs_i = instr_to_exprs rs i in
671
         exprs@exprs_i, rs@rs_i
672
       )
673
         ([], reset_instances) instrs 
674
	 
675
	 
676
    | [] -> [], reset_instances
677
  in
678
  let e = 
679
    match e_list with
680
    | [e] -> e
681
    | [] -> Z3.Boolean.mk_true !ctx
682
    | _ -> Z3.Boolean.mk_and !ctx e_list
683
  in
684
  e, rs
685

  
686
        
687
let machine_reset machines m =
688
  let locals = local_memory_vars machines m in
689
  
690
  (* print "x_m = x_c" for each local memory *)
691
  let mid_mem_def =
692
    List.map (fun v ->
693
      Z3.Boolean.mk_eq !ctx
694
	(horn_var_to_expr (rename_mid v))
695
	(horn_var_to_expr (rename_current v))
696
    ) locals
697
  in
698

  
699
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
700
     Special treatment for _arrow: _first = true
701
  *)
702

  
703
  let reset_instances =
704
    
705
    List.map (fun (id, (n, _)) ->
706
      let name = node_name n in
707
      if name = "_arrow" then (
708
	Z3.Boolean.mk_eq !ctx
709
	  (
710
	    let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
711
	    Z3.Expr.mk_const_f !ctx vdecl
712
	  )
713
	  (Z3.Boolean.mk_true !ctx)
714
	  
715
      ) else (
716
	let machine_n = get_machine machines name in 
717
	
718
	Z3.Expr.mk_app
719
	  !ctx
720
	  (get_fdecl (name ^ "_reset"))
721
	  (List.map (horn_var_to_expr)
722
	     (rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
723
	  )
724
	  
725
      )
726
    ) m.minstances
727
      
728
      
729
  in
730
  
731
  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
732
    
733
        
734

  
735
(*  TODO: empty list means true statement *)
736
let decl_machine machines m =
737
  if m.mname.node_id = Arrow.arrow_id then
738
    (* We don't do arrow function *)
739
    ()
740
  else
741
    begin
742
      let _ =
743
        List.map decl_var
744
      	  (
745
      	    (inout_vars machines m)@
746
      	      (rename_current_list (full_memory_vars machines m)) @
747
      	      (rename_mid_list (full_memory_vars machines m)) @
748
      	      (rename_next_list (full_memory_vars machines m)) @
749
      	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
750
      	  )
751
      in
752
      
753
      if is_stateless m then
754
	begin
755
	  (* Declaring single predicate *)
756
	  let vars = inout_vars machines m in
757
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars in
758
	  let horn_body, _ (* don't care for reset here *) =
759
	    instrs_to_expr
760
	      machines
761
	      ([] (* No reset info for stateless nodes *) )
762
	      m
763
	      m.mstep.step_instrs
764
	  in
765
	  let horn_head = 
766
	    Z3.Expr.mk_app
767
	      !ctx
768
	      (get_fdecl (machine_stateless_name m.mname.node_id))
769
	      (List.map (horn_var_to_expr) vars)
770
	  in
771
	  let vars = vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
772
	  match m.mstep.step_asserts with
773
	  | [] ->
774
	     begin
775
	       (* Rule for single predicate : "; Stateless step rule @." *)
776
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
777
		 
778
	     end
779
	  | assertsl ->
780
	     begin
781
	       (*Rule for step "; Stateless step rule with Assertions @.";*)
782
	       let body_with_asserts =
783
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
784
	       in
785
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
786
	     end
787
	end
788
      else
789
	begin
790

  
791
	  (* Rule for reset *)
792

  
793
	  let vars = reset_vars machines m in
794
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars in
795
	  let horn_reset_body = machine_reset machines m in	    
796
	  let horn_reset_head = 
797
	    Z3.Expr.mk_app
798
	      !ctx
799
	      (get_fdecl (machine_reset_name m.mname.node_id))
800
	      (List.map (horn_var_to_expr) vars)
801
	  in
802
	  
803
	  let _ =
804
	    add_rule vars (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
805
	      
806
	  in
807

  
808
	  (* Rule for step*)
809
	  let vars = step_vars machines m in
810
          let _ = decl_rel (machine_step_name m.mname.node_id) vars in
811
	  let horn_step_body, _ (* don't care for reset here *) =
812
	    instrs_to_expr
813
	      machines
814
	      []
815
	      m
816
	      m.mstep.step_instrs
817
	  in
818
	  let horn_step_head = 
819
	    Z3.Expr.mk_app
820
	      !ctx
821
	      (get_fdecl (machine_step_name m.mname.node_id))
822
	      (List.map (horn_var_to_expr) vars)
823
	  in
824
	  match m.mstep.step_asserts with
825
	  | [] ->
826
	     begin
827
	       (* Rule for single predicate *)
828
	       let vars = vars @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
829
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
830
		 
831
	     end
832
	  | assertsl ->
833
	     begin
834
	       (* Rule for step Assertions @.; *)
835
	       let body_with_asserts =
836
		 Z3.Boolean.mk_and !ctx
837
		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
838
	       in
839
	       let vars = vars @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
840
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
841
		 
842
	     end
843
     	       
844
	end
845
    end
846

  
847

  
848
(* Local Variables: *)
849
(* compile-command:"make -C ../.." *)
850
(* End: *)
src/tools/zustre/zustre_data.ml
1
let ctx = ref (Z3.mk_context [])
2
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx)
3

  
4

  
5
let const_sorts : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t = Hashtbl.create 13
6
let const_tags : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t = Hashtbl.create 13
7
let sort_elems : (Z3.Sort.sort, Lustre_types.ident list) Hashtbl.t = Hashtbl.create 13
8

  
9

  
10
let decls: (Lustre_types.ident, Z3.FuncDecl.func_decl) Hashtbl.t = Hashtbl.create 13
11

  
12

  
13
(* Local Variables: *)
14
(* compile-command:"make -C ../.." *)
15
(* End: *)
src/tools/zustre/zustre_verifier.ml
1

  
2
(*
3
TODO
4

  
5
A property/contract is attached to a node foo and could be analyzed
6
- while considering the exact semantics
7
- while substituting some callee by their definition (doing it incrementaly ?)
8
- the returned cex could be given at node level
9
- or while considering a main node and producing the output at the main node level
10

  
11
One can consider the following algorithm:
12
- main node foo, local node bar, with a target property/contract
13
- declare bar using only the contract of its subnodes (callee)
14
- if the property is valid, 
15
  - check the validity status of the subnode contracts used
16
    - if one is not proved, perform the analysis again (of bar contract) using
17
      the actual definition of the unproven contract
18
  - return the computed invariants with the dependencies (subcontracts assumed, subcontracts proved)
19
- if the property is invalid
20
  - check invalidity wrt to full definition of the node bar (with the actual definition of its subnodes)
21
  - return the cex
22
  - try to see if the cex (or a similar violation of the contract) is reachable from its parents 
23
    (up to main node foo)
24
    
25

  
26
Other features:
27
- check equivalence btw two nodes, provided an equivalence map on some callee
28
  (A equiv B) with map (A id equiv B id) 
29
  - substitute each callee appearing B nodes 
30

  
31
Analysis:
32
  - take a main definition, a boolean proposition, and build the collecting semantics
33
  - then check that the proposition remains valid
34

  
35
*)
36

  
37

  
38
open Zustre_common
39
open Zustre_data
40

  
41
let param_stat = ref false
42
let param_eldarica = ref false
43
let param_utvpi = ref false
44
let param_tosmt = ref false
45
let param_pp = ref false
46

  
47
let active = ref false
48

  
49
module Verifier =
50
  (struct
51
    include VerifierType.Default
52
    let name = "zustre"
53
    let options = [
54
        "-stat", Arg.Set param_stat, "print statistics";
55
        "-eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules";
56
        "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
57
        "-tosmt", Arg.Set param_tosmt, "Print low-level (possibly unreadable) SMT2 statements";
58
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
59
      ]
60
                
61
    let activate () = (
62
        active := true;
63
        Options.output := "horn";
64
      )
65
    let is_active () = !active
66

  
67
    let get_normalization_params () =
68
      (* make sure the output is "Horn" *)
69
      assert(!Options.output = "horn");
70
      Backends.get_normalization_params ()
71

  
72
    let setup_solver () =
73
      fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
74
      (* let help = Z3.Fixedpoint.get_help fp in
75
       * Format.eprintf "Fp help : %s@." help;
76
       * 
77
       * let solver =Z3.Solver.mk_solver !ctx None in
78
       * let help = Z3.Solver.get_help solver in
79
       * Format.eprintf "Z3 help : %s@." help; *)
80
      
81
      let module P = Z3.Params in
82
      let module S = Z3.Symbol in
83
      let mks = S.mk_string !ctx in
84
      let params = P.mk_params !ctx in
85

  
86
      (* self.fp.set (engine='spacer') *)
87
      P.add_symbol params (mks "engine") (mks "spacer");
88
      
89
       (* #z3.set_option(rational_to_decimal=True) *)
90
       (* #self.fp.set('precision',30) *)
91
      if !param_stat then 
92
        (* self.fp.set('print_statistics',True) *)
93
        P.add_bool params (mks "print_statistics") true;
94

  
95
      (* Dont know where to find this parameter *)
96
      (* if !param_spacer_verbose then
97
         *   if self.args.spacer_verbose: 
98
         *        z3.set_option (verbose=1) *)
99

  
100
      (* The option is not recogined*)
101
      (* self.fp.set('use_heavy_mev',True) *)
102
      (* P.add_bool params (mks "use_heavy_mev") true; *)
103
      
104
      (* self.fp.set('pdr.flexible_trace',True) *)
105
      P.add_bool params (mks "pdr.flexible_trace") true;
106

  
107
      (* self.fp.set('reset_obligation_queue',False) *)
108
      P.add_bool params (mks "spacer.reset_obligation_queue") false;
109

  
110
      (* self.fp.set('spacer.elim_aux',False) *)
111
      P.add_bool params (mks "spacer.elim_aux") false;
112

  
113
      (* if self.args.eldarica:
114
        *     self.fp.set('print_fixedpoint_extensions', False) *)
115
      if !param_eldarica then
116
        P.add_bool params (mks "print_fixedpoint_extensions") false;
117
      
118
      (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
119
      if !param_utvpi then
120
        P.add_bool params (mks "pdr.utvpi") false;
121

  
122
      (* if self.args.tosmt:
123
       *        self.log.info("Setting low level printing")
124
       *        self.fp.set ('print.low_level_smt2',True) *)
125
      if !param_tosmt then
126
        P.add_bool params (mks "print.low_level_smt2") true;
127

  
128
      (* if not self.args.pp:
129
       *        self.log.info("No pre-processing")
130
       *        self.fp.set ('xform.slice', False)
131
       *        self.fp.set ('xform.inline_linear',False)
132
       *        self.fp.set ('xform.inline_eager',False) *\) *)
133
      if !param_pp then (
134
        P.add_bool params (mks "xform.slice") false;
135
        P.add_bool params (mks "xform.inline_linear") false;
136
        P.add_bool params (mks "xform.inline_eager") false
137
      );
138
      Z3.Fixedpoint.set_parameters !fp params
139
              
140
      
141
    let run basename prog machines =
142
      let machines = Machine_code_common.arrow_machine::machines in
143
      let machines = preprocess machines in
144
      setup_solver ();
145

  
146

  
147
      (* TODO
148
	 load deps: cf print_dep in horn_backend.ml
149

  
150
      *)
151
      if false then (
152
	
153
	let queries = Z3.Fixedpoint.parse_file !fp "mini.smt2" in
154

  
155
      (* Debug instructions *)
156
      let rules_expr = Z3.Fixedpoint.get_rules !fp in
157
      Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
158
      	(Utils.fprintf_list ~sep:"@ "
159
      	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
160
      	rules_expr;
161

  
162
	let res_status = Z3.Fixedpoint.query !fp (List.hd queries )in
163
	
164
	Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)
165
      )
166
      else (
167
	
168
	
169
      decl_sorts ();
170
      
171
      List.iter (decl_machine machines) (List.rev machines);
172

  
173

  
174
      (* (\* Debug instructions *\) *)
175
      (* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
176
      (* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
177
      (* 	(Utils.fprintf_list ~sep:"@ " *)
178
      (* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
179
      (* 	rules_expr; *)
180

  
181
      if !Options.main_node <> "" then
182
      	begin
183
      	  Zustre_analyze.check machines !Options.main_node
184

  
185
      	end
186
      else
187
      	failwith "Require main node";
188
      
189
      ()
190
      )
191
	
192

  
193
  end: VerifierType.S)
194
    
195
(* Local Variables: *)
196
(* compile-command:"make -C ../.." *)
197
(* End: *)
src/tools/zustre_verifier.ml
1
open Lustre_types
2
open Machine_code_types
3
open Machine_code_common
4
open Format
5
(* open Horn_backend_common
6
 * open Horn_backend *)
7

  
8
module HBC = Horn_backend_common
9
let machine_step_name = HBC.machine_step_name
10
let node_name = HBC.node_name
11
let concat = HBC.concat
12
let rename_machine = HBC.rename_machine
13
let rename_machine_list = HBC.rename_machine_list
14
let rename_next = HBC.rename_next
15
let rename_current = HBC.rename_current
16
let rename_current_list = HBC.rename_current_list
17
let rename_mid_list = HBC.rename_mid_list
18
let rename_next_list = HBC.rename_next_list
19
let full_memory_vars = HBC.full_memory_vars
20
let inout_vars = HBC.inout_vars
21
let reset_vars = HBC.reset_vars
22
let step_vars = HBC.step_vars
23
let local_memory_vars = HBC.local_memory_vars
24
  
25
let machine_reset_name = HBC.machine_reset_name 
26
let machine_stateless_name = HBC.machine_stateless_name 
27

  
28
let rename_mid = HBC.rename_mid
29

  
30
let preprocess = Horn_backend.preprocess
31
  
32
let active = ref false
33
let ctx = ref (Z3.mk_context [])
34
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx)
35

  
36
(** Sorts
37

  
38
A sort is introduced for each basic type and each enumerated type.
39

  
40
A hashtbl records these and allow easy access to sort values, when
41
   provided with a enumerated type name. 
42

  
43
*)
44
        
45
let bool_sort = Z3.Boolean.mk_sort !ctx
46
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
47
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
48

  
49
let const_sorts = Hashtbl.create 13
50
let const_tags = Hashtbl.create 13
51
let sort_elems = Hashtbl.create 13
52

  
53
let get_const_sort = Hashtbl.find const_sorts 
54
let get_sort_elems = Hashtbl.find sort_elems
55
let get_tag_sort = Hashtbl.find const_tags
56
  
57

  
58
  
59
let decl_sorts () =
60
  Hashtbl.iter (fun typ decl ->
61
    match typ with
62
    | Tydec_const var ->
63
      (match decl.top_decl_desc with
64
      | TypeDef tdef -> (
65
	match tdef.tydef_desc with
66
	| Tydec_enum tl ->
67
	  let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
68
          Hashtbl.add const_sorts var new_sort;
69
          Hashtbl.add sort_elems new_sort tl;
70
          List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl
71
          
72
	| _ -> Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false
73
      )
74
      | _ -> assert false
75
      )
76
    | _        -> ()) Corelang.type_table
77

  
78
                 
79
let rec type_to_sort t =
80
  if Types.is_bool_type t  then bool_sort else
81
    if Types.is_int_type t then int_sort else 
82
  if Types.is_real_type t then real_sort else 
83
  match (Types.repr t).Types.tdesc with
84
  | Types.Tconst ty       -> get_const_sort ty
85
  | Types.Tclock t        -> type_to_sort t
86
  | Types.Tarray(dim,ty)   -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
87
  | Types.Tstatic(d, ty)-> type_to_sort ty
88
  | Types.Tarrow _
89
  | _                     -> Format.eprintf "internal error: pp_type %a@."
90
                               Types.print_ty t; assert false
91

  
92
(** Func decls
93

  
94
Similarly fun_decls are registerd, by their name, into a hashtbl. The
95
   proposed encoding introduces a 0-ary fun_decl to model variables
96
   and fun_decl with arguments to declare reset and step predicates.
97

  
98

  
99

  
100
 *)
101
let decls = Hashtbl.create 13
102
let register_fdecl id fd = Hashtbl.add decls id fd
103
let get_fdecl id = Hashtbl.find decls id
104
                 
105
let decl_var id =
106
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
107
  register_fdecl id.var_id fdecl;
108
  fdecl
109

  
110
let decl_rel name args =
111
  (*verifier ce qui est construit. On veut un declare-rel *)
112
  let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in
113
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
114
  register_fdecl name fdecl;
115
  fdecl
116
  
117

  
118

  
119
(** Conversion functions
120

  
121
The following is similar to the Horn backend. Each printing function
122
   is rephrased from pp_xx to xx_to_expr and produces a Z3 value.
123

  
124
 *)
125

  
126

  
127
(* Returns the f_decl associated to the variable v *)
128
let horn_var_to_expr v =
129
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
130

  
131

  
132

  
133

  
134
  (* Used to print boolean constants *)
135
let horn_tag_to_expr t =
136
  if t = Corelang.tag_true then
137
    Z3.Boolean.mk_true !ctx
138
  else if t = Corelang.tag_false then
139
    Z3.Boolean.mk_false !ctx
140
  else
141
    (* Finding the associated sort *)
142
    let sort = get_tag_sort t in
143
    let elems = get_sort_elems sort in 
144
    let res : Z3.Expr.expr option =
145
      List.fold_left2 (fun res cst expr ->
146
          match res with
147
          | Some _ -> res
148
          | None -> if t = cst then Some (expr:Z3.Expr.expr) else None
149
        ) None elems (Z3.Enumeration.get_consts sort)
150
    in
151
    match res with None -> assert false | Some s -> s
152
    
153
(* Prints a constant value *)
154
let rec horn_const_to_expr c =
155
  match c with
156
    | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
157
    | Const_real (_,_,s)   -> Z3.Arithmetic.Real.mk_numeral_i !ctx 0
158
    | Const_tag t    -> horn_tag_to_expr t
159
    | _              -> assert false
160

  
161

  
162

  
163
(* Default value for each type, used when building arrays. Eg integer array
164
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
165
   for the type integer (arrays).
166
*)
167
let rec horn_default_val t =
168
  let t = Types.dynamic_type t in
169
  if Types.is_bool_type t  then Z3.Boolean.mk_true !ctx else
170
  if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
171
  if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
172
  (* match (Types.dynamic_type t).Types.tdesc with
173
   * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\)
174
   *    let valt = Types.array_element_type t in
175
   *    fprintf fmt "((as const (Array Int %a)) %a)"
176
   *      pp_type valt 
177
   *      pp_default_val valt
178
   * | Types.Tstruct(l) -> assert false
179
   * | Types.Ttuple(l) -> assert false
180
   * |_ -> *) assert false
181

  
182
(* Conversion of basic library functions *)
183
    
184
let horn_basic_app i val_to_expr vl =
185
  match i, vl with
186
  | "ite", [v1; v2; v3] ->
187
     Z3.Boolean.mk_ite
188
       !ctx
189
       (val_to_expr v1)
190
       (val_to_expr v2)
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff