From 06086c646285037bcb242dc70705fbaa690e8ebd Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 20 Jun 2024 17:55:07 +0300 Subject: [PATCH 1/4] Refactor YAML witness validation result passing --- src/framework/control.ml | 14 +++++++++----- src/witness/witness.ml | 25 ++++++++----------------- src/witness/yamlWitness.ml | 16 +++++++++++++++- 3 files changed, 32 insertions(+), 23 deletions(-) diff --git a/src/framework/control.ml b/src/framework/control.ml index 05fad90caf..bb1d7bab58 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -789,15 +789,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 ( diff --git a/src/witness/witness.ml b/src/witness/witness.ml index fb88c2ce7b..651e7a76d5 100644 --- a/src/witness/witness.ml +++ b/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 (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 diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 42254f30de..71bb75afef 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -840,5 +840,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 From bc3fac895299e7b96ad8ac216d446bc6751a831c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 25 Jun 2024 11:51:07 +0300 Subject: [PATCH 2/4] Add witness missing verdict to YAML witness validation Better than "EXCEPTION (Failure)" as verdict. --- src/goblint.ml | 5 +++++ src/witness/svcomp.ml | 5 +++++ src/witness/witness.ml | 2 +- src/witness/yamlWitness.ml | 4 +++- 4 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/goblint.ml b/src/goblint.ml index a687badb8e..52b9bbdfc0 100644 --- a/src/goblint.ml +++ b/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 diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index bb887e6cb1..59a8f01b40 100644 --- a/src/witness/svcomp.ml +++ b/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 diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 651e7a76d5..7b0213b601 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -695,7 +695,7 @@ struct | Some false -> print_svcomp_result "ERROR (verify)" | _ -> match yaml_validate_result with - | Some (Error msg) -> + | Some (Stdlib.Error msg) -> print_svcomp_result ("ERROR (" ^ msg ^ ")") | Some (Ok (Svcomp.Result.False _ | Unknown as result)) -> print_svcomp_result (Result.to_string result) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 71bb75afef..bb91e195ef 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -581,7 +581,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 From 9fd0fd5bd3dcb7b22d200e4f655535789d846d51 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 25 Jun 2024 11:59:00 +0300 Subject: [PATCH 3/4] Add witness missing verdict to YAML witness unassume Better than "EXCEPTION (Failure)" as verdict. --- src/analyses/unassumeAnalysis.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 265e9c6925..85b33edc79 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/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 From 85ab1fdc9edddf65a8f1a6c8bae74c1a417859f0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 25 Jun 2024 12:09:46 +0300 Subject: [PATCH 4/4] Check YAML witness existence before analysis --- src/framework/control.ml | 1 + src/witness/yamlWitness.ml | 9 +++++++++ 2 files changed, 10 insertions(+) diff --git a/src/framework/control.ml b/src/framework/control.ml index bb1d7bab58..5e92282210 100644 --- a/src/framework/control.ml +++ b/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"; diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index bb91e195ef..7134211d32 100644 --- a/src/witness/yamlWitness.ml +++ b/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