Merge pull request #1226 from goblint/sv-comp-yaml

Refactor GraphML witness options
goblint · Nov 2, 2023 · 8aaa9d0 · 8aaa9d0
2 parents 6131273 + 6cd62e5
commit 8aaa9d0
Show file tree

Hide file tree

Showing 19 changed files with 118 additions and 81 deletions.
diff --git a/conf/ldv-races.json b/conf/ldv-races.json
@@ -53,8 +53,11 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   },
   "solver": "td3",
   "sem": {

diff --git a/conf/svcomp-yaml.json b/conf/svcomp-yaml.json
@@ -76,7 +76,9 @@
     "region-offsets": true
   },
   "witness": {
-    "enabled": false,
+    "graphml": {
+      "enabled": false
+    },
     "yaml": {
       "enabled": true
     },

diff --git a/conf/svcomp.json b/conf/svcomp.json
@@ -91,8 +91,11 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   },
   "pre": {
     "enabled": false

diff --git a/conf/svcomp21.json b/conf/svcomp21.json
@@ -64,6 +64,9 @@
     }
   },
   "witness": {
-    "id": "enumerate"
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate"
+    }
   }
 }
diff --git a/conf/svcomp22-intervals-novareq-affeq-apron.json b/conf/svcomp22-intervals-novareq-affeq-apron.json
@@ -68,7 +68,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
diff --git a/conf/svcomp22-intervals-novareq-affeq-native.json b/conf/svcomp22-intervals-novareq-affeq-native.json
@@ -65,7 +65,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
diff --git a/conf/svcomp22-intervals-novareq-octagon-apron.json b/conf/svcomp22-intervals-novareq-octagon-apron.json
@@ -68,7 +68,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
diff --git a/conf/svcomp22-intervals-novareq-polyhedra-apron.json b/conf/svcomp22-intervals-novareq-polyhedra-apron.json
@@ -68,7 +68,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
diff --git a/conf/svcomp22.json b/conf/svcomp22.json
@@ -67,7 +67,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
diff --git a/conf/svcomp23.json b/conf/svcomp23.json
@@ -90,7 +90,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
@@ -2279,24 +2279,56 @@
       "title": "witness",
       "type": "object",
       "properties": {
-        "enabled": {
-          "title": "witness.enabled",
-          "description": "Output witness",
-          "type": "boolean",
-          "default": true
-        },
-        "path": {
-          "title": "witness.path",
-          "description": "Witness output path",
-          "type": "string",
-          "default": "witness.graphml"
-        },
-        "id": {
-          "title": "witness.id",
-          "description": "Which witness node IDs to use? node/enumerate",
-          "type": "string",
-          "enum": ["node", "enumerate"],
-          "default": "node"
+        "graphml": {
+          "title": "witness.graphml",
+          "type": "object",
+          "properties": {
+            "enabled": {
+              "title": "witness.graphml.enabled",
+              "description": "Output GraphML witness",
+              "type": "boolean",
+              "default": false
+            },
+            "path": {
+              "title": "witness.graphml.path",
+              "description": "GraphML witness output path",
+              "type": "string",
+              "default": "witness.graphml"
+            },
+            "id": {
+              "title": "witness.graphml.id",
+              "description": "Which witness node IDs to use? node/enumerate",
+              "type": "string",
+              "enum": ["node", "enumerate"],
+              "default": "node"
+            },
+            "minimize": {
+              "title": "witness.graphml.minimize",
+              "description": "Try to minimize the witness",
+              "type": "boolean",
+              "default": false
+            },
+            "uncil": {
+              "title": "witness.graphml.uncil",
+              "description":
+                "Try to undo CIL control flow transformations in witness",
+              "type": "boolean",
+              "default": false
+            },
+            "stack": {
+              "title": "witness.graphml.stack",
+              "description": "Construct stacktrace-based witness nodes",
+              "type": "boolean",
+              "default": true
+            },
+            "unknown": {
+              "title": "witness.graphml.unknown",
+              "description": "Output witness for unknown result",
+              "type": "boolean",
+              "default": true
+            }
+          },
+          "additionalProperties": false
         },
         "invariant": {
           "title": "witness.invariant",
@@ -2333,7 +2365,7 @@
               "title": "witness.invariant.accessed",
               "description": "Only emit invariants for locally accessed variables",
               "type": "boolean",
-              "default": true
+              "default": false
             },
             "full": {
               "title": "witness.invariant.full",
@@ -2376,31 +2408,6 @@
           },
           "additionalProperties": false
         },
-        "minimize": {
-          "title": "witness.minimize",
-          "description": "Try to minimize the witness",
-          "type": "boolean",
-          "default": false
-        },
-        "uncil": {
-          "title": "witness.uncil",
-          "description":
-            "Try to undo CIL control flow transformations in witness",
-          "type": "boolean",
-          "default": false
-        },
-        "stack": {
-          "title": "witness.stack",
-          "description": "Construct stacktrace-based witness nodes",
-          "type": "boolean",
-          "default": true
-        },
-        "unknown": {
-          "title": "witness.unknown",
-          "description": "Output witness for unknown result",
-          "type": "boolean",
-          "default": true
-        },
         "yaml": {
           "title": "witness.yaml",
           "type": "object",

diff --git a/src/framework/control.ml b/src/framework/control.ml
@@ -14,7 +14,7 @@ module type S2S = functor (X : Spec) -> Spec
 (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
 let spec_module: (module Spec) Lazy.t = lazy (
   GobConfig.building_spec := true;
-  let arg_enabled = (get_bool "ana.sv-comp.enabled" && get_bool "witness.enabled") || get_bool "exp.arg" in
+  let arg_enabled = get_bool "witness.graphml.enabled" || get_bool "exp.arg" in
   let open Batteries in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
@@ -160,7 +160,8 @@ let check_arguments () =
         ^ String.concat " and " @@ List.map (fun s -> "'" ^ s ^ "'") imprecise_options)
   );
   if get_bool "solvers.td3.space" && get_bool "solvers.td3.remove-wpoint" then fail "solvers.td3.space is incompatible with solvers.td3.remove-wpoint";
-  if get_bool "solvers.td3.space" && get_string "solvers.td3.side_widen" = "sides-local" then fail "solvers.td3.space is incompatible with solvers.td3.side_widen = 'sides-local'"
+  if get_bool "solvers.td3.space" && get_string "solvers.td3.side_widen" = "sides-local" then fail "solvers.td3.space is incompatible with solvers.td3.side_widen = 'sides-local'";
+  if not (get_bool "ana.sv-comp.enabled") && get_bool "witness.graphml.enabled" then fail "witness.graphml.enabled: cannot generate GraphML witness without SV-COMP mode (ana.sv-comp.enabled)"
 
 (** Initialize some globals in other modules. *)
 let handle_flags () =

diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml
@@ -320,7 +320,7 @@ struct
 
 
   let rec next_opt' n = match n with
-    | Statement {sid; skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.uncil" -> (* TODO: use elocs instead? *)
+    | Statement {sid; skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.graphml.uncil" -> (* TODO: use elocs instead? *)
       let (e, if_true_next_n,  if_false_next_n) = partition_if_next (Arg.next n) in
       (* avoid infinite recursion with sid <> sid2 in if_nondet_var *)
       (* TODO: why physical comparison if_false_next_n != n doesn't work? *)
@@ -373,7 +373,7 @@ struct
       Question(e_cond, e_true, e_false, Cilfacade.typeOf e_false)
 
   let next_opt' n = match n with
-    | Statement {skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.uncil" -> (* TODO: use eloc instead? *)
+    | Statement {skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.graphml.uncil" -> (* TODO: use eloc instead? *)
       let (e_cond, if_true_next_n, if_false_next_n) = partition_if_next (Arg.next n) in
       if Node.location if_true_next_n = loc && Node.location if_false_next_n = loc then
         match Arg.next if_true_next_n, Arg.next if_false_next_n with

diff --git a/src/witness/witness.ml b/src/witness/witness.ml
@@ -13,7 +13,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
   let module Invariant = WitnessUtil.Invariant (Task) in
 
   let module TaskResult =
-    (val if get_bool "witness.stack" then
+    (val if get_bool "witness.graphml.stack" then
         (module StackTaskResult (Task.Cfg) (TaskResult) : WitnessTaskResult)
       else
         (module TaskResult)
@@ -24,7 +24,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
   struct
     (* type node = N.t
     type edge = TaskResult.Arg.Edge.t *)
-    let minwitness = get_bool "witness.minimize"
+    let minwitness = get_bool "witness.graphml.minimize"
     let is_interesting_real from_node edge to_node =
       (* TODO: don't duplicate this logic with write_node, write_edge *)
       (* startlines aren't currently interesting because broken, see below *)
@@ -58,12 +58,12 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
   let module N = Arg.Node in
   let module GML = XmlGraphMlWriter in
   let module GML =
-    (val match get_string "witness.id" with
+    (val match get_string "witness.graphml.id" with
       | "node" ->
         (module ArgNodeGraphMlWriter (N) (GML) : GraphMlWriter with type node = N.t)
       | "enumerate" ->
         (module EnumerateNodeGraphMlWriter (N) (GML))
-      | _ -> failwith "witness.id: illegal value"
+      | _ -> failwith "witness.graphml.id: illegal value"
     )
   in
   let module GML = DeDupGraphMlWriter (N) (GML) in
@@ -305,7 +305,7 @@ struct
 
   let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
     let module Arg: BiArgInvariant =
-      (val if GobConfig.get_bool "witness.enabled" then (
+      (val if GobConfig.get_bool "witness.graphml.enabled" then (
            let module Arg = (val ArgTool.create entrystates) in
            let module Arg =
            struct
@@ -572,13 +572,13 @@ struct
 
   let write entrystates =
     let module Task = (val (BatOption.get !task)) in
-    let module TaskResult = (val (Timing.wrap "determine" (determine_result entrystates) (module Task))) in
+    let module TaskResult = (val (Timing.wrap "sv-comp result" (determine_result entrystates) (module Task))) in
 
     print_task_result (module TaskResult);
 
-    if get_bool "witness.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.unknown") then (
-      let witness_path = get_string "witness.path" in
-      Timing.wrap "write" (write_file witness_path (module Task)) (module TaskResult)
+    if get_bool "witness.graphml.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.graphml.unknown") then (
+      let witness_path = get_string "witness.graphml.path" in
+      Timing.wrap "graphml witness" (write_file witness_path (module Task)) (module TaskResult)
     )
 
   let write entrystates =
@@ -595,7 +595,4 @@ struct
       )
       else
         write entrystates
-
-  let write entrystates =
-    Timing.wrap "witness" write entrystates
 end
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
@@ -392,6 +392,9 @@ struct
     ];
 
     yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"))
+
+  let write () =
+    Timing.wrap "yaml witness" write ()
 end
 
 

diff --git a/sv-comp/sv-comp-run-no-overflow.py b/sv-comp/sv-comp-run-no-overflow.py
@@ -13,7 +13,7 @@
 
 OVERVIEW = False # with True Goblint isn't executed
 # TODO: don't hard-code specification
-GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/no-overflow.prp --set witness.path {witness_filename} {code_filename} -v"
+GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/no-overflow.prp --set witness.graphml.path {witness_filename} {code_filename} -v"
 TIMEOUT = 10 # with some int that's Goblint timeout for single execution
 START = 1
 EXIT_ON_ERROR = True

diff --git a/sv-comp/sv-comp-run.py b/sv-comp/sv-comp-run.py
@@ -13,7 +13,7 @@
 
 OVERVIEW = False # with True Goblint isn't executed
 # TODO: don't hard-code specification
-GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/unreach-call-__VERIFIER_error.prp --set witness.path {witness_filename} {code_filename}"
+GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/unreach-call-__VERIFIER_error.prp --set witness.graphml.path {witness_filename} {code_filename}"
 TIMEOUT = 30 # with some int that's Goblint timeout for single execution
 START = 1
 EXIT_ON_ERROR = True

diff --git a/tests/sv-comp/observer/path_nofun_true-unreach-call.c b/tests/sv-comp/observer/path_nofun_true-unreach-call.c
@@ -21,4 +21,4 @@ int main()
     return 0;
 }
 
-// ./goblint --enable ana.sv-comp --enable ana.wp --enable witness.uncil --disable ana.int.def_exc --enable ana.int.interval --set ana.activated '["base"]' --html tests/sv-comp/observer/path_nofun_true-unreach-call.c
+// ./goblint --enable ana.sv-comp --enable ana.wp --enable witness.graphml.uncil --disable ana.int.def_exc --enable ana.int.interval --set ana.activated '["base"]' --html tests/sv-comp/observer/path_nofun_true-unreach-call.c
-Original file line number
+Diff line change
@@ Expand Up / @@ -392,6 +392,9 @@ struct @@
         ];
         yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"))
+      let write () =
+        Timing.wrap "yaml witness" write ()
     end
@@ Expand Down @@