Commit 36636e2e authored by Martin Spiessl's avatar Martin Spiessl

Merge branch 'bugfixes' into 'master'

Bugfixes

See merge request !1
parents 91a37d09 e3e058aa
# MetaVal - a Meta-Validator for Verification Witnesses
# MetaVal: A Meta-Validator for Verification Witnesses
MetaVal takes as input a program and a witness and reduces the task of validating the witness into a verification task.
For the transformation, CPAchecker is used as a frontend.
MetaVal takes as input a program, a specification, and a witness, and reduces the task of witness-based result validation to an ordinary verification task.
For the reduction, CPAchecker is used as program transformer.
At the backend, an arbitrary verifier can be used as long as it understands the specification format of SV-COMP.
As verification backend, any standard verifier can be used as long as it understands the specification format of SV-COMP.
## Execute using BenchExec
MetaVal is most conveniently called via BenchExec.
In your benchmark definition, all you have to do is to specify the following options:
The benchmark definition needs to specify the following options:
--metavalVerifierBackend
--metavalWitness
these are then filtered by benchexec's tool-info module and not actually passed to metaval.sh
These are then filtered by BenchExec's tool-info module and not actually passed to metaval.sh.
Example snippet from the SV-COMP task definition:
<option name="--metavalWitness">../../results-verified/LOGDIR/${rundefinition_name}.${taskdef_name}/witness.graphml</option>
<option name="--metavalVerifierBackend">cpachecker</option>
The currently supported backends are:
The currently supported verification backends are:
- cpachecker-metaval: use the CPAchecker version that is also used in the frontend
- cpachecker: use the CPAchecker version from the submission CPA-Seq of SV-COMP'2019
- symbiotic: use the Symbiotic version from the submission of SV-COMP'2019
- yogar-cbmc: use the Yogar-CBMC version from the submission of SV-COMP'2019
- ultimateautomizer: use the Ultimate Automizer version from the submission of SV-COMP'2019
- cpachecker-metaval: use the CPAchecker version that is also used as program transformer
- cpachecker: use the CPAchecker version from the submission CPA-Seq to SV-COMP'2019
- symbiotic: use the Symbiotic version from the submission to SV-COMP'2019
- yogar-cbmc: use the Yogar-CBMC version from the submission to SV-COMP'2019
- ultimateautomizer: use the Ultimate version from the submission UAutomizer to SV-COMP'2019
## Execute metaval.sh directly
If you want to call metaval directly, you can do so with the following syntax:
To call MetaVal directly, the following syntax can be used:
metaval.sh --witness path/to/witness --verifier nameOfVerifier -- $BACKENDVERIFIERCMD
$BACKENDVERIFIERCMD is the command with which you would normally call the backend verifier, assuming that you are in its directory.
You will also have to use ../output/ARG.c instead of the path to the original program from the task, since metaval will create the reduced program there.
$BACKENDVERIFIERCMD is the command with which the backend verifier would normally be called, assuming its directory as working directory.
The file ../output/ARG.c has to be used instead of the original program from the verification task, since MetaVal will create the reduced program there.
Example for using CPAchecker as verifier backend:
Example for using CPAchecker as verification backend:
./metaval.sh --verifier 'CPAchecker-1.7-svn 29852-unix' --witness witness.graphml \
../sv-benchmarks/c/bitvector/jain_1-1.c -- scripts/cpa.sh -predicateAnalysis-PredAbsRefiner-ABEl \
......
#!/bin/bash
if [ -f metaval.zip ]
then
rm metaval.zip
......
......@@ -2,7 +2,7 @@
set -e
count=0
name=""
VERSION="0.1.4"
VERSION="0.1.8"
if [ "$1" == "--version" ]
then
......@@ -25,7 +25,7 @@ shift
if [ "$1" != "--witness" ]
then
echo "expected a witness as seconf option, but got $1"
echo "expected a witness as second option, but got $1"
exit 1
fi
......@@ -74,11 +74,23 @@ echo "task is $name"
echo "generating residual program from task and witness"
CPAchecker/scripts/cpa.sh -witness2reach -spec $witness $name -setprop witness.useInvariantsAsAssumptions=true -setprop witness.checkInvariantViolations=true -setprop cpa.arg.export.code.header=false -setprop witness.checkProgramHash=false 1>/dev/null
echo $TRANSFORMERCMD
TRANSFORMERCMD="CPAchecker/scripts/cpa.sh -witness2reach -spec $witness $name -setprop witness.useInvariantsAsAssumptions=true -setprop witness.checkInvariantViolations=true -setprop cpa.arg.export.code.header=false -setprop witness.strictChecking=false -setprop witness.checkProgramHash=false"
ARCHITECTUREWARNING="Invalid configuration (Cannot parse witness: The architecture assumed for the given verification-task differs from the architecture assumed by the witness."
echo $TRANSFORMERCMD
# temporary workaround for the architecture (it is irrelevant for the transformation step, but CPAchecker still complains if it does not match).
if eval $TRANSFORMERCMD 2>&1 1>/dev/null | \
sed --expression="s|Error: $ARCHITECTUREWARNING|$ARCHITECTUREWARNING|g" | \
perl -pe "print STDERR $_;" | grep -q "$ARCHITECTUREWARNING" ; then
echo "architecture mismatch detected. This is irrelevant for program transformation, retrying with 64 bit:"
$TRANSFORMERCMD -64 1>/dev/null
fi
echo "starting validation"
cd "$verifier"
echo "$verifier"
echo $(pwd)
echo "$@"
exec $@
exec "$@" | sed --expression='s|__VERIFIER_error(); called in|unreach-call: __VERIFIER_error(); called in|g'
# sed is called to work around the fact that CPAchecker from SV-COMP'19 does not get handled properly by newer BenchExec versions
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment