Merge pull request diffblue#359 from diffblue/update-models-library

Update models library

Author: owen-jones-diffblue

benchmarks/LIBRARIES/models/.travis.yml

@@ -46,8 +46,10 @@ install:
   - sudo apt-get update
   - sudo apt-get install gauge
   - gauge install java
-  - gauge install html-report
+    # Temporarily disable html-report (installing this plugin might not be required anyway)
+    # gauge install html-report
   - gauge config plugin_kill_timeout 20000
+  - gauge telemetry off
   - export MAVEN_OPTS="-XX:+TieredCompilation -XX:TieredStopAtLevel=1"
   - export DIFFBLUE_MODEL_TESTS_PROCESS_TIMEOUT="500"
 

benchmarks/LIBRARIES/models/README.md

@@ -196,76 +196,128 @@ the file on Google Cloud.
 
 ### Adding New Tests
 
+#### Quick overview of testing
+
+In models-library, there are three levels of tests:
+- Level 0 - verify model matching behaviour of JDK
+- Level 1 - small "unit" tests that verify tests can be generated, compile, run and pass for one configuration of one method or constructor
+- Level 2 - like Level 1 tests, but more typical use cases mimicking client code combining methods or classes.
+
+When writing new models, we tend to focus on writing Level 1 tests. We aim
+to ensure that all possible branches are covered. For example, in `ArrayList`,
+to check test generation of the `get(int i)` method, which gets an element
+at a particular index, you might a make class file `L1Get.java` that
+contains three methods for the following tests:
+- `i >= 0` and there is an element at `i`
+- `i >= al.size()` where `al` is an ArrayList (throws exception)
+- `i < 0` (throws exception)
+
+The Gauge spec file will take the class file, generate tests for it
+using models-library, verify that the tests give full coverage,
+compile the tests, run the tests using the JDK and
+verify that they pass, or throw an error.
+
+#### Gauge spec files
+
 You will probably want to supply test specifications alongside any new models.
 First, you should probably familiarise yourself with how Gauge works, using the
 official documentation [here](https://docs.getgauge.io/using.html).
 Generally, test specifications will look like this:
 
 ```
-# java.package.ClassName
+# java.<package>.<Class>
 
-Tags: my-unique-tag
+* Setup Maven project "test_data/maven/java/<package>/<Class>"
 
-Plain text here is interpreted as a comment. Tags here apply to the entire
-file, so if you add known-bug as a tag, *none of the tests in the file will run
-in CI*.
+## Level 1 <Class>
 
-* Bullet points correspond to methods in the TestRunner.java
-* Bullets at the top of the file are run for each subsequent subheading
+Level 1 - <constructor or method>
+<Optional comments>
+* Set class file "target/classes/<ClassFileName1>.class"
+* Generate tests for "<ClassFileName1>.<TestName1>"
+* Generate tests for "<ClassFileName1>.<TestName2>"
 
+Level 1 - <another constructor or method>
+<Optional comments>
+* Set class file "target/classes/<ClassFileName2>.class"
+* Generate tests for "<ClassFileName2>.<TestName1>"
+* Generate tests for "<ClassFileName2>.<TestName2>"
 
-## method name or signature
+* Verify tests in Maven project
+* Unset class file
 
-Tags: known-bug
 
-This test is known to fail. Normally we'll put a link to a relevant
-github issue here.
+## Level 1 <Class> <tagname>
 
-* This step runs the test
+Tags: <tagname>
 
-## another method name or signature
+<Jira ticket if a known-bug or future>
+<Optional comments>
+* Set class file "target/classes/<ClassFileName1>.class"
+* Generate tests for "<ClassFileName1>.<TestName1>"
+* Generate tests for "<ClassFileName1>.<TestName2>"
 
-Tags: support-v1
+* Verify tests in Maven project
+* Unset class file
+```
 
-This test is known to pass, and is required for the support-v1 goal.
+where tags are:
+- `future`
+- `long`
+- `known-bug`
 
-* This step runs the test
-```
+The `long` tag is used to prevent tests that take too long from running
+on CI. We rarely use the `future` tag, but occasionally we develop models
+before deeptest is ready for them. Anything tagged with `known-bug` should
+include the Jira ticket number.
 
-Check in the `specs` directory to see what "real" specs look like.  Some of the
-most important steps/bullet-points used specifically in the models tests
-follow.
+Some of the most important steps/bullet-points used specifically
+in the models tests follow.
 
 #### Verification
 
 ```
 * Run "classname.class", expecting exit code "0" and output "VERIFICATION SUCCESSFUL"
 ```
 
+These are Level 0 tests.
+
 This step will do a CBMC-style verification (using the test-generator
 executable) of the `main` method in the provided class. The second argument
 denotes the expected return code, and the final argument is a snippet that
 should be matched in the program's stdout.
 
 #### Grouped Test Generation (recommended)
 
-The process for generating tests and verfying them (compile, run, pass) in a
+These are Level 1 and 2 tests.
+
+The process for generating tests and verifying them (compile, run, pass) in a
 specified maven directory is as follows:
 
 Set the maven directory and clean all test files:
 ```
 * Setup Maven project "path/to/directory"
 ```
-Run test-generator to populate the Maven project with generated test:
+Run test-generator to populate the Maven project with generated test from
+methods in a class file:
+```
+* Set class file "target/classes/<ClassFileName1>.class"
+* Generate tests for "<ClassFileName1>.<TestName1>"
+* Generate tests for "<ClassFileName1>.<TestName2>"
+```
+for as many class files as required.
+
+In older spec files you may also see this more cumbersome notation:
 ```
 * Generate tests for "java.function.signature1" in "target/classes/test1.class"
 * Generate tests for "java.function.signature2" in "target/classes/test2.class"
 * Generate tests for "java.function.signature3" in "target/classes/test3.class"
   ...
 ```
-Run mvn test on the Maven project:
+Run mvn test on the Maven project and unset the class file:
 ```
 * Verify tests in Maven project
+* Unset class file
 ```
 
 #### Standalone Test Generation (not recommended)
@@ -347,4 +399,3 @@ variables set by the test-gen superbuild.
 
 [build_img]: https://travis-ci.com/diffblue/models-library.svg?token=i8KzPhcTpXyyoppmAEw1
 [travis]: https://travis-ci.com/diffblue/models-library
-

benchmarks/LIBRARIES/models/model/modelTests/pom.xml

@@ -11,7 +11,7 @@
     <dependency>
       <groupId>com.thoughtworks.gauge</groupId>
       <artifactId>gauge-java</artifactId>
-      <version>0.6.4</version>
+      <version>0.6.6</version>
       <scope>test</scope>
     </dependency>
     <dependency>

benchmarks/LIBRARIES/models/model/modelTests/specs/bugs.spec

@@ -6,17 +6,16 @@
 
 Tests that were previously disabled due to a bug that has now been fixed
 
-TG-1877 Types of elements of input arrays ignored by lazy methods
-  causes TG-1712 Incorrect tests for comparison of primitive wrapper classes in array
 * Generate tests for "tg1877.ArrayListElementsCustom.callMethodOnElement" in "target/classes/tg1877/ArrayListElementsCustom.class"
 * Generate tests for "tg1877.ArrayListElementsInteger.callLessOnElement" in "target/classes/tg1877/ArrayListElementsInteger.class"
 * Generate tests for "tg1877.ArrayListElementsInteger.callLessOnElementAndConst" in "target/classes/tg1877/ArrayListElementsInteger.class"
 * Generate tests for "tg1877.ArrayListElementsInteger.callPrimitiveLessOnElement" in "target/classes/tg1877/ArrayListElementsInteger.class"
 * Generate tests for "tg1877.ArrayListElementsBitSet.callMethodOnElement" in "target/classes/tg1877/ArrayListElementsBitSet.class"
 
-TG-1245 Object.getClass not working for Objects that may be null
 * Generate tests for "tg1245.ObjectGetClassMaybeNull.test" in "target/classes/tg1245/ObjectGetClassMaybeNull.class"
 
+* Generate tests for "tg1931.L1ToStringOnObject.toStringObject" in "target/classes/tg1931/L1ToStringOnObject.class"
+
 * Verify tests in Maven project
 
 ## LONG
@@ -26,8 +25,19 @@ too long to be enabled on CI.
 
 Tags: long
 
-TG-1877 Types of elements of input arrays ignored by lazy methods
-  causes TG-1712 Incorrect tests for comparison of primitive wrapper classes in array
 * Generate tests for "tg1877.CustomType.moreComplicatedCalls" in "target/classes/tg1877/CustomType.class"
 
 * Verify tests in Maven project
+
+
+## KNOWN BUGS
+
+Tests for which there is a known issue that has not yet been fixed
+
+Tags: known-bug
+
+TG-2717
+Specializing fields of a generic abstract class implementation does not work
+* Generate tests for "tg2717.GenericInterface.hashmapNdMap" in "target/classes/tg2717/GenericInterface.class"
+
+* Verify tests in Maven project

benchmarks/LIBRARIES/models/model/modelTests/specs/java/io/File.spec

@@ -1,29 +1,21 @@
 # java.io.File
 
-## Level 1+ tests - java.io.File
-
 * Setup Maven project "test_data/maven/java/io/File"
 
-TODO Review these tests and sort into level 1 and level 2
-* Generate tests for "FileConstructorPath.test" in "target/classes/FileConstructorPath.class"
-* Generate tests for "FileConstructorPC.test" in "target/classes/FileConstructorPC.class"
-* Generate tests for "FileConstructorFC.test" in "target/classes/FileConstructorFC.class"
-* Generate tests for "FileConstructor.test" in "target/classes/FileConstructor.class"
-
-* Verify tests in Maven project
-
-## Level 1 Known Bugs - java.io.File
-
-Tags: known-bug
-
-* Setup Maven project "test_data/maven/java/io/File"
+## Level 1+ tests - java.io.File
 
-TG-1081/ TG-1976 Static fields not initialised in test
+Level 1 public fields
 * Set class file "target/classes/L1Fields.class"
 * Generate tests for "L1Fields.fieldSeparatorChar"
 * Generate tests for "L1Fields.fieldSeparator"
 * Generate tests for "L1Fields.fieldPathSeparatorChar"
 * Generate tests for "L1Fields.fieldPathSeparator"
 * Unset class file
 
+TODO Review these tests and sort into level 1 and level 2
+* Generate tests for "FileConstructorPath.test" in "target/classes/FileConstructorPath.class"
+* Generate tests for "FileConstructorPC.test" in "target/classes/FileConstructorPC.class"
+* Generate tests for "FileConstructorFC.test" in "target/classes/FileConstructorFC.class"
+* Generate tests for "FileConstructor.test" in "target/classes/FileConstructor.class"
+
 * Verify tests in Maven project

benchmarks/LIBRARIES/models/model/modelTests/specs/java/lang/Class.spec

@@ -1,53 +1,42 @@
 # java.lang.Class
 
-## toString
+* Setup Maven project "test_data/maven/java/lang/Class"
 
-Tags: support-v1
+## toString
 
-* Setup Maven project "test_data/maven/java/lang/Class"
 * Generate tests for "GetClassToString.test" in "target/classes/GetClassToString.class"
 * Generate tests for "IntegerGetClassToString.test" in "target/classes/IntegerGetClassToString.class"
-* Verify tests in Maven project
-
-## toString_KNOWNBUG
-
-Tags: support-v1, known-bug
-* Setup Maven project "test_data/maven/java/lang/Class"
-
-TG-1081: Integer.TYPE is always (erroneously) initialized to null
 * Generate tests for "IntegerTypeToString.test" in "target/classes/IntegerTypeToString.class"
 * Verify tests in Maven project
 
 ## getName
 
-Tags: support-v1
-
 diffblue/models-library#111
 * Working directory is "test_data/functional/java/lang/Class"
 * Run "getName_Pass.class", expecting exit code "0" and output "VERIFICATION SUCCESSFUL"
 
 ## isAssignableFrom
 
-Tags: support-v1, known-bug
+Tags: known-bug
 * Working directory is "test_data/functional/java/lang/Class"
 * Run "isAssignableFrom_Pass.class", expecting exit code "0" and output "VERIFICATION SUCCESSFUL"
 
 ## getMethod
 
-Tags: support-v1, known-bug
+Tags: known-bug
 
 diffblue/models-library#112
 * Working directory is "test_data/functional/java/lang/Class"
 * Run "getMethod_Pass.class", expecting exit code "0" and output "VERIFICATION SUCCESSFUL"
 
 ## getClassLoader
 
-Tags: support-v1, known-bug
+Tags: known-bug
 * Working directory is "test_data/functional/java/lang/Class"
 * Run "getClassLoader_Pass.class", expecting exit code "0" and output "VERIFICATION SUCCESSFUL"
 
 ## getSimpleName
 
-Tags: support-v1, known-bug
+Tags: known-bug
 * Working directory is "test_data/functional/java/lang/Class"
 * Run "getSimpleName_Pass.class", expecting exit code "0" and output "VERIFICATION SUCCESSFUL"