Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_common.ml @ 5778dd5e

History | View | Annotate | Download (24.3 KB)

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: *)