Project

General

Profile

Revision a0c92fa8 src/tools/seal/seal_extract.ml

View differences:

src/tools/seal/seal_extract.ml
91 91
   * let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *)
92 92
  
93 93
  let rec e2ze e =
94
    (* Format.eprintf "e2ze %a: %a@." Printers.pp_expr e Types.print_ty e.expr_type; *)
94 95
    if mem_expr e then (
95 96
      get_zexpr e
96 97
    )
......
121 122
          )
122 123
        )
123 124
        | Expr_appl (id,args, None) (* no reset *) ->
124
           let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in
125
           let el = Corelang.expr_list_of_expr args in
126
           
127
           let eltyp = List.map (fun e -> e.expr_type) el in
128
           let elv = List.map e2ze el in
129
           let z3e = Zustre_common.horn_basic_app id elv (eltyp, e.expr_type) in
125 130
           add_expr e z3e;
126 131
           z3e
127 132
        | Expr_tuple [e] ->
......
597 602
           expr.expr_loc
598 603
           (Expr_appl(id, deelem e, None))
599 604
       in
605
       let new_e = { new_e with expr_type = expr.expr_type; expr_clock = expr.expr_clock } in
600 606
       guards,
601 607
       Expr (Corelang.partial_eval new_e) 
602 608
         ) args 
......
905 911
            "@[<v 2>===> @[%t@ @]@]@ @]@ "
906 912
            (fun fmt -> List.iter (fun (gl,up) ->
907 913
                            Format.fprintf fmt "[@[%a@]] -> (%a)@ "
908
                              (pp_guard_list Printers.pp_expr) gl pp_up up) res);
914
                              (pp_guard_list Printers.pp_expr) gl (pp_up Printers.pp_expr) up) res);
909 915
          
910 916
    ));
911 917
    res
912 918
  
913 919

  
914
      
915
(* Take a normalized node and extract a list of switches: (cond,
916
   update) meaning "if cond then update" where update shall define all
917
   node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *)
918
let node_as_switched_sys consts (mems:var_decl list) nd =
919
   Z3.Params.update_param_value !ctx "timeout" "10000";
920
let build_environement  consts (mems:var_decl list) nd =
921
    
922
  Z3.Params.update_param_value !ctx "timeout" "10000";
920 923

  
921 924
 
922 925
  (* rescheduling node: has been scheduled already, no need to protect
......
1018 1021
                  (pp_guard_expr pp_elem)) mdefs
1019 1022
        ))
1020 1023
        mem_defs);
1021
  (* Format.eprintf "Split init@."; *)
1022
  let init_defs, update_defs =
1023
    split_init mem_defs 
1024
  mem_defs, output_defs 
1025

  
1026

  
1027
(* Iter through the elements and gather them by updates *)
1028
let merge_updates sys =
1029
  (* The map will associate to each update up the pair (set, set
1030
       list) where set is the share guards and set list a list of
1031
       disjunctive guards. Each set represents a conjunction of
1032
       expressions. *)
1033
  
1034
  (* We perform multiple pass to avoid errors *)
1035
  let map =
1036
    List.fold_left (fun map (gl,up) ->
1037
        (* creating a new set to describe gl *)
1038
        let new_set =
1039
          List.fold_left
1040
            (fun set g -> Guards.add g set)
1041
            Guards.empty
1042
            gl
1043
        in
1044
        (* updating the map with up -> new_set *)
1045
        if UpMap.mem up map then
1046
          let guard_set = UpMap.find up map in
1047
          UpMap.add up (new_set::guard_set) map
1048
        else
1049
          UpMap.add up [new_set] map
1050
      ) UpMap.empty sys
1024 1051
  in
1025
  let init_out, update_out =
1026
    split_init output_defs
1052

  
1053
  (* Processing the set of guards leading to the same update: return
1054
       conj, disj with conf is a set of guards, and disj a DNF, ie a
1055
       list of set of guards *)
1056
  let map =
1057
    UpMap.map (
1058
        fun guards ->
1059
        match guards with
1060
        | [] -> Guards.empty, [] (* Nothing *)
1061
        | [s]-> s, [] (* basic case *)
1062
        | hd::tl ->
1063
           let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in
1064
           let remaining = List.map (fun s -> Guards.diff s shared) guards in
1065
           (* If one of them is empty, we can remove the others, otherwise keep them *)
1066
           if List.exists Guards.is_empty remaining then
1067
             shared, []
1068
           else
1069
             shared, remaining
1070
      ) map
1027 1071
  in
1028
  report ~level:3
1029
    (fun fmt ->
1030
      Format.fprintf fmt
1031
        "@[<v 0>Init:@ %a@]@."
1032
        (Utils.fprintf_list ~sep:"@ "
1033
           (fun fmt (m,mdefs) ->
1034
             Format.fprintf fmt
1035
               "%s -> @[<v 0>[%a@] ]@ "
1036
               m
1037
               (Utils.fprintf_list ~sep:"@ "
1038
                  (pp_guard_expr pp_elem)) mdefs
1039
        ))
1040
        init_defs);
1041
  report ~level:3
1042
    (fun fmt ->
1043
      Format.fprintf fmt
1044
        "@[<v 0>Step:@ %a@]@."
1045
        (Utils.fprintf_list ~sep:"@ "
1046
           (fun fmt (m,mdefs) ->
1047
             Format.fprintf fmt
1048
               "%s -> @[<v 0>[%a@] ]@ "
1049
               m
1050
               (Utils.fprintf_list ~sep:"@ "
1051
                  (pp_guard_expr pp_elem)) mdefs
1052
        ))
1053
        update_defs);
1054
  (* Format.eprintf "Build init@."; *)
1055
  
1056
  report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ...@.");
1057
  let sw_init= 
1058
    build_switch_sys init_defs []
1072
  let rec mk_binop op l = match l with
1073
      [] -> assert false
1074
    | [e] -> e
1075
    | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl]
1059 1076
  in
1060
  (* Format.eprintf "Build step@."; *)
1061
  let sw_sys =
1062
    build_switch_sys update_defs []
1077
  let gl_as_expr gl =
1078
    let gl = Guards.elements gl in
1079
    let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in 
1080
    match gl with
1081
      [] -> []
1082
    | [e] -> [export e]
1083
    | _ ->
1084
       [mk_binop "&&"
1085
          (List.map export gl)]
1063 1086
  in
1064
  report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ... done@.");
1087
  let rec clean_disj disj =
1088
    match disj with
1089
    | [] -> []
1090
    | [_] -> assert false (* A disjunction with a single case can be ignored *) 
1091
    | _::_::_ -> (
1092
      (* First basic version: producing a DNF One can later, (1)
1093
           simplify it with z3, or (2) build the compact tree with
1094
           maximum shared subexpression (and simplify it with z3) *)
1095
      let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in
1096
      let or_expr = mk_binop "||" elems in
1097
      [or_expr]
1065 1098

  
1066
  report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ...@.");
1067
  let init_out =
1068
    build_switch_sys init_out []
1069
  in
1070
  (* report ~level:1 (fun fmt -> Format.fprintf fmt "Build step out@."); *)
1071 1099

  
1072
  let update_out =
1073
    build_switch_sys update_out []
1100
    (* TODO disj*)
1101
    (* get the item that occurs in most case *)
1102
    (* List.fold_left (fun accu s ->
1103
     *     List.fold_left (fun accu (e,b) ->
1104
     *         if List.mem_assoc (e.expr_tag, b)
1105
     *       ) accu (Guards.elements s)
1106
     *   ) [] disj *)
1107

  
1108
    )
1074 1109
  in
1075
  report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ... done@.");
1110
  if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map);
1111
  UpMap.fold (fun up (common, disj) accu ->
1112
      if !seal_debug then
1113
        report ~level:6 (fun fmt -> Format.fprintf fmt 
1114
                                      "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1115
                                      Guards.pp_short common
1116
                                      (fprintf_list ~sep:";@ " Guards.pp_long) disj
1117
                                      UpMap.pp up);
1118
      let disj = clean_disj disj in
1119
      let guard_expr = (gl_as_expr common)@disj in
1120
      
1121
      ((match guard_expr with
1122
        | [] -> None 
1123
        | _ -> Some (mk_binop "&&" guard_expr)), up)::accu
1124
    ) map []
1125
  
1126
    
1127
    
1076 1128

  
1077
  report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ...@.");
1129
(* Take a normalized node and extract a list of switches: (cond,
1130
   update) meaning "if cond then update" where update shall define all
1131
   node memories. Everything as to be expressed over inputs or
1132
   memories, intermediate variables are removed through inlining *)
1133
let node_as_switched_sys consts (mems:var_decl list) nd =
1134
  let mem_defs, output_defs = build_environement consts mems nd in
1135
  
1136
  let init_defs, update_defs = split_init mem_defs in
1137
  let init_out, update_out =   split_init output_defs in
1138
  
1139
  report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 0>Init:@ %a@ Step:@ %a@]@."
1140
                                (pp_assign_map pp_elem) init_defs
1141
                                (pp_assign_map pp_elem) update_defs);
1142
  
1143

  
1144
  report ~level:1 (fun fmt -> Format.fprintf fmt
1145
                                "init/step as a switched system ...@.");
1146
  let sw_init= build_switch_sys init_defs [] in
1147
  let sw_sys = build_switch_sys update_defs [] in
1148
  report ~level:1 (fun fmt -> Format.fprintf fmt
1149
                                "init/step as a switched system ... done@.");
1150

  
1151

  
1152
  report ~level:1 (fun fmt -> Format.fprintf fmt
1153
                                "output function as a switched system ...@.");
1154
  let init_out =   build_switch_sys init_out [] in
1155
  let update_out = build_switch_sys update_out [] in
1156
  
1157
  report ~level:1 (fun fmt -> Format.fprintf fmt
1158
                                "output function as a switched system ... done@.");
1159

  
1160
  report ~level:1 (fun fmt -> Format.fprintf fmt
1161
                                "removing dead branches and merging remaining ...@.");
1078 1162

  
1079 1163
  let sw_init = clean_sys sw_init in
1080 1164
  let sw_sys = clean_sys sw_sys in
1081 1165
  let init_out = clean_sys init_out in
1082 1166
  let update_out = clean_sys update_out in
1083
  report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ... done@.");
1167

  
1168
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@.");
1169
  let sw_init = merge_updates sw_init in
1170
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@.");
1171
  let sw_sys = merge_updates sw_sys in
1172
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@.");
1173
  let init_out = merge_updates init_out in
1174
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@.");
1175
  let update_out = merge_updates update_out in
1176
  report ~level:1 (fun fmt ->
1177
      Format.fprintf fmt "removing dead branches and merging remaining ... done@.");
1178

  
1179
  sw_init , sw_sys, init_out, update_out
1180

  
1181

  
1182
let fun_as_switched_sys consts  nd =
1183
  let _, update_out = build_environement consts [] nd in
1184

  
1185
  report ~level:1 (fun fmt -> Format.fprintf fmt
1186
                                "output function as a switched system ...@.");
1187
  let update_out = build_switch_sys update_out [] in
1188
  report ~level:1 (fun fmt -> Format.fprintf fmt
1189
                                "output function as a switched system ... done@.");
1190

  
1191
  report ~level:1 (fun fmt -> Format.fprintf fmt
1192
                                "removing dead branches and merging remaining ...@.");
1193
  let update_out = clean_sys update_out in
1194
  let update_out = merge_updates update_out in
1195
  report ~level:1 (fun fmt ->
1196
      Format.fprintf fmt "removing dead branches and merging remaining ... done@.");
1197

  
1198
  update_out
1199

  
1200

  
1201

  
1202

  
1203
                                
1204
                                (* Some code that was used to check for duplicate entries in guards.
1205

  
1084 1206

  
1085 1207
  (* Some additional checks *)
1086 1208
  
......
1156 1278
    end;
1157 1279
  
1158 1280

  
1159
  (* Iter through the elements and gather them by updates *)
1160
  let process sys =
1161
    (* The map will associate to each update up the pair (set, set
1162
       list) where set is the share guards and set list a list of
1163
       disjunctive guards. Each set represents a conjunction of
1164
       expressions. *)
1165
    report ~level:3 (fun fmt -> Format.fprintf fmt "%t@."
1166
                                  (fun fmt -> List.iter (fun (gl,up) ->
1167
                                                  Format.fprintf fmt "[@[%a@]] -> (%a)@ "
1168
                                                    (pp_guard_list Printers.pp_expr) gl pp_up up) sw_init));
1169
    
1170
    (* We perform multiple pass to avoid errors *)
1171
    let map =
1172
      List.fold_left (fun map (gl,up) ->
1173
          (* creating a new set to describe gl *)
1174
          let new_set =
1175
            List.fold_left
1176
              (fun set g -> Guards.add g set)
1177
              Guards.empty
1178
              gl
1179
          in
1180
          (* updating the map with up -> new_set *)
1181
          if UpMap.mem up map then
1182
            let guard_set = UpMap.find up map in
1183
            UpMap.add up (new_set::guard_set) map
1184
          else
1185
            UpMap.add up [new_set] map
1186
        ) UpMap.empty sys
1187
    in
1188
    (* Processing the set of guards leading to the same update: return
1189
       conj, disj with conf is a set of guards, and disj a DNF, ie a
1190
       list of set of guards *)
1191
    let map =
1192
      UpMap.map (
1193
          fun guards ->
1194
          match guards with
1195
          | [] -> Guards.empty, [] (* Nothing *)
1196
          | [s]-> s, [] (* basic case *)
1197
          | hd::tl ->
1198
             let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in
1199
             let remaining = List.map (fun s -> Guards.diff s shared) guards in
1200
             (* If one of them is empty, we can remove the others, otherwise keep them *)
1201
             if List.exists Guards.is_empty remaining then
1202
               shared, []
1203
             else
1204
               shared, remaining
1205
        ) map
1206
    in
1207
  let rec mk_binop op l = match l with
1208
      [] -> assert false
1209
    | [e] -> e
1210
    | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl]
1211
  in
1212
  let gl_as_expr gl =
1213
    let gl = Guards.elements gl in
1214
    let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in 
1215
    match gl with
1216
      [] -> []
1217
    | [e] -> [export e]
1218
    | _ ->
1219
       [mk_binop "&&"
1220
          (List.map export gl)]
1221
  in
1222
  let rec clean_disj disj =
1223
    match disj with
1224
    | [] -> []
1225
    | [_] -> assert false (* A disjunction was a single case can be ignored *) 
1226
    | _::_::_ -> (
1227
      (* First basic version: producing a DNF One can later, (1)
1228
           simplify it with z3, or (2) build the compact tree with
1229
           maximum shared subexpression (and simplify it with z3) *)
1230
      let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in
1231
      let or_expr = mk_binop "||" elems in
1232
      [or_expr]
1233

  
1234

  
1235
    (* TODO disj*)
1236
    (* get the item that occurs in most case *)
1237
    (* List.fold_left (fun accu s ->
1238
     *     List.fold_left (fun accu (e,b) ->
1239
     *         if List.mem_assoc (e.expr_tag, b)
1240
     *       ) accu (Guards.elements s)
1241
     *   ) [] disj *)
1242

  
1243
    )
1244
  in
1245
  if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map);
1246
  UpMap.fold (fun up (common, disj) accu ->
1247
      if !seal_debug then
1248
        report ~level:6 (fun fmt -> Format.fprintf fmt 
1249
          "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1250
          Guards.pp_short common
1251
          (fprintf_list ~sep:";@ " Guards.pp_long) disj
1252
          UpMap.pp up);
1253
      let disj = clean_disj disj in
1254
      let guard_expr = (gl_as_expr common)@disj in
1255
      
1256
      ((match guard_expr with
1257
        | [] -> None 
1258
        | _ -> Some (mk_binop "&&" guard_expr)), up)::accu
1259
    ) map []
1260
  
1261
    in
1262
    
1263
    
1264
    
1265
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@.");
1266
    let sw_init = process sw_init in
1267
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@.");
1268
    let sw_sys = process sw_sys in
1269
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@.");
1270
    let init_out = process init_out in
1271
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@.");
1272
    let update_out = process update_out in
1273
    sw_init , sw_sys, init_out, update_out
1281
                                 *)

Also available in: Unified diff