Merge pull request #1512 from goblint/yaml-witness-violation-reject

Add primitive verdict-based YAML violation witness rejection

conf/svcomp-validate.json

@@ -0,0 +1,142 @@
+{
+  "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",
+      "abortUnless",
+      "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",
+        "loopUnrollHeuristic",
+        "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",
+        "violation_sequence"
+      ],
+      "invariant-types": [
+        "location_invariant",
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": true,
+      "other": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}

src/analyses/unassumeAnalysis.ml

@@ -71,18 +71,6 @@ struct
         | _ -> ()
       );
 
-    let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
-      file = location.file_name;
-      line = location.line;
-      column = location.column;
-      byte = -1;
-      endLine = -1;
-      endColumn = -1;
-      endByte = -1;
-      synthetic = false;
-    }
-    in
-
     let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with
       | Ok yaml -> yaml
       | Error (`Msg m) ->
@@ -125,7 +113,7 @@ struct
       in
 
       let unassume_location_invariant (location_invariant: YamlWitnessType.LocationInvariant.t) =
-        let loc = loc_of_location location_invariant.location in
+        let loc = YamlWitness.loc_of_location location_invariant.location in
         let inv = location_invariant.location_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
@@ -137,7 +125,7 @@ struct
       in
 
       let unassume_loop_invariant (loop_invariant: YamlWitnessType.LoopInvariant.t) =
-        let loc = loc_of_location loop_invariant.location in
+        let loc = YamlWitness.loc_of_location loop_invariant.location in
         let inv = loop_invariant.loop_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
@@ -187,7 +175,7 @@ struct
       in
 
       let unassume_precondition_loop_invariant (precondition_loop_invariant: YamlWitnessType.PreconditionLoopInvariant.t) =
-        let loc = loc_of_location precondition_loop_invariant.location in
+        let loc = YamlWitness.loc_of_location precondition_loop_invariant.location in
         let pre = precondition_loop_invariant.precondition.string in
         let inv = precondition_loop_invariant.loop_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
@@ -202,7 +190,7 @@ struct
       let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
 
         let unassume_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
-          let loc = loc_of_location location_invariant.location in
+          let loc = YamlWitness.loc_of_location location_invariant.location in
           let inv = location_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
@@ -214,7 +202,7 @@ struct
         in
 
         let unassume_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) =
-          let loc = loc_of_location loop_invariant.location in
+          let loc = YamlWitness.loc_of_location loop_invariant.location in
           let inv = loop_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 

src/config/options.schema.json

@@ -2608,7 +2608,8 @@
                   "precondition_loop_invariant",
                   "loop_invariant_certificate",
                   "precondition_loop_invariant_certificate",
-                  "invariant_set"
+                  "invariant_set",
+                  "violation_sequence"
                 ]
               },
               "default": [

src/witness/yamlWitness.ml

@@ -43,13 +43,20 @@ struct
       specification
     }
 
-  let location ~location:(loc: Cil.location) ~(location_function): Location.t = {
-    file_name = loc.file;
-    file_hash = sha256_file loc.file;
-    line = loc.line;
-    column = loc.column;
-    function_ = location_function;
-  }
+  let location ~location:(loc: Cil.location) ~(location_function): Location.t =
+    let file_hash =
+      match GobConfig.get_string "witness.yaml.format-version" with
+      | "0.1" -> Some (sha256_file loc.file)
+      | "2.0" -> None
+      | _ -> assert false
+    in
+    {
+      file_name = loc.file;
+      file_hash;
+      line = loc.line;
+      column = Some loc.column;
+      function_ = Some location_function;
+    }
 
   let invariant invariant: Invariant.t = {
     string = invariant;
@@ -524,6 +531,17 @@ let init () =
       Svcomp.errorwith "witness missing"
     )
 
+let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
+  file = location.file_name;
+  line = location.line;
+  column = Option.value location.column ~default:1;
+  byte = -1;
+  endLine = -1;
+  endColumn = -1;
+  endByte = -1;
+  synthetic = false;
+}
+
 module ValidationResult =
 struct
   (* constructor order is important for the chain lattice *)
@@ -562,17 +580,6 @@ struct
   module InvariantParser = WitnessUtil.InvariantParser
   module VR = ValidationResult
 
-  let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
-    file = location.file_name;
-    line = location.line;
-    column = location.column;
-    byte = -1;
-    endLine = -1;
-    endColumn = -1;
-    endByte = -1;
-    synthetic = false;
-  }
-
   let validate () =
     let location_locator = Locator.create () in
     let loop_locator = Locator.create () in
@@ -806,6 +813,15 @@ struct
         None
       in
 
+      let validate_violation_sequence (violation_sequence: YamlWitnessType.ViolationSequence.t) =
+        (* TODO: update cnt-s appropriately (needs access to SV-COMP result pre-witness validation) *)
+        (* Nothing needs to be checked here!
+           If program is correct and we can prove it, we output true, which counts as refutation of violation witness.
+           If program is correct and we cannot prove it, we output unknown.
+           If program is incorrect, we output unknown. *)
+        None
+      in
+
       match entry_type_enabled target_type, entry.entry_type with
       | true, LocationInvariant x ->
         validate_location_invariant x
@@ -815,7 +831,9 @@ struct
         validate_precondition_loop_invariant x
       | true, InvariantSet x ->
         validate_invariant_set x
-      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) ->
+      | true, ViolationSequence x ->
+        validate_violation_sequence x
+      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _ | ViolationSequence _) ->
         incr cnt_disabled;
         M.info_noloc ~category:Witness "disabled entry of type %s" target_type;
         None