Skip to content

Test gen strings update regression #976

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jun 5, 2017
Merged

Test gen strings update regression #976

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
86de08f
Update strings-smoke-test
romainbrenguier Mar 7, 2017
56800d5
Add strings-smoke-tests to regression Makefile
Apr 20, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions regression/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ DIRS = ansi-c \
goto-analyzer \
goto-instrument \
goto-instrument-typedef \
strings-smoke-tests \
test-script \
# Empty last line

Expand Down
35 changes: 32 additions & 3 deletions regression/strings-smoke-tests/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,38 @@
default: tests.log

test:
@../test.pl -c ../../../src/cbmc/cbmc
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
../failed-tests-printer.pl ; \
exit 1 ; \
fi

testfuture:
@../test.pl -c ../../../src/cbmc/cbmc -CF
@if ! ../test.pl -c ../../../src/cbmc/cbmc -CF ; then \
../failed-tests-printer.pl ; \
exit 1 ; \
fi

testall:
@../test.pl -c ../../../src/cbmc/cbmc -CFTK
@if ! ../test.pl -c ../../../src/cbmc/cbmc -CFTK ; then \
../failed-tests-printer.pl ; \
exit 1 ; \
fi

tests.log: ../test.pl
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
../failed-tests-printer.pl ; \
exit 1 ; \
fi

show:
@for dir in *; do \
if [ -d "$$dir" ]; then \
vim -o "$$dir/*.c" "$$dir/*.out"; \
fi; \
done;

clean:
find -name '*.out' -execdir $(RM) '{}' \;
find -name '*.gb' -execdir $(RM) '{}' \;
$(RM) tests.log

2 changes: 1 addition & 1 deletion regression/strings-smoke-tests/java_append_int/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
FUTURE
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry don't know anything but how come this is being marked as Future? Is there a corresponding issue to re-enable it?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These tests have never actually been enabled, because the test suite was not called from the regression/Makefile. For this one in particular, the behaviour might be affected when we add models for strings. It is just easier to go through all these tests once everything is merged, then enable those that work, and create issues for those that don't. There is no particular issue to enable the tests, but it is an ongoing process.

test_append_int.class
--refine-strings
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this and others have the --string-max-length 100 added as well?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I understand that --string-max-length something will become the default on test-gen. However, on cbmc itself, the option should not be necessary (because we do not need to create real counterexamples). If anything, the option should be removed in the test descriptions where it is present, but that is not a priority I think.

^EXIT=0$
Expand Down
5 changes: 2 additions & 3 deletions regression/strings-smoke-tests/java_contains/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,8 @@
KNOWNBUG
CORE
test_contains.class
--refine-strings
^EXIT=10$
^EXIT=0$
^SIGNAL=0$
^\[.*assertion.1\].* line 8.* SUCCESS$
^\[.*assertion.2\].* line 9.* FAILURE$
--
Issue: diffblue/test-gen#201
Binary file modified regression/strings-smoke-tests/java_contains/test_contains.class
View file
Open in desktop
Binary file not shown.
3 changes: 2 additions & 1 deletion regression/strings-smoke-tests/java_contains/test_contains.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ public static void main(/*String[] argv*/)
String u = "bc";
String t = "ab";
assert(s.contains(u));
assert(s.contains(t));
// Long version:
// assert(s.contains(t));
}
}
2 changes: 1 addition & 1 deletion regression/strings-smoke-tests/java_endswith/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
test_endswith.class
--refine-strings
--refine-strings --string-max-length 100
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 9.* SUCCESS$
Expand Down
2 changes: 1 addition & 1 deletion regression/strings-smoke-tests/java_float/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
FUTURE
test_float.class
--refine-strings
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/strings-smoke-tests/java_insert_int/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE
FUTURE
test_insert_int.class
--refine-strings
^EXIT=0$
Expand Down
34 changes: 34 additions & 0 deletions regression/strings-smoke-tests/performance.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
#!/usr/bin/python

'''
This script collects the running times of the tests present in the current
directory.

It does not run the tests but reads the already present output files.

Usage:
python performance.py

Dependencies:
gnuplot http://www.gnuplot.info/
'''

import time
from subprocess import check_output
from subprocess import check_call

git_output = check_output(['git', 'show', 'HEAD'])
commit = git_output.split('\n')[0]
commit_id = time.strftime('%Y_%m_%d__%H_%M_%S')+'__'+commit[7:]

process = check_output(['grep', '^Runtime decision procedure', '-R'])
Copy link
Contributor

@smowton smowton Jun 5, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's no point reading the output into a Python string then writing it back out again-- change this to something like:

file_name = 'performance_'+commit_id+'.out'
print 'writing to file', file_name
with open(file_name, 'w') as f:
  check_call(['grep', '^Runtime decision procedure', '-R'], stdout=f)

Otherwise lgtm

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@smowton As suggested above, this doesn't work because we cannot write the output of a grep in the directory we are currently grepping. I get the following error:

writing to file performance_2017_06_05__14_53_24__56800d52eca33b06978f8863f333ef43fbabc6c3.out
grep: input file 'performance_2017_06_05__14_53_24__56800d52eca33b06978f8863f333ef43fbabc6c3.out’ is also the output
Traceback (most recent call last):
  File "performance.py", line 29, in <module>
    check_call(['grep', '^Runtime decision procedure', '-R'], stdout=f)
  File "/usr/lib/python2.7/subprocess.py", line 541, in check_call
    raise CalledProcessError(retcode, cmd)
subprocess.CalledProcessError: Command '['grep', '^Runtime decision procedure', '-R']' returned non-zero exit status 2

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, makes sense

file_name = 'performance_'+commit_id+'.out'

print 'writing to file', file_name
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you're fixing this, doesn't this also need the comment here: #976 (comment)

(i.e. print('writing to file ' + file_name)


with open(file_name, 'w') as f:
f.write(process)

print('drawing to file', file_name+'.png')
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This still using the comma/python2 thing so if you agree I think this should become:

print('drawing to file '+file_name+'.png')

check_call(['gnuplot', '-e', 'file="'+file_name+'"', '-e',
'outputfile="'+file_name+'.png"', 'performance_draw.gp'])
7 changes: 7 additions & 0 deletions regression/strings-smoke-tests/performance_draw.gp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
set datafile separator ":"
set term png
set output outputfile
set logscale y 10
set yrange [0.01:100]

plot file using 3 with lines
2 changes: 1 addition & 1 deletion regression/strings/StringValueOf08/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
FUTURE
StringValueOf08.class
--refine-strings
--refine-strings --string-max-length 100
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Expand Down