Thread-modular witnesses benchmarking fixes

conf/bench-yaml-validate.json

@@ -1,24 +1,31 @@
 {
   "ana": {
+    "sv-comp": {
+      "functions": true
+    },
     "int": {
       "def_exc": true,
       "enums": false,
       "interval": true
     },
     "activated": [
-      "expRelation",
       "base",
       "threadid",
       "threadflag",
       "threadreturn",
-      "escape",
+      "mallocWrapper",
       "mutexEvents",
       "mutex",
       "access",
       "race",
-      "mallocWrapper",
+      "escape",
+      "expRelation",
       "mhp",
       "assert",
+      "var_eq",
+      "symb_locks",
+      "thread",
+      "threadJoins",
       "unassume"
     ],
     "malloc": {
@@ -65,6 +72,9 @@
     },
     "int": {
       "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
     }
   },
   "pre": {

conf/bench-yaml.json

@@ -1,24 +1,31 @@
 {
   "ana": {
+    "sv-comp": {
+      "functions": true
+    },
     "int": {
       "def_exc": true,
       "enums": false,
       "interval": true
     },
     "activated": [
-      "expRelation",
       "base",
       "threadid",
       "threadflag",
       "threadreturn",
-      "escape",
+      "mallocWrapper",
       "mutexEvents",
       "mutex",
       "access",
       "race",
-      "mallocWrapper",
+      "escape",
+      "expRelation",
       "mhp",
-      "assert"
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "thread",
+      "threadJoins"
     ],
     "malloc": {
       "wrappers": [
@@ -67,6 +74,9 @@
     },
     "int": {
       "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
     }
   },
   "pre": {

conf/svcomp-yaml-validate.json

@@ -68,6 +68,9 @@
       "tokens": true
     }
   },
+  "pre": {
+    "transform-paths": false
+  },
   "exp": {
     "region-offsets": true
   },

conf/svcomp-yaml.json

@@ -64,6 +64,9 @@
       "enabled": false
     }
   },
+  "pre": {
+    "transform-paths": false
+  },
   "exp": {
     "region-offsets": true
   },

src/analyses/base.ml

@@ -45,7 +45,7 @@ struct
 
   module V =
   struct
-    include Printable.Either (Priv.V) (ThreadIdDomain.Thread)
+    include Printable.Either (struct include Priv.V let name () = "priv" end) (struct include ThreadIdDomain.Thread let name () = "threadreturn" end)
     let priv x = `Left x
     let thread x = `Right x
     include StdV
@@ -1606,6 +1606,8 @@ struct
 
     let id_meet_down ~old ~c = ID.meet old c
     let fd_meet_down ~old ~c = FD.meet old c
+
+    let contra _ = raise Deadcode
   end
 
   module Invariant = BaseInvariant.Make (InvariantEval)
@@ -2453,6 +2455,8 @@ struct
           (* don't meet with current octx values when propagating inverse operands down *)
           let id_meet_down ~old ~c = c
           let fd_meet_down ~old ~c = c
+
+          let contra st = st
         end
         in
         let module Unassume = BaseInvariant.Make (UnassumeEval) in

src/analyses/baseInvariant.ml

@@ -29,6 +29,8 @@ sig
 
   val id_meet_down: old:ID.t -> c:ID.t -> ID.t
   val fd_meet_down: old:FD.t -> c:FD.t -> FD.t
+
+  val contra: D.t -> D.t
 end
 
 module Make (Eval: Eval) =
@@ -81,7 +83,7 @@ struct
       (* make that address meet the invariant, i.e exclusion sets will be joined *)
       if is_some_bot new_val then (
         if M.tracing then M.tracel "branch" "C The branch %B is dead!\n" tv;
-        raise Analyses.Deadcode
+        contra st
       )
       else if VD.is_bot new_val
       then set a gs st addr t_lval value ~ctx (* no *_raw because this is not a real assignment *)
@@ -97,7 +99,7 @@ struct
       let offs = convert_offset a gs st o in
       let newv = VD.update_offset a oldv offs c' (Some exp) x (var.vtype) in
       let v = VD.meet oldv newv in
-      if is_some_bot v then raise Analyses.Deadcode
+      if is_some_bot v then contra st
       else (
         if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)\n" d_varinfo var VD.pretty oldv VD.pretty v pretty c VD.pretty c';
         let r = set' (Var var,NoOffset) v st in
@@ -110,7 +112,7 @@ struct
       let oldv = eval_rv_lval_refine a gs st exp x in
       let oldv = map_oldval oldv (Cilfacade.typeOfLval x) in
       let v = VD.meet oldv c' in
-      if is_some_bot v then raise Analyses.Deadcode
+      if is_some_bot v then contra st
       else (
         if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)\n" d_lval x VD.pretty oldv VD.pretty v pretty c VD.pretty c';
         set' x v st
@@ -339,11 +341,10 @@ struct
         in
         a, b
       | Eq | Ne as op ->
-        let both x = x, x in
-        let m = ID.meet a b in
         begin match op, ID.to_bool c with
           | Eq, Some true
-          | Ne, Some false -> both m (* def. equal: if they compare equal, both values must be from the meet *)
+          | Ne, Some false -> (* def. equal: if they compare equal, both values must be from the meet *)
+            (id_meet_down ~old:a ~c:b, id_meet_down ~old:b ~c:a)
           | Eq, Some false
           | Ne, Some true -> (* def. unequal *)
             (* Both values can not be in the meet together, but it's not sound to exclude the meet from both.
@@ -544,7 +545,7 @@ struct
     let eval_bool e st = match eval e st with `Int i -> ID.to_bool i | _ -> None in
     let rec inv_exp c_typed exp (st:D.t): D.t =
       (* trying to improve variables in an expression so it is bottom means dead code *)
-      if VD.is_bot_value c_typed then raise Analyses.Deadcode;
+      if VD.is_bot_value c_typed then contra st else
       match exp, c_typed with
       | UnOp (LNot, e, _), `Int c ->
         let ikind = Cilfacade.get_ikind_exp e in
@@ -633,7 +634,17 @@ struct
         in
         begin match eqs_st with
           | Some st -> st
-          | None -> st (* TODO: not bothering to fall back, no other case can refine LOr anyway *)
+          | None when ID.to_bool c = Some true ->
+            begin match inv_exp (`Int c) arg1 st with
+              | st1 ->
+                begin match inv_exp (`Int c) arg2 st with
+                  | st2 -> D.join st1 st2
+                  | exception Analyses.Deadcode -> st1
+                end
+              | exception Analyses.Deadcode -> inv_exp (`Int c) arg2 st (* Deadcode falls through *)
+            end
+          | None ->
+            st (* TODO: not bothering to fall back, no other case can refine LOr anyway *)
         end
       | (BinOp (op, e1, e2, _) as e, `Float _)
       | (BinOp (op, e1, e2, _) as e, `Int _) ->
@@ -720,7 +731,7 @@ struct
          | v -> fallback ("CastE: e did not evaluate to `Int, but " ^ sprint VD.pretty v) st)
       | e, _ -> fallback (sprint d_plainexp e ^ " not implemented") st
     in
-    if eval_bool exp st = Some (not tv) then raise Analyses.Deadcode (* we already know that the branch is dead *)
+    if eval_bool exp st = Some (not tv) then contra st (* we already know that the branch is dead *)
     else
       (* C11 6.5.13, 6.5.14, 6.5.3.3: LAnd, LOr and LNot also return 0 or 1 *)
       let is_cmp = function

src/analyses/commonPriv.ml

@@ -85,6 +85,7 @@ struct
   struct
     (* TODO: Either3? *)
     include Printable.Either (Printable.Either (VMutex) (VMutexInits)) (VGlobal)
+    let name () = "MutexGlobals"
     let mutex x: t = `Left (`Left x)
     let mutex_inits: t = `Left (`Right ())
     let global x: t = `Right x

src/analyses/mCPRegistry.ml

@@ -197,7 +197,8 @@ struct
     f n (assoc_dom n) d
 
   let pretty () = unop_map (fun n (module S: Printable.S) x ->
-      Pretty.dprintf "%s:%a" (S.name ()) S.pretty (obj x)
+      let analysis_name = find_spec_name n in
+      Pretty.dprintf "%s:%a" analysis_name S.pretty (obj x)
     )
 
   let show = unop_map (fun n (module S: Printable.S) x ->
@@ -257,6 +258,7 @@ struct
   open Obj
 
   include DomVariantPrintable (PrintableOfSysVarSpec (DLSpec))
+  let name () = "MCP.V"
 
   let unop_map f ((n, d):t) =
     f n (assoc_dom n) d

src/analyses/mutexAnalysis.ml

@@ -25,7 +25,7 @@ struct
 
     module V =
     struct
-      include Printable.Either (CilType.Varinfo) (ValueDomain.Addr)
+      include Printable.Either (struct include CilType.Varinfo let name () = "protecting" end) (struct include ValueDomain.Addr let name () = "protected" end)
       let name () = "mutex"
       let protecting x = `Left x
       let protected x = `Right x

src/analyses/unassumeAnalysis.ml

@@ -55,7 +55,7 @@ struct
     let rec iter_node node =
       if not (NH.mem reachable node) then begin
         NH.replace reachable node ();
-        (* TODO: filter synthetic like in Validator *)
+        (* TODO: filter synthetic? *)
         if WitnessInvariant.is_invariant_node node then
           Locator.add locator (Node.location node) node;
         if WitnessUtil.NH.mem WitnessInvariant.loop_heads node then
@@ -229,7 +229,7 @@ struct
     match es with
     | x :: xs ->
       let e = List.fold_left (fun a {exp = b; _} -> Cil.(BinOp (LAnd, a, b, intType))) x.exp xs in
-      (* M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e; *)
+      M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e;
       if not !Goblintutil.postsolving then (
         if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (ctx.ask (EvalInt e)) = Some false) then (
           let uuids = x.uuid :: List.map (fun {uuid; _} -> uuid) xs in

src/domains/printable.ml

@@ -255,13 +255,13 @@ struct
 
   let pretty () (state:t) =
     match state with
-    | `Left n ->  Base1.pretty () n
-    | `Right n ->  Base2.pretty () n
+    | `Left n -> Pretty.dprintf "%s:%a" (Base1.name ()) Base1.pretty n
+    | `Right n -> Pretty.dprintf "%s:%a" (Base2.name ()) Base2.pretty n
 
   let show state =
     match state with
-    | `Left n ->  Base1.show n
-    | `Right n ->  Base2.show n
+    | `Left n -> (Base1.name ()) ^ ":" ^ Base1.show n
+    | `Right n -> (Base2.name ()) ^ ":" ^ Base2.show n
 
   let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name ()
   let printXml f = function

src/framework/constraints.ml

@@ -450,8 +450,8 @@ struct
     | `G x -> `G (GV.relift x)
 
   let pretty_trace () = function
-    | `L a -> LV.pretty_trace () a
-    | `G a -> GV.pretty_trace () a
+    | `L a -> Pretty.dprintf "L:%a" LV.pretty_trace a
+    | `G a -> Pretty.dprintf "G:%a" GV.pretty_trace a
 
   let printXml f = function
     | `L a -> LV.printXml f a
@@ -1211,6 +1211,7 @@ struct
   module V =
   struct
     include Printable.Either (S.V) (Node)
+    let name () = "DeadBranch"
     let s x = `Left x
     let node x = `Right x
     let is_write_only = function

src/maingoblint.ml

@@ -385,9 +385,14 @@ let parse_preprocessed preprocessed =
         (path_str, system_header) (* ignore special "paths" *)
       | _ ->
         let path = Fpath.v path_str in
-        let dir = (Option.get task_opt).ProcessPool.cwd |? goblint_cwd in (* relative to compilation database directory or goblint's cwd *)
-        let path' = Fpath.normalize @@ Fpath.append dir path in
-        let path' = Fpath.rem_prefix goblint_cwd path' |? path' in (* remove goblint cwd prefix (if has one) for readability *)
+        let path' = if get_bool "pre.transform-paths" then (
+            let dir = (Option.get task_opt).ProcessPool.cwd |? goblint_cwd in (* relative to compilation database directory or goblint's cwd *)
+            let path' = Fpath.normalize @@ Fpath.append dir path in
+            Fpath.rem_prefix goblint_cwd path' |? path' (* remove goblint cwd prefix (if has one) for readability *)
+          )
+          else
+            path
+        in
         Preprocessor.FpathH.modify_def Fpath.Map.empty preprocessed_file (Fpath.Map.add path' system_header) Preprocessor.dependencies; (* record dependency *)
         (Fpath.to_string path', system_header)
     in

src/solvers/td3.ml

@@ -311,7 +311,7 @@ module Base =
             if not wp then tmp
             else
               if term then
-                match phase with Widen -> S.Dom.widen old (S.Dom.join old tmp) | Narrow -> S.Dom.narrow old tmp
+                match phase with Widen -> S.Dom.widen old (S.Dom.join old tmp) | Narrow when GobConfig.get_bool "exp.no-narrow" -> old (* no narrow *) | Narrow -> S.Dom.narrow old tmp
               else
                 box old tmp
           in
@@ -415,6 +415,7 @@ module Base =
         if tracing then trace "sol2" "stable add %a\n" S.Var.pretty_trace y;
         HM.replace stable y ();
         if not (S.Dom.leq tmp old) then (
+          if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %b) from %a\n" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x;
           let sided = match x with
             | Some x ->
               let sided = VS.mem x old_sides in

src/util/gobConfig.ml

@@ -387,7 +387,7 @@ struct
   (** Merge configurations form a file with current. *)
   let merge_file fn =
     let cwd = Fpath.v (Sys.getcwd ()) in
-    let config_dirs = cwd :: Goblint_sites.conf in
+    let config_dirs = cwd :: Fpath.(parent (v Sys.executable_name)) :: Goblint_sites.conf in
     let file = List.find_map_opt (fun custom_include_dir ->
         let path = Fpath.append custom_include_dir fn in
         if Sys.file_exists (Fpath.to_string path) then

src/util/options.schema.json

@@ -242,6 +242,12 @@
             }
           },
           "additionalProperties": false
+        },
+        "transform-paths": {
+          "title": "pre.transform-paths",
+          "description": "Normalize and relativize paths in parsed CIL locations. Can cause issues locating YAML witness invariants due to differing paths.",
+          "type": "boolean",
+          "default": true
         }
       },
       "additionalProperties": false

src/witness/yamlWitness.ml

@@ -16,7 +16,7 @@ struct
   let producer: Producer.t = {
     name = "Goblint";
     version = Version.goblint;
-    command_line = Goblintutil.command_line;
+    command_line = Some Goblintutil.command_line;
   }
 
   let metadata ?task (): Metadata.t =
@@ -447,7 +447,8 @@ struct
     let loop_locator = Locator.create () in
     LHT.iter (fun ((n, _) as lvar) _ ->
         let loc = Node.location n in
-        if not loc.synthetic then
+        (* TODO: filter synthetic? *)
+        if WitnessInvariant.is_invariant_node n then
           Locator.add locator loc lvar;
         if WitnessUtil.NH.mem WitnessInvariant.loop_heads n then
           Locator.add loop_locator loc lvar