@@ -41,37 +41,113 @@ interfaces of objects, avoiding reflection.
4141
4242### Writing models
4343
44+ - Don't remove public static fields. Doing so could lead to invariant
45+ violations during test generation. Changing the value that is assigned to the
46+ field is fine.
4447- Don't remove exceptions, unless you can do so while maintaining the
4548 documented behaviour of the method.
4649- 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
50+ assume that certain conditions always hold. To use this library, `import
4851 org.cprover.CProver;` at the top of your model class, and use the
49- ` CProver.nondet* ` or ` CProver.assume ` methods.
52+ ` CProver.nondet* ` or ` CProver.assume ` methods. The library is located in
53+ ` model/src/main/java/org/cprover/CProver.java ` .
54+ For example, for a method that takes an argument that we do not currently
55+ support being null, you could add the line
56+ ```
57+ CProver.assume(arg != null);
58+ ```
59+ in that method, and for a method with return type ` int ` that should give
60+ nondeterministic results, you could write
61+ ```
62+ return CProver.nondetInt();
63+ ```
64+ Methods that are not currently modelled should include the line
65+ ```
66+ CProver.notModelled();
67+ ```
68+ in the method body. Deeptest will discard any tests that depend on any such
69+ method.
5070 - More information about CProver's assume functionality can be found in [ the
5171 manual] ( http://www.cprover.org/cprover-manual/modeling-assertions.shtml ) .
5272- CBMC is smart about strings. Most of the ` java.lang.String ` methods are
5373 intercepted and handled natively by CBMC. Therefore, it should be fine to
54- keep ` String ` -based functionality in your models.
74+ keep ` String ` -based functionality in your models. However, when ` String `
75+ operations are unlikely to be necessary it can be preferable to avoid them
76+ as they can slow down test generation in some cases. For example, we usually
77+ avoid detail messages in ` Throwable ` s when they would include string
78+ concatenation, e.g.
79+ ```
80+ throw new IllegalArgumentException("Illegal Capacity: "+(initialCapacity));
81+ ```
82+ would be commented out and replaced with a simple
83+ ```
84+ throw new IllegalArgumentException();
85+ ```
5586- 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.
87+ - Run ` mvn package ` from the ` model ` directory to check that your model builds.
88+ - Leave existing comments in the code to keep diffs minimal, and comment out
89+ original code from the JDK rather than delete it, to make it easier to review
90+ what the original implementation does and what was changed/simplified.
5891- For non-trivial changes, please add a comment describing how the new modelled
5992 implementation differs from the original. So that this comment can be
6093 differentiated from existing comments, it should begin with
6194 ```
6295 // DIFFBLUE MODEL LIBRARY
6396```
6497
98+ ### Generating the documentation
99+
100+ The javadoc for the model library can be generated from the ` model ` directory
101+ with the command:
102+ ```
103+ mvn javadoc:javadoc
104+ ```
105+ The generated site can then be found in
106+ ` model/target/site/apidocs/index.html ` .
107+ The javadoc interprets the following tags placed in field, method, and class
108+ headers:
109+ - @diffblue .fullSupport
110+ - @diffblue .limitedSupport
111+ - @diffblue .noSupport
112+ - @diffblue .untested
113+ - @diffblue .todo
114+ - @diffblue .mock
115+
116+ For instance, if the following tag is present in the header of a method:
117+ ```
118+ /**
119+ * Returns a {@code Byte} instance representing the specified
120+ * {@code byte} value.
121+ *
122+ * @param b a byte value.
123+ * @return a {@code Byte} instance representing {@code b}.
124+ *
125+ * @diffblue.limitedSupport
126+ * Restricted to non-negative values.
127+ * Might be slow if argument is non-deterministic.
128+ */
129+ public static Byte valueOf(byte b) {
130+ ...
131+ ```
132+ The following output can be observed in the documentation of the Byte class:
133+ <blockquote ><b >DIFFBLUE: Limited support</b ><br />
134+ Restricted to non-negative values. Might be slow if argument is
135+ non-deterministic.
136+ </blockquote >
137+
138+
65139### Running Tests
66140
67141To test models with test-gen, you'll need an up-to-date copy of the
68142test-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
143+ submodule, you can ` cd model/modelTests ` and run ` setup.sh "build" ` to symlink
70144` test-generator ` and ` models.jar ` into the ` under_test ` directory.
71- ` setup.sh ` will link ` test-generator ` from the outer test-gen repo, and
145+ ` setup.sh "build" ` will link ` test-generator ` from the outer test-gen repo, and
72146` models.jar ` from the ` target ` directory, so it's important that these files
73147are in the expected locations, and have been built against the current branch
74- of the models repo.
148+ of the models repo. The argument to ` setup.sh ` is the directory passed to cmake
149+ when building ` test-generator ` , so if you ran ` cmake -H. -B$DIR ` , you should
150+ run ` setup.sh $DIR ` .
75151
76152Once you've set up the tests, you can run them using Gauge through Maven. Run
77153the 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.
111187see reports/html-report/index.html
112188```
113189
190+ Travis also provides a report after running all the models-library tests, which
191+ is saved as a Travis artifact and is hence available for 30 days. It can be
192+ accessed by following the link at the bottom of the Travis output and by
193+ unfolding the ` # Save the html report ` line. The link there will lead you to
194+ the file on Google Cloud.
195+
196+
114197### Adding New Tests
115198
116199You 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
164247denotes the expected return code, and the final argument is a snippet that
165248should be matched in the program's stdout.
166249
167- #### Test Generation
250+ #### Grouped Test Generation (recommended)
251+
252+ The process for generating tests and verfying them (compile, run, pass) in a
253+ specified maven directory is as follows:
254+
255+ Set the maven directory and clean all test files:
256+ ```
257+ * Setup Maven project "path/to/directory"
258+ ```
259+ Run test-generator to populate the Maven project with generated test:
260+ ```
261+ * Generate tests for "java.function.signature1" in "target/classes/test1.class"
262+ * Generate tests for "java.function.signature2" in "target/classes/test2.class"
263+ * Generate tests for "java.function.signature3" in "target/classes/test3.class"
264+ ...
265+ ```
266+ Run mvn test on the Maven project:
267+ ```
268+ * Verify tests in Maven project
269+ ```
270+
271+ #### Standalone Test Generation (not recommended)
168272
169273```
170274* 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
183287be useful for debugging in the cases where the Gauge output doesn't supply
184288enough information.
185289
290+ This procedure is not recommended as the overhead for running the maven tests
291+ is several seconds. It is therefore better to group tests as suggested above.
292+
186293##### Supplying Function Signatures
187294
188295Most of the time, test-gen will be able to find the function you're testing
@@ -207,30 +314,6 @@ The important points:
207314 - End with ` ; `
208315 - Use ` / ` instead of ` . ` to separate class paths
209316
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-
234317### Misc
235318
236319` 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.
264347
265348[ build_img ] : https://travis-ci.com/diffblue/models-library.svg?token=i8KzPhcTpXyyoppmAEw1
266349[ travis ] : https://travis-ci.com/diffblue/models-library
350+
0 commit comments