Merge pull request diffblue#337 from diffblue/models-merge

SEC-242: Update the models library in the security scanner repo.

Author: smowton

CMakeLists.txt

@@ -70,6 +70,10 @@ execute_process(COMMAND ${boost-include_SOURCE_DIR}/b2 dll-path=${boost-include_
                 WORKING_DIRECTORY ${boost-include_SOURCE_DIR}
 )
 
+execute_process(COMMAND mvn package
+                WORKING_DIRECTORY ${PROJECT_SOURCE_DIR}/benchmarks/LIBRARIES/models/model
+)
+
 set(boost_include_include_dir ${boost-include_SOURCE_DIR})
 set(boost_lib_dir ${boost-include_SOURCE_DIR}/stage/lib)
 link_directories(${boost_lib_dir})
@@ -82,7 +86,6 @@ set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/lib")
 SET(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE)
 
 add_subdirectory(cbmc)
-add_subdirectory(benchmarks/LIBRARIES/models)
 
 add_subdirectory(src)
 

benchmarks/LIBRARIES/models/.gitignore

@@ -1,6 +1,5 @@
-target
-jdk-original
-plug/build
+/model/target
+/model/jdk-original
 
 *.txt
 *.d

benchmarks/LIBRARIES/models/.travis.yml

@@ -26,18 +26,19 @@ before_install:
     CLOUDSDK_CORE_DISABLE_PROMPTS=1; curl https://sdk.cloud.google.com | bash > /tmp/gcloud.log || cat /tmp/gcloud.log; fi
   - source /home/travis/google-cloud-sdk/path.bash.inc
   # Add gcloud to $PATH
-  - gcloud --quiet components update
+  # Temporarily disable gcloud update to avoid crash. See TG-2513 for details (and as a reminder to re-enable this).
+  # gcloud --quiet components update
   - gcloud auth activate-service-account --key-file .gcloud-travis-models-library.json
   # Resolve dependencies for gsutil
-  - pip install google_compute_engine --upgrade
+  - sudo pip install google_compute_engine --upgrade
 
 install:
   - cd model
   - mvn package
   - cd modelTests
-  - gsutil cp gs://travis-artifacts/test-gen/${TEST_GEN_BUILD:-"latest-master-ubuntu"}.tar.gz cbmc-testgen-latest.tar.gz
+  - gsutil cp gs://travis-artifacts/test-gen/${TEST_GEN_BUILD:-"latest-develop-ubuntu"}.tar.gz cbmc-testgen-latest.tar.gz
   - tar -zxvf cbmc-testgen-latest.tar.gz -C under_test
-  - mvn install:install-file -Dfile=under_test/diffblue.jar -DpomFile=under_test/pom.xml
+  - mvn install:install-file -Dfile=under_test/deeptestutils-1.0.0.jar -DpomFile=under_test/pom.xml
   - mv ../target/models.jar under_test
   # Setup gauge
   - sudo apt-key adv --keyserver hkp://pool.sks-keyservers.net --recv-keys 023EDB0B
@@ -46,20 +47,38 @@ install:
   - sudo apt-get install gauge
   - gauge install java
   - gauge install html-report
+  - gauge config plugin_kill_timeout 20000
+  - export MAVEN_OPTS="-XX:+TieredCompilation -XX:TieredStopAtLevel=1"
+  - export DIFFBLUE_MODEL_TESTS_PROCESS_TIMEOUT="500"
 
 script:
-  - mvn test -Dtags='!known-bug' -Dflags='-s' -DspecsDir='specs'
-  - bash print-reports.sh reports/html-report/specs
+  - mvn test -Dtags='!known-bug,!future,!long' -Dflags='--verbose' -DspecsDir='specs'
+
+before_cache:
+    # To be able to update via pip
+  - sudo apt-get remove python-openssl
+    # Upgrade pyopenssl (signurl prereq) via pip
+  - sudo pip install pyopenssl --upgrade
+
+  - |
+    # Save the html report
+    ( set -euo pipefail
+      if [[ -d reports/html-report ]]
+      then
+        REPORT_FILE=html-report-$(git describe --tags --always).tar.gz
+        tar -zcvf ${REPORT_FILE} reports/html-report
+        gsutil -h "Content-Disposition:attachment; filename=models-${TRAVIS_BUILD_NUMBER}-report.tar.gz" \
+          cp ${REPORT_FILE} gs://travis-artifacts/models-library/models-${TRAVIS_BUILD_NUMBER}-report.tar.gz
+        echo Link to html report:
+        echo "https://console.cloud.google.com/storage/browser/travis-artifacts/models-library?project=diffblue-cr&prefix=models-${TRAVIS_BUILD_NUMBER}"
+      fi
+    )
 
 after_success:
   - |
     set -euo pipefail
     if [[ "${TRAVIS_PULL_REQUEST_BRANCH:-$TRAVIS_BRANCH}" =~ ^master|develop$ ]]
     then
-      # To be able to update via pip
-      sudo apt-get remove python-openssl
-      # Upgrade pyopenssl (signurl prereq) via pip
-      pip install pyopenssl --upgrade
       BRANCH=$(echo ${TRAVIS_PULL_REQUEST_BRANCH:-$TRAVIS_BRANCH} | tr '/' '_')
       FILE=models-$(git describe --tags --always).jar
       mv under_test/models.jar ${FILE}
@@ -78,5 +97,5 @@ after_success:
       SIGNED_URL=$(gsutil signurl -d 365d -m GET ${TRAVIS_BUILD_DIR}/.gcloud-travis-models-library.json \
         gs://diffblue-binaries/models-library/${BRANCH}/${FILE} | awk '$5 ~ /https/ {print $5}')
     fi
-    set +u
+    set +eu
   - echo ${SIGNED_URL}

benchmarks/LIBRARIES/models/CMakeLists.txt

@@ -0,0 +1,2 @@
+# These owners will be the default owners for everything in the repo.
+*      @allredj @antlechner @romainbrenguier

benchmarks/LIBRARIES/models/CODEOWNERS

@@ -41,37 +41,113 @@ interfaces of objects, avoiding reflection.
 
 ### Writing models
 
+- Don't remove public static fields. Doing so could lead to invariant
+  violations during test generation. Changing the value that is assigned to the
+  field is fine.
 - Don't remove exceptions, unless you can do so while maintaining the
   documented behaviour of the method.
 - Use the methods in the CProver library to supply nondet variables, or to
-  assume that certain invariants always hold. To use this library, `import
+  assume that certain conditions always hold. To use this library, `import
   org.cprover.CProver;` at the top of your model class, and use the
-  `CProver.nondet*` or `CProver.assume` methods.
+  `CProver.nondet*` or `CProver.assume` methods. The library is located in
+  `model/src/main/java/org/cprover/CProver.java`.
+  For example, for a method that takes an argument that we do not currently
+  support being null, you could add the line
+  ```
+  CProver.assume(arg != null);
+  ```
+  in that method, and for a method with return type `int` that should give
+  nondeterministic results, you could write
+  ```
+  return CProver.nondetInt();
+  ```
+  Methods that are not currently modelled should include the line
+  ```
+  CProver.notModelled();
+  ```
+  in the method body. Deeptest will discard any tests that depend on any such
+  method.
   - More information about CProver's assume functionality can be found in [the
     manual](http://www.cprover.org/cprover-manual/modeling-assertions.shtml).
 - CBMC is smart about strings. Most of the `java.lang.String` methods are
   intercepted and handled natively by CBMC. Therefore, it should be fine to
-  keep `String`-based functionality in your models.
+  keep `String`-based functionality in your models. However, when `String`
+  operations are unlikely to be necessary it can be preferable to avoid them
+  as they can slow down test generation in some cases. For example, we usually
+  avoid detail messages in `Throwable`s when they would include string
+  concatenation, e.g.
+  ```
+  throw new IllegalArgumentException("Illegal Capacity: "+(initialCapacity));
+  ```
+  would be commented out and replaced with a simple
+  ```
+  throw new IllegalArgumentException();
+  ```
 - Unbounded loops are bad, so try to avoid those.
-- Run `mvn package` to check that your model builds.
-- Leave existing comments in the code, to keep diffs minimal.
+- Run `mvn package` from the `model` directory to check that your model builds.
+- Leave existing comments in the code to keep diffs minimal, and comment out
+  original code from the JDK rather than delete it, to make it easier to review
+  what the original implementation does and what was changed/simplified.
 - For non-trivial changes, please add a comment describing how the new modelled
   implementation differs from the original. So that this comment can be
   differentiated from existing comments, it should begin with
   ```
   // DIFFBLUE MODEL LIBRARY
   ```
 
+### Generating the documentation
+
+The javadoc for the model library can be generated from the `model` directory
+with the command:
+```
+mvn javadoc:javadoc
+```
+The generated site can then be found in
+`model/target/site/apidocs/index.html`.
+The javadoc interprets the following tags placed in field, method, and class
+headers:
+- @diffblue.fullSupport
+- @diffblue.limitedSupport
+- @diffblue.noSupport
+- @diffblue.untested
+- @diffblue.todo
+- @diffblue.mock
+
+For instance, if the following tag is present in the header of a method:
+```
+    /**
+     * Returns a {@code Byte} instance representing the specified
+     * {@code byte} value.
+     *
+     * @param  b a byte value.
+     * @return a {@code Byte} instance representing {@code b}.
+     *
+     * @diffblue.limitedSupport
+     * Restricted to non-negative values.
+     * Might be slow if argument is non-deterministic.
+     */
+    public static Byte valueOf(byte b) {
+        ...
+```
+The following output can be observed in the documentation of the Byte class:
+<blockquote><b>DIFFBLUE: Limited support</b><br/>
+Restricted to non-negative values. Might be slow if argument is
+non-deterministic.
+</blockquote>
+
+
 ### Running Tests
 
 To test models with test-gen, you'll need an up-to-date copy of the
 test-generator binary. If you're developing models-library from the test-gen
-submodule, you can `cd model/modelTests` and run `setup.sh` to symlink
+submodule, you can `cd model/modelTests` and run `setup.sh "build"` to symlink
 `test-generator` and `models.jar` into the `under_test` directory.
-`setup.sh` will link `test-generator` from the outer test-gen repo, and
+`setup.sh "build"` will link `test-generator` from the outer test-gen repo, and
 `models.jar` from the `target` directory, so it's important that these files
 are in the expected locations, and have been built against the current branch
-of the models repo.
+of the models repo. The argument to `setup.sh` is the directory passed to cmake
+when building `test-generator`, so if you ran `cmake -H. -B$DIR`, you should
+run `setup.sh $DIR`.
 
 Once you've set up the tests, you can run them using Gauge through Maven.  Run
 the following command from the modelTests directory. It will get all the
@@ -111,6 +187,13 @@ report. To open it, run the following command from the `modelTests` directory.
 see reports/html-report/index.html
 ```
 
+Travis also provides a report after running all the models-library tests, which
+is saved as a Travis artifact and is hence available for 30 days. It can be
+accessed by following the link at the bottom of the Travis output and by
+unfolding the `# Save the html report` line. The link there will lead you to
+the file on Google Cloud.
+
+
 ### Adding New Tests
 
 You will probably want to supply test specifications alongside any new models.
@@ -164,7 +247,28 @@ 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.
 
-#### Test Generation
+#### Grouped Test Generation (recommended)
+
+The process for generating tests and verfying 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:
+```
+* 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:
+```
+* Verify tests in Maven project
+```
+
+#### Standalone Test Generation (not recommended)
 
 ```
 * Verify test case for function "java.function.signature" in file "../under_test/models.jar"
@@ -183,6 +287,9 @@ The last-generated test will be left in the current Maven directory, which can
 be useful for debugging in the cases where the Gauge output doesn't supply
 enough information.
 
+This procedure is not recommended as the overhead for running the maven tests
+is several seconds. It is therefore better to group tests as suggested above.
+
 ##### Supplying Function Signatures
 
 Most of the time, test-gen will be able to find the function you're testing
@@ -207,30 +314,6 @@ The important points:
   - End with `;`
   - Use `/` instead of `.` to separate class paths
 
-### Adding Initialisation Code
-
-This repo also contains some C++ code in the `plug` folder which is intended to
-be compiled into test-generator. This plugin tells test-gen how to initialise
-modelled classes, in the cases where test-generator can't work it out
-automatically using input-synthesis.
-
-At the moment, the plugin works like this:
-
-A function with the following signature is created, which returns a string of
-Java code initialising a variable with the given `name` to the state contained
-in `value`:
-```
-std::string classname_init(const struct_exprt &value, const std::string &name);
-```
-
-Then, this function is registered into the `writer_table` map in
-`plug/java_init.cpp`. That's it!
-
-Test-gen can query this map using the `get_model_writer` function to see
-whether there exists a custom initialiser for a given class. If so,
-test-generator will use this custom initialiser, and if not it will fall back
-to input synthesis or possibly reflection.
-
 ### Misc
 
 `create-small-rt-jar.sh` can be used to create a jar file which contains the
@@ -264,3 +347,4 @@ 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/README.md

@@ -2,9 +2,14 @@
 logs
 reports
 gauge_bin
-target
+/target
 
-generated_test/src/test/java/MyTest.java
+**/src/test/java/TestFor*.java
 
 under_test/models.jar
 under_test/test-generator
+
+**/target/surefire-reports
+**/target/*.jar
+**/target/test-classes
+**/target/maven-archiver