Skip to content

Incremental: (Cheap!) Full Reachability to Prune #713

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 19 commits into from
May 3, 2022
Merged

Incremental: (Cheap!) Full Reachability to Prune #713

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
a33457a
Add example where incremental postsolver does not remove warnings
michael-schwarz Apr 28, 2022
bda1100
Steps towards cheap full reachability
michael-schwarz Apr 30, 2022
080d474
Add fundamental problem where multi-threaded code becomes dead
michael-schwarz Apr 30, 2022
5d8d36d
Newline for dep log
michael-schwarz May 1, 2022
b9252dc
dep: Relift VS too
michael-schwarz May 1, 2022
ee55218
Simplify
michael-schwarz May 2, 2022
c1933db
Undo unneeded modifications
michael-schwarz May 2, 2022
5850d93
minimize diff
michael-schwarz May 2, 2022
83ec1a1
Move incr_verify specific changes back
michael-schwarz May 2, 2022
ddda093
Cleanup
michael-schwarz May 2, 2022
f45f194
Cleanup
michael-schwarz May 2, 2022
9940dea
Add incremental test where race in removed call remains
sim642 Mar 18, 2022
da4564d
Record less in `dep`, do not clear `side_infl` and `side_dep`
michael-schwarz May 2, 2022
8b7d4d3
Print same solver stats consistently
michael-schwarz May 2, 2022
50fed60
Typo
michael-schwarz May 2, 2022
56d230f
Merge branch 'interactive' into interactive_postsolver_pruning
michael-schwarz May 3, 2022
d622611
Comment about resetting side_infl
michael-schwarz May 3, 2022
3f96c77
Rename incremental.verify -> incremental.postsolver.enabled
michael-schwarz May 3, 2022
44f1efa
Add option `incremental.postsolver.superstable-reached`
michael-schwarz May 3, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/framework/constraints.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -797,13 +797,14 @@ module EqIncrSolverFromEqSolver (Sol: GenericEqBoxSolver): GenericEqBoxIncrSolve
functor (Arg: IncrSolverArg) (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) ->
struct
module Sol = Sol (S) (VH)
module Post = PostSolver.MakeList (PostSolver.ListArgFromStdArg (S) (VH) (Arg))
module VS = BatSet.Make(S.Var)
module Post = PostSolver.MakeList (PostSolver.ListArgFromStdArg (S) (VH) (VS) (Arg))

type marshal = unit

let solve box xs vs =
let vh = Sol.solve box xs vs in
Post.post xs vs vh;
Post.post xs vs vh None;
(vh, ())
end

Expand Down
72 changes: 48 additions & 24 deletions src/solvers/postSolver.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ module type S =
sig
module S: EqConstrSys
module VH: Hashtbl.S with type key = S.v
module VS: BatSet.S with type elt = S.v

val init: unit -> unit
val one_side: vh:S.Dom.t VH.t -> x:S.v -> y:S.v -> d:S.Dom.t -> unit
Expand All @@ -16,26 +17,28 @@ end

(** Functorial postsolver for any system. *)
module type F =
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) ->
S with module S = S and module VH = VH
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) (VS: BatSet.S with type elt = S.v) ->
S with module S = S and module VH = VH and module VS = VS

(** Base implementation for postsolver. *)
module Unit: F =
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) ->
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) (VS: BatSet.S with type elt = S.v) ->
struct
module S = S
module VH = VH
module VS = VS
let init () = ()
let one_side ~vh ~x ~y ~d = ()
let one_constraint ~vh ~x ~rhs = ()
let finalize ~vh ~reachable = ()
end

(** Sequential composition of two postsolvers. *)
module Compose (PS1: S) (PS2: S with module S = PS1.S and module VH = PS1.VH): S with module S = PS1.S and module VH = PS1.VH =
module Compose (PS1: S) (PS2: S with module S = PS1.S and module VH = PS1.VH and module VS = PS1.VS): S with module S = PS1.S and module VH = PS1.VH and module VS = PS1.VS =
struct
module S = PS1.S
module VH = PS1.VH
module VS = PS1.VS

let init () =
PS1.init ();
Expand All @@ -53,9 +56,9 @@ end

(** Postsolver for pruning solution using reachability. *)
module Prune: F =
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) ->
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) (VS: BatSet.S with type elt = S.v) ->
struct
include Unit (S) (VH)
include Unit (S) (VH) (VS)

let finalize ~vh ~reachable =
if get_bool "dbg.debug" then
Expand All @@ -68,9 +71,9 @@ module Prune: F =

(** Postsolver for verifying solution in demand-driven fashion. *)
module Verify: F =
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) ->
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) (VS: BatSet.S with type elt = S.v) ->
struct
include Unit (S) (VH)
include Unit (S) (VH) (VS)

let init () =
Goblintutil.verified := Some true
Expand Down Expand Up @@ -98,9 +101,9 @@ module Verify: F =

(** Postsolver for enabling messages (warnings) output. *)
module Warn: F =
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) ->
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) (VS: BatSet.S with type elt = S.v) ->
struct
include Unit (S) (VH)
include Unit (S) (VH) (VS)

let old_should_warn = ref None

Expand All @@ -114,9 +117,9 @@ module Warn: F =

(** Postsolver for save_run option. *)
module SaveRun: F =
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) ->
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) (VS: BatSet.S with type elt = S.v) ->
struct
include Unit (S) (VH)
include Unit (S) (VH) (VS)

let finalize ~vh ~reachable =
(* copied from Control.solve_and_postprocess *)
Expand Down Expand Up @@ -172,9 +175,10 @@ end
module MakeIncr (PS: IncrS) =
struct
module S = PS.S
module VS = PS.VS
module VH = PS.VH

let post xs vs vh =
let post xs vs vh dep =
if get_bool "dbg.verbose" then
print_endline "Postsolving\n";

Expand Down Expand Up @@ -211,13 +215,30 @@ struct
if M.tracing then M.trace "postsolver" "one_constraint %a %a\n" S.Var.pretty_trace x S.Dom.pretty rhs;
PS.one_constraint ~vh ~x ~rhs
in
List.iter one_var vs;

PS.finalize ~vh ~reachable;
(Stats.time "potentially_incremental_reach" (List.iter one_var)) vs;

match dep with
| None -> PS.finalize ~vh ~reachable:reachable;
| Some dep -> (
(* Perform reachability on whole constraint system, but cheaply by using logged dependencies *)
(* This only works if the other reachability has been performed before, so dependencies created only during postsolve are recorded *)
let reachable' = VH.create (VH.length vh) in
let rec one_var' x =
if not (VH.mem reachable' x) then (
VH.replace reachable' x ();
match VH.find_option dep x with
| Some vs -> VS.iter one_var' vs
| None -> ()
)
in
(Stats.time "cheap_full_reach" (List.iter one_var')) vs;
PS.finalize ~vh ~reachable:reachable';
)
;
Goblintutil.postsolving := false

let post xs vs vh =
Stats.time "postsolver" (post xs vs) vh
let post xs vs vh dep =
Stats.time "postsolver" (post xs vs vh) dep
end

(** List of postsolvers. *)
Expand All @@ -226,8 +247,9 @@ sig
(* Specify S and VH here to constrain all postsolvers to use the same. *)
module S: EqConstrSys
module VH: Hashtbl.S with type key = S.v
module VS: BatSet.S with type elt = S.v
(* Auxiliary module type because first-class module types cannot contain module constraints. *)
module type M = S with module S = S and module VH = VH
module type M = S with module S = S and module VH = VH and module VS = VS

val postsolvers: (module M) list
end
Expand All @@ -246,6 +268,7 @@ module MakeIncrList (Arg: MakeIncrListArg) =
struct
module S = Arg.S
module VH = Arg.VH
module VS = Arg.VS

let postsolver_opt: (module Arg.M) option =
match Arg.postsolvers with
Expand All @@ -256,7 +279,7 @@ struct
in
Some (List.reduce compose postsolvers)

let post xs vs vh =
let post xs vs vh dep =
match postsolver_opt with
| None -> ()
| Some (module PS) ->
Expand All @@ -267,7 +290,7 @@ struct
end
in
let module M = MakeIncr (IncrPS) in
M.post xs vs vh
M.post xs vs vh dep
end

(** Make complete (non-incremental) postsolving function from list of postsolvers.
Expand All @@ -292,13 +315,14 @@ sig
end

(** List of standard postsolvers. *)
module ListArgFromStdArg (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) (Arg: MakeStdArg): MakeListArg with module S = S and module VH = VH =
module ListArgFromStdArg (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) (VS: BatSet.S with type elt = S.v) (Arg: MakeStdArg): MakeListArg with module S = S and module VH = VH and module VS = VS =
struct
open Arg

module S = S
module VH = VH
module type M = S with module S = S and module VH = VH
module VS = VS
module type M = S with module S = S and module VH = VH and module VS = VS

let postsolvers: (bool * (module F)) list = [
(should_prune, (module Prune));
Expand All @@ -311,5 +335,5 @@ struct
postsolvers
|> List.filter fst
|> List.map snd
|> List.map (fun (module F: F) -> (module F (S) (VH): M))
|> List.map (fun (module F: F) -> (module F (S) (VH) (VS): M))
end
Loading