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/1592 and https://gitlab.com/sosy-lab/benchmarking/task-definition-format/-/merge_requests/3

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.1'

additional_information:
  task_type: validation
  verification:
    - property_file: ../../properties/unreach-call.prp
      expected_verdict: true


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_input_file: '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	validation task file
Validator Witness passing option is set (e.g. --witness present)	Command line is build as before	Witness passed with the option is used and a warning is given about the ignored witness
Validator Witness passing option is unset (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]

@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

[matthiaskettl]

I went over the changes and could not find any inconsistencies.

[marian-lingsch]

I went over the changes and could not find any inconsistencies.

Thanks a lot @PhilippWendler this should take care of #1093 (comment) right?

[PhilippWendler]

I went over the changes and could not find any inconsistencies.

Thanks a lot @PhilippWendler this should take care of #1093 (comment) right?

Thanks @matthiaskettl, yes.

[dbeyer]

@marian-lingsch Could you please update the format of the witness in the description? It currently does not match version 2.1.
(Once you are at it, please also fix 'unsert' and use 'validation task file' instead of 'witness task-definition file' (mind the hyphen).)

[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.

This is finished now and I believe all necessary changes are made (in MRs so far).

[dbeyer]

@marian-lingsch Also, the description of the action in the table "Exception (Two witnesses)" should be adjusted to the implementation: "witness in task definition ignored".

[marian-lingsch]

@marian-lingsch Could you please update the format of the witness in the description? It currently does not match version 2.1. (Once you are at it, please also fix 'unsert' and use 'validation task file' instead of 'witness task-definition file' (mind the hyphen).)

@dbeyer many thanks for catching the inconsistency in the description. This was left over from the previous validation task file format. Has been updated.