Skip to content

Draft: Fix expected result for weaver benchmarks (verified by deagle, valiated by dartagnan)

Hernan Ponce de Leon requested to merge 1313 into main

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

witnesses.zip

Edited by Hernan Ponce de Leon

Merge request reports