Update all validators to handle Validation tasks

[marian-lingsch]

The goal of this PR is to add support for validation tasks, whose format is described in: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1572

The goal is to make every validator be able to handle this tasks in time for SV-COMP25. This was discussed in the SV-COMP community meeting on the 2024-10-22 under point 6, see: https://docs.google.com/document/d/1A-GSaImjWSMbspERfOVAInmsjw3_tkIuAcHshn98Ro8/edit?tab=t.0#heading=h.3q9vj3p8sr3g

This PR implements the support for all validators, by creating some helper functions and adjusting all tool info modules of current validators to handle the new validation task definition files.

More concretely, given a validation task definition files such as the one below, what a validator needs to do is separate the witness file from other input files and use handle each of these two separate types of input files accordingly.

format_version: '2.0'

input_files: 
  - '../linear-inequality-inv-a.c'
  - 'linear-inequality-inv-a.1.witness-2.0.yml'

properties:
  - property_file: ../../properties/unreach-call.prp
    expected_verdict: false

options:
  language: C
  data_model: ILP32
  witness: 'linear-inequality-inv-a.1.witness-2.0.yml'

To remain backwards compatible with the previous usage of validators, we consider four possible cases:

	Normal Task Definition File	Witness Task Definition File
Validator Witness passing option is set (e.g. --witness present)	Command line is build as before	Exception (Two witnesses)
Validator Witness passing option is unsert (e.g. --witness not present)	Exception (No witness)	Add the witness option set to the witness to the command line

[marian-lingsch]

For testing these changes I used the scripts and examples contained here:
test-validators.zip

Unpacking this in a BenchExec clone will allow you to run all make targets called toolname which will download the tool and run the tool on the benchmark xml with the targets run-toolname

[PhilippWendler]

The code is fine for me now, thanks!

However, I would still prefer if someone independent has a quick look at all the tool-info modules and compares the old and new code to check whether for example the correct enum value is passed, whether the options are inserted correctly, and whether the input files are taken correctly from the result of the new function. The reviewer would not need to be familiar with the existing code nor would they need to look at the code of sv_benchmarks_utils.py. I don't think it is much effort, I just prefer to not do it myself because I think it is likely that people involved in writing such code will easily overlook mistakes.

[dbeyer]

Dear All, Many thanks for the great work done here.
I am now designing and considering the changes to the rest of the competition infrastructure,
including the category structure, the CI checks, and the scoring schema in SV-COMP.
I would like to ask you to wait with merging until I am done with the design of the rest of the components.

[PhilippWendler]

This PR depends on the format in https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1572, so unless that is accepted it should not be merged anyway.

[PhilippWendler]

@marian-lingsch Did you find a reviewer for #1093 (comment) already?

[PhilippWendler]

What is the URL for the description of this witness key and how it is supposed to be used? We should add the link to the docs of handle_witness_of_task.

[marian-lingsch]

@marian-lingsch Did you find a reviewer for #1093 (comment) already?

I saw that @sim642 and @danieldietsch did some pass over the files, but will look for someone to do a full review

[marian-lingsch]

What is the URL for the description of this witness key and how it is supposed to be used? We should add the link to the docs of handle_witness_of_task.

Thanks for pointing this out!

Addressed in b550e76