Merge pull request #1575 from goblint/constraints-split

Move `Spec` lifters out of `Constraints`

src/framework/compareConstraints.ml

@@ -0,0 +1,217 @@
+open Batteries
+open Analyses
+open ConstrSys
+open GobConfig
+
+
+module CompareGlobSys (SpecSys: SpecSys) =
+struct
+  open SpecSys
+  module Sys = EQSys
+  module LH = LHT
+  module GH = GHT
+
+  open Spec
+  module G = Sys.G
+
+  module PP = Hashtbl.Make (Node)
+
+  let compare_globals g1 g2 =
+    let eq, le, gr, uk = ref 0, ref 0, ref 0, ref 0 in
+    let f_eq () = incr eq in
+    let f_le () = incr le in
+    let f_gr () = incr gr in
+    let f_uk () = incr uk in
+    let f k v1 =
+      let v2 = try GH.find g2 k with Not_found -> G.bot () in
+      let b1 = G.leq v1 v2 in
+      let b2 = G.leq v2 v1 in
+      if b1 && b2 then
+        f_eq ()
+      else if b1 then begin
+        if get_bool "dbg.compare_runs.diff" then
+          Logs.info "Global %a is more precise using left:\n%a" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1);
+        f_le ()
+      end else if b2 then begin
+        if get_bool "dbg.compare_runs.diff" then
+          Logs.info "Global %a is more precise using right:\n%a" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2);
+        f_gr ()
+      end else begin
+        if get_bool "dbg.compare_runs.diff" then (
+          Logs.info "Global %a is incomparable (diff):\n%a" Sys.GVar.pretty_trace k G.pretty_diff (v1,v2);
+          Logs.info "Global %a is incomparable (reverse diff):\n%a" Sys.GVar.pretty_trace k G.pretty_diff (v2,v1);
+        );
+        f_uk ()
+      end
+    in
+    GH.iter f g1;
+    Logs.info "globals:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d" !eq !le !gr !uk
+
+  let compare_locals h1 h2 =
+    let eq, le, gr, uk = ref 0, ref 0, ref 0, ref 0 in
+    let f k v1 =
+      if PP.mem h2 k then
+        let v2 = PP.find h2 k in
+        let b1 = D.leq v1 v2 in
+        let b2 = D.leq v2 v1 in
+        if b1 && b2 then
+          incr eq
+        else if b1 then begin
+          if get_bool "dbg.compare_runs.diff" then
+            Logs.info "%a @@ %a is more precise using left:\n%a" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1);
+          incr le
+        end else if b2 then begin
+          if get_bool "dbg.compare_runs.diff" then
+            Logs.info "%a @@ %a is more precise using right:\n%a" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2);
+          incr gr
+        end else begin
+          if get_bool "dbg.compare_runs.diff" then (
+            Logs.info "%a @@ %a is incomparable (diff):\n%a" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v1,v2);
+            Logs.info "%a @@ %a is incomparable (reverse diff):\n%a" Node.pretty_plain k CilType.Location.pretty (Node.location k) D.pretty_diff (v2,v1);
+          );
+          incr uk
+        end
+    in
+    PP.iter f h1;
+    (* let k1 = Set.of_enum @@ PP.keys h1 in
+       let k2 = Set.of_enum @@ PP.keys h2 in
+       let o1 = Set.cardinal @@ Set.diff k1 k2 in
+       let o2 = Set.cardinal @@ Set.diff k2 k1 in
+       Logs.info "locals: \tequal = %d\tleft = %d[%d]\tright = %d[%d]\tincomparable = %d" !eq !le o1 !gr o2 !uk *)
+    Logs.info "locals: \tequal = %d\tleft = %d\tright = %d\tincomparable = %d" !eq !le !gr !uk
+
+  let compare_locals_ctx h1 h2 =
+    let eq, le, gr, uk, no2, no1 = ref 0, ref 0, ref 0, ref 0, ref 0, ref 0 in
+    let f_eq () = incr eq in
+    let f_le () = incr le in
+    let f_gr () = incr gr in
+    let f_uk () = incr uk in
+    let f k v1 =
+      if not (LH.mem h2 k) then incr no2 else
+        let v2 = LH.find h2 k in
+        let b1 = D.leq v1 v2 in
+        let b2 = D.leq v2 v1 in
+        if b1 && b2 then
+          f_eq ()
+        else if b1 then begin
+          if get_bool "dbg.compare_runs.diff" then
+            Logs.info "%a is more precise using left:\n%a" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1);
+          f_le ()
+        end else if b2 then begin
+          if get_bool "dbg.compare_runs.diff" then
+            Logs.info "%a is more precise using right:\n%a" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2);
+          f_gr ()
+        end else begin
+          if get_bool "dbg.compare_runs.diff" then (
+            Logs.info "%a is incomparable (diff):\n%a" Sys.LVar.pretty_trace k D.pretty_diff (v1,v2);
+            Logs.info "%a is incomparable (reverse diff):\n%a" Sys.LVar.pretty_trace k D.pretty_diff (v2,v1);
+          );
+          f_uk ()
+        end
+    in
+    LH.iter f h1;
+    let f k v2 =
+      if not (LH.mem h1 k) then incr no1
+    in
+    LH.iter f h2;
+    (* let k1 = Set.of_enum @@ PP.keys h1 in *)
+    (* let k2 = Set.of_enum @@ PP.keys h2 in *)
+    (* let o1 = Set.cardinal @@ Set.diff k1 k2 in *)
+    (* let o2 = Set.cardinal @@ Set.diff k2 k1 in *)
+    Logs.info "locals_ctx:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d\tno_ctx_in_right = %d\tno_ctx_in_left = %d" !eq !le !gr !uk !no2 !no1
+
+  let compare (name1,name2) (l1,g1) (l2,g2) =
+    let one_ctx (n,_) v h =
+      PP.replace h n (try D.join v (PP.find h n) with Not_found -> v);
+      h
+    in
+    (* these contain results where the contexts per node have been joined *)
+    let h1 = PP.create 113 in
+    let h2 = PP.create 113 in
+    let _  = LH.fold one_ctx l1 h1 in
+    let _  = LH.fold one_ctx l2 h2 in
+    Logs.newline ();
+    Logs.info "Comparing GlobConstrSys precision of %s (left) with %s (right):" name1 name2;
+    compare_globals g1 g2;
+    compare_locals h1 h2;
+    compare_locals_ctx l1 l2;
+    Logs.newline ();
+end
+
+module CompareHashtbl (Var: VarType) (Dom: Lattice.S) (VH: Hashtbl.S with type key = Var.t) =
+struct
+  module Var =
+  struct
+    include Printable.Std
+    include Var
+    let name () = "var"
+
+    let pretty = pretty_trace
+    include Printable.SimplePretty (
+      struct
+        type nonrec t = t
+        let pretty = pretty
+      end
+      )
+  end
+
+  include PrecCompare.MakeHashtbl (Var) (Dom) (VH)
+end
+
+module CompareEqSys (Sys: EqConstrSys) (VH: Hashtbl.S with type key = Sys.Var.t) =
+struct
+  module Compare = CompareHashtbl (Sys.Var) (Sys.Dom) (VH)
+
+  let compare (name1, name2) vh1 vh2 =
+    Logs.newline ();
+    Logs.info "Comparing EqConstrSys precision of %s (left) with %s (right):" name1 name2;
+    let verbose = get_bool "dbg.compare_runs.diff" in
+    let (_, msg) = Compare.compare ~verbose ~name1 vh1 ~name2 vh2 in
+    Logs.info "EqConstrSys comparison summary: %t" (fun () -> msg);
+    Logs.newline ();
+end
+
+module CompareGlobal (GVar: VarType) (G: Lattice.S) (GH: Hashtbl.S with type key = GVar.t) =
+struct
+  module Compare = CompareHashtbl (GVar) (G) (GH)
+
+  let compare (name1, name2) vh1 vh2 =
+    Logs.newline ();
+    Logs.info "Comparing globals precision of %s (left) with %s (right):" name1 name2;
+    let verbose = get_bool "dbg.compare_runs.diff" in
+    let (_, msg) = Compare.compare ~verbose ~name1 vh1 ~name2 vh2 in
+    Logs.info "Globals comparison summary: %t" (fun () -> msg);
+    Logs.newline ();
+end
+
+module CompareNode (C: Printable.S) (D: Lattice.S) (LH: Hashtbl.S with type key = VarF (C).t) =
+struct
+  module Node =
+  struct
+    include Node
+    let var_id _ = "nodes"
+    let node x = x
+    let is_write_only _ = false
+  end
+  module NH = Hashtbl.Make (Node)
+
+  module Compare = CompareHashtbl (Node) (D) (NH)
+
+  let join_contexts (lh: D.t LH.t): D.t NH.t =
+    let nh = NH.create 113 in
+    LH.iter (fun (n, _) d ->
+        let d' = try D.join (NH.find nh n) d with Not_found -> d in
+        NH.replace nh n d'
+      ) lh;
+    nh
+
+  let compare (name1, name2) vh1 vh2 =
+    Logs.newline ();
+    Logs.info "Comparing nodes precision of %s (left) with %s (right):" name1 name2;
+    let vh1' = join_contexts vh1 in
+    let vh2' = join_contexts vh2 in
+    let verbose = get_bool "dbg.compare_runs.diff" in
+    let (_, msg) = Compare.compare ~verbose ~name1 vh1' ~name2 vh2' in
+    Logs.info "Nodes comparison summary: %t" (fun () -> msg);
+    Logs.newline ();
+end