Project

General

Profile

Revision 03c767b1 src/tools/seal/seal_extract.ml

View differences:

src/tools/seal/seal_extract.ml
6 6

  
7 7
(* Switched system extraction: expression are memoized *)
8 8
(*let expr_mem = Hashtbl.create 13*)
9
             
10
type element = IsInit | Expr of expr
11
                              
12
type guard = (element * bool) list
13
type guarded_expr = guard * element
14
type mdef_t = guarded_expr list
15

  
16
let pp_elem fmt e =
17
  match e with
18
  | IsInit -> Format.fprintf fmt "init"
19
  | Expr e -> Format.fprintf fmt "%a" Printers.pp_expr e 
20

  
21
let pp_guard_list fmt gl =
22
  (fprintf_list ~sep:"; "
23
     (fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl
24
  
25
let pp_guard_expr fmt (gl,e) =
26
  Format.fprintf fmt "%a -> %a"
27
    pp_guard_list  gl
28
    pp_elem e
29

  
30
let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel
31

  
32
  
9
    
33 10
let add_init defs vid =
34 11
  Hashtbl.add defs vid [[], IsInit]
35 12

  
36
let deelem e =  match e with
37
    Expr e -> e
38
  | IsInit -> assert false (* Wasn't expecting isinit here: we are building values! *)
39

  
40
let is_eq_elem elem elem' =
41
  match elem, elem' with
42
  | IsInit, IsInit -> true
43
  | Expr e, Expr e' -> e = e' (*
44
     Corelang.is_eq_expr e e' *)
45
  | _ -> false
46

  
47
let select_elem elem (gelem, _) =
48
  is_eq_elem elem gelem
49

  
50 13

  
51 14
(**************************************************************)
52 15
(* Convert from Lustre expressions to Z3 expressions and back *)
......
325 288
    Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid)
326 289
  else
327 290
    begin
328
      if !debug then (
329
        Format.eprintf "Checking implication: %s => %s? "
291
      if !seal_debug then (
292
        report ~level:6 (fun fmt -> Format.fprintf fmt "Checking implication: %s => %s?@ "
330 293
          (Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2)
331
      ); 
294
      )); 
332 295
      let solver = Z3.Solver.mk_simple_solver !ctx in
333 296
      let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in
334 297
      let res =
335 298
        try
336 299
          let status_res = Z3.Solver.check solver [tgt] in
337 300
          match status_res with
338
          | Z3.Solver.UNSATISFIABLE -> if !debug then Format.eprintf "Valid!@."; 
301
          | Z3.Solver.UNSATISFIABLE -> if !seal_debug then
302
                                         report ~level:6 (fun fmt -> Format.fprintf fmt "Valid!@ "); 
339 303
             true
340
          | _ -> if !debug then Format.eprintf "not proved valid@."; 
304
          | _ -> if !seal_debug then report ~level:6 (fun fmt -> Format.fprintf fmt "not proved valid@ "); 
341 305
             false
342 306
        with Zustre_common.UnknownFunction(id, msg) -> (
343 307
          report ~level:1 msg;
......
376 340
      tl
377 341
  )
378 342
  
379
let check_sat ?(just_check=false) (l:guard) : bool * guard =
343
let check_sat ?(just_check=false) (l: elem_boolexpr guard) : bool * (elem_boolexpr guard) =
380 344
  (* Syntactic simplification *)
381 345
  if false then
382
    Format.eprintf "Before simplify: %a@." pp_guard_list l; 
346
    Format.eprintf "Before simplify: %a@." (pp_guard_list pp_elem) l; 
383 347
  let l = simplify_neg_guard l in
384 348
  if false then (
385
    Format.eprintf "After simplify: %a@." pp_guard_list l; 
386
    Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l;
349
    Format.eprintf "After simplify: %a@." (pp_guard_list pp_elem) l; 
350
    Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " (pp_guard_list pp_elem)l;
387 351
  );
388 352
  let solver = Z3.Solver.mk_simple_solver !ctx in
389 353
  try (
......
589 553
(* Rewrite the expression expr, replacing any occurence of a variable
590 554
   by its definition.
591 555
*)
592
let rec rewrite defs expr : guarded_expr list =
556
let rec rewrite defs expr : elem_guarded_expr list =
593 557
  let rewrite = rewrite defs in
594 558
  let res =
595 559
    match expr.expr_desc with
......
623 587
       (* Each expr is associated to its flatten guarded expr list *)
624 588
       let gell = List.map rewrite el in
625 589
       (* Computing all combinations: we obtain a list of guarded tuple *)
626
       let rec aux gell : (guard * expr list) list =
590
       let rec aux gell : (elem_boolexpr guard * expr list) list =
627 591
         match gell with
628 592
         | [] -> assert false (* Not happening *)
629 593
         | [gel] -> List.map (fun (g,e) -> g, [deelem e]) gel
......
635 599
                    fun accu (gl, minituple) ->
636 600
                    let is_compat, guard_comb = combine_guards g gl in
637 601
                    if is_compat then
638
                      let new_gt : guard * expr list = (guard_comb, (deelem e)::minituple) in
602
                      let new_gt : elem_boolexpr guard * expr list = (guard_comb, (deelem e)::minituple) in
639 603
                      new_gt::accu
640 604
                    else
641 605
                      accu
......
677 641
returns the same list of ge splited into the ones where the guard is true and the ones where it is false. In both lists the associated ge do not mention that guard anymore.
678 642

  
679 643
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *)
680
let split_mdefs elem (mdefs: guarded_expr list) =
644
let split_mdefs elem (mdefs: elem_guarded_expr list) =
681 645
  List.fold_left (
682 646
      fun (selected, left_out)
683 647
          ((guards, expr) as ge) ->
......
696 660
      | _ -> (
697 661
        Format.eprintf "@.Spliting list on elem %a.@.List:%a@."
698 662
          pp_elem elem
699
          pp_mdefs mdefs;
663
          (pp_mdefs pp_elem) mdefs;
700 664
        assert false (* more then one element selected. Should
701 665
                          not happen , or trival dead code like if
702 666
                              x then if not x then dead code *)
......
705 669
    
706 670
let split_mem_defs
707 671
      (elem: element)
708
      (mem_defs: (ident * guarded_expr list) list)
672
      (mem_defs: (ident * elem_guarded_expr list) list)
709 673
      :
710
      ((ident * mdef_t) list) * ((ident * mdef_t) list)
674
      ((ident * elem_guarded_expr mdef_t) list) * ((ident * elem_guarded_expr mdef_t) list)
711 675
  
712 676
  =
713 677
  List.fold_right (fun (m,mdefs)
......
770 734
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)
771 735
*)
772 736
let rec build_switch_sys
773
          (mem_defs : (Utils.ident * guarded_expr list) list )
737
          (mem_defs : (Utils.ident * elem_guarded_expr list) list )
774 738
          prefix
775 739
        :
776 740
          ((expr * bool) list * (ident * expr) list ) list =
777
  if !debug then
778
    Format.eprintf "Build_switch with %a@."
741
  if !seal_debug then
742
    report ~level:4 (fun fmt -> Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@."
779 743
      (Utils.fprintf_list ~sep:",@ "
780
         (fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a@ ]@]"
744
         (fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]"
781 745
                                 id
782
                                 pp_mdefs gel))
783
      mem_defs;
746
                                 (pp_mdefs pp_elem) gel))
747
      mem_defs);
784 748
  (* if all mem_defs have empty guards, we are done, return prefix,
785 749
     mem_defs expr.
786 750

  
787 751
     otherwise pick a guard in one of the mem, eg (g, b) then for each
788 752
     other mem, one need to select the same guard g with the same
789 753
     status b, *)
754
  let res =
790 755
  if List.for_all (fun (m,mdefs) ->
791 756
         (* All defs are unguarded *)
792 757
         match mdefs with
......
810 775
    (* Picking a guard *)
811 776
    let elem_opt : expr option = pick_guard mem_defs in
812 777
    match elem_opt with
813
      None -> []
778
      None -> assert false (* Otherwise the first case should have matched *)
814 779
    | Some elem -> (
780
      report ~level:4 (fun fmt -> Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem);
815 781
      let pos, neg =
816 782
        split_mem_defs
817 783
          (Expr elem)
......
844 810
         let pos_prefix = (elem, true)::prefix in
845 811
         let neg_prefix = (elem, false)::prefix in
846 812
         let ok_pos, pos_prefix = clean pos_prefix in         
847
         let ok_neg, neg_prefix = clean neg_prefix in         
848
         (if ok_pos then build_switch_sys pos pos_prefix else [])
849
         @
850
           (if ok_neg then build_switch_sys neg neg_prefix else [])
813
         let ok_neg, neg_prefix = clean neg_prefix in
814
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing %a@." Printers.pp_expr elem);
815
         let ok_l = if ok_pos then build_switch_sys pos pos_prefix else [] in
816
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing not(%a)@." Printers.pp_expr elem);
817
         let nok_l = if ok_neg then build_switch_sys neg neg_prefix else [] in
818
         ok_l @ nok_l
851 819
    )
852

  
820
  in
821
    if !seal_debug then (
822
      report ~level:4 (fun fmt ->
823
          Format.fprintf fmt
824
            "@[<v 2>===> @[%t@ @]@]@ @]@ "
825
            (fun fmt -> List.iter (fun (gl,up) ->
826
                            Format.fprintf fmt "[@[%a@]] -> (%a)@ "
827
                              (pp_guard_list Printers.pp_expr) gl pp_up up) res);
828
          
829
    ));
830
    res
831
  
853 832

  
854 833
      
855 834
(* Take a normalized node and extract a list of switches: (cond,
......
863 842
  let eqs, auts = Corelang.get_node_eqs nd in
864 843
  assert (auts = []); (* Automata should be expanded by now *)
865 844
  let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
866
  let defs : (ident,  guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
845
  let defs : (ident,  elem_guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
867 846
  let add_def = add_def defs in
868 847

  
869 848
  let vars = Corelang.get_node_vars nd in
......
910 889
                 Format.fprintf fmt "Output variable %s@." vid);
911 890
             add_def vid eq.eq_rhs;
912 891
             accu_mems, (vid, rewrite defs eq.eq_rhs)::accu_outputs
913
          
892
             
914 893
           )
915 894
           else
916 895
             (
917
             report ~level:3 (fun fmt ->
918
                 Format.fprintf fmt "Registering variable %s@." vid);
919
             add_def vid eq.eq_rhs;
920
             accu_mems, accu_outputs
921
           )
896
               report ~level:3 (fun fmt ->
897
                   Format.fprintf fmt "Registering variable %s@." vid);
898
               add_def vid eq.eq_rhs;
899
               accu_mems, accu_outputs
900
             )
922 901
        | _ -> assert false (* should have been removed by normalization *)
923 902
      ) ([], []) sorted_eqs
924 903
  in
......
929 908
  report ~level:3
930 909
    (fun fmt ->
931 910
      Format.fprintf fmt
932
        "@[<v 0>%a@]@ "
911
        "@[<v 0>%a@]@."
933 912
        (Utils.fprintf_list ~sep:"@ "
934 913
           (fun fmt (m,mdefs) ->
935 914
             Format.fprintf fmt
936 915
               "%s -> [@[<v 0>%a@] ]@ "
937 916
               m
938 917
               (Utils.fprintf_list ~sep:"@ "
939
                  pp_guard_expr) mdefs
918
                  (pp_guard_expr pp_elem)) mdefs
940 919
        ))
941 920
        mem_defs);
942 921
  (* Format.eprintf "Split init@."; *)
......
949 928
  report ~level:3
950 929
    (fun fmt ->
951 930
      Format.fprintf fmt
952
        "@[<v 0>Init:@ %a@ Step@ %a@]@ "
931
        "@[<v 0>Init:@ %a@]@."
953 932
        (Utils.fprintf_list ~sep:"@ "
954 933
           (fun fmt (m,mdefs) ->
955 934
             Format.fprintf fmt
956 935
               "%s -> @[<v 0>[%a@] ]@ "
957 936
               m
958 937
               (Utils.fprintf_list ~sep:"@ "
959
                  pp_guard_expr) mdefs
938
                  (pp_guard_expr pp_elem)) mdefs
960 939
        ))
961
        init_defs
940
        init_defs);
941
  report ~level:3
942
    (fun fmt ->
943
      Format.fprintf fmt
944
        "@[<v 0>Step:@ %a@]@."
962 945
        (Utils.fprintf_list ~sep:"@ "
963 946
           (fun fmt (m,mdefs) ->
964 947
             Format.fprintf fmt
965 948
               "%s -> @[<v 0>[%a@] ]@ "
966 949
               m
967 950
               (Utils.fprintf_list ~sep:"@ "
968
                  pp_guard_expr) mdefs
951
                  (pp_guard_expr pp_elem)) mdefs
969 952
        ))
970 953
        update_defs);
971 954
  (* Format.eprintf "Build init@."; *)
972

  
955
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init@.");
973 956
  let sw_init= 
974 957
    build_switch_sys init_defs []
975 958
  in
976 959
  (* Format.eprintf "Build step@."; *)
960
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step@.");
977 961
  let sw_sys =
978 962
    build_switch_sys update_defs []
979 963
  in
980 964

  
965
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init out@.");
981 966
  let init_out =
982 967
    build_switch_sys init_out []
983 968
  in
969
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step out@.");
970

  
984 971
  let update_out =
985 972
    build_switch_sys update_out []
986 973
  in
......
991 978
  let update_out = clean_sys update_out in
992 979

  
993 980
  (* Some additional checks *)
994
  let pp_gl pp_expr =
995
    fprintf_list ~sep:", " (fun fmt (e,b) -> Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e)
996
  in
997
  let pp_gl_short = pp_gl (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) in
998
  let pp_up fmt up = List.iter (fun (id,e) -> Format.fprintf fmt "%s->%i; " id e.expr_tag) up in
999 981
  
1000 982
  if false then
1001 983
    begin
......
1070 1052
  
1071 1053

  
1072 1054
  (* Iter through the elements and gather them by updates *)
1073
  let module UpMap =
1074
    struct
1075
      include Map.Make (
1076
                  struct
1077
                    type t = (ident * expr) list
1078
                    let compare l1 l2 =
1079
                      let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in
1080
                      compare (proj l1) (proj l2) 
1081
                  end)
1082
      let pp = pp_up 
1083
    end
1084
  in
1085
  let module Guards = struct
1086
      include Set.Make (
1087
                  struct
1088
                    type t = (expr * bool) 
1089
                    let compare l1 l2 =
1090
                      let proj (e,b) = e.expr_tag, b in
1091
                      compare (proj l1) (proj l2) 
1092
                  end)
1093
      let pp_short fmt s = pp_gl_short fmt (elements s)
1094
      let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s)
1095
    end
1096
  in
1097 1055
  let process sys =
1098 1056
    (* The map will associate to each update up the pair (set, set
1099 1057
       list) where set is the share guards and set list a list of
1100 1058
       disjunctive guards. Each set represents a conjunction of
1101 1059
       expressions. *)
1102
    let map = 
1060
    report ~level:3 (fun fmt -> Format.fprintf fmt "%t@."
1061
                                  (fun fmt -> List.iter (fun (gl,up) ->
1062
                                                  Format.fprintf fmt "[@[%a@]] -> (%a)@ "
1063
                                                    (pp_guard_list Printers.pp_expr) gl pp_up up) sw_init));
1064
    
1065
    (* We perform multiple pass to avoid errors *)
1066
    let map =
1103 1067
      List.fold_left (fun map (gl,up) ->
1104 1068
          (* creating a new set to describe gl *)
1105 1069
          let new_set =
......
1110 1074
          in
1111 1075
          (* updating the map with up -> new_set *)
1112 1076
          if UpMap.mem up map then
1113
            let (shared, disj) = UpMap.find up map in
1114
            let new_shared = Guards.inter shared new_set in
1115
            let remaining_shared = Guards.diff shared new_shared in
1116
            let remaining_new_set = Guards.diff new_set new_shared in
1117
            (* Adding remaining_shared to all elements of disj *)
1118
            let disj' = List.map (fun gs -> Guards.union remaining_shared gs) disj in
1119
            UpMap.add up (new_shared, remaining_new_set::disj') map
1077
            let guard_set = UpMap.find up map in
1078
            UpMap.add up (new_set::guard_set) map
1120 1079
          else
1121
            UpMap.add up (new_set, []) map
1080
            UpMap.add up [new_set] map
1122 1081
        ) UpMap.empty sys
1123 1082
    in
1124
     let rec mk_binop op l = match l with
1125
         [] -> assert false
1126
       | [e] -> e
1127
       | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl]
1128
    in
1129
    let gl_as_expr gl =
1130
      let gl = Guards.elements gl in
1131
      let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in 
1132
      match gl with
1133
        [] -> []
1134
      | [e] -> [export e]
1135
      | _ ->
1136
         [mk_binop "&&"
1137
            (List.map export gl)]
1083
    (* Processing the set of guards leading to the same update: return
1084
       conj, disj with conf is a set of guards, and disj a DNF, ie a
1085
       list of set of guards *)
1086
    let map =
1087
      UpMap.map (
1088
          fun guards ->
1089
          match guards with
1090
          | [] -> Guards.empty, [] (* Nothing *)
1091
          | [s]-> s, [] (* basic case *)
1092
          | hd::tl ->
1093
             let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in
1094
             let remaining = List.map (fun s -> Guards.diff s shared) guards in
1095
             (* If one of them is empty, we can remove the others, otherwise keep them *)
1096
             if List.exists Guards.is_empty remaining then
1097
               shared, []
1098
             else
1099
               shared, remaining
1100
        ) map
1138 1101
    in
1139
    let rec clean_disj disj =
1140
      match disj with
1141
      | [] | [_] -> [] 
1142
      | _::_::_ -> (
1143
        (* First basic version: producing a DNF One can later, (1)
1102
  let rec mk_binop op l = match l with
1103
      [] -> assert false
1104
    | [e] -> e
1105
    | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl]
1106
  in
1107
  let gl_as_expr gl =
1108
    let gl = Guards.elements gl in
1109
    let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in 
1110
    match gl with
1111
      [] -> []
1112
    | [e] -> [export e]
1113
    | _ ->
1114
       [mk_binop "&&"
1115
          (List.map export gl)]
1116
  in
1117
  let rec clean_disj disj =
1118
    match disj with
1119
    | [] -> []
1120
    | [_] -> assert false (* A disjunction was a single case can be ignored *) 
1121
    | _::_::_ -> (
1122
      (* First basic version: producing a DNF One can later, (1)
1144 1123
           simplify it with z3, or (2) build the compact tree with
1145 1124
           maximum shared subexpression (and simplify it with z3) *)
1146
        let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in
1147
        let or_expr = mk_binop "||" elems in
1148
        [or_expr]
1125
      let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in
1126
      let or_expr = mk_binop "||" elems in
1127
      [or_expr]
1149 1128

  
1150 1129

  
1151
         (* TODO disj*)
1152
      (* get the item that occurs in most case *)
1153
      (* List.fold_left (fun accu s ->
1154
       *     List.fold_left (fun accu (e,b) ->
1155
       *         if List.mem_assoc (e.expr_tag, b)
1156
       *       ) accu (Guards.elements s)
1157
       *   ) [] disj *)
1130
    (* TODO disj*)
1131
    (* get the item that occurs in most case *)
1132
    (* List.fold_left (fun accu s ->
1133
     *     List.fold_left (fun accu (e,b) ->
1134
     *         if List.mem_assoc (e.expr_tag, b)
1135
     *       ) accu (Guards.elements s)
1136
     *   ) [] disj *)
1158 1137

  
1159
      )
1138
    )
1139
  in
1140
  if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map);
1141
  UpMap.fold (fun up (common, disj) accu ->
1142
      if !seal_debug then
1143
        Format.eprintf
1144
          "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1145
          Guards.pp_short common
1146
          (fprintf_list ~sep:";@ " Guards.pp_long) disj
1147
          UpMap.pp up;
1148
      let disj = clean_disj disj in
1149
      let guard_expr = (gl_as_expr common)@disj in
1150
      
1151
      ((match guard_expr with
1152
        | [] -> None 
1153
        | _ -> Some (mk_binop "&&" guard_expr)), up)::accu
1154
    ) map []
1155
  
1160 1156
    in
1161
    if !debug then Format.eprintf "Map: %i elements@." (UpMap.cardinal map);
1162
    UpMap.fold (fun up (common, disj) accu ->
1163
        if !debug then
1164
          Format.eprintf
1165
            "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1166
            Guards.pp_short common
1167
            (fprintf_list ~sep:";@ " Guards.pp_long) disj
1168
            UpMap.pp up;
1169
        let disj = clean_disj disj in
1170
        let guard_expr = (gl_as_expr common)@disj in
1171
        
1172
        ((match guard_expr with
1173
         | [] -> None
1174
         | _ -> Some (mk_binop "&&" guard_expr)), up)::accu
1175
      ) map []
1176 1157
    
1177
  in
1178
  process sw_init, process sw_sys, process init_out, process update_out
1158
    
1159
    
1160
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@.");
1161
    let sw_init = process sw_init in
1162
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@.");
1163
    let sw_sys = process sw_sys in
1164
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@.");
1165
    let init_out = process init_out in
1166
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@.");
1167
    let update_out = process update_out in
1168
    sw_init , sw_sys, init_out, update_out

Also available in: Unified diff