|
| 1 | +# Model JDK classes [![Build Status][build_img]][travis] |
| 2 | + |
| 3 | +## Overview |
| 4 | + |
| 5 | +The role of the models library is twofold: |
| 6 | + |
| 7 | +Firstly, it provides simplified versions of the classes in the JDK, which speed |
| 8 | +up analysis with test-gen and also remove `native` methods. This means that |
| 9 | +tests can be generated more quickly. |
| 10 | + |
| 11 | +Secondly, it allows us to supply custom code to construct and set-up instances |
| 12 | +of modelled classes in generated tests, to make them more human readable. This |
| 13 | +is useful in cases where input-synthesis is unable to create a recipe for a |
| 14 | +particular object state. This should mean that generated tests only use public |
| 15 | +interfaces of objects, avoiding reflection. |
| 16 | + |
| 17 | +## Development |
| 18 | + |
| 19 | +### Getting started |
| 20 | + |
| 21 | +- Install Gauge from [here](https://getgauge.io/get-started.html). |
| 22 | +- Install the required Gauge plugins: |
| 23 | + ``` |
| 24 | + gauge install java |
| 25 | + gauge install html-report |
| 26 | + ``` |
| 27 | +- Navigate to the `model` subdirectory (`cd model`). |
| 28 | +- Run `mvn package` from the `model` directory to build a new copy of the |
| 29 | + `models.jar`, which will be placed in `model/target`. |
| 30 | +- Run `get-original-jdk.sh` to download a copy of the real jdk classes. |
| 31 | +- Use `add-new-file.sh` to copy a java class from the 'real' directory to our |
| 32 | + directory of models. For example, to copy the jdk implementation of |
| 33 | + java.lang.Long, run `add-new-file.sh java/lang/Long.java`. |
| 34 | +- Create a branch using the scheme `yourname/classname`. where `classname` is |
| 35 | + the class for which you're creating a model. |
| 36 | +- Commit the file you just copied. |
| 37 | +- Now, you can start making changes, and the git history will allow us to see a |
| 38 | + diff of all the changes from the original file. |
| 39 | +- Remember to re-run `mvn package` from the `model` directory after making |
| 40 | + changes, so that the model library contains your modifications. |
| 41 | + |
| 42 | +### Writing models |
| 43 | + |
| 44 | +- Don't remove exceptions, unless you can do so while maintaining the |
| 45 | + documented behaviour of the method. |
| 46 | +- Use the methods in the CProver library to supply nondet variables, or to |
| 47 | + assume that certain invariants always hold. To use this library, `import |
| 48 | + org.cprover.CProver;` at the top of your model class, and use the |
| 49 | + `CProver.nondet*` or `CProver.assume` methods. |
| 50 | + - More information about CProver's assume functionality can be found in [the |
| 51 | + manual](http://www.cprover.org/cprover-manual/modeling-assertions.shtml). |
| 52 | +- CBMC is smart about strings. Most of the `java.lang.String` methods are |
| 53 | + intercepted and handled natively by CBMC. Therefore, it should be fine to |
| 54 | + keep `String`-based functionality in your models. |
| 55 | +- Unbounded loops are bad, so try to avoid those. |
| 56 | +- Run `mvn package` to check that your model builds. |
| 57 | +- Leave existing comments in the code, to keep diffs minimal. |
| 58 | +- For non-trivial changes, please add a comment describing how the new modelled |
| 59 | + implementation differs from the original. So that this comment can be |
| 60 | + differentiated from existing comments, it should begin with |
| 61 | + ``` |
| 62 | + // DIFFBLUE MODEL LIBRARY |
| 63 | + ``` |
| 64 | + |
| 65 | +### Running Tests |
| 66 | + |
| 67 | +To test models with test-gen, you'll need an up-to-date copy of the |
| 68 | +test-generator binary. If you're developing models-library from the test-gen |
| 69 | +submodule, you can `cd model/modelTests` and run `setup.sh` to symlink |
| 70 | +`test-generator` and `models.jar` into the `under_test` directory. |
| 71 | +`setup.sh` will link `test-generator` from the outer test-gen repo, and |
| 72 | +`models.jar` from the `target` directory, so it's important that these files |
| 73 | +are in the expected locations, and have been built against the current branch |
| 74 | +of the models repo. |
| 75 | + |
| 76 | +Once you've set up the tests, you can run them using Gauge through Maven. Run |
| 77 | +the following command from the modelTests directory. It will get all the |
| 78 | +dependencies required for building and running the tests. Then, it will run all |
| 79 | +specs designated necessary for the support-v1 target, and which are known to |
| 80 | +pass. |
| 81 | +``` |
| 82 | +mvn test -Dtags='support-v1,!known-bug' '-DspecsDir=specs' '-Dflags=--verbose' |
| 83 | +``` |
| 84 | +The `verbose` flag is optional, but is recommended (at least at first) as it |
| 85 | +gives more information about which steps are being executed in the specs. |
| 86 | + |
| 87 | +This commandline can be modified to run different sets of tests. To run |
| 88 | +*all* tests (even failing ones), you can run |
| 89 | +``` |
| 90 | +mvn test |
| 91 | +``` |
| 92 | + |
| 93 | +To run just tests required for the support-v1 target, run |
| 94 | +``` |
| 95 | +mvn test -Dtags='support-v1', '-DspecsDir=specs' |
| 96 | +``` |
| 97 | + |
| 98 | +To run a specific test, run |
| 99 | +``` |
| 100 | +mvn test '-DspecsDir=specs/path/to/specfile.spec:15' |
| 101 | +``` |
| 102 | +where the number after the colon is the line number of the test to run. |
| 103 | + |
| 104 | +There are more details about running tests on the [maven gauge plugin |
| 105 | +readme](https://github.com/getgauge/gauge-maven-plugin). |
| 106 | + |
| 107 | +The Gauge standard-output just provides a high-level overview of what works and |
| 108 | +what doesn't. For more information, you will need to check the generated |
| 109 | +report. To open it, run the following command from the `modelTests` directory. |
| 110 | +``` |
| 111 | +see reports/html-report/index.html |
| 112 | +``` |
| 113 | + |
| 114 | +### Adding New Tests |
| 115 | + |
| 116 | +You will probably want to supply test specifications alongside any new models. |
| 117 | +First, you should probably familiarise yourself with how Gauge works, using the |
| 118 | +official documentation [here](https://docs.getgauge.io/using.html). |
| 119 | +Generally, test specifications will look like this: |
| 120 | + |
| 121 | +``` |
| 122 | +# java.package.ClassName |
| 123 | +
|
| 124 | +Tags: my-unique-tag |
| 125 | +
|
| 126 | +Plain text here is interpreted as a comment. Tags here apply to the entire |
| 127 | +file, so if you add known-bug as a tag, *none of the tests in the file will run |
| 128 | +in CI*. |
| 129 | +
|
| 130 | +* Bullet points correspond to methods in the TestRunner.java |
| 131 | +* Bullets at the top of the file are run for each subsequent subheading |
| 132 | +
|
| 133 | +
|
| 134 | +## method name or signature |
| 135 | +
|
| 136 | +Tags: known-bug |
| 137 | +
|
| 138 | +This test is known to fail. Normally we'll put a link to a relevant |
| 139 | +github issue here. |
| 140 | +
|
| 141 | +* This step runs the test |
| 142 | +
|
| 143 | +## another method name or signature |
| 144 | +
|
| 145 | +Tags: support-v1 |
| 146 | +
|
| 147 | +This test is known to pass, and is required for the support-v1 goal. |
| 148 | +
|
| 149 | +* This step runs the test |
| 150 | +``` |
| 151 | + |
| 152 | +Check in the `specs` directory to see what "real" specs look like. Some of the |
| 153 | +most important steps/bullet-points used specifically in the models tests |
| 154 | +follow. |
| 155 | + |
| 156 | +#### Verification |
| 157 | + |
| 158 | +``` |
| 159 | +* Run "classname.class", expecting exit code "0" and output "VERIFICATION SUCCESSFUL" |
| 160 | +``` |
| 161 | + |
| 162 | +This step will do a CBMC-style verification (using the test-generator |
| 163 | +executable) of the `main` method in the provided class. The second argument |
| 164 | +denotes the expected return code, and the final argument is a snippet that |
| 165 | +should be matched in the program's stdout. |
| 166 | + |
| 167 | +#### Test Generation |
| 168 | + |
| 169 | +``` |
| 170 | +* Verify test case for function "java.function.signature" in file "../under_test/models.jar" |
| 171 | +``` |
| 172 | + |
| 173 | +This step will generate, compile, and run a test for the given method. |
| 174 | +Generated tests are written to `<mavenProject>/src/test/java/MyTest.java`, |
| 175 | +where `<mavenProject>` is the currently-set Maven project. By default, this |
| 176 | +is `model/modelTests/generated_test`, although you can change this using the |
| 177 | +``` |
| 178 | +* Maven project is "path/to/directory" |
| 179 | +``` |
| 180 | +step, where the directory path is relative to `model/modelTests`. |
| 181 | + |
| 182 | +The last-generated test will be left in the current Maven directory, which can |
| 183 | +be useful for debugging in the cases where the Gauge output doesn't supply |
| 184 | +enough information. |
| 185 | + |
| 186 | +##### Supplying Function Signatures |
| 187 | + |
| 188 | +Most of the time, test-gen will be able to find the function you're testing |
| 189 | +using its name alone. However, sometimes a class will contain several methods |
| 190 | +with the same name, in which case you will need to supply a disambiguated name |
| 191 | +to the test generation step. |
| 192 | + |
| 193 | +Detailed information about disambiguated names can be found [at this |
| 194 | +link](https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.3.2). |
| 195 | +In short, for a function `Object func(int i, double d, MyObj m)` in class |
| 196 | +`org.project.Klass`, the disambiguated name will look like this: |
| 197 | + |
| 198 | +``` |
| 199 | +org.project.Klass.func:(IDLorg/project/MyObj;)Ljava/lang/Object; |
| 200 | +``` |
| 201 | + |
| 202 | +The important points: |
| 203 | +- There is a colon before the open bracket of the parameter list |
| 204 | +- Parameters are *not* comma-separated |
| 205 | +- Object references: |
| 206 | + - Start with `L` |
| 207 | + - End with `;` |
| 208 | + - Use `/` instead of `.` to separate class paths |
| 209 | + |
| 210 | +### Adding Initialisation Code |
| 211 | + |
| 212 | +This repo also contains some C++ code in the `plug` folder which is intended to |
| 213 | +be compiled into test-generator. This plugin tells test-gen how to initialise |
| 214 | +modelled classes, in the cases where test-generator can't work it out |
| 215 | +automatically using input-synthesis. |
| 216 | + |
| 217 | +At the moment, the plugin works like this: |
| 218 | + |
| 219 | +A function with the following signature is created, which returns a string of |
| 220 | +Java code initialising a variable with the given `name` to the state contained |
| 221 | +in `value`: |
| 222 | +``` |
| 223 | +std::string classname_init(const struct_exprt &value, const std::string &name); |
| 224 | +``` |
| 225 | + |
| 226 | +Then, this function is registered into the `writer_table` map in |
| 227 | +`plug/java_init.cpp`. That's it! |
| 228 | + |
| 229 | +Test-gen can query this map using the `get_model_writer` function to see |
| 230 | +whether there exists a custom initialiser for a given class. If so, |
| 231 | +test-generator will use this custom initialiser, and if not it will fall back |
| 232 | +to input synthesis or possibly reflection. |
| 233 | + |
| 234 | +### Misc |
| 235 | + |
| 236 | +`create-small-rt-jar.sh` can be used to create a jar file which contains the |
| 237 | +original jdk classes, rather than models, but does not contain any jdk clasess |
| 238 | +for which models don't exist. This might be useful in A-B testing. |
| 239 | + |
| 240 | +#### Model Stats |
| 241 | + |
| 242 | +The overall progress of the library modelling effort can be tracked using |
| 243 | +the script `model/modelTests/get_test_stats.py`. Navigate to `model/modelTests` |
| 244 | +and run |
| 245 | +``` |
| 246 | +python get_model_stats.py specs/jdk |
| 247 | +``` |
| 248 | + |
| 249 | +This script will scan all the specs under the provided path (`specs/jdk` in |
| 250 | +this case) for tests marked `support-v1`. Then, it will print the proportion of |
| 251 | +these tests which are *also* marked `known-bug`. Ideally, for the support-v1 |
| 252 | +target, the proportion of failing tests should be 0%. |
| 253 | + |
| 254 | +## Deployment |
| 255 | + |
| 256 | +For use with test-gen, this repo must be built alongside the test-gen repo. |
| 257 | +Currently, test-gen master has this repo as a submodule, and the master |
| 258 | +makefile there will call the makefile in `plug`. The `plug` makefile will build |
| 259 | +the C++ component as a static library, and will also build the Java models into |
| 260 | +`model/target/models.jar`. |
| 261 | + |
| 262 | +Note that the makefile in `plug` cannot be used standalone, as it depends on |
| 263 | +variables set by the test-gen superbuild. |
| 264 | + |
| 265 | +[build_img]: https://travis-ci.com/diffblue/models-library.svg?token=i8KzPhcTpXyyoppmAEw1 |
| 266 | +[travis]: https://travis-ci.com/diffblue/models-library |
0 commit comments