diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml index ef169869f984cf4b429b7cfa39478ddb40b58cde..9b5813b495f5be539ec48d3a6fdd2717a7462cd9 100644 --- a/src/compiler_stages.ml +++ b/src/compiler_stages.ml @@ -123,7 +123,7 @@ let stage1 params prog dirname basename extension = (* Generating a .lusi header file only *) - if !Options.lusi then + if !Options.lusi || !Options.print_nodes then (* We stop here the processing and produce the current prog. It will be exported as a lusi *) raise (StopPhase1 prog); diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml index 7b5e5763cd7037cfdd32a24894deba0a95eb2222..a7391ee2511d61cbf99fb470747bd63f6beff79d 100644 --- a/src/main_lustre_compiler.ml +++ b/src/main_lustre_compiler.ml @@ -47,7 +47,7 @@ let rec compile dirname basename extension = (* Parsing source *) let prog = parse source_name extension in - + let prog = if !Options.mpfr && extension = ".lus" (* trying to avoid the injection of the module for lusi files *) @@ -71,6 +71,10 @@ let rec compile dirname basename extension = Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@."); exit 0 end + else if !Options.print_nodes then ( + Format.printf "%a@.@?" Printers.pp_node_list prog; + exit 0 + ) else assert false ) diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml index d3d59b750b36ae719b9bfc552db95a9048d2cab9..95dccd2367cb189da4d2dec94ae22d60fb6ace31 100644 --- a/src/main_lustre_testgen.ml +++ b/src/main_lustre_testgen.ml @@ -46,8 +46,19 @@ let testgen_source dirname basename extension = (* Parsing source *) let prog = parse source_name extension in let params = Backends.get_normalization_params () in - let prog, dependencies = Compiler_stages.stage1 params prog dirname basename extension in - + let prog, dependencies = + try + Compiler_stages.stage1 params prog dirname basename extension + with Compiler_stages.StopPhase1 prog -> ( + if !Options.print_nodes then ( + Format.printf "%a@.@?" Printers.pp_node_list prog; + exit 0 + ) + else + assert false + ) + in + (* Two cases - generation of coverage conditions - generation of mutants: a number of mutated lustre files diff --git a/src/main_lustre_verifier.ml b/src/main_lustre_verifier.ml index 2e802799b3e8b573b4772f53da706caad7b10bdd..7aed1884f27a985d2028b0c8950228c6f954fc08 100644 --- a/src/main_lustre_verifier.ml +++ b/src/main_lustre_verifier.ml @@ -65,6 +65,11 @@ let rec verify dirname basename extension = decr Options.verbose_level; Compiler_stages.stage1 params prog dirname basename extension with Compiler_stages.StopPhase1 prog -> ( + if !Options.print_nodes then ( + Format.printf "%a@.@?" Printers.pp_node_list prog; + exit 0 + ) + else assert false ) in diff --git a/src/options.ml b/src/options.ml index 99dd6565a8c733871137cbaad5dc442eacd7ee48..4d87b07655b98226e15c47eedf38a13bd297d1da 100644 --- a/src/options.ml +++ b/src/options.ml @@ -29,6 +29,7 @@ let global_inline = ref false let witnesses = ref false let optimization = ref 2 let lusi = ref false +let print_nodes = ref false let print_reuse = ref false let const_unfold = ref false let mpfr = ref false diff --git a/src/options_management.ml b/src/options_management.ml index 480fbb29189af28d97517133419a951f62c2465d..acc58285b880279bf1180c1bd390a00fe6e455e0 100644 --- a/src/options_management.ml +++ b/src/options_management.ml @@ -92,6 +92,7 @@ let common_options = "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node"; "-print-types", Arg.Set print_types, "prints node types"; "-print-clocks", Arg.Set print_clocks, "prints node clocks"; + "-print-nodes", Arg.Set print_nodes, "prints node list"; "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops"; "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops <default: 15>"; "-kind2", Arg.Set kind2_print, "active kind2 output"; diff --git a/src/printers.ml b/src/printers.ml index a78404e98eae0443c83e5f3edc14ba8a2649e16d..2cff5cce9eca3e9fb58c0bd8fb0fbab5c8a93515 100644 --- a/src/printers.ml +++ b/src/printers.ml @@ -601,6 +601,17 @@ let pp_offset fmt offset = | Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i | Field f -> fprintf fmt ".%s" f +let pp_node_list fmt prog = + Format.fprintf fmt "@[<h 2>%a@]" + (fprintf_list + ~sep:"@ " + (fun fmt decl -> + match decl.top_decl_desc with + | Node nd -> Format.fprintf fmt "%s" nd.node_id + | _ -> () + )) + prog + (* Local Variables: *) (* compile-command:"make -C .." *) (* End: *) diff --git a/src/tools/seal/seal_export.ml b/src/tools/seal/seal_export.ml index 7a93bef5644825e153ac70086794161f12f82278..8c750487d248355c3edc2973e2479bf3ba1da212 100644 --- a/src/tools/seal/seal_export.ml +++ b/src/tools/seal/seal_export.ml @@ -62,7 +62,7 @@ let process_sw vars f_e sw = match g_opt with | None -> ( Format.eprintf "SEAL issue: process_sw with %a" - pp_sys sw + (pp_sys Printers.pp_expr) sw ; assert false (* How could this happen anyway ? *) ) @@ -117,10 +117,33 @@ let sw_to_lustre m sw_init sw_step init_out update_out = in new_nd, orig_nd + +let funsw_to_lustre m update_out = + let orig_nd = m.mname in + let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in + let output_eq = + let e_update_out = process_sw copy_nd.node_outputs (fun x -> x) update_out in + [ + Eq + { eq_loc = Location.dummy_loc; + eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; + eq_rhs = e_update_out + }; + ] + in + let new_nd = + { copy_nd with + node_id = copy_nd.node_id ^ "_seal"; + node_locals = []; + node_stmts = output_eq; + } + in + new_nd, orig_nd + -let to_lustre basename prog m sw_init sw_step init_out update_out = + +let to_lustre basename prog new_node orig_node = let loc = Location.dummy_loc in - let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in Global.type_env := Typing.type_node !Global.type_env new_node loc; Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node; @@ -139,8 +162,17 @@ let to_lustre basename prog m sw_init sw_step init_out update_out = let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in let out_verif = open_out output_file_verif in let fmt_verif = Format.formatter_of_out_channel out_verif in - let check_nd = Lustre_utils.check_eq new_node orig_nd in + let check_nd = Lustre_utils.check_eq new_node orig_node in let check_top = Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd) in - Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]); + Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]) + +let node_to_lustre basename prog m sw_init sw_step init_out update_out = + let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in + to_lustre basename prog new_node orig_nd + +let fun_to_lustre basename prog m update_out = + let new_node, orig_nd = funsw_to_lustre m update_out in + to_lustre basename prog new_node orig_nd + diff --git a/src/tools/seal/seal_extract.ml b/src/tools/seal/seal_extract.ml index 8dcd86cd15e1015d868db0342d395ecd8937527a..b28fdb680aa1c72ff5d7d7b4d52bc5495745464b 100644 --- a/src/tools/seal/seal_extract.ml +++ b/src/tools/seal/seal_extract.ml @@ -91,6 +91,7 @@ let expr_to_z3_expr, zexpr_to_expr = * let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *) let rec e2ze e = + (* Format.eprintf "e2ze %a: %a@." Printers.pp_expr e Types.print_ty e.expr_type; *) if mem_expr e then ( get_zexpr e ) @@ -121,7 +122,11 @@ let expr_to_z3_expr, zexpr_to_expr = ) ) | Expr_appl (id,args, None) (* no reset *) -> - let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in + let el = Corelang.expr_list_of_expr args in + + let eltyp = List.map (fun e -> e.expr_type) el in + let elv = List.map e2ze el in + let z3e = Zustre_common.horn_basic_app id elv (eltyp, e.expr_type) in add_expr e z3e; z3e | Expr_tuple [e] -> @@ -597,6 +602,7 @@ let rec rewrite defs expr : elem_guarded_expr list = expr.expr_loc (Expr_appl(id, deelem e, None)) in + let new_e = { new_e with expr_type = expr.expr_type; expr_clock = expr.expr_clock } in guards, Expr (Corelang.partial_eval new_e) ) args @@ -905,18 +911,15 @@ let rec build_switch_sys "@[<v 2>===> @[%t@ @]@]@ @]@ " (fun fmt -> List.iter (fun (gl,up) -> Format.fprintf fmt "[@[%a@]] -> (%a)@ " - (pp_guard_list Printers.pp_expr) gl pp_up up) res); + (pp_guard_list Printers.pp_expr) gl (pp_up Printers.pp_expr) up) res); )); res - -(* Take a normalized node and extract a list of switches: (cond, - update) meaning "if cond then update" where update shall define all - node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *) -let node_as_switched_sys consts (mems:var_decl list) nd = - Z3.Params.update_param_value !ctx "timeout" "10000"; +let build_environement consts (mems:var_decl list) nd = + + Z3.Params.update_param_value !ctx "timeout" "10000"; (* rescheduling node: has been scheduled already, no need to protect @@ -1018,69 +1021,188 @@ let node_as_switched_sys consts (mems:var_decl list) nd = (pp_guard_expr pp_elem)) mdefs )) mem_defs); - (* Format.eprintf "Split init@."; *) - let init_defs, update_defs = - split_init mem_defs + mem_defs, output_defs + + +(* Iter through the elements and gather them by updates *) +let merge_updates sys = + (* The map will associate to each update up the pair (set, set + list) where set is the share guards and set list a list of + disjunctive guards. Each set represents a conjunction of + expressions. *) + + (* We perform multiple pass to avoid errors *) + let map = + List.fold_left (fun map (gl,up) -> + (* creating a new set to describe gl *) + let new_set = + List.fold_left + (fun set g -> Guards.add g set) + Guards.empty + gl + in + (* updating the map with up -> new_set *) + if UpMap.mem up map then + let guard_set = UpMap.find up map in + UpMap.add up (new_set::guard_set) map + else + UpMap.add up [new_set] map + ) UpMap.empty sys in - let init_out, update_out = - split_init output_defs + + (* Processing the set of guards leading to the same update: return + conj, disj with conf is a set of guards, and disj a DNF, ie a + list of set of guards *) + let map = + UpMap.map ( + fun guards -> + match guards with + | [] -> Guards.empty, [] (* Nothing *) + | [s]-> s, [] (* basic case *) + | hd::tl -> + let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in + let remaining = List.map (fun s -> Guards.diff s shared) guards in + (* If one of them is empty, we can remove the others, otherwise keep them *) + if List.exists Guards.is_empty remaining then + shared, [] + else + shared, remaining + ) map in - report ~level:3 - (fun fmt -> - Format.fprintf fmt - "@[<v 0>Init:@ %a@]@." - (Utils.fprintf_list ~sep:"@ " - (fun fmt (m,mdefs) -> - Format.fprintf fmt - "%s -> @[<v 0>[%a@] ]@ " - m - (Utils.fprintf_list ~sep:"@ " - (pp_guard_expr pp_elem)) mdefs - )) - init_defs); - report ~level:3 - (fun fmt -> - Format.fprintf fmt - "@[<v 0>Step:@ %a@]@." - (Utils.fprintf_list ~sep:"@ " - (fun fmt (m,mdefs) -> - Format.fprintf fmt - "%s -> @[<v 0>[%a@] ]@ " - m - (Utils.fprintf_list ~sep:"@ " - (pp_guard_expr pp_elem)) mdefs - )) - update_defs); - (* Format.eprintf "Build init@."; *) - - report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ...@."); - let sw_init= - build_switch_sys init_defs [] + let rec mk_binop op l = match l with + [] -> assert false + | [e] -> e + | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl] in - (* Format.eprintf "Build step@."; *) - let sw_sys = - build_switch_sys update_defs [] + let gl_as_expr gl = + let gl = Guards.elements gl in + let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in + match gl with + [] -> [] + | [e] -> [export e] + | _ -> + [mk_binop "&&" + (List.map export gl)] in - report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ... done@."); + let rec clean_disj disj = + match disj with + | [] -> [] + | [_] -> assert false (* A disjunction with a single case can be ignored *) + | _::_::_ -> ( + (* First basic version: producing a DNF One can later, (1) + simplify it with z3, or (2) build the compact tree with + maximum shared subexpression (and simplify it with z3) *) + let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in + let or_expr = mk_binop "||" elems in + [or_expr] - report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ...@."); - let init_out = - build_switch_sys init_out [] - in - (* report ~level:1 (fun fmt -> Format.fprintf fmt "Build step out@."); *) - let update_out = - build_switch_sys update_out [] + (* TODO disj*) + (* get the item that occurs in most case *) + (* List.fold_left (fun accu s -> + * List.fold_left (fun accu (e,b) -> + * if List.mem_assoc (e.expr_tag, b) + * ) accu (Guards.elements s) + * ) [] disj *) + + ) in - report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ... done@."); + if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map); + UpMap.fold (fun up (common, disj) accu -> + if !seal_debug then + report ~level:6 (fun fmt -> Format.fprintf fmt + "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@." + Guards.pp_short common + (fprintf_list ~sep:";@ " Guards.pp_long) disj + UpMap.pp up); + let disj = clean_disj disj in + let guard_expr = (gl_as_expr common)@disj in + + ((match guard_expr with + | [] -> None + | _ -> Some (mk_binop "&&" guard_expr)), up)::accu + ) map [] + + + - report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ...@."); +(* Take a normalized node and extract a list of switches: (cond, + update) meaning "if cond then update" where update shall define all + node memories. Everything as to be expressed over inputs or + memories, intermediate variables are removed through inlining *) +let node_as_switched_sys consts (mems:var_decl list) nd = + let mem_defs, output_defs = build_environement consts mems nd in + + let init_defs, update_defs = split_init mem_defs in + let init_out, update_out = split_init output_defs in + + report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 0>Init:@ %a@ Step:@ %a@]@." + (pp_assign_map pp_elem) init_defs + (pp_assign_map pp_elem) update_defs); + + + report ~level:1 (fun fmt -> Format.fprintf fmt + "init/step as a switched system ...@."); + let sw_init= build_switch_sys init_defs [] in + let sw_sys = build_switch_sys update_defs [] in + report ~level:1 (fun fmt -> Format.fprintf fmt + "init/step as a switched system ... done@."); + + + report ~level:1 (fun fmt -> Format.fprintf fmt + "output function as a switched system ...@."); + let init_out = build_switch_sys init_out [] in + let update_out = build_switch_sys update_out [] in + + report ~level:1 (fun fmt -> Format.fprintf fmt + "output function as a switched system ... done@."); + + report ~level:1 (fun fmt -> Format.fprintf fmt + "removing dead branches and merging remaining ...@."); let sw_init = clean_sys sw_init in let sw_sys = clean_sys sw_sys in let init_out = clean_sys init_out in let update_out = clean_sys update_out in - report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ... done@."); + + report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@."); + let sw_init = merge_updates sw_init in + report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@."); + let sw_sys = merge_updates sw_sys in + report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@."); + let init_out = merge_updates init_out in + report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@."); + let update_out = merge_updates update_out in + report ~level:1 (fun fmt -> + Format.fprintf fmt "removing dead branches and merging remaining ... done@."); + + sw_init , sw_sys, init_out, update_out + + +let fun_as_switched_sys consts nd = + let _, update_out = build_environement consts [] nd in + + report ~level:1 (fun fmt -> Format.fprintf fmt + "output function as a switched system ...@."); + let update_out = build_switch_sys update_out [] in + report ~level:1 (fun fmt -> Format.fprintf fmt + "output function as a switched system ... done@."); + + report ~level:1 (fun fmt -> Format.fprintf fmt + "removing dead branches and merging remaining ...@."); + let update_out = clean_sys update_out in + let update_out = merge_updates update_out in + report ~level:1 (fun fmt -> + Format.fprintf fmt "removing dead branches and merging remaining ... done@."); + + update_out + + + + + + (* Some code that was used to check for duplicate entries in guards. + (* Some additional checks *) @@ -1156,118 +1278,4 @@ let node_as_switched_sys consts (mems:var_decl list) nd = end; - (* Iter through the elements and gather them by updates *) - let process sys = - (* The map will associate to each update up the pair (set, set - list) where set is the share guards and set list a list of - disjunctive guards. Each set represents a conjunction of - expressions. *) - report ~level:3 (fun fmt -> Format.fprintf fmt "%t@." - (fun fmt -> List.iter (fun (gl,up) -> - Format.fprintf fmt "[@[%a@]] -> (%a)@ " - (pp_guard_list Printers.pp_expr) gl pp_up up) sw_init)); - - (* We perform multiple pass to avoid errors *) - let map = - List.fold_left (fun map (gl,up) -> - (* creating a new set to describe gl *) - let new_set = - List.fold_left - (fun set g -> Guards.add g set) - Guards.empty - gl - in - (* updating the map with up -> new_set *) - if UpMap.mem up map then - let guard_set = UpMap.find up map in - UpMap.add up (new_set::guard_set) map - else - UpMap.add up [new_set] map - ) UpMap.empty sys - in - (* Processing the set of guards leading to the same update: return - conj, disj with conf is a set of guards, and disj a DNF, ie a - list of set of guards *) - let map = - UpMap.map ( - fun guards -> - match guards with - | [] -> Guards.empty, [] (* Nothing *) - | [s]-> s, [] (* basic case *) - | hd::tl -> - let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in - let remaining = List.map (fun s -> Guards.diff s shared) guards in - (* If one of them is empty, we can remove the others, otherwise keep them *) - if List.exists Guards.is_empty remaining then - shared, [] - else - shared, remaining - ) map - in - let rec mk_binop op l = match l with - [] -> assert false - | [e] -> e - | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl] - in - let gl_as_expr gl = - let gl = Guards.elements gl in - let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in - match gl with - [] -> [] - | [e] -> [export e] - | _ -> - [mk_binop "&&" - (List.map export gl)] - in - let rec clean_disj disj = - match disj with - | [] -> [] - | [_] -> assert false (* A disjunction was a single case can be ignored *) - | _::_::_ -> ( - (* First basic version: producing a DNF One can later, (1) - simplify it with z3, or (2) build the compact tree with - maximum shared subexpression (and simplify it with z3) *) - let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in - let or_expr = mk_binop "||" elems in - [or_expr] - - - (* TODO disj*) - (* get the item that occurs in most case *) - (* List.fold_left (fun accu s -> - * List.fold_left (fun accu (e,b) -> - * if List.mem_assoc (e.expr_tag, b) - * ) accu (Guards.elements s) - * ) [] disj *) - - ) - in - if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map); - UpMap.fold (fun up (common, disj) accu -> - if !seal_debug then - report ~level:6 (fun fmt -> Format.fprintf fmt - "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@." - Guards.pp_short common - (fprintf_list ~sep:";@ " Guards.pp_long) disj - UpMap.pp up); - let disj = clean_disj disj in - let guard_expr = (gl_as_expr common)@disj in - - ((match guard_expr with - | [] -> None - | _ -> Some (mk_binop "&&" guard_expr)), up)::accu - ) map [] - - in - - - - report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@."); - let sw_init = process sw_init in - report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@."); - let sw_sys = process sw_sys in - report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@."); - let init_out = process init_out in - report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@."); - let update_out = process update_out in - sw_init , sw_sys, init_out, update_out + *) diff --git a/src/tools/seal/seal_utils.ml b/src/tools/seal/seal_utils.ml index 5829323effae1704d2c287ca862b613f8a926cc1..52089a7562932155395ad125f129047910f17d50 100644 --- a/src/tools/seal/seal_utils.ml +++ b/src/tools/seal/seal_utils.ml @@ -28,13 +28,20 @@ let pp_guard_list pp_elem fmt gl = (fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl let pp_guard_expr pp_elem fmt (gl,e) = - Format.fprintf fmt "@[%a@] -> @[<hov 2>%a@]" + Format.fprintf fmt "@[<v 2>@[%a@] ->@ @[<hov 2>%a@]@]" (pp_guard_list pp_elem) gl pp_elem e let pp_mdefs pp_elem fmt gel = fprintf_list ~sep:"@ " (pp_guard_expr pp_elem) fmt gel - +let pp_assign_map pp_elem = + fprintf_list ~sep:"@ " + (fun fmt (m, mdefs) -> + Format.fprintf fmt + "%s -> @[<v 0>[%a@] ]@ " + m + (pp_mdefs pp_elem) mdefs + ) let deelem e = match e with Expr e -> e @@ -53,15 +60,25 @@ let pp_gl pp_expr = fprintf_list ~sep:", " (fun fmt (e,b) -> Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e) let pp_gl_short = pp_gl (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) -let pp_up fmt up = List.iter (fun (id,e) -> Format.fprintf fmt "%s->%i; " id e.expr_tag) up -let pp_sys fmt sw = List.iter (fun (gl,up) -> - match gl with - | None -> - pp_up fmt up - | Some gl -> - Format.fprintf fmt "[@[%a@]] -> (%a)@ " - Printers.pp_expr gl pp_up up) sw +let pp_up pp_elem fmt up = + fprintf_list ~sep:"@ " + (fun fmt (id,e) -> Format.fprintf fmt "%s == %a;@ " id pp_elem e) + fmt + up + +let pp_sys pp_elem fmt sw = + fprintf_list ~sep:"@ " + (fun fmt (gl,up) -> + match gl with + | None -> + (pp_up pp_elem) fmt up + | Some gl -> + Format.fprintf fmt "@[<v 2>[@[%a@]]:@ %a@]" + Printers.pp_expr gl (pp_up pp_elem) up) + fmt + sw + let pp_all_defs = (Utils.fprintf_list ~sep:",@ " (fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]" @@ -76,7 +93,7 @@ module UpMap = let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in compare (proj l1) (proj l2) end) - let pp = pp_up + let pp = pp_up Printers.pp_expr end module Guards = struct diff --git a/src/tools/seal/seal_verifier.ml b/src/tools/seal/seal_verifier.ml index 45aea72b325cd2e82251dfe13666964334631cfe..4802d2179f16a3ccec37bec0b1aab24342dd9b89 100644 --- a/src/tools/seal/seal_verifier.ml +++ b/src/tools/seal/seal_verifier.ml @@ -1,13 +1,3 @@ -open Seal_slice -open Seal_extract -open Seal_utils - -let active = ref false -let seal_export = ref None - -let set_export s = match s with - | "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s - | _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1) (* TODO - build the output function: for the moment we slice the node with @@ -35,6 +25,18 @@ let set_export s = match s with the property to prove *) + + +open Seal_slice +open Seal_extract +open Seal_utils + +let active = ref false +let seal_export = ref None + +let set_export s = match s with + | "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s + | _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1) (* Select the appropriate node, should have been inlined already and extract update/output functions. *) @@ -64,73 +66,73 @@ let seal_run ~basename prog machines = in let m = Machine_code_common.get_machine machines node_name in let nd = m.mname in - (* Format.eprintf "Node %a@." Printers.pp_node nd; *) let mems = m.mmemory in + report ~level:1 (fun fmt -> Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id (List.length mems)); - (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *) + + (* Slicing node *) let msch = Utils.desome m.msch in - (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *) let sliced_nd = slice_node (mems@nd.node_outputs) msch nd in - if false then Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@."); + report ~level:10 (fun fmt -> Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd); let consts = Corelang.(List.map const_of_top (get_consts prog)) in - let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in - let pp_res pp_expr = - (Utils.fprintf_list ~sep:"@ " - (fun fmt (g, up) -> - Format.fprintf fmt "@[<v 2>[%t]:@ %a@]" - (fun fmt -> match g with None -> () | Some g -> pp_expr fmt g) - - (* (Utils.fprintf_list ~sep:"; " - * (fun fmt (e,b) -> - * if b then pp_expr fmt e - * else Format.fprintf fmt "not(%a)" - * pp_expr e)) gel *) - (Utils.fprintf_list ~sep:";@ " - (fun fmt (id, e) -> - Format.fprintf fmt "%s = @[<hov 0>%a@]" - id - pp_expr e)) up - )) - in - report ~level:1 ( - fun fmt -> Format.fprintf fmt - "%i memories, %i init, %i step switch cases@." - (List.length mems) - (List.length sw_init) - (List.length sw_sys) - - ); - report ~level:1 (fun fmt -> - (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) in*) - let pp_res = pp_res Printers.pp_expr in - Format.fprintf fmt "DynSys:@ @[<v 0>@[<v 3>Init:@ %a@]@ " - pp_res sw_init; - Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@." - pp_res sw_sys - ); - - - - report ~level:1 (fun fmt -> - (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) in*) - let pp_res = pp_res Printers.pp_expr in - Format.fprintf fmt "Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ " - (List.length init_out) - (List.length update_out) - pp_res init_out; - Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@." - pp_res update_out - ); - let _ = match !seal_export with - | Some "lustre" | Some "lus" -> - Seal_export.to_lustre basename prog m sw_init sw_sys init_out update_out - | Some "matlab" | Some "m" -> assert false (* TODO *) - | Some _ -> assert false - | None -> () - in - () + + let pp_sys = pp_sys Printers.pp_expr in + if List.length mems = 0 then + begin (* A stateless node = a function ! *) + + let update_out = fun_as_switched_sys consts sliced_nd in + + report ~level:1 (fun fmt -> + Format.fprintf fmt + "Output (%i step switch cases):@ @[<v 0>%a@]@." + (List.length update_out) + pp_sys update_out + ); + + let _ = match !seal_export with + | Some "lustre" | Some "lus" -> + Seal_export.fun_to_lustre basename prog m update_out + | Some "matlab" | Some "m" -> assert false (* TODO *) + | Some _ -> assert false + | None -> () + in + () + end + else + begin (* A stateful node *) + + let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in + + report ~level:1 (fun fmt -> + Format.fprintf fmt + "DynSys: (%i memories, %i init, %i step switch cases)@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@." + (List.length mems) + (List.length sw_init) + (List.length sw_sys) + pp_sys sw_init + pp_sys sw_sys + ); + + report ~level:1 (fun fmt -> + Format.fprintf fmt + "Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@." + (List.length init_out) + (List.length update_out) + pp_sys init_out + pp_sys update_out + ); + + let _ = match !seal_export with + | Some "lustre" | Some "lus" -> + Seal_export.node_to_lustre basename prog m sw_init sw_sys init_out update_out + | Some "matlab" | Some "m" -> assert false (* TODO *) + | Some _ -> assert false + | None -> () + in + () + end module Verifier = (struct @@ -151,7 +153,7 @@ module Verifier = let is_active () = !active let run = seal_run - - + + end: VerifierType.S) diff --git a/src/tools/zustre/zustre_common.ml b/src/tools/zustre/zustre_common.ml index 12fe2358271cdbf4d382cd0f2f36b5edcbea6b15..d8eed30ae6b272cb840aac84e2c4805d46510be4 100644 --- a/src/tools/zustre/zustre_common.ml +++ b/src/tools/zustre/zustre_common.ml @@ -5,7 +5,9 @@ open Format (* open Horn_backend_common * open Horn_backend *) open Zustre_data - + +let report = Log.report ~plugin:"z3 interface" + module HBC = Horn_backend_common let node_name = HBC.node_name @@ -111,7 +113,7 @@ let register_fdecl id fd = Hashtbl.add decls id fd let get_fdecl id = try Hashtbl.find decls id - with Not_found -> (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found) + with Not_found -> (report ~level:3 (fun fmt -> Format.fprintf fmt "Unable to find func_decl %s@.@?" id); raise Not_found) let pp_fdecls fmt = Format.fprintf fmt "Registered fdecls: @[%a@]@ " @@ -124,6 +126,13 @@ let decl_var id = register_fdecl id.var_id fdecl; fdecl +(* Declaring the function used in expr *) +let decl_fun op args typ = + let args = List.map type_to_sort args in + let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in + register_fdecl op fdecl; + fdecl + let idx_sort = int_sort let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort let uid_conc = @@ -242,133 +251,107 @@ let rec horn_default_val t = (* Conversion of basic library functions *) -let horn_basic_app i val_to_expr vl = +let horn_basic_app i vl (vltyp, typ) = match i, vl with - | "ite", [v1; v2; v3] -> - Z3.Boolean.mk_ite - !ctx - (val_to_expr v1) - (val_to_expr v2) - (val_to_expr v3) - - | "uminus", [v] -> - Z3.Arithmetic.mk_unary_minus - !ctx - (val_to_expr v) + | "ite", [v1; v2; v3] -> Z3.Boolean.mk_ite !ctx v1 v2 v3 + | "uminus", [v] -> Z3.Arithmetic.mk_unary_minus + !ctx v | "not", [v] -> Z3.Boolean.mk_not - !ctx - (val_to_expr v) + !ctx v | "=", [v1; v2] -> Z3.Boolean.mk_eq - !ctx - (val_to_expr v1) - (val_to_expr v2) + !ctx v1 v2 | "&&", [v1; v2] -> Z3.Boolean.mk_and !ctx - [val_to_expr v1; - val_to_expr v2] + [v1; v2] | "||", [v1; v2] -> Z3.Boolean.mk_or !ctx - [val_to_expr v1; - val_to_expr v2] + [v1; + v2] | "impl", [v1; v2] -> Z3.Boolean.mk_implies - !ctx - (val_to_expr v1) - (val_to_expr v2) + !ctx v1 v2 | "mod", [v1; v2] -> Z3.Arithmetic.Integer.mk_mod - !ctx - (val_to_expr v1) - (val_to_expr v2) + !ctx v1 v2 | "equi", [v1; v2] -> Z3.Boolean.mk_eq !ctx - (val_to_expr v1) - (val_to_expr v2) + v1 v2 | "xor", [v1; v2] -> Z3.Boolean.mk_xor - !ctx - (val_to_expr v1) - (val_to_expr v2) + !ctx v1 v2 | "!=", [v1; v2] -> Z3.Boolean.mk_not !ctx ( Z3.Boolean.mk_eq - !ctx - (val_to_expr v1) - (val_to_expr v2) + !ctx v1 v2 ) | "/", [v1; v2] -> Z3.Arithmetic.mk_div - !ctx - (val_to_expr v1) - (val_to_expr v2) + !ctx v1 v2 | "+", [v1; v2] -> Z3.Arithmetic.mk_add !ctx - [val_to_expr v1; val_to_expr v2] - + [v1; v2] | "-", [v1; v2] -> Z3.Arithmetic.mk_sub !ctx - [val_to_expr v1 ; val_to_expr v2] + [v1 ; v2] | "*", [v1; v2] -> Z3.Arithmetic.mk_mul !ctx - [val_to_expr v1; val_to_expr v2] + [ v1; v2] | "<", [v1; v2] -> Z3.Arithmetic.mk_lt - !ctx - (val_to_expr v1) - (val_to_expr v2) - + !ctx v1 v2 | "<=", [v1; v2] -> Z3.Arithmetic.mk_le - !ctx - (val_to_expr v1) - (val_to_expr v2) - + !ctx v1 v2 | ">", [v1; v2] -> Z3.Arithmetic.mk_gt - !ctx - (val_to_expr v1) - (val_to_expr v2) - + !ctx v1 v2 | ">=", [v1; v2] -> Z3.Arithmetic.mk_ge - !ctx - (val_to_expr v1) - (val_to_expr v2) - + !ctx v1 v2 | "int_to_real", [v1] -> Z3.Arithmetic.Integer.mk_int2real - !ctx - (val_to_expr v1) - + !ctx v1 + | _ -> + let fd = + try + get_fdecl i + with Not_found -> begin + 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); + decl_fun i vltyp typ + end + in + Z3.FuncDecl.apply fd vl + (* | _, [v1; v2] -> Z3.Boolean.mk_and * !ctx * (val_to_expr v1) * (val_to_expr v2) * * Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) - | _ -> ( - let msg fmt = Format.fprintf fmt - "internal error: zustre unkown function %s (nb args = %i)@." - i (List.length vl) - in - raise (UnknownFunction(i, msg)) - ) + +(* | _ -> ( + * let msg fmt = Format.fprintf fmt + * "internal error: zustre unkown function %s (nb args = %i)@." + * i (List.length vl) + * in + * raise (UnknownFunction(i, msg)) + * ) *) (* Convert a value expression [v], with internal function calls only. [pp_var] @@ -376,6 +359,7 @@ let horn_basic_app i val_to_expr vl = may be added for array variables *) let rec horn_val_to_expr ?(is_lhs=false) m self v = + (* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *) match v.value_desc with | Cst c -> horn_const_to_expr c @@ -425,7 +409,7 @@ let rec horn_val_to_expr ?(is_lhs=false) m self v = (rename_machine self v) - | Fun (n, vl) -> horn_basic_app n (horn_val_to_expr m self) vl + | 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) let no_reset_to_exprs machines m i = let (n,_) = List.assoc i m.minstances in