### Profile

1 2 3 5778dd5e ploc ```(* ``` ```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 ``` ```*) ``` 9c4cc944 Corentin Lauverjat ```open Lustrec ``` 5778dd5e ploc ```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"; ``` 4300981b ploc ``` "-timeout", Arg.Set_int timeout, "Set timeout in ms (default 10000 = 10 s)"; ``` 5778dd5e ploc ``` "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)"; ``` 4300981b ploc ``` "-debug", Arg.Set debug, "Debug mode"; ``` 5778dd5e ploc ``` ] ``` ``` ``` ``` let activate () = ( ``` ``` active := true; ``` 9c4cc944 Corentin Lauverjat ``` Lustrec.Options.output := "horn"; ``` 5778dd5e ploc ``` ) ``` 57d61d67 ploc 5778dd5e ploc ``` let is_active () = !active ``` ``` let get_normalization_params () = ``` ``` (* make sure the output is "Horn" *) ``` 9c4cc944 Corentin Lauverjat ``` assert(!Lustrec.Options.output = "horn"); ``` 5778dd5e ploc ``` 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; *) ``` 4300981b ploc 5778dd5e ploc ``` let module P = Z3.Params in ``` ``` let module S = Z3.Symbol in ``` ``` let mks = S.mk_string !ctx in ``` 4300981b ploc ``` ``` ``` (* Fixpoint Engine parameters *) ``` ``` ``` ``` let fp_params = P.mk_params !ctx in ``` 5778dd5e ploc 51ec4e8c ploc ``` (* (\* self.fp.set (engine='spacer') *\) *) ``` 4300981b ploc ``` P.add_symbol fp_params (mks "engine") (mks "spacer"); ``` ``` (* P.add_symbol fp_params (mks "engine") (mks "pdr"); *) ``` 5778dd5e ploc ``` ``` ``` (* #z3.set_option(rational_to_decimal=True) *) ``` ``` (* #self.fp.set('precision',30) *) ``` ``` if !param_stat then ``` ``` (* self.fp.set('print_statistics',True) *) ``` 4300981b ploc ``` P.add_bool fp_params (mks "print_statistics") true; ``` 5778dd5e ploc ``` (* 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) *) ``` 4300981b ploc ``` (* P.add_bool fp_params (mks "use_heavy_mev") true; *) ``` 5778dd5e ploc ``` ``` ``` (* self.fp.set('pdr.flexible_trace',True) *) ``` 4300981b ploc ``` P.add_bool fp_params (mks "pdr.flexible_trace") true; ``` 5778dd5e ploc ``` (* self.fp.set('reset_obligation_queue',False) *) ``` 4300981b ploc ``` P.add_bool fp_params (mks "spacer.reset_obligation_queue") false; ``` 5778dd5e ploc ``` (* self.fp.set('spacer.elim_aux',False) *) ``` 4300981b ploc ``` P.add_bool fp_params (mks "spacer.elim_aux") false; ``` 5778dd5e ploc ``` (* if self.args.eldarica: ``` ``` * self.fp.set('print_fixedpoint_extensions', False) *) ``` ``` if !param_eldarica then ``` 4300981b ploc ``` P.add_bool fp_params (mks "print_fixedpoint_extensions") false; ``` 5778dd5e ploc ``` ``` ``` (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *) ``` ``` if !param_utvpi then ``` 4300981b ploc ``` P.add_bool fp_params (mks "pdr.utvpi") false; ``` 5778dd5e ploc ``` (* if self.args.tosmt: ``` ``` * self.log.info("Setting low level printing") ``` ``` * self.fp.set ('print.low_level_smt2',True) *) ``` ``` if !param_tosmt then ``` 4300981b ploc ``` P.add_bool fp_params (mks "print.low_level_smt2") true; ``` 5778dd5e ploc ``` (* 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) *\) *) ``` 57d61d67 ploc ``` if not !param_pp then ( ``` ``` (* Mandatory to print all steps and recover cex *) ``` 4300981b ploc ``` P.add_bool fp_params (mks "xform.slice") false; ``` ``` P.add_bool fp_params (mks "xform.inline_linear") false; ``` ``` P.add_bool fp_params (mks "xform.inline_eager") false ``` 5778dd5e ploc ``` ); ``` 4300981b ploc ``` (* Ploc's options. Do not seem to have any effect yet *) ``` ``` P.add_bool fp_params (mks "print_answer") true; ``` 57d61d67 ploc ``` (* P.add_bool fp_params (mks "print_certificate") true; *) ``` ``` P.add_bool fp_params (mks "xform.slice") false ; (* required to preserve signatures *) ``` ``` (* P.add_bool fp_params (mks "print_statistics") true; *) ``` ``` (* P.add_bool fp_params (mks "print_certificate") true; *) ``` 4300981b ploc ``` (* Adding a timeout *) ``` ``` P.add_int fp_params (mks "timeout") !timeout; ``` ``` Z3.Fixedpoint.set_parameters !fp fp_params ``` 5778dd5e ploc ``` ``` 7a4fd94d ploc ``` let run ~basename prog machines = ``` 9c4cc944 Corentin Lauverjat ``` let machines = Lustrec.Machine_code_common.arrow_machine::machines in ``` 5778dd5e ploc ``` let machines = preprocess machines in ``` ``` setup_solver (); ``` ``` (* TODO ``` ``` load deps: cf print_dep in horn_backend.ml ``` ea758c12 ploc ``` ``` 5778dd5e ploc ``` if false then ( ``` ``` ``` 57d61d67 ploc ``` let queries = Z3.Fixedpoint.parse_file !fp "nstep.smt2" in ``` 5778dd5e ploc 51ec4e8c ploc ``` (* Debug instructions *) ``` ``` ``` 5778dd5e ploc 51ec4e8c ploc ``` ``` ``` let rules_expr = Z3.Fixedpoint.get_rules !fp in ``` ``` Format.eprintf "@[Registered rules:@ %a@ @]@." ``` 9c4cc944 Corentin Lauverjat ``` (Lustrec.Utils.fprintf_list ~sep:"@ " ``` 51ec4e8c ploc ``` (fun fmt e -> ``` ``` (* let e2 = Z3.Quantifier.get_body eq in *) ``` ``` (* let fd = Z3.Expr.get_func_decl e in *) ``` ``` Format.fprintf fmt "Rule: %s@." ``` ``` (Z3.Expr.to_string e); ``` ``` )) rules_expr; ``` ``` ``` ``` let _ = List.map extract_expr_fds rules_expr in ``` ``` Format.eprintf "%t" pp_fdecls; ``` 57d61d67 ploc ``` let decl_err = List.hd queries in ``` ``` let res_status = Z3.Fixedpoint.query !fp decl_err in ``` 51ec4e8c ploc ``` ``` 57d61d67 ploc ``` Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status); ``` ``` (* let _ = *) ``` ``` (* match res_status with *) ``` ``` (* | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err *) ``` ``` (* | _ -> () *) ``` ``` (* in *) ``` ``` exit 0 ``` 5778dd5e ploc ``` ) ``` 51ec4e8c ploc ``` else if false then ( ``` ``` (* No queries here *) ``` ``` let _ = Z3.Fixedpoint.parse_file !fp "mini_decl.smt2" in ``` ``` (* Debug instructions *) ``` ``` ``` ``` ``` ``` let rules_expr = Z3.Fixedpoint.get_rules !fp in ``` ``` Format.eprintf "@[Registered rules:@ %a@ @]@." ``` 9c4cc944 Corentin Lauverjat ``` (Lustrec.Utils.fprintf_list ~sep:"@ " ``` 51ec4e8c ploc ``` (fun fmt e -> ``` ``` (* let e2 = Z3.Quantifier.get_body eq in *) ``` ``` (* let fd = Z3.Expr.get_func_decl e in *) ``` ``` Format.fprintf fmt "Rule: %s@." ``` ``` (Z3.Expr.to_string e); ``` ``` )) rules_expr; ``` ``` ``` ``` let _ = List.map extract_expr_fds rules_expr in ``` ``` Format.eprintf "%t" pp_fdecls; ``` 9c4cc944 Corentin Lauverjat ``` if !Lustrec.Options.main_node <> "" then ``` 51ec4e8c ploc ``` begin ``` 9c4cc944 Corentin Lauverjat ``` Zustre_analyze.check machines !Lustrec.Options.main_node ``` 51ec4e8c ploc ``` end ``` ``` else ``` ``` failwith "Require main node"; ``` ``` () ``` ``` ) ``` ea758c12 ploc ``` else ``` ``` *) ``` ``` ( ``` 5778dd5e ploc ``` ``` ``` ``` 51ec4e8c ploc ``` decl_sorts (); ``` ``` ``` ``` List.iter (decl_machine machines) (List.rev machines); ``` 5778dd5e ploc 51ec4e8c ploc ``` (* (\* Debug instructions *\) *) ``` ``` (* let rules_expr = Z3.Fixedpoint.get_rules !fp in *) ``` ``` (* Format.eprintf "@[Registered rules:@ %a@ @]@." *) ``` 9c4cc944 Corentin Lauverjat ``` (* (Lustrec.Utils.fprintf_list ~sep:"@ " *) ``` 51ec4e8c ploc ``` (* (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *) ``` ``` (* rules_expr; *) ``` 5778dd5e ploc 9c4cc944 Corentin Lauverjat ``` if !Lustrec.Options.main_node <> "" then ``` 51ec4e8c ploc ``` begin ``` 9c4cc944 Corentin Lauverjat ``` Zustre_analyze.check machines !Lustrec.Options.main_node ``` 5778dd5e ploc 51ec4e8c ploc ``` end ``` ``` else ``` ``` failwith "Require main node"; ``` ``` ``` ``` () ``` 5778dd5e ploc ``` ) ``` ``` ``` 51ec4e8c ploc ``` end: VerifierType.S) ``` 5778dd5e ploc ``` ``` ```(* Local Variables: *) ``` 57d61d67 ploc ```(* compile-command:"make -C ../.. lustrev" *) ``` 5778dd5e ploc ```(* End: *) ```