Skip to content

Commit c9546e5

Browse files
antlechnerantlechner
committed
Add script to generate JSON file for regression tests
This will make it easier to adapt the tests or try out the --static-values option on other examples.
1 parent 70fcf31 commit c9546e5

File tree

8 files changed

+301
-0
lines changed

8 files changed

+301
-0
lines changed

‎jbmc/regression/jbmc/deterministic_assignments_json/README

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,3 +4,7 @@ Most of the tests are in StaticValues.java, some more tests are included in
44
Color.java, and all other classes are used to create instances of various kinds
55
of objects to use in the tests.
66
The initial static field values are read from the file clinit-state.json.
7+
The script generate-json.sh (which calls org.cprover.JsonGenerator in the Maven
8+
project) can be used to generate output similar to the contents of
9+
clinit-state.json (with slightly less pretty-printing/newlines, which are not
10+
supported in the custom writers and were manually added to clinit-state.json).

‎jbmc/regression/jbmc/deterministic_assignments_json/generate-json.sh

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
#!/bin/bash
2+
3+
mvn package
4+
java -cp target/jsonGenerator-1.0-SNAPSHOT-jar-with-dependencies.jar:. org.cprover.JsonGenerator
5+
# The following command only works using GNU sed.
6+
# (Remove all lines containing the string "StaticFieldMap" as they are not needed.)
7+
sed -i '/StaticFieldMap/d' clinit-state.json

‎jbmc/regression/jbmc/deterministic_assignments_json/pom.xml

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>jsonGenerator</groupId>
7+
<artifactId>jsonGenerator</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<dependencies>
11+
<dependency>
12+
<groupId>com.cedarsoftware</groupId>
13+
<artifactId>json-io</artifactId>
14+
<version>4.10.1</version>
15+
</dependency>
16+
</dependencies>
17+
18+
<build>
19+
<plugins>
20+
<plugin>
21+
<groupId>org.apache.maven.plugins</groupId>
22+
<artifactId>maven-assembly-plugin</artifactId>
23+
<executions>
24+
<execution>
25+
<phase>package</phase>
26+
<goals>
27+
<goal>single</goal>
28+
</goals>
29+
<configuration>
30+
<archive>
31+
<manifest>
32+
<mainClass>
33+
com.diffblue.prototype.StaticInitState
34+
</mainClass>
35+
</manifest>
36+
</archive>
37+
<descriptorRefs>
38+
<descriptorRef>jar-with-dependencies</descriptorRef>
39+
</descriptorRefs>
40+
</configuration>
41+
</execution>
42+
</executions>
43+
</plugin>
44+
<plugin>
45+
<groupId>org.apache.maven.plugins</groupId>
46+
<artifactId>maven-jar-plugin</artifactId>
47+
<configuration>
48+
<archive>
49+
<manifest>
50+
<mainClass>com.diffblue.prototype.StaticInitState</mainClass>
51+
</manifest>
52+
</archive>
53+
</configuration>
54+
</plugin>
55+
</plugins>
56+
</build>
57+
58+
<properties>
59+
<maven.compiler.source>1.8</maven.compiler.source>
60+
<maven.compiler.target>1.8</maven.compiler.target>
61+
</properties>
62+
63+
</project>

‎jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/EnumWriter.java

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
package org.cprover;
2+
3+
import com.cedarsoftware.util.io.JsonWriter;
4+
5+
import java.io.IOException;
6+
import java.io.Writer;
7+
import java.lang.reflect.Field;
8+
import java.lang.reflect.Modifier;
9+
import java.util.Map;
10+
11+
import static com.cedarsoftware.util.io.JsonWriter.JsonClassWriterEx.Support.getWriter;
12+
13+
public class EnumWriter implements JsonWriter.JsonClassWriterEx {
14+
15+
/**
16+
* Writes enums just like regular class types: by writing a key-value pair for all of its fields.
17+
* The difference to the standard way of writing enums in json-io is that the latter ignores the
18+
* ordinal field.
19+
*/
20+
public void write(Object obj, boolean showType, Writer output, Map<String, Object> args)
21+
throws IOException {
22+
JsonWriter outerWriter = getWriter(args);
23+
Enum<?> enumm = (Enum<?>) obj;
24+
output.write("\"name\":\"" + enumm.name() + "\"");
25+
output.write(',');
26+
output.write("\"ordinal\":" + enumm.ordinal());
27+
for (Field field : enumm.getDeclaringClass().getDeclaredFields()) {
28+
if ((field.getModifiers() & Modifier.STATIC) != Modifier.STATIC) {
29+
output.write(",\"" + field.getName() + "\":");
30+
try {
31+
field.setAccessible(true);
32+
outerWriter.writeImpl(field.get(enumm), true, true, true);
33+
}
34+
catch (IllegalAccessException ex) {
35+
System.err.println("Could not access field " + field.getName() + " in class " +
36+
enumm.getDeclaringClass() + ".");
37+
}
38+
}
39+
}
40+
}
41+
}

‎jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/JsonGenerator.java

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
package org.cprover;
2+
3+
import java.io.File;
4+
import java.io.FileWriter;
5+
import java.io.IOException;
6+
import java.lang.reflect.Field;
7+
import java.lang.reflect.Modifier;
8+
import java.util.*;
9+
10+
import com.cedarsoftware.util.io.JsonWriter;
11+
12+
public class JsonGenerator {
13+
14+
/**
15+
* For all *.class files in the current directory, assuming one Java file per class file, write
16+
* the initial values of their static fields to the file clinit-state.json.
17+
*/
18+
public static void main(String[] args) throws ClassNotFoundException, IOException {
19+
File here = new File(System.getProperty("user.dir"));
20+
File jsonFile = new File("clinit-state.json");
21+
StaticFieldMap<StaticFieldMap<Object>> classMap = new StaticFieldMap<>();
22+
for (File file : here.listFiles()) {
23+
if (file.getName().endsWith(".class")) {
24+
String className = classNameFromFile(file);
25+
StaticFieldMap<Object> staticFieldMap = staticFieldMap(Class.forName(className));
26+
if (!staticFieldMap.isEmpty()) {
27+
classMap.put(className, staticFieldMap);
28+
}
29+
}
30+
}
31+
Map<String, Object> jsonArgs = jsonWriterArgs();
32+
String json = JsonWriter.objectToJson(classMap, jsonArgs);
33+
FileWriter writer = new FileWriter(jsonFile);
34+
writer.write(json);
35+
writer.close();
36+
}
37+
38+
public static Map<String, Object> jsonWriterArgs() {
39+
Map<String, Object> args = new HashMap<>();
40+
args.put(JsonWriter.WRITE_LONGS_AS_STRINGS, true);
41+
args.put(JsonWriter.PRETTY_PRINT, true);
42+
43+
// We do not use json-io's shorthands for these types.
44+
Map<String, String> typeNameMap = new HashMap<>();
45+
typeNameMap.put("java.lang.Boolean", "java.lang.Boolean");
46+
typeNameMap.put("java.lang.Byte", "java.lang.Byte");
47+
typeNameMap.put("java.lang.Character", "java.lang.Character");
48+
typeNameMap.put("java.lang.Class", "java.lang.Class");
49+
typeNameMap.put("java.lang.Double", "java.lang.Double");
50+
typeNameMap.put("java.lang.Float", "java.lang.Float");
51+
typeNameMap.put("java.lang.Integer", "java.lang.Integer");
52+
typeNameMap.put("java.lang.Long", "java.lang.Long");
53+
typeNameMap.put("java.lang.Short", "java.lang.Short");
54+
typeNameMap.put("java.lang.String", "java.lang.String");
55+
typeNameMap.put("java.util.Date", "java.util.Date");
56+
args.put(JsonWriter.TYPE_NAME_MAP, typeNameMap);
57+
58+
Map<Class, JsonWriter.JsonClassWriterBase> customWriters = new HashMap<>();
59+
customWriters.put(Enum.class, new EnumWriter());
60+
customWriters.put(String.class, new StringModelWriter());
61+
customWriters.put(StaticFieldMap.class, new StaticFieldMapWriter());
62+
args.put(JsonWriter.CUSTOM_WRITER_MAP, customWriters);
63+
return args;
64+
}
65+
66+
/**
67+
* Assumes that a file MyClass.class contains exactly one Java class called MyClass.
68+
*/
69+
public static String classNameFromFile(File file) {
70+
String fileName = file.getName();
71+
return fileName.substring(0, fileName.length() - 6);
72+
}
73+
74+
public static StaticFieldMap<Object> staticFieldMap(Class<?> clazz) {
75+
StaticFieldMap<Object> staticFields = new StaticFieldMap<>();
76+
for (Field field : getAllStaticFields(clazz)) {
77+
field.setAccessible(true);
78+
try {
79+
if (!field.getName().equals("$assertionsDisabled")) {
80+
staticFields.put(field.getName(), field.get(null));
81+
}
82+
}
83+
catch (IllegalAccessException e) {
84+
System.err.println("Could not access field " + field.getName() + " in class " +
85+
clazz.getName() + ".");
86+
}
87+
}
88+
return staticFields;
89+
}
90+
91+
public static List<Field> getAllStaticFields(Class<?> clazz) {
92+
List<Field> fields = new ArrayList<>();
93+
if (clazz == null) {
94+
return fields;
95+
}
96+
for (Field field : clazz.getDeclaredFields()) {
97+
if ((field.getModifiers() & Modifier.STATIC) == Modifier.STATIC) {
98+
fields.add(field);
99+
}
100+
}
101+
fields.addAll(getAllStaticFields(clazz.getSuperclass()));
102+
for (Class<?> interfaze : clazz.getInterfaces()) {
103+
fields.addAll(getAllStaticFields(interfaze));
104+
}
105+
return fields;
106+
}
107+
}

‎jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StaticFieldMap.java

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
package org.cprover;
2+
3+
import java.util.HashMap;
4+
5+
/**
6+
* A map whose keys are of type String.
7+
* We use this instead of e.g. HashMap and define a custom writer for it because
8+
* json-io prints Maps in a special way that would ignore our custom String
9+
* writer for both the keys and values of the Map. We want to use the custom
10+
* String writer for values but not for keys.
11+
*/
12+
public class StaticFieldMap<V> extends HashMap<String, V> {
13+
}

‎jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StaticFieldMapWriter.java

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
package org.cprover;
2+
3+
import com.cedarsoftware.util.io.JsonWriter;
4+
5+
import java.io.IOException;
6+
import java.io.Writer;
7+
import java.util.Iterator;
8+
import java.util.Map;
9+
10+
import static com.cedarsoftware.util.io.JsonWriter.JsonClassWriterEx.Support.getWriter;
11+
12+
public class StaticFieldMapWriter implements JsonWriter.JsonClassWriterEx {
13+
14+
public void write(Object obj, boolean showType, Writer output, Map<String, Object> args)
15+
throws IOException {
16+
StaticFieldMap<?> map = (StaticFieldMap<?>) obj;
17+
writeHelper(map, output, args);
18+
}
19+
20+
private <V> void writeHelper(StaticFieldMap<V> map, Writer output, Map<String, Object> args)
21+
throws IOException {
22+
JsonWriter outerWriter = getWriter(args);
23+
// Make sure the output is still valid JSON if we (accidentally) try to write an empty map.
24+
if (map.isEmpty()) {
25+
output.write("\"@noFields\": true");
26+
return;
27+
}
28+
Iterator<Map.Entry<String, V>> it = map.entrySet().iterator();
29+
Map.Entry<String, V> entry = it.next();
30+
output.write('"' + entry.getKey() + "\":");
31+
outerWriter.writeImpl(entry.getValue(), true, true, true);
32+
while (it.hasNext()) {
33+
output.write(',');
34+
entry = it.next();
35+
output.write('"' + entry.getKey() + "\":");
36+
outerWriter.writeImpl(entry.getValue(), true, true, true);
37+
}
38+
}
39+
}

‎jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/StringModelWriter.java

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
package org.cprover;
2+
3+
import com.cedarsoftware.util.io.JsonWriter;
4+
5+
import java.io.IOException;
6+
import java.io.Writer;
7+
8+
import static com.cedarsoftware.util.io.JsonWriter.writeJsonUtf8String;
9+
10+
/**
11+
* This duplicates JsonStringWriter from json-io.
12+
* json-io has a check for JsonStringWriter which results in never printing its type.
13+
* We avoid this check by having our own custom writer for strings.
14+
*/
15+
public class StringModelWriter implements JsonWriter.JsonClassWriter {
16+
17+
public void write(Object obj, boolean showType, Writer output) throws IOException {
18+
output.write("\"value\":");
19+
writeJsonUtf8String((String) obj, output);
20+
}
21+
22+
public boolean hasPrimitiveForm() { return true; }
23+
24+
public void writePrimitiveForm(Object o, Writer output) throws IOException {
25+
writeJsonUtf8String((String) o, output);
26+
}
27+
}

0 commit comments

Comments
 (0)