Merge pull request #1521 from goblint/yaml-witness-validate-missing

Nicer SV-COMP result for validator when witness is missing

src/analyses/unassumeAnalysis.ml

@@ -85,7 +85,9 @@ struct
 
     let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with
       | Ok yaml -> yaml
-      | Error (`Msg m) -> failwith ("Yaml_unix.of_file: " ^ m)
+      | Error (`Msg m) ->
+        Logs.error "Yaml_unix.of_file: %s" m;
+        Svcomp.errorwith "witness missing"
     in
     let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in
 

src/framework/control.ml

@@ -357,6 +357,7 @@ struct
     (* real beginning of the [analyze] function *)
     if get_bool "ana.sv-comp.enabled" then
       Witness.init (module FileCfg); (* TODO: move this out of analyze_loop *)
+    YamlWitness.init ();
 
     AnalysisState.global_initialization := true;
     GobConfig.earlyglobs := get_bool "exp.earlyglobs";
@@ -789,15 +790,19 @@ struct
     );
 
     (* Before SV-COMP, so result can depend on YAML witness validation. *)
-    if get_string "witness.yaml.validate" <> "" then (
-      let module YWitness = YamlWitness.Validator (R) in
-      YWitness.validate ()
-    );
+    let yaml_validate_result =
+      if get_string "witness.yaml.validate" <> "" then (
+        let module YWitness = YamlWitness.Validator (R) in
+        Some (YWitness.validate ())
+      )
+      else
+        None
+    in
 
     if get_bool "ana.sv-comp.enabled" then (
       (* SV-COMP and witness generation *)
       let module WResult = Witness.Result (R) in
-      WResult.write entrystates
+      WResult.write yaml_validate_result entrystates
     );
 
     if get_bool "witness.yaml.enabled" then (

src/goblint.ml

@@ -83,6 +83,11 @@ let main () =
     Logs.error "%s" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!"));
     Goblint_timing.teardown_tef ();
     exit 124
+  | Svcomp.Error msg ->
+    do_stats ();
+    Witness.print_svcomp_result ("ERROR (" ^ msg ^ ")");
+    Goblint_timing.teardown_tef ();
+    exit 1
 
 (* We do this since the evaluation order of top-level bindings is not defined, but we want `main` to run after all the other side-effects (e.g. registering analyses/solvers) have happened. *)
 let () = at_exit main

src/witness/svcomp.ml

@@ -60,6 +60,11 @@ struct
     | Unknown -> "unknown"
 end
 
+exception Error of string
+
+let errorwith s = raise (Error s)
+
+
 module type TaskResult =
 sig
   module Arg: MyARG.S

src/witness/witness.ml

@@ -690,25 +690,16 @@ struct
       Timing.wrap "graphml witness" (write_file witness_path (module Task)) (module TaskResult)
     )
 
-  let write entrystates =
+  let write yaml_validate_result entrystates =
     match !AnalysisState.verified with
     | Some false -> print_svcomp_result "ERROR (verify)"
     | _ ->
-      if get_string "witness.yaml.validate" <> "" then (
-        match get_bool "witness.yaml.strict" with
-        | true when !YamlWitness.cnt_error > 0 ->
-          print_svcomp_result "ERROR (witness error)"
-        | true when !YamlWitness.cnt_unsupported > 0 ->
-          print_svcomp_result "ERROR (witness unsupported)"
-        | true when !YamlWitness.cnt_disabled > 0 ->
-          print_svcomp_result "ERROR (witness disabled)"
-        | _ when !YamlWitness.cnt_refuted > 0 ->
-          print_svcomp_result (Result.to_string (False None))
-        | _ when !YamlWitness.cnt_unconfirmed > 0 ->
-          print_svcomp_result (Result.to_string Unknown)
-        | _ ->
-          write entrystates
-      )
-      else
+      match yaml_validate_result with
+      | Some (Stdlib.Error msg) ->
+        print_svcomp_result ("ERROR (" ^ msg ^ ")")
+      | Some (Ok (Svcomp.Result.False _ | Unknown as result)) ->
+        print_svcomp_result (Result.to_string result)
+      | Some (Ok True)
+      | None ->
         write entrystates
 end

src/witness/yamlWitness.ml

@@ -514,6 +514,15 @@ struct
     Timing.wrap "yaml witness" write ()
 end
 
+let init () =
+  match GobConfig.get_string "witness.yaml.validate" with
+  | "" -> ()
+  | path ->
+    (* Check witness existence before doing the analysis. *)
+    if not (Sys.file_exists path) then (
+      Logs.error "witness.yaml.validate: %s not found" path;
+      Svcomp.errorwith "witness missing"
+    )
 
 module ValidationResult =
 struct
@@ -581,7 +590,9 @@ struct
 
     let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.validate")) with
       | Ok yaml -> yaml
-      | Error (`Msg m) -> failwith ("Yaml_unix.of_file: " ^ m)
+      | Error (`Msg m) ->
+        Logs.error "Yaml_unix.of_file: %s" m;
+        Svcomp.errorwith "witness missing"
     in
     let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in
 
@@ -840,5 +851,19 @@ struct
 
     let certificate_path = GobConfig.get_string "witness.yaml.certificate" in
     if certificate_path <> "" then
-      yaml_entries_to_file (List.rev yaml_entries') (Fpath.v certificate_path)
+      yaml_entries_to_file (List.rev yaml_entries') (Fpath.v certificate_path);
+
+    match GobConfig.get_bool "witness.yaml.strict" with
+    | true when !cnt_error > 0 ->
+      Error "witness error"
+    | true when !cnt_unsupported > 0 ->
+      Error "witness unsupported"
+    | true when !cnt_disabled > 0 ->
+      Error "witness disabled"
+    | _ when !cnt_refuted > 0 ->
+      Ok (Svcomp.Result.False None)
+    | _ when !cnt_unconfirmed > 0 ->
+      Ok Unknown
+    | _ ->
+      Ok True
 end