diff --git a/Makefile b/Makefile index d1fef2f4..aa3996fe 100644 --- a/Makefile +++ b/Makefile @@ -9,7 +9,7 @@ clean: dune clean test: - dune runtest -f + dune runtest --profile release -f install: dune build @install diff --git a/duet/cmdLine.ml b/duet/cmdLine.ml index 6842b513..7d36022e 100644 --- a/duet/cmdLine.ml +++ b/duet/cmdLine.ml @@ -27,6 +27,11 @@ let verbose_arg = Arg.String (fun v -> Log.set_verbosity_level v `info), " Raise verbosity for a particular module") +let trace_arg = + ("-trace", + Arg.String (fun v -> Log.set_verbosity_level v `trace), + " Set verbosity for a particular module to trace") + let verbose_list_arg = ("-verbose-list", Arg.Unit (fun () -> @@ -36,7 +41,7 @@ let verbose_list_arg = ) Log.loggers; exit 0; ), - " List modules which can be used with -verbose") + " List modules which can be used with -verbose/-trace") let stats_arg = ("-stats", Arg.Set show_stats, " Display statistics") @@ -113,6 +118,7 @@ let debug_args = ref let config_args = ref [ verbose_arg; + trace_arg; verbose_list_arg; verbosity_arg; stats_arg; diff --git a/duet/cra.ml b/duet/cra.ml index 9acde36a..96a2431f 100644 --- a/duet/cra.ml +++ b/duet/cra.ml @@ -90,45 +90,79 @@ let map_value f = function | VPos v -> VPos (f v) | VWidth v -> VWidth (f v) -module V = struct - module I = struct - type t = value [@@deriving ord] - let pp formatter = function - | VVal v -> Var.pp formatter v - | VWidth v -> Format.fprintf formatter "%a@@width" Var.pp v - | VPos v -> Format.fprintf formatter "%a@@pos" Var.pp v - let show = SrkUtil.mk_show pp - let equal x y = compare x y = 0 - let hash = function - | VVal v -> Hashtbl.hash (Var.hash v, 0) - | VPos v -> Hashtbl.hash (Var.hash v, 1) - | VWidth v -> Hashtbl.hash (Var.hash v, 2) - end - include I - - let sym_to_var = Hashtbl.create 991 - let var_to_sym = ValueHT.create 991 - - let typ v = tr_typ (Var.get_type (var_of_value v)) - - let symbol_of var = - if ValueHT.mem var_to_sym var then - ValueHT.find var_to_sym var - else begin - let sym = Ctx.mk_symbol ~name:(show var) (typ var) in - ValueHT.add var_to_sym var sym; - Hashtbl.add sym_to_var sym var; - sym + module V = struct + module I = struct + type t = value [@@deriving ord] + let pp formatter = function + | VVal v -> Var.pp formatter v + | VWidth v -> Format.fprintf formatter "%a@@width" Var.pp v + | VPos v -> Format.fprintf formatter "%a@@pos" Var.pp v + let show = SrkUtil.mk_show pp + let equal x y = compare x y = 0 + let hash = function + | VVal v -> Hashtbl.hash (Var.hash v, 0) + | VPos v -> Hashtbl.hash (Var.hash v, 1) + | VWidth v -> Hashtbl.hash (Var.hash v, 2) end - - let of_symbol sym = - if Hashtbl.mem sym_to_var sym then - Some (Hashtbl.find sym_to_var sym) - else - None - - let is_global = Var.is_global % var_of_value -end + include I + + + + let sym_to_var = Hashtbl.create 991 + let var_to_sym = ValueHT.create 991 + let prophecy_vars = ValueHT.create 991 (* var -> var mapping *) + let var_of_prophecy_vars = ValueHT.create 991 (* reverse mapping of prophecy_vars *) + + let typ v = tr_typ (Var.get_type (var_of_value v)) + + let symbol_of var = + if ValueHT.mem var_to_sym var then + ValueHT.find var_to_sym var + else begin + let sym = Ctx.mk_symbol ~name:(show var) (typ var) in + ValueHT.add var_to_sym var sym; + Hashtbl.add sym_to_var sym var; + sym + end + + let of_symbol sym = + if Hashtbl.mem sym_to_var sym then + Some (Hashtbl.find sym_to_var sym) + else + None + + let is_global = Var.is_global % var_of_value + + let make_var sym is_global = + let v = + begin match is_global with + | true -> + Varinfo.mk_global (Syntax.show_symbol srk sym) (Concrete (Int 8)) + | false -> + Varinfo.mk_local (Syntax.show_symbol srk sym) (Concrete (Int 8)) + end |> Var.mk + in + Hashtbl.add sym_to_var sym (VVal v); + ValueHT.add var_to_sym (VVal v) sym; + VVal v + + let prophesize var = + let sym = symbol_of var in + let sym_name = (Syntax.show_symbol srk sym) ^ "_prophecy" in + let sym' = Syntax.mk_symbol srk ~name:sym_name (Syntax.typ_symbol srk sym) in + let var' = make_var sym' false in + ValueHT.add prophecy_vars var var'; + ValueHT.add var_of_prophecy_vars var' var; + var' + + let var_of_prophecy_var var' = ValueHT.find_opt var_of_prophecy_vars var' + let prophecy_var_of_var var = ValueHT.find_opt prophecy_vars var + let is_prophecy_var v = + match var_of_prophecy_var v with + | Some _ -> true + | None -> false + end + module K = struct module Tr = Transition.Make(Ctx)(V) @@ -212,6 +246,8 @@ module K = struct Log.time "cra:star" star x let project = exists V.is_global + + let project_custom v = exists v end type ptr_term = @@ -751,21 +787,114 @@ let decorate_transition_system predicates ts entry = let invariant = abstract_domain.formula_of (abstract_domain.exists (member live) (inv v)) in + logf "loop header location: %d" v; logf "Found invariant at %d:@;%a" v (Syntax.Formula.pp srk) invariant; + logf "New ID: %d" fresh_id; WG.split_vertex ts v (Weight (K.assume invariant)) fresh_id) ts -let make_transition_system rg = +module VSet = BatSet.Make(V) +module ISet = BatSet.Make(Int) + +let create_gas_variable () = + let mk_int k = Ctx.mk_real (QQ.of_int k) in + let gas_var = Var.mk (Varinfo.mk_global "__duet_gas" (Concrete (Int 8))) in + let gas_var_sym = Syntax.mk_symbol srk ~name:"__duet_gas" `TyInt in + let gas_var_term = Syntax.mk_const srk gas_var_sym in + Hashtbl.add V.sym_to_var gas_var_sym (VVal gas_var); + ValueHT.add V.var_to_sym (VVal gas_var) gas_var_sym; + let gasexpr = (Syntax.mk_lt srk (mk_int 0) gas_var_term) in + let gasweight = + let assume_positive = K.assume gasexpr in + let decr_by_one = Syntax.mk_sub srk gas_var_term (mk_int 1) |> K.assign (VVal gas_var) in + K.mul assume_positive decr_by_one in + let initial_gas = K.havoc [ VVal gas_var ] in + (gasweight, gasexpr, initial_gas) + +let new_vtx () = (Def.mk (Assume Bexpr.ktrue)).did + +let instrument_with_gas (ts: TSG.t) gasexpr : TSG.t = + let modify_pre ts u = + Printf.printf " --- %d is call edge\n" u; + let g = ref ts in + (* step 1: add new in-edge to (u, v) *) + let x = new_vtx () in + g := WG.add_vertex !g x; + (* step 2: add weighted edge x-(gasexpr)->u *) + g := WG.add_edge !g x (Weight gasexpr) u; + (* step 3: redirect every p->u to be y->x->u *) + WG.iter_pred_e (fun (p, weight, _) -> + Printf.printf "changing %d->%d to %d->%d->%d\n" p u p x u; + g := WG.add_edge !g p weight x; + g := WG.remove_edge !g p u + ) ts u; + !g in + let modify_post ts u = + Printf.printf " --- %d is loop header\n" u; + let g = ref ts in + let x = new_vtx () in + (* step 1: add new out-edge from u -> x *) + g := WG.add_vertex !g x; + g := WG.add_edge !g u (Weight gasexpr) x; + (* step 2: for each u -> v, make it u -> x -> v *) + WG.iter_succ_e (fun (_, weight, v) -> + Printf.printf "changing %d->%d to %d->%d->%d\n" u v u x v; + g := WG.add_edge !g x weight v; + g := WG.remove_edge !g u v + ) ts u; + !g in + (* for each call-edge, u->v, add new predecessor edge x->u->v where x->u is an instrumented edge. *) + let loop_headers = + let module L = Loop.Make(TSG) in + (List.map (fun loop -> L.header loop) @@ L.all_loops (L.loop_nest ts)) + |> List.map (fun x -> (x, true)) in + let call_edge_headers, _ = + WG.fold_edges (fun (u, w, _) (headers, callees) -> + match w with + | Call (s, _) -> ISet.add u headers, ISet.add s callees + | Weight _ -> (headers, callees)) ts (ISet.empty, ISet.empty) in + + List.fold_left (fun ts (header, is_call_edge) -> + if is_call_edge then + modify_post ts header + else + modify_pre ts header) ts + (loop_headers + @ (List.map (fun x -> (x, false)) @@ ISet.to_list call_edge_headers)) + +let instrument_main tg entry init_gas_expr = + let post_entry = new_vtx () in + (* step 1: add a vertex called post_entry *) + let tg = WG.add_vertex tg post_entry in + (* step 2: remove each edge (entry->v) and make it (post_entry->v) *) + let gg = ref tg in + WG.iter_succ_e (fun (u, w, v) -> + assert (u = entry); + gg := WG.remove_edge !gg entry v; + gg := WG.add_edge !gg post_entry w v + ) tg entry; + (* step 3: add edge from entry->post_entry labeled by init_gas_expr *) + WG.add_edge !gg entry (Weight init_gas_expr) post_entry + +let make_transition_system ?(simplify=true) ?(instr_gas=false) (main_entry: int) rg = + let gasweight, gasexpr, init_gas_weight = create_gas_variable () in let call_edge block = Call ((RG.block_entry rg block).did, (RG.block_exit rg block).did) in let assertions = ref SrkUtil.Int.Map.empty in - let add_assert v e = - assertions := SrkUtil.Int.Map.add v e (!assertions) + let assert_vars = ref VSet.empty in + let add_assert v (cond, loc, msg) = + assertions := SrkUtil.Int.Map.add v (cond, loc, msg) (!assertions); + let open Syntax in + Symbol.Set.iter (fun (s : Syntax.symbol) -> + match V.of_symbol s with + | Some v -> assert_vars := VSet.add v (!assert_vars) + | None -> ()) + (Syntax.symbols cond) in let ts = - BatEnum.fold (fun ts (block, graph) -> - let tg = + BatEnum.fold (fun ts (block, graph) -> (* CFG of current function *) + let tg = (* TS of current CFG *) RG.G.fold_vertex (fun def tg -> let tg = WG.add_vertex tg def.did in let label = @@ -820,8 +949,14 @@ let make_transition_system rg = let point_of_interest v = v = entry || v = exit || SrkUtil.Int.Map.mem v (!assertions) in - let tg = TS.simplify point_of_interest tg in - let tg = TS.remove_temporaries tg in + let elim_var v = + V.is_global v || VSet.mem v (!assert_vars) + in + let tg = if (instr_gas && entry = main_entry) then instrument_main tg entry init_gas_weight else tg in + let tg = if instr_gas then instrument_with_gas tg gasweight else tg in + let predicates = if instr_gas then gasexpr :: predicates else predicates in + let tg = if simplify then TS.simplify point_of_interest tg else tg in + let tg = TS.remove_temporaries elim_var tg in let tg = if !forward_inv_gen then Log.phase "Forward invariant generation" @@ -841,7 +976,12 @@ let make_transition_system rg = TS.empty (RG.bodies rg) in - (ts, !assertions) + (* perform some inlining *) + Printf.printf "calling inliner...\n"; + let inlined_ts, new_assertions = + TS.inline ts main_entry (fun _ -> ()) (!assertions) in + Printf.printf "----------inlining done-----\n"; + (inlined_ts, new_assertions) let mk_query ts entry = TS.mk_query ts entry @@ -856,7 +996,7 @@ let analyze file = | [main] -> begin let rg = Interproc.make_recgraph file in let entry = (RG.block_entry rg main).did in - let (ts, assertions) = make_transition_system rg in + let (ts, assertions) = make_transition_system entry rg in (*TSDisplay.display ts;*) let query = mk_query ts entry in assertions |> SrkUtil.Int.Map.iter (fun v (phi, loc, msg) -> @@ -1093,7 +1233,7 @@ let prove_termination_main file = | [main] -> begin let rg = Interproc.make_recgraph file in let entry = (RG.block_entry rg main).did in - let (ts, _) = make_transition_system rg in + let (ts, _) = make_transition_system entry rg in if !CmdLine.display_graphs then TSDisplay.display ts; let query = mk_query ts entry in @@ -1152,7 +1292,8 @@ let resource_bound_analysis file = match file.entry_points with | [main] -> begin let rg = Interproc.make_recgraph file in - let (ts, _) = make_transition_system rg in + let entry = (RG.block_entry rg main).did in + let (ts, _) = make_transition_system entry rg in let entry = (RG.block_entry rg main).did in let query = mk_query ts entry in let cost = diff --git a/duet/duet.ml b/duet/duet.ml index 02971557..29bf90b8 100644 --- a/duet/duet.ml +++ b/duet/duet.ml @@ -11,6 +11,7 @@ open! Cra open! Proofspace open! Dependence open! Categorize +open! Gps let usage_msg = "Duet program analyzer\nUsage: duet [OPTIONS] file.[c|bp]" @@ -18,6 +19,12 @@ let anon_fun s = ignore (CmdLine.parse s) let _ = Sys.set_signal Sys.sigtstp (Sys.Signal_handle (fun _ -> Log.print_stats ())); + Printexc.record_backtrace true;; + Sys.set_signal Sys.sigint (Sys.Signal_handle (fun _ -> + Printf.eprintf "SIGINT received. Backtrace:\n%!"; + Printexc.print_backtrace stderr; + exit 1 + ));; let spec_list = CmdLine.spec_list () in Arg.parse (Arg.align spec_list) anon_fun usage_msg; match !CfgIr.gfile with diff --git a/duet/gps.ml b/duet/gps.ml new file mode 100644 index 00000000..b09438b2 --- /dev/null +++ b/duet/gps.ml @@ -0,0 +1,747 @@ +open Core +open Srk +open CfgIr +open BatPervasives +open Cra + +module TS = TransitionSystem.Make(Ctx)(V)(K) + +include Log.Make(struct let name = "gps" end) + +module ProcName = struct + type t = int * int + + let make ((u, v) : TS.vertex * TS.vertex) : t = (u, v) + + let string_of (p: t) = + let u, v = p in Printf.sprintf "%d:%d" u v + + let of_string (s: string) = + match String.split_on_char ':' s with + | [ us ; vs ] -> (make ((int_of_string us), (int_of_string vs))) + | _ -> failwith @@ Printf.sprintf "illegal procedure identifier %s" s + + (* lexicographic comparison using Stdlib.compare *) + let compare (p1: t) (p2: t) = Stdlib.compare p1 p2 + let hash = Hashtbl.hash + let equal = (=) +end + +module ProcHT = BatHashtbl.Make(ProcName) +module ProcMap = BatMap.Make(ProcName) +module IntMap = BatMap.Make(Int) +module StringMap = BatMap.Make(String) +module DQ = BatDeque +module ARR = Batteries.DynArray +type cfg_t = TSG.t +type idq_t = int BatDeque.t +type state_formula = Ctx.t Syntax.formula +exception Mexception of string +let mk_true () = Syntax.mk_true Ctx.context +let mk_false () = Syntax.mk_false Ctx.context +let mk_query ts entry = TS.mk_query ts entry (if !monotone then (module MonotoneDom) else (module TransitionDom)) + +let log_formulas prefix formulas = + List.iteri (fun i f -> logf "[formula] %s(%i): %a\n" prefix i (Syntax.pp_expr srk) f) formulas + +let log_weights prefix weights = + List.iteri (fun i f -> logf "[weight] %s(%i): %a\n" prefix i K.pp f) weights + + +let log_model prefix model = + logf "[model] %s: %a\n" prefix Interpretation.pp model + +(* +let assert_i = ref 0 +let new_assert_var cond = + let i = !assert_i in + let name = "__assert" ^ (string_of_int i) in + let v = Varinfo.mk_global name (Concrete (Int 8)) |> Var.mk in + let assert_var = Syntax.mk_symbol srk ~name:name `TyInt in + let assert_term = Syntax.mk_const srk assert_var in + assert_i := !assert_i + 1; + K.assign v cond + +let process_interproc_assertion (ts: cfg_t) (phi: Ctx.formula) v = + let a_var, a_term = new_assert_var @@ Ctx.mk_not phi in + +*) + +(* Convert assertion checking problem to vertex reachability problem. *) +let safety_to_reachability (ts : cfg_t) assertions = + let err_loc = 1 + (WG.fold_vertex (fun v max -> if v > max then v else max) ts 0) in + let ts = WG.add_vertex ts err_loc in + let ts = + SrkUtil.Int.Map.fold (fun v (phi, _, _) ts -> + let s = Printf.sprintf " Adding assertion node %d -> %d for label " v err_loc in + log_formulas s [ Ctx.mk_not phi ] ; + WG.add_edge ts v (Weight (K.assume (Ctx.mk_not phi))) err_loc) + assertions + ts + in + (ts, err_loc) + +module Summarizer = + struct + module SMap = BatMap.Make(ProcName) + type t = { + query: TS.query; + rev_query: TS.reverse_query; + mutable underapprox: K.t SMap.t; + mutable overapprox: K.t SMap.t; (* Caution: used only for silent mode where no CRA-generated summaries are used. *) + silent: bool; + } + + let init (graph: cfg_t) (src: int) (tgt: int) (enable_summary: bool) : t = + let q = mk_query graph src in + let rq = TS.mk_reverse_query q tgt in + { query = q + ; rev_query = rq + ; underapprox = SMap.empty + ; overapprox = SMap.empty + ; silent = not enable_summary } + + + let filt_over (ctx: t) x = + if ctx.silent then begin + (*logf "filt_over: context is silent! \n";*) + K.assume @@ mk_true () + end + else begin + (*logf "filt_over: context isn't silent!\n";*) + x end + + let filt_under (ctx: t) x = + if ctx.silent then K.assume @@ mk_false () + else x + + (** retrieve over-approximate procedure summary *) + let over_proc_summary (ctx: t) ((u, v) : ProcName.t) = + if ctx.silent then begin + match SMap.find_opt (u, v) ctx.overapprox with + | Some s -> s + | None -> + let init = K.assume @@ mk_true () in + ctx.overapprox <- SMap.add (u, v) init ctx.overapprox; init + end else + TS.get_summary ctx.query (u, v) + |> K.exists (V.is_global) + + (** set over-approximate procedure summary *) + let set_over_proc_summary (ctx: t) ((u, v): ProcName.t) (w: K.t) = + if ctx.silent then begin + match SMap.find_opt (u, v) ctx.overapprox with + | Some s -> + ctx.overapprox <- SMap.add (u, v) (K.conjunct s w) ctx.overapprox + | None -> + ctx.overapprox <- SMap.add (u, v) w ctx.overapprox; + end else + TS.set_summary ctx.query (u, v) w + + (** retrieve under-approximate procedure summary *) + let under_proc_summary (ctx: t) ((u, v): ProcName.t) : K.t = + match SMap.find_default K.zero (u, v) ctx.underapprox + |> K.project_mbp (V.is_global) + with + | `Sat tr -> tr + | _ -> + log_weights "under_proc_summary: this weight is unsat: " [SMap.find_default K.zero (u, v) ctx.underapprox]; + K.zero + (*failwith "under_proc_summary: cannot model-based project"*) + + (** set under-approximate procedure summary *) + let set_under_proc_summary (ctx: t) ((u, v): ProcName.t) (w: K.t) : unit = + ctx.underapprox <- SMap.add (u, v) w ctx.underapprox + + (** refinement of procedure summaries using a two-voc transition formula *) + let refine_over_summary (ctx: t) ((u, v): ProcName.t) (rfn: K.t) = + if ctx.silent then begin + match SMap.find_opt (u, v) ctx.overapprox with + | Some s -> + ctx.overapprox <- SMap.add (u, v) (K.conjunct s rfn) ctx.overapprox + | None -> + ctx.overapprox <- SMap.add (u, v) rfn ctx.overapprox + end else + over_proc_summary ctx (u, v) + |> K.conjunct rfn + |> set_over_proc_summary ctx (u, v) + + let refine_under_summary (ctx: t) ((u, v): ProcName.t) (w:K.t) : unit = + let summary = under_proc_summary ctx (u, v) in + let summary' = K.add summary w in + log_weights "under-approx summary refined to " [summary']; + set_under_proc_summary ctx (u, v) summary' + + let path_weight_intra (ctx: t) (src: int) (dst: int) = + TS.exit_summary ctx.rev_query src dst + |> filt_over ctx + + let path_weight_inter (ctx: t) (src: int) = + TS.target_summary ctx.rev_query src + |> filt_over ctx + + end + +type path_type = + | OverApprox + | UnderApprox + +let srk = Ctx.context + +module GPS = struct + module Graph = struct + type t = + { graph : cfg_t + ; call_summary : ProcName.t -> K.t + ; target_summary : int -> K.t } + + type vertex = TS.vertex + + type weight = K.t + + let edge_label g u v = WG.edge_weight g.graph u v + + let weight g u v = + match WG.edge_weight g.graph u v with + | Call (src, dst) -> + g.call_summary (src, dst) + | Weight w -> w + + let fold_succ f g u acc = + WG.U.fold_succ f (WG.forget_weights g.graph) u acc + + let summary g src = g.target_summary src + + let compare_vertex = Stdlib.compare + let pp_vertex = Format.pp_print_int + end + + module Label = struct + type t = Ctx.t Syntax.formula + let top = Ctx.mk_true + let bottom = Ctx.mk_false + let meet f g = Ctx.mk_and [f; g] + let leq f g = + match Smt.entails Ctx.context f g with + | `Yes -> true + | _ -> false + let negate f = Ctx.mk_not f + let pp = Syntax.Formula.pp srk + end + module Transition = struct + type t = K.t + type label = Ctx.t Syntax.formula + type state = Ctx.t Interpretation.interpretation + let check pre trs post = + K.interpolate_or_concrete_model ((K.assume pre)::trs) post + + let is_deterministic = + let is_det tr = + not (K.contains_havoc tr) || K.is_deterministic tr + in + Memo.memo is_det + + let post_model = K.get_post_model + let pp = K.pp + let mul = K.mul + let assume = K.assume + let guard = K.guard + let pp_state = Interpretation.pp + end + + (* ART module *) + (* module ReachTree = ReachTree.ART(Ctx)(K)(TS')(ProcName)(VN)(Summarizer)*) + module ReachTree = ReachTree.ART(Graph)(Label)(Transition) + + let generate_test_sgt art node = + logf "Generating test @ %a\n" ReachTree.pp_node node; + let post = Ctx.mk_not (K.guard (ReachTree.path_to_error art node)) in + let rec path_weight v = + match ReachTree.parent_weight art v with + | Some (parent, w) -> K.mul (path_weight parent) w + | None -> K.one + in + match K.interpolate_or_concrete_model [path_weight node] post with + | `Invalid v_model -> `Test v_model + | `Unknown -> failwith "generate_test_sgt: got UNKNOWN as a result for interpolate_or_get_model" + | `Valid _ -> `Pruned + + let sgt graph src dst = + let art = ReachTree.make graph Ctx.mk_true ~src ~dst in + let rec loop () = + match ReachTree.deque_frontier art with + | None -> `Safe + | Some node -> + match generate_test_sgt art node with + | `Pruned -> loop () + | `Test state -> + match ReachTree.execute art node state with + | `Safe -> loop () + | `Unsafe _ -> `Unsafe + in + loop () + + + (* to print the reachability tree (+ worklist), or not *) + (* RF 3/2/25: If you enable this flag, and even if *) + (* the logf output stream is suppressed, it incurs a _huge_ *) + (* performance penalty. *) + let print_tree = false + + type global_context = + { g_graph : cfg_t + ; g_summarizer : Summarizer.t + ; g_errloc : int } + + and mc_result = + | Safe of K.t + | Unsafe of K.t + + + (* contextual information maintained by GPS algorithm. *) + (* intraprocedural context *) + type intra_context = { + id : ProcName.t; + cfg : Graph.t; + mutable art : ReachTree.t; + global_ctx : global_context; + } + (* global context *) + (** some helper functions that operate on the context *) + let get_summarizer ctx = ctx.global_ctx.g_summarizer + + let log_labelled_weights ctx uu prefix weights = + List.iteri + (fun i f -> + match f with + | Call (u, v) -> + let p = + begin match uu with + | OverApprox -> Summarizer.over_proc_summary ctx.g_summarizer (ProcName.make (u, v)) + | UnderApprox -> Summarizer.under_proc_summary ctx.g_summarizer (ProcName.make (u, v)) + end in + logf "[labelled weight] %s(%i, call(%d,%d)): %a\n" prefix i u v K.pp p + | Weight w -> + logf "[labelled weight] %s(%i): %a\n" prefix i K.pp w) weights + + + (* Express a relational query as a precondition/postcondition pair over + prophecy variables *) + let demote_precondition (query : K.t) = + let preconditions, postconditions = + BatEnum.fold (fun (preconditions, postconditions) (var, asgn) -> + let prophecy_var = V.prophesize var in + let prophecy_sym = V.symbol_of prophecy_var in + let prophecy_term = Syntax.mk_const srk prophecy_sym in + let var_term = Syntax.mk_const srk (V.symbol_of var) in + (Syntax.mk_eq srk prophecy_term asgn::preconditions, + Syntax.mk_eq srk prophecy_term var_term::postconditions)) + ([K.guard query], []) + (K.transform query) + in + (Syntax.mk_and srk preconditions, Syntax.mk_and srk postconditions) + + + (* promote an arbitrary state formula (not necessarily the pre-state) to a transition formula. *) + (* To do so, we substitute in fresh skolem symbols for all prophecy variables inside [f], and *) + (* create a transform map, treating the substituted formula as guard. *) + let promote (f : Ctx.t Syntax.formula) = + let sym_map = ValueHT.create 991 in + let substitute = Memo.memo (fun sym -> + match V.of_symbol sym with + | Some v -> + begin match V.var_of_prophecy_var v with + | Some original_var -> + let fresh_skolem = Syntax.mk_symbol srk (Syntax.typ_symbol srk sym) in + let term = Syntax.mk_const srk fresh_skolem in + ValueHT.add sym_map original_var term; + term + | None -> Syntax.mk_const srk sym + end + | None -> Syntax.mk_const srk sym) in + K.construct (Syntax.substitute_const srk substitute (Syntax.mk_not srk f)) (ValueHT.to_seq sym_map |> List.of_seq) + + + let mk_intra_context (gctx: global_context) ((src,tgt): ProcName.t) (query: K.t) = + let pre_state, equalities = demote_precondition query in + let target_summary v = + K.mul + (Summarizer.path_weight_intra gctx.g_summarizer v tgt) + (K.assume equalities) + in + let dst = gctx.g_errloc in + let graph = + Graph.{ graph = WG.add_edge (gctx.g_graph) tgt (Weight (K.assume equalities)) dst + ; call_summary = Summarizer.over_proc_summary gctx.g_summarizer + ; target_summary = target_summary } + in + { + id = (src,dst); + cfg = graph; + art = ReachTree.make graph pre_state ~src ~dst; + global_ctx = gctx; + } + + let rec art_cfg_path_pair (ctx: intra_context) (p: ReachTree.node list) = + match p with + | u :: v :: t -> + let u_vtx = ReachTree.maps_to ctx.art u in + let v_vtx = ReachTree.maps_to ctx.art v in + (u, (u_vtx, v_vtx), v) :: (art_cfg_path_pair ctx (v :: t)) + | _ -> [] + + + let print_vocabulary tr = + let g_vocab, l_vocab = K.vocabulary tr in + let vname x = + match V.of_symbol x with + | Some var -> V.show var + | None -> " [havoc] " + in + log_weights " [vocabulary of transition] " [tr]; + logf " ------ globals: ---- {\n"; + List.iter (fun x -> logf " %s %s\n" (Syntax.show_symbol srk x) (vname x)) g_vocab; + logf "}\n ------ locals: ---- {\n"; + List.iter (fun x -> logf " %s %s\n" (Syntax.show_symbol srk x) (vname x)) l_vocab + + (* CFG path condition from art.src -> art.v *) + let path_condition (ctx: intra_context) condition_type (v: ReachTree.node) = + let art = ctx.art in + let art_nodes = ReachTree.tree_path art v in + let ts = ctx.cfg.Graph.graph in + let cfg_nodes = List.map (fun x -> ReachTree.maps_to art x) art_nodes in + let rec to_weights l : K.t label list = + match l with + | a :: b :: t -> + WG.edge_weight ts a b :: (to_weights (b :: t)) + | _ -> [] + in + let summ = get_summarizer ctx in + let pathcond = List.map (fun (weight: K.t label) -> + match weight with + | Call (src, dst) -> + begin match condition_type with + | OverApprox -> Summarizer.over_proc_summary summ (ProcName.make (src, dst)) + | UnderApprox -> + let under = Summarizer.under_proc_summary summ (ProcName.make (src, dst)) in + log_weights "underapproximate summary" [under]; + print_vocabulary under; + under + end + | Weight w -> w) (to_weights cfg_nodes) in + logf " ---- path_condition: path length: %d, before add1: %d\n" ((List.length pathcond)+1) (List.length pathcond); + let l = (K.assume (ReachTree.get_precondition ctx.art)) :: pathcond in + log_weights "path conditions " l; l + + let get_global_ctx (ctx: intra_context) = ctx.global_ctx + + let extract_refinement (ctx: intra_context) = + let art = ctx.art in + let rfn = ReachTree.label art ReachTree.root |> promote in + log_weights "refinement: " [rfn]; + K.exists (fun v -> V.is_global v) (rfn) + + let seq = List.fold_left K.mul K.one (* sequentially multiply, left-right *) + + + let rec handle_path_to_error ctx left curr right dir err_leaf : [`Unsafe of K.t | `Safe] = + let handle_right_case caller_id = + let f = List.map (fun (_, w, _) -> w) in + let left = f left in + let right = f right in + match K.project_mbp (V.is_global) (path_condition ctx UnderApprox err_leaf |> seq) with + | `Sat t -> `Unsafe t + | _ -> + logf " ------------------------ handle_path_to_error debug info: called by case %s ------------------\n" caller_id; + log_weights "faulty weight: " (path_condition ctx UnderApprox err_leaf); + logf "\nlength of left path: %d" (List.length left); + logf "\nlength of right path: %d" (List.length right); + logf "\nPrinting left path... \n"; + + log_labelled_weights ctx.global_ctx UnderApprox "left path - " left; + logf "error: handle_path_to_error: cannot project path condition" ; + `Safe in + let handle_left_case caller_id = + logf "handle_path_to_error: %s\n" caller_id; + `Safe in + match curr with + | (_, Weight _, _) -> + begin match left, dir, right with + | [], `Left, _ -> + handle_left_case "reached leftmost item, `curr` variable is NOT a call-edge" + | _, `Right, [] -> + handle_right_case "reached rightmost item, `curr` variable is NOT a call-edge" + | a :: left', `Left, _ -> handle_path_to_error ctx left' a (curr :: right) dir err_leaf + | _, `Right, a :: right' -> handle_path_to_error ctx (curr :: left) a right' dir err_leaf + end + | (u, (Call (src, dst)), _) -> + let prefix = path_condition ctx UnderApprox u |> seq in + let summ = get_summarizer ctx in + let suffix = + List.map (fun (_, ew, _) -> + match ew with + | Weight w -> w + | Call (s, t) -> Summarizer.over_proc_summary summ (ProcName.make (s, t))) + right + |> seq in + let summary = Summarizer.over_proc_summary summ (ProcName.make (src, dst)) in + begin match K.contextualize prefix summary suffix with + | `Sat query -> + let answer = + mk_intra_context (ctx.global_ctx) (ProcName.make (src, dst)) query + |> intraproc_check + in begin match answer with + | Safe r -> + Summarizer.refine_over_summary summ (ProcName.make (src, dst)) r; + handle_path_to_error ctx left curr right dir err_leaf + | Unsafe trs -> + begin match trs |> K.project_mbp (V.is_global) with + | `Sat tr -> + Summarizer.refine_under_summary summ (ProcName.make (src, dst)) tr; + begin match right with + | a :: right' -> + handle_path_to_error ctx (curr::left) a right' `Right err_leaf + | [] -> (* we're done *) + handle_right_case "rightmost edge is call-edge, underapproximation successful" + end + | _ -> failwith "error: cannot do mbp on returned error trace in handle_path_to_error" + end + end + | `Unsat -> (* procedure summary at `curr` is UNSAT, so backtrack *) + begin match left with + | a :: left' -> + handle_path_to_error ctx left' a (curr :: right) `Left err_leaf + | [] -> (* at the very left. we're done *) + handle_left_case "at the leftmost edge, is a call-edge, done" + end + end + + + and intraproc_check (ctx: intra_context) : mc_result = + match ReachTree.gps ctx.art with + | `Safe -> Safe (extract_refinement ctx) + | `Unsafe w -> + logf "--- GPS: found path-to-error at tree node %d (cfg vertex %d) \n" (ReachTree.of_node w) (ReachTree.maps_to ctx.art w); + logf " --- forming path to error... \n"; + let has_calls, path_to_w = + ReachTree.tree_path ctx.art w + |> art_cfg_path_pair ctx + |> List.map (fun (u, (u_vtx, v_vtx), v) -> (u, WG.edge_weight ctx.cfg.Graph.graph u_vtx v_vtx, v)) + |> List.fold_left (fun (has_call, l) (u, w, v) -> + match w with + | Call _ -> (true, (u, w, v) :: l) + | _ -> (has_call, (u, w, v) :: l) + ) (false, []) + in + logf " --- finished forming path to error, calling handle_path_to_error ... \n"; + begin match has_calls, path_to_w with + | true, curr :: right -> + begin match handle_path_to_error ctx [] curr right `Right w with + | `Safe -> (* path-to-error concretization failed. frontier_node is the src node of a call-edge. *) + (* we can mark `w` as a frontier node to be refined, and continue. *) + ReachTree.add_frontier ctx.art w; + intraproc_check ctx + | `Unsafe pathcond -> + logf "--- GPS: managed to concretize an intraprocedural path-to-error. returning... "; + Unsafe pathcond end + | false, _::_ -> + (* TODO! *) +(* Unsafe (seq (List.map (fun (_, w, _) -> + match w with + | Weight w -> w + | _ -> assert false) + path_to_w)) + *) + + Unsafe K.one + | _, [] -> + (* corner case: either no calls along the path, or if the path to error is of length 0. *) + Unsafe K.one + end + + + let execute (ts : cfg_t) (entry : int) (err_loc : int) (enable_summary:bool) : mc_result = + let gctx = + { g_graph = ts + ; g_summarizer = Summarizer.init ts entry err_loc enable_summary + ; g_errloc = err_loc } + in + (* interproc_graph represents the language of interprocedural paths from + entry to err_loc (including interprocedural paths that make calls that + never return---i.e., the ``unbalanced left'' language of + interprocedurally-valid paths) *) + let interproc_graph = + WG.fold_edges (fun (u, w, _) interproc_graph -> + match w with + | Call (en, _) -> + WG.add_edge interproc_graph u (Weight K.one) en + | Weight _ -> interproc_graph) + ts + ts + in + let graph = + Graph.{ graph = interproc_graph + ; call_summary = Summarizer.over_proc_summary gctx.g_summarizer + ; target_summary = Summarizer.path_weight_inter gctx.g_summarizer } + in + let main_context = + { + id = (entry,err_loc); + cfg = graph; + art = ReachTree.make graph Ctx.mk_true ~src:entry ~dst:err_loc; + global_ctx = gctx; + } + in + logf "executing GPS: start\n"; + intraproc_check main_context +end + + +module BM = BatMap.Make(Int) + + +let analyze_mc enable_gas enable_summary file = + let open Srk.Iteration in + populate_offset_table file; + K.domain := split (product [ PolyhedronGuard.exp + ; LossyTranslation.exp ]); + match file.entry_points with + | [main] -> begin + let rg = Interproc.make_recgraph file in + let entry = (RG.block_entry rg main).did in + let (ts, assertions) = make_transition_system ~simplify:true ~instr_gas:enable_gas entry rg in + let ts, err_loc = safety_to_reachability ts assertions in + if !CmdLine.display_graphs then TSDisplay.display ts; + logf "\nentry: %d\n" entry; + Printf.printf "testing reachability of location %d\n" err_loc ; + Printf.printf "------------------------------\n"; + begin match GPS.execute ts entry err_loc enable_summary with + | Safe _ -> Printf.printf " proven safe\n"; + | Unsafe _ -> Printf.printf " proven unsafe\n" + end; + Printf.printf "------------------------------\n" + end + | _ -> assert false + + +let analyze_sgt enable_gas enable_summary file = + let open Srk.Iteration in + populate_offset_table file; + K.domain := split (product [ PolyhedronGuard.exp + ; LossyTranslation.exp ]); + match file.entry_points with + | [main] -> begin + let rg = Interproc.make_recgraph file in + let entry = (RG.block_entry rg main).did in + let (ts, assertions) = make_transition_system ~simplify:true ~instr_gas:enable_gas entry rg in + let ts, err_loc = safety_to_reachability ts assertions in + if !CmdLine.display_graphs then TSDisplay.display ts; + logf "\nentry: %d\n" entry; + Printf.printf "testing reachability of location %d\n" err_loc ; + Printf.printf "------------------------------\n"; + let summ = Summarizer.init ts entry err_loc enable_summary in + let graph = + GPS.Graph.{ graph = ts + ; call_summary = (fun _ -> failwith "SGT: procedure call") + ; target_summary = Summarizer.path_weight_inter summ } + in + begin match GPS.sgt graph entry err_loc with + | `Safe -> Printf.printf " proven safe\n"; + | `Unsafe -> Printf.printf " proven unsafe\n" + | `Error s -> Printf.printf "ERR: %s\n" s + end; + Printf.printf "------------------------------\n" + end + | _ -> assert false + +let analyze_impact file = + let open Srk.Iteration in + populate_offset_table file; + K.domain := split (product [ PolyhedronGuard.exp + ; LossyTranslation.exp ]); + match file.entry_points with + | [main] -> begin + let rg = Interproc.make_recgraph file in + let entry = (RG.block_entry rg main).did in + let (ts, assertions) = make_transition_system ~simplify:true entry rg in + let ts, err_loc = safety_to_reachability ts assertions in + if !CmdLine.display_graphs then TSDisplay.display ts; + logf "\nentry: %d\n" entry; + Printf.printf "testing reachability of location %d\n" err_loc ; + Printf.printf "------------------------------\n"; + let graph = + GPS.Graph.{ graph = ts + ; call_summary = (fun _ -> failwith "IMPACT: procedure call") + ; target_summary = (fun _ -> K.one) } + in + let module ART = GPS.ReachTree in + let art = ART.make graph Ctx.mk_true ~src:entry ~dst:err_loc in + let rec loop () = + match ART.deque_frontier art with + | None -> `Safe + | Some u -> + (* Fetched tree node u from work list. First attempt to close it. *) + if ART.is_covered art u then loop () + else if ART.lclose art u then loop () + else if ART.maps_to art u == err_loc then + match ART.generate_test art u with + | `Pruned -> + List.iter (fun v -> ignore (ART.lclose art v)) (ART.tree_path art u); + loop () + | `Test _ -> `Unsafe + else (ART.expand art u; loop ()) + in + begin match loop () with + | `Safe -> Printf.printf " proven safe\n"; + | `Unsafe -> Printf.printf " proven unsafe\n" + | `Error s -> Printf.printf "ERR: %s\n" s + end; + Printf.printf "------------------------------\n" + end + | _ -> assert false + + +(** dump simplified CFG before doing model checking / CRA / concolic execution *) +let dump_cfg simplify instrument file = + populate_offset_table file; + match file.entry_points with + | [main] -> + begin + let rg = Interproc.make_recgraph file in + let entry = (RG.block_entry rg main).did in + let (ts, assertions) = make_transition_system ~simplify:simplify ~instr_gas:instrument entry rg in + let ts, _ = safety_to_reachability ts assertions in + TSDisplay.display ts + end + | _ -> assert false + +let _ = + CmdLine.register_pass + ("-gps", analyze_mc false true, " GPS model checking algorithm, without gas-instrumentation"); + CmdLine.register_pass + ("-gps-gas", analyze_mc true true, " GPS model checking algorithm, with gas-instrumentation (i.e., refutation-complete)"); + CmdLine.register_pass + ("-gps-nosum", analyze_mc false false, "GPS with neither gas nor CRA-generated summary"); + CmdLine.register_pass + ("-gps-nosum-nogas", analyze_mc true false, "GPS with gas but without CRA-generated summary (i.e., refutation-complete)"); + + CmdLine.register_pass + ("-sgt", analyze_sgt false true, "Summary-guided testing, without gas-instrumentation"); + CmdLine.register_pass + ("-sgt-gas", analyze_sgt true true, "Summary-guided testing, with gas"); + CmdLine.register_pass + ("-sgt-nosum", analyze_sgt false false, "Summary-guided testing without CRA-generated summary"); + CmdLine.register_pass + ("-sgt-nosum-nogas", analyze_sgt true false, "Summary-guided testing with gas but without CRA-generated summary"); + + CmdLine.register_pass + ("-impact", analyze_impact, "Lazy abstraction with interpolants"); + + CmdLine.register_pass + ("-dump-unsimplified-cfg", dump_cfg false false, "dump unsimplified CFG"); + CmdLine.register_pass + ("-dump-simplified-cfg", dump_cfg true false, "dump simplified CFG"); + CmdLine.register_pass + ("-dump-instrumented-unsimplified-cfg", dump_cfg false true, "dump unsimplified CFG"); + CmdLine.register_pass + ("-dump-instrumented-simplified-cfg", dump_cfg true true, "dump simplified CFG"); diff --git a/duet/proofspace.ml b/duet/proofspace.ml index 6c600e0f..e5ec80f3 100644 --- a/duet/proofspace.ml +++ b/duet/proofspace.ml @@ -64,6 +64,8 @@ module IV = struct Some (Hashtbl.find sym_to_var sym) else None + + let is_global _ = failwith "unimplemented" end module P = struct diff --git a/duet/reachTree.ml b/duet/reachTree.ml new file mode 100644 index 00000000..0ca5c440 --- /dev/null +++ b/duet/reachTree.ml @@ -0,0 +1,616 @@ +(** reachability tree module *) + +open Srk +open BatPervasives +module RG = Interproc.RG +module WG = Srk.WeightedGraph +module G = RG.G +module Int = SrkUtil.Int +module TF = TransitionFormula + +module TransitionSystem = Srk.TransitionSystem +module Syntax = Srk.Syntax +module Interpretation = Srk.Interpretation + + +include Log.Make (struct + let name = "reachTree" +end) + +type equery = OverApprox | UnderApprox + +module ART + (G : sig + type t + type vertex + type weight + val fold_succ : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a + val weight : t -> vertex -> vertex -> weight + val summary : t -> vertex -> weight + val compare_vertex : vertex -> vertex -> int + val pp_vertex : Format.formatter -> vertex -> unit + end) + (L : sig + type t + val top : t + val meet : t -> t -> t + val leq : t -> t -> bool + val negate : t -> t + val pp : Format.formatter -> t -> unit + end) + (T : sig + type t + type label + type state + val check : label -> t list -> label -> [ `Valid of label list + | `Invalid of state + | `Unknown ] + val post_model : state -> t -> state option + val is_deterministic : t -> bool + val mul : t -> t -> t + val assume : label -> t + val guard : t -> label + val pp_state : Format.formatter -> state -> unit + end with type t = G.weight + and type label = L.t) = +struct + (* type for a tree node *) + type node = int + type state = T.state + type weight = T.t + + module IntMap = BatMap.Make (Int) + module VertexMap = BatMap.Make(struct + type t = G.vertex + let compare = G.compare_vertex + end) + module StringMap = BatMap.Make (String) + module ISet = BatSet.Make (Int) + module DQ = BatDeque + module ARR = Batteries.DynArray + + let log_formulas prefix formulas = + List.iteri + (fun i f -> + logf "[formula] %s(%i): %a\n" prefix i + L.pp f) + formulas + + type node_info = + { parent : int + ; cfg_vertex : G.vertex + ; mutable label : L.t + ; mutable children : int list } + + type t = { + graph : G.t; + err_loc : G.vertex; + nodes : node_info ARR.t; + precondition : L.t; + mutable covers : int IntMap.t; + (* also maintain reverse map for each y, storing (x, y) that are in cover. *) + (* i.e. reverse_covers[y] returns all x such that (x,y) is in the cover. *) + mutable reverse_covers : ISet.t IntMap.t; + (* precedent_nodes[v] stores all tree nodes mapping to CFG vertex v. Used in mc_close. *) + mutable precedent_nodes : ISet.t VertexMap.t; + mutable frontier : node DQ.t; + } + + let root = 0 + + let make (g : G.t) (precondition : L.t) ~(src : G.vertex) ~(dst : G.vertex) = + let nodes = ARR.make 65536 in + ARR.add nodes { parent = -1 + ; cfg_vertex = src + ; label = L.top + ; children = [] }; + { graph = g + ; err_loc = dst + ; nodes = nodes + ; precondition = precondition + ; covers = IntMap.empty (* for (u, v) in cover, u is ancestor of v and label(v) |= label(u). v is covered if (u, v) in cover. Then cover[v] = u. *) + ; reverse_covers = IntMap.empty (* for each v, store the v's that cover it: i.e. cover[v] *) + ; precedent_nodes = VertexMap.empty + ; frontier = DQ.cons root DQ.empty } + + let get_err_loc (art : t) = art.err_loc + let get_entry (art: t) = (ARR.get art.nodes 0).cfg_vertex + let get_precondition (art : t) = art.precondition + + (** [print_tree t ident v] prints an ART t with indentation `ident` rooted at node v *) + let print_tree (art : t) (indent : string) (v : node) = + let rec print_tree_ (art : t) indent v = + logf "%s|" indent; + logf "%s+-%d(%a)" indent v + G.pp_vertex (ARR.get art.nodes v).cfg_vertex; + List.iter + (fun x -> print_tree_ art (indent ^ " ") x) + (ARR.get art.nodes v).children + in + logf "*"; + print_tree_ art indent v + + (* [parent t i] gets parent of node i in tree t. *) + let parent (art : t) (i : node) : node = (ARR.get art.nodes i).parent + + + (* [t %-> i]: get CFG vertex mapped by node i in tree t. *) + let maps_to (art : t) (i : node) : G.vertex = (ARR.get art.nodes i).cfg_vertex + + let parent_weight (art : t) (i : node) = + let parent = (ARR.get art.nodes i).parent in + if parent < 0 then + None + else + Some (parent, G.weight art.graph (maps_to art parent) (maps_to art i)) + + (* [tree_path t u] returns list of tree nodes that form the corrsp. tree path from root of t to tree node u *) + let tree_path (art : t) ?(src=root) (u : node) : node list = + let rec tree_path_rev art u = + if u = root || u = src then [ u ] + else u :: tree_path_rev art (parent art u) + in + List.rev @@ tree_path_rev art u + + (* [children t v] returns children of tree node v in tree t. *) + let children (art : t) (v : node) : node list = (ARR.get art.nodes v).children + + (* [descendants t v] returns descendants of tree node v in tree t in DFS order. *) + let rec descendants (art : t) (v : node) : node list = + let v_children = children art v in + v :: List.fold_left (fun l ch -> descendants art ch @ l) [] v_children + + (* is a node in tree a leaf? *) + let is_leaf (art : t) (v : node) : bool = + match children art v with + | [] -> true + | _ -> false + + (* [label t v] returns the node label of tree node v in tree t. *) + let label (art : t) (v : node) : L.t = (ARR.get art.nodes v).label + + (* [get_precedent_nodes t v] retrieves a sequence of precedent nodes of tree node vin preorder in tree t. *) + (* the list of precedent nodes for a cfg vertex is a list of tree nodes which map to the same cfg location, ordered by < on integers. *) + let get_precedent_nodes (art : t) (v : node) = + let cfg_vertex = maps_to art v in + let precedents_set = + VertexMap.find_default ISet.empty cfg_vertex art.precedent_nodes + in + ISet.elements precedents_set + + (* Add new tree leaf mapping to CFG vertex v and with parent tree node p. *) + let add_tree_vertex (art : t) ?(label = L.top) (v : G.vertex) + (p : node) = + (* note that new_vertex refers to a new tree vertex, where as v is a corresp. cfg location. *) + let id = ARR.length art.nodes in + ARR.add art.nodes { cfg_vertex = v + ; parent = p + ; label = label + ; children = [] }; + + (* set children of parent to be vtxcnt :: children. *) + begin if p >= 0 then + let parent = ARR.get art.nodes p in + parent.children <- id::parent.children + end; + (* Add v to precedent_nodes. *) + let precedent_nodes = + VertexMap.find_default ISet.empty v art.precedent_nodes + |> ISet.add id + in + art.precedent_nodes <- VertexMap.add v precedent_nodes art.precedent_nodes; + id + + let deque_frontier art = + match DQ.front art.frontier with + | None -> None + | Some (u, frontier') -> + art.frontier <- frontier'; + Some u + + let add_frontier art node = art.frontier <- DQ.snoc art.frontier node + + let expand (art : t) (v : node) = + G.fold_succ (fun succ () -> + let new_node = add_tree_vertex art succ v in + add_frontier art new_node) + art.graph + (maps_to art v) + () + + (** maintenance of coverings *) + + (* for w that is an ancestor/precedent of v, *) + (* Adds (v -> w) to covering relation if possible and returns true, false otherwise. *) + (* note that (v, w) in covering if stateLabel(v) IMPLIES stateLabel(w) *) + let cover (art : t) v w = + let v_label = label art v in + let w_label = label art w in + if maps_to art v <> maps_to art w then + failwith + @@ Format.asprintf "error: %d->%a but %d->%a\n" + v + G.pp_vertex (maps_to art v) + w + G.pp_vertex (maps_to art w) + else if L.leq v_label w_label then begin + logf " cover success (v=%d, w=%d). \n" v w; + log_formulas " v label " [ v_label ]; + log_formulas " w label " [ w_label ]; + let reverse_covers_w = + IntMap.find_default ISet.empty w art.reverse_covers + in + art.covers <- IntMap.add v w art.covers; + art.reverse_covers <- + IntMap.add w (ISet.add v reverse_covers_w) art.reverse_covers; + true + end else false + + + let fold_leaves art f v acc = + let rec go worklist acc = + match worklist with + | [] -> acc + | v::worklist -> + match children art v with + | [] -> go worklist (f v acc) + | children -> go (List.rev_append children worklist) acc + in + go [v] acc + + (** [close art v] visits precedents of v in tree and attempts to derive covering relations from v. *) + let close (art : t) (v : node) = + (* A _precedent_ of v in tree is any vertex u + if status || w == v || w > v (* preorder constraint *) then + (status, wl) + else + (* try to "cover v" by deciding if v --> w. If so, no need to further explore v. *) + (* cover v using w *) + let cover_success = cover art v w in + let wl' = ref wl in + (if cover_success then + (* remove, for each descendant of v, nodes that are sinks of covers. *) + let v_descendants = descendants art v in + List.iter + (fun y -> + (* Find relations (x,y) in covering relation where y is descendant of v. *) + if y <> v then ( + (* xs = {x | x -> y} *) + let xs = + IntMap.find_default ISet.empty y art.reverse_covers + in + (* Iterate through and remove pairs (x, y) from covering relation. *) + (* Step 1: Remove (x |-> y) from ptt.covers. *) + ISet.iter + (fun x -> art.covers <- IntMap.remove x art.covers) + xs; + (* Step 2: Remove (y |-> xs) from pthit.reverse_covers. *) + art.reverse_covers <- IntMap.remove y art.reverse_covers; + (* Step 3: add xs to worklist. *) + ISet.iter + (fun x -> + (* add x's subtree leaves back to the worklist. *) + fold_leaves + art + (fun x_leaf () -> + logf + " close: adding %d back to worklist \n" + x_leaf; + wl' := x_leaf :: !wl') + x + ()) + xs)) + v_descendants); + (cover_success, !wl')) + precedents (false, []) + in + result + + (* Checks if tree node v is covered. It is covered if its ancestors or it is in covering relation. *) + let rec is_covered (art : t) v = + match IntMap.find_opt v art.covers with + | None -> if v == 0 then false else is_covered art (parent art v) + | Some u -> + logf " | covered by %d\n" u; + true + + (* refine the label of each tree node u along path from tree root to v. *) + let refine (art : t) path interpolants = + List.iter2 + (fun u interpolant -> + let u_info = ARR.get art.nodes u in + let u_label' = L.meet u_info.label interpolant in + log_formulas + (Format.asprintf "[relabelling %d CFG vertex %a] to label: " u + G.pp_vertex (maps_to art u)) + [ u_label' ]; + u_info.label <- u_label'; + (* remove ( * -> u) in covering relation; we justined label(u) so implications of form label(y)->label(u) + might not hold anymore. *) + match IntMap.find_opt u art.reverse_covers with + | None -> () + | Some l -> + (* remove covers (List.iter (fun x -> Printf.printf " (%d->%d)" x u) l *) + let u_coverers = + ISet.fold + (fun x coverers -> + (* test if label(x) --> new label(u)*) + let x_label = label art x in + let u_label = label art u in + if L.leq x_label u_label then + (logf + " refine: cover (x %d-> u %d) still holds\n" x u; + log_formulas " x label: " [ x_label ]; + log_formulas " u label: " [ u_label ]; + ISet.add x coverers (* unchanged. *)) + else begin + (* remove (x, u) from covering. *) + logf " refine: removing cover (%d->%d)\n" + x u; + art.covers <- IntMap.remove x art.covers; + (* add x's subtree leaves back to the worklist. *) + fold_leaves + art + (fun x_leaf () -> + logf + " refine: adding %d back to worklist \n" + x_leaf; + add_frontier art x_leaf) + x + (); + coverers + end) + l + ISet.empty + in + art.reverse_covers <- IntMap.add u u_coverers art.reverse_covers) + path + interpolants + + + let rec glue l = + match l with + | a :: b :: t -> (a, b) :: (glue (b :: t)) + | _ -> [] + + + + (* convention: w is an ancestor of v. returns true if we can add (v, w) to covers such that label(v) |= label(w) *) + let force_cover (art : t) v w = (* check if v_label -> w_label where v is an ancestor at w *) + if maps_to art v <> maps_to art w then false + else begin + logf "force_cover(%d, %d)\n" v w; + (* let v_label = label art v in *) + let w_label = label art w in + let artpath = tree_path art ~src:w v in + let path_weights = + artpath + |> glue + |> List.map (fun (x, y) -> + G.weight art.graph (maps_to art x) (maps_to art y)) + in + match T.check w_label path_weights w_label with + | `Valid itps -> + refine art (List.tl artpath) (List.tl itps); + assert (cover art v w); + true + + | `Invalid _ -> false + | `Unknown -> failwith "force_cover: interpolation failed with status UNKNOWN." + end + + + (** a more lightweight version of close *) + let lclose (art: t) v = + let rec go u = + if u = -1 then false + else begin + if maps_to art u <> maps_to art v then + try go (parent art u) + with Not_found -> false + else + if force_cover art v u then true + else + try go (parent art u) + with Not_found -> false + end + in + let res = match v with + | 0 -> false + | _ -> go (parent art v) + in + logf " --- lclose result of %d : %b ---\n" v res ; res + + + (** TODO: [deprecated] procedures for lightweight verification of ART invariants *) + + let _verify_well_labelled_tree (t : t) = + let rec aux v = + let children = children t v in + match children with + | [] (* leaf node *) -> ( + match IntMap.find_opt v t.covers with + | None -> + logf "!!! found uncovered leaf: %d\n" v; + G.fold_succ + (fun y _ -> + logf + " ERROR ERROR ERROR: mapped cfg vertex %a has \ + out-neighbor %a\n" + G.pp_vertex (maps_to t v) + G.pp_vertex y; + false) + t.graph (maps_to t v) true + | Some _ -> true) + | _ -> ( + match IntMap.find_opt v t.covers with + | None -> + logf "node %d uncovered\n" v; + List.fold_left (fun acc u -> aux u && acc) true children + | Some u -> + logf "node %d covered by %d\n" v u; + true) + in + logf "verifying well-labelledness of ART...\n"; + let r = aux 0 in + logf "...done verifying well-labelledness of ART\n"; + r + + let _check_covering_welformedness (t : t) = + logf "checking welformedness of covering relations\n"; + IntMap.iter + (fun dst covered_from -> + ISet.iter + (fun src -> + logf "checking if (%d, %d) in covering\n" src dst; + match IntMap.find_opt src t.covers with + | Some dst' -> + if dst' <> dst then + failwith + @@ Printf.sprintf "ERROR: (%d, %d) in covering\n" src dst' + | None -> failwith "ERROR: not in covering") + covered_from) + t.reverse_covers; + logf "performing a reverse check\n"; + IntMap.iter + (fun src dst -> + match IntMap.find_opt dst t.reverse_covers with + | Some reverse_covers -> ( + match ISet.mem src reverse_covers with + | false -> + failwith + @@ Printf.sprintf + "ERROR: (%d, %d) in t.covers but %d not in %d's \ + reverse_covers\n" + src dst src dst + | true -> ()) + | None -> + failwith + @@ Printf.sprintf + "ERROR: (%d, %d) in t.covers but no list found in \ + reverse_covers\n" + src dst) + t.covers; + logf "...done checking welformedness of covering relations\n" + + (** pretty-printing functionalities *) + let tree_printer_get_name (art : t) i = + match IntMap.find_opt i art.covers with + | None -> Format.asprintf "%d(%a)" i G.pp_vertex (maps_to art i) + | Some j -> + Format.asprintf "[%d(%a)]->%d" i G.pp_vertex (maps_to art i) j + + let log_art (art : t) = + logf " +----------------- ART ----------------+\n"; + let string_of_art = + Tree_printer.to_string ~line_prefix:"* " + ~get_name:(tree_printer_get_name art) + ~get_children:(children art) 0 + in + logf "%s" string_of_art; + logf " +----------------- ART ----------------+\n" + + let log_node u = + logf " node: visit %d\n" u + + let pp_node = Format.pp_print_int + + let of_node u = u + + let execute art node state = + let rec loop worklist = + match worklist with + | [] -> `Safe + | (u, u_model)::worklist -> + logf " visit %d (%a)\n" u G.pp_vertex (maps_to art u); + if (maps_to art u) = (get_err_loc art) then begin + logf " *** found path-to-error"; + (* We're abandoning the search without exhausting worklist, so + worklist must be added to frontier. *) + List.iter (fun (v, _) -> art.frontier <- DQ.snoc art.frontier v) worklist; + `Unsafe u + end else begin + logf "model of %d (%a): @[%a@]" + u + G.pp_vertex (maps_to art u) + T.pp_state u_model; + let u_v = maps_to art u in + let worklist = + G.fold_succ (fun succ worklist -> + let succ_node = add_tree_vertex art succ u in + let weight = G.weight art.graph u_v succ in + let weight = + if T.is_deterministic weight then weight + else + T.mul weight (T.assume @@ T.guard @@ G.summary art.graph succ) + in + match T.post_model u_model weight with + | Some model -> (succ_node,model)::worklist + | None -> add_frontier art succ_node; worklist) + art.graph + u_v + worklist + in + loop worklist + end + in + loop [(node, state)] + + let path_to_error art node = G.summary art.graph (maps_to art node) + + let generate_test art node = + let post = L.negate (T.guard (path_to_error art node)) in + let rec get_path rest node = + match parent_weight art node with + | Some (p, weight) -> get_path (weight::rest) p + | None -> rest + in + let path = get_path [] node in + match T.check art.precondition path post with + | `Invalid v_model -> + logf ~level:`trace "-> found test"; + `Test v_model + | `Unknown -> failwith "generate_test: got UNKNOWN as a result for interpolate_or_get_model" + | `Valid interpolants -> + logf ~level:`trace "-> pruned"; + log_formulas "interpolants - " interpolants; + refine art (tree_path art node) interpolants; + `Pruned + + let gps art = + let rec loop () = + match deque_frontier art with + | None -> `Safe + | Some u -> + (* Fetched tree node u from work list. First attempt to close it. *) + logf ~level:`trace "At frontier node %d:" u; + if is_covered art u then + (logf ~level:`trace "-> covered"; + loop ()) + else begin + if lclose art u then (* Close succeeded. No need to further explore it. *) + (logf ~level:`trace "-> closed"; loop ()) + else begin + (* u is uncovered. *) + match generate_test art u with + | `Pruned -> (* refinement succeeded *) + (* for every node along path of refinement try close *) + List.iter (fun v -> ignore (close art v)) (tree_path art u); + + loop () + | `Test state -> + logf ~level:`trace "-> found test"; + match execute art u state with + | `Safe -> loop () + | `Unsafe n -> `Unsafe n + end + end + in + loop () + +end diff --git a/duet/reachTree.mli b/duet/reachTree.mli new file mode 100644 index 00000000..674146fe --- /dev/null +++ b/duet/reachTree.mli @@ -0,0 +1,73 @@ +module TransitionSystem = Srk.TransitionSystem +module Syntax = Srk.Syntax +module Interpretation = Srk.Interpretation + +type equery = OverApprox | UnderApprox +module ART + (G : sig + type t + type vertex + type weight + val fold_succ : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a + val weight : t -> vertex -> vertex -> weight + val summary : t -> vertex -> weight + val compare_vertex : vertex -> vertex -> int + val pp_vertex : Format.formatter -> vertex -> unit + end) + (L : sig + type t + val top : t + val bottom : t + val meet : t -> t -> t + val leq : t -> t -> bool + val negate : t -> t + val pp : Format.formatter -> t -> unit + end) + (T : sig + type t + type label + type state + val check : label -> t list -> label -> [ `Valid of label list + | `Invalid of state + | `Unknown ] + val post_model : state -> t -> state option + val is_deterministic : t -> bool + val mul : t -> t -> t + val assume : label -> t + val guard : t -> label + val pp_state : Format.formatter -> state -> unit + end with type t = G.weight + and type label = L.t) : sig + type node + type t + type state = T.state + type weight = T.t + val make : G.t -> L.t -> src:G.vertex -> dst:G.vertex -> t + val get_entry : t -> G.vertex + val get_err_loc : t -> G.vertex + val get_precondition : t -> L.t + val print_tree : t -> string -> node -> unit + val parent : t -> node -> node + val parent_weight : t -> node -> (node * weight) option + val maps_to : t -> node -> G.vertex + val add_frontier : t -> node -> unit + val deque_frontier : t -> node option + val tree_path : t -> ?src:node -> node -> node list + val is_leaf : t -> node -> bool + val label : t -> node -> L.t + val expand : t -> node -> unit + val close : t -> node -> (bool * node list) + val force_cover : t -> node -> node -> bool + val lclose : t -> node -> bool + val is_covered : t -> node -> bool + val refine: t -> node list -> L.t list -> unit + val log_art : t -> unit + val log_node : node -> unit + val of_node : node -> int + val root : node + val pp_node : Format.formatter -> node -> unit + val execute : t -> node -> T.state -> [ `Safe | `Unsafe of node ] + val gps : t -> [ `Safe | `Unsafe of node ] + val path_to_error : t -> node -> weight + val generate_test : t -> node -> [ `Test of state | `Pruned ] +end diff --git a/duet/summaryProvider.ml b/duet/summaryProvider.ml new file mode 100644 index 00000000..56ff7e02 --- /dev/null +++ b/duet/summaryProvider.ml @@ -0,0 +1,244 @@ +open Core +open Srk +open CfgIr +open BatPervasives +open Cra + +(* + +include Log.Make(struct let name = "sgt" end) + +module IntMap = BatMap.Make(Int) +module StringMap = BatMap.Make(String) +module DQ = BatDeque +module ARR = Batteries.DynArray +type idq_t = int BatDeque.t +type state_formula = Ctx.t Syntax.formula +exception Mexception of string + + + + +let log_formulas prefix formulas = + List.iteri (fun i f -> logf "[formula] %s(%i): %a\n" prefix i (Syntax.pp_expr srk) f) formulas + +let log_weights prefix weights = + List.iteri (fun i f -> logf "[weight] %s(%i): %a\n" prefix i K.pp f) weights + + +let log_model prefix model = + logf "[model] %s: %a\n" prefix Interpretation.pp model + +module LeftRegularSummaryProvider (Ctx: Srk.Syntax.Context) +(** transition formula algebra *) +(K : sig + type t + type var + val pp : Format.formatter -> t -> unit + val guard : t -> Ctx.t Srk.Syntax.formula + val transform : t -> (var * Ctx.t Srk.Syntax.arith_term) BatEnum.t + val mem_transform : var -> t -> bool + val get_transform : var -> t -> Ctx.t Srk.Syntax.arith_term + val assume : Ctx.t Srk.Syntax.formula -> t + val mul : t -> t -> t + val add : t -> t -> t + val conjunct : t -> t -> t + val zero : t + val one : t + val star : t -> t + val exists : (var -> bool) -> t -> t + val contains_havoc : t -> bool + val contextualize : t -> t -> t -> [ `Sat of t | `Unsat ] + val interpolate_or_concrete_model : t list -> Ctx.t Syntax.formula + -> [`Valid of Ctx.t Syntax.formula list + | `Invalid of Ctx.t Interpretation.interpretation | `Unknown ] + + val get_post_model : + Ctx.t Srk.Interpretation.interpretation -> + t -> Ctx.t Srk.Interpretation.interpretation option + val is_deterministic : t -> bool + end) + (TS : sig + type vertex + type transition = K.t + type t + type query + type reverse_query + val empty : t + val path_weight : query -> vertex -> transition + val call_weight : query -> vertex * vertex -> transition + val mk_reverse_query : query -> vertex -> reverse_query + val exit_summary : reverse_query -> vertex -> vertex -> K.t + val target_summary : reverse_query -> vertex -> K.t + val set_summary : query -> vertex * vertex -> transition -> unit + val get_summary : query -> vertex * vertex -> transition + val simplify : ?try_rtc:bool -> (vertex -> bool) -> t -> t + val iter_succ_e : + ((vertex * (transition TransitionSystem.label) * vertex) -> unit) -> t -> vertex -> unit + val edge_weight : + t -> vertex -> vertex -> K.t Srk.TransitionSystem.label + val fold_succ_e : (vertex * (K.t Srk.TransitionSystem.label) * vertex -> 'b -> 'b) -> t -> vertex -> 'b -> 'b + end) += +struct + type t = { + graph: TS.t; + src: int; + query: TS.query; + rev_query: TS.reverse_query; + silent: bool; + monotone: bool; + } + let mk_query ts entry = TS.mk_query ts entry (if !monotone then (module MonotoneDom) else (module TransitionDom)) + + let init (graph: TS.t) (src: int) (tgt: int) (enable_summary: bool) : t = + let q = mk_query graph src in + let rq = TS.mk_reverse_query q tgt in + { graph = graph + ; src = src + ; query = q + ; rev_query = rq + ; silent = not enable_summary } + + + let path_weight_intra (ctx: t) (src: int) (dst: int) = + TS.exit_summary ctx.rev_query src dst + + let path_weight_inter (ctx: t) (src: int) = + TS.target_summary ctx.rev_query src + +end + +module InterproceduralSummaryProvider(ProcName : sig + type t = int * int + val make : TS.vertex * TS.vertex -> t + val string_of : t -> string + val of_string : string -> t + val compare : t -> t -> int +end) += + struct + module SMap = BatMap.Make(ProcName) + type t = { + graph: cfg_t; + src: int; + query: TS.query; + rev_query: TS.reverse_query; + mutable underapprox: K.t SMap.t; + mutable overapprox: K.t SMap.t; (* Caution: used only for silent mode where no CRA-generated summaries are used. *) + } + + let init (graph: cfg_t) (src: int) (tgt: int) : t = + let q = mk_query graph src in + let rq = TS.mk_reverse_query q tgt in + { graph = graph + ; src = src + ; query = q + ; rev_query = rq + ; underapprox = SMap.empty + ; overapprox = SMap.empty } + + (** retrieve over-approximate procedure summary *) + let over_proc_summary (ctx: t) ((u, v) : ProcName.t) = + TS.get_summary ctx.query (u, v) + |> K.exists (V.is_global) + + (** set over-approximate procedure summary *) + let set_over_proc_summary (ctx: t) ((u, v): ProcName.t) (w: K.t) = + TS.set_summary ctx.query (u, v) w + + (** retrieve under-approximate procedure summary *) + let under_proc_summary (ctx: t) ((u, v): ProcName.t) : K.t = + match SMap.find_default K.zero (u, v) ctx.underapprox + |> K.project_mbp (V.is_global) + with + | `Sat tr -> tr + | _ -> + log_weights "under_proc_summary: this weight is unsat: " [SMap.find_default K.zero (u, v) ctx.underapprox]; + K.zero + (*failwith "under_proc_summary: cannot model-based project"*) + + (** set under-approximate procedure summary *) + let set_under_proc_summary (ctx: t) ((u, v): ProcName.t) (w: K.t) : unit = + ctx.underapprox <- SMap.add (u, v) w ctx.underapprox + + (** refinement of procedure summaries using a two-voc transition formula *) + let refine_over_summary (ctx: t) ((u, v): ProcName.t) (rfn: K.t) = + over_proc_summary ctx (u, v) + |> K.conjunct rfn + |> set_over_proc_summary ctx (u, v) + + let refine_under_summary (ctx: t) ((u, v): ProcName.t) (w:K.t) : unit = + let summary = under_proc_summary ctx (u, v) in + let summary' = K.add summary w in + log_weights "under-approx summary refined to " [summary']; + set_under_proc_summary ctx (u, v) summary' + + end + +module SilentSummaryProvider(ProcName : sig + type t = int * int + val make : TS.vertex * TS.vertex -> t + val string_of : t -> string + val of_string : string -> t + val compare : t -> t -> int +end) = +struct + module SMap = BatMap.Make(ProcName) + type t = { + graph: cfg_t; + src: int; + mutable underapprox: K.t SMap.t; + mutable overapprox: K.t SMap.t; (* Caution: used only for silent mode where no CRA-generated summaries are used. *) + } + + let init (graph: cfg_t) (src: int) (tgt: int) : t = + { graph = graph + ; src = src + ; underapprox = SMap.empty + ; overapprox = SMap.empty } + + (** retrieve over-approximate procedure summary *) + let over_proc_summary (ctx: t) ((u, v) : ProcName.t) = + match SMap.find_opt (u, v) ctx.overapprox with + | Some s -> s + | None -> + let init = K.assume @@ mk_true () in + ctx.overapprox <- SMap.add (u, v) init ctx.overapprox; + init + + (** set over-approximate procedure summary *) + let set_over_proc_summary (ctx: t) ((u, v): ProcName.t) (w: K.t) = + match SMap.find_opt (u, v) ctx.overapprox with + | Some s -> + ctx.overapprox <- SMap.add (u, v) (K.conjunct s w) ctx.overapprox + | None -> + ctx.overapprox <- SMap.add (u, v) w ctx.overapprox + + (** retrieve under-approximate procedure summary *) + let under_proc_summary (ctx: t) ((u, v): ProcName.t) : K.t = + match SMap.find_default K.zero (u, v) ctx.underapprox |> K.project_mbp (V.is_global) with + | `Sat tr -> tr + | _ -> + log_weights "under_proc_summary: this weight is unsat: " [SMap.find_default K.zero (u, v) ctx.underapprox]; + K.zero + + (** set under-approximate procedure summary *) + let set_under_proc_summary (ctx: t) ((u, v): ProcName.t) (w: K.t) : unit = + ctx.underapprox <- SMap.add (u, v) w ctx.underapprox + + (** refinement of procedure summaries using a two-voc transition formula *) + let refine_over_summary (ctx: t) ((u, v): ProcName.t) (rfn: K.t) = + match SMap.find_opt (u, v) ctx.overapprox with + | Some s -> + ctx.overapprox <- SMap.add (u, v) (K.conjunct s rfn) ctx.overapprox + | None -> + ctx.overapprox <- SMap.add (u, v) rfn ctx.overapprox + + let refine_under_summary (ctx: t) ((u, v): ProcName.t) (w:K.t) : unit = + let summary = under_proc_summary ctx (u, v) in + let summary' = K.add summary w in + log_weights "under-approx summary refined to " [summary']; + set_under_proc_summary ctx (u, v) summary' +end +*) \ No newline at end of file diff --git a/duet/summaryProvider.mli b/duet/summaryProvider.mli new file mode 100644 index 00000000..0fe44028 --- /dev/null +++ b/duet/summaryProvider.mli @@ -0,0 +1,159 @@ +(* +module TransitionSystem = Srk.TransitionSystem +module Syntax = Srk.Syntax +module Interpretation = Srk.Interpretation +*) +(* +module LeftRegularSummaryProvider : + functor + (Ctx: Srk.Syntax.Context) + (** transition formula algebra *) + (K : sig + type t + type var + val pp : Format.formatter -> t -> unit + val guard : t -> Ctx.t Srk.Syntax.formula + val transform : t -> (var * Ctx.t Srk.Syntax.arith_term) BatEnum.t + val mem_transform : var -> t -> bool + val get_transform : var -> t -> Ctx.t Srk.Syntax.arith_term + val assume : Ctx.t Srk.Syntax.formula -> t + val mul : t -> t -> t + val add : t -> t -> t + val conjunct : t -> t -> t + val zero : t + val one : t + val star : t -> t + val exists : (var -> bool) -> t -> t + val contains_havoc : t -> bool + val contextualize : t -> t -> t -> [ `Sat of t | `Unsat ] + val interpolate_or_concrete_model : t list -> Ctx.t Syntax.formula + -> [`Valid of Ctx.t Syntax.formula list + | `Invalid of Ctx.t Interpretation.interpretation | `Unknown ] + + val get_post_model : + Ctx.t Srk.Interpretation.interpretation -> + t -> Ctx.t Srk.Interpretation.interpretation option + val is_deterministic : t -> bool + end) + (TS : sig + type vertex + type transition = K.t + type t + type query + type reverse_query + val empty : t + val path_weight : query -> vertex -> transition + val call_weight : query -> vertex * vertex -> transition + val mk_reverse_query : query -> vertex -> reverse_query + val exit_summary : reverse_query -> vertex -> vertex -> K.t + val target_summary : reverse_query -> vertex -> K.t + val set_summary : query -> vertex * vertex -> transition -> unit + val get_summary : query -> vertex * vertex -> transition + val simplify : ?try_rtc:bool -> (vertex -> bool) -> t -> t + val iter_succ_e : + ((vertex * (transition TransitionSystem.label) * vertex) -> unit) -> t -> vertex -> unit + val edge_weight : + t -> vertex -> vertex -> K.t Srk.TransitionSystem.label + val fold_succ_e : (vertex * (K.t Srk.TransitionSystem.label) * vertex -> 'b -> 'b) -> t -> vertex -> 'b -> 'b + end) + -> sig + type t + val init : TS.t -> int -> int -> bool -> t + val path_weight_intra : t -> int -> int -> TS.transition + val path_weight_inter : t -> int -> TS.transition + end + +module InterproceduralSummaryProvider : +(Ctx: Srk.Syntax.Context) +(K : sig + type t + type var + val pp : Format.formatter -> t -> unit + val guard : t -> Ctx.t Srk.Syntax.formula + val transform : t -> (var * Ctx.t Srk.Syntax.arith_term) BatEnum.t + val mem_transform : var -> t -> bool + val get_transform : var -> t -> Ctx.t Srk.Syntax.arith_term + val assume : Ctx.t Srk.Syntax.formula -> t + val mul : t -> t -> t + val add : t -> t -> t + val conjunct : t -> t -> t + val zero : t + val one : t + val star : t -> t + val exists : (var -> bool) -> t -> t + val contains_havoc : t -> bool + val contextualize : t -> t -> t -> [ `Sat of t | `Unsat ] + val interpolate_or_concrete_model : t list -> Ctx.t Syntax.formula + -> [`Valid of Ctx.t Syntax.formula list + | `Invalid of Ctx.t Interpretation.interpretation | `Unknown ] + + val get_post_model : + Ctx.t Srk.Interpretation.interpretation -> + t -> Ctx.t Srk.Interpretation.interpretation option + val is_deterministic : t -> bool + end) +(TS : sig + type vertex + type transition = K.t + type t + type query + type reverse_query + val empty : t + val path_weight : query -> vertex -> transition + val call_weight : query -> vertex * vertex -> transition + val mk_reverse_query : query -> vertex -> reverse_query + val exit_summary : reverse_query -> vertex -> vertex -> K.t + val target_summary : reverse_query -> vertex -> K.t + val set_summary : query -> vertex * vertex -> transition -> unit + val get_summary : query -> vertex * vertex -> transition + val simplify : ?try_rtc:bool -> (vertex -> bool) -> t -> t + val iter_succ_e : + ((vertex * (transition TransitionSystem.label) * vertex) -> unit) -> t -> vertex -> unit + val edge_weight : + t -> vertex -> vertex -> K.t Srk.TransitionSystem.label + val fold_succ_e : (vertex * (K.t Srk.TransitionSystem.label) * vertex -> 'b -> 'b) -> t -> vertex -> 'b -> 'b + end) + (ProcName : sig + type t = int * int + val make : int * int -> t + val string_of : t -> string + val of_string : string -> t + val compare : t -> t -> int + end) + -> + sig + type t + val init : TS.t -> int -> int -> t + val over_proc_summary : t -> ProcName.t -> TS.transition + val set_over_proc_summary : t -> ProcName.t -> TS.transition -> unit + val under_proc_summary : t -> ProcName.t -> TS.transition + val set_under_proc_summary : t -> ProcName.t -> TS.transition -> unit + val refine_over_summary : t -> ProcName.t -> TS.transition -> unit + val refine_under_summary : t -> ProcName.t -> TS.transition -> unit + end + +module SilentSummaryProvider : +functor + (TS : sig + type t + type transition + end) + (ProcName : sig + type t = int * int + val make : int * int -> t + val string_of : t -> string + val of_string : string -> t + val compare : t -> t -> int + end) + -> + sig + type t + val init : TS.t -> int -> int -> t + val over_proc_summary : t -> ProcName.t -> TS.transition + val set_over_proc_summary : t -> ProcName.t -> TS.transition -> unit + val under_proc_summary : t -> ProcName.t -> TS.transition + val set_under_proc_summary : t -> ProcName.t -> TS.transition -> unit + val refine_over_summary : t -> ProcName.t -> TS.transition -> unit + val refine_under_summary : t -> ProcName.t -> TS.transition -> unit + end +*) \ No newline at end of file diff --git a/duet/translateCil.ml b/duet/translateCil.ml index 49694d7b..18906776 100644 --- a/duet/translateCil.ml +++ b/duet/translateCil.ml @@ -298,8 +298,8 @@ let rec tr_expr = function | Cil.Mod -> BinaryOp (e1, Mod, e2, typ) | Cil.Shiftlt -> BinaryOp (e1, ShiftL, e2, typ) | Cil.Shiftrt -> BinaryOp (e1, ShiftR, e2, typ) - | Cil.BAnd -> BinaryOp (e1, BAnd, e2, typ) - | Cil.BOr -> BinaryOp (e1, BOr, e2, typ) + | Cil.BAnd -> BoolExpr (And (Bexpr.of_aexpr e1, Bexpr.of_aexpr e2)) (* BinaryOp (e1, BAnd, e2, typ) *) + | Cil.BOr -> BoolExpr (Or (Bexpr.of_aexpr e1, Bexpr.of_aexpr e2)) (* BinaryOp (e1, BOr, e2, typ) *) | Cil.BXor -> BinaryOp (e1, BXor, e2, typ) | Cil.Lt -> BoolExpr (Atom (Lt, e1, e2)) | Cil.Gt -> BoolExpr (Bexpr.gt e1 e2) @@ -396,6 +396,7 @@ let verifier_builtins = "pthread_mutex_lock"; "pthread_mutex_unlock"; "spin_lock"; "spin_unlock"; "pthread_create"; "pthread_create"; "exit"; "abort"; "rand"; "__VERIFIER_nondet_char"; "__VERIFIER_nondet_int"; "__VERIFIER_nondet_long"; + "__VERIFIER_nondet_bool"; "__VERIFIER_nondet_uchar"; "__VERIFIER_nondet_pointer"; "__VERIFIER_nondet_uint"; "__CPROVER_atomic_begin"; "__CPROVER_atomic_end"; "__VERIFIER_atomic_begin"; "__VERIFIER_atomic_end"] @@ -478,6 +479,13 @@ let tr_instr ctx instr = | ("__VERIFIER_nondet_char", Some (Variable v), []) -> mk_def (Assign (v, Havoc (Concrete (Int 1)))) + | ("__VERIFIER_nondet_uchar", Some (Variable v), []) -> + let havoc = mk_def (Assign (v, Havoc (Concrete (Int 1)))) in + let assume0 = + mk_def (Assume (Atom (Le, Aexpr.zero, AccessPath (Variable v)))) in + let assume1 = + mk_def (Assume (Atom (Le, AccessPath (Variable v), Constant (CInt (255, 1))))) in + mk_seq havoc @@ mk_seq assume0 assume1 | ("__VERIFIER_nondet_int", Some (Variable v), []) -> mk_def (Assign (v, Havoc (Concrete (Int machine_int_width)))) | ("__VERIFIER_nondet_long", Some (Variable v), []) -> @@ -485,6 +493,13 @@ let tr_instr ctx instr = mk_def (Assign (v, Havoc (Concrete (Int sz)))) | ("__VERIFIER_nondet_pointer", Some (Variable v), []) -> mk_def (Assign (v, Havoc (Concrete (Int pointer_width)))) + | ("__VERIFIER_nondet_bool", Some (Variable v), []) -> + let assume_lb = + mk_def (Assume (Atom (Le, Aexpr.zero, AccessPath (Variable v)))) in (* 0 <= v *) + let assume_ub = + mk_def (Assume (Atom (Le, AccessPath (Variable v), Aexpr.one))) in (* v <= 1 *) + let havoc = mk_def (Assign (v, Havoc (Concrete (Int 1)))) in + mk_seq havoc @@ mk_seq assume_lb assume_ub | ("__VERIFIER_nondet_uint", Some (Variable v), []) -> let havoc = mk_def (Assign (v, Havoc (Concrete (Int unknown_width)))) in let assume = @@ -791,3 +806,4 @@ let parse filename = let () = CmdLine.register_parser ("c", parse); CmdLine.register_parser ("i", parse_preprocessed); + diff --git a/duet/tree_printer.ml b/duet/tree_printer.ml new file mode 100644 index 00000000..543fa6d7 --- /dev/null +++ b/duet/tree_printer.ml @@ -0,0 +1,39 @@ +open Printf + +let rec iter f = function + | [] -> () + | [x] -> + f true x + | x :: tl -> + f false x; + iter f tl + +let to_buffer ?(line_prefix = "") ~get_name ~get_children buf x = + let rec print_root indent x = + bprintf buf "%s\n" (get_name x); + let children = get_children x in + iter (print_child indent) children + and print_child indent is_last x = + let line = + if is_last then + "└── " + else + "├── " + in + bprintf buf "%s%s" indent line; + let extra_indent = + if is_last then + " " + else + "│ " + in + print_root (indent ^ extra_indent) x + in + Buffer.add_string buf line_prefix; + print_root line_prefix x + +let to_string ?line_prefix ~get_name ~get_children x = + let buf = Buffer.create 1000 in + to_buffer ?line_prefix ~get_name ~get_children buf x; + Buffer.contents buf + diff --git a/duet/tree_printer.mli b/duet/tree_printer.mli new file mode 100644 index 00000000..74711f9f --- /dev/null +++ b/duet/tree_printer.mli @@ -0,0 +1,16 @@ +(* + Print a tree or a DAG as tree, similarly to the 'tree' command. + Source: https://gist.github.com/mjambon/75f54d3c9f1a352b38a8eab81880a735 +*) + +val to_buffer : + ?line_prefix: string -> + get_name: ('a -> string) -> + get_children: ('a -> 'a list) -> + Buffer.t -> 'a -> unit + +val to_string : + ?line_prefix: string -> + get_name: ('a -> string) -> + get_children: ('a -> 'a list) -> + 'a -> string \ No newline at end of file diff --git a/srk/dune-project b/srk/dune-project index 8f5722aa..64bc2358 100644 --- a/srk/dune-project +++ b/srk/dune-project @@ -2,7 +2,6 @@ (name srk) (using menhir 2.0) (generate_opam_files true) - (package (name srk) (synopsis "Symbolic Reasoning Kit") diff --git a/srk/src/dune b/srk/src/dune index ecd62a9c..11e8c5ed 100644 --- a/srk/src/dune +++ b/srk/src/dune @@ -12,6 +12,7 @@ (public_name srk) (modules (:standard \ bigtop)) (modes native) + (flags (:standard -w -32)) (libraries batteries ppx_deriving ppx_deriving.show ppx_deriving.ord ppx_deriving.eq diff --git a/srk/src/interpretation.ml b/srk/src/interpretation.ml index 328d3f50..4e1a806c 100644 --- a/srk/src/interpretation.ml +++ b/srk/src/interpretation.ml @@ -453,3 +453,7 @@ let select_ite interp ?(env=Env.empty) expr = in let expr' = rewrite interp.srk ~down:rewriter expr in (expr', !conditions) + + +let restrict (f : symbol -> bool) interp = + {interp with map = SM.filter (fun k _ -> f k) interp.map} diff --git a/srk/src/interpretation.mli b/srk/src/interpretation.mli index 8bc69590..baa28298 100644 --- a/srk/src/interpretation.mli +++ b/srk/src/interpretation.mli @@ -67,6 +67,9 @@ val select_ite : 'a interpretation -> ('a,'b) expr -> (('a,'b) expr) * ('a formula list) +val restrict : (symbol -> bool) -> 'a interpretation -> 'a interpretation + + val destruct_atom : 'a context -> 'a formula -> [ `ArithComparison of ([`Lt | `Leq | `Eq] * 'a arith_term * 'a arith_term) diff --git a/srk/src/iteration.ml b/srk/src/iteration.ml index 71266167..269c057e 100644 --- a/srk/src/iteration.ml +++ b/srk/src/iteration.ml @@ -20,7 +20,7 @@ module Solver = struct let preprocess srk = function | `LIRR -> Syntax.eliminate_floor_mod_div srk - | `LIRA -> rewrite srk ~down:(pos_rewriter srk) % (Nonlinear.linearize srk) + | `LIRA -> rewrite srk ~down:(pos_rewriter srk) % (Nonlinear.linearize srk) % Syntax.eliminate_floor_mod_div srk let make srk ?(theory=get_theory srk) tf = let phi = preprocess srk theory (TF.formula tf) in diff --git a/srk/src/smt.mli b/srk/src/smt.mli index 81a2f1f2..6a3bbd6b 100644 --- a/srk/src/smt.mli +++ b/srk/src/smt.mli @@ -25,6 +25,11 @@ module StdSolver : sig val get_unsat_core : 'a t -> ('a formula) list -> [ `Sat | `Unsat of ('a formula) list | `Unknown ] + val get_unsat_core_or_model : ?symbols:symbol list -> 'a t -> + ('a formula) list -> + [ `Sat of 'a interpretation + | `Unsat of ('a formula) list + | `Unknown ] end module Model : sig diff --git a/srk/src/srkZ3.ml b/srk/src/srkZ3.ml index d1a6db92..5085efe8 100644 --- a/srk/src/srkZ3.ml +++ b/srk/src/srkZ3.ml @@ -574,6 +574,19 @@ module Solver = struct | `Unsat -> `Unsat (List.map solver.formula_of (Z3.Solver.get_unsat_core solver.s)) + let get_unsat_core_or_model ?(symbols=[]) solver assumptions = + let srk = solver.srk in + let z3 = solver.z3 in + match check ~assumptions solver with + | `Sat -> + begin match Z3.Solver.get_model solver.s with + | Some m -> `Sat (Interpretation.wrap ~symbols srk (model_get_value srk z3 m)) + | None -> `Unknown + end + | `Unknown -> `Unknown + | `Unsat -> + `Unsat (List.map solver.formula_of (Z3.Solver.get_unsat_core solver.s)) + let get_reason_unknown solver = Z3.Solver.get_reason_unknown solver.s end diff --git a/srk/src/srkZ3.mli b/srk/src/srkZ3.mli index c0d4def5..510c8d2a 100644 --- a/srk/src/srkZ3.mli +++ b/srk/src/srkZ3.mli @@ -80,6 +80,13 @@ module Solver : sig ('a formula) list -> [ `Sat | `Unsat of ('a formula) list | `Unknown ] + + val get_unsat_core_or_model : ?symbols: symbol list -> 'a t -> + ('a formula) list -> + [ `Sat of 'a interpretation + | `Unsat of ('a formula) list + | `Unknown ] + val get_reason_unknown : 'a t -> string end diff --git a/srk/src/syntax.mli b/srk/src/syntax.mli index e9bdade4..f96232fd 100644 --- a/srk/src/syntax.mli +++ b/srk/src/syntax.mli @@ -559,6 +559,9 @@ val pp_smtlib2 : ?env:(string Env.t) -> 'a context -> val pp_expr_unnumbered : ?env:(string Env.t) -> 'a context -> Format.formatter -> ('a, 'b) expr -> unit +val pp_expr : ?env:(string Env.t) -> 'a context -> + Format.formatter -> ('a, 'b) expr -> unit + module Formula : sig type 'a t = 'a formula val equal : 'a formula -> 'a formula -> bool diff --git a/srk/src/transition.ml b/srk/src/transition.ml index 2343a783..fa2cfa09 100644 --- a/srk/src/transition.ml +++ b/srk/src/transition.ml @@ -11,6 +11,8 @@ module type Var = sig val compare : t -> t -> int val symbol_of : t -> symbol val of_symbol : symbol -> t option + + val is_global : t -> bool end module Make @@ -113,40 +115,47 @@ struct (M.map (substitute_const srk left_subst) right.transform) in { transform; guard } - - let add left right = - let left_eq = ref [] in - let right_eq = ref [] in - let transform = - let merge v x y = - match x, y with - | Some s, Some t when Term.equal s t -> Some s - | _, _ -> - let phi = - mk_symbol srk ~name:("phi_" ^ (Var.show v)) ((Var.typ v) :> typ) - |> mk_const srk - in - let left_term = - match x with - | Some s -> s - | None -> mk_const srk (Var.symbol_of v) - in - let right_term = - match y with - | Some t -> t - | None -> mk_const srk (Var.symbol_of v) - in - left_eq := (mk_eq srk left_term phi)::(!left_eq); - right_eq := (mk_eq srk right_term phi)::(!right_eq); - Some phi + let compose left right ty = + let left_eq = ref [] in + let right_eq = ref [] in + let transform = + let merge v x y = + match x, y with + | Some s, Some t when Term.equal s t -> Some s + | _, _ -> + let phi = + mk_symbol srk ~name:("phi_" ^ (Var.show v)) ((Var.typ v) :> typ) + |> mk_const srk + in + let left_term = + match x with + | Some s -> s + | None -> mk_const srk (Var.symbol_of v) + in + let right_term = + match y with + | Some t -> t + | None -> mk_const srk (Var.symbol_of v) + in + left_eq := (mk_eq srk left_term phi)::(!left_eq); + right_eq := (mk_eq srk right_term phi)::(!right_eq); + Some phi + in + M.merge merge left.transform right.transform in - M.merge merge left.transform right.transform - in - let guard = - mk_or srk [mk_and srk (left.guard::(!left_eq)); - mk_and srk (right.guard::(!right_eq))] - in - { guard; transform } + let guard = match ty with + | `Add -> + mk_or srk [mk_and srk (left.guard::(!left_eq)); + mk_and srk (right.guard::(!right_eq))] + | `And -> + mk_and srk [mk_and srk (left.guard::(!left_eq)); + mk_and srk (right.guard::(!right_eq))] + in + { guard; transform } + + let add left right = compose left right `Add + let conjunct left right = compose left right `And + (* Canonical names for post-state symbols. Having canonical names simplifies equality testing and widening. *) @@ -438,10 +447,459 @@ struct (wp::itp, wp)) trs guards - ([post], post) + ([ + mk_not srk post + |> Quantifier.mbp srk (fun x -> Var.of_symbol x <> None) + |> mk_not srk + ], post) in `Valid (List.tl itp) + + let get_post_model m f = + let f_guard = guard f in + let replacer (sym : Syntax.symbol) = + if Var.of_symbol sym == None then Syntax.mk_const C.context sym + else mk_real C.context @@ Interpretation.real m sym + in + let f_guard' = Syntax.substitute_const C.context replacer f_guard in + let symbols = Syntax.symbols f_guard' |> Symbol.Set.elements in + let post pm = + BatEnum.fold (fun m' (lhs, rhs) -> + let sub_expr = Syntax.substitute_const C.context replacer rhs in + let lhs_symbol = Var.symbol_of lhs in + let sub_val = Interpretation.evaluate_term pm sub_expr in + Interpretation.add lhs_symbol (`Real sub_val) m') + m + (M.enum f.transform) + in + match Formula.destruct srk f_guard' with + | `Fls -> None + | `Tru -> + let zero_model = Interpretation.wrap srk (fun s -> + match typ_symbol srk s with + | `TyInt | `TyReal -> `Real QQ.zero + | `TyBool -> `Bool true + | _ -> assert false) + in + Some (post zero_model) + | _ -> + match Smt.get_model ~symbols:(symbols) C.context f_guard' with + | `Sat skolem_model -> Some (post skolem_model) + | _ -> None + + (* helper method for interpolate/extrapolate procedures. creates fresh copies of skolem variables in tr *) + let rename_skolems tr = + let fresh_skolem = + Memo.memo (fun sym -> + match Var.of_symbol sym with + | Some _ -> mk_const srk sym + | None -> + let name = show_symbol srk sym in + let typ = typ_symbol srk sym in + mk_const srk (mk_symbol srk ~name typ)) + in + { transform = M.map (substitute_const srk fresh_skolem) tr.transform; + guard = substitute_const srk fresh_skolem tr.guard } + + let interpolate_unsat_core trs post guards core = + let core_symbols = + List.fold_left (fun core phi -> + match Formula.destruct srk phi with + | (`Proposition (`App (s, []))) -> Symbol.Set.add s core + | _ -> assert false) + Symbol.Set.empty + core + in + let (itp, _) = + List.fold_right2 (fun tr guard (itp, post) -> + let subst sym = + match Var.of_symbol sym with + | Some var -> + if M.mem var tr.transform then + M.find var tr.transform + else + mk_const srk sym + | None -> mk_const srk sym + in + let post' = substitute_const srk subst post in + let reduced_guard = + List.filter_map (fun (indicator, guard) -> + if Symbol.Set.mem indicator core_symbols then + Some (mk_not srk guard) + else + None) + guard + in + let wp = + (mk_not srk (mk_or srk (post'::reduced_guard))) + |> Quantifier.mbp srk (fun s -> Var.of_symbol s != None) + |> mk_not srk + in + (wp::itp, wp)) + trs + guards + ([ + mk_not srk post + |> Quantifier.mbp srk (fun x -> Var.of_symbol x <> None) + |> mk_not srk + ], post) + in `Valid (List.tl itp) + + + let interpolate_query trs post sat_callback unsat_callback = + let solver = Smt.StdSolver.make C.context in + (* Break guards into conjunctions, associate each conjunct with an indicator *) + let guards = + List.map (fun tr -> + List.map + (fun phi -> (mk_symbol srk `TyBool, phi)) + (destruct_and srk tr.guard)) + trs in + let indicators, indicator_symbols = + List.concat_map (List.map (fun (s, _) -> mk_const srk s)) guards, + List.concat_map (List.map fst) guards |> Symbol.Set.of_list + in + let subscript_tbl = Hashtbl.create 991 in + let ss_inv = Hashtbl.create 991 in + let sst = Hashtbl.create 991 in + let subscript sym = + try + Hashtbl.find subscript_tbl sym + with Not_found -> mk_const srk sym + in + (* Convert tr into a formula, and simultaneously update the subscript + table *) + let to_ss_formula tr guards = + let ss_guards = + List.map (fun (indicator, guard) -> + mk_if srk + (mk_const srk indicator) + (substitute_const srk subscript guard)) + guards + in + let (ss, phis) = + M.fold (fun var term (ss, phis) -> + let var_sym = Var.symbol_of var in + let var_ss_sym = mk_symbol srk (Var.typ var :> typ) in + let var_ss_term = mk_const srk var_ss_sym in + let term_ss = substitute_const srk subscript term in + ((var_sym, var_ss_sym, var_ss_term)::ss, + mk_eq srk var_ss_term term_ss::phis)) + tr.transform + ([], ss_guards) + in + List.iter (fun (k, l, v) -> + Hashtbl.add subscript_tbl k v; + Hashtbl.add ss_inv l k; + Hashtbl.add sst k l) ss; + mk_and srk phis + in + (* gather all symbols into a list, while adding formulas to the solver object *) + let symbols, added_formulas = List.fold_left + (fun (symbols, added_formulas) (tr, guard) -> + let f = to_ss_formula tr guard in + Smt.StdSolver.add solver [f]; + (Syntax.symbols f) :: symbols, f::added_formulas) + ([], []) (List.combine trs guards) in + let _ = List.iter (fun f -> + let f = substitute_const srk + (fun v -> + match Hashtbl.find_opt ss_inv v with + | None -> Syntax.mk_const srk v + | Some v' -> Syntax.mk_const srk v') f + in logf "added formula: %a\n" (Syntax.pp_expr srk) f) added_formulas + (* subscript the symbols in the `post` formula, as well *) in + let target = substitute_const srk subscript (mk_not srk post) in + let symbols = (Syntax.symbols target) :: symbols + |> List.rev + |> List.map (fun ss -> Symbol.Set.diff ss indicator_symbols) in + Smt.StdSolver.add solver [target]; + logf "-----------------------------interpolation---\n"; + List.iter (fun f -> + let f = substitute_const srk + (fun v -> + match Hashtbl.find_opt ss_inv v with + | None -> Syntax.mk_const srk v + | Some v' -> Syntax.mk_const srk v') f + in logf "indicator formula: %a\n" (Syntax.pp_expr srk) f) indicators; + logf "-------------------interpolation end---\n"; + logf "--- indicator length %d\n" @@ List.length indicators; + logf "\ntarget formula: %a\n" (Syntax.pp_expr srk) target; + match Smt.StdSolver.get_unsat_core_or_model solver indicators with + | `Sat m -> + (sat_callback m symbols sst ss_inv) + | `Unsat core -> (unsat_callback trs post guards core) + | `Unknown -> `Unknown + + + (* let interpolate trs post = + let trs = List.map rename_skolems trs in + interpolate_query trs post (fun _ _ _ _ -> `Invalid) @@ interpolate_unsat_core +*) + let interpolate_or_concrete_model trs post = + (* subst_model: rename skolem constants back to their appropriate names using reverse subscript table *) + let trs = List.map rename_skolems trs in + let sat_model model (symbols: Symbol.Set.t list) ss ss_inv = + let m = + List.fold_left (fun m' symbols -> + Symbol.Set.fold (fun s m -> + (* the provided model is over both subscripted vocabulary and original vocabulary *) + begin match Hashtbl.find_opt ss_inv s with + | Some s' -> (* subscripted variable *) + Interpretation.add s' (Interpretation.value model s) m + | None -> (* non-subscripted; query directly *) + Interpretation.add s (Interpretation.value model s) m + end) symbols m' + ) (Interpretation.wrap srk (fun s -> + match Hashtbl.find_opt ss s with + | Some sss -> Interpretation.value model sss + | None -> `Real (Q.of_int 47))) (*(Interpretation.wrap srk (fun s -> + match Hashtbl.find_opt ss s with + | Some sss -> Interpretation.value model sss + | None -> Interpretation.value model s))*) (*(Interpretation.empty srk)*) symbols in + logf "hashtable length: %d\n" (Hashtbl.length ss_inv); + logf "%a" Interpretation.pp m; + Format.print_flush (); + (* symbols is a list of subscripted symbols arranged in left-to-right order. + folding over this in left-to-right order amounts to forward concrete execution. *) + `Invalid (m + |> Interpretation.restrict + (fun s -> + match Var.of_symbol s with + | Some _ -> true + | None -> false)) + in interpolate_query trs post sat_model @@ interpolate_unsat_core + + + let vocabulary tr = + let tr_guard = guard tr in + let tr_trans = transform tr in + let guard_v = tr_guard |> Syntax.symbols in + let trans_v = BatEnum.fold (fun s (var, term) -> + let s = Symbol.Set.add (Var.symbol_of var) s in + let t = Syntax.symbols term in + Symbol.Set.union s t) Symbol.Set.empty tr_trans in + let v = Symbol.Set.union guard_v trans_v in + let globals = Symbol.Set.filter (fun x -> + match Var.of_symbol x with + | Some var -> Var.is_global var + | None -> false ) v in + let locals = Symbol.Set.diff v globals in + (Symbol.Set.to_list globals, Symbol.Set.to_list locals) + + + let contextualize t1 t2 t3 : [`Sat of t | `Unsat ] = + let t1 = rename_skolems t1 + in let t2 = rename_skolems t2 + in let t3 = rename_skolems t3 + in let subscript subscript_tbl sym = + try + Hashtbl.find subscript_tbl sym + with Not_found -> + mk_const srk sym + in + (* preprocess each formula to get rid of certain undesirable things *) + let preprocess_formula f = + let pos_rewriter = Syntax.pos_rewriter srk in + f |> Syntax.eliminate_ite srk + |> Syntax.eliminate_floor_mod_div srk + |> Syntax.rewrite srk ~down:pos_rewriter in + (* Convert tr into a formula, and simultaneously update the subscript + table *) + let to_ss_formula tr subscript_tbl reverse_subscript_tbl = + let ss_guard = substitute_const srk (subscript subscript_tbl) (guard tr) + in let (ss, phis) = + M.fold (fun var term (ss, phis) -> + let var_sym = Var.symbol_of var in + let var_ss_sym = mk_symbol srk (Var.typ var :> typ) in + let var_ss_term = mk_const srk var_ss_sym in + let term_ss = substitute_const srk (subscript subscript_tbl) term in + ((var_sym, var_ss_term, var_ss_sym)::ss, + (mk_eq srk var_ss_term term_ss)::phis)) + tr.transform + ([], [ ss_guard ]) + in + List.iter (fun (k, v, l) -> + Hashtbl.add subscript_tbl k v; Hashtbl.add reverse_subscript_tbl l k) ss; + mk_and srk phis |> preprocess_formula, Hashtbl.copy reverse_subscript_tbl + in let subscript_tbl = Hashtbl.create 991 + in let reverse_subscript_tbl = Hashtbl.create 991 + in let ss_t1, reverse_subscript_tbl1 = to_ss_formula t1 subscript_tbl reverse_subscript_tbl + in let ss_t2, reverse_subscript_tbl2 = to_ss_formula t2 subscript_tbl reverse_subscript_tbl + in let ss_t3, _ = to_ss_formula t3 subscript_tbl reverse_subscript_tbl + in let conj = mk_and srk [ss_t1; ss_t2; ss_t3] + in let is_global t x = + try + begin match Var.of_symbol (Hashtbl.find t x) with + | None -> false + | Some v -> + if Var.is_global v then begin + logf "symbol %s is global\n" (Syntax.show_symbol srk (Hashtbl.find reverse_subscript_tbl x)); true + end else false + end + with Not_found -> false + in let symbols_t1 = Syntax.symbols ss_t1 + in let symbols_t2 = Syntax.symbols ss_t2 + in let symbols_t3 = Syntax.symbols ss_t3 + in let symbols_t1_t2 = + Syntax.symbols ss_t1 (* symbols in t1 that are either globals _and_ in t2 are preserved during projection *) + |> Symbol.Set.filter + (fun x -> (is_global reverse_subscript_tbl1 x)) + in let symbols_t3_t2 = + symbols_t3 (* symbols in t3 that are globals _and_ in t2, t1 are preserved during projection *) + |> Symbol.Set.filter (fun x -> (is_global reverse_subscript_tbl2 x) && (Symbol.Set.mem x symbols_t2)) + in let symbols_conj = Symbol.Set.union symbols_t1 (Symbol.Set.union symbols_t2 symbols_t3) + in + let project srk (f1: 'a formula) (f3: 'a formula) symbols_f1 symbols_f3 all_symbols model = + let open Polyhedron in + (* first do POS conversion on f1, f3 before computing their implicants *) + (* rjf Mar '24: we do this as part of preprocessing to avoid rewriting the formula after an SMT query to get `model`*) + (*let pos_rewriter = Syntax.pos_rewriter srk in + let f1 = Syntax.rewrite srk ~down:(pos_rewriter) f1 in + let f3 = Syntax.rewrite srk ~down:(pos_rewriter) f3 in*) + let implicant_o1 = Interpretation.select_implicant model f1 in + let implicant_o2 = Interpretation.select_implicant model f3 in + match implicant_o1, implicant_o2 with + | Some f1, Some f2 -> + let cube = of_cube srk (f1@f2) in + let value_of_coord = (* coord (int) -> x (symbol) -> m[x] (value in R) *) + fun coord -> + Syntax.symbol_of_int coord + |> Interpretation.real model + in let xs = + Symbol.Set.diff all_symbols (Symbol.Set.union symbols_f1 symbols_f3) + |> Symbol.Set.elements + |> List.map Syntax.int_of_symbol + in let projected = local_project value_of_coord xs cube + in cube_of srk projected |> Syntax.mk_and srk + | None, Some f -> + logf "contextualize: select_implicant failed on left formula: \n"; + logf "\n-- left formula: %a\n" (Syntax.pp_expr srk) f1; + logf "\n-- right formula:%a\n" (Syntax.pp_expr srk) f3; + List.iteri (fun _ x -> logf "\n -- impicant of right formula:%a\n" (Syntax.pp_expr srk) x) f; + logf "\n * model: %a\n" (Interpretation.pp) model; + failwith "error extrapolating: select_implicant failed on left formula" + | Some f, None -> + logf "contextualize: select_implicant failed on right formula: \n"; + logf "\n-- left formula: %a\n" (Syntax.pp_expr srk) f1; + List.iteri (fun _ x -> logf "\n -- impicant of left formula:%a\n" (Syntax.pp_expr srk) x) f; + logf "\n-- right formula:%a\n" (Syntax.pp_expr srk) f3; + logf "\n * model: %a\n" (Interpretation.pp) model; + failwith "error extrapolating: select_implicant failed on right formula" + | None, None -> + logf "left: %a\n" (Syntax.pp_expr srk) f1; + Format.print_flush (); + logf "right: %a\n" (Syntax.pp_expr srk) f3; + Format.print_flush (); + logf "\n * model: %a\n" (Interpretation.pp) model; + Format.print_flush (); + failwith "error extrapolating: select_implicant failed on both formulae" + in + match Smt.get_model ~symbols:(symbols_conj |> Symbol.Set.elements) srk conj with + | `Sat m -> + let prepost = project srk ss_t1 ss_t3 symbols_t1_t2 symbols_t3_t2 symbols_conj m in + let reverse_rename_t1 s = + begin match Hashtbl.find_opt reverse_subscript_tbl1 s with + | Some s' -> mk_const srk s' + | None -> mk_const srk s end in + let r_guard = substitute_const srk (reverse_rename_t1) prepost in + let r_transform = + (* for each skolem symbol in r_guard, see if it can be mapped back to a variable. *) + let r_symbols = Syntax.symbols r_guard |> Symbol.Set.to_list in + List.fold_left (fun m x -> + match Hashtbl.find_opt reverse_subscript_tbl x with + | Some y -> + begin match Var.of_symbol y with + | Some var -> M.add var (mk_const srk x) m + | None -> m + end + | None -> m) M.empty r_symbols in + let r = {transform=r_transform; guard=r_guard} + in + `Sat r + | `Unknown -> failwith "contextualize status unknown" + | `Unsat -> `Unsat + + + + (** underapproximate existential quantification. Given a transition formula tr over vocabulary X, + use model-based projection to project out any variable v in X such that f(v) = false. *) + let project_mbp (f : var -> bool) tr = + let ss_to_sym = Hashtbl.create 991 in + (* preprocessing of a formula *) + let preprocess f = + let pos_rewriter = Syntax.pos_rewriter srk in + f |> Syntax.eliminate_ite srk |> Syntax.eliminate_floor_mod_div srk + |> Syntax.rewrite srk ~down:pos_rewriter in + let phis = + M.fold (fun var term phis -> + let var_sym = Var.symbol_of var in + let var_ss_sym = mk_symbol srk (Var.typ var :> typ) in + let var_ss_term = mk_const srk var_ss_sym in + Hashtbl.add ss_to_sym var_ss_sym var_sym; + (mk_eq srk var_ss_term term)::phis) + tr.transform + [ guard tr ] in + let tr_formula = mk_and srk phis |> preprocess in + let tr_symbols = Syntax.symbols tr_formula in + let tr_symbols_preserved = + tr_symbols + |> Symbol.Set.filter (fun s -> + match Hashtbl.find_opt ss_to_sym s with + | Some sym -> + begin match Var.of_symbol sym with + | Some v -> f v + | None -> false + end + | None -> false (* discard any skolem constants *)) in + let tr_symbols_removed = Symbol.Set.diff tr_symbols tr_symbols_preserved in + let prj formula voc model = + let open Polyhedron in + (* first do POS conversion on [formula] before computing their implicants *) + (* rjf Mar '24: This is done using the preprocess function defined above.*) + (*let pos_rewriter = Syntax.pos_rewriter srk in + let formula' = + formula + |> Syntax.eliminate_ite srk + |> Syntax.eliminate_floor_mod_div srk + |> Syntax.rewrite srk ~down:(pos_rewriter) in*) + let implicant = Interpretation.select_implicant model formula in + match implicant with + | Some i -> + let cube = of_cube srk i in + let value_of_coord = (* coord (int) -> x (symbol) -> m[x] (value in R) *) + fun coord -> + Syntax.symbol_of_int coord + |> Interpretation.real model + in let xs = (* coordinates to be projected out *) + voc + |> Symbol.Set.elements + |> List.map Syntax.int_of_symbol + in let projected = local_project value_of_coord xs cube + in cube_of srk projected |> Syntax.mk_and srk + | _ -> + logf "\n--select_implicant formula: %a\n" (Syntax.pp_expr srk) formula; + Format.print_flush (); + logf "\n--select_implicant model: %a\n" (Interpretation.pp) model; + Format.print_flush(); + failwith "error projecting: select_implicant returned None" + in match Smt.get_model ~symbols:(tr_symbols |> Symbol.Set.elements) srk tr_formula with + | `Sat m -> + let projected = prj tr_formula tr_symbols_removed m in + let tr_transform = + Hashtbl.fold (fun ss sym acc -> + let ss_term = mk_const srk ss in + match Var.of_symbol sym with + | Some v -> M.add v ss_term acc + | None -> failwith "u_exists: shoul not get here: subscript invariant broken") + ss_to_sym M.empty + in + `Sat {guard=projected;transform=tr_transform} + | `Unknown -> failwith "u_exists: got unknown as a result of get_model" + | _ -> `Unsat + + let valid_triple phi path post = let path_not_post = List.fold_right mul path (assume (mk_not srk post)) in match Smt.is_sat srk (mk_and srk [phi; path_not_post.guard]) with @@ -492,6 +950,20 @@ struct |> rewrite srk ~down:(pos_rewriter srk) |> Abstract.abstract ~exists srk man + + + let contains_havoc tr = + M.fold (fun _ rhs acc -> + if acc then acc + else begin + Symbol.Set.fold + (fun s acc -> + match Var.of_symbol s with + | Some _ -> acc + | None -> true || acc) (Syntax.symbols rhs) false + end + ) tr.transform false + let linearize tr = let (transform, defs) = M.fold (fun var t (transform, defs) -> @@ -515,4 +987,120 @@ struct Nonlinear.linearize srk (mk_and srk (tr.guard::defs)) in { transform; guard } + + let is_deterministic tr = + let tr' = rename_skolems tr in + let solver = Smt.Solver.make srk in + let same_post = + M.fold (fun var t rest -> + (mk_eq srk t (M.find var tr'.transform)::rest)) + tr.transform + [] + in + Smt.Solver.add solver [tr.guard; tr'.guard; mk_not srk (mk_and srk same_post)]; + match Smt.Solver.check solver with + | `Unsat -> true + | `Sat | `Unknown -> false + + (* Given a guarded translation and a loop counter k, compute a + representation of its k-fold repetition. *) + let cf_translation loop_counter trans guard = + let cf k = (* x + k*v *) + M.mapi (fun var t -> + mk_add srk [mk_const srk (Var.symbol_of var); mk_mul srk [mk_real srk t; k]]) + trans + in + + (* forall subcounter. 0 <= subcounter < loop_counter ==> G(Sx + t*subcounter) *) + let subcounter = mk_symbol srk `TyInt in + let subcounter_term = mk_const srk subcounter in + let prestate sym = Var.of_symbol sym != None in + let guard = Quantifier.mbp srk prestate guard in + let cf_subst = + let sub_cf = cf subcounter_term in + substitute_const srk (fun sym -> + match Var.of_symbol sym with + | Some v -> (try M.find v sub_cf with Not_found -> mk_const srk sym) + | None -> assert false) + in + let guard_tf = + mk_if srk + (mk_and srk [mk_leq srk (mk_int srk 0) subcounter_term; + mk_lt srk subcounter_term loop_counter]) + (cf_subst guard) + |> mk_not srk + |> Quantifier.mbp srk (fun x -> x != subcounter) + |> mk_not srk + in + { transform = cf loop_counter; + guard = mk_and srk [guard_tf; + mk_leq srk (mk_int srk 0) loop_counter] } + + let try_rtc tr = + let solver = Smt.StdSolver.make srk in + let translation_of_model m = + M.fold (fun var rhs trans -> + M.add + var + (QQ.sub + (Interpretation.evaluate_term m rhs) + (Interpretation.real m (Var.symbol_of var))) + trans) + tr.transform + M.empty + in + let translation_formula trans = + M.fold (fun var rhs xs -> + (mk_eq srk + (mk_sub srk rhs (mk_const srk (Var.symbol_of var))) + (mk_real srk (M.find var trans))) + ::xs + ) + tr.transform + [] + |> mk_and srk + in + Smt.StdSolver.add solver [tr.guard]; + match Smt.StdSolver.get_model solver with + | `Unknown -> None + | `Unsat -> Some one + | `Sat m -> + let trans1 = translation_of_model m in + let trans1_formula = translation_formula trans1 in + Smt.StdSolver.add solver [mk_not srk trans1_formula]; + match Smt.StdSolver.get_model solver with + | `Unsat -> + let loop_counter = mk_const srk (mk_symbol srk `TyInt) in + Some (cf_translation loop_counter trans1 tr.guard) + | `Unknown -> None + | `Sat m2 -> + let trans2 = translation_of_model m2 in + let trans2_formula = translation_formula trans2 in + Smt.StdSolver.add solver [mk_not srk trans2_formula]; + match Smt.StdSolver.check solver with + | `Sat | `Unknown -> None + | _ -> + let tr1 = { tr with guard = mk_and srk [ tr.guard; trans1_formula ] } in + let tr2 = { tr with guard = mk_and srk [ tr.guard; trans2_formula ] } in + match Smt.is_sat srk (guard (mul tr1 tr2)), + Smt.is_sat srk (guard (mul tr2 tr1)) + with + | `Unsat, `Sat -> (* 12 UNSAT => (1+2)* = 2*1* *) + let loop_counter1 = mk_const srk (mk_symbol srk `TyInt) in + let loop_counter2 = mk_const srk (mk_symbol srk `TyInt) in + Some (mul + (cf_translation loop_counter2 trans2 tr2.guard) + (cf_translation loop_counter1 trans1 tr1.guard)) + | `Sat, `Unsat -> (* 21 UNSAT => (1+2)* = 1*2* *) + let loop_counter1 = mk_const srk (mk_symbol srk `TyInt) in + let loop_counter2 = mk_const srk (mk_symbol srk `TyInt) in + Some (mul + (cf_translation loop_counter1 trans1 tr1.guard) + (cf_translation loop_counter2 trans2 tr2.guard)) + | `Unsat, `Unsat -> (* 12 & 21 UNSAT => (1+2)* = 1*+2* *) + let loop_counter = mk_const srk (mk_symbol srk `TyInt) in + Some (add + (cf_translation loop_counter trans1 tr1.guard) + (cf_translation loop_counter trans2 tr2.guard)) + | _, _ -> None end diff --git a/srk/src/transition.mli b/srk/src/transition.mli index 5eba6e6b..465254f6 100644 --- a/srk/src/transition.mli +++ b/srk/src/transition.mli @@ -9,6 +9,7 @@ module type Var = sig val compare : t -> t -> int val symbol_of : t -> symbol val of_symbol : symbol -> t option + val is_global : t -> bool end module Make @@ -70,6 +71,9 @@ module Make (** Non-deterministically choose between two transitions *) val add : t -> t -> t + (** take conjunction of two transition formulas *) + val conjunct : t -> t -> t + (** Unexecutable transition (unit of [add]). *) val zero : t @@ -110,9 +114,32 @@ module Make support the proof (for each [i], [{ phi_{i-1} } tr_i { phi_i }] holds, where [phi_0] is [true] and [phi_n] implies the post-condition). *) - val interpolate : t list -> C.t formula -> [ `Valid of C.t formula list - | `Invalid - | `Unknown ] + val interpolate : t list -> C.t formula -> [ `Valid of C.t formula list + | `Invalid + | `Unknown ] + + val contextualize : t -> t -> t -> [ `Sat of t | `Unsat ] + + (** Same as interpolate, but returns a concrete model if interpllation fails. *) + val interpolate_or_concrete_model : t list -> C.t formula + -> [`Valid of C.t formula list | `Invalid of C.t Interpretation.interpretation | `Unknown ] + + + + (** + transtion : guard, transform + interpretation: M + find a model of the guard where we use M to replace all the pre-state value. + check interpretation.substitute + *) + val get_post_model : C.t Interpretation.interpretation -> t -> (C.t Interpretation.interpretation) option + + + (** Underapproximate existential quantification using model-based projection. + The variables to be preserved are set to `true` in the initial map. + Note the input map specifies variables to be preserved, not removed. *) + val project_mbp : (var -> bool) -> t -> [> `Sat of t | `Unsat] + (** Given a pre-condition [P], a path [path], and a post-condition [Q], determine whether the Hoare triple [{P}path{Q}] is valid. *) @@ -120,6 +147,9 @@ module Make | `Invalid | `Unknown ] + val contains_havoc : t -> bool + + val defines : t -> var list val uses : t -> var list @@ -131,4 +161,18 @@ module Make val domain : (C.t Iteration.exp_op) ref val star : t -> t val linearize : t -> t + + (** If [is_deterministic tr] holds, [tr] is deterministic (at most one + post-state for any given pre-state). If [is_deterministic tr] does not + hold, either [tr] is non-deterministic, or a proof of determinacy could + not be found. *) + val is_deterministic : t -> bool + + (** Attempt to compute the reflexive transitive closure of the input + transition formula; return [None] of the exact RTC was not successfully + found. *) + val try_rtc : t -> t option + + (** vocabulary of a transition formula, (globals, locals)*) + val vocabulary : t -> ((Syntax.symbol list) * (Syntax.symbol list)) end diff --git a/srk/src/transitionSystem.ml b/srk/src/transitionSystem.ml index 63c434fc..517e9699 100644 --- a/srk/src/transitionSystem.ml +++ b/srk/src/transitionSystem.ml @@ -5,15 +5,17 @@ include Log.Make(struct let name = "srk.transitionSystem" end) module WG = WeightedGraph module Int = SrkUtil.Int +module ISet = BatSet.Make(Int) type 'a label = | Weight of 'a | Call of int * int + module Make (C : sig type t - val context : t context + val context : t context end) (Var : sig type t @@ -41,6 +43,7 @@ module Make val one : t val star : t -> t val exists : (var -> bool) -> t -> t + val try_rtc : t -> t option end) = struct @@ -49,6 +52,7 @@ module Make type tlabel = T.t label type query = T.t WG.RecGraph.weight_query + type reverse_query = T.t WG.RecGraph.reverse_query let mk_query ?(delay=1) ts source dom = let rg = @@ -149,6 +153,17 @@ module Make (add_symbols (symbols (T.guard tr)) VarSet.empty) (T.transform tr) + + let set_summary q (u, v) summary = + WG.RecGraph.set_summary q (u, v) summary + + let get_summary q (u, v) = + WG.RecGraph.get_summary q (u, v) + + let mk_reverse_query = WG.RecGraph.mk_reverse_query + let exit_summary = WG.RecGraph.exit_summary + let target_summary = WG.RecGraph.target_summary + (* Variables whose abstract values may change as the result of a transition *) let abstract_defs tr = @@ -505,16 +520,23 @@ module Make let hash = Hashtbl.hash end + module IntPairPair = struct + type t = IntPair.t * IntPair.t [@@deriving ord] + let equal (x, y) (x', y') = (x=x' && y=y') + let hash = Hashtbl.hash + end + module PS = BatSet.Make(IntPair) + module PPS = BatSet.Make(IntPairPair) (* used in inliner *) module PHT = BatHashtbl.Make(IntPair) module VHT = BatHashtbl.Make(Var) (* Remove temporary variables that are referenced by only one transition *) - let remove_temporaries tg = + let remove_temporaries proj tg = (* Map each local variable to the set of transitions that refer to it *) let ref_map = VHT.create 991 in let add_ref var (u, v) = - if not (Var.is_global var) then + if not (proj var) then VHT.modify_def PS.empty var (PS.add (u,v)) ref_map in tg |> WG.iter_edges (fun (u, label, v) -> @@ -541,7 +563,7 @@ module Make List.fold_right VarSet.remove (uses tr) (PHT.find tmp_map (u, v)) in Weight (T.exists (fun x -> not (VarSet.mem x tmp)) tr) - with Not_found -> label) + with Not_found -> label) let forward_invariants_ivl tg entry = let init v = @@ -662,18 +684,168 @@ module Make in List.map invariants (L.all_loops (L.loop_nest tg)) - let simplify p tg = + + let inline ?(depth=(-1)) tg entry (displayer: t -> unit) (assertion_map : 'x SrkUtil.Int.Map.t) = + let pmap = PHT.create 998 in (* y in pmap[x] means call from x->y *) + let qmap = PHT.create 998 in (* (x, z) in qmap[y] means call from x->y via call-edge z *) + let greatest = ref (WG.fold_vertex max tg (-1)) in + let assertions = ref assertion_map in + PHT.add pmap (entry, -1) PS.empty; + PHT.add qmap (entry, -1) PPS.empty; + let procedures = + WG.fold_edges (fun (_, w, _) acc -> + match w with + | Call (x, y) -> + begin match PHT.find_opt pmap (x, y) with + | None -> + PHT.add pmap (x, y) PS.empty + | Some _ -> () + end; + begin match PHT.find_opt qmap (x, y) with + | None -> + PHT.add qmap (x, y) PPS.empty + | Some _ -> () + end; + PS.add (x, y) acc + | _ -> acc + ) tg (PS.add (entry, -1) PS.empty) in + let rec dfs (proc: int * int) tg src (f: (vertex * vertex) -> vertex -> vertex * 'a label * vertex -> unit) (visited : ISet.t) = + Printf.printf "dfs: visiting %d\n" src; + WG.fold_succ_e (fun (u, w, v) visited -> + f proc src (u, w, v); + begin match ISet.find_opt v visited with + | None -> ISet.union (dfs proc tg v f (ISet.add v visited)) visited + | Some _ -> visited + end) tg src visited in + PS.iter (fun (x, y) -> + Printf.printf "populating p/qmaps with dfs... %d %d\n" x y; + ignore @@ dfs (x, y) tg x (fun proc src (_, w, v) -> + match w with + | Call (x, y) -> + let caller_set = PHT.find pmap proc in + let callee_set = PHT.find qmap (x, y) in + PHT.add pmap proc (PS.add (x, y) caller_set); + PHT.add qmap (x, y) (PPS.add (proc, (src, v)) callee_set); + | _ -> () + ) (ISet.add x ISet.empty)) procedures; (* populate pmap, qmap *) + let compute_sinks () = + PS.fold (fun (x, y) acc -> (* compute sink locations to start inlining from *) + match (PHT.find_opt pmap (x, y), PHT.find_opt qmap (x, y)) with + | Some callees, Some callers -> + (* a procedure is considered for inlining if it is (1) a sink in the call graph (2) at least one function calls it.*) + if ((PS.cardinal callees) == 0) && ((PPS.cardinal callers) > 0) then PS.add (x, y) acc else + begin + Printf.printf "%d %d is not a sink; num callees = %d num callers = %d\n" x y (PS.cardinal callees) (PPS.cardinal callers); + acc + end + | (_, _) -> failwith "" + ) procedures PS.empty in + let copy_subgraph tg src = + let vertices = dfs (-1, -1) tg src (fun _ _ _ -> ()) (ISet.add src ISet.empty) in + let to_map = Hashtbl.create 998 in + let rtg = ref tg in + ISet.iter (fun x -> + greatest := !greatest + 1; + Hashtbl.add to_map x (!greatest); + begin match SrkUtil.Int.Map.find_opt x !assertions with (* if x in assertions, new vertex also in assertions *) + | Some assert_value -> + assertions := SrkUtil.Int.Map.add !greatest assert_value !assertions + | None -> () end; + rtg := WG.add_vertex !rtg !greatest + ) vertices; + ISet.iter (fun x -> + rtg := WG.fold_succ_e (fun (u, w, v) tg' -> + WG.add_edge tg' (Hashtbl.find to_map u) w (Hashtbl.find to_map v)) + !rtg x !rtg) vertices; + (!rtg, Hashtbl.find to_map) + in let remove_subgraph tg src = + let vertices = dfs (-1, -1) tg src (fun _ _ _ -> ()) (ISet.add src ISet.empty) in + ISet.fold (fun vtx tg' -> + begin match SrkUtil.Int.Map.find_opt vtx !assertions with + (* remove vertex from assertions map, new copied vertices already in it *) + | Some _ -> + assertions := SrkUtil.Int.Map.remove vtx !assertions + | None -> () + end; + WG.remove_vertex tg' vtx) vertices tg in + let inline_one tg (src, dst) (call_x, call_y) (call_src, call_dst) = + Printf.printf "inlining %d-%d into call edge %d-%d\n" src dst call_x call_y; + let (tg, to_map) = copy_subgraph tg src in + let tg = WG.add_edge tg call_x (Weight T.one) (to_map src) in + let tg = WG.add_edge tg (to_map dst) (Weight T.one) call_y in + let tg = WG.remove_edge tg call_x call_y in + let callees = PHT.find pmap (call_src, call_dst) in + let callers = PHT.find qmap (src, dst) in + (* remove (src, dst) from callees list in caller *) + PHT.add pmap (call_src, call_dst) (PS.remove (src, dst) callees); + (* remove (call_src, call_dst) from callers list *) + PHT.add qmap (src, dst) (PPS.remove ((call_src, call_dst),(call_x, call_y)) callers); + tg + in let rec do_inline depth tg = + if depth == 0 then tg else + let sinks = compute_sinks () in + let aux currproc tg = (* inline currproc into procedures that call it, assuming currproc is inlined. *) + let inline_targets = PHT.find qmap currproc in + let tg' = + PPS.fold (fun (call_proc, (call_x, call_y)) tg -> + Printf.printf "do_inline: at edge %d %d\n\n" call_x call_y; + inline_one tg currproc (call_x, call_y) call_proc + ) inline_targets tg in + let (src, _) = currproc in + remove_subgraph tg' src + in + displayer tg; + match PS.cardinal sinks with + | n when n > 0 -> + Printf.printf "inliner: there are %d sinks to inline \n" n; + let tg' = (PS.fold aux sinks tg) in + tg' + |> do_inline ( + Printf.printf "doing more inling...\n"; + if depth > 0 then depth - 1 else depth) + | _ -> Printf.printf "no more sinks to inline. done\n"; tg + in let result = do_inline depth tg in + (result, !assertions) + + + + + let simplify ?(try_rtc=true) p tg = let rec go tg = + Printf.printf "simplify: simplifying...\n"; let continue = ref false in let tg' = WG.fold_vertex (fun v tg -> let ug = WG.forget_weights tg in if (p v || WG.mem_edge tg v v - || WG.U.in_degree ug v != 1 - || WG.U.out_degree ug v != 1) + || (WG.U.in_degree ug v != 1 + && WG.U.out_degree ug v != 1)) then - tg + begin if try_rtc then begin + begin if WG.mem_edge tg v v then + match WG.edge_weight tg v v with + | Weight tr -> + (try begin match T.try_rtc tr with + | Some rtc -> + let u = -1 in + (try + let tg = WG.remove_edge tg v v in + let tg = + WG.contract_vertex (WG.split_vertex tg v (Weight rtc) u) u + in + continue := true; + tg + with _ -> tg) + | None -> tg end + with _ -> tg) + | Call (_, _) -> tg + else + tg + end + end + else tg + end else begin try let tg = WG.contract_vertex tg v in diff --git a/srk/src/transitionSystem.mli b/srk/src/transitionSystem.mli index 03cd48ca..fc10abed 100644 --- a/srk/src/transitionSystem.mli +++ b/srk/src/transitionSystem.mli @@ -6,9 +6,9 @@ type 'a label = module Make (C : sig - type t - val context : t Syntax.context - end) + type t + val context : t context + end) (Var : sig type t val pp : Format.formatter -> t -> unit @@ -35,12 +35,14 @@ module Make val one : t val star : t -> t val exists : (var -> bool) -> t -> t + val try_rtc : t -> t option end) : sig type vertex = int type transition = T.t type t = (transition label) WeightedGraph.t type query = T.t WeightedGraph.RecGraph.weight_query + type reverse_query = T.t WeightedGraph.RecGraph.reverse_query module VarSet : BatSet.S with type elt = Var.t @@ -68,9 +70,19 @@ module Make starting at a given vertex. *) val omega_path_weight : query -> (transition,'b) Pathexpr.omega_algebra -> 'b - (** Project out local variables from each transition that are referenced - only by that transition. *) - val remove_temporaries : t -> t + val mk_reverse_query : query -> vertex -> reverse_query + val exit_summary : reverse_query -> vertex -> vertex -> T.t + val target_summary : reverse_query -> vertex -> T.t + + (** Project out variables that do not satisfy the given predicate from each + transition that are referenced only by that transition. *) + val remove_temporaries : (Var.t -> bool) -> t -> t + + (** Set procedure summary; delegates call to WG.RecGraph.set_summary *) + val set_summary : query -> (vertex * vertex) -> transition -> unit + + (** Get procedure summary; delegates call to WG.RecGraph.get_summary *) + val get_summary : query -> (vertex * vertex) -> transition (** Compute interval invariants for each loop header of a transition system. The invariant computed for a loop is defined only over the variables @@ -90,7 +102,11 @@ module Make the given predicate. Simplification does not guarantee that all such vertices are contracted. In particular, simplification will not contract vertices with loops or vertices adjacent to call edges. *) - val simplify : (vertex -> bool) -> t -> t + val simplify : ?try_rtc:bool -> (vertex -> bool) -> t -> t + + (** Perform inlining of a potentially recursive iCFG. + *) + val inline : ?depth:int -> t -> vertex -> (t -> unit) -> ('x SrkUtil.Int.Map.t) -> (t * 'x SrkUtil.Int.Map.t) (** Given a transition system and entry, compute a set of loop headers along with the set of variables that are read within the diff --git a/srk/src/weightedGraph.ml b/srk/src/weightedGraph.ml index d3fced8e..e9d0b947 100644 --- a/srk/src/weightedGraph.ml +++ b/srk/src/weightedGraph.ml @@ -50,6 +50,9 @@ let empty algebra = labels = M.empty; algebra = algebra } +let get_algebra wg = + wg.algebra + let add_vertex wg vertex = { wg with graph = U.add_vertex wg.graph vertex } @@ -203,9 +206,9 @@ let _solve_dense (wg : 'a weighted_graph) (src : vertex) = v, and reachable is an enumeration of the vertices reachable from src. *) let _path_weight - (wg : 'a t) - (omega : ('a, 'b) omega_algebra) - (src : vertex) = + (wg : 'a t) + (omega : ('a, 'b) omega_algebra) + (src : vertex) = (* Ensure that src has no incoming edges *) let (wg, src) = let start = max_vertex wg + 1 in @@ -225,11 +228,11 @@ let _path_weight if BatHashtbl.mem wg_to_forest v then BatHashtbl.find wg_to_forest v else begin - let r = F.root forest in - BatHashtbl.add wg_to_forest v r; - BatHashtbl.add forest_to_wg r v; - r - end + let r = F.root forest in + BatHashtbl.add wg_to_forest v r; + BatHashtbl.add forest_to_wg r v; + r + end in let find v = BatHashtbl.find forest_to_wg (F.find forest (to_forest v)) @@ -239,6 +242,9 @@ let _path_weight in let eval v = F.eval forest (to_forest v) in let idom = D.compute_idom wg.graph src in + let is_reachable x = + try ignore (idom x); true with Not_found -> false + in let children = D.idom_to_dom_tree wg.graph idom in let rec solve (v : vertex) = let children_omega = List.map solve (children v) in @@ -249,13 +255,15 @@ let _path_weight let sibling_graph = List.fold_left (fun sg child -> - U.fold_pred (fun pred sg -> - let pred = find pred in - if pred = v then sg - else U.add_edge sg pred child) - wg.graph - child - (U.add_vertex sg child)) + U.fold_pred (fun pred sg -> + if is_reachable pred then + let pred = find pred in + if pred = v then sg + else U.add_edge sg pred child + else sg) + wg.graph + child + (U.add_vertex sg child)) U.empty (children v) in @@ -263,32 +271,32 @@ let _path_weight let omega_weight = List.fold_right (fun component omega_weight -> - let component_wg = - List.fold_left (fun component_wg v -> - U.fold_pred (fun p component_wg -> - let weight = mul (eval p) (edge_weight wg p v) in - add_edge component_wg (find p) weight v) - wg.graph - v - component_wg) - (empty wg.algebra) - component - in - let reduced = _solve_dense component_wg v in - List.fold_left (fun omega_weight c -> - let v_to_c = edge_weight reduced v c in - let (omega_weight, weight) = - if U.mem_edge reduced.graph c c then - let c_to_c = edge_weight reduced c c in - let v_c_omega = omega.omega_mul v_to_c (omega.omega c_to_c) in - (omega.omega_add omega_weight v_c_omega, - mul v_to_c (star c_to_c)) - else (omega_weight, v_to_c) - in - link c weight v; - omega_weight) - omega_weight - component) + let component_wg = + List.fold_left (fun component_wg v -> + U.fold_pred (fun p component_wg -> + let weight = mul (eval p) (edge_weight wg p v) in + add_edge component_wg (find p) weight v) + wg.graph + v + component_wg) + (empty wg.algebra) + component + in + let reduced = _solve_dense component_wg v in + List.fold_left (fun omega_weight c -> + let v_to_c = edge_weight reduced v c in + let (omega_weight, weight) = + if U.mem_edge reduced.graph c c then + let c_to_c = edge_weight reduced c c in + let v_c_omega = omega.omega_mul v_to_c (omega.omega c_to_c) in + (omega.omega_add omega_weight v_c_omega, + mul v_to_c (star c_to_c)) + else (omega_weight, v_to_c) + in + link c weight v; + omega_weight) + omega_weight + component) (C.scc_list sibling_graph) (omega.omega wg.algebra.zero) in @@ -553,6 +561,11 @@ module RecGraph = struct (* An algebra for assigning weights to non-call edges and *) algebra : 'a Pathexpr.nested_algebra } + type 'a reverse_query = + { parent : 'a weight_query + ; path_to_exit : Pathexpr.nested Pathexpr.t weighted_graph + ; path_to_target : int -> Pathexpr.nested Pathexpr.t } + let pathexpr_algebra context = { mul = mk_mul context; add = mk_add context; @@ -613,6 +626,7 @@ module RecGraph = struct interproc_paths = msat_path_weight interproc [src]; src = src } + let call_pathexpr query (src, tgt) = (* intraproc_paths is only set when src is an entry vertex *) if not (U.mem_vertex query.interproc.graph src) then @@ -723,6 +737,14 @@ module RecGraph = struct query.changed := CallSet.add call !(query.changed); HT.replace query.summaries call weight + let exit_summary rev_query src tgt = + let (table, algebra) = prepare rev_query.parent in + Pathexpr.eval_nested ~table ~algebra (path_weight rev_query.path_to_exit tgt src) + + let target_summary rev_query src = + let (table, algebra) = prepare rev_query.parent in + Pathexpr.eval_nested ~table ~algebra (rev_query.path_to_target src) + let mk_weight_query query algebra = { query = query; summaries = HT.create 991; @@ -730,6 +752,70 @@ module RecGraph = struct table = Pathexpr.mk_table (); algebra = algebra } + let mk_reverse_query weight_query tgt = + let rg = weight_query.query.recgraph in + let context = rg.context in + let reverse f graph = (* Reverse edges in a graph *) + let reverse_algebra = + { mul = (fun x y -> mk_mul context y x); + add = mk_add context; + star = mk_star context; + zero = mk_zero context; + one = mk_one context } + in + let vertices = + fold_vertex + (fun v rev_graph -> add_vertex rev_graph v) + graph + (empty reverse_algebra) + in + fold_edges + (fun (u, w, v) rev_graph -> add_edge rev_graph v (f w) u) + graph + vertices + in + (* rg.path_graph, with each edge reversed *) + let reverse_graph = reverse Pathexpr.promote rg.path_graph in + let callset = + M.fold (fun _ call callset -> + CallSet.add call callset) + rg.call_edges + CallSet.empty + in + let entries, exits = + let entries, exits = + CallSet.fold (fun (entry, exit) (entries, exits) -> + (VertexSet.add entry entries, VertexSet.add exit exits)) + callset + (VertexSet.empty, VertexSet.empty) + in + (VertexSet.elements entries, VertexSet.elements exits) + in + (* Intraprocedural paths from entries to target *) + let (_, entry_to_target, _) = + _path_weight reverse_graph omega_trivial tgt + in + let reverse_interproc = + List.fold_left (fun g entry -> + add_edge g tgt (Pathexpr.mk_segment context (entry_to_target entry)) entry) + (reverse (fun x -> x) weight_query.query.interproc) + entries + in + let (_, entry_to_target, _) = + _path_weight reverse_interproc omega_trivial tgt + in + (* Interprocedural paths from entries to target *) + let instrumented_graph = + M.fold (fun (u, _) (entry, _) acc -> + add_edge acc tgt (entry_to_target entry) u) + rg.call_edges + reverse_graph + in + let (_, path_to_target, _) = _path_weight instrumented_graph omega_trivial tgt in + let path_to_exit = msat_path_weight reverse_graph exits in + { parent = weight_query; path_to_exit; path_to_target } + + let path_weight query tgt = let (table, algebra) = prepare query in Pathexpr.eval_nested ~table ~algebra (pathexpr query.query tgt) diff --git a/srk/src/weightedGraph.mli b/srk/src/weightedGraph.mli index 97d7febd..5d172de4 100644 --- a/srk/src/weightedGraph.mli +++ b/srk/src/weightedGraph.mli @@ -29,6 +29,8 @@ type vertex = int (** Create an empty weighted graph over the given algebra of weights. *) val empty : ('a algebra) -> 'a t +val get_algebra : 'a t -> ('a algebra) + (** Add a vertex to a graph. *) val add_vertex : 'a t -> vertex -> 'a t @@ -61,6 +63,7 @@ val cut_graph : 'a t -> vertex list -> 'a t (** Remove a vertex from a graph. *) val remove_vertex : 'a t -> vertex -> 'a t +val remove_edge : 'a t -> vertex -> vertex -> 'a t (** [contract g v] removes vertex [v] from [g] while preserving all weighted paths among remaining vertices. That is, for each pair of edges [p -pw-> @@ -146,6 +149,10 @@ module RecGraph : sig weight queries. *) type 'a weight_query + (** A weight query is an intermediate structure for perfoming + single-destination path weight queries. *) + type 'a reverse_query + exception No_summary of call (** The callgraph of a recursive graph has calls as vertices, and an @@ -192,6 +199,11 @@ module RecGraph : sig weights to call edges. *) val mk_weight_query : query -> 'a Pathexpr.nested_algebra -> 'a weight_query + (** Create a reverse query for the selected destination. The reverse query + shares procedure summaries with the underlying weight query, so + [set_summary] impacts both. *) + val mk_reverse_query : 'a weight_query -> vertex -> 'a reverse_query + (** Build call summaries via successive approximation. *) val summarize_iterative : query -> 'a Pathexpr.nested_algebra -> @@ -206,10 +218,18 @@ module RecGraph : sig (** Find the sum of weights of all intraprocedural paths through a given call. *) val call_weight : 'a weight_query -> call -> 'a - val get_summary : 'a weight_query -> call -> 'a val set_summary : 'a weight_query -> call -> 'a -> unit + (** [exit_summary rq u v] computes the sum of the weights of all + intraprocedural paths beginning at [u] and ending at [v]. The target + vertex [v] is required to be the exit vertex of some procedure. *) + val exit_summary : 'a reverse_query -> vertex -> vertex -> 'a + + (** Find the sum of weights of all interprocedural paths beginning + at the given vertex and ending in the query's target *) + val target_summary : 'a reverse_query -> vertex -> 'a + (** Find the sum of weights of all infinite interprocedural paths beginning at the query's source vertex. *) val omega_path_weight : 'a weight_query -> ('a,'b) Pathexpr.omega_algebra -> 'b diff --git a/srk/test/test_WeightedGraph.ml b/srk/test/test_WeightedGraph.ml index c85d5994..86e8dbc4 100644 --- a/srk/test/test_WeightedGraph.ml +++ b/srk/test/test_WeightedGraph.ml @@ -363,6 +363,15 @@ module PathlenDomain = struct let widen = ISet.inter end +module TrivialPE = struct + type weight = Pathexpr.simple Pathexpr.t + type abstract_weight = Pathexpr.simple Pathexpr.t + let abstract exp = exp + let concretize exp = exp + let equal = Pathexpr.equiv pe_context + let widen = Pathexpr.mk_add pe_context +end + let mk_pathlen_query edges call_edges src = let open WG in let g = @@ -380,6 +389,40 @@ let mk_pathlen_query edges call_edges src = let query = RecGraph.mk_query g src in RecGraph.summarize_iterative query pathlen_algebra (module PathlenDomain) +let rev_query_test edges call_edges src tgt () = + let open WG in + let g = + List.fold_left + (fun g (u,v) -> RecGraph.add_edge g u v) + (RecGraph.empty ()) + edges + in + let g = + List.fold_left + (fun g (u, (s, t), v) -> RecGraph.add_call_edge g u (s, t) v) + g + call_edges + in + let algebra = function + | `Edge (x, y) -> Pathexpr.mk_edge pe_context x y + | `Add (x, y) -> Pathexpr.mk_add pe_context x y + | `Zero -> Pathexpr.mk_zero pe_context + | `One -> Pathexpr.mk_one pe_context + | `Star x -> Pathexpr.mk_star pe_context x + | `Mul (x, y) -> Pathexpr.mk_mul pe_context x y + | `Segment x -> x + in + let query = + RecGraph.summarize_iterative + (RecGraph.mk_query g src) + algebra + (module TrivialPE) + in + let rev_query = RecGraph.mk_reverse_query query tgt in + assert_equal_pathexpr pe_context + (RecGraph.target_summary rev_query src) + (RecGraph.path_weight query tgt) + let get_cyclelen query = WG.RecGraph.omega_path_weight query pathlen_omega_algebra @@ -567,4 +610,48 @@ let suite = "WeightedGraph" >::: [ assert_equal ~cmp:ISet.equal ~printer:ISet.show (ISet.of_list [2]) (get_cyclelen query)) + + ; "rev_query_simple" >:: + (rev_query_test + [(0, 1); (1, 2); (2, 3); (2, 0); (0, 3)] + [] + 0 + 3) + + ; "rev_query_simple2" >:: + (rev_query_test + [(0, 1); (1, 2); (2, 3); (2, 0); (0, 3)] + [] + 0 + 1) + + ; "rev_query_simple3" >:: + (rev_query_test + [ (89, 95); (95, 16); (16, 94); (94, 73) + ; (73, 95); (94, 95); (73, 96) ] + [] + 73 + 96) + + + ; "rev_query_big" >:: + (rev_query_test + [ (53, 10); (10, 56); (10, 52) + ; (56, 17); (17, 55); (55, 21); (21, 56); (21, 38) + ; (38, 47); (47, 57); (47, 43); (43, 52); (43, 52) + ; (38, 34); (34, 52); (34, 57); (52, 54) ] + [] + 53 + 57) + + ; "rev_query_rec" >:: + (rev_query_test + [(0, 1); (2, 3); (0, 3); + (4, 5); (6, 7); (4, 7); (7, 4)] + [(1, (4, 7), 2); + (5, (0, 3), 6); + (8, (0, 3), 9)] + 8 + 1) ] + diff --git a/srk/test/test_transition.ml b/srk/test/test_transition.ml index 2627986c..8949ef75 100644 --- a/srk/test/test_transition.ml +++ b/srk/test/test_transition.ml @@ -27,6 +27,7 @@ module V = struct Some (Hashtbl.find rev_sym_table sym) else None + let is_global _ = true end module T = Transition.Make(Ctx)(V)