Enable regression tests of weak memory model instrumentation #5937
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
tautschnig
force-pushed
the
wmm-tests
branch
8 times, most recently
from
abc0896 to
f4499e3
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5937 +/- ##
===========================================
+ Coverage 74.23% 75.01% +0.77%
===========================================
Files 1431 1431
Lines 155291 155294 +3
===========================================
+ Hits 115287 116499 +1212
+ Misses 40004 38795 -1209
Continue to review full report at Codecov.
|
martin-cs
approved these changes
Mar 18, 2021
I'll create a separate PR for this. |
Store the elements to be removed in a set until after the iteration is done, and then remove the chosen elements. The more standard approach could be returning the iterator to the next element in the remove-an-element function, but this requires larger changes here. Thus keeping it small and simple for now.
These regression tests are a selected subset (cf. README.txt) of the full set of available tests (stored in goto-instrument-wmm-full.tgz), and will ensure basic testing of the functionality implemented in goto-instrument. Test specifications were updated to work with current infrastructure.
Make all regression tests from the archive available (yet marking them as
THOROUGH or KNOWNBUG to avoid including them by default). This avoids having an
unused archive file bit-rotting in the repository. This commit was generated as
follows:
```
set -e
cd regression/goto-instrument-wmm-core/
tar xzf ../goto-instrument-wmm-full.tgz --strip-components=1
for f in $(tar tzf ../goto-instrument-wmm-full.tgz | sed 's#^goto-instrument-wmm-full/##')
do
[ -f $f ] || continue
if git status --porcelain $f | grep -q '^?'
then
if [[ $(basename $f) == "test.desc" ]]
then
sed -i '1s/^CORE$/THOROUGH/' $f
if ! grep -q EXIT $f
then
if grep -q "VERIFICATION FAILED" $f
then
sed -i '/SIGNAL=0/ i ^EXIT=10$' $f
else
sed -i '/SIGNAL=0/ i ^EXIT=0$' $f
fi
fi
elif [[ $f =~ \.c$ ]]
then
clang-format -i $f
fi
git add $f
else
git checkout -- $f
fi
done
git rm ../goto-instrument-wmm-full.tgz
git commit -F - <<EOF
Add regression tests from goto-instrument-wmm-full.tgz
Make all regression tests from the archive available (yet marking them as
THOROUGH or KNOWNBUG to avoid including them by default). This avoids having an
unused archive file bit-rotting in the repository. This commit was generated as
follows:
\`\`\`
$(<../../script.sh)
\`\`\`
EOF
```
Tag all *_OPT tests "glpk" and exclude them from test runs by default as we don't currently build with glpk by default.
Some of the tests that were previously imported as THOROUGH from the tar archive actually are failing and require further investigation.
These tests currently pass and each of them completes in under 1 second.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
These regression tests are a selected subset (cf. README.txt) of the
full set of available tests (stored in goto-instrument-wmm-full.tgz),
and will ensure basic testing of the functionality implemented in
goto-instrument.