Project

General

Profile

Revision 8c934ccd src/tools/seal/seal_extract.ml

View differences:

src/tools/seal/seal_extract.ml
1 1
open Lustre_types
2 2
open Utils
3 3
open Seal_utils			
4
open Zustre_data (* Access to Z3 context *)
5
   
4 6

  
5 7
(* Switched system extraction *)
6 8
type element = IsInit | Expr of expr
......
39 41
let select_elem elem (gelem, _) =
40 42
  is_eq_elem elem gelem
41 43

  
44

  
45
(**************************************************************)
46
(* Convert from Lustre expressions to Z3 expressions and back *)
47
(* All (free) variables have to be declared in the Z3 context *)
48
(**************************************************************)
49

  
50
let is_init_name = "__is_init"
51

  
52
let const_defs = Hashtbl.create 13
53
let is_const id = Hashtbl.mem const_defs id
54
let get_const id = Hashtbl.find const_defs id
55
                 
56
(* expressions are only basic constructs here, no more ite, tuples,
57
   arrows, fby, ... *)
58
let expr_to_z3_expr, zexpr_to_expr =
59
  (* List to store converted expression. Some expressions seem to
60
     produce segfaults in z3. Storing the processed ones may solved
61
     the issue. Using list instead of hash to ease the comparison of
62
     expressions. *)
63
  let hash = ref [] in
64
  let comp_expr e (e', _) = Corelang.is_eq_expr e e' in
65
  let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in
66
  let mem_expr e = List.exists (comp_expr e) !hash in
67
  let mem_zexpr ze = List.exists (comp_zexpr ze) !hash in
68
  let get_zexpr e =
69
    let (_, ze) = List.find (comp_expr e) !hash in
70
    ze
71
  in
72
  let get_expr ze =
73
    let (e, _) = List.find (comp_zexpr ze) !hash in
74
    e
75
  in
76
  let add_expr e ze = hash := (e, ze)::!hash in
77
  let rec e2ze e =
78
    if mem_expr e then (
79
      get_zexpr e
80
    )
81
    else (
82
      let res =
83
        match e.expr_desc with
84
        | Expr_const c ->
85
           let z3e = Zustre_common.horn_const_to_expr c in
86
           add_expr e z3e;
87
           z3e
88
        | Expr_ident id -> (
89
          if is_const id then (
90
            let c = get_const id in
91
            let z3e = Zustre_common.horn_const_to_expr c in
92
            add_expr e z3e;
93
            z3e
94
        )
95
        else (
96
          let fdecl_id = Zustre_common.get_fdecl id in
97
          let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in
98
          add_expr e z3e;
99
          z3e
100
          )
101
        )
102
      | Expr_appl (id,args, None) (* no reset *) ->
103
         let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in
104
         add_expr e z3e;
105
         z3e
106
         
107
      | _ -> assert false
108
      in
109
      res
110
    )
111
  in
112
  let rec ze2e ze =
113
    let ze_name ze =
114
      let fd = Z3.Expr.get_func_decl ze in
115
      Z3.Symbol.to_string (Z3.FuncDecl.get_name fd)
116
    in
117
    if mem_zexpr ze then
118
      None, Some (get_expr ze)
119
    else
120
      let open Corelang in
121
      let fd = Z3.Expr.get_func_decl ze in
122
      let zel = Z3.Expr.get_args ze in
123
      match Z3.Symbol.to_string (Z3.FuncDecl.get_name fd), zel with
124
      (*      | var, [] -> (* should be in env *) get_e *)
125

  
126
      (* Extracting IsInit status *)
127
      | "not", [ze] when ze_name ze = is_init_name ->
128
         Some false, None
129
      | name, [] when name = is_init_name -> Some true, None
130
      (* Other constructs are converted to a lustre expression *)
131
      | op, _ -> (
132
        
133
        
134
        if Z3.Expr.is_numeral ze then
135
          let e =
136
            if Z3.Arithmetic.is_real ze then
137
              let num =  Num.num_of_ratio (Z3.Arithmetic.Real.get_ratio ze) in
138
              let s = Z3.Arithmetic.Real.numeral_to_string ze in
139
              mkexpr
140
                Location.dummy_loc
141
                (Expr_const
142
                   (Const_real
143
                      (num, 0, s)))
144
            else if Z3.Arithmetic.is_int ze then
145
              mkexpr
146
                Location.dummy_loc
147
                (Expr_const
148
                   (Const_int
149
                      (Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int ze))))
150
            else if Z3.Expr.is_const ze then
151
              match Z3.Expr.to_string ze with
152
              | "true" -> mkexpr Location.dummy_loc
153
                            (Expr_const (Const_tag (tag_true)))
154
              | "false" ->
155
                 mkexpr Location.dummy_loc
156
                   (Expr_const (Const_tag (tag_false)))
157
              | _ -> assert false
158
            else
159
              (
160
                Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze) (Z3.Expr.is_const ze);
161
                assert false (* a numeral but no int nor real *)
162
              )
163
          in
164
          None, Some e
165
        else
166
          match op with
167
          | "not" | "=" | "-" | "*" | "/"
168
            | ">=" | "<=" | ">" | "<" 
169
            ->
170
             let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
171
             None, Some (mkpredef_call Location.dummy_loc op args)
172
          | "+" -> ( (* Special treatment of + for 2+ args *)
173
            let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
174
            let e = match args with
175
                [] -> assert false
176
              | [hd] -> hd
177
              | e1::e2::tl ->
178
                 let first_binary_and = mkpredef_call Location.dummy_loc op [e1;e2] in
179
                 if tl = [] then first_binary_and else
180
                   List.fold_left (fun e e_new ->
181
                       mkpredef_call Location.dummy_loc op [e;e_new]
182
                     ) first_binary_and tl
183
                 
184
            in
185
            None, Some e 
186
          )
187
          | "and" -> (
188
            (* Special case since it can contain is_init pred *)
189
            let args = List.map (fun ze -> ze2e ze) zel in
190
            match args with
191
            | [] -> assert false
192
            | [hd] -> hd
193
            | hd::tl ->
194
               List.fold_left
195
                 (fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) ->
196
                   (match is_init_opt1, is_init_opt2 with
197
                      None, x | x, None -> x
198
                      | Some _, Some _ -> assert false),
199
                   (match expr_opt1, expr_opt2 with
200
                    | None, x | x, None -> x
201
                    | Some e1, Some e2 ->
202
                       Some (mkpredef_call Location.dummy_loc "&&" [e1; e2])
203
                 ))
204
                 hd tl 
205
          )
206
                   
207
          | op -> 
208
             let args = List.map (fun ze ->  (snd (ze2e ze))) zel in
209
             Format.eprintf "deal with op %s (%i). Expr is %s@."  op (List.length args) (Z3.Expr.to_string ze); assert false
210
      )
211
  in
212
  (fun e -> e2ze e), (fun ze -> ze2e ze)
213

  
214
let is_init_z3e = Z3.Expr.mk_const_s !ctx is_init_name  Zustre_common.bool_sort 
215
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e 
216

  
217
(*****************************************************************)
218
(* Checking sat(isfiability) of an expression and simplifying it *)
219
(* All (free) variables have to be declared in the Z3 context    *)
220
(*****************************************************************)
221
               
222
let check_sat, clean_guard = 
223
  (
224
    fun l ->
225
    let solver = Z3.Solver.mk_simple_solver !ctx in
226
    try (
227
    let zl =
228
      List.map (fun (e, posneg) ->
229
          let ze =
230
            match e with
231
            | IsInit -> is_init_z3e
232
            | Expr e -> expr_to_z3_expr e 
233
          in
234
          if posneg then
235
            ze
236
          else
237
            neg_ze ze
238
        ) l
239
    in
240
    let status_res = Z3.Solver.check solver zl in
241
    let sat = match status_res with
242
      | Z3.Solver.UNSATISFIABLE -> false
243
      | _ -> true in
244
    sat, if not sat then [] else l
245
    )
246
    with Zustre_common.UnknownFunction(id, msg) -> (
247
      report ~level:1 msg;
248
      true, l (* keeping everything. *)
249
    )
250
      
251
  
252
  ),
253
  ( fun l ->
254
    try (
255
        let solver = Z3.Solver.mk_simple_solver !ctx in
256
     let zl =
257
    List.map (fun (e, posneg) ->
258
        let ze = expr_to_z3_expr e 
259
        in
260
        if posneg then
261
          ze
262
        else
263
          neg_ze ze
264
      ) l
265
     in
266
     let goal = Z3.Goal.mk_goal !ctx false false false in
267
     let status_res = Z3.Solver.check solver zl in
268
     Z3.Goal.add goal zl;
269
    let goal' = Z3.Goal.simplify goal None in
270
    
271
    Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@."
272
      (Z3.Goal.to_string goal)
273
      (Z3.Goal.to_string goal')
274
      (Z3.Solver.string_of_status status_res)
275
    ;
276
    let ze = Z3.Goal.as_expr goal' in
277
    Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze);
278
   (* let l =
279
      match zexpr_to_expr ze with
280
      | None, None -> []
281
      | None, Some e -> [e, true]
282
      | _ -> assert false
283
    (*      | Some init, None -> [IsInit, init]
284
      | Some init, Some e -> [IsInit, init; Expr e, true]
285
     *)  in
286
     *)
287
    l
288
    )
289
      with Zustre_common.UnknownFunction(id, msg) -> (
290
      report ~level:1 msg;
291
      l (* keeping everything. *)
292
    )
293
  )
294

  
295

  
296
(**************************************************************)
297

  
298
  
299
let clean_sys sys =
300
  List.fold_left (fun accu (guards, updates) ->
301
      let guards' = clean_guard guards in
302
      let sat, _ =  check_sat (List.map (fun (g, pn) -> Expr g, pn) guards') in
303
      (*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@."
304
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards
305
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards'
306
        sat
307

  
308
      ;*)
309
        if sat then
310
        (guards', updates)::accu
311
      else
312
        accu
313
    )
314
    [] sys
42 315
  
43 316
let combine_guards ?(fresh=None) gl1 gl2 =
44 317
  (* Filtering out trivial cases. More semantics ones would have to be
......
52 325
      status=posneg, l
53 326
    else
54 327
      (* Valid: no overlap *)
55
      true, (gexpr, posneg)::l
328
      (* Individual checkat *)
329
      let ok, e = check_sat [gexpr, posneg] in
330
      if ok then
331
        let l = e@l in
332
        let ok, l = check_sat l in
333
        ok, l 
334
      else
335
        true, l
56 336
  in
57 337
  let ok, gl =
58 338
    List.fold_left (
......
191 471
    
192 472
let split_mem_defs
193 473
      (elem: element)
194
      (mem_defs: (ident * guarded_expr list) list) :
474
      (mem_defs: (ident * guarded_expr list) list)
475
      :
195 476
      ((ident * mdef_t) list) * ((ident * mdef_t) list)
477
  
196 478
  =
197 479
  List.fold_right (fun (m,mdefs)
198 480
                       (accu_pos, accu_neg) ->
199 481
      let pos, neg =
200
        split_mdefs elem mdefs
482
        split_mdefs elem mdefs 
201 483
      in
202 484
      (m, pos)::accu_pos,
203 485
      (m, neg)::accu_neg
......
207 489
(* Split a list of mem_defs into init and step lists of guarded
208 490
   expressions per memory. *)
209 491
let split_init mem_defs =
210
  split_mem_defs IsInit mem_defs
492
  split_mem_defs IsInit mem_defs 
211 493

  
212
let pick_guard mem_defs : expr =
494
let pick_guard mem_defs : expr option =
213 495
  let gel = List.flatten (List.map snd mem_defs) in
214 496
  let gl = List.flatten (List.map fst gel) in
215 497
  let all_guards =
......
225 507
  in
226 508
  (* TODO , one could sort by occurence and provided the most common
227 509
     one *)
228
  List.hd all_guards  
229
  
510
  try
511
  Some (List.hd all_guards)  
512
  with _ -> None
230 513
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)
231 514
*)
232 515
let rec build_switch_sys
......
243 526
         (* All defs are unguarded *)
244 527
         match mdefs with
245 528
         | [[], _] -> true
246
         | _ -> false) mem_defs
529
         | _ -> false
530
       ) mem_defs
247 531
  then
248 532
    [prefix ,
249 533
     List.map (fun (m,gel) ->
......
259 543
       ) mem_defs]
260 544
  else
261 545
    (* Picking a guard *)
262
    let elem : expr = pick_guard mem_defs in
263
    let pos, neg =
264
      split_mem_defs
265
        (Expr elem)
266
        mem_defs
267
    in
268
    (* Special cases to avoid useless computations: true, false conditions *)
269
    match elem.expr_desc with
270
    | Expr_ident "true"  ->   build_switch_sys pos prefix
271
    | Expr_const (Const_tag tag) when tag = Corelang.tag_true
272
                         ->   build_switch_sys pos prefix
273
    | Expr_ident "false" ->   build_switch_sys neg prefix
274
    | Expr_const (Const_tag tag) when tag = Corelang.tag_false 
275
                         ->   build_switch_sys neg prefix
276
    | _ -> (* Regular case *)
277
       (* let _ = (
278
        *     Format.eprintf "Expr is %a@." Printers.pp_expr elem;
279
        *     match elem.expr_desc with
280
        *     | Expr_const _ -> Format.eprintf "a const@."
281
        *                     
282
        *     | Expr_ident _ -> Format.eprintf "an ident@."
283
        *     | _ -> Format.eprintf "something else@."
284
        *   )
285
        * in *)
286
       (build_switch_sys pos ((elem, true)::prefix))
287
       @
288
         (build_switch_sys neg ((elem, false)::prefix))
289
      
546
    let elem_opt : expr option = pick_guard mem_defs in
547
    match elem_opt with
548
      None -> []
549
    | Some elem -> (
550
      let pos, neg =
551
        split_mem_defs
552
          (Expr elem)
553
          mem_defs
554
      in
555
      (* Special cases to avoid useless computations: true, false conditions *)
556
      match elem.expr_desc with
557
      | Expr_ident "true"  ->   build_switch_sys pos prefix
558
      | Expr_const (Const_tag tag) when tag = Corelang.tag_true
559
        ->   build_switch_sys pos prefix
560
      | Expr_ident "false" ->   build_switch_sys neg prefix
561
      | Expr_const (Const_tag tag) when tag = Corelang.tag_false 
562
        ->   build_switch_sys neg prefix
563
      | _ -> (* Regular case *)
564
         (* let _ = (
565
          *     Format.eprintf "Expr is %a@." Printers.pp_expr elem;
566
          *     match elem.expr_desc with
567
          *     | Expr_const _ -> Format.eprintf "a const@."
568
          *                     
569
          *     | Expr_ident _ -> Format.eprintf "an ident@."
570
          *     | _ -> Format.eprintf "something else@."
571
          *   )
572
          * in *)
573
         (build_switch_sys pos ((elem, true)::prefix))
574
         @
575
           (build_switch_sys neg ((elem, false)::prefix))
576
    )
290 577

  
291 578

  
292 579
      
293 580
(* Take a normalized node and extract a list of switches: (cond,
294 581
   update) meaning "if cond then update" where update shall define all
295 582
   node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *)
296
let node_as_switched_sys (mems:var_decl list) nd =
583
let node_as_switched_sys consts (mems:var_decl list) nd =
297 584
  (* rescheduling node: has been scheduled already, no need to protect
298 585
     the call to schedule_node *)
299 586
  let nd_report = Scheduling.schedule_node nd in
......
303 590
  let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
304 591
  let defs : (ident,  guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
305 592
  let add_def = add_def defs in
306
  (* Registering node equations *)
593

  
594
  let vars = Corelang.get_node_vars nd in
595
  (* Registering all locals variables as Z3 predicates. Will be use to
596
     simplify the expansion *) 
597
  let _ =
598
    List.iter (fun v ->
599
        let fdecl = Z3.FuncDecl.mk_func_decl_s
600
                      !ctx
601
                      v.var_id
602
                      []
603
                      (Zustre_common.type_to_sort v.var_type)
604
        in
605
        ignore (Zustre_common.register_fdecl v.var_id fdecl)
606
      ) vars
607
  in
608
  let _ =
609
    List.iter (fun c -> Hashtbl.add const_defs c.const_id c.const_value) consts
610
  in
611
  
612
  (* Registering node equations: identifying mem definitions and
613
     storing others in the "defs" hashtbl. *)
307 614
  let mem_defs =
308 615
    List.fold_left (fun accu eq ->
309 616
        match eq.eq_lhs with
310 617
        | [vid] ->
311 618
           (* Only focus on non memory definitions *)
312 619
           if not (List.exists (fun v -> v.var_id = vid) mems) then (
313
             report ~level:3 (fun fmt -> Format.fprintf fmt "Registering variable %s@." vid);
620
             report ~level:3 (fun fmt ->
621
                 Format.fprintf fmt "Registering variable %s@." vid);
314 622
             add_def vid eq.eq_rhs;
315 623
             accu
316 624
           )
......
318 626
             (
319 627
               match eq.eq_rhs.expr_desc with
320 628
               | Expr_pre def_m ->
321
                  report ~level:3 (fun fmt -> Format.fprintf fmt "Preparing mem %s@." vid);
322

  
629
                  report ~level:3 (fun fmt ->
630
                      Format.fprintf fmt "Preparing mem %s@." vid);
323 631
                  (vid, rewrite defs def_m)::accu
324 632
               | _ -> assert false
325 633
             )
326 634
        | _ -> assert false (* should have been removed by normalization *)
327 635
      ) [] sorted_eqs
328 636
  in
637

  
638
  
329 639
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
330 640
  (* Printing memories definitions *)
331 641
  report ~level:3
......
341 651
                  pp_guard_expr) mdefs
342 652
        ))
343 653
        mem_defs);
654
  
344 655
  let init_defs, update_defs =
345
    split_init mem_defs
656
    split_init mem_defs 
346 657
  in
347 658
  report ~level:3
348 659
    (fun fmt ->
......
366 677
                  pp_guard_expr) mdefs
367 678
        ))
368 679
        update_defs);
680

  
369 681
  let sw_init= 
370 682
    build_switch_sys init_defs []
371 683
  in
372 684
  let sw_sys =
373 685
    build_switch_sys update_defs []
374 686
  in
375
  sw_init, sw_sys
687
  clean_sys sw_init, clean_sys sw_sys

Also available in: Unified diff