### Profile

 1 ```(* ``` ```TODO ``` ```A property/contract is attached to a node foo and could be analyzed ``` ```- while considering the exact semantics ``` ```- while substituting some callee by their definition (doing it incrementaly ?) ``` ```- the returned cex could be given at node level ``` ```- or while considering a main node and producing the output at the main node level ``` ```One can consider the following algorithm: ``` ```- main node foo, local node bar, with a target property/contract ``` ```- declare bar using only the contract of its subnodes (callee) ``` ```- if the property is valid, ``` ``` - check the validity status of the subnode contracts used ``` ``` - if one is not proved, perform the analysis again (of bar contract) using ``` ``` the actual definition of the unproven contract ``` ``` - return the computed invariants with the dependencies (subcontracts assumed, subcontracts proved) ``` ```- if the property is invalid ``` ``` - check invalidity wrt to full definition of the node bar (with the actual definition of its subnodes) ``` ``` - return the cex ``` ``` - try to see if the cex (or a similar violation of the contract) is reachable from its parents ``` ``` (up to main node foo) ``` ``` ``` ```Other features: ``` ```- check equivalence btw two nodes, provided an equivalence map on some callee ``` ``` (A equiv B) with map (A id equiv B id) ``` ``` - substitute each callee appearing B nodes ``` ```Analysis: ``` ``` - take a main definition, a boolean proposition, and build the collecting semantics ``` ``` - then check that the proposition remains valid ``` ```*) ``` ```open Zustre_common ``` ```open Zustre_data ``` ```let param_stat = ref false ``` ```let param_eldarica = ref false ``` ```let param_utvpi = ref false ``` ```let param_tosmt = ref false ``` ```let param_pp = ref false ``` ```let active = ref false ``` ```module Verifier = ``` ``` (struct ``` ``` include VerifierType.Default ``` ``` let name = "zustre" ``` ``` let options = [ ``` ``` "-stat", Arg.Set param_stat, "print statistics"; ``` ``` "-eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules"; ``` ``` "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy"; ``` ``` "-tosmt", Arg.Set param_tosmt, "Print low-level (possibly unreadable) SMT2 statements"; ``` ``` "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)"; ``` ``` ] ``` ``` ``` ``` let activate () = ( ``` ``` active := true; ``` ``` Options.output := "horn"; ``` ``` ) ``` ``` let is_active () = !active ``` ``` let get_normalization_params () = ``` ``` (* make sure the output is "Horn" *) ``` ``` assert(!Options.output = "horn"); ``` ``` Backends.get_normalization_params () ``` ``` let setup_solver () = ``` ``` fp := Z3.Fixedpoint.mk_fixedpoint !ctx; ``` ``` (* let help = Z3.Fixedpoint.get_help fp in ``` ``` * Format.eprintf "Fp help : %s@." help; ``` ``` * ``` ``` * let solver =Z3.Solver.mk_solver !ctx None in ``` ``` * let help = Z3.Solver.get_help solver in ``` ``` * Format.eprintf "Z3 help : %s@." help; *) ``` ``` ``` ``` let module P = Z3.Params in ``` ``` let module S = Z3.Symbol in ``` ``` let mks = S.mk_string !ctx in ``` ``` let params = P.mk_params !ctx in ``` ``` (* self.fp.set (engine='spacer') *) ``` ``` P.add_symbol params (mks "engine") (mks "spacer"); ``` ``` ``` ``` (* #z3.set_option(rational_to_decimal=True) *) ``` ``` (* #self.fp.set('precision',30) *) ``` ``` if !param_stat then ``` ``` (* self.fp.set('print_statistics',True) *) ``` ``` P.add_bool params (mks "print_statistics") true; ``` ``` (* Dont know where to find this parameter *) ``` ``` (* if !param_spacer_verbose then ``` ``` * if self.args.spacer_verbose: ``` ``` * z3.set_option (verbose=1) *) ``` ``` (* The option is not recogined*) ``` ``` (* self.fp.set('use_heavy_mev',True) *) ``` ``` (* P.add_bool params (mks "use_heavy_mev") true; *) ``` ``` ``` ``` (* self.fp.set('pdr.flexible_trace',True) *) ``` ``` P.add_bool params (mks "pdr.flexible_trace") true; ``` ``` (* self.fp.set('reset_obligation_queue',False) *) ``` ``` P.add_bool params (mks "spacer.reset_obligation_queue") false; ``` ``` (* self.fp.set('spacer.elim_aux',False) *) ``` ``` P.add_bool params (mks "spacer.elim_aux") false; ``` ``` (* if self.args.eldarica: ``` ``` * self.fp.set('print_fixedpoint_extensions', False) *) ``` ``` if !param_eldarica then ``` ``` P.add_bool params (mks "print_fixedpoint_extensions") false; ``` ``` ``` ``` (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *) ``` ``` if !param_utvpi then ``` ``` P.add_bool params (mks "pdr.utvpi") false; ``` ``` (* if self.args.tosmt: ``` ``` * self.log.info("Setting low level printing") ``` ``` * self.fp.set ('print.low_level_smt2',True) *) ``` ``` if !param_tosmt then ``` ``` P.add_bool params (mks "print.low_level_smt2") true; ``` ``` (* if not self.args.pp: ``` ``` * self.log.info("No pre-processing") ``` ``` * self.fp.set ('xform.slice', False) ``` ``` * self.fp.set ('xform.inline_linear',False) ``` ``` * self.fp.set ('xform.inline_eager',False) *\) *) ``` ``` if !param_pp then ( ``` ``` P.add_bool params (mks "xform.slice") false; ``` ``` P.add_bool params (mks "xform.inline_linear") false; ``` ``` P.add_bool params (mks "xform.inline_eager") false ``` ``` ); ``` ``` Z3.Fixedpoint.set_parameters !fp params ``` ``` ``` ``` ``` ``` let run basename prog machines = ``` ``` let machines = Machine_code_common.arrow_machine::machines in ``` ``` let machines = preprocess machines in ``` ``` setup_solver (); ``` ``` (* TODO ``` ``` load deps: cf print_dep in horn_backend.ml ``` ``` *) ``` ``` if false then ( ``` ``` ``` ``` let queries = Z3.Fixedpoint.parse_file !fp "mini.smt2" in ``` ``` (* Debug instructions *) ``` ``` let rules_expr = Z3.Fixedpoint.get_rules !fp in ``` ``` Format.eprintf "@[Registered rules:@ %a@ @]@." ``` ``` (Utils.fprintf_list ~sep:"@ " ``` ``` (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) ``` ``` rules_expr; ``` ``` let res_status = Z3.Fixedpoint.query !fp (List.hd queries )in ``` ``` ``` ``` Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status) ``` ``` ) ``` ``` else ( ``` ``` ``` ``` ``` ``` decl_sorts (); ``` ``` ``` ``` List.iter (decl_machine machines) (List.rev machines); ``` ``` (* (\* Debug instructions *\) *) ``` ``` (* let rules_expr = Z3.Fixedpoint.get_rules !fp in *) ``` ``` (* Format.eprintf "@[Registered rules:@ %a@ @]@." *) ``` ``` (* (Utils.fprintf_list ~sep:"@ " *) ``` ``` (* (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *) ``` ``` (* rules_expr; *) ``` ``` if !Options.main_node <> "" then ``` ``` begin ``` ``` Zustre_analyze.check machines !Options.main_node ``` ``` end ``` ``` else ``` ``` failwith "Require main node"; ``` ``` ``` ``` () ``` ``` ) ``` ``` ``` ``` end: VerifierType.S) ``` ``` ``` ```(* Local Variables: *) ``` ```(* compile-command:"make -C ../.." *) ``` ```(* End: *) ```