diff --git a/key.core.testgen/build.gradle b/key.core.testgen/build.gradle
index 771d651021a..f7038cc682e 100644
--- a/key.core.testgen/build.gradle
+++ b/key.core.testgen/build.gradle
@@ -2,4 +2,5 @@ description "Test Case Generation based on proof attempts."
dependencies {
implementation project(":key.core")
+ implementation("com.squareup:javapoet:1.13.0")
}
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Assignment.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Assignment.java
deleted file mode 100644
index 190463361a8..00000000000
--- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Assignment.java
+++ /dev/null
@@ -1,69 +0,0 @@
-/* This file is part of KeY - https://key-project.org
- * KeY is licensed under the GNU General Public License Version 2
- * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.testgen;
-
-/**
- * This class creates either assignments or creates calls to setter methods to initiate fields.
- *
- * @author gladisch
- * @author herda
- */
-public class Assignment {
-
-
- protected final String type;
- protected final Object left;
- protected final String right;
-
- public Assignment(String left, String right) {
- type = "";
- this.left = left;
- this.right = right;
- }
-
- /**
- * The argument left of type RefEx must contains all needed information to invoke a setter
- * method.
- */
- public Assignment(RefEx left, String right) {
- type = "";
- this.left = left;
- this.right = right;
- }
-
- public Assignment(String type, Object left, String right) {
- this.type = type;
- this.left = left;
- this.right = right;
- }
-
- @Override
- public String toString() {
- return type + " " + left + " = " + right + ";";
- }
-
- /**
- * @param rfl If this argument is true, then an invokation of a setter method is created,
- * otherwise an assignment is created.
- * @return String representation of an assignment or a call to a setter method.
- */
- public String toString(boolean rfl) {
- if (rfl) {
- if (left instanceof RefEx leftEx) {
- return ReflectionClassCreator.NAME_OF_CLASS + "."
- + ReflectionClassCreator.SET_PREFIX
- + ReflectionClassCreator.cleanTypeName(leftEx.fieldType) + "("
- + leftEx.rcObjType + ".class, " + leftEx.rcObj + ", \"" + leftEx.field + "\", "
- + right + ");";
- } else {
- return type + " " + left + " = " + right + ";";
- }
- } else {
- return type + " " + left + " = " + right + ";";
- }
- }
-
-
-
-}
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Format.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Format.java
new file mode 100644
index 00000000000..32fbb062cc3
--- /dev/null
+++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Format.java
@@ -0,0 +1,5 @@
+package de.uka.ilkd.key.testgen;
+
+public enum Format {
+ Plain, JUnit4, JUnit5, TestNG,
+}
\ No newline at end of file
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java
index 0b66418b71b..4bda83f01c0 100644
--- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java
+++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java
@@ -21,7 +21,7 @@
import de.uka.ilkd.key.settings.ProofDependentSMTSettings;
import de.uka.ilkd.key.settings.ProofIndependentSMTSettings;
import de.uka.ilkd.key.settings.ProofIndependentSettings;
-import de.uka.ilkd.key.settings.TestGenerationSettings;
+import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
import de.uka.ilkd.key.smt.*;
import de.uka.ilkd.key.smt.lang.SMTSort;
import de.uka.ilkd.key.smt.model.Model;
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java
index cc140fd6171..795fb6cc004 100644
--- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java
+++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java
@@ -24,16 +24,11 @@
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
-public class ProofInfo {
+public record ProofInfo(Proof proof, Services services) {
private static final Logger LOGGER = LoggerFactory.getLogger(ProofInfo.class);
- private final Proof proof;
-
- private final Services services;
-
public ProofInfo(Proof proof) {
- this.proof = proof;
- this.services = proof.getServices();
+ this(proof, proof.getServices());
}
public IProgramMethod getMUT() {
@@ -79,7 +74,7 @@ public Term getPreConTerm() {
if (c instanceof FunctionalOperationContract t) {
OriginalVariables orig = t.getOrigVars();
Term post = t.getPre(services.getTypeConverter().getHeapLDT().getHeap(), orig.self,
- orig.params, orig.atPres, services);
+ orig.params, orig.atPres, services);
return post;
}
// no pre <==> false
@@ -170,7 +165,7 @@ private String processUpdate(Term update) {
return "";
}
return " \n" + up.lhs().sort() + " " + up.lhs().toString() + " = " + update.sub(0)
- + ";";
+ + ";";
}
StringBuilder result = new StringBuilder();
for (Term sub : update.subs()) {
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/RefEx.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/RefEx.java
index 79a173dd319..d3ecd9f48d2 100644
--- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/RefEx.java
+++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/RefEx.java
@@ -3,28 +3,17 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.testgen;
+import org.jspecify.annotations.Nullable;
+
/**
- * Reference expression
+ * Reference expression.
+ *
+ * Example: rcObj.field, where rcObjType is the type of rcObj. The prefix "rc" stands for
+ * receiver.
*
* @author gladisch
*/
-public class RefEx {
- public final String rcObjType;
- public final String rcObj;
- public final String fieldType;
- public final String field;
-
- /**
- * Example: rcObj.field, where rcObjType is the type of rcObj. The prefix "rc" stands for
- * receiver.
- */
- public RefEx(String rcObjType, String rcObj, String fieldType, String field) {
- this.rcObjType = rcObjType;
- this.rcObj = rcObj;
- this.fieldType = fieldType;
- this.field = field;
- }
-
+public record RefEx(@Nullable String rcObjType, String rcObj, String fieldType, String field) {
@Override
public String toString() {
if (rcObjType != null && !rcObjType.isEmpty()) {
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java
index de0aaf772bb..91b57c1dc9f 100644
--- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java
+++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java
@@ -3,15 +3,12 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.testgen;
-import java.util.HashSet;
-
+import com.squareup.javapoet.*;
import de.uka.ilkd.key.logic.sort.Sort;
-import de.uka.ilkd.key.util.KeYConstants;
-
-import org.key_project.util.java.StringUtil;
-import org.slf4j.Logger;
-import org.slf4j.LoggerFactory;
+import javax.lang.model.element.Modifier;
+import java.util.HashMap;
+import java.util.HashSet;
/**
* Creates the RFL.java file, that provides setter and getter methods using the reflection API as
@@ -19,14 +16,9 @@
*
* @author mbender
* @author gladisch
+ * @author weigl -- rewrite for javapoet
*/
public class ReflectionClassCreator {
- /**
- * Constant for the line break which is used by the operating system.
- *
- * Do not use {@code \n}!
- */
- public static final String NEW_LINE = StringUtil.NEW_LINE;
public static final String NAME_OF_CLASS = "RFL";
@@ -36,12 +28,10 @@ public class ReflectionClassCreator {
// setter and getter methods will be created for these types.
private static final String[] PRIMITIVE_TYPES =
- { "int", "long", "byte", "char", "boolean", "float", "double" };
+ {"int", "long", "byte", "char", "boolean", "float", "double"};
// Default values for primitive types
- private static final String[] PRIM_TYP_DEF_VAL = { "0", "0", "0", "' '", "false", "0", "0" };
-
- private static final Logger LOGGER = LoggerFactory.getLogger(ReflectionClassCreator.class);
+ private static final String[] PRIM_TYP_DEF_VAL = {"0", "0", "0", "' '", "false", "0", "0"};
private final HashSet usedObjectSorts;
private final HashSet usedObjectSortsStrings;
@@ -56,21 +46,15 @@ public ReflectionClassCreator() {
* Creates the RFL.java file, that provides setter and getter methods using the reflection API
* as well as object creation functions based on the objenesis library.
*/
- public StringBuilder createClass(boolean staticClass) {
+ public TypeSpec createClass(boolean staticClass) {
final HashSet sorts = sortsToString();
- final var result = new StringBuilder();
- result.append(classDecl(staticClass));
- result.append(ghostMapDecls(true));
- result.append(staticInitializer(true));
- result.append(instanceMethod());
- result.append(instances(sorts));
- result.append(getterAndSetter(sorts));
- result.append(footer());
- if (!checkBraces(result)) {
- throw new IllegalStateException("ReflectionClassCreator.createClass(): "
- + "Problem: the number of opening and closing braces of the generated RFL file is not equal!");
- }
- return result;
+ var clazz = classDecl(staticClass);
+ ghostMapDecls(clazz);
+ staticInitializer(true, clazz);
+ instanceMethod(clazz);
+ instances(sorts, clazz);
+ getterAndSetter(sorts, clazz);
+ return clazz.build();
}
/**
@@ -123,142 +107,97 @@ private HashSet sortsToString() {
/**
* @return Beginning of the RFL class
*/
- private StringBuilder classDecl(boolean staticClass) {
- final StringBuilder r = new StringBuilder();
- r.append(NEW_LINE);
- r.append("// This file was generated by KeY Version ").append(KeYConstants.VERSION)
- .append(" (www.key-project.org).").append(NEW_LINE).append(NEW_LINE)
- .append(
- "/** This class enables the test suite to read and write protected and private")
- .append(NEW_LINE)
- .append(
- " * fields of other classes. It can also simulate ghost fields using a hashmap.")
- .append(NEW_LINE)
- .append(
- " * Ghostfields are implicit fields that exist in the specification but not in the")
- .append(NEW_LINE)
- .append(
- " * actual Java class. Futhermore, this class also enables to create an object of ")
- .append(NEW_LINE)
- .append(
- " * any class even if it has no default constructor. To create objects the ")
- .append(NEW_LINE)
- .append(
- " * the objenesis library is required and must be provided when compiling and")
- .append(NEW_LINE).append(" * executing the test suite. ").append(NEW_LINE);
- r.append(" * @see http://docs.oracle.com/javase/tutorial/reflect/member/ctorInstance.html")
- .append(NEW_LINE);
- r.append(" * @see http://code.google.com/p/objenesis/").append(NEW_LINE)
- .append(" * @see http://objenesis.org/").append(NEW_LINE);
- r.append(" * @author gladisch").append(NEW_LINE);
- r.append(" * @author mbender").append(NEW_LINE);
- r.append(" */").append(NEW_LINE);
- r.append("public ");
- if (staticClass) {
- r.append("static ");
- }
- r.append("class " + NAME_OF_CLASS + " {").append(NEW_LINE);
- return r;
+ private TypeSpec.Builder classDecl(boolean staticClass) {
+ var tb = TypeSpec.classBuilder(NAME_OF_CLASS);
+ tb.addModifiers(Modifier.PUBLIC);
+ if (staticClass) tb.addModifiers(Modifier.STATIC);
+ tb.addJavadoc("""
+ // This file was generated by KeY Version %s (www.key-project.org).
+ /** This class enables the test suite to read and write protected and private
+ * fields of other classes. It can also simulate ghost fields using a hashmap.
+ * Ghostfields are implicit fields that exist in the specification but not in the
+ * actual Java class. Futhermore, this class also enables to create an object of
+ * any class even if it has no default constructor. To create objects the
+ * the objenesis library is required and must be provided when compiling and
+ * executing the test suite. * @see http://docs.oracle.com/javase/tutorial/reflect/member/ctorInstance.html
+ * @see http://code.google.com/p/objenesis
+ * @see http://objenesis.org/
+ * @author gladisch").append(NEW_LINE);
+ * @author mbender").append(NEW_LINE);
+ */""");
+ return tb;
}
/**
* Writes a hashmap and a utility method for associating ghost/model fiels with objects.
*
- * @param ghostMapActive becomes are runtime flag that determins if the hashmap should be
- * enabled or not.
+ * @param clazz a builder to append the necessary declarations
*/
- private StringBuilder ghostMapDecls(boolean ghostMapActive) {
- final StringBuilder r = new StringBuilder();
- r.append(NEW_LINE);
-
- r.append(" private static final String NoSuchFieldExceptionText;");
-
- r.append(" public static boolean ghostMapActive;");
-
- r.append(" public static java.util.HashMap ghostModelFields;")
- .append(NEW_LINE).append(NEW_LINE);
-
- r.append(" public static int getHash(Class c, Object obj, String attr){")
- .append(NEW_LINE);
- r.append(" return c.hashCode() * (obj!=null?obj.hashCode():1) * attr.hashCode();")
- .append(NEW_LINE);
- r.append(" }").append(NEW_LINE).append(NEW_LINE);
- return r;
+ private void ghostMapDecls(TypeSpec.Builder clazz) {
+ clazz.addField(String.class, "NoSuchFieldExceptionText", Modifier.PUBLIC, Modifier.STATIC);
+ clazz.addField(Boolean.TYPE, "ghostMapActive", Modifier.PUBLIC, Modifier.STATIC);
+ clazz.addField(ParameterizedTypeName.get(HashMap.class, Integer.class, Object.class),
+ "ghostModelFields",
+ Modifier.PUBLIC, Modifier.STATIC);
+ clazz.addMethod(MethodSpec.methodBuilder("getHash")
+ .addModifiers(Modifier.PUBLIC, Modifier.STATIC)
+ .addParameter(Class.class, "c")
+ .addParameter(Object.class, "obj")
+ .addParameter(String.class, "attr")
+ .addStatement("return c.hashCode() * (obj!=null?obj.hashCode():1) * attr.hashCode();")
+ .build());
}
/**
- * @return The method that allows to create new instances
+ * The method that allows to create new instances
*/
- private StringBuilder instanceMethod() {
- final StringBuilder r = new StringBuilder();
- r.append(NEW_LINE).append(NEW_LINE);
- r.append(
- " /** The Objenesis library can create instances of classes that have no default constructor. */")
- .append(NEW_LINE);
- r.append(" private static org.objenesis.Objenesis objenesis;").append(NEW_LINE)
- .append(NEW_LINE);
- r.append(" private static Object newInstance(Class c) throws Exception {")
- .append(NEW_LINE);
- r.append(" Object res=objenesis.newInstance(c);").append(NEW_LINE);
- r.append(" if (res==null)").append(NEW_LINE);
- r.append(" throw new Exception(\"Couldn't create instance of class:\"+c);")
- .append(NEW_LINE);
- r.append(" return res;").append(NEW_LINE);
- r.append(" }").append(NEW_LINE);
- return r;
+ private void instanceMethod(TypeSpec.Builder clazz) {
+ clazz.addField(ClassName.get("org.objenesis", "Objenesis"), "objenesis");
+ var ms = MethodSpec.methodBuilder("newInstance")
+ .addModifiers(Modifier.PUBLIC, Modifier.STATIC)
+ .returns(Object.class)
+ .addParameter(Class.class, "c")
+ .addException(Exception.class)
+ .addJavadoc("The Objenesis library can create instances of classes that have no default constructor.")
+ .addStatement("Object res=objenesis.newInstance(c);")
+ .beginControlFlow("if (res==null)")
+ .addStatement("throw new Exception($S+c);", "Couldn't create instance of class: ")
+ .endControlFlow()
+ .addStatement("return res;");
+ clazz.addMethod(ms.build());
}
- private StringBuilder staticInitializer(boolean ghostMapActive) {
- StringBuilder r = new StringBuilder();
- String tab = " ";
- r.append(NEW_LINE).append(NEW_LINE);
- r.append(tab).append("static{").append(NEW_LINE);
-
- r.append(tab).append("objenesis = new org.objenesis.ObjenesisStd();").append(NEW_LINE);
-
- r.append(tab).append("ghostMapActive = ").append(ghostMapActive).append(";")
- .append(NEW_LINE);
-
- r.append(tab).append("ghostModelFields = new java.util.HashMap();")
- .append(NEW_LINE);
-
- r.append(tab).append("NoSuchFieldExceptionText =").append(NEW_LINE);
- r.append(tab).append(tab).append(
- " \"This exception occurs when ghost fields or model fields are used in the code or \" +")
- .append(NEW_LINE);
- r.append(tab).append(tab).append(
- " \"if mock objects are used that have different fields, than the real objects. \" +")
- .append(NEW_LINE);
- r.append(tab).append(tab).append(
- " \"The tester should extend the handling of such fields in this generated utility class RFL.java.\";")
- .append(NEW_LINE);
-
- r.append("}").append(NEW_LINE).append(NEW_LINE);
-
- return r;
+ private void staticInitializer(boolean ghostMapActive, TypeSpec.Builder clazz) {
+ clazz.addStaticBlock(
+ CodeBlock.builder()
+ .addStatement("objenesis = new org.objenesis.ObjenesisStd();")
+ .add("ghostMapActive = $L;", ghostMapActive)
+ .add("ghostModelFields = new java.util.HashMap();")
+ .add("NoSuchFieldExceptionText =")
+ .addStatement("/*This exception occurs when ghost fields or model fields are used in " +
+ "the code or if mock objects are used that have different fields, than the real objects." +
+ "The tester should extend the handling of such fields in this generated utility class RFL.java.*/;)"
+ ).build()
+ );
}
/**
- * @param sorts
- * @return All calls to create objects for the given sorts
+ * All calls to create objects for the given sorts
*/
- private StringBuilder instances(final HashSet sorts) {
- final StringBuilder r = new StringBuilder();
- r.append(NEW_LINE).append(" // ---The methods for object creation---").append(NEW_LINE)
- .append(NEW_LINE);
+ private void instances(final HashSet sorts, TypeSpec.Builder clazz) {
+ //r.append(NEW_LINE).append(" // ---The methods for object creation---").append(NEW_LINE)
+ // .append(NEW_LINE);
for (final String sort : sorts) {
- r.append(newRef(sort));
+ clazz.addMethod(newRef(sort));
}
- r.append(NEW_LINE);
- return r;
}
/**
* @return The call to create an object of given type
*/
- private StringBuilder newRef(final String sort) {
+ private MethodSpec newRef(final String sort) {
if (sort.indexOf('[') != -1) {
- return newArray(sort);
+ return newArrayField(sort);
} else {
return newInstance(sort);
}
@@ -290,34 +229,28 @@ public static String cleanTypeName(String s) {
* @param sort
* @return The call to create an object of given type
*/
- private StringBuilder newInstance(final String sort) {
- final StringBuilder r = new StringBuilder();
- r.append(NEW_LINE);
- r.append(" public static ").append(sort).append(" new").append(cleanTypeName(sort))
- .append("() throws java.lang.RuntimeException {").append(NEW_LINE);
- r.append(" try{").append(NEW_LINE);
- r.append(" return (").append(sort).append(")newInstance(").append(sort)
- .append(".class);").append(NEW_LINE);
- r.append(" } catch (java.lang.Throwable e) {").append(NEW_LINE);
- r.append(" throw new java.lang.RuntimeException(e);").append(NEW_LINE);
- r.append(" }").append(NEW_LINE);
- r.append(" }").append(NEW_LINE);
- return r;
+ private MethodSpec newInstance(final String sort) {
+ String methodName = cleanTypeName(sort);
+ ClassName returnType = ClassName.get("", sort);
+ return MethodSpec.methodBuilder(methodName)
+ .returns(returnType)
+ .addException(RuntimeException.class)
+ .addStatement("try{ return ($N) newInstance($N.class); } " +
+ "catch (java.lang.Throwable e) { throw new java.lang.RuntimeException(e); }",
+ returnType)
+ .build();
}
/**
* @param sort
* @return The call to create an Array of given type
*/
- private StringBuilder newArray(final String sort) {
- final StringBuilder r = new StringBuilder();
- r.append(NEW_LINE);
- r.append(" public static ").append(sort).append(" new").append(cleanTypeName(sort))
- .append("(int dim){").append(NEW_LINE);
- r.append(" return new ").append(sort.substring(0, sort.length() - 2)).append("[dim];")
- .append(NEW_LINE);
- r.append(" }").append(NEW_LINE);
- return r;
+ private MethodSpec newArrayField(final String sort) {
+ String typeName = cleanTypeName(sort);
+ String substring = sort.substring(0, sort.length() - 2);
+ return MethodSpec.methodBuilder("new" + typeName)
+ .addStatement("return new $N[dim];", substring)
+ .build();
}
private boolean isPrimitiveType(String sort) {
@@ -329,52 +262,45 @@ private boolean isPrimitiveType(String sort) {
return false;
}
- private StringBuilder getterAndSetter(final HashSet sorts) {
- final StringBuilder result = new StringBuilder();
- result.append(NEW_LINE).append(" // ---Getter and setter for primitive types---")
- .append(NEW_LINE);
+ private void getterAndSetter(final HashSet sorts, TypeSpec.Builder clazz) {
for (int i = 0; i < 7; i++) {
- result.append(NEW_LINE);
- result.append(declareSetter(PRIMITIVE_TYPES[i], true));
- result.append(declareGetter(PRIMITIVE_TYPES[i], PRIM_TYP_DEF_VAL[i], true));
+ clazz.addMethod(declareSetter(PRIMITIVE_TYPES[i], true));
+ clazz.addMethod(declareGetter(PRIMITIVE_TYPES[i], PRIM_TYP_DEF_VAL[i], true));
}
- result.append(NEW_LINE);
- result.append(NEW_LINE).append(" // ---Getter and setter for Reference types---")
- .append(NEW_LINE);
for (final String sort : sorts) {
- result.append(NEW_LINE);
- result.append(declareSetter(sort, false));
- result.append(declareGetter(sort, "null", false));
+ clazz.addMethod(declareSetter(sort, false));
+ clazz.addMethod(declareGetter(sort, "null", false));
}
- return result;
}
- private StringBuilder declareSetter(final String sort, final boolean prim) {
- final StringBuilder r = new StringBuilder();
- final String cmd =
- " " + (prim
- ? "f.set" + Character.toUpperCase(sort.charAt(0)) + sort.substring(1)
- + "(obj, val);" + NEW_LINE
- : "f.set(obj, val);" + NEW_LINE);
- r.append(NEW_LINE);
- r.append(" public static void " + SET_PREFIX).append(cleanTypeName(sort))
- .append("(Class c, Object obj, String attr, ").append(sort)
- .append(" val) throws RuntimeException{").append(NEW_LINE);
- r.append(" try {").append(NEW_LINE);
- r.append(" java.lang.reflect.Field f = c.getDeclaredField(attr);").append(NEW_LINE);
- r.append(" f.setAccessible(true);").append(NEW_LINE);
- r.append(cmd);
- r.append(" } catch(NoSuchFieldException e) {").append(NEW_LINE);
- r.append(" if(ghostMapActive)").append(NEW_LINE);
- r.append(" ghostModelFields.put(getHash(c,obj,attr), val);").append(NEW_LINE);
- r.append(" else").append(NEW_LINE);
- r.append(" throw new RuntimeException(e.toString() + NoSuchFieldExceptionText);")
- .append(NEW_LINE);
- r.append(" } catch(Exception e) {").append(NEW_LINE);
- r.append(" throw new RuntimeException(e);").append(NEW_LINE);
- r.append(" }").append(NEW_LINE);
- r.append(" }").append(NEW_LINE);
- return r;
+ private MethodSpec declareSetter(final String sort, final boolean prim) {
+
+ var retType = ClassName.get("", sort);
+ var ms = MethodSpec.methodBuilder(SET_PREFIX + cleanTypeName(sort))
+ .addParameter(Class.class, "c")
+ .addParameter(TypeName.OBJECT, "obj")
+ .addParameter(String.class, "attr")
+ .addParameter(retType, "val")
+ .beginControlFlow("try")
+ .addStatement("$T f = c.getDeclaredField(attr);", java.lang.reflect.Field.class)
+ .addStatement("f.setAccessible(true);");
+
+ if (prim)
+ ms.addStatement("f.set" + Character.toUpperCase(sort.charAt(0)) + sort.substring(1)
+ + "(obj, val);");
+ else
+ ms.addStatement("f.set(obj, val);");
+
+ ms.nextControlFlow("catch(NoSuchFieldException e)")
+ .beginControlFlow("if(ghostMapActive)")
+ .addStatement("ghostModelFields.put(getHash(c,obj,attr), val);")
+ .nextControlFlow("else")
+ .addStatement("throw new RuntimeException(e.toString() + NoSuchFieldExceptionText);")
+ .endControlFlow()
+ .nextControlFlow("catch(Exception e)")
+ .addStatement("throw new RuntimeException(e);")
+ .endControlFlow();
+ return ms.build();
}
private String primToWrapClass(String sort) {
@@ -387,64 +313,31 @@ private String primToWrapClass(String sort) {
}
}
- private StringBuilder declareGetter(final String sort, final String def, final boolean prim) {
- final StringBuilder r = new StringBuilder();
- final String cmd =
- " " + (prim
- ? "return f.get" + Character.toUpperCase(sort.charAt(0)) + sort.substring(1)
- + "(obj);" + NEW_LINE
- : "return (" + sort + ") f.get(obj);" + NEW_LINE);
- r.append(NEW_LINE);
- r.append(" public static ").append(sort).append(" ").append(GET_PREFIX)
- .append(cleanTypeName(sort))
- .append("(Class c, Object obj, String attr) throws RuntimeException{")
- .append(NEW_LINE);
- r.append(" ").append(sort).append(" res = ").append(def).append(";").append(NEW_LINE);
- r.append(" try {").append(NEW_LINE);
- r.append(" java.lang.reflect.Field f = c.getDeclaredField(attr);").append(NEW_LINE);
- r.append(" f.setAccessible(true);").append(NEW_LINE);
- r.append(cmd);
- r.append(" } catch(NoSuchFieldException e) {").append(NEW_LINE);
- r.append(" return (").append(prim ? primToWrapClass(sort) : sort)
- .append(")ghostModelFields.get(getHash(c,obj,attr));").append(NEW_LINE);
- r.append(" } catch(Exception e) {").append(NEW_LINE);
- r.append(" throw new RuntimeException(e);").append(NEW_LINE);
- r.append(" }").append(NEW_LINE);
- r.append(" }").append(NEW_LINE);
- return r;
+ private MethodSpec declareGetter(final String sort, final String def, final boolean prim) {
+ var retType = ClassName.get("", sort);
+ var ms = MethodSpec.methodBuilder(GET_PREFIX + cleanTypeName(sort))
+ .returns(retType)
+ .addParameter(Class.class, "c")
+ .addParameter(TypeName.OBJECT, "obj")
+ .addParameter(String.class, "attr")
+ .addStatement("rest = $L;", def)
+ .beginControlFlow("try")
+ .addStatement("$T f = c.getDeclaredField(attr);", java.lang.reflect.Field.class)
+ .addStatement("f.setAccessible(true);");
+
+ if (prim)
+ ms.addStatement("return f.get" + Character.toUpperCase(sort.charAt(0))
+ + sort.substring(1) + "(obj);");
+ else
+ ms.addStatement("return ($N) f.get(obj);", retType);
+
+ ms.nextControlFlow("catch($N e)", NoSuchFieldException.class);
+ ms.addStatement(prim ? primToWrapClass(sort) : sort);
+ ms.addStatement("ghostModelFields.get(getHash(c,obj,attr));");
+ ms.nextControlFlow("catch(Exception e)");
+ ms.addStatement("throw new RuntimeException(e);");
+ ms.endControlFlow();
+
+ return ms.build();
}
-
- /**
- * @return the closing bracket and a newline for the end of the class
- */
- private String footer() {
- return "}" + NEW_LINE;
- }
-
- /**
- * Sanity check. Checks if number of opening and closing braces is equal.
- */
- private boolean checkBraces(final StringBuilder buf) {
- int curly = 0;
- int round = 0;
- int edged = 0;
- for (int i = 0; i < buf.length(); i++) {
- switch (buf.charAt(i)) {
- case '{' -> curly++;
- case '}' -> curly--;
- case '(' -> round++;
- case ')' -> round--;
- case '[' -> edged++;
- case ']' -> edged--;
- }
- }
- if (curly == 0 && round == 0 && edged == 0) {
- return true;
- } else {
- LOGGER.error("Error braces in RFL.java: curly: {} round: {}: egded: {}", curly, round,
- edged);
- return false;
- }
- }
-
}
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGMain.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGMain.java
new file mode 100644
index 00000000000..edee09ef533
--- /dev/null
+++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGMain.java
@@ -0,0 +1,96 @@
+package de.uka.ilkd.key.testgen;
+
+import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.macros.ProofMacroFinishedInfo;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
+import de.uka.ilkd.key.prover.ProverTaskListener;
+import de.uka.ilkd.key.prover.TaskStartedInfo;
+import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo;
+import de.uka.ilkd.key.settings.DefaultSMTSettings;
+import de.uka.ilkd.key.settings.NewSMTTranslationSettings;
+import de.uka.ilkd.key.settings.ProofDependentSMTSettings;
+import de.uka.ilkd.key.settings.ProofIndependentSMTSettings;
+import de.uka.ilkd.key.smt.SMTProblem;
+import de.uka.ilkd.key.smt.SMTSolver;
+import de.uka.ilkd.key.smt.SolverLauncher;
+import de.uka.ilkd.key.smt.SolverLauncherListener;
+import de.uka.ilkd.key.smt.solvertypes.SolverType;
+import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
+import de.uka.ilkd.key.testgen.macros.SemanticsBlastingMacro;
+import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLog;
+import de.uka.ilkd.key.testgen.template.Templates;
+
+import java.io.File;
+import java.io.IOException;
+import java.util.Collection;
+import java.util.List;
+
+public class TGMain {
+ public static void main(String[] args) throws ProblemLoaderException, InterruptedException {
+ SolverTypes.Z3_CE_SOLVER.checkForSupport();
+
+ var env = KeYEnvironment.load(new File(args[0]));
+ TestGenerationLog log = new TestGenerationLog() {
+ @Override
+ public void writeln(String string) {
+ System.out.println(string);
+ }
+
+ @Override
+ public void write(String string) {
+ System.out.print(string);
+ }
+
+ @Override
+ public void writeException(Throwable t) {
+ t.printStackTrace();
+ }
+
+ @Override
+ public void testGenerationCompleted() {
+ System.out.println("Completed!");
+ }
+ };
+
+ Proof proof = env.getLoadedProof();
+ final TestCaseGenerator tg = new TestCaseGenerator(proof, Templates.TEMPLATE_JUNIT4);
+ tg.setLogger(log);
+
+
+ NewSMTTranslationSettings newSettings = new NewSMTTranslationSettings();
+ ProofDependentSMTSettings pdSettings = ProofDependentSMTSettings.getDefaultSettingsData();
+ ProofIndependentSMTSettings piSettings = ProofIndependentSMTSettings.getDefaultSettingsData();
+ final var smtSettings = new DefaultSMTSettings(pdSettings, piSettings, newSettings, proof);
+ var launcher = new SolverLauncher(smtSettings);
+ launcher.addListener(new SolverLauncherListener() {
+ @Override
+ public void launcherStopped(SolverLauncher launcher,
+ Collection finishedSolvers) {
+ try {
+ tg.generateJUnitTestSuite(finishedSolvers);
+ if (tg.isJunit()) {
+ log.writeln("Compile the generated files using a Java compiler.");
+ } else {
+ log.writeln("Compile and run the file with openjml!");
+ }
+ } catch (IOException e) {
+ e.printStackTrace();
+ }
+ }
+
+ @Override
+ public void launcherStarted(Collection problems,
+ Collection solverTypes, SolverLauncher launcher) {
+ }
+ });
+ var solvers = List.of(SolverTypes.Z3_CE_SOLVER);
+ final SemanticsBlastingMacro macro = new SemanticsBlastingMacro();
+ var info = ProofMacroFinishedInfo.getDefaultInfo(macro, proof);
+ final ProverTaskListener ptl = env.getUi().getProofControl().getDefaultProverTaskListener();
+ ptl.taskStarted(new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Macro, macro.getName(), 0));
+ info = macro.applyTo(env.getUi(), proof, proof.openEnabledGoals(), null, ptl);
+ final Collection problems = SMTProblem.createSMTProblems(proof);
+ launcher.launch(solvers, problems, proof.getServices());
+ }
+}
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java
index e9b17899bd5..d18c80c7d84 100644
--- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java
+++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java
@@ -4,15 +4,19 @@
package de.uka.ilkd.key.testgen;
import java.io.*;
-import java.nio.charset.StandardCharsets;
+import java.nio.file.*;
+import java.nio.file.attribute.BasicFileAttributes;
import java.util.*;
+import java.util.concurrent.atomic.AtomicInteger;
+import com.squareup.javapoet.*;
import de.uka.ilkd.key.java.JavaInfo;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
import de.uka.ilkd.key.java.declaration.MethodDeclaration;
import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
import de.uka.ilkd.key.java.declaration.VariableSpecification;
+import de.uka.ilkd.key.java.reference.TypeReference;
import de.uka.ilkd.key.ldt.HeapLDT;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
@@ -21,22 +25,29 @@
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.settings.ProofIndependentSettings;
-import de.uka.ilkd.key.settings.TestGenerationSettings;
+import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
import de.uka.ilkd.key.smt.SMTSolver;
import de.uka.ilkd.key.smt.model.Heap;
import de.uka.ilkd.key.smt.model.Model;
import de.uka.ilkd.key.smt.model.ObjectVal;
-import de.uka.ilkd.key.smt.testgen.TestGenerationLog;
+import de.uka.ilkd.key.testgen.smt.testgen.MemoryTestGenerationLog;
+import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLog;
import de.uka.ilkd.key.testgen.oracle.OracleGenerator;
-import de.uka.ilkd.key.testgen.oracle.OracleMethod;
import de.uka.ilkd.key.testgen.oracle.OracleMethodCall;
+import de.uka.ilkd.key.testgen.template.Template;
import de.uka.ilkd.key.util.KeYConstants;
+import org.jspecify.annotations.Nullable;
import org.key_project.util.java.StringUtil;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
+import javax.lang.model.element.Modifier;
+
+import static de.uka.ilkd.key.testgen.TestgenUtils.*;
+import static de.uka.ilkd.key.testgen.template.Constants.*;
+
/**
* @author gladisch
* @author herda
@@ -49,161 +60,77 @@ public class TestCaseGenerator {
private static final Logger LOGGER = LoggerFactory.getLogger(TestCaseGenerator.class);
+ private static final AtomicInteger FILE_COUNTER = new AtomicInteger();
+
/**
- * Constant for the line break which is used by the operating system.
- *
- * Do not use {@code \n}!
+ * Classes of the Java environment needed by KeY can be placed in this subdirectory.
*/
- public static final String NEW_LINE = StringUtil.NEW_LINE;
-
- private static final String NULLABLE = "/*@ nullable */";
- public static final String ALL_OBJECTS = "allObjects";
- public static final String ALL_INTS = "allInts";
- public static final String ALL_BOOLS = "allBools";
- public static final String ALL_HEAPS = "allHeaps";
- public static final String ALL_FIELDS = "allFields";
- public static final String ALL_SEQ = "allSeq";
- public static final String ALL_LOCSETS = "allLocSets";
-
- public static final String OBJENESIS_NAME = "objenesis-2.2.jar";
+ public static final String DONT_COPY = "aux";
+ private static final ClassName JUNIT4_TEST_ANNOTATION = ClassName.get("org.junit", "Test");
+ private static final ClassName JUNIT5_TEST_ANNOTATION = ClassName.get("org.junit.jupiter.api", "Test");
+ private static final ClassName TESTNG_TEST_ANNOTATION = ClassName.get("org.junit", "Test");
- public static final String OLDMap = "old";
- public static final String TAB = " ";
private final Services services;
- static int fileCounter = 0;
- private final boolean junitFormat;
- private static final String DONT_COPY = "aux"; // Classes of the Java
- // environment needed by KeY
- // can be placed in this
- // subdirectory.
-
- public static boolean modelIsOK(Model m) {
- return m != null && !m.isEmpty() && m.getHeaps() != null && m.getHeaps().size() > 0
- && m.getTypes() != null;
- }
+ private final Template template;
+ private final Format format;
private final boolean rflAsInternalClass;
- protected final boolean useRFL;
- protected final ReflectionClassCreator rflCreator;
- private final String dontCopy;
- protected final String modDir;
- protected final String directory;
- private TestGenerationLog logger;
- private String fileName;
+ private final boolean useRFL;
+ private final AssignmentCreator assignmentCreator;
+ private final ReflectionClassCreator rflCreator;
+ private final String modDirName;
+ private final Path outputFolder;
+ private final Path outputModDir;
+ private final Path outputDontCopy;
+
+ private TestGenerationLog logger = new MemoryTestGenerationLog();
+ @Nullable
+ private String fileName = "TestGeneric" + TestCaseGenerator.FILE_COUNTER;
+ @Nullable
private String packageName;
private final String mutName;
private final ProofInfo info;
private final OracleGenerator oracleGenerator;
- private List oracleMethods;
+ private List oracleMethods = new ArrayList<>(0);
+ @Nullable
private String oracleMethodCall;
- private final Map sortDummyClass;
- final String dummyPostfix = "DummyImpl";
-
- // TODO: in future remove this string and provide the file in the
- // KeY-project
- private String compileWithOpenJML =
- "#!/bin/bash" + NEW_LINE + NEW_LINE + "if [ -e \"openjml.jar\" ]" + NEW_LINE + "then"
- + NEW_LINE + " java -jar openjml.jar -cp \".\" -rac *" + JAVA_FILE_EXTENSION_WITH_DOT
- + NEW_LINE + "else" + NEW_LINE + " echo \"openjml.jar not found!\"" + NEW_LINE
- + " echo \"Download openJML from http://sourceforge.net/projects/jmlspecs/files/\""
- + NEW_LINE + " echo \"Copy openjml.jar into the directory with test files.\""
- + NEW_LINE + "fi" + NEW_LINE;
-
- private String createCompileWithOpenJML(String openJMLPath, String objenesisPath) {
- return "#!/bin/bash" + NEW_LINE + NEW_LINE + "if [ -e \"" + openJMLPath + File.separator
- + "openjml.jar\" ] " + NEW_LINE + "then" + NEW_LINE + " if [ -e \"" + objenesisPath
- + File.separator + OBJENESIS_NAME + "\" ]" + NEW_LINE + " then" + NEW_LINE
- + " java -jar " + openJMLPath + File.separator + "openjml.jar -cp \"."
- + objenesisPath + File.separator + OBJENESIS_NAME + "\" -rac *"
- + JAVA_FILE_EXTENSION_WITH_DOT + NEW_LINE + " else" + NEW_LINE
- + " echo \"objenesis-2.2.jar not found!\"" + NEW_LINE + " fi" + NEW_LINE + "else"
- + NEW_LINE + " echo \"openjml.jar not found!\"" + NEW_LINE
-
- + " echo \"Download openJML from http://sourceforge.net/projects/jmlspecs/files/\""
- + NEW_LINE + " echo \"Copy openjml.jar into the directory with test files.\""
- + NEW_LINE + "fi" + NEW_LINE;
- }
+ private final Set sortDummyClass = new HashSet<>();
+ private final List dummyClasses = new ArrayList<>(8);
- // TODO: in future remove this string and provide the file in the
- // KeY-project
- private final String executeWithOpenJML;
-
- private String createExecuteWithOpenJML(String path, String objenesisPath) {
- return "#!/bin/bash" + NEW_LINE + "if [ -e \"" + path + File.separator
- + "jmlruntime.jar\" ]" + NEW_LINE + "then" + " if [ -e \"" + path + File.separator
- + "jmlspecs.jar\" ]" + NEW_LINE + " then" + NEW_LINE + " if [ -e \""
- + objenesisPath + File.separator + OBJENESIS_NAME + "\" ]" + NEW_LINE + " then"
- + NEW_LINE + " if [ \"$1\" = \"\" ] ; then" + NEW_LINE
- + " echo \"Provide the test driver as an argument (without "
- + JAVA_FILE_EXTENSION_WITH_DOT + " postfix). For example:\"" + NEW_LINE
- + " echo \" executeWithOpenJML.sh TestGeneric0 \"" + NEW_LINE
- + " echo \"Make sure that jmlruntime.jar and jmlspecs.jar are in the\""
- + NEW_LINE + " echo \"current directory.\"" + NEW_LINE + " quit"
- + NEW_LINE + " else" + NEW_LINE + " java -cp " + objenesisPath
- + File.separator + OBJENESIS_NAME + ":" + path + File.separator + "jmlruntime.jar:"
- + path + File.separator + "jmlspecs.jar:. $1" + NEW_LINE + " fi" + NEW_LINE
- + " else" + NEW_LINE + " echo \"objenesis-2.2.jar not found!\"" + NEW_LINE
- + " fi" + NEW_LINE + "else" + NEW_LINE + " echo \"jmlspecs.jar not found!\""
- + NEW_LINE
- + " echo \"Download openJML from http://sourceforge.net/projects/jmlspecs/files/\""
- + NEW_LINE + " echo \"Copy jmlspecs.jar into the directory with test files.\""
- + NEW_LINE + " quit" + NEW_LINE + "fi" + NEW_LINE + "else" + NEW_LINE
- + " echo \"jmlruntime.jar not found!\"" + NEW_LINE
- + " echo \"Download openJML from http://sourceforge.net/projects/jmlspecs/files/\""
- + NEW_LINE + " echo \"Copy jmlruntime.jar into the directory with test files.\""
- + NEW_LINE + " quit" + NEW_LINE + "fi" + NEW_LINE;
- }
+ private final TestGenerationSettings settings;
- public TestCaseGenerator(Proof proof) {
- this(proof, false);
+
+ public TestCaseGenerator(Proof proof, Template template) {
+ this(proof, template, false);
}
- public TestCaseGenerator(Proof proof, boolean rflAsInternalClass) {
- super();
+ public TestCaseGenerator(Proof proof, Template template, boolean rflAsInternalClass) {
+ this.template = template;
this.rflAsInternalClass = rflAsInternalClass;
- final TestGenerationSettings settings = TestGenerationSettings.getInstance();
+ settings = TestGenerationSettings.getInstance();
services = proof.getServices();
- junitFormat = settings.useJunit();
+ format = settings.useJunit();
useRFL = settings.useRFL();
- modDir = computeProjectSubPath(services.getJavaModel().getModelDir());
- dontCopy = modDir + File.separator + TestCaseGenerator.DONT_COPY;
- directory = settings.getOutputFolderPath();
- sortDummyClass = new HashMap<>();
+ assignmentCreator = useRFL
+ ? TestgenUtils::createAssignmentWithRfl
+ : TestgenUtils::createAssignmentWithoutRfl;
+
+ modDirName = services.getJavaModel().getModelDir();
+ outputFolder = Paths.get(settings.getOutputFolderPath());
+ outputModDir = outputFolder.resolve(modDirName);
+ outputDontCopy = outputModDir.resolve(TestCaseGenerator.DONT_COPY);
+
info = new ProofInfo(proof);
mutName = info.getMUT().getFullName();
rflCreator = new ReflectionClassCreator();
- executeWithOpenJML =
- createExecuteWithOpenJML(settings.getOpenjmlPath(), settings.getObjenesisPath());
- compileWithOpenJML =
- createCompileWithOpenJML(settings.getOpenjmlPath(), settings.getObjenesisPath());
oracleGenerator = new OracleGenerator(services, rflCreator, useRFL);
- if (junitFormat) {
+ if (format == Format.JUnit4) {
oracleMethods = new LinkedList<>();
oracleMethodCall = getOracleAssertion(oracleMethods);
}
}
- /**
- * Computes the project specific sub path of the output directory ({@link #directory}) in which
- * the generated files will be stored.
- *
- * @param modelDir The path to the source files of the performed {@link Proof}.
- * @return The computed sub path.
- */
- protected String computeProjectSubPath(String modelDir) {
- if (modelDir.startsWith("/")) {
- return modelDir;
- } else {
- int index = modelDir.indexOf(File.separator);
- if (index >= 0) {
- return modelDir.substring(index); // Remove drive letter, e.g. Microsoft Windows
- } else {
- return modelDir;
- }
- }
- }
-
public String getMUTCall() {
IProgramMethod m = info.getMUT();
String name = m.getFullName();
@@ -214,7 +141,7 @@ public String getMUTCall() {
params.append(",").append(var.name());
}
}
- if (params.length() > 0) {
+ if (!params.isEmpty()) {
params = new StringBuilder(params.substring(1));
}
@@ -233,24 +160,18 @@ public String getMUTCall() {
}
}
- protected String buildDummyClassForAbstractSort(Sort sort) {
+ public String buildDummyClassForAbstractSort(Sort sort) {
final JavaInfo jinfo = services.getJavaInfo();
final KeYJavaType kjt = jinfo.getKeYJavaType(sort);
final String className = getDummyClassNameFor(sort);
- if (sortDummyClass.containsKey(sort)) {
+ if (!sortDummyClass.add(sort)) {
return className;
}
- final var sb = new StringBuilder();
- sortDummyClass.put(sort, sb);
- // Put the string buffer as soon as possible, due to possible recursive calls of this
- // method.
- sb.append("import ").append(sort.declarationString()).append(";").append(NEW_LINE)
- .append(NEW_LINE);
- sb.append("class ").append(className).append(" implements ")
- .append(sort.declarationString()).append("{").append(NEW_LINE);
+
+ var clazz = TypeSpec.classBuilder(className);
+ //sb.append("import ").append(sort.declarationString()).append(";\n\n");
+ clazz.addSuperinterface(ClassName.get("", sort.declarationString()));
// TODO:extends or implements depending if it is a class or interface.
- sb.append(" public ").append(className).append("(){ };").append(NEW_LINE); // default
- // constructor
for (IProgramMethod m : jinfo.getAllProgramMethods(kjt)) {
if (m.getFullName().indexOf('<') > -1) {
@@ -259,157 +180,107 @@ protected String buildDummyClassForAbstractSort(Sort sort) {
if (m.isPrivate() || m.isFinal() || !m.isAbstract()) {
continue;
}
- sb.append(" ");
final MethodDeclaration md = m.getMethodDeclaration();
-
- if (m.isProtected()) {
- sb.append("protected ");
- }
- if (m.isPublic()) {
- sb.append("public ");
- }
- if (m.isFinal()) {
- sb.append("final "); // Is this possible?
- }
- if (m.isStatic()) {
- sb.append("static ");
- }
- if (m.isSynchronized()) {
- sb.append("synchronized ");
- }
- if (md.getTypeReference() == null) {
- sb.append("void ");
- } else {
- sb.append(md.getTypeReference().toString()).append(" ");
+ var ms = MethodSpec.methodBuilder(m.getName());
+ if (m.isProtected()) ms.addModifiers(Modifier.PROTECTED);
+ if (m.isPublic()) ms.addModifiers(Modifier.PUBLIC);
+ if (m.isFinal()) ms.addModifiers(Modifier.FINAL);
+ if (m.isStatic()) ms.addModifiers(Modifier.STATIC);
+ if (m.isSynchronized()) ms.addModifiers(Modifier.SYNCHRONIZED);
+
+ if (md.getTypeReference() != null) {
+ ms.returns(getTypeName(md.getTypeReference()));
}
- sb.append(m.getName()).append("(");
- final Iterator pdIter = md.getParameters().iterator();
+
+ var pdIter = md.getParameters();
int varcount = 0;
- while (pdIter.hasNext()) {
- final ParameterDeclaration pd = pdIter.next();
- if (pd.isFinal()) {
- sb.append("final ");
- }
- if (pd.getTypeReference() == null) {
- sb.append("void /*unkown type*/ ");
- } else {
- sb.append(pd.getTypeReference().toString()).append(" ");
- }
- if (pd.getVariables().isEmpty()) {
- sb.append("var").append(varcount);
- } else {
- sb.append(pd.getVariables().iterator().next().getFullName());
- }
- if (pdIter.hasNext()) {
- sb.append(", ");
- }
+ for (ParameterDeclaration pd : pdIter) {
+ var type = pd.getTypeReference() == null ? TypeName.VOID :
+ getTypeName(pd.getTypeReference());
+
+ var name = pd.getVariables().isEmpty()
+ ? "var" + varcount
+ : pd.getVariables().iterator().next().getFullName();
+
+ var ps = ParameterSpec.builder(type, name);
+ if (pd.isFinal()) ps.addModifiers(Modifier.FINAL);
+ ms.addParameter(ps.build());
varcount++;
}
- sb.append(")");
+
if (md.getThrown() != null) {
- sb.append(" throws ").append(md.getThrown().getTypeReferenceAt(0)).append(" ")
- .append(NEW_LINE).append(" ");
+ ms.addException(getTypeName(md.getThrown().getTypeReferenceAt(0)));
}
if (md.getTypeReference() == null) {
- sb.append("{ };");
+ ms.addStatement(CodeBlock.builder().build());
} else {
final String type = md.getTypeReference().toString();
if (isNumericType(type)) {
- sb.append("{ return 0;}");
+ ms.addStatement("return 0;");
} else if (type.equals("boolean")) {
- sb.append("{ return true;}");
+ ms.addStatement("{ return true;}");
} else if (type.equals("char")) {
- sb.append("{ return 'a';}");
+ ms.addStatement("{ return 'a';}");
} else {
boolean returnNull = true;
try {
final String retType =
- md.getTypeReference().getKeYJavaType().getSort().name().toString();
+ md.getTypeReference().getKeYJavaType().getSort().name().toString();
if (retType.equals("java.lang.String")) {
- sb.append("{ return \"").append(className).append("\";}");
+ ms.addStatement("{ return $S;", className);
returnNull = false;
}
- } catch (final Exception e) {
- returnNull = true;
+ } catch (final Exception ignored) {
}
+
if (returnNull) {
- sb.append("{ return null;}");
+ ms.addStatement("return null;");
}
}
}
- sb.append(NEW_LINE);
}
- sb.append("}");
+
+ var jfile = JavaFile.builder("", clazz.build());
+ dummyClasses.add(jfile.build());
return className;
}
- private void copyFiles(final String srcName, final String targName) throws IOException {
+ private static TypeName getTypeName(TypeReference tr) {
+ return ClassName.get("", tr.getName());
+ }
+
+ private void copyFiles(Path srcFolder, Path target) throws IOException {
// We don't want to copy the Folder with API Reference
- // Implementation
- if (srcName.equals(dontCopy)) {
- return;
- }
- // Create the File with given filename and check if it exists and if
- // it's readable
- final File srcFile = new File(srcName);
- if (!srcFile.exists()) {
- throw new IOException("FileCopy: " + "no such source file: " + srcName);
- }
- if (!srcFile.canRead()) {
- throw new IOException("FileCopy: " + "source file is unreadable: " + srcName);
- }
- if (srcFile.isDirectory()) {
- final String newTarget;
- if (srcName.equals(modDir)) {
- newTarget = targName;
- } else {
- newTarget = targName + File.separator + srcFile.getName();
- }
- for (final String subName : srcFile.list()) {
- copyFiles(srcName + File.separator + subName, newTarget);
+ if (srcFolder.equals(target)) return;
+ Files.walkFileTree(srcFolder, new SimpleFileVisitor<>() {
+ @Override
+ public FileVisitResult visitFile(Path file, BasicFileAttributes attrs) throws IOException {
+ var relFile = srcFolder.relativize(file);
+ var tarFile = target.resolve(relFile);
+ Files.copy(file, tarFile);
+ return FileVisitResult.CONTINUE;
}
- } else if (srcFile.isFile()) {
- final File targDir = new File(targName);
- if (!targDir.exists()) {
- targDir.mkdirs();
- }
- final File targFile = new File(targDir, srcFile.getName());
- if (targFile.exists()) {
- if (!targFile.canWrite()) {
- throw new IOException(
- "FileCopy: " + "destination file is unwriteable: " + targName);
- }
- }
- try (var src = new FileInputStream(srcFile);
- var targ = new FileOutputStream(targFile)) {
- final byte[] buffer = new byte[4096];
- int bytesRead;
- while ((bytesRead = src.read(buffer)) != -1) {
- targ.write(buffer, 0, bytesRead); // write
- }
+
+ @Override
+ public FileVisitResult postVisitDirectory(Path dir, IOException exc) {
+ if (dir.equals(outputDontCopy)) return FileVisitResult.SKIP_SUBTREE;
+ return FileVisitResult.CONTINUE;
}
- } else {
- throw new IOException("FileCopy: " + srcName + " is neither a file nor a directory!");
- }
+ });
}
- protected void createDummyClasses() throws IOException {
- for (final Sort s : sortDummyClass.keySet()) {
- final var sb = sortDummyClass.get(s);
- final String file = getDummyClassNameFor(s) + JAVA_FILE_EXTENSION_WITH_DOT;
- writeToFile(file, sb);
- }
+ public void createDummyClasses() throws IOException {
+ for (final var s : dummyClasses) s.writeTo(outputFolder);
}
/**
* Creates the RFL.java file, that provides setter and getter methods using the reflection API
* as well as object creation functions based on the objenesis library.
- *
- * @throws IOException
*/
- protected void writeRFLFile() throws IOException {
- writeToFile(ReflectionClassCreator.NAME_OF_CLASS + JAVA_FILE_EXTENSION_WITH_DOT,
- createRFLFileContent());
+ public void writeRFLFile() throws IOException {
+ var content = createRFLFileContent();
+ var jfile = JavaFile.builder("", content).build();
+ jfile.writeTo(outputFolder);
}
/**
@@ -417,50 +288,43 @@ protected void writeRFLFile() throws IOException {
*
* @return The content of the RFL file.
*/
- public StringBuilder createRFLFileContent() {
+ public TypeSpec createRFLFileContent() {
return rflCreator.createClass(rflAsInternalClass);
}
- protected void createOpenJMLShellScript() throws IOException {
- StringBuilder sb = new StringBuilder();
- String filestr = "compileWithOpenJML.sh";
- File file = new File(directory + modDir + File.separator + filestr);
- if (!file.exists()) {
- sb.append(compileWithOpenJML);
- writeToFile(filestr, sb);
- }
- filestr = "executeWithOpenJML.sh";
- file = new File(directory + modDir + File.separator + filestr);
- if (!file.exists()) {
- sb = new StringBuilder();
- sb.append(executeWithOpenJML);
- writeToFile(filestr, sb);
+ public void createOpenJMLShellScript() throws IOException {
+ var executeWithOpenJML =
+ template.shExecuteWithOpenJML(settings.getOpenjmlPath(), settings.getObjenesisPath());
+ var compileWithOpenJML =
+ template.shCompileWithOpenJML(settings.getOpenjmlPath(), settings.getObjenesisPath());
+ var file = outputModDir.resolve("compileWithOpenJML.sh");
+ if (!Files.exists(file)) {
+ Files.writeString(file, compileWithOpenJML);
}
- }
- protected void exportCodeUnderTest() throws IOException {
- // Copy the involved classes without modification
- copyFiles(modDir, directory + modDir);
+ var executeOpenJml = outputFolder.resolve("executeWithOpenJML.sh");
+ if (!Files.exists(executeOpenJml)) {
+ Files.writeString(executeOpenJml, executeWithOpenJML);
+ }
}
- private boolean filterVal(String s) {
- return !s.startsWith("#a") && !s.startsWith("#s") && !s.startsWith("#h")
- && !s.startsWith("#l") && !s.startsWith("#f");
+ /**
+ * Copy the involved classes without modification
+ */
+ public void exportCodeUnderTest() throws IOException {
+ copyFiles(Paths.get(modDirName), outputModDir);
}
- protected String getOracleAssertion(List oracleMethods) {
+ public String getOracleAssertion(List oracleMethods) {
Term postcondition = getPostCondition();
- OracleMethod oracle = oracleGenerator.generateOracleMethod(postcondition);
-
-
+ var oracle = oracleGenerator.generateOracleMethod(postcondition);
OracleMethodCall oracleCall = new OracleMethodCall(oracle, oracle.getArgs());
-
- oracleMethods.add(oracle);
- oracleMethods.addAll(oracleGenerator.getOracleMethods());
+ oracleMethods.add(oracle.build());
+ oracleGenerator.getOracleMethods().forEach(it -> oracleMethods.add(it.build()));
LOGGER.debug("Modifier Set: {}",
- oracleGenerator.getOracleLocationSet(info.getAssignable()));
+ oracleGenerator.getOracleLocationSet(info.getAssignable()));
return "assertTrue(" + oracleCall + ");";
}
@@ -469,89 +333,92 @@ private Term getPostCondition() {
return info.getPostCondition();
}
+ /**
+ * Entry function to the world of test case generation.
+ *
+ * @param problemSolvers
+ * @return
+ * @throws IOException
+ */
public String generateJUnitTestSuite(Collection problemSolvers) throws IOException {
initFileName();
- StringBuilder testSuite = createTestCaseCotent(problemSolvers);
- writeToFile(fileName + JAVA_FILE_EXTENSION_WITH_DOT, testSuite);
- logger.writeln("Writing test file to:" + directory + modDir + File.separator + fileName
- + JAVA_FILE_EXTENSION_WITH_DOT);
+ var testSuite = createTestCaseContent(problemSolvers);
+ testSuite.writeTo(outputFolder);
+ logger.writeln("Writing test file");
+
exportCodeUnderTest();
createDummyClasses();
+
try {
if (useRFL) {
writeRFLFile();
}
} catch (Exception ex) {
logger.writeln("Error: The file RFL" + JAVA_FILE_EXTENSION_WITH_DOT
- + " is either not generated or it has an error.");
+ + " is either not generated or it has an error.");
LOGGER.error("Error: The file RFL {} is either not generated or it has an error.",
- JAVA_FILE_EXTENSION_WITH_DOT);
+ JAVA_FILE_EXTENSION_WITH_DOT);
}
createOpenJMLShellScript();
- TestCaseGenerator.fileCounter++;
+ TestCaseGenerator.FILE_COUNTER.incrementAndGet();
return testSuite.toString();
}
public void initFileName() {
- fileName = "TestGeneric" + TestCaseGenerator.fileCounter;
+ fileName = "TestGeneric" + TestCaseGenerator.FILE_COUNTER;
String mut = getMUTCall();
if (mut == null) {
mut = " //Manually write a call to the method under test, "
- + "because KeY could not determine it automatically.";
+ + "because KeY could not determine it automatically.";
} else {
fileName += "_" + mutName;
}
}
- public StringBuilder createTestCaseCotent(Collection problemSolvers) {
+ public JavaFile createTestCaseContent(Collection problemSolvers) {
// TODO: Include package definition (same as type containing the proof obligation)
- final StringBuilder testSuite = new StringBuilder();
- testSuite.append(getFilePrefix(fileName, packageName)).append(NEW_LINE);
- final StringBuilder testMethods = new StringBuilder();
- int i = 0;
+
+ var clazz = TypeSpec.classBuilder(ClassName.get(packageName, fileName));
+
+ int counter = 0;
for (final SMTSolver solver : problemSolvers) {
try {
- final StringBuilder testMethod = new StringBuilder();
- final String originalNodeName = solver.getProblem().getGoal()
- /*
- * TODO:Warning this is wrong if we generate a test from an inner node (e.g.
- * closed proof tree), because goals are mutable. A Node should be used here
- * instead.
- */
- .proof().name().toString();
+ var goal = solver.getProblem().getGoal();
+ var node = goal.node();
+ final String originalNodeName = node.proof().name().toString();
+ var ms = MethodSpec.methodBuilder("testcode_" + counter);
+
boolean success = false;
if (solver.getSocket().getQuery() != null) {
final Model m = solver.getSocket().getQuery().getModel();
- if (TestCaseGenerator.modelIsOK(m)) {
+ if (modelIsOK(m)) {
logger.writeln("Generate: " + originalNodeName);
- Map typeInfMap =
- generateTypeInferenceMap(solver.getProblem().getGoal().node());
-
- testMethod.append(" //").append(originalNodeName).append(NEW_LINE);
- testMethod.append(getTestMethodSignature(i)).append("{").append(NEW_LINE);
- testMethod.append(
- " //Test preamble: creating objects and intializing test data")
- .append(generateTestCase(m, typeInfMap)).append(NEW_LINE)
- .append(NEW_LINE);
+ Map typeInfMap = generateTypeInferenceMap(goal.node());
+ ms.addComment(originalNodeName);
+ switch (format) {
+ case JUnit4 -> ms.addAnnotation(JUNIT4_TEST_ANNOTATION);
+ case JUnit5 -> ms.addAnnotation(JUNIT5_TEST_ANNOTATION);
+ case TestNG -> ms.addAnnotation(TESTNG_TEST_ANNOTATION);
+ case Plain -> {
+ }
+ }
+ ms.addComment("Test preamble: creating objects and intializing test data");
+ generateTestCase(ms, m, typeInfMap);
Set vars = new HashSet<>();
info.getProgramVariables(info.getPO(), vars);
- testMethod.append(TAB + "//Other variables").append(NEW_LINE)
- .append(getRemainingConstants(m.getConstants().keySet(), vars))
- .append(NEW_LINE);
- testMethod.append(" //Calling the method under test ").append(NEW_LINE)
- .append(info.getCode()).append(NEW_LINE);
-
-
- if (junitFormat) {
- testMethod.append(" //calling the test oracle").append(NEW_LINE)
- .append(TAB).append(oracleMethodCall).append(NEW_LINE);
+ ms.addComment("Other variables")
+ .addStatement(getRemainingConstants(m.getConstants().keySet(), vars))
+ .addComment(" //Calling the method under test ")
+ .addStatement(info.getCode());
+
+ if (isJunit()) {
+ ms.addComment("calling the test oracle")
+ .addStatement(oracleMethodCall);
}
-
- testMethod.append(" }").append(NEW_LINE).append(NEW_LINE);
- i++;
+ counter++;
success = true;
- testMethods.append(testMethod);
+ clazz.addMethod(ms.build());
}
}
if (!success) {
@@ -562,36 +429,51 @@ public StringBuilder createTestCaseCotent(Collection problemSolvers)
logger.writeln(ste.toString());
}
logger.writeln(
- "A test case was not generated due to an exception. Continuing test generation...");
+ "A test case was not generated due to an exception. Continuing test generation...");
}
}
- if (i == 0) {
+
+ if (counter == 0) {
logger.writeln(
- "Warning: no test case was generated. Adjust the SMT solver settings (e.g. timeout) "
- + "in Options->SMT Solvers.");
- } else if (i < problemSolvers.size()) {
+ "Warning: no test case was generated. Adjust the SMT solver settings (e.g. timeout) "
+ + "in Options->SMT Solvers.");
+ } else if (counter < problemSolvers.size()) {
logger.writeln("Warning: SMT solver could not solve all test data constraints. "
- + "Adjust the SMT solver settings (e.g. timeout) in Options->SMT Solvers.");
+ + "Adjust the SMT solver settings (e.g. timeout) in Options->SMT Solvers.");
}
- testSuite.append(getMainMethod(fileName, i)).append(NEW_LINE).append(NEW_LINE);
- testSuite.append(testMethods);
- if (junitFormat) {
- for (OracleMethod m : oracleMethods) {
- testSuite.append(NEW_LINE).append(NEW_LINE);
- testSuite.append(m);
- }
- }
+ clazz.addMethod(getMainMethod(fileName, counter));
- if (rflAsInternalClass) {
- testSuite.append(createRFLFileContent());
+ if (isJunit()) {
+ clazz.addMethods(oracleMethods);
}
- testSuite.append(NEW_LINE).append("}");
- return testSuite;
+ if (rflAsInternalClass) {
+ clazz.addType(createRFLFileContent());
+ }
+
+ var jfile = JavaFile.builder(packageName, clazz.build());
+ jfile.addFileComment(
+ """
+ /** This is a test driver generated by KeY $S (www.key-project.org).
+ * Possible use cases:" + NEW_LINE
+ * Use Case 1. Using JUnit 4:" + NEW_LINE
+ * javac -cp .:PATH_TO_JUNIT4_JAR *.java" + NEW_LINE
+ * java -cp .:PATH_TO_JUNIT4_JAR:PATH_TO_HAMCREST_JAR org.junit.runner.JUnitCore "
+ className + NEW_LINE + " * Use Case 2. Use JML runtime checker: " + NEW_LINE
+ * Compile this file and and execute the main method with a JML runtime checker. On linux you can use the built-in scripts:"
+ * ./compileWithOpenJML.sh"
+ * ./executeWithOpenJML.sh " + $S
+ * Use Case 3. Use simply a program debugger to follow and understand the execution of the program."
+ * @author Christoph Gladisch
+ * @author Mihai Herda
+ */
+ """, KeYConstants.VERSION, fileName + ".java"
+ );
+ return jfile.build();
}
- protected String inferSort(Map typeInfMap, String progVar) {
+ public String inferSort(Map typeInfMap, String progVar) {
if (typeInfMap.containsKey(progVar)) {
return typeInfMap.get(progVar).name().toString();
}
@@ -599,7 +481,7 @@ protected String inferSort(Map typeInfMap, String progVar) {
return "NOTYPE";
}
- protected Map generateTypeInferenceMap(Node n) {
+ public Map generateTypeInferenceMap(Node n) {
HashMap typeInfMap = new HashMap<>();
for (SequentFormula sequentFormula : n.sequent()) {
Term t = sequentFormula.formula();
@@ -619,7 +501,7 @@ private void generateTypeInferenceMapHelper(Term t, Map map) {
}
} else {
LOGGER.debug("PV {} Sort: {} KeYJavaType: {}", name, pv.sort(),
- pv.getKeYJavaType());
+ pv.getKeYJavaType());
map.put(name, pv.sort());
}
} else if (op instanceof Function && !(op instanceof ObserverFunction)) {
@@ -633,19 +515,15 @@ private void generateTypeInferenceMapHelper(Term t, Map map) {
if (sort == hLDT.getFieldSort()) {
ProgramVariable pv = getProgramVariable(t);
- if (pv != null) {
- name = name.replace("::$", "::");
+ name = name.replace("::$", "::");
- if (map.containsKey(name)) {
- if (map.get(name) != pv.sort()) {
- LOGGER.warn("Function {} is ambiguous.", name);
- }
- } else {
- LOGGER.debug("Func: {} Sort: {} PV.sort: {}", name, func.sort(), pv.sort());
- map.put(name, pv.sort());
+ if (map.containsKey(name)) {
+ if (map.get(name) != pv.sort()) {
+ LOGGER.warn("Function {} is ambiguous.", name);
}
} else {
- LOGGER.warn("Program variable could not be determined: {}", t);
+ LOGGER.debug("Func: {} Sort: {} PV.sort: {}", name, func.sort(), pv.sort());
+ map.put(name, pv.sort());
}
}
}
@@ -673,7 +551,7 @@ private ProgramVariable getProgramVariable(Term locationTerm) {
}
private String getRemainingConstants(Collection existingConstants,
- Collection newConstants) {
+ Collection newConstants) {
StringBuilder result = new StringBuilder();
for (Term c : newConstants) {
@@ -691,7 +569,7 @@ private String getRemainingConstants(Collection existingConstants,
result.append(NEW_LINE).append(TAB).append(NULLABLE).append(" ")
.append(getSafeType(c.sort())).append(" ").append(c).append(" = ")
.append(init).append(";");
- if (junitFormat) {
+ if (isJunit()) {
result.append(NEW_LINE).append(TAB).append(NULLABLE).append(" ")
.append(getSafeType(c.sort())).append(" ")
.append(getPreName(c.toString())).append(" = ").append(init)
@@ -728,17 +606,14 @@ private boolean isInPrestate(Collection prestate, String na
}
public String generateModifierSetAssertions(Model m) {
-
-
return TAB + "//Modifier set assertions";
}
- public String generateTestCase(Model m, Map typeInfMap) {
+ public void generateTestCase(MethodSpec.Builder mb, Model m, Map typeInfMap) {
m.removeUnnecessaryObjects();
Set objects = new HashSet<>();
- final List assignments = new LinkedList<>();
Heap heap = null;
for (final Heap h : m.getHeaps()) {
if (h.getName().equals(HeapLDT.BASE_HEAP_NAME.toString())) {
@@ -750,8 +625,6 @@ public String generateTestCase(Model m, Map typeInfMap) {
// Set prestate = getPrestateObjects(m);
Set prestate = new HashSet<>();
if (heap != null) {
-
-
// create objects
for (final ObjectVal o : heap.getObjects()) {
if (o.getName().equals("#o0")) {
@@ -761,7 +634,7 @@ public String generateTestCase(Model m, Map typeInfMap) {
String right;
if (type.endsWith("[]")) {
right =
- "new " + type.substring(0, type.length() - 2) + "[" + o.getLength() + "]";
+ "new " + type.substring(0, type.length() - 2) + "[" + o.getLength() + "]";
} else if (o.getSort() == null || o.getSort().toString().equals("Null")) {
right = "null";
} else {
@@ -776,12 +649,15 @@ public String generateTestCase(Model m, Map typeInfMap) {
String objName = createObjectName(o);
objects.add(objName);
- assignments.add(new Assignment(type, objName, right));
- if (junitFormat && isInPrestate(prestate, o)) {
- assignments.add(new Assignment(type, getPreName(objName), right));
+ mb.addStatement(assignmentCreator.assign(type, objName, right));
+
+ if (isJunit() && isInPrestate(prestate, o)) {
+ mb.addStatement(assignmentCreator.assign(type, getPreName(objName), right));
}
}
}
+
+
// init constants
for (final String c : m.getConstants().keySet()) {
String val = m.getConstants().get(c);
@@ -806,21 +682,22 @@ public String generateTestCase(Model m, Map typeInfMap) {
declType = type;
}
val = translateValueExpression(val);
- assignments.add(new Assignment(declType, c, "(" + type + ")" + val));
- if (junitFormat && (isObject || Character.isJavaIdentifierStart(c.charAt(0)))
+ mb.addStatement(assignmentCreator.assign(declType, c, "(" + type + ")" + val));
+
+
+ if (isJunit() && (isObject || Character.isJavaIdentifierStart(c.charAt(0)))
&& isInPrestate(prestate, val)) {
if (isLiteral) {
- assignments.add(
- new Assignment(declType, getPreName(c), "(" + type + ")" + val));
+ mb.addStatement(assignmentCreator.assign(declType, getPreName(c), "(" + type + ")" + val));
} else {
- assignments.add(new Assignment(declType, getPreName(c),
- "(" + type + ")" + getPreName(val)));
+ mb.addStatement(assignmentCreator.assign(declType, getPreName(c),
+ "(" + type + ")" + getPreName(val)));
}
-
}
}
}
}
+
// init fields
if (heap != null) {
for (final ObjectVal o : heap.getObjects()) {
@@ -845,11 +722,13 @@ && isInPrestate(prestate, val)) {
LOGGER.debug("Added sort (init fields): {}", vType);
val = translateValueExpression(val);
final String rcObjType = getSafeType(o.getSort());
- assignments.add(
- new Assignment(new RefEx(rcObjType, receiverObject, vType, fieldName),
+
+ mb.addStatement(assignmentCreator.assign("",
+ new RefEx(rcObjType, receiverObject, vType, fieldName),
"(" + vType + ")" + val));
- if (junitFormat && isInPrestate(prestate, o)) {
+
+ if (isJunit() && isInPrestate(prestate, o)) {
// if value that is pointed to is object and in prestate then use prestate
// object
if (!vType.equals("int") && !vType.equals("boolean")
@@ -857,10 +736,8 @@ && isInPrestate(prestate, val) && !val.equals("null")) {
val = getPreName(val);
}
-
- assignments.add(new Assignment(
- new RefEx(rcObjType, getPreName(receiverObject), vType, fieldName),
- "(" + vType + ")" + val));
+ mb.addStatement(assignmentCreator.assign("", new RefEx(rcObjType, getPreName(receiverObject), vType, fieldName),
+ "(" + vType + ")" + val));
}
}
@@ -875,48 +752,37 @@ && isInPrestate(prestate, val) && !val.equals("null")) {
final String fieldName = "[" + i + "]";
String val = o.getArrayValue(i);
val = translateValueExpression(val);
- assignments.add(new Assignment(receiverObject + fieldName, val));
- if (junitFormat && isInPrestate(prestate, o)) {
+ mb.addStatement(assignmentCreator.assign("", receiverObject + fieldName, val));
+
+ if (isJunit() && isInPrestate(prestate, o)) {
if (!elementType.equals("int") && !elementType.equals("boolean")
&& isInPrestate(prestate, val) && !val.equals("null")) {
val = getPreName(val);
}
- assignments.add(
- new Assignment(getPreName(receiverObject) + fieldName, val));
+ mb.addStatement(assignmentCreator.assign("", getPreName(receiverObject) + fieldName, val));
}
-
-
}
}
}
}
- final StringBuilder result = new StringBuilder();
- for (final Assignment a : assignments) {
- result.append(NEW_LINE).append(" ");
- result.append(a.toString(useRFL));
- }
- if (junitFormat) {
- result.append(NEW_LINE);
- result.append(createOldMap(objects)).append(NEW_LINE);
- result.append(createBoolSet()).append(NEW_LINE);
- result.append(createIntSet()).append(NEW_LINE);
- result.append(createObjSet(heap)).append(NEW_LINE);
+ if (isJunit()) {
+ createOldMap(mb, objects);
+ createBoolSet(mb);
+ createIntSet(mb);
+ createObjSet(mb, heap);
}
-
-
- return result.toString();
}
- private String createOldMap(Set objNames) {
- StringBuilder result = new StringBuilder(
- NEW_LINE + TAB + "Map " + OLDMap + " = new HashMap();");
+ private void createOldMap(MethodSpec.Builder mb, Set objNames) {
+ ClassName NAME_HASH_MAP = ClassName.get(HashMap.class);
+ var map =
+ ParameterizedTypeName.get(NAME_HASH_MAP, ClassName.OBJECT, ClassName.OBJECT);
+ mb.addStatement("$T $N = new $T();", map, OLDMap, map);
for (String o : objNames) {
- result.append(NEW_LINE).append(TAB).append(OLDMap).append(".put(").append(getPreName(o))
- .append(",").append(o).append(");");
+ mb.addStatement("$N.put($N, $L);", OLDMap, getPreName(o), o);
}
- return result.toString();
}
private String getPreName(String val) {
@@ -930,44 +796,16 @@ private String createObjectName(final ObjectVal o) {
private String getDummyClassNameFor(Sort sort) {
final JavaInfo jinfo = services.getJavaInfo();
final KeYJavaType kjt = jinfo.getKeYJavaType(sort);
- return kjt.getName() + dummyPostfix;
+ return kjt.getName() + DUMMY_POSTFIX;
}
- private String getFilePrefix(String className, String packageName) {
- String res = "/** This is a test driver generated by KeY " + KeYConstants.VERSION
- + " (www.key-project.org). " + NEW_LINE + " * Possible use cases:" + NEW_LINE
- + " * Use Case 1. Using JUnit 4:" + NEW_LINE
- + " * javac -cp .:PATH_TO_JUNIT4_JAR *.java" + NEW_LINE
- + " * java -cp .:PATH_TO_JUNIT4_JAR:PATH_TO_HAMCREST_JAR org.junit.runner.JUnitCore "
- + className + NEW_LINE + " * Use Case 2. Use JML runtime checker: " + NEW_LINE
- + " * Compile this file and and execute the main method with a JML runtime checker. On linux you can use the built-in scripts:"
- + NEW_LINE + " * ./compileWithOpenJML.sh" + NEW_LINE
- + " * ./executeWithOpenJML.sh " + className + NEW_LINE
- + " * Use Case 3. Use simply a program debugger to follow and understand the execution of the program."
- + NEW_LINE + " * @author Christoph Gladisch" + NEW_LINE + " * @author Mihai Herda"
- + NEW_LINE + " */" + NEW_LINE;
- if (packageName != null) {
- res += "package " + packageName + ";" + NEW_LINE;
- }
-
- if (junitFormat) {
- res += "import java.util.Set;" + NEW_LINE + "import java.util.HashSet;" + NEW_LINE
- + "import java.util.Map;" + NEW_LINE + "import java.util.HashMap;" + NEW_LINE
- + " public class " + className + " extends junit.framework.TestCase {" + NEW_LINE
- + NEW_LINE + " public static junit.framework.Test suite() { "
- + " return new junit.framework.JUnit4TestAdapter(" + className + ".class);"
- + NEW_LINE + " } " + NEW_LINE + NEW_LINE + " public " + className + "(){}"
- + NEW_LINE + NEW_LINE;
- } else {
- res += "public class " + className + "{ " + NEW_LINE + NEW_LINE + " public " + className
- + "(){}" + NEW_LINE;
- }
- return res;
- }
+ private MethodSpec getMainMethod(String className, int i) {
+ var main = MethodSpec.methodBuilder("main")
+ .addModifiers(Modifier.PUBLIC, Modifier.STATIC, Modifier.FINAL)
+ .addParameter(String[].class, "args")
+ .build();
- private StringBuilder getMainMethod(String className, int i) {
- final StringBuilder res = new StringBuilder();
- res.append(" public static void main (java.lang.String[] arg) {").append(NEW_LINE)
+ /*res.append(" public static void main (java.lang.String[] arg) {").append(NEW_LINE)
.append(" ").append(className).append(" testSuiteObject;").append(NEW_LINE)
.append(" testSuiteObject=new ").append(className).append(" ();").append(NEW_LINE)
.append(NEW_LINE);
@@ -977,41 +815,40 @@ private StringBuilder getMainMethod(String className, int i) {
if (i == 0) {
res.append(" //Warning:no test methods were generated.").append(NEW_LINE);
}
- res.append(" }");
- return res;
+ res.append(" }");*/
+
+ var clazz = TypeSpec.classBuilder(className);
+ clazz.addMethod(main);
+ return main;
}
- private String createBoolSet() {
+ private void createBoolSet(MethodSpec.Builder mb) {
// bool
- String allbool = ALL_BOOLS;
- return NEW_LINE + TAB + "Set " + allbool + "= new HashSet();" + NEW_LINE
- + TAB + allbool + ".add(true);" + NEW_LINE + TAB + allbool + ".add(false);" + NEW_LINE;
+ var SET_NAME = ClassName.get(HashSet.class);
+ var BOOL_SET = ParameterizedTypeName.get(SET_NAME, TypeName.BOOLEAN);
+ mb.addStatement("$T $N = new $T();", BOOL_SET, ALL_BOOLS, BOOL_SET);
+ mb.addStatement("$N.add($L);", ALL_BOOLS, true);
+ mb.addStatement("$N.add($L);", ALL_BOOLS, false);
}
- private String createIntSet() {
-
- StringBuilder res = new StringBuilder();
+ private static void createIntSet(MethodSpec.Builder mb) {
long size = ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings().getIntBound();
-
long low = (long) -Math.pow(2, size - 1);
long hi = (long) (Math.pow(2, size - 1) - 1);
- String allint = ALL_INTS;
- res.append(TAB + "Set ").append(allint).append("= new HashSet();")
- .append(NEW_LINE);
+ var SET_NAME = ClassName.get(HashSet.class);
+ var SET_INT = ParameterizedTypeName.get(SET_NAME, TypeName.INT.box());
+ mb.addStatement("$T $N = new $T();", SET_INT, ALL_INTS, SET_INT);
for (long i = low; i <= hi; i++) {
- res.append(TAB).append(allint).append(".add(").append(i).append(");").append(NEW_LINE);
+ mb.addStatement("$N.add($L);", ALL_INTS, i);
}
- return res.toString();
}
- private String createObjSet(Heap h) {
-
- StringBuilder res = new StringBuilder();
-
- res.append(TAB + "Set