diff --git a/dune-project b/dune-project index aabe7b4243..abbd133ec0 100644 --- a/dune-project +++ b/dune-project @@ -39,6 +39,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e (ocaml (>= 4.14)) (goblint-cil (>= 2.0.9)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint. (batteries (>= 3.9.0)) + ocamlgraph (zarith (>= 1.12)) (yojson (and (>= 2.0.0) (< 3))) ; json-data-encoding has incompatible yojson representation for yojson 3 (qcheck-core (>= 0.19)) diff --git a/goblint.opam b/goblint.opam index 9d899df327..aa3189128c 100644 --- a/goblint.opam +++ b/goblint.opam @@ -41,6 +41,7 @@ depends: [ "ocaml" {>= "4.14"} "goblint-cil" {>= "2.0.9"} "batteries" {>= "3.9.0"} + "ocamlgraph" "zarith" {>= "1.12"} "yojson" {>= "2.0.0" & < "3"} "qcheck-core" {>= "0.19"} diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index f9aed59f2c..cc2fc2ad50 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -391,6 +391,9 @@ struct (Pretty.dprintf "total memory locations: %d" total, None); ]; ) + else + (); + () end let _ = diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 134ce7eb95..c222cee536 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -2456,6 +2456,13 @@ "type": "integer", "default": 0 }, + "race-coloring": { + "title": "warn.race-coloring", + "description": "Group race warnings by graph coloring (none, greedy, dsatur, rlf, optimal).", + "type": "string", + "enum": ["none", "greedy", "dsatur", "rlf", "optimal"], + "default": "none" + }, "deterministic": { "title": "warn.deterministic", "description": "Output messages in deterministic order. Useful for cram testing.", diff --git a/src/domains/access.ml b/src/domains/access.ml index bc24cf2d31..d0276629e7 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -152,7 +152,8 @@ let init (f:file) = let reset () = TSH.clear typeVar; - TSH.clear typeIncl + TSH.clear typeIncl; + () type acc_typ = [ `Type of CilType.Typ.t | `Struct of CilType.Compinfo.t * Offset.Unit.t ] [@@deriving eq, ord, hash] (** Old access type inferred from an expression. *) @@ -484,6 +485,55 @@ struct AS.pretty w.node AS.pretty w.prefix AS.pretty w.type_suffix AS.pretty w.type_suffix_prefix end +module InterferenceGraph = struct + module Vertex = struct + type t = A.t + + let compare = A.compare + let hash = A.hash + let equal = A.equal + end + + module G = Graph.Imperative.Graph.Concrete (Vertex) + + type t = G.t + + let of_warn_accs (warn_accs : WarnAccs.t) = + let graph = G.create () in + let all = WarnAccs.union_all warn_accs in + AS.iter (fun acc -> G.add_vertex graph acc) all; + let accs = AS.elements all in + let rec loop = function + | [] -> () + | a :: rest -> + List.iter (fun b -> + if may_race a b then + G.add_edge graph a b + ) rest; + loop rest + in + loop accs; + graph + + module Coloring = AccessColoring.Make (G) + + let of_accesses (accs : AS.t) = + let graph = G.create () in + AS.iter (fun acc -> G.add_vertex graph acc) accs; + let accs_list = AS.elements accs in + let rec loop = function + | [] -> () + | a :: rest -> + List.iter (fun b -> + if may_race a b then + G.add_edge graph a b + ) rest; + loop rest + in + loop accs_list; + graph +end + let group_may_race (warn_accs:WarnAccs.t) = if M.tracing then M.tracei "access" "group_may_race %a" WarnAccs.pretty warn_accs; (* BFS to traverse one component with may_race edges *) @@ -594,16 +644,54 @@ let incr_summary ~safe ~vulnerable ~unsafe grouped_accs = | Some n when n >= 100 -> is_all_safe := false; incr unsafe | Some n -> is_all_safe := false; incr vulnerable -let print_accesses memo grouped_accs = +let print_accesses ?coloring_mode memo grouped_accs = let allglobs = get_bool "allglobs" in let race_threshold = get_int "warn.race-threshold" in - let msgs race_accs = + let coloring_for accs = + match coloring_mode with + | None -> None + | Some "greedy" -> + let graph = InterferenceGraph.of_accesses accs in + Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Greedy) graph) + | Some "dsatur" -> + let graph = InterferenceGraph.of_accesses accs in + Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Dsatur) graph) + | Some "rlf" -> + let graph = InterferenceGraph.of_accesses accs in + Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Rlf) graph) + | Some "optimal" -> + let graph = InterferenceGraph.of_accesses accs in + Some (InterferenceGraph.Coloring.color_with (module InterferenceGraph.Coloring.Optimal) graph) + | Some _ -> None + in + let msgs ?coloring race_accs = let h A.{conf; kind; node; exp; acc} = let doc = dprintf "%a with %a (conf. %d) (exp: %a)" AccessKind.pretty kind MCPAccess.A.pretty acc conf d_exp exp in (doc, Some (Messages.Location.Node node)) in - AS.elements race_accs - |> List.map h + match coloring with + | None -> + AS.elements race_accs + |> List.map h + | Some coloring -> + let module IntMap = Map.Make (Int) in + let module C = InterferenceGraph.Coloring in + let add_to_map acc map = + match C.color_of coloring acc with + | None -> map + | Some c -> + IntMap.update c (function + | None -> Some [acc] + | Some accs -> Some (acc :: accs) + ) map + in + let color_map = AS.fold add_to_map race_accs IntMap.empty in + IntMap.bindings color_map + |> List.concat_map (fun (color, accs) -> + let header = (dprintf "Color %d" color, None) in + let acc_msgs = accs |> List.rev |> List.map h in + header :: acc_msgs + ) in let group_loc = match memo with | (`Var v, _) -> Some (M.Location.CilLocation v.vdecl) (* TODO: offset location *) @@ -621,7 +709,8 @@ let print_accesses memo grouped_accs = else Info in - M.msg_group severity ?loc:group_loc ~category:Race "Memory location %a (race with conf. %d)" Memo.pretty memo conf (msgs accs); + let coloring = coloring_for accs in + M.msg_group severity ?loc:group_loc ~category:Race "Memory location %a (race with conf. %d)" Memo.pretty memo conf (msgs ?coloring accs); safe_accs ) (AS.empty ()) |> (fun safe_accs -> @@ -630,6 +719,12 @@ let print_accesses memo grouped_accs = ) let warn_global ~safe ~vulnerable ~unsafe warn_accs memo = + let coloring_mode = + match get_string "warn.race-coloring" with + | "" | "none" -> None + | "greedy" | "dsatur" | "rlf" | "optimal" as mode -> Some mode + | _ -> None + in let grouped_accs = group_may_race warn_accs in (* do expensive component finding only once *) incr_summary ~safe ~vulnerable ~unsafe grouped_accs; - print_accesses memo grouped_accs + print_accesses ?coloring_mode memo grouped_accs diff --git a/src/domains/accessColoring.ml b/src/domains/accessColoring.ml new file mode 100644 index 0000000000..cb84fa133a --- /dev/null +++ b/src/domains/accessColoring.ml @@ -0,0 +1,213 @@ +module Make (G : Graph.Coloring.G) = struct + module C = Graph.Coloring.Make (G) + module IntSet = Set.Make (Int) + + type coloring = int C.H.t + + module type ALGORITHM = sig + val color : G.t -> coloring + end + + let k_color g k = C.coloring g k + let color_with (module A : ALGORITHM) g = A.color g + let color_of coloring v = C.H.find_opt coloring v + let colors_used coloring = C.H.fold (fun _ c acc -> max acc c) coloring 0 + + module Greedy : ALGORITHM = struct + let color g = + let n = G.nb_vertex g in + let coloring = C.H.create n in + let vertices = + G.fold_vertex (fun v acc -> (G.out_degree g v, v) :: acc) g [] + |> List.sort (fun (d1, _) (d2, _) -> compare d2 d1) + |> List.map snd + in + let next_color v = + let used = ref IntSet.empty in + G.iter_succ (fun u -> + match C.H.find_opt coloring u with + | None -> () + | Some c -> used := IntSet.add c !used + ) g v; + let rec pick c = + if IntSet.mem c !used then + pick (c + 1) + else + c + in + pick 1 + in + List.iter (fun v -> C.H.add coloring v (next_color v)) vertices; + coloring + end + + module Optimal : ALGORITHM = struct + let color g = + let max_colors = max 1 (G.nb_vertex g) in + let rec loop k = + if k > max_colors then + raise Graph.Coloring.NoColoring + else + try C.coloring g k with + | Graph.Coloring.NoColoring -> loop (k + 1) + in + loop 1 + end + + module Dsatur : ALGORITHM = struct + let color g = + let n = G.nb_vertex g in + let coloring = C.H.create n in + let saturation = C.H.create n in + let degree = C.H.create n in + G.iter_vertex (fun v -> + C.H.replace saturation v IntSet.empty; + C.H.replace degree v (G.out_degree g v) + ) g; + let is_colored v = C.H.mem coloring v in + let sat_count v = + match C.H.find_opt saturation v with + | None -> 0 + | Some s -> IntSet.cardinal s + in + let choose_vertex () = + let pick v best_opt = + if is_colored v then + best_opt + else + match best_opt with + | None -> Some v + | Some best -> + let sv = sat_count v in + let sb = sat_count best in + if sv > sb then + Some v + else if sv < sb then + Some best + else ( + let dv = C.H.find degree v in + let db = C.H.find degree best in + if dv > db then Some v else Some best + ) + in + G.fold_vertex pick g None + in + let pick_color v = + let used = + match C.H.find_opt saturation v with + | None -> IntSet.empty + | Some s -> s + in + let rec pick c = + if IntSet.mem c used then + pick (c + 1) + else + c + in + pick 1 + in + let rec loop () = + match choose_vertex () with + | None -> () + | Some v -> + let c = pick_color v in + C.H.add coloring v c; + G.iter_succ (fun u -> + if not (is_colored u) then + let s = + match C.H.find_opt saturation u with + | None -> IntSet.empty + | Some s -> s + in + C.H.replace saturation u (IntSet.add c s) + ) g v; + loop () + in + loop (); + coloring + end + + module Rlf : ALGORITHM = struct + module VSet = struct + let create n = C.H.create n + let mem s v = C.H.mem s v + let add s v = C.H.replace s v () + let remove s v = C.H.remove s v + end + + let color g = + let n = G.nb_vertex g in + let coloring = C.H.create n in + let uncolored = VSet.create n in + G.iter_vertex (fun v -> VSet.add uncolored v) g; + let degree v = G.out_degree g v in + let pick_start () = + G.fold_vertex (fun v best -> + if not (VSet.mem uncolored v) then + best + else + match best with + | None -> Some v + | Some b -> + if degree v > degree b then Some v else Some b + ) g None + in + let add_forbidden forbidden v = + G.iter_succ (fun u -> + if VSet.mem uncolored u then + VSet.add forbidden u + ) g v + in + let candidate_score forbidden v = + let count = ref 0 in + G.iter_succ (fun u -> + if VSet.mem forbidden u then + incr count + ) g v; + !count + in + let pick_candidate forbidden = + G.fold_vertex (fun v best -> + if not (VSet.mem uncolored v) || VSet.mem forbidden v then + best + else + match best with + | None -> Some v + | Some b -> + let sv = candidate_score forbidden v in + let sb = candidate_score forbidden b in + if sv > sb then + Some v + else if sv < sb then + Some b + else if degree v > degree b then + Some v + else + Some b + ) g None + in + let rec color_class color = + match pick_start () with + | None -> () + | Some v0 -> + let forbidden = VSet.create n in + let add_vertex v = + C.H.add coloring v color; + VSet.remove uncolored v; + add_forbidden forbidden v + in + add_vertex v0; + let rec fill () = + match pick_candidate forbidden with + | None -> () + | Some v -> + add_vertex v; + fill () + in + fill (); + color_class (color + 1) + in + color_class 1; + coloring + end +end diff --git a/src/dune b/src/dune index 2b5f369e30..ed13199932 100644 --- a/src/dune +++ b/src/dune @@ -7,7 +7,7 @@ (name goblint_lib) (public_name goblint.lib) (modules :standard \ goblint privPrecCompare apronPrecCompare messagesCompare) - (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims + (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common ocamlgraph goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims ; Conditionally compile based on whether apron optional dependency is installed or not. ; Alternative dependencies seem like the only way to optionally depend on optional dependencies. ; See: https://dune.readthedocs.io/en/stable/reference/library-dependencies.html#alternative-dependencies