diff --git a/.gitignore b/.gitignore index a94b7c16..9e14dc4d 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +*.install *.annot *.cmo *.cma diff --git a/Makefile b/Makefile index d1fef2f4..49e53106 100644 --- a/Makefile +++ b/Makefile @@ -3,13 +3,13 @@ all: build build: - dune build duet + dune build duet 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..199f8bd4 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,10 @@ let make_transition_system rg = TS.empty (RG.bodies rg) in - (ts, !assertions) + (* perform some inlining *) + let inlined_ts, new_assertions = + TS.inline ts main_entry (fun _ -> ()) (!assertions) in + (inlined_ts, new_assertions) let mk_query ts entry = TS.mk_query ts entry @@ -856,7 +994,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 +1231,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 +1290,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..355e89c7 --- /dev/null +++ b/duet/gps.ml @@ -0,0 +1,443 @@ +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) + +(** some global flags for GPS *) +let enable_gas = ref true +let enable_summary = ref true +let enable_refinement = ref true (* main distinction between GPS / GPSLite *) +let enable_inlining = ref true +let enable_acceleration = ref true +let enable_ts_simplify = ref true +let print_stats = ref false + +let num_check_calls = ref 0 +let num_tests_generated = ref 0 + +let num_interpolants_generated = ref 0 + +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 + + +(* 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 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(Graph)(Label)(Transition) + + let generate_test art node = + let post = Ctx.mk_not (K.guard (ReachTree.path_to_error art node)) in + let rec get_path rest node = + match ReachTree.parent_weight art node with + | Some (p, weight) -> get_path (weight::rest) p + | None -> rest + in + let path = get_path [] node in + num_check_calls := !num_check_calls + 1; + match K.interpolate_or_concrete_model ((K.assume @@ ReachTree.get_precondition art) :: path) post with + | `Invalid v_model -> + logf ~level:`trace "-> found test"; + num_tests_generated := !num_tests_generated + 1; + `Test v_model + | `Unknown -> failwith "generate_test: got UNKNOWN as a result for interpolate_or_get_model" + | `Valid interpolants -> + num_interpolants_generated := !num_interpolants_generated + 1; + logf ~level:`trace "-> pruned"; + log_formulas "interpolants - " interpolants; + `Pruned (interpolants) + + let gps 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 art + | Some u -> + (* Fetched tree node u from work list. First attempt to close it. *) + logf ~level:`trace "At frontier node %d:" (ReachTree.of_node u); + if !enable_refinement && (ReachTree.is_covered art u) then + (logf ~level:`trace "-> covered"; + loop ()) + else begin + if !enable_refinement && (ReachTree.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 (interpolants) -> + if !enable_refinement then begin + (* refinement *) + logf ~level:`trace " * refinement: path length %d\n" (List.length (ReachTree.tree_path art u)); + logf ~level:`trace " * interpolants length: %d\n" (List.length interpolants); + ReachTree.refine art (ReachTree.tree_path art u) interpolants; + (* for every node along path of refinement try close *) + List.iter (fun v -> ignore (ReachTree.close art v)) (ReachTree.tree_path art u); + loop () + end else begin (* GPSlite, no refinement *) + loop () + end + | `Test state -> + logf ~level:`trace "-> found test"; + match ReachTree.execute art u state with + | `Safe -> loop () + | `Unsafe n -> `Unsafe (n, art) + end + end + in + loop () +end + + +let analyze_mc 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:(!enable_ts_simplify) ~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 "GPS: procedure call") + ; target_summary = (Summarizer.path_weight_inter summ) } + in + let art = + begin match GPS.gps graph entry err_loc with + | `Safe art -> Printf.printf " proven safe\n"; art + | `Unsafe (_, art) -> Printf.printf " proven unsafe\n"; art + end in + if !print_stats then begin + let statistics = GPS.ReachTree.get_statistics art in + Printf.printf " Statistics\n"; + Printf.printf " Number of check calls: %d\n" !num_check_calls; + Printf.printf " Number of tests generated: %d\n" !num_tests_generated; + Printf.printf " Number of dead-end-interpolants generated: %d\n" !num_interpolants_generated; + Printf.printf " Number of refinements performed: %d\n" statistics.num_refinements_performed; + Printf.printf " Number of coverings added: %d\n" statistics.num_covers_added; + Printf.printf " Number of coverings removed: %d\n" statistics.num_covers_removed + 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; + logf "testing reachability of location %d\n" err_loc ; + logf "------------------------------\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 GPS.generate_test art u with + | `Pruned interpolants -> + ART.refine art (ART.tree_path art u) interpolants; + 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_config + ("-gps-disable-gas", Arg.Clear enable_gas, " Disable gas-instrumentation in GPS (enabled by default)"); + CmdLine.register_config + ("-gps-disable-summary", Arg.Clear enable_summary, " Disable CRA-generated summaries in GPS (enabled by default)"); + CmdLine.register_config + ("-gps-disable-acceleration", Arg.Clear enable_acceleration, " Disable loop acceleration during preprocessing (enabled by default)"); + CmdLine.register_config + ("-gps-disable-simplify", Arg.Clear enable_ts_simplify, " Disable CFG simplification (enabled by default)"); + CmdLine.register_config + ("-gps-disable-refinement", Arg.Clear enable_refinement, " Disable invariant synthesis capabilities of GPS"); + CmdLine.register_config + ("-gps-stats", Arg.Unit (fun () -> print_stats := true), " Enable statistics reporting of a GPS run (disabled by default)"); + CmdLine.register_pass + ("-gps", analyze_mc, " GPS model checker for intraprocedural programs"); + 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..192fa29e --- /dev/null +++ b/duet/reachTree.ml @@ -0,0 +1,583 @@ +(** 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 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 stats = { + mutable num_covers_added : int; + mutable num_covers_removed : int; + mutable num_refinements_performed : int; + } + + 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; + + statistics : stats; + } + + 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 + ; statistics = { + num_covers_added = 0 + ; num_covers_removed = 0 + ; num_refinements_performed = 0 }} + + 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.statistics.num_covers_added <- art.statistics.num_covers_added + 1; + 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; + art.statistics.num_covers_removed <- art.statistics.num_covers_removed + 1) + 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 = + art.statistics.num_refinements_performed <- art.statistics.num_refinements_performed + 1; + 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.statistics.num_covers_removed <- art.statistics.num_covers_removed + 1; + 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 get_statistics art = art.statistics +end diff --git a/duet/reachTree.mli b/duet/reachTree.mli new file mode 100644 index 00000000..0fe5ca03 --- /dev/null +++ b/duet/reachTree.mli @@ -0,0 +1,76 @@ +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 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 + type stats = { + mutable num_covers_added : int; + mutable num_covers_removed : int; + mutable num_refinements_performed : int; + } + 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 path_to_error : t -> node -> weight + val get_statistics : t -> stats +end 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..58230969 100644 --- a/srk/src/dune +++ b/srk/src/dune @@ -12,6 +12,8 @@ (public_name srk) (modules (:standard \ bigtop)) (modes native) + (flags (:standard -w -32)) + (modules_without_implementation interpolant) (libraries batteries ppx_deriving ppx_deriving.show ppx_deriving.ord ppx_deriving.eq diff --git a/srk/src/interpolant.mli b/srk/src/interpolant.mli new file mode 100644 index 00000000..81229854 --- /dev/null +++ b/srk/src/interpolant.mli @@ -0,0 +1,70 @@ +(** Interpolation of transition formulas. *) +open Syntax + +module type Interpolant = functor + (C: sig + type t + val context : t context + end) + (V: sig + type t + val show : t -> string + val typ : t -> [ `TyInt | `TyReal ] + val compare : t -> t -> int + val symbol_of : t -> symbol + val of_symbol : symbol -> t option + val is_global : t -> bool + end) + (T: sig + type t + type var = V.t + val equal : t -> t -> bool + val compare : t -> t -> int + + (** Guarded parallel assignment *) + val construct : C.t formula -> (var * C.t arith_term) list -> t + + val create : C.t formula -> (var * C.t arith_term) BatEnum.t -> t + (** [exists ex tr] removes the variables that do not satisfy the predicate + [ex] from the footprint of a transition. For example, projecting a + variable [x] out of a transition [tr] is logically equivalent to + [(exists x. tr) && x' = x]. *) + val exists : (var -> bool) -> t -> t + + (** (Needed by interpolation) *) + val destruct_and : (C.t context) -> (C.t formula) -> (C.t formula) list + + (** Enumerate the variables and values assigned in a transition. *) + val transform : t -> (var * C.t arith_term) BatEnum.t + + (** Variables written to inside the transform of a transition. *) + val defines : t -> var list + + (** Variables used by a a transition, including non-Skolem symbols in both the guard and the transform. *) + val uses : t -> var list + + (** The condition under which a transition may be executed. *) + val guard : t -> C.t formula + + val state_vocabulary : t -> (var * Syntax.symbol) list + + end) -> sig + + + (** Given a path (list of transitions [tr_1 ... tr_n]) and a post-condition + formula, determine whether the path implies the post-condition. If yes, + return a sequence of intermediate assertions [phi_1 ... phi_n] that + 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.t list -> C.t formula -> [ `Valid of C.t formula list + | `Invalid + | `Unknown ] + + + (** Same as interpolate, but returns a concrete model if interpllation fails. *) + val interpolate_or_concrete_model : T.t list -> C.t formula + -> [`Valid of C.t formula list + | `Invalid of C.t Interpretation.interpretation + | `Unknown ] +end 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/newtonInterpolant.ml b/srk/src/newtonInterpolant.ml new file mode 100644 index 00000000..e4c71d14 --- /dev/null +++ b/srk/src/newtonInterpolant.ml @@ -0,0 +1,457 @@ +open Syntax +open BatPervasives +open Interpolant + +include Log.Make(struct let name = "srk.newtonInterpolant" end) + +module NewtonBackwards : Interpolant = functor (C: sig + type t + val context : t context + end) + (V: sig + type t + val show : t -> string + val typ : t -> [ `TyInt | `TyReal ] + val compare : t -> t -> int + val symbol_of : t -> symbol + val of_symbol : symbol -> t option + val is_global : t -> bool + end) + (T: sig + type t + type var = V.t + val equal : t -> t -> bool + val compare : t -> t -> int + + (** Guarded parallel assignment *) + val construct : C.t formula -> (var * C.t arith_term) list -> t + + val create : C.t formula -> (var * C.t arith_term) BatEnum.t -> t + (** [exists ex tr] removes the variables that do not satisfy the predicate + [ex] from the footprint of a transition. For example, projecting a + variable [x] out of a transition [tr] is logically equivalent to + [(exists x. tr) && x' = x]. *) + val exists : (var -> bool) -> t -> t + + (** (Needed by interpolation) *) + val destruct_and : (C.t context) -> (C.t formula) -> (C.t formula) list + + (** Enumerate the variables and values assigned in a transition. *) + val transform : t -> (var * C.t arith_term) BatEnum.t + + val defines : t -> var list + + (** Variables used by a a transition, including non-Skolem symbols in both the guard and the transform. *) + val uses : t -> var list + + (** The condition under which a transition may be executed. *) + val guard : t -> C.t formula + + val state_vocabulary : t -> (var * Syntax.symbol) list + end) -> struct + + let srk = C.context + module M = BatMap.Make(V) + + (* The helper functions below implement the live-variables analysis described in: + + Daniel Dietsch, Matthias Heizmann, Betim Musa, Alexander Nutz, and Andreas Podelski. + Craig vs. Newton in software model checking. ESEC/FSE 2017. + + For a sequence of transition formulas [trs]: + + Def 1 (future-live variable). We call a variable [x] future-live in [trs] at position i if there is + a transition tr_j in [trs] with j > i, such that + - tr_j reads x, and + - for all k with i < k < j the transition tr_k neither writes nor havocs [x]. + + Def 2 (past-live variable).We call a variable [x] past-live in [trs] at i if there is a transition tr_j in [trs] with + j <= i, such that + - tr_j writes x or reads x, and + - for all k with j < k <= i the transition tr_k does not havoc x. + *) + + (** test whether a variable [x] of type [var] is future-live in future transitions [trs]. *) + + let is_future_live x trs = + if trs = [] then false else begin + (* In srk, havocs are writes, so suffices to detect writes only. + Logic: Scan the transitions from right-to-left, + - if tr_j reads x, then switch to verify that all transitions left of tr_j does not write to x. + - if some tr_k writes to x, then we need to re-find some j + if has_been_read then begin + if has_been_written then begin + if List.mem x (T.uses tr) && (not (List.mem x (T.defines tr))) then (has_been_read, false) + else (has_been_read, has_been_written) + end else (has_been_read, List.mem x (T.defines tr)) + end else begin + (List.mem x (T.uses tr) && not(List.mem x (T.defines tr)), false) + end + ) (false, false) (List.rev trs) in + match state with + (* a variable is future-live if it's used in the future and not modified between current point and point-of-use. *) + | (true, false) -> true + | _ -> false + end + + (** For a list of transitions [trs], compute the set of future-live variables for each transition's vocabulary. + Returns a list of type [var Set.t] where the i-th set is the set of non-live variables at transition i. *) + let future_live_analysis trs = + let live_vars, _ = + List.fold_left (fun (acc, trs') tr -> + let vars = List.map (fun (x, _) -> x) (T.state_vocabulary tr) in + (List.filter (fun x -> is_future_live x trs') vars :: acc, tr :: trs') + ) ([], []) (List.rev trs) in + live_vars + + (** figure out set of variables with non-deterministic right-hand-side expressions in [tr]. *) + let havoc_vars tr = + let transform = T.transform tr in + BatEnum.fold (fun curr (v, term) -> + if (Syntax.symbols term + |> Symbol.Set.filter (fun x -> V.of_symbol x = None) (* every skolem symbol is non-deterministic. *) + |> Symbol.Set.cardinal) > 0 then + curr (* variable v is deterministically assigned *) + else + v :: curr (* variable v is assigned a non-det expression *) + ) [] transform + + + (** test whether a variable [x] is past-live w.r.t. past transitions [trs]. *) + let is_past_live x trs = + let used x tr = List.mem x (T.uses tr) || List.mem x (T.defines tr) in + let havoced x tr = List.mem x (havoc_vars tr) in + if trs = [] then false else begin + (* A simpler definition of past-variable is if a variable x is + (1) used and (2) never havoc'ed beyond some point j in [trs]. + *) + let state = List.fold_left (fun (been_used, been_havoced) tr -> + if been_used then begin + if been_havoced then begin + if (used x tr) && not(havoced x tr) then (been_used, false) + else (been_used, been_havoced) + end else + (been_used, havoced x tr) + end else begin + (used x tr, false) + end + ) (false, false) trs in + match state with + | (true, false) -> true + | _ -> false + end + + let past_live_analysis trs = + let live_vars, _ = + List.fold_left (fun (acc, trs') tr -> + let vars = List.map (fun (x, _) -> x) (T.state_vocabulary tr) in + (List.filter (fun x -> is_past_live x trs') vars :: acc, tr :: trs') + ) ([], []) trs in + live_vars + + let interpolate trs post = + (* The following step ensures all Skolem constants in [trs] are unique. *) + let trs = + trs |> List.map (fun tr -> + let fresh_skolem = + (* If sym is a non-skolem (i.e. stored in V), return the same symbol. Otherwise, create a fresh Skolem symbol. *) + Memo.memo (fun sym -> + match V.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 + let transform = M.map (substitute_const srk fresh_skolem) (M.of_enum @@ T.transform tr) in + let guard = substitute_const srk fresh_skolem (T.guard tr) in + T.create guard @@ M.enum transform) + in + (* Take the list of guards for each transition in the sequence. + Break guards into a list of conjunctions, and associate each conjunct with + an indicator variable that is true iff the conjunct is included in the final UNSAT core. *) + let guards = + List.map (fun tr -> + List.map + (fun phi -> (mk_symbol srk `TyBool, phi)) + (T.destruct_and srk (T.guard tr))) + trs + in + let indicators = + List.concat_map (List.map (fun (s, _) -> mk_const srk s)) guards + in + let subscript_tbl = 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 = V.symbol_of var in + let var_ss_sym = mk_symbol srk (V.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_term)::ss, + mk_eq srk var_ss_term term_ss::phis)) + (M.of_enum (T.transform tr)) + ([], ss_guards) + in + List.iter (fun (k, v) -> Hashtbl.add subscript_tbl k v) ss; + mk_and srk phis + in + let module Solver = Smt.StdSolver in + let solver = Solver.make srk in + List.iter2 (fun tr guard -> + Solver.add solver [to_ss_formula tr guard]) + trs + guards; + Solver.add solver [substitute_const srk subscript (mk_not srk post)]; + match Solver.get_unsat_core solver indicators with + | `Sat -> `Invalid + | `Unknown -> `Unknown + | `Unsat 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 V.of_symbol sym with + | Some var -> + if M.mem var (M.of_enum (T.transform tr)) then + M.find var (M.of_enum (T.transform tr)) + 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 -> V.of_symbol s != None) + |> mk_not srk + in + (wp::itp, wp)) + trs + guards + ([ + mk_not srk post + |> Quantifier.mbp srk (fun x -> V.of_symbol x <> None) + |> mk_not srk + ], post) + in + `Valid (List.tl itp) + + + (* 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 V.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 + let transform = M.map (substitute_const srk fresh_skolem) (M.of_enum @@ T.transform tr) in + let guard = substitute_const srk fresh_skolem (T.guard tr) in + T.create guard (M.enum transform) + + 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 V.of_symbol sym with + | Some var -> + if M.mem var (M.of_enum @@ T.transform tr) then + M.find var (M.of_enum @@ T.transform tr) + 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 -> V.of_symbol s != None) + |> mk_not srk + in + (wp::itp, wp)) + trs + guards + ([ + mk_not srk post + |> Quantifier.mbp srk (fun x -> V.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)) + (T.destruct_and srk @@ T.guard tr)) + 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 = V.symbol_of var in + let var_ss_sym = mk_symbol srk (V.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)) + (M.of_enum @@ T.transform tr) + ([], 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 V.of_symbol s with + | Some _ -> true + | None -> false)) + in interpolate_query trs post sat_model @@ interpolate_unsat_core + + + + end 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..fcfe10da 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 @@ -63,6 +65,12 @@ struct List.fold_left (fun m (v, term) -> M.add v term m) M.empty assignment; guard = guard } + let create guard transform_e = + { + transform = M.of_enum transform_e; + guard = guard + } + let assign v term = { transform = M.add v term M.empty; guard = mk_true srk } @@ -113,40 +121,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. *) @@ -328,6 +343,9 @@ struct let mem_transform x tr = M.mem x tr.transform let get_transform x tr = M.find x tr.transform let transform tr = M.enum tr.transform + + let transform_map tr = tr.transform + let guard tr = tr.guard let rec destruct_and srk phi = @@ -438,10 +456,466 @@ 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 state_vocabulary tr = + let global_v, local_v = vocabulary tr in + List.filter_map (fun x -> + match Var.of_symbol x with + | Some var -> Some(var, x) + | None -> None + ) (global_v @ local_v) + + 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 +966,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 +1003,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..9e9b9e5b 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 @@ -47,6 +48,7 @@ module Make (** Guarded parallel assignment *) val construct : C.t formula -> (var * C.t arith_term) list -> t + val create : C.t formula -> (var * C.t arith_term) BatEnum.t -> t (** [assume phi] is a transition that doesn't modify any variables, but can only be executed when [phi] holds *) @@ -70,6 +72,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 @@ -101,6 +106,9 @@ module Make (** Enumerate the variables and values assigned in a transition. *) val transform : t -> (var * C.t arith_term) BatEnum.t + (** Destruct conjunctions, needed by the interpolation API *) + val destruct_and : (C.t context) -> (C.t formula) -> (C.t formula) list + (** The condition under which a transition may be executed. *) val guard : t -> C.t formula @@ -110,9 +118,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,7 +151,13 @@ module Make | `Invalid | `Unknown ] + val contains_havoc : t -> bool + + + (** Variables written to inside the transform of a transition. *) val defines : t -> var list + + (** Variables used by a a transition, including non-Skolem symbols in both the guard and the transform. *) val uses : t -> var list val abstract_post : (C.t,'abs) SrkApron.property -> t -> (C.t,'abs) SrkApron.property @@ -131,4 +168,22 @@ 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)) + + (** non-existentially quantified vocabulary of a transition formula, with all skolem symbols left out. + returns a list of pairs [var, sym] with a Var.t and a symbol corresponding to the variable. *) + val state_vocabulary: t -> (var * Syntax.symbol) list end diff --git a/srk/src/transitionSystem.ml b/srk/src/transitionSystem.ml index 63c434fc..e2968b35 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,158 @@ 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) = + 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) -> + 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 acc + | (_, _) -> 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) = + 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 -> + 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 -> + let tg' = (PS.fold aux sinks tg) in + tg' + |> do_inline ( + if depth > 0 then depth - 1 else depth) + | _ -> (); 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_newton_interpolant.ml b/srk/test/test_newton_interpolant.ml new file mode 100644 index 00000000..518e83b5 --- /dev/null +++ b/srk/test/test_newton_interpolant.ml @@ -0,0 +1,150 @@ +open Srk +open OUnit +open Syntax +open Test_pervasives +open NewtonInterpolant +module V = struct + type t = string + + let typ_table = Hashtbl.create 991 + let sym_table = Hashtbl.create 991 + let rev_sym_table = Hashtbl.create 991 + + let register_var name typ = + assert (not (Hashtbl.mem typ_table name)); + let sym = Ctx.mk_symbol ~name (typ :> typ) in + Hashtbl.add typ_table name typ; + Hashtbl.add sym_table name sym; + Hashtbl.add rev_sym_table sym name + + let pp = Format.pp_print_string + let show x = x + let typ = Hashtbl.find typ_table + let compare = Stdlib.compare + let symbol_of = Hashtbl.find sym_table + let of_symbol sym = + if Hashtbl.mem rev_sym_table sym then + Some (Hashtbl.find rev_sym_table sym) + else + None + let is_global _ = true +end +module T = Transition.Make(Ctx)(V) +module NITP = NewtonBackwards(Ctx)(V)(T) + +let () = + T.domain := Iteration.split (!T.domain) + +let () = + V.register_var "i" `TyInt; + V.register_var "j" `TyInt; + V.register_var "k" `TyInt; + V.register_var "n" `TyInt; + V.register_var "x" `TyInt; + V.register_var "y" `TyInt; + V.register_var "z" `TyInt + +let x = Ctx.mk_const (V.symbol_of "x") +let y = Ctx.mk_const (V.symbol_of "y") +let z = Ctx.mk_const (V.symbol_of "z") +let i = Ctx.mk_const (V.symbol_of "i") +let j = Ctx.mk_const (V.symbol_of "j") +let k = Ctx.mk_const (V.symbol_of "k") +let n = Ctx.mk_const (V.symbol_of "n") + +let assert_post tr phi = + let not_post = + rewrite srk ~down:(pos_rewriter srk) (Ctx.mk_not phi) + in + let pathcond = + T.guard (T.mul tr (T.assume not_post)) + in + if Wedge.is_sat srk pathcond != `Unsat then + assert_failure (Printf.sprintf "%s\n is not a post-condition of\n%s" + (Formula.show srk phi) + (T.show tr)) + +let assert_equal_tr = assert_equal ~cmp:T.equal ~printer:T.show + +let mk_block = BatList.reduce T.mul + +let mk_if cond bthen belse = + T.add + (mk_block ((T.assume cond)::bthen)) + (mk_block ((T.assume (Ctx.mk_not cond))::belse)) + +let mk_while cond body = + T.mul + (T.star (mk_block ((T.assume cond)::body))) + (T.assume (Ctx.mk_not cond)) + +let assert_valid pre tr post = + if (T.valid_triple pre [tr] post) != `Valid then + assert_failure (Printf.sprintf "Invalid Hoare triple: {%s} %s {%s}" + (Formula.show srk pre) + (T.show tr) + (Formula.show srk post)) + + +let check_interpolant path itp = + let rec go path itp = + match path, itp with + | tr::path, pre::post::itp -> + assert_valid pre tr post; + go path (post::itp) + | [], [_] -> () + | _, _ -> assert false + in + go path (Ctx.mk_true::itp) + +let interpolate1 () = + let path = + let open Infix in + [T.assign "x" (int 0); + T.assign "y" (int 0); + T.assume (x < (int 10)); + T.assign "x" (x + (int 1)); + T.assign "y" (y + (int 1)); + T.assume ((int 10) <= x); + T.assume ((int 10) < x || x < (int 10))] + in + let post = Ctx.mk_false in + match NITP.interpolate path post with + | `Valid itp -> + check_interpolant path itp + | _ -> assert_failure "Invalid post-condition" + +let interpolate2 () = + let path = + let open Infix in + [T.assume (x < (int 10)); + T.assign "x" (x + (int 1)); + T.assign "y" (y + (int 1)); + T.assume ((int 10) <= x); + T.assume ((int 10) < x || x < (int 10))] + in + let post = Ctx.mk_false in + match NITP.interpolate path post with + | `Valid itp -> + check_interpolant path itp + | _ -> assert_failure "Invalid post-condition" + +let interpolate_havoc () = + let path = + let open Infix in + [T.assign "x" (int 0); + T.assign "y" v; (* havoc *) + T.assume (x <= y); + T.assume (y < (int 0))] + in + let post = Ctx.mk_false in + match NITP.interpolate path post with + | `Valid itp -> + check_interpolant path itp + | _ -> assert_failure "Invalid post-condition" + +let suite = "Newton_interpolant" >::: [ + "interpolate1" >:: interpolate1; + "interpolate2" >:: interpolate2; + "interpolate_havoc" >:: interpolate_havoc; + ] diff --git a/srk/test/test_srk.ml b/srk/test/test_srk.ml index 71daec76..219953f0 100644 --- a/srk/test/test_srk.ml +++ b/srk/test/test_srk.ml @@ -26,6 +26,7 @@ let suite = "Main" >::: [ Test_iteration.suite; Test_termination.suite; Test_transition.suite; + Test_newton_interpolant.suite; Test_WeightedGraph.suite; Test_chc.suite; Test_numberField.suite; diff --git a/srk/test/test_transition.ml b/srk/test/test_transition.ml index 2627986c..28991b0a 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) @@ -254,70 +255,6 @@ let equal1 () = in assert_equal_tr tr1 tr2 -let assert_valid pre tr post = - if (T.valid_triple pre [tr] post) != `Valid then - assert_failure (Printf.sprintf "Invalid Hoare triple: {%s} %s {%s}" - (Formula.show srk pre) - (T.show tr) - (Formula.show srk post)) - -let check_interpolant path itp = - let rec go path itp = - match path, itp with - | tr::path, pre::post::itp -> - assert_valid pre tr post; - go path (post::itp) - | [], [_] -> () - | _, _ -> assert false - in - go path (Ctx.mk_true::itp) - -let interpolate1 () = - let path = - let open Infix in - [T.assign "x" (int 0); - T.assign "y" (int 0); - T.assume (x < (int 10)); - T.assign "x" (x + (int 1)); - T.assign "y" (y + (int 1)); - T.assume ((int 10) <= x); - T.assume ((int 10) < x || x < (int 10))] - in - let post = Ctx.mk_false in - match T.interpolate path post with - | `Valid itp -> - check_interpolant path itp - | _ -> assert_failure "Invalid post-condition" - -let interpolate2 () = - let path = - let open Infix in - [T.assume (x < (int 10)); - T.assign "x" (x + (int 1)); - T.assign "y" (y + (int 1)); - T.assume ((int 10) <= x); - T.assume ((int 10) < x || x < (int 10))] - in - let post = Ctx.mk_false in - match T.interpolate path post with - | `Valid itp -> - check_interpolant path itp - | _ -> assert_failure "Invalid post-condition" - -let interpolate_havoc () = - let path = - let open Infix in - [T.assign "x" (int 0); - T.assign "y" v; (* havoc *) - T.assume (x <= y); - T.assume (y < (int 0))] - in - let post = Ctx.mk_false in - match T.interpolate path post with - | `Valid itp -> - check_interpolant path itp - | _ -> assert_failure "Invalid post-condition" - let negative_eigenvalue () = let tr = let open Infix in @@ -346,8 +283,5 @@ let suite = "Transition" >::: [ "split" >:: split; "split2" >:: split2; "equal1" >:: equal1; - "interpolate1" >:: interpolate1; - "interpolate2" >:: interpolate2; - "interpolate_havoc" >:: interpolate_havoc; "negative_eigenvalue" >:: negative_eigenvalue; ]