Location fixes for YAML witness generation/validation

conf/svcomp-validate.json

@@ -0,0 +1,139 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "unassume"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc",
+        "ldv_kzalloc"
+      ]
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "memsafetySpecification",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    },
+    "widen": {
+      "tokens": true
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": false
+    },
+    "yaml": {
+      "enabled": false,
+      "strict": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "location_invariant",
+        "loop_invariant",
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "location_invariant",
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": true,
+      "other": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}

conf/svcomp.json

@@ -84,7 +84,6 @@
         "congruence",
         "octagon",
         "wideningThresholds",
-        "loopUnrollHeuristic",
         "memsafetySpecification",
         "termination",
         "tmpSpecialAnalysis"

goblint.opam

@@ -78,7 +78,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#fb471582d7e9685ab705ba57f7a6675b97ca8f64" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

goblint.opam.locked

@@ -134,7 +134,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.3"
-    "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5"
+    "git+https://github.com/goblint/cil.git#fb471582d7e9685ab705ba57f7a6675b97ca8f64"
   ]
   [
     "ppx_deriving.5.2.1"

goblint.opam.template

@@ -3,7 +3,7 @@
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#fb471582d7e9685ab705ba57f7a6675b97ca8f64" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

src/analyses/unassumeAnalysis.ml

@@ -27,7 +27,7 @@ struct
 
   module Locator = WitnessUtil.Locator (Node)
 
-  let locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *)
+  let location_locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *)
   let loop_locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *)
 
   type inv = {
@@ -41,26 +41,26 @@ struct
   let pre_invs: inv EH.t NH.t = NH.create 100
 
   let init _ =
-    Locator.clear locator;
+    Locator.clear location_locator;
     Locator.clear loop_locator;
     let module FileCfg =
     struct
       let file = !Cilfacade.current_file
       module Cfg = (val !MyCFG.current_cfg)
     end  in
-    let module WitnessInvariant = WitnessUtil.Invariant (FileCfg) in
+    let module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) in
 
     (* DFS, copied from CfgTools.find_backwards_reachable *)
     let reachable = NH.create 100 in
     let rec iter_node node =
       if not (NH.mem reachable node) then begin
         NH.replace reachable node ();
-        (* TODO: filter synthetic?
-           See YamlWitness. *)
-        if WitnessInvariant.is_invariant_node node then
-          Locator.add locator (Node.location node) node;
-        if WitnessUtil.NH.mem WitnessInvariant.loop_heads node then
-          Locator.add loop_locator (Node.location node) node;
+        Option.iter (fun loc ->
+            Locator.add location_locator loc node
+          ) (WitnessInvariant.location_location node);
+        Option.iter (fun loc ->
+            Locator.add loop_locator loc node
+          ) (WitnessInvariant.loop_location node);
         List.iter (fun (_, prev_node) ->
             iter_node prev_node
           ) (FileCfg.Cfg.prev node)
@@ -130,7 +130,7 @@ struct
         let inv = location_invariant.location_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
-        match Locator.find_opt locator loc with
+        match Locator.find_opt location_locator loc with
         | Some nodes ->
           unassume_nodes_invariant ~loc ~nodes inv
         | None ->
@@ -193,7 +193,7 @@ struct
         let inv = precondition_loop_invariant.loop_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
-        match Locator.find_opt locator loc with
+        match Locator.find_opt loop_locator loc with
         | Some nodes ->
           unassume_precondition_nodes_invariant ~loc ~nodes pre inv
         | None ->
@@ -207,7 +207,7 @@ struct
           let inv = location_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
-          match Locator.find_opt locator loc with
+          match Locator.find_opt location_locator loc with
           | Some nodes ->
             unassume_nodes_invariant ~loc ~nodes inv
           | None ->

src/common/framework/cfgTools.ml

@@ -132,13 +132,7 @@ let () = Printexc.register_printer (function
     | _ -> None (* for other exceptions *)
   )
 
-(** Type of CFG "edges": keyed by 'from' and 'to' nodes,
-    along with the list of connecting instructions. *)
-module CfgEdge = struct
-  type t = Node.t * MyCFG.edges * Node.t [@@deriving eq, hash]
-end
 
-module CfgEdgeH = BatHashtbl.Make (CfgEdge)
 
 let createCFG (file: file) =
   let cfgF = H.create 113 in
@@ -254,7 +248,7 @@ let createCFG (file: file) =
         let pseudo_return = lazy (
           if Messages.tracing then Messages.trace "cfg" "adding pseudo-return to the function %s.\n" fd.svar.vname;
           let fd_end_loc = {fd_loc with line = fd_loc.endLine; byte = fd_loc.endByte; column = fd_loc.endColumn} in
-          let newst = mkStmt (Return (None, fd_end_loc)) in
+          let newst = mkStmt (Return (None, fd_end_loc, locUnknown)) in
           newst.sid <- Cilfacade.get_pseudo_return_id fd;
           Cilfacade.StmtH.add Cilfacade.pseudo_return_to_fun newst fd;
           Cilfacade.IntH.replace Cilfacade.pseudo_return_stmt_sids newst.sid newst;
@@ -340,8 +334,8 @@ let createCFG (file: file) =
             (* CIL's xform_switch_stmt (via prepareCFG) always adds both continue and break statements to all Loops. *)
             failwith "MyCFG.createCFG: unprepared Loop"
 
-          | Return (exp, loc) ->
-            addEdge (Statement stmt) (loc, Ret (exp, fd)) (Function fd)
+          | Return (exp, loc, eloc) ->
+            addEdge (Statement stmt) (Cilfacade.eloc_fallback ~eloc ~loc, Ret (exp, fd)) (Function fd)
 
           | Goto (_, loc) ->
             (* Gotos are generally unnecessary and unwanted because find_real_stmt skips over these. *)
@@ -608,7 +602,7 @@ let fprint_hash_dot cfg  =
   close_out out
 
 
-let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t =
+let getCFG (file: file) : cfg * cfg * _ =
   let cfgF, cfgB, skippedByEdge = createCFG file in
   let cfgF, cfgB, skippedByEdge =
     if get_bool "exp.mincfg" then
@@ -617,13 +611,11 @@ let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t =
       (cfgF, cfgB, skippedByEdge)
   in
   if get_bool "justcfg" then fprint_hash_dot cfgB;
-  (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), skippedByEdge
+  (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), (fun u e v -> CfgEdgeH.find skippedByEdge (u, e, v))
 
-let compute_cfg_skips file =
+let compute_cfg file =
   let cfgF, cfgB, skippedByEdge = getCFG file in
-  (module struct let prev = cfgB let next = cfgF end : CfgBidir), skippedByEdge
-
-let compute_cfg file = fst (compute_cfg_skips file)
+  (module struct let prev = cfgB let next = cfgF let skippedByEdge = skippedByEdge end : CfgBidirSkip)
 
 
 let iter_fd_edges (module Cfg : CfgBackward) fd =

src/common/framework/myCFG.ml

@@ -42,19 +42,34 @@ sig
   include CfgForward
 end
 
+(** Type of CFG "edges": keyed by 'from' and 'to' nodes,
+    along with the list of connecting instructions. *)
+module CfgEdge = struct
+  type t = Node.t * edges * Node.t [@@deriving eq, hash]
+end
+
+module CfgEdgeH = BatHashtbl.Make (CfgEdge)
+
+module type CfgBidirSkip =
+sig
+  include CfgBidir
+  val skippedByEdge: node -> edges -> node -> stmt list
+end
+
 
 module NodeH = BatHashtbl.Make (Node)
 
 
 let current_node = Node.current_node
-let current_cfg : (module CfgBidir) ref =
+let current_cfg : (module CfgBidirSkip) ref =
   let module Cfg =
   struct
     let next _ = raise Not_found
     let prev _ = raise Not_found
+    let skippedByEdge _ _ _ = raise Not_found
   end
   in
-  ref (module Cfg: CfgBidir)
+  ref (module Cfg: CfgBidirSkip)
 
 let unknown_exp : exp = mkString "__unknown_value__"
 let dummy_func = emptyFunction "__goblint_dummy_init" (* TODO get rid of this? *)
@@ -64,5 +79,5 @@ let dummy_node = FunctionEntry Cil.dummyFunDec
 module type FileCfg =
 sig
   val file: Cil.file
-  module Cfg: CfgBidir
+  module Cfg: CfgBidirSkip
 end

src/common/util/cilLocation.ml

@@ -34,7 +34,7 @@ let rec get_stmtLoc stmt: locs =
     {loc = locUnknown; eloc = locUnknown}
 
   | Instr (hd :: _) -> get_instrLoc hd
-  | Return (_, loc) -> {loc; eloc = locUnknown}
+  | Return (_, loc, eloc) -> {loc; eloc}
   | Goto (_, loc) -> {loc; eloc = locUnknown}
   | ComputedGoto (_, loc) -> {loc; eloc = locUnknown}
   | Break loc -> {loc; eloc = locUnknown}

src/common/util/cilfacade.ml

@@ -494,7 +494,7 @@ class countFnVisitor = object
   inherit nopCilVisitor
   method! vstmt s =
     match s.skind with
-    | Return (_, loc)
+    | Return (_, loc, _)
     | Goto (_, loc)
     | ComputedGoto (_, loc)
     | Break loc

src/common/util/cilfacade0.ml

@@ -42,7 +42,7 @@ let rec get_stmtLoc stmt =
     get_labelsLoc stmt.labels
 
   | Instr (hd :: _) -> get_instrLoc hd
-  | Return (_, loc) -> loc
+  | Return (_, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Goto (_, loc) -> loc
   | ComputedGoto (_, loc) -> loc
   | Break loc -> loc