Project

General

Profile

Download (24.4 KB) Statistics
| Branch: | Tag: | Revision:
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
  register_fdecl id.var_id fdecl;
112
  fdecl
113

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

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

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

    
191

    
192
(** Conversion functions
193

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

    
197
 *)
198

    
199

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

    
204

    
205

    
206

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

    
234

    
235

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

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

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

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

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

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

    
340

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
575

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

    
586

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

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

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

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

    
661
and instrs_to_expr machines reset_instances m instrs = 
662
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
663
  let e_list, rs = 
664
    match instrs with
665
    | [x] -> instr_to_exprs reset_instances x 
666
    | _::_ -> (* 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 *)
667
       
668
       List.fold_left (fun (exprs, rs) i -> 
669
         let exprs_i, rs_i = instr_to_exprs rs i in
670
         exprs@exprs_i, rs@rs_i
671
       )
672
         ([], reset_instances) instrs 
673
	 
674
	 
675
    | [] -> [], reset_instances
676
  in
677
  let e = 
678
    match e_list with
679
    | [e] -> e
680
    | [] -> Z3.Boolean.mk_true !ctx
681
    | _ -> Z3.Boolean.mk_and !ctx e_list
682
  in
683
  e, rs
684

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

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

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

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

    
790
	  (* Rule for reset *)
791

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

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

    
846

    
847
(* Local Variables: *)
848
(* compile-command:"make -C ../.." *)
849
(* End: *)
(2-2/4)