TG-945 Add default platform arguments and benchmarking to the perl script #1458

LAJW · 2017-10-10T12:29:38Z

Perl script replaces $PLATFORM string with platform arguments (which are stored in a string in the perl script itself).
Perl script benchmarks each successful test.

The latter change is non-essential, but would help us keep our CORE/THOROUGH tests in check. Right now there are some CORE tests that are running slowly and some THOROUGH tests that are not. Given how many regression tests we have, it's fairly difficult to tell which ones are the slow ones and which no longer should be marked as THOROUGH.

Fixes issue: https://diffblue.atlassian.net/browse/TG-945

martin-cs · 2017-10-10T12:34:40Z

Have I got the wrong end of the stick or is this removing the ability to fix platform options at run time and then hard coding them to a particular value?

LAJW · 2017-10-10T12:34:53Z

@allredj @smowton @thk123 Please review, as it touches perl script and alters the test output.

LAJW · 2017-10-10T12:36:42Z

@martin-cs Quite the contrary. Every single test right now has hard-coded values. This would let us create new tests that would be run with platform arguments.

I'm creating another PR on test-gen that does just that - adds additional .desc files with $PLATFORM in place of old arguments.

martin-cs · 2017-10-10T12:37:19Z

The times also won't necessarily be stable so you won't be able to diff the output of the script any more. I don't know if anyone does this but it sounds like the kind of thing you might want to do.

LAJW · 2017-10-10T12:39:17Z

I do in fact, so I've put the benchmark info after [OK] so I can discard anything after the opening bracket.

martin-cs · 2017-10-10T12:41:04Z

Will there be a way of setting an option for all regressions to use without editing test.pl?

LAJW · 2017-10-10T12:43:38Z

I wanted to pass them as an extra argument to the perl script or get them from the platform JSON file (which could be copy-pasted/linked from platform repository). @allredj insisted that they should be either stored in a text file in the same directory as the perl script or as they are now - within the perl file. I don't need convincing that this should be implemented differently.

tautschnig

Please go back to the drawing board. The options now hardwired into a script are not portable across tools, and neither across benchmarks. If you want to put them in a single file, create a wrapper around cbmc (as is done with, e.g., goto-instrument).

allredj · 2017-10-10T13:31:32Z

@martin-cs @tautschnig Thanks for you comments which are perfectly valid. In hindsight it's not a great idea to have some test-gen-specific code in test.pl, so we'll do it differently.

tautschnig · 2017-10-10T15:38:26Z

regression/test.pl

@@ -227,6 +228,8 @@ ($$$$)
  -T         thorough: run expensive tests
  -F         future: run checks for future features
  -K         known: run tests associated with known bugs
+  -P         platform: list of arguments which replaces the \$PLATFORM string
+             in .desc files


What is the difference between test.pl -c cbmc -P bla and test.pl -c "cbmc bla" ?

The former is only applied to specific tests, the latter to all tests.
I don't want to break any existing tests, I just want to provide an option to create new tests with standardised parameter set.

Indeed I was wrong to conflate the two approaches; what I continue to struggle with is 1) the name PLATFORM and 2) how to document what good, common values are. My assumption would be that over time you will want a $PLATFORM1, $PLATFORM2, etc.

I honestly struggle to find a better name. "defaults" or "common" would be misleading, as one would assume that those arguments would be added to all tests. Merged with existing ones.

We don't foresee adding extra $PLATFORMs, as there's a singular "platform" we're considering.

I am running the risk of being very narrow-minded, hence the following is a serious question: isn't a "platform" more commonly an operating system, a particular hardware, or the combination of those? It might be just about changing this to PLATFORM_OPTS for clarity.

If you are talking about a single $PLATFORM, are just really just introducing a shorthand to save some typing?

LAJW · 2017-10-16T10:00:05Z

Re-requesting review (platform arguments have been moved out of the perl script).

smowton · 2017-10-16T10:14:06Z

How hard would it be to allow arbitrary -DNAME=val style parameterisation? Surely we'll quickly want to do PLATFORM2, PLATFORM3, ...

LAJW · 2017-10-16T10:19:26Z

How hard would it be to allow arbitrary -DNAME=val style parameterisation? Surely we'll quickly want to do PLATFORM2, PLATFORM3, ...

@smowton Hard enough. I'd have to roll a custom command line parser. The one employed here, expects a set of keys to be provided before it starts parsing. Besides I'm not a fan of over-engineering. This feature is not going to be used in a very far foreseeable future, but should we need another $argument, we will start worrying about it then.

smowton · 2017-10-16T10:21:29Z

OK then I guess my worst criticism is this is "a bit gross", but it's the test script, no big deal.

tautschnig · 2017-10-16T13:05:25Z

I'm fine with the time measurement changes. The $PLATFORM remains a hack to me and I just don't see why what is being argued as a single use case should yield changes in a test script. If you're trying to solve a local problem, solve it locally.

allredj · 2017-10-17T08:03:06Z

I don't really see the problem with that solution, as it adds a simple option that is very useful for everyone using the perl script in the context of diffblue and doesn't change anything for the people who do not want to use it.

We've lost too much time on this minor fix already. Would everyone be happier with a wrapper around test-generator that seded $PLATFORM toward the actual platform arguments?

tautschnig · 2017-10-17T09:00:27Z

I don't really see the problem with that solution, as it adds a simple option that is very useful for everyone [...]

I strongly disagree with your use of "everyone":

As has been highlighted by @smowton and myself, if that were the case, then surely you'd want sets $PLATFORM1, $PLATFORM2, etc.
With that change, people might start adding $PLATFORM to test.desc files, but only a closed group of people will know what value to use, hence others are precluded from even executing those same tests.

Quite frankly, I don't see any advantage over just putting your preferred set of options in the respective test.desc files. If you feel like changing that fixed set, use sed -i or perl -p -i -e and be happy.

LAJW · 2017-10-17T09:11:23Z

@tautschnig

If you feel like changing that fixed set, use sed -i or perl -p -i -e and be happy.

With 3000 regression tests and counting, each with different set of core arguments, that are test-specific and each with different CORE/THOROUGH/FUTURE/KNOWNBUG tag. That doesn't sound like a sensible solution.

tautschnig · 2017-10-17T09:17:41Z

With 3000 regression tests and counting, each with different set of core arguments, that are test-specific and each with different CORE/THOROUGH/FUTURE/KNOWNBUG tag. That doesn't sound like a sensible solution.

If they truly have test-specific arguments, then a single $PLATFORM isn't a solution either.

If they are the same, then find . -name "*.desc" -exec perl -p -i -e 's/.../.../' is your friend as you will surely be aware.

LAJW · 2017-10-17T09:24:56Z

No. The test-specific arguments are about specifying --function or --property flags and running tests in either C or Java and those general test markers. That bash script would have to be really complicated, understand different types of CBMC/test-gen arguments.

Everything else (--string-max-length, --java-assume-inputs-non-null, etc.) should be universal.

tautschnig · 2017-10-17T10:01:07Z

Everything else (--string-max-length, --java-assume-inputs-non-null, etc.) should be universal.

Would you have a number for how many regression (!) tests should actually be using this "universal" set of options? I was assuming that you would just insert the very same sequence of options in all their test.desc files, at which point you could always replace that one, fixed sequence of options by something else. As we are talking about regression tests, either the options you are talking about should really be the defaults with their respective tools, or these aren't actually regression tests.

romainbrenguier · 2017-10-17T10:09:21Z

@tautschnig

either the options you are talking about should really be the defaults with their respective tools, or these aren't actually regression tests.

Most of these aren't actually regression tests.

tautschnig · 2017-10-17T10:22:27Z

Most of these aren't actually regression tests.

What are we talking about then?

romainbrenguier · 2017-10-17T10:26:51Z

What are we talking about then?

Tests

LAJW · 2017-10-17T10:30:54Z

@tautschnig OK, I've found a way to somewhat implement @smowton's approach. Now you can "define" arguments by providing -d flag in a following way:

test.pl -d "PLATFORM=--string-max-length ..."

Hope this meets your standards.

tautschnig · 2017-10-17T10:39:15Z

Tests

What kind of "tests"?

As far as I can tell, we are discussing changes to the file "regression/test.pl". By definition, the files this is to be run on are regression tests. As a side note, last I heard execution time on Travis was a problem. If you are implying we might be running anything other than regression tests (well, unit tests are arguably being run as well), then there is a problem. See #1492 for another form of testing.

tautschnig · 2017-10-17T10:43:34Z

@LAJW not withstanding the discussion that's arising on "what are we actually doing here": I do like your proposal. It does leave the question of "what are sensible/not useful values for PLATFORM" open, but we would get out of that works-for-me-only rabbit hole.

allredj · 2017-10-20T11:43:32Z

@tautschnig what do you think of @LAJW's last proposal? I still believe this could be useful for anyone that uses a set of cbmc options recurrently, so instead of repeating them in the test descriptions, they can just be passed once to the caller of the test script and replace any template that they have in their test descriptors. That is not even specific to test-gen or cbmc, but can be used on everything we use test.pl on.

One advantage of this small enhancement is that this set of options can be easily updated in one place when necessary (i.e. where the script is called).

Another advantage is that we can have some test descriptions that uses the templates, some that don't, which makes it more flexible than a manual sed over all test descriptions (though arguably there are workarounds that would make the sed solution feasible, but it is not really practical).

I've looked at the "wrapper around test-gen" solution but it's not that straightforward, as it would require to make a separate target test-gen executable and we would have to do some alterations in our cmake builds.

Please give me your thoughts.

tautschnig · 2017-10-20T11:49:35Z

@tautschnig what do you think of @LAJW's last proposal? [...]

As I have said above, I do like it! I just thought I'd comment in more detail once the implementation is out, but also I'm happy to say more beforehand. I think the only question that remains is how to document sensible values for any such parameter, but likely that should be done in commit messages or, in fact better: in the comments section of the respective test.desc file. Certainly, none of my worries about this being a very limited solution apply anymore. It's just about getting the documentation/procedures right.

LAJW · 2017-10-23T10:19:41Z

@tautschnig The version with modifiable key is online, please comment.

allredj · 2017-10-26T08:18:48Z

Hi @tautschnig! Do you have any feedback to give on this change? Thanks!

smowton · 2017-10-27T09:59:24Z

One thing -- if there's a $XYZ in a test.desc and XYZ is not specified, we should either warn and replace with empty string or else die complaining that needed definitions were not supplied.

LAJW · 2017-10-27T10:52:54Z

@smowton Updated - script warns if -D option is provided and there are words in the options string that start with a $.

smowton · 2017-10-27T11:11:57Z

Should accept multiple -D
Should warn about unsubbed tokens, not the key I did specify

allredj · 2017-10-27T11:20:50Z

regression/test.pl

+    my $value = substr($definition, $equal_sign + 1);
+    $options =~ s/\$$key/$value/g;
+    if (index($options, " \$") != -1 || (substr($options, 0, 1) cmp '$') == 0) {
+      print "\n  Warning: Key \"$key\" not found\n";


Could the message rather be:
Warning: a '$' symbol has been found in the arguments but no corresponding '-D' option exists?

LAJW · 2017-10-27T14:05:52Z

@allredj @smowton Warnings now warn about unexpected keys in the .desc file and perl script accepts multiple -D arguments.

smowton

Looks good, suggest only improving the error to:

path/file.desc: variable $abc not replaced; consider passing -Dabc=...

allredj

LGTM. Needs squashing before merge.

allredj · 2017-10-27T17:11:14Z

regression/test.pl

+  if (scalar @keys) {
+    foreach my $word (split(/\s/, $options)) {
+      if ((substr($word, 0, 1) cmp '$') == 0) {
+        print "\n  Warning: Key \"$word\" not replaced\n";


I still think the message should mention the -D option, otherwise a user not aware of that option will wonder why the script is complaining on $. But that's a non-blocking comment (and the only one).

LAJW · 2017-10-30T10:15:55Z

Updated the warning message, as requested by @smowton and @allredj. Squashed. To be merged by @romainbrenguier.

4820601 Merge remote-tracking branch 'diffblue/develop' into merge-dev-to-ss 278f309 Merge pull request diffblue#1526 from reuk/reuk/fixup-unified-diff 69ba9e7 Merge pull request diffblue#1546 from smowton/smowton/feature/expose_tarjan 05dc65c Use lower-case characters to start error messages 8d0b23b Change asserts to invariants a7afc6c Return from get_diff by value 6833af6 Fix formatting 4555d9f Remove unused parameter e32c6c5 Make instructions_equal static f815cc0 Move instructions_equal definition 11c9acc Add getter for data member 8c35211 Make data member private f54db47 Rename differences map data member b67d6e8 Merge pull request diffblue#1543 from chrisr-diffblue/cleanup/add-java-array-element-type-helper c9241cd Make generic Tarjan's algorithm publically available ebabdb9 Merge pull request diffblue#1542 from smowton/smowton/cleanup/sharing-node-assertion a523d6f Add a helper function for accessing the element type of a Java array type d8e8a68 Use INVARIANT rather than assert for sharing-node assertions 64d5dd2 Merge pull request diffblue#1538 from smowton/smowton/cleanup/remove-returns-asserts-to-invariants fca7c04 Merge pull request diffblue#1537 from smowton/smowton/cleanup/sharing-node-test-to-catch e35372a Merge pull request diffblue#1539 from romainbrenguier/bugfix/char-array-in-java-strings#TG-58#newpr 4d011b5 Merge pull request diffblue#1541 from owen-jones-diffblue/replace-unsigned-with-number-type b2a4e39 Merge pull request diffblue#1540 from owen-jones-diffblue/rename-detach 2f6ceed Replace unsigned with appropriate type 938ab2b Replace 'detatch' with 'detach' c219663 Convert sharing-node test to run under Catch dec5ddf Remove-returns: asserts -> invariants 3b1f485 Merge pull request diffblue#1535 from andreast271/ignore-eclipse-vs-dirs 6cea5aa Ignore files and directories created by Eclipse and Visual Studio aa94fe8 Style: add nolint marker on lines formated by clang ee4a887 Merge pull request diffblue#1458 from LAJW/perl-platform 4da5a94 Add templating functionality to the perl script 21b2641 Move make_function_application to java_utils 5196e40 Merge pull request diffblue#884 from nmanthey/ipasir-no-ci 3ee3b25 Refactor: remove m_ prefix from member fields 539ff9f Refactoring: simplify and remove unused expression 5a0d6b4 Rename first_index in array_expr d03b8cc Remove regression test that is not checking anything 90c8495 Improve tests for StringBuilder.append([C) 232617c Add code for String constructor from array a2d7811 Use dynamic object instead of tmp_object in init daef30f Splitting is_string and init_string parts of init ad65847 Style: rename i in chr_int to avoid clash e59349f Remove redundant check in from_int_with_radix 038b476 Allow index for argument of associate array to pointer 73d51fc Remove insert_long which duplicates insert_int bb22700 Cleanup unused fields of constraint generator 2355e8e Fix set of created strings in generator and use it 26e895d Distinguish strings and char arrays in get 4b8a421 Make get_array return array of unknown expr ca8213f Simplify not_contains constraints before negation 92897f7 Style fixes in string_constraint_generator.h 145364c String refinement: Improve debug information 3e5b3f1 Minor code improvements in string refinement 3d5465e Minor code improvements in generator_insert 86e1444 Refactoring: use begin()+3 instead of 3 times next fef1c5f Correction in debug model 28590fe Correction in constraints for concat 6861b9d Documentation fixes in stirng constraint generator c410159 Regression: StringBuilder append with int argument e6700ff Minor improvements in bytecode typecheck 61f0e1b Making check_axioms for string_constraints and not_contains_constraints more uniform f2122c6 Correct signature of convert_exprt_to_string_exprt_unit_test 9edbb90 [string-refinement] Change get_array to return optional 86e4782 [string-refinement] Allow index set saturation if not_contains_constraints are present c9c612d [string-refinement] Do not update index set of constant arrays b88fe35 [string-refinement] Check for char type 1a22916 [string-refinement] Display debug info for index-set 982a5fc Style and documentation fixes in preprocessing a83daa7 Minor indentation, naming and const-fixes 15fd1b4 Fix typos in strings and comments of string solver 26ae9a9 Unit test improve convert exprt to string exprt b76b116 Minor improvements in string preprocessing 05a6b09 [constraint-generator] Removing declarations of unimplemented functions 302f92e Make string primitives return return_code_type b80d063 Doxygen corrections 369dd62 Unit test: adapte instantiate_nc for new signature dcae158 [string-refinement] Removing unused functions b6b2669 Style changes in string_constraint_generator_testing edf7057 Complete string solver rework 9ea2eda Unit tests for union_find_replacet 4adf5d0 New class for union find replace 1d112d5 Java object factory for nondet strings 0ae71b0 [string-preprocessing] New functions for calling string primitives in initialization e89f5e4 [string-preprocess] Refactor java_types_matches_tag 2505982 Extra preconditions in string solver 6378400 Style improvements in the string solver 36d6e6d [util/irep_ids] Additional identifiers fa45b34 Regression test mprovement for if expressions 76cd14d Unit test for gen_nondet_string_init c71c64b Regression: include model for string to char array c3d527c compiling: add IPASIR notes for Linux 900a0fc tests: do not match iterations line 751208d tests: drop number of iterations 12a6917 build: add ipasir solver support 14419d2 solvers: add ipasir driver 8aa89be build: introduce LIBSOLVER environment variable df45bdb Merge pull request diffblue#1524 from reuk/reuk/fix-linter 4b39446 Merge pull request diffblue#1518 from diffblue/taint-for-C 25e18c0 Merge pull request diffblue#1529 from smowton/smowton/fix/float128 3cf67f7 Merge pull request diffblue#1531 from reuk/reuk/expr-cast-fixup 2169a39 Add _Float128 spelling for 128-bit float type a3cf849 Merge pull request diffblue#1530 from martin-cs/feature/document-return-codes 188f263 Enable casting from derived types to other derived types 3dd7f6c first regression tests 29bc3b8 custom_bitvector_domain: allow objects that are members ab7270e check taint on sinks _before_ the call 6daa8bd Merge pull request diffblue#1528 from tautschnig/shl-overflow 2df2abb Change a few erronious return codes so that they are more internally consistent. cf96cef Minor changes to erronious exit behaviour. c8dfd48 Replace constants exit codes with meaningfully named macros. 961d33a Replace literal constants in returns / exits with their symbolic names. e74b442 Named, possibly even descriptive macros for the exit codes that are used. 1e3712c Shifts of non-integers and left shifts of negative integers are undefined 6bb3872 Check for overflow on left shift of signed ints f9af374 Merge pull request diffblue#1512 from thk123/bugfix/TG-1058/crash-inner-class-generic-class bd2e9c2 Merge pull request diffblue#1522 from reuk/reuk/clang-format-plain-diff f892f4a Added tests for bracket matcher to include different types of brackets 3beab8b Fixed error in find_closing_delimiter 0b3058f Tightened up exception for unknown handling 9f87a80 Assertion on unmatched ; for parsing reference types 5922826 Adding doubly nested generic tests 4a62b07 Simplifying method names for unit test ee39620 Extended tests to verify the generic information is being parsed correctly. 465a473 Parse multiple nested generic type informations b8d43ab Pulled out method for parsing a list of multiple types 2a5c280 Correctly parse multiple input parameters for functions 35d974f Add method for finding the matching ; corresponding to a reference L e1621a3 Hide methods relating to getting multiple type variables for specific param e952708 Adding tests for parsing methods of generic classes with inner classes 958c006 Adding utilities for code_type structures 72a041b Don't crash when found an invalid reference type ed545cb Refactored out the code for erasing generic types effc1b2 Parse the whole class when generics are present d23a0cc Added function for getting the full class name of a type 34c185e Unit test reproducing the bug described in TG-1058 5b92002 Adding utilities for checking types in unit tests a00edd3 Disable dowhile brace check by default d38b5d8 Disable colour in travis diff display git-subtree-dir: cbmc git-subtree-split: 4820601

tautschnig requested changes Oct 10, 2017

View reviewed changes

thk123 self-requested a review October 10, 2017 13:20

tautschnig reviewed Oct 10, 2017

View reviewed changes

LAJW changed the title ~~Add default platform arguments and benchmarking to the perl script~~ TG-840 Add default platform arguments and benchmarking to the perl script Oct 11, 2017

LAJW changed the title ~~TG-840 Add default platform arguments and benchmarking to the perl script~~ TG-945 Add default platform arguments and benchmarking to the perl script Oct 16, 2017

romainbrenguier requested review from smowton and allredj October 17, 2017 10:07

allredj suggested changes Oct 27, 2017

View reviewed changes

smowton approved these changes Oct 27, 2017

View reviewed changes

tautschnig approved these changes Oct 27, 2017

View reviewed changes

allredj approved these changes Oct 27, 2017

View reviewed changes

LAJW closed this Oct 30, 2017

romainbrenguier reopened this Oct 30, 2017

Add templating functionality to the perl script

4da5a94

romainbrenguier merged commit ee4a887 into diffblue:develop Oct 30, 2017

LAJW deleted the perl-platform branch October 30, 2017 12:05

TG-945 Add default platform arguments and benchmarking to the perl script #1458

TG-945 Add default platform arguments and benchmarking to the perl script #1458

Conversation

LAJW commented Oct 10, 2017 • edited Loading

martin-cs commented Oct 10, 2017

LAJW commented Oct 10, 2017

LAJW commented Oct 10, 2017

martin-cs commented Oct 10, 2017

LAJW commented Oct 10, 2017

martin-cs commented Oct 10, 2017

LAJW commented Oct 10, 2017

tautschnig left a comment

Choose a reason for hiding this comment

allredj commented Oct 10, 2017

tautschnig Oct 10, 2017

Choose a reason for hiding this comment

LAJW Oct 10, 2017

Choose a reason for hiding this comment

tautschnig Oct 10, 2017

Choose a reason for hiding this comment

LAJW Oct 10, 2017 • edited Loading

Choose a reason for hiding this comment

tautschnig Oct 10, 2017

Choose a reason for hiding this comment

LAJW commented Oct 16, 2017

smowton commented Oct 16, 2017

LAJW commented Oct 16, 2017

smowton commented Oct 16, 2017

tautschnig commented Oct 16, 2017

allredj commented Oct 17, 2017

tautschnig commented Oct 17, 2017

LAJW commented Oct 17, 2017 • edited Loading

tautschnig commented Oct 17, 2017

LAJW commented Oct 17, 2017 • edited Loading

tautschnig commented Oct 17, 2017

romainbrenguier commented Oct 17, 2017

tautschnig commented Oct 17, 2017

romainbrenguier commented Oct 17, 2017

LAJW commented Oct 17, 2017

tautschnig commented Oct 17, 2017

tautschnig commented Oct 17, 2017

allredj commented Oct 20, 2017

tautschnig commented Oct 20, 2017

LAJW commented Oct 23, 2017

allredj commented Oct 26, 2017

smowton commented Oct 27, 2017

LAJW commented Oct 27, 2017

smowton commented Oct 27, 2017

allredj Oct 27, 2017

Choose a reason for hiding this comment

LAJW commented Oct 27, 2017 • edited Loading

smowton left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj Oct 27, 2017

Choose a reason for hiding this comment

LAJW commented Oct 30, 2017

LAJW commented Oct 10, 2017 •

edited

Loading

LAJW Oct 10, 2017 •

edited

Loading

LAJW commented Oct 17, 2017 •

edited

Loading

LAJW commented Oct 17, 2017 •

edited

Loading

LAJW commented Oct 27, 2017 •

edited

Loading