Draft: Fix expected result for weaver benchmarks (verified by deagle, valiated by dartagnan)
This MR fixes some of the benchmarks mentioned in #1313 (closed) for which I was able to confirm that the expected result is wrong.
To make this claim fair, I used independent tools: deagle
as a verifier and dartagnan
as a validator.
I attach the witnesses generated by deagle
; all of them are validated by dartagnan
.
However, the easiest way to check this MR is correct would be to run the chain verifier->validator
using CoVeriTeam
:
../bin/coveriteam validating-verifier.cvt \
--input verifier_path=../actors/deagle.yml \
--input validator_path=../actors/dartagnan-validate-violation-witnesses.yml \
--input program_path=../../sv-benchmarks/c/weaver/popl20-threaded-sum-3.wvr.c \
--input specification_path=../../sv-benchmarks/c/properties/unreach-call.prp \
--data-model ILP32 \
--remote
-------------------------------------------------------------------------
...
Following is the type of the actor validating_verifier:
SEQUENCE :: {'program': 'Program', 'spec': 'Specification'} --> {'verdict': 'Verdict', 'witness': 'Witness'}
Verifier :: deagle :: {'program': 'Program', 'spec': 'Specification'} --> {'verdict': 'Verdict', 'witness': 'Witness'}
ITE :: {'verdict': 'Verdict', 'program': 'Program', 'spec': 'Specification', 'witness': 'Witness'} --> {'verdict': 'Verdict', 'witness': 'Witness'}
Validator :: dartagnan-validate-violation-witnesses :: {'program': 'Program', 'spec': 'Specification', 'witness': 'Witness', 'verdict': 'Verdict'} --> {'verdict': 'Verdict', 'witness': 'Witness'}
None
The following artifacts were produced by the execution:
{'verdict': 'false(unreach-call)', 'witness': }
...
The output produced by the CoVeriTeam program during execution can be found in the directory: cvt-output/6eda5728-60a4-4d97-b30a-83ebcb4834c4
The last line {'verdict': 'false(unreach-call)', 'witness': }
means that the validator was successful in validating the witness. To be precise, this is just the output of the last tool in the chain (here the validator). If you want to see the intermediate results, you need to run find cvt-output/some-random-name
(see the last line of CoVeriTeam
output).