Project

General

Profile

Revision 3b7f916b

View differences:

src/tools/seal/seal_extract.ml
4 4
open Zustre_data (* Access to Z3 context *)
5 5
   
6 6

  
7
(* Switched system extraction *)
7
(* Switched system extraction: expression are memoized *)
8
(*let expr_mem = Hashtbl.create 13*)
9
             
8 10
type element = IsInit | Expr of expr
11
                              
9 12
type guard = (element * bool) list
10 13
type guarded_expr = guard * element
11 14
type mdef_t = guarded_expr list
......
13 16
let pp_elem fmt e =
14 17
  match e with
15 18
  | IsInit -> Format.fprintf fmt "init"
16
  | Expr e -> Printers.pp_expr fmt e
19
  | Expr e -> Format.fprintf fmt "%a" Printers.pp_expr e 
17 20

  
18 21
let pp_guard_list fmt gl =
19 22
  (fprintf_list ~sep:"; "
......
37 40
let is_eq_elem elem elem' =
38 41
  match elem, elem' with
39 42
  | IsInit, IsInit -> true
40
  | Expr e, Expr e' ->
41
     Corelang.is_eq_expr e e'
43
  | Expr e, Expr e' -> e = e' (*
44
     Corelang.is_eq_expr e e' *)
42 45
  | _ -> false
43 46

  
44 47
let select_elem elem (gelem, _) =
......
58 61
                 
59 62
(* expressions are only basic constructs here, no more ite, tuples,
60 63
   arrows, fby, ... *)
64

  
65
(* Set of hash to support memoization *)
66
let expr_hash: (expr * Utils.tag) list ref = ref []
67
let ze_hash: (Z3.Expr.expr, Utils.tag) Hashtbl.t = Hashtbl.create 13
68
let e_hash: (Utils.tag, Z3.Expr.expr) Hashtbl.t = Hashtbl.create 13
69
let pp_hash pp_key pp_v fmt h = Hashtbl.iter (fun key v -> Format.fprintf fmt "%a -> %a@ " pp_key key pp_v v) h
70
let pp_e_map fmt = List.iter (fun (e,t) -> Format.fprintf fmt "%i -> %a@ " t Printers.pp_expr e) !expr_hash
71
let pp_ze_hash fmt = pp_hash
72
                      (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
73
                      Format.pp_print_int
74
                      fmt
75
                      ze_hash
76
let pp_e_hash fmt = pp_hash
77
                      Format.pp_print_int
78
                      (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
79
                      fmt
80
                      e_hash                              
81
let mem_expr e =
82
  (* Format.eprintf "Searching for %a in map: @[<v 0>%t@]"
83
   *   Printers.pp_expr e
84
   *   pp_e_map; *)
85
  let res = List.exists (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in
86
  (* Format.eprintf "found?%b@." res; *)
87
  res
88
  
89
let mem_zexpr ze =
90
  Hashtbl.mem ze_hash ze
91
let get_zexpr e =
92
  let eref, uid = List.find (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in
93
  (* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref eref.expr_tag; *)
94
  Hashtbl.find e_hash uid
95
let get_expr ze =
96
  let uid = Hashtbl.find ze_hash ze in
97
  let e,_ = List.find (fun (e,t) -> t = uid) !expr_hash in
98
  e
99
  
100
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e 
101
let is_init_z3e =
102
  Z3.Expr.mk_const_s !ctx is_init_name  Zustre_common.bool_sort 
103

  
104
let get_zid (ze:Z3.Expr.expr) : Utils.tag = 
105
  try
106
    if Z3.Expr.equal ze is_init_z3e then -1 else
107
      if Z3.Expr.equal ze (neg_ze is_init_z3e) then -2 else
108
    Hashtbl.find ze_hash ze
109
  with _ -> (Format.eprintf "Looking for ze %s in Hash %a"
110
               (Z3.Expr.to_string ze)
111
               (fun fmt hash -> Hashtbl.iter (fun ze uid -> Format.fprintf fmt "%s -> %i@ " (Z3.Expr.to_string ze) uid) hash ) ze_hash;
112
             assert false)
113
let add_expr =
114
  let cpt = ref 0 in
115
  fun e ze ->
116
  incr cpt;
117
  let uid = !cpt in
118
  expr_hash := (e, uid)::!expr_hash;
119
  Hashtbl.add e_hash uid ze;
120
  Hashtbl.add ze_hash ze uid
121

  
122
  
61 123
let expr_to_z3_expr, zexpr_to_expr =
62 124
  (* List to store converted expression. *)
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
125
  (* let hash = ref [] in
126
   * let comp_expr e (e', _) = Corelang.is_eq_expr e e' in
127
   * let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *)
128
  
77 129
  let rec e2ze e =
78 130
    if mem_expr e then (
79 131
      get_zexpr e
......
216 268
  in
217 269
  (fun e -> e2ze e), (fun ze -> ze2e ze)
218 270

  
219
let is_init_z3e = Z3.Expr.mk_const_s !ctx is_init_name  Zustre_common.bool_sort 
220
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e 
221

  
271
               
222 272
let zexpr_to_guard_list ze =
223 273
  let init_opt, expr_opt = zexpr_to_expr ze in
224 274
  (match init_opt with
......
228 278
       | None -> []
229 279
       | Some e -> [Expr e, true]
230 280
      )
281
                
282
               
231 283
let simplify_neg_guard l =
232 284
  List.map (fun (g,posneg) ->
233 285
      match g with
......
249 301
(* Checking sat(isfiability) of an expression and simplifying it *)
250 302
(* All (free) variables have to be declared in the Z3 context    *)
251 303
(*****************************************************************)
304
(*
252 305
let goal_simplify zl =
253 306
  let goal = Z3.Goal.mk_goal !ctx false false false in
254 307
  Z3.Goal.add goal zl;
......
260 313
   * ; *)
261 314
  let ze = Z3.Goal.as_expr goal' in
262 315
  (* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *)
263
  ze
264

  
265
let implies e1 e2 =
266
  (* Format.eprintf "Checking implication: %s => %s? "
267
   * (Z3.Expr.to_string e1) (Z3.Expr.to_string e2)
268
   * ; *)
269
  let solver = Z3.Solver.mk_simple_solver !ctx in
270
  let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx e1 e2) in
271
  try
272
    let status_res = Z3.Solver.check solver [tgt] in
273
    match status_res with
274
    | Z3.Solver.UNSATISFIABLE -> (* Format.eprintf "Valid!@."; *)
275
                                 true
276
    | _ -> (* Format.eprintf "not proved valid@."; *)
277
           false
278
  with Zustre_common.UnknownFunction(id, msg) -> (
279
    report ~level:1 msg;
280
    false
281
  )
316
  zexpr_to_guard_list ze
317
  *)
318
  
319
let implies =
320
  let ze_implies_hash : ((Utils.tag * Utils.tag), bool) Hashtbl.t  = Hashtbl.create 13 in
321
  fun ze1 ze2 ->
322
  let ze1_uid = get_zid ze1 in
323
  let ze2_uid = get_zid ze2 in
324
  if Hashtbl.mem ze_implies_hash (ze1_uid, ze2_uid) then
325
    Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid)
326
  else
327
    begin
328
       Format.eprintf "Checking implication: %s => %s? "
329
        (Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2)
330
        ; 
331
      let solver = Z3.Solver.mk_simple_solver !ctx in
332
      let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in
333
      let res =
334
        try
335
          let status_res = Z3.Solver.check solver [tgt] in
336
          match status_res with
337
          | Z3.Solver.UNSATISFIABLE -> Format.eprintf "Valid!@."; 
338
             true
339
          | _ -> Format.eprintf "not proved valid@."; 
340
             false
341
        with Zustre_common.UnknownFunction(id, msg) -> (
342
          report ~level:1 msg;
343
          false
344
        )
345
      in
346
      Hashtbl.add ze_implies_hash (ze1_uid,ze2_uid) res ;
347
      res
348
    end
282 349
                                               
283 350
let rec simplify zl =
284 351
  match zl with
285 352
  | [] | [_] -> zl
286 353
  | hd::tl -> (
287
  (* Forall e in tl, checking whether hd => e or e => hd, to keep hd
354
    (* Forall e in tl, checking whether hd => e or e => hd, to keep hd
288 355
     in the first case and e in the second one *)
289 356
    let tl = simplify tl in
290 357
    let keep_hd, tl =
......
310 377
  
311 378
let check_sat ?(just_check=false) (l:guard) : bool * guard =
312 379
  (* Syntactic simplification *)
313
  (* Format.eprintf "Before simplify: %a@." pp_guard_list l; *)
380
  if false then
381
    Format.eprintf "Before simplify: %a@." pp_guard_list l; 
314 382
  let l = simplify_neg_guard l in
315
  (* Format.eprintf "After simplify: %a@." pp_guard_list l; *)
316
  (* Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l; *)
383
  if false then (
384
    Format.eprintf "After simplify: %a@." pp_guard_list l; 
385
    Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l;
386
  );
317 387
  let solver = Z3.Solver.mk_simple_solver !ctx in
318 388
  try (
319 389
    let zl =
......
329 399
            neg_ze ze
330 400
        ) l
331 401
    in
332
    (* Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; *)
402
    if false then Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
333 403
    let zl = simplify zl in
334
       (* Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; *)
404
        if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
335 405
    let status_res = Z3.Solver.check solver zl in
336
    (* Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); *)
406
     if false then Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); 
337 407
    match status_res with
338 408
    | Z3.Solver.UNSATISFIABLE -> false, []
339 409
    | _ -> (
340 410
      if false && just_check then
341 411
        true, l
342 412
      else
343
        let zl = goal_simplify zl in
344
        let l = zexpr_to_guard_list zl in
413
        (* TODO: may be reactivate but it may create new expressions *)
414
        (* let l = goal_simplify zl in *)
415
        let l = List.fold_left
416
                  (fun accu ze -> accu @ (zexpr_to_guard_list ze))
417
                  []
418
                  zl
419
        in
345 420
  (* Format.eprintf "@.@[<v 2>Check_Sat:@ before: %a@ after:
346 421
       %a@. Goal precise? %b/%b@]@.@. " * pp_guard_list l
347 422
       pp_guard_list l' * (Z3.Goal.is_precise goal) *
......
381 456
        accu
382 457
    )
383 458
    [] sys
384
  
459

  
460
(* Most costly function: has the be efficiently implemented.  All
461
   registered guards are initially produced by the call to
462
   combine_guards. We csan normalize the guards to ease the
463
   comparisons.
464

  
465
   We assume that gl1 and gl2 are already both satisfiable and in a
466
   kind of reduced form. Let lshort and llong be the short and long
467
   list of gl1, gl2. We check whether each element elong of llong is
468
   satisfiable with lshort. If no, stop. If yes, we search to reduce
469
   the list. If elong => eshort_i, we can remove eshort_i from
470
   lshort. we can continue with this lshort shortened, lshort'; it is
471
   not necessary to add yet elong in lshort' since we already know
472
   rthat elong is somehow reduced with respect to other elements of
473
   llong. If eshort_i => elong, then we keep ehosrt_i in lshort and do
474
   not store elong.
475

  
476
   After iterating through llong, we have a shortened version of
477
   lshort + some elements of llong that have to be remembered. We add
478
   them to this new consolidated list. 
479

  
480
 *)
481

  
482
(* combine_guards ~fresh:Some(e,b) gl1 gl2 returns ok, gl with ok=true
483
   when (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated
484
   version of it.  *)
385 485
let combine_guards ?(fresh=None) gl1 gl2 =
386 486
  (* Filtering out trivial cases. More semantics ones would have to be
387 487
     addressed later *)
388
  let check (gexpr, posneg) l =
389
    (* Format.eprintf "Checking %a=%b in %a@ "
390
     *   pp_elem gexpr
391
     *   posneg
392
     *   pp_guard_list l
393
     * ; *)
394
    (* Check if gepxr is part of l *)
395
   let sel_fun = select_elem gexpr in
396
   let ok, res =
397
     if List.exists sel_fun l then (
398
      (* Checking the guard value posneg *)
399
      let _, status = List.find sel_fun l in
400
      (* Format.eprintf "Found %a in %a. @ Checking status (%b).@ "
401
     *     pp_elem gexpr
402
     *     pp_guard_list l
403
     *     (status=posneg)
404
     * ; *)
405
      status=posneg, l
406
    )
407
    else (
408
      (* Format.eprintf "Not found.@ "; *)
409
      (* Valid: no overlap *)
410
      (* Individual checkat *)
411
      let ok, e = check_sat ~just_check:true [gexpr, posneg] in
412
      (* let ok, e = true, [gexpr, posneg] in (* TODO solve the issue with check_sat *) *)
413
      (* Format.eprintf "Check_sat? %b@ " ok; *)
414
      if ok then
415
        let l = e@l in
416
        let ok, l = check_sat ~just_check:true l in
417
        (* let ok, l = true, l in (* TODO solve the issue with check_sat *) *)
418
        ok, l 
419
      else
420
        false, []
421
     )
422
   in
423
   (* Format.eprintf "Check sat res: %a@ "
424
    *   pp_guard_list res; *)
425
   ok, res
488
  let check_sat e = (* temp function before we clean the original one *)
489
    let ok, _ = check_sat e in
490
    ok
426 491
  in
427
  let ok, gl =
428
    List.fold_left (
429
        fun (ok, l) g ->
430
        (* Bypass for negative output *)
431
        if not ok then false, []
492
  let implies (e1,pn1) (e2,pn2) =
493
    let e2z e pn =
494
      match e with
495
        | IsInit -> if pn then is_init_z3e else neg_ze is_init_z3e
496
        | Expr e -> expr_to_z3_expr (if pn then e else (Corelang.push_negations ~neg:true e))
497
      in
498
    implies (e2z e1 pn1) (e2z e2 pn2)
499
  in
500
  let lshort, llong =
501
    if List.length gl1 > List.length gl2 then gl2, gl1 else gl1, gl2
502
  in
503
  let merge long short =
504
    let short, long_sel, ok = 
505
    List.fold_left (fun (short,long_sel, ok) long_e ->
506
        if not ok then
507
          [],[], false (* Propagating unsat case *)
508
        else if check_sat (long_e::short) then
509
          let short, keep_long_e =
510
            List.fold_left (fun (accu_short, keep_long_e) eshort_i ->
511
                if not keep_long_e then (* shorten the algo *)
512
                  eshort_i :: accu_short, false
513
                else (* keep_long_e = true in the following *)
514
                  if implies eshort_i long_e then
515
                    (* First case is trying to remove long_e!
516

  
517
                     Since short is already normalized, we can remove
518
                     long_e. If later long_e is stronger than another
519
                     element of short, then necessarily eshort_i =>
520
                     long_e ->
521
                     that_other_element_of_short. Contradiction. *)
522
                    eshort_i::accu_short, false
523
                  else if implies long_e eshort_i then 
524
                    (* removing eshort_i, keeping long_e. *)
525
                    accu_short, true
526
                  else (* Not comparable, keeping both *)
527
                    eshort_i::accu_short, true
528
              )
529
              ([],true) (* Initially we assume that we will keep long_e *)
530
              short
531
          in
532
          if keep_long_e then
533
            short, long_e::long_sel, true
534
          else
535
            short, long_sel, true
432 536
        else
433
          check g l 
434
      ) (true, gl2) gl1
537
          [],[],false
538
      ) (short, [], true) long
539
    in
540
    ok, long_sel@short
435 541
  in
436
  if ok then
437
    match fresh with
438
      None -> true, gl
439
    | Some fresh_g -> (
440
    (* Checking the fresh element *)
441
      check fresh_g gl
442
    )
443
  else
542
  let ok, l = match fresh with
543
    | None -> true, []
544
    | Some g -> merge [g] []
545
  in
546
  if not ok then
444 547
    false, []
548
  else
549
    let ok, lshort = merge lshort l in
550
    if not ok then
551
      false, []
552
    else
553
      merge llong lshort
554
    
445 555

  
446
(* DEBUG 
447
let combine_guards  ?(fresh=None) gl1 gl2 =
448
  true,
449
  (match fresh with None -> [] | Some (gexpr, posneg) -> [gexpr, posneg])@gl1@gl2
450
 *)
451 556
(* Encode "If gel1=posneg then gel2":
452 557
   - Compute the combination of guarded exprs in gel1 and gel2:
453 558
     - Each guarded_expr in gel1 is transformed as a guard: the
......
456 561
     - We keep expr in the ge of gel2 as the legitimate expression 
457 562
 *)
458 563
let concatenate_ge gel1 posneg gel2 =
459
  List.fold_left (
460
      fun accu (g2,e2) ->
461
      List.fold_left (
462
          fun accu (g1,e1) ->
463
           (* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ "
464
            *  pp_elem e1
465
            *  posneg
466
            *  pp_guard_list g1
467
            *  pp_guard_list g2; *)
468
            
469
          let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in
470
          (* Format.eprintf "@]@ Result is [%a]@ "
471
           *   pp_guard_list gl; *)
472
            
473
          if ok then
474
            (gl, e2)::accu
475
          else (
476
            
477
            accu
478
          )
479
        ) accu gel1
480
    ) [] gel2
481

  
564
  let l, all_invalid =
565
    List.fold_left (
566
        fun (accu, all_invalid) (g2,e2) ->
567
        List.fold_left (
568
            fun (accu, all_invalid) (g1,e1) ->
569
            (* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ "
570
             *  pp_elem e1
571
             *  posneg
572
             *  pp_guard_list g1
573
             *  pp_guard_list g2; *)
574

  
575
            let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in
576
            (* Format.eprintf "@]@ Result is [%a]@ "
577
             *   pp_guard_list gl; *)
578

  
579
            if ok then
580
              (gl, e2)::accu, false
581
            else (
582
              accu, all_invalid
583
            )
584
          ) (accu, all_invalid) gel1
585
      ) ([], true) gel2
586
  in
587
  not all_invalid, l
588
     
589
(* Rewrite the expression expr, replacing any occurence of a variable
590
   by its definition.
591
*)
482 592
let rec rewrite defs expr : guarded_expr list =
483 593
  let rewrite = rewrite defs in
484 594
  let res =
......
500 610
       let g = rewrite g and
501 611
           e1 = rewrite e1 and
502 612
           e2 = rewrite e2 in
503
       (concatenate_ge g true e1)@
504
         (concatenate_ge g false e2)
613
       let ok_then, g_then = concatenate_ge g true e1 in
614
       let ok_else, g_else = concatenate_ge g false e2 in
615
       (if ok_then then g_then else [])@
616
         (if ok_else then g_else else [])
505 617
    | Expr_merge (g, branches) ->
506 618
       assert false (* TODO: deal with merges *)
507 619
      
......
611 723
let split_init mem_defs =
612 724
  split_mem_defs IsInit mem_defs 
613 725

  
614
let pick_guard mem_defs : expr option =
726
(* Previous version of the function: way too costly 
727
let pick_guard mem_defs : expr option =  
615 728
  let gel = List.flatten (List.map snd mem_defs) in
616 729
  let gl = List.flatten (List.map fst gel) in
617 730
  let all_guards =
......
630 743
  try
631 744
  Some (List.hd all_guards)  
632 745
  with _ -> None
746
   *)
747

  
748
(* Returning the first non empty guard expression *)
749
let rec pick_guard mem_defs : expr option =
750
  match mem_defs with
751
  | [] -> None
752
  | (_, gel)::tl -> (
753
    let found =
754
      List.fold_left (fun found (g,_) ->
755
          if found = None then
756
            match g with
757
            | [] -> None
758
            | (Expr e, _)::_ -> Some e
759
            | (IsInit, _)::_ -> assert false (* should be removed already *)
760
          else
761
            found
762
        ) None gel
763
    in
764
    if found = None then pick_guard tl else found
765
  )
766
          
767

  
633 768
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)
634 769
*)
635 770
let rec build_switch_sys
......
698 833
           ok, l
699 834
         in
700 835
         let pos_prefix = (elem, true)::prefix in
701
         let ok_pos, pos_prefix = clean pos_prefix in         
702 836
         let neg_prefix = (elem, false)::prefix in
837
         Format.eprintf "Pos_prefix: %a@.Neg_prefix: %a@."
838
           pp_guard_list (List.map (fun (e,b) -> Expr e ,b) pos_prefix)
839
           pp_guard_list (List.map (fun (e,b) -> Expr e ,b) neg_prefix);
840
         let ok_pos, pos_prefix = clean pos_prefix in         
703 841
         let ok_neg, neg_prefix = clean neg_prefix in         
704
         
842
         Format.eprintf "Pos_prefix: %b %a@.Neg_prefix: %b %a@."
843
           ok_pos pp_guard_list (List.map (fun (e,b) -> Expr e ,b) pos_prefix)
844
           ok_neg pp_guard_list (List.map (fun (e,b) -> Expr e ,b) neg_prefix);
705 845
         (if ok_pos then build_switch_sys pos pos_prefix else [])
706 846
         @
707 847
           (if ok_neg then build_switch_sys neg neg_prefix else [])
......
743 883

  
744 884
  
745 885
  (* Registering node equations: identifying mem definitions and
746
     storing others in the "defs" hashtbl. *)
886
     storing others in the "defs" hashtbl.
887

  
888
     Each assign is stored in a hash tbl as list of guarded
889
     expressions. The memory definition is also "rewritten" as such a
890
     list of guarded assigns.  *)
747 891
  let mem_defs =
748 892
    List.fold_left (fun accu eq ->
749 893
        match eq.eq_lhs with

Also available in: Unified diff