Project

General

Profile

Revision a0c92fa8

View differences:

src/compiler_stages.ml
123 123

  
124 124

  
125 125
  (* Generating a .lusi header file only *)
126
  if !Options.lusi then
126
  if !Options.lusi || !Options.print_nodes then
127 127
    (* We stop here the processing and produce the current prog. It will be
128 128
       exported as a lusi *)
129 129
    raise (StopPhase1 prog);
src/main_lustre_compiler.ml
47 47

  
48 48
  (* Parsing source *)
49 49
  let prog = parse source_name extension in
50

  
50
  
51 51
  let prog =
52 52
    if !Options.mpfr &&
53 53
         extension = ".lus" (* trying to avoid the injection of the module for lusi files *) 
......
71 71
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
72 72
	  exit 0
73 73
	end
74
      else if !Options.print_nodes then (
75
        Format.printf "%a@.@?" Printers.pp_node_list prog;
76
        exit 0
77
      )
74 78
      else
75 79
        assert false
76 80
    )
src/main_lustre_testgen.ml
46 46
  (* Parsing source *)
47 47
  let prog = parse source_name extension in
48 48
  let params = Backends.get_normalization_params () in
49
  let prog, dependencies = Compiler_stages.stage1 params prog dirname basename extension in
50

  
49
  let prog, dependencies =
50
    try
51
      Compiler_stages.stage1 params prog dirname basename extension 
52
   with Compiler_stages.StopPhase1 prog -> (
53
      if !Options.print_nodes then (
54
        Format.printf "%a@.@?" Printers.pp_node_list prog;
55
        exit 0
56
      )
57
      else
58
        assert false
59
    )
60
 in
61
  
51 62
  (* Two cases
52 63
     - generation of coverage conditions
53 64
     - generation of mutants: a number of mutated lustre files 
src/main_lustre_verifier.ml
65 65
      decr Options.verbose_level;
66 66
      Compiler_stages.stage1 params prog dirname basename extension
67 67
    with Compiler_stages.StopPhase1 prog -> (
68
      if !Options.print_nodes then (
69
        Format.printf "%a@.@?" Printers.pp_node_list prog;
70
        exit 0
71
      )
72
      else
68 73
        assert false
69 74
    )
70 75
  in
src/options.ml
29 29
let witnesses = ref false
30 30
let optimization = ref 2
31 31
let lusi = ref false
32
let print_nodes = ref false
32 33
let print_reuse = ref false
33 34
let const_unfold = ref false
34 35
let mpfr = ref false
src/options_management.ml
92 92
    "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
93 93
    "-print-types", Arg.Set print_types, "prints node types";
94 94
    "-print-clocks", Arg.Set print_clocks, "prints node clocks";
95
    "-print-nodes",  Arg.Set print_nodes, "prints node list";
95 96
    "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops";
96 97
    "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops  <default: 15>";
97 98
    "-kind2", Arg.Set kind2_print, "active kind2 output";
src/printers.ml
601 601
  | Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i
602 602
  | Field f -> fprintf fmt ".%s" f
603 603

  
604
let pp_node_list fmt prog =
605
  Format.fprintf fmt "@[<h 2>%a@]"
606
    (fprintf_list
607
       ~sep:"@ "
608
       (fun fmt decl ->
609
         match decl.top_decl_desc with
610
         | Node nd -> Format.fprintf fmt "%s" nd.node_id
611
         | _ -> ()
612
    ))
613
    prog
614
    
604 615
(* Local Variables: *)
605 616
(* compile-command:"make -C .." *)
606 617
(* End: *)
src/tools/seal/seal_export.ml
62 62
       match g_opt with
63 63
       | None -> (
64 64
         Format.eprintf "SEAL issue: process_sw with %a"
65
           pp_sys sw
65
           (pp_sys Printers.pp_expr) sw
66 66
       ;
67 67
         assert false (* How could this happen anyway ? *)
68 68
       )
......
117 117
  in
118 118
  new_nd, orig_nd
119 119

  
120
    
121
let funsw_to_lustre m update_out =
122
  let orig_nd = m.mname in
123
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
124
  let output_eq =
125
    let e_update_out = process_sw copy_nd.node_outputs  (fun x -> x) update_out in
126
    [ 
127
      Eq
128
        { eq_loc = Location.dummy_loc;
129
          eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; 
130
          eq_rhs = e_update_out
131
        };
132
    ]
133
  in
134
  let new_nd =
135
    { copy_nd with
136
      node_id = copy_nd.node_id ^ "_seal";
137
      node_locals = [];
138
      node_stmts = output_eq;
139
    }
140
  in
141
  new_nd, orig_nd
142
  
120 143
  
121
let to_lustre basename prog m sw_init sw_step init_out update_out =
144

  
145
let to_lustre basename prog new_node orig_node =
122 146
  let loc = Location.dummy_loc in
123
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
124 147
  Global.type_env := Typing.type_node !Global.type_env new_node loc;
125 148
  Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node;
126 149

  
......
139 162
  let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in
140 163
  let out_verif = open_out output_file_verif in
141 164
  let fmt_verif = Format.formatter_of_out_channel out_verif in
142
  let check_nd = Lustre_utils.check_eq new_node orig_nd in
165
  let check_nd = Lustre_utils.check_eq new_node orig_node in
143 166
  let check_top =
144 167
    Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd)
145 168
  in
146
  Format.fprintf fmt_verif "%a@." Printers.pp_prog  (prog@[new_top;check_top]);
169
  Format.fprintf fmt_verif "%a@." Printers.pp_prog  (prog@[new_top;check_top])
170
  
171
let node_to_lustre basename prog m sw_init sw_step init_out update_out =
172
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
173
  to_lustre basename prog new_node orig_nd
174

  
175
let fun_to_lustre basename prog m update_out =
176
  let new_node, orig_nd = funsw_to_lustre m update_out in
177
  to_lustre basename prog new_node orig_nd
178

  
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
                                 *)
src/tools/seal/seal_utils.ml
28 28
     (fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl
29 29
  
30 30
let pp_guard_expr pp_elem  fmt (gl,e) =
31
  Format.fprintf fmt "@[%a@] -> @[<hov 2>%a@]"
31
  Format.fprintf fmt "@[<v 2>@[%a@] ->@ @[<hov 2>%a@]@]"
32 32
    (pp_guard_list pp_elem) gl
33 33
    pp_elem e
34 34

  
35 35
let pp_mdefs pp_elem fmt gel = fprintf_list ~sep:"@ " (pp_guard_expr pp_elem) fmt gel
36 36

  
37
                             
37
let pp_assign_map pp_elem =
38
  fprintf_list ~sep:"@ "
39
    (fun fmt (m, mdefs) ->
40
      Format.fprintf fmt
41
        "%s -> @[<v 0>[%a@] ]@ "
42
        m
43
        (pp_mdefs pp_elem) mdefs
44
    )
38 45
  
39 46
let deelem e =  match e with
40 47
    Expr e -> e
......
53 60
  fprintf_list ~sep:", " (fun fmt (e,b) -> Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e)
54 61
  
55 62
let pp_gl_short = pp_gl (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) 
56
let pp_up fmt up = List.iter (fun (id,e) -> Format.fprintf fmt "%s->%i; " id e.expr_tag) up 
57 63

  
58
let pp_sys fmt sw = List.iter (fun (gl,up) ->
59
                        match gl with
60
                        | None ->
61
                           pp_up fmt up
62
                        | Some gl ->
63
                           Format.fprintf fmt "[@[%a@]] -> (%a)@ "
64
                             Printers.pp_expr gl pp_up up) sw
64
let pp_up pp_elem fmt up =
65
  fprintf_list ~sep:"@ "
66
    (fun fmt (id,e) -> Format.fprintf fmt "%s == %a;@ " id pp_elem e)
67
    fmt
68
    up 
69

  
70
let pp_sys pp_elem fmt sw =
71
  fprintf_list ~sep:"@ "
72
    (fun fmt (gl,up) ->
73
      match gl with
74
      | None ->
75
         (pp_up pp_elem) fmt up
76
      | Some gl ->
77
         Format.fprintf fmt "@[<v 2>[@[%a@]]:@ %a@]"
78
           Printers.pp_expr gl (pp_up pp_elem) up)
79
    fmt
80
    sw
81
  
65 82
let pp_all_defs =
66 83
  (Utils.fprintf_list ~sep:",@ "
67 84
     (fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]"
......
76 93
                        let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in
77 94
                        compare (proj l1) (proj l2) 
78 95
                    end)
79
        let pp = pp_up 
96
        let pp = pp_up Printers.pp_expr 
80 97
      end
81 98
    
82 99
module Guards = struct
src/tools/seal/seal_verifier.ml
1
open Seal_slice
2
open Seal_extract
3
open Seal_utils
4

  
5
let active = ref false
6
let seal_export = ref None
7

  
8
let set_export s = match s with
9
  | "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s
10
  | _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1)
11 1
(* TODO
12 2

  
13 3
   - build the output function: for the moment we slice the node with
......
35 25
       the property to prove
36 26
     
37 27
 *)
28

  
29

  
30
open Seal_slice
31
open Seal_extract
32
open Seal_utils
33

  
34
let active = ref false
35
let seal_export = ref None
36

  
37
let set_export s = match s with
38
  | "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s
39
  | _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1)
38 40
           
39 41
(* Select the appropriate node, should have been inlined already and
40 42
   extract update/output functions. *)
......
64 66
  in
65 67
  let m = Machine_code_common.get_machine machines node_name in
66 68
  let nd = m.mname in
67
  (* Format.eprintf "Node %a@." Printers.pp_node nd; *)
68 69
  let mems = m.mmemory in
70

  
69 71
  report ~level:1 (fun fmt -> Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id (List.length mems));
70
  (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *)
72

  
73
  (* Slicing node *)
71 74
  let msch = Utils.desome m.msch in
72
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
73 75
  let sliced_nd = slice_node (mems@nd.node_outputs) msch nd in
74
  if false then Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd;
75 76
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
77
  report ~level:10 (fun fmt -> Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd);
76 78

  
77 79
  let consts = Corelang.(List.map const_of_top (get_consts prog)) in
78
  let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in
79
  let pp_res pp_expr =
80
    (Utils.fprintf_list ~sep:"@ "
81
       (fun fmt (g, up) ->
82
         Format.fprintf fmt "@[<v 2>[%t]:@ %a@]"
83
           (fun fmt -> match g with None -> () | Some g -> pp_expr fmt g)
84
           
85
           (* (Utils.fprintf_list ~sep:"; "
86
            *    (fun fmt (e,b) ->
87
            *      if b then pp_expr fmt e
88
            *      else Format.fprintf fmt "not(%a)"
89
            *             pp_expr e)) gel *)
90
           (Utils.fprintf_list ~sep:";@ "
91
              (fun fmt (id, e) ->
92
                Format.fprintf fmt "%s = @[<hov 0>%a@]"
93
                  id
94
                  pp_expr e)) up
95
    ))
96
  in
97
  report ~level:1 (
98
      fun fmt -> Format.fprintf fmt
99
                   "%i memories, %i init, %i step switch cases@."
100
                   (List.length mems)
101
                   (List.length sw_init)
102
                   (List.length sw_sys)
103
               
104
    );
105
  report ~level:1 (fun fmt ->
106
      (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag)  in*)
107
       let pp_res = pp_res Printers.pp_expr in
108
      Format.fprintf fmt "DynSys:@ @[<v 0>@[<v 3>Init:@ %a@]@ "
109
        pp_res  sw_init;
110
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@."
111
        pp_res  sw_sys
112
    );
113

  
114

  
115
                
116
 report ~level:1 (fun fmt ->
117
      (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag)  in*)
118
       let pp_res = pp_res Printers.pp_expr in
119
      Format.fprintf fmt "Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ "
120
             (List.length init_out)
121
                   (List.length update_out)
122
                   pp_res  init_out;
123
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@."
124
        pp_res  update_out
125
    );
126
  let _ = match !seal_export with
127
    | Some "lustre" | Some "lus" ->
128
       Seal_export.to_lustre basename prog m sw_init sw_sys init_out update_out  
129
    | Some "matlab" | Some "m" -> assert false (* TODO *)
130
    | Some _ -> assert false 
131
    | None -> ()
132
  in
133
  ()
80

  
81
  let pp_sys = pp_sys Printers.pp_expr in
82
  if List.length mems = 0 then
83
    begin (* A stateless node = a function ! *)
84
      
85
      let update_out = fun_as_switched_sys consts sliced_nd in
86

  
87
      report ~level:1 (fun fmt ->
88
          Format.fprintf fmt
89
            "Output (%i step switch cases):@ @[<v 0>%a@]@."
90
            (List.length update_out)
91
            pp_sys update_out
92
        );
93
      
94
      let _ = match !seal_export with
95
        | Some "lustre" | Some "lus" ->
96
           Seal_export.fun_to_lustre basename prog m update_out  
97
        | Some "matlab" | Some "m" -> assert false (* TODO *)
98
        | Some _ -> assert false 
99
        | None -> ()
100
      in
101
      ()
102
    end
103
  else
104
    begin (* A stateful node *)
105

  
106
      let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in
107

  
108
      report ~level:1 (fun fmt ->
109
          Format.fprintf fmt
110
            "DynSys: (%i memories, %i init, %i step switch cases)@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."
111
            (List.length mems)
112
            (List.length sw_init)
113
            (List.length sw_sys)
114
            pp_sys  sw_init
115
            pp_sys  sw_sys
116
        );
117
      
118
      report ~level:1 (fun fmt ->
119
          Format.fprintf fmt
120
            "Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."
121
            (List.length init_out)
122
            (List.length update_out)
123
            pp_sys  init_out
124
            pp_sys  update_out
125
        );
126
      
127
      let _ = match !seal_export with
128
        | Some "lustre" | Some "lus" ->
129
           Seal_export.node_to_lustre basename prog m sw_init sw_sys init_out update_out  
130
        | Some "matlab" | Some "m" -> assert false (* TODO *)
131
        | Some _ -> assert false 
132
        | None -> ()
133
      in
134
      ()
135
    end
134 136
  
135 137
module Verifier =
136 138
  (struct
......
151 153
      
152 154
    let is_active () = !active
153 155
    let run = seal_run
154
      
155
                    
156
            
157
            
156 158
  end: VerifierType.S)
157 159
    
src/tools/zustre/zustre_common.ml
5 5
(* open Horn_backend_common
6 6
 * open Horn_backend *)
7 7
open Zustre_data
8

  
8
  
9
let report = Log.report ~plugin:"z3 interface"
10
           
9 11
module HBC = Horn_backend_common
10 12
let node_name = HBC.node_name
11 13

  
......
111 113
let get_fdecl id =
112 114
  try
113 115
    Hashtbl.find decls id
114
  with Not_found -> (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found)
116
  with Not_found -> (report ~level:3 (fun fmt -> Format.fprintf fmt  "Unable to find func_decl %s@.@?" id); raise Not_found)
115 117

  
116 118
let pp_fdecls fmt =
117 119
  Format.fprintf fmt "Registered fdecls: @[%a@]@ "
......
124 126
  register_fdecl id.var_id fdecl;
125 127
  fdecl
126 128

  
129
(* Declaring the function used in expr *) 
130
let decl_fun op args typ =
131
  let args = List.map type_to_sort args in
132
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in
133
  register_fdecl op fdecl;
134
  fdecl
135

  
127 136
let idx_sort = int_sort
128 137
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort
129 138
let uid_conc = 
......
242 251

  
243 252
(* Conversion of basic library functions *)
244 253
    
245
let horn_basic_app i val_to_expr vl =
254
let horn_basic_app i vl (vltyp, typ) =
246 255
  match i, vl with
247
  | "ite", [v1; v2; v3] ->
248
     Z3.Boolean.mk_ite
249
       !ctx
250
       (val_to_expr v1)
251
       (val_to_expr v2)
252
       (val_to_expr v3)
253

  
254
  | "uminus", [v] ->
255
     Z3.Arithmetic.mk_unary_minus
256
       !ctx
257
       (val_to_expr v)
256
  | "ite", [v1; v2; v3] ->  Z3.Boolean.mk_ite !ctx v1 v2 v3
257
  | "uminus", [v] ->    Z3.Arithmetic.mk_unary_minus
258
       !ctx v
258 259
  | "not", [v] ->
259 260
     Z3.Boolean.mk_not
260
       !ctx
261
       (val_to_expr v)
261
       !ctx v
262 262
  | "=", [v1; v2] ->
263 263
     Z3.Boolean.mk_eq
264
       !ctx
265
       (val_to_expr v1)
266
       (val_to_expr v2)
264
       !ctx v1 v2
267 265
  | "&&", [v1; v2] ->
268 266
     Z3.Boolean.mk_and
269 267
       !ctx
270
       [val_to_expr v1;
271
        val_to_expr v2]
268
       [v1; v2]
272 269
  | "||", [v1; v2] ->
273 270
          Z3.Boolean.mk_or
274 271
       !ctx
275
       [val_to_expr v1;
276
        val_to_expr v2]
272
       [v1;
273
         v2]
277 274

  
278 275
  | "impl", [v1; v2] ->
279 276
     Z3.Boolean.mk_implies
280
       !ctx
281
       (val_to_expr v1)
282
       (val_to_expr v2)
277
       !ctx v1 v2
283 278
 | "mod", [v1; v2] ->
284 279
          Z3.Arithmetic.Integer.mk_mod
285
       !ctx
286
       (val_to_expr v1)
287
       (val_to_expr v2)
280
       !ctx v1 v2
288 281
  | "equi", [v1; v2] ->
289 282
          Z3.Boolean.mk_eq
290 283
       !ctx
291
       (val_to_expr v1)
292
       (val_to_expr v2)
284
       v1 v2
293 285
  | "xor", [v1; v2] ->
294 286
          Z3.Boolean.mk_xor
295
       !ctx
296
       (val_to_expr v1)
297
       (val_to_expr v2)
287
       !ctx v1 v2
298 288
  | "!=", [v1; v2] ->
299 289
     Z3.Boolean.mk_not
300 290
       !ctx
301 291
       (
302 292
         Z3.Boolean.mk_eq
303
           !ctx
304
           (val_to_expr v1)
305
           (val_to_expr v2)
293
           !ctx v1 v2
306 294
       )
307 295
  | "/", [v1; v2] ->
308 296
     Z3.Arithmetic.mk_div
309
       !ctx
310
       (val_to_expr v1)
311
       (val_to_expr v2)
297
       !ctx v1 v2
312 298

  
313 299
  | "+", [v1; v2] ->
314 300
     Z3.Arithmetic.mk_add
315 301
       !ctx
316
       [val_to_expr v1; val_to_expr v2]
317

  
302
       [v1; v2]
318 303
  | "-", [v1; v2] ->
319 304
     Z3.Arithmetic.mk_sub
320 305
       !ctx
321
       [val_to_expr v1 ; val_to_expr v2]
306
       [v1 ;  v2]
322 307
       
323 308
  | "*", [v1; v2] ->
324 309
     Z3.Arithmetic.mk_mul
325 310
       !ctx
326
       [val_to_expr v1; val_to_expr v2]
311
       [ v1;  v2]
327 312

  
328 313

  
329 314
  | "<", [v1; v2] ->
330 315
     Z3.Arithmetic.mk_lt
331
       !ctx
332
       (val_to_expr v1)
333
       (val_to_expr v2)
334

  
316
       !ctx v1 v2
335 317
  | "<=", [v1; v2] ->
336 318
     Z3.Arithmetic.mk_le
337
       !ctx
338
       (val_to_expr v1)
339
       (val_to_expr v2)
340

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

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

  
325
       !ctx v1 v2
353 326
  | "int_to_real", [v1] ->
354 327
     Z3.Arithmetic.Integer.mk_int2real
355
       !ctx
356
       (val_to_expr v1)
357

  
328
       !ctx v1
329
  | _ ->
330
     let fd =
331
       try
332
         get_fdecl i
333
       with Not_found -> begin
334
           report ~level:3 (fun fmt -> Format.fprintf fmt "Registering function %s as uninterpreted function in Z3@.%s: (%a) -> %a" i i (Utils.fprintf_list ~sep:"," Types.print_ty) vltyp Types.print_ty typ); 
335
           decl_fun i vltyp typ
336
         end
337
     in
338
     Z3.FuncDecl.apply fd vl
358 339
    
340
     
359 341
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
360 342
   *      !ctx
361 343
   *      (val_to_expr v1)
362 344
   *      (val_to_expr v2)
363 345
   * 
364 346
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
365
  | _ -> (
366
    let msg fmt = Format.fprintf fmt
367
                    "internal error: zustre unkown function %s (nb args = %i)@."
368
                    i (List.length vl)
369
    in
370
    raise (UnknownFunction(i, msg))
371
  )
347

  
348
(* | _ -> (
349
 *     let msg fmt = Format.fprintf fmt
350
 *                     "internal error: zustre unkown function %s (nb args = %i)@."
351
 *                     i (List.length vl)
352
 *     in
353
 *     raise (UnknownFunction(i, msg))
354
 *   ) *)
372 355

  
373 356
           
374 357
(* Convert a value expression [v], with internal function calls only.  [pp_var]
......
376 359
   may be added for array variables
377 360
*)
378 361
let rec horn_val_to_expr ?(is_lhs=false) m self v =
362
  (* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *)
379 363
  match v.value_desc with
380 364
  | Cst c       -> horn_const_to_expr c
381 365

  
......
425 409
         (rename_machine
426 410
            self
427 411
            v)
428
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr m self) vl
412
  | Fun (n, vl)   -> horn_basic_app n (List.map (horn_val_to_expr m self) vl) (List.map (fun v -> v.value_type) vl, v.value_type)
429 413

  
430 414
let no_reset_to_exprs machines m i =
431 415
  let (n,_) = List.assoc i m.minstances in

Also available in: Unified diff