From 25a0200947cf18c631dbe2f27075adf3a6ba728b Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 19 Jan 2024 00:58:11 +0100 Subject: [PATCH] Renovation of the TestCase generation --- key.core.testgen/build.gradle | 1 + .../de/uka/ilkd/key/testgen/Assignment.java | 69 -- .../java/de/uka/ilkd/key/testgen/Format.java | 5 + .../uka/ilkd/key/testgen/ModelGenerator.java | 2 +- .../de/uka/ilkd/key/testgen/ProofInfo.java | 13 +- .../java/de/uka/ilkd/key/testgen/RefEx.java | 25 +- .../key/testgen/ReflectionClassCreator.java | 421 ++++----- .../java/de/uka/ilkd/key/testgen/TGMain.java | 96 ++ .../ilkd/key/testgen/TestCaseGenerator.java | 830 +++++++----------- .../uka/ilkd/key/testgen/TestgenFacade.java | 10 + .../de/uka/ilkd/key/testgen/TestgenUtils.java | 68 ++ .../macros/SemanticsBlastingMacro.java | 3 +- .../{ => testgen}/macros/TestGenMacro.java | 7 +- .../testgen/oracle/ModifiesSetTranslator.java | 39 +- .../key/testgen/oracle/OracleBinTerm.java | 31 +- .../key/testgen/oracle/OracleConstant.java | 26 +- .../key/testgen/oracle/OracleGenerator.java | 37 +- .../oracle/OracleInvariantTranslator.java | 22 +- .../key/testgen/oracle/OracleLocation.java | 39 +- .../key/testgen/oracle/OracleLocationSet.java | 93 +- .../ilkd/key/testgen/oracle/OracleMethod.java | 31 +- .../key/testgen/oracle/OracleMethodCall.java | 26 +- .../ilkd/key/testgen/oracle/OracleTerm.java | 3 +- .../ilkd/key/testgen/oracle/OracleType.java | 4 - .../key/testgen/oracle/OracleUnaryTerm.java | 2 +- .../key/testgen/oracle/OracleVariable.java | 29 - .../ilkd/key/testgen/oracle/package-info.java | 4 + .../de/uka/ilkd/key/testgen/package-info.java | 3 + .../settings/TestGenerationSettings.java | 35 +- .../key/testgen/settings/package-info.java | 3 + .../AbstractCounterExampleGenerator.java | 4 +- ...tractSideProofCounterExampleGenerator.java | 2 +- .../smt/counterexample/package-info.java | 3 + .../smt/testgen/AbstractTestGenerator.java | 41 +- .../smt/testgen/MemoryTestGenerationLog.java | 10 +- .../smt/testgen/StopRequest.java | 2 +- .../smt/testgen/TestGenerationLog.java | 2 +- .../key/testgen/smt/testgen/package-info.java | 3 + .../ilkd/key/testgen/template/Constants.java | 29 + .../key/testgen/template/JUnit4Template.java | 5 + .../key/testgen/template/PlainTemplate.java | 75 ++ .../ilkd/key/testgen/template/Template.java | 9 + .../ilkd/key/testgen/template/Templates.java | 5 + .../key/testgen/template/package-info.java | 3 + .../uka/ilkd/key/testcase/smt/ce/TestCE.java | 4 +- .../key/testcase/smt/testgen/TestTestgen.java | 2 +- .../key/gui/testgen/CounterExampleAction.java | 6 +- .../ilkd/key/gui/testgen/TGInfoDialog.java | 2 +- .../de/uka/ilkd/key/gui/testgen/TGWorker.java | 4 +- .../key/gui/testgen/TestgenExtension.java | 2 +- .../key/gui/testgen/TestgenOptionsPanel.java | 15 +- 51 files changed, 990 insertions(+), 1215 deletions(-) delete mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Assignment.java create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Format.java create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGMain.java create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenFacade.java create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenUtils.java rename key.core.testgen/src/main/java/de/uka/ilkd/key/{ => testgen}/macros/SemanticsBlastingMacro.java (98%) rename key.core.testgen/src/main/java/de/uka/ilkd/key/{ => testgen}/macros/TestGenMacro.java (94%) create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/package-info.java create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/package-info.java rename key.core.testgen/src/main/java/de/uka/ilkd/key/{ => testgen}/settings/TestGenerationSettings.java (92%) create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/settings/package-info.java rename key.core.testgen/src/main/java/de/uka/ilkd/key/{ => testgen}/smt/counterexample/AbstractCounterExampleGenerator.java (98%) rename key.core.testgen/src/main/java/de/uka/ilkd/key/{ => testgen}/smt/counterexample/AbstractSideProofCounterExampleGenerator.java (96%) create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/package-info.java rename key.core.testgen/src/main/java/de/uka/ilkd/key/{ => testgen}/smt/testgen/AbstractTestGenerator.java (94%) rename key.core.testgen/src/main/java/de/uka/ilkd/key/{ => testgen}/smt/testgen/MemoryTestGenerationLog.java (82%) rename key.core.testgen/src/main/java/de/uka/ilkd/key/{ => testgen}/smt/testgen/StopRequest.java (83%) rename key.core.testgen/src/main/java/de/uka/ilkd/key/{ => testgen}/smt/testgen/TestGenerationLog.java (88%) create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/package-info.java create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Constants.java create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/JUnit4Template.java create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/PlainTemplate.java create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Template.java create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Templates.java create mode 100644 key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/package-info.java 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 " + ALL_OBJECTS + "= new HashSet();") - .append(NEW_LINE); + private void createObjSet(MethodSpec.Builder mb, Heap h) { + var SET_NAME = ClassName.get(HashSet.class); + var BOOL_SET = ParameterizedTypeName.get(SET_NAME, TypeName.OBJECT); + mb.addStatement("$T $N = new $T();", BOOL_SET, ALL_OBJECTS, BOOL_SET); for (ObjectVal o : h.getObjects()) { String name = o.getName(); @@ -1019,16 +856,12 @@ private String createObjSet(Heap h) { continue; } name = name.replace("#", "_"); - res.append(TAB + ALL_OBJECTS + ".add(").append(name).append(");").append(NEW_LINE); - + mb.addStatement("$N.add($N);", ALL_OBJECTS, name); } - - return res.toString(); } - public String getSafeType(Sort sort) { - if (sort == null || sort.name().toString().equals("Null")) { + if (sort.name().toString().equals("Null")) { return "java.lang.Object"; } else if (sort.isAbstract()) { return buildDummyClassForAbstractSort(sort); @@ -1037,57 +870,14 @@ public String getSafeType(Sort sort) { } } - private String getTestMethodSignature(int i) { - final String sig = " public void testcode" + i + "()"; - if (junitFormat) { - return "@org.junit.Test" + NEW_LINE + sig; - } else { - return sig; - } - } - public boolean isJunit() { - return junitFormat; - } - - protected boolean isNumericType(String type) { - return type.equals("byte") || type.equals("short") || type.equals("int") - || type.equals("long") || type.equals("float") || type.equals("double"); - } - - protected boolean isPrimitiveType(String type) { - return isNumericType(type) || type.equals("boolean") || type.equals("char"); + return format == Format.JUnit4 || format == Format.JUnit5; } public void setLogger(TestGenerationLog logger) { this.logger = logger; } - protected String translateValueExpression(String val) { - if (val.contains("/")) { - val = val.substring(0, val.indexOf('/')); - } - if (val.equals("#o0")) { - return "null"; - } - val = val.replace("|", ""); - val = val.replace("#", "_"); - return val; - } - - public void writeToFile(String file, StringBuilder sb) throws IOException { - final File dir = new File(directory + modDir); - if (!dir.exists()) { - dir.mkdirs(); - } - final File pcFile = new File(dir, file); - LOGGER.debug("Writing file: {}", pcFile); - try (BufferedWriter bw = - new BufferedWriter(new FileWriter(pcFile, StandardCharsets.UTF_8))) { - bw.write(sb.toString()); - } - } - public boolean isUseRFL() { return useRFL; } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenFacade.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenFacade.java new file mode 100644 index 00000000000..dcef7bc8f58 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenFacade.java @@ -0,0 +1,10 @@ +package de.uka.ilkd.key.testgen; + +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.testgen.settings.TestGenerationSettings; + +public record TestgenFacade(TestGenerationSettings settings) { + public static void generateTestcases(Proof proof) { + + } +} diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenUtils.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenUtils.java new file mode 100644 index 00000000000..f9fce390706 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenUtils.java @@ -0,0 +1,68 @@ +package de.uka.ilkd.key.testgen; + +import de.uka.ilkd.key.smt.model.Model; +import org.jspecify.annotations.Nullable; + +import static org.antlr.tool.LeftRecursiveRuleAnalyzer.ASSOC.left; + +public class TestgenUtils { + interface AssignmentCreator { + String assign(String type, Object left, String right); + } + + public String createAssignment(boolean rfl, String type, Object left, String right) { + if (rfl) { + return createAssignmentWithRfl(type, left, right); + } else { + return createAssignmentWithoutRfl(type, left, right); + } + } + + public static String createAssignmentWithRfl(String type, Object left, String right) { + 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 createAssignmentWithoutRfl(type, left, right); + } + } + + public static String createAssignmentWithoutRfl(String type, Object left, String right) { + return type + " " + left + " = " + right + ";"; + } + + public static boolean isNumericType(String type) { + return type.equals("byte") || type.equals("short") || type.equals("int") + || type.equals("long") || type.equals("float") || type.equals("double"); + } + + public static boolean isPrimitiveType(String type) { + return isNumericType(type) || type.equals("boolean") || type.equals("char"); + } + + + public static String translateValueExpression(String val) { + if (val.contains("/")) { + val = val.substring(0, val.indexOf('/')); + } + if (val.equals("#o0")) { + return "null"; + } + val = val.replace("|", ""); + val = val.replace("#", "_"); + return val; + } + + public static boolean filterVal(String s) { + return !s.startsWith("#a") && !s.startsWith("#s") && !s.startsWith("#h") + && !s.startsWith("#l") && !s.startsWith("#f"); + } + + public static boolean modelIsOK(@Nullable Model m) { + return m != null && !m.isEmpty() && m.getHeaps() != null && !m.getHeaps().isEmpty() + && m.getTypes() != null; + } +} diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/SemanticsBlastingMacro.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/SemanticsBlastingMacro.java similarity index 98% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/macros/SemanticsBlastingMacro.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/SemanticsBlastingMacro.java index 30e2db9dc14..47e751e406a 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/SemanticsBlastingMacro.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/SemanticsBlastingMacro.java @@ -1,11 +1,12 @@ /* 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.macros; +package de.uka.ilkd.key.testgen.macros; import java.util.HashSet; import java.util.Set; +import de.uka.ilkd.key.macros.AbstractBlastingMacro; import de.uka.ilkd.key.proof.rulefilter.RuleFilter; import de.uka.ilkd.key.rule.Rule; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/TestGenMacro.java similarity index 94% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/TestGenMacro.java index 611f6ce8f88..09f7f71fcff 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/TestGenMacro.java @@ -1,19 +1,22 @@ /* 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.macros; +package de.uka.ilkd.key.testgen.macros; import java.util.HashSet; import java.util.Set; import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.macros.FilterStrategy; +import de.uka.ilkd.key.macros.ModalityCache; +import de.uka.ilkd.key.macros.StrategyProofMacro; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.RuleApp; -import de.uka.ilkd.key.settings.TestGenerationSettings; +import de.uka.ilkd.key.testgen.settings.TestGenerationSettings; import de.uka.ilkd.key.strategy.NumberRuleAppCost; import de.uka.ilkd.key.strategy.RuleAppCost; import de.uka.ilkd.key.strategy.Strategy; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/ModifiesSetTranslator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/ModifiesSetTranslator.java index 8f095c3580d..71c52cb9269 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/ModifiesSetTranslator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/ModifiesSetTranslator.java @@ -7,12 +7,7 @@ import de.uka.ilkd.key.ldt.LocSetLDT; import de.uka.ilkd.key.logic.Term; -public class ModifiesSetTranslator { - - private final Services services; - private final OracleGenerator gen; - - +public record ModifiesSetTranslator(Services services, OracleGenerator gen) { public boolean isSingleTon(Term t) { return t.op().equals(getLocSetLDT().getSingleton()); } @@ -41,14 +36,7 @@ private LocSetLDT getLocSetLDT() { return services.getTypeConverter().getLocSetLDT(); } - public ModifiesSetTranslator(Services services, OracleGenerator gen) { - this.services = services; - this.gen = gen; - } - - public OracleLocationSet translate(Term t) { - if (isSingleTon(t)) { Term obj = t.sub(0); Term field = t.sub(1); @@ -56,39 +44,24 @@ public OracleLocationSet translate(Term t) { String fieldString = gen.generateOracle(field, false).toString(); OracleLocation loc = new OracleLocation(objString, fieldString); return OracleLocationSet.singleton(loc); - } - - else if (isUnion(t)) { + } else if (isUnion(t)) { OracleLocationSet left = translate(t.sub(0)); OracleLocationSet right = translate(t.sub(1)); return OracleLocationSet.union(left, right); - } - - else if (isIntersection(t)) { + } else if (isIntersection(t)) { OracleLocationSet left = translate(t.sub(0)); OracleLocationSet right = translate(t.sub(1)); return OracleLocationSet.intersect(left, right); - } - - else if (isAllFields(t)) { + } else if (isAllFields(t)) { Term obj = t.sub(0); String objString = gen.generateOracle(obj, false).toString(); OracleLocation loc = new OracleLocation(objString); return OracleLocationSet.singleton(loc); - } - - else if (isEmpty(t)) { + } else if (isEmpty(t)) { return OracleLocationSet.EMPTY; - } - - else if (isAllLocs(t)) { + } else if (isAllLocs(t)) { return OracleLocationSet.ALL_LOCS; } - - throw new RuntimeException("Unsupported locset operation: " + t.op()); } - - - } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleBinTerm.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleBinTerm.java index 1ab97b6f9b9..f9cee816bbb 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleBinTerm.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleBinTerm.java @@ -3,37 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.testgen.oracle; -public class OracleBinTerm implements OracleTerm { - - private final String op; - - private final OracleTerm left; - - private final OracleTerm right; - - public OracleBinTerm(String op, OracleTerm left, OracleTerm right) { - super(); - this.op = op; - this.left = left; - this.right = right; - } - - public String getOp() { - return op; - } - - public OracleTerm getLeft() { - return left; - } - - public OracleTerm getRight() { - return right; - } - +public record OracleBinTerm(String op, OracleTerm left, OracleTerm right) implements OracleTerm { public String toString() { return "(" + left.toString() + " " + op + " " + right.toString() + ")"; } - - - } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleConstant.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleConstant.java index 044e76a1c6c..27478f53edc 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleConstant.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleConstant.java @@ -5,35 +5,11 @@ import de.uka.ilkd.key.logic.sort.Sort; -public class OracleConstant implements OracleTerm { - - private final String value; - - private Sort sort; - +public record OracleConstant(String value, Sort sort) implements OracleTerm { public static final OracleConstant TRUE = new OracleConstant("true", Sort.FORMULA); public static final OracleConstant FALSE = new OracleConstant("false", Sort.FORMULA); - public OracleConstant(String value, Sort sort) { - this.value = value; - this.sort = sort; - } - - public String getValue() { - return value; - } - - public Sort getSort() { - return sort; - } - - public void setSort(Sort sort) { - this.sort = sort; - } - public String toString() { return value; } - - } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java index 92b17312e1a..d2e561fa653 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java @@ -21,6 +21,8 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import static de.uka.ilkd.key.testgen.template.Constants.*; + public class OracleGenerator { private static final Logger LOGGER = LoggerFactory.getLogger(OracleGenerator.class); @@ -181,10 +183,10 @@ private List getMethodArgs(Term t) { Sort allObjSort = createSetSort("java.lang.Object"); Sort oldMapSort = new SortImpl(new Name("Map")); - OracleVariable allInts = new OracleVariable(TestCaseGenerator.ALL_INTS, allIntSort); - OracleVariable allBools = new OracleVariable(TestCaseGenerator.ALL_BOOLS, allBoolSort); - OracleVariable allObj = new OracleVariable(TestCaseGenerator.ALL_OBJECTS, allObjSort); - OracleVariable oldMap = new OracleVariable(TestCaseGenerator.OLDMap, oldMapSort); + OracleVariable allInts = new OracleVariable(ALL_INTS, allIntSort); + OracleVariable allBools = new OracleVariable(ALL_BOOLS, allBoolSort); + OracleVariable allObj = new OracleVariable(ALL_OBJECTS, allObjSort); + OracleVariable oldMap = new OracleVariable(OLDMap, oldMapSort); for (Term c : constants) { result.add(new OracleVariable(c.toString(), c.sort())); @@ -476,7 +478,7 @@ private OracleTerm translateSelect(Term term, boolean initialSelect) { if (!initialSelect && isPreHeap(heapTerm) && term.sort().extendsTrans(services.getJavaInfo().getJavaLangObject().getSort())) { - return new OracleConstant(TestCaseGenerator.OLDMap + ".get(" + value + ")", + return new OracleConstant(OLDMap + ".get(" + value + ")", term.sort()); } @@ -605,9 +607,9 @@ public Set getPrestateTerms() { private String getSetName(Sort s) { if (s.equals(Sort.FORMULA)) { - return TestCaseGenerator.ALL_BOOLS; + return ALL_BOOLS; } else if (s.equals(services.getTypeConverter().getIntegerLDT().targetSort())) { - return TestCaseGenerator.ALL_INTS; + return ALL_INTS; } else if (s.equals(services.getTypeConverter().getLocSetLDT().targetSort())) { throw new RuntimeException("Not implemented yet."); // return TestCaseGenerator.ALL_LOCSETS @@ -623,7 +625,7 @@ private String getSetName(Sort s) { } - return TestCaseGenerator.ALL_OBJECTS; + return ALL_OBJECTS; } private OracleMethod createQuantifierMethod(Term term, boolean initialSelect) { @@ -659,7 +661,7 @@ private OracleMethod createQuantifierMethod(Term term, boolean initialSelect) { } private String createForallBody(QuantifiableVariable qv, String setName, OracleUnaryTerm neg) { - String tab = TestCaseGenerator.TAB; + String tab = TAB; return "\n" + tab + "for(" + qv.sort().name() + " " + qv.name() + " : " + setName + "){" + "\n" + tab + tab + "if(" + neg.toString() + "){" + "\n" + tab + tab + tab + "return false;" + "\n" + tab + tab + "}" + "\n" + tab + "}" + "\n" + tab @@ -667,21 +669,24 @@ private String createForallBody(QuantifiableVariable qv, String setName, OracleU } private String createExistsBody(QuantifiableVariable qv, String setName, OracleTerm cond) { - String tab = TestCaseGenerator.TAB; - return "\n" + tab + "for(" + qv.sort().name() + " " + qv.name() + " : " + setName + "){" - + "\n" + tab + tab + "if(" + cond.toString() + "){" + "\n" + tab + tab + tab - + "return true;" + "\n" + tab + tab + "}" + "\n" + tab + "}" + "\n" + tab - + "return false;"; + String tab = TAB; + return (""" + %sfor(%s %s : %s){ + %s%sif(%s){ + %s%s%sreturn true; + %s%s} + %s} + %sreturn false;""").formatted( + tab, qv.sort().name(), qv.name(), setName, tab, tab, cond.toString(), + tab, tab, tab, tab, tab, tab, tab); } private static OracleTerm neg(OracleTerm t) { - if (t instanceof OracleUnaryTerm) { return ((OracleUnaryTerm) t).sub(); } else { return new OracleUnaryTerm(t, Op.Neg); } - } private static OracleTerm eq(OracleTerm left, OracleTerm right) { diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleInvariantTranslator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleInvariantTranslator.java index 23a3ca1c271..1aee4509554 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleInvariantTranslator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleInvariantTranslator.java @@ -19,14 +19,9 @@ import de.uka.ilkd.key.speclang.ClassAxiom; import de.uka.ilkd.key.speclang.RepresentsAxiom; -public class OracleInvariantTranslator { - - private final Services services; - - public OracleInvariantTranslator(Services services) { - this.services = services; - } +import java.util.Objects; +public record OracleInvariantTranslator(Services services) { public Term getInvariantTerm(Sort s) { JavaInfo info = services.getJavaInfo(); TermBuilder tb = new TermBuilder(services.getTermFactory(), services); @@ -36,8 +31,7 @@ public Term getInvariantTerm(Sort s) { LogicVariable h = new LogicVariable(new Name("h"), heapSort); - - KeYJavaType kjt = info.getKeYJavaType(s); + KeYJavaType kjt = Objects.requireNonNull(info.getKeYJavaType(s)); if (!(kjt.getJavaType() instanceof ClassDeclaration || kjt.getJavaType() instanceof InterfaceDeclaration @@ -73,19 +67,9 @@ public Term getInvariantTerm(Sort s) { result = tb.and(result, left); } } - - } - - } - } - return tb.tt(); - - - } - } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocation.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocation.java index c7190509695..c883ca9d8ea 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocation.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocation.java @@ -3,57 +3,22 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.testgen.oracle; -public class OracleLocation { - +public record OracleLocation(String object, String field) { public static final String ALL_FIELDS = ""; - private final String object; - - private final String field; - - public OracleLocation(String object, String field) { - this.object = object; - this.field = field; - } - public OracleLocation(String object) { - this.object = object; - this.field = ALL_FIELDS; - } - - - public String getObject() { - return object; - } - - - public String getField() { - return field; + this(object, ALL_FIELDS); } public boolean isAllFields() { return field.equals(ALL_FIELDS); } - public boolean equals(Object o) { - - if (o instanceof OracleLocation l) { - return object.equals(l.object) && field.equals(l.field); - } - - return false; - - } - public String toString() { - if (field.startsWith("[")) { return object + field; } else { return object + "." + field; } - - } - } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocationSet.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocationSet.java index c8910efb3f2..3c72102f6d4 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocationSet.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocationSet.java @@ -6,34 +6,17 @@ import java.util.HashSet; import java.util.Set; -public class OracleLocationSet { +sealed interface OracleLocationSet { + EmptyOracleLocationSet EMPTY = new EmptyOracleLocationSet(); + AllLocsLocationSet ALL_LOCS = new AllLocsLocationSet(); - private final Set locs; - - public static final EmptyOracleLocationSet EMPTY = new EmptyOracleLocationSet(); - - public static final AllLocsLocationSet ALL_LOCS = new AllLocsLocationSet(); - - - public OracleLocationSet() { - locs = new HashSet<>(); - } - - private void add(OracleLocation loc) { - locs.add(loc); - } - - private void add(OracleLocationSet loc) { - locs.addAll(loc.locs); - } - - public static OracleLocationSet singleton(OracleLocation loc) { - OracleLocationSet result = new OracleLocationSet(); + static OracleLocationSet singleton(OracleLocation loc) { + var result = new OracleDefaultLocationSet(); result.add(loc); return result; } - public static OracleLocationSet union(OracleLocationSet l1, OracleLocationSet l2) { + static OracleLocationSet union(OracleLocationSet l1, OracleLocationSet l2) { if (l1 == ALL_LOCS || l2 == ALL_LOCS) { return ALL_LOCS; @@ -47,14 +30,13 @@ public static OracleLocationSet union(OracleLocationSet l1, OracleLocationSet l2 return l1; } - OracleLocationSet result = new OracleLocationSet(); + var result = new OracleDefaultLocationSet(); result.add(l1); result.add(l2); return result; } - public static OracleLocationSet intersect(OracleLocationSet l1, OracleLocationSet l2) { - + static OracleLocationSet intersect(OracleLocationSet l1, OracleLocationSet l2) { if (l1 == EMPTY || l2 == EMPTY) { return EMPTY; } @@ -67,15 +49,18 @@ public static OracleLocationSet intersect(OracleLocationSet l1, OracleLocationSe return l1; } - OracleLocationSet result = new OracleLocationSet(); - for (OracleLocation l : l1.locs) { + + var s1 = (OracleDefaultLocationSet) l1; + var s2 = (OracleDefaultLocationSet) l2; + + var result = new OracleDefaultLocationSet(); + for (OracleLocation l : s1.locs) { if (l2.contains(l)) { result.add(l); } } - - for (OracleLocation l : l2.locs) { + for (OracleLocation l : s2.locs) { if (l1.contains(l)) { result.add(l); } @@ -84,33 +69,36 @@ public static OracleLocationSet intersect(OracleLocationSet l1, OracleLocationSe return result; } + boolean contains(OracleLocation l); +} + +final class OracleDefaultLocationSet implements OracleLocationSet { + final Set locs = new HashSet<>(); + + void add(OracleLocation loc) { + locs.add(loc); + } + + void add(OracleLocationSet loc) { + if (loc instanceof OracleDefaultLocationSet o) + locs.addAll(o.locs); + } + + @Override public boolean contains(OracleLocation l) { for (OracleLocation loc : locs) { - if (loc.equals(l)) { return true; } - if (loc.isAllFields() && loc.getObject().equals(l.getObject())) { + if (loc.isAllFields() && loc.object().equals(l.object())) { return true; } - } - return false; } public String toString() { - - if (this == EMPTY) { - return "Empty"; - } - - if (this == ALL_LOCS) { - return "All"; - } - - StringBuilder result = new StringBuilder(); result.append("{"); @@ -130,15 +118,28 @@ public String toString() { } -class EmptyOracleLocationSet extends OracleLocationSet { +final class EmptyOracleLocationSet implements OracleLocationSet { + @Override public boolean contains(OracleLocation l) { return false; } + + @Override + public String toString() { + return "Empty"; + + } } -class AllLocsLocationSet extends OracleLocationSet { +final class AllLocsLocationSet implements OracleLocationSet { + @Override public boolean contains(OracleLocation l) { return true; } + + @Override + public String toString() { + return "All"; + } } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethod.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethod.java index 0125a8e536e..67220ed8dd9 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethod.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethod.java @@ -3,10 +3,15 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.testgen.oracle; +import com.squareup.javapoet.ClassName; +import com.squareup.javapoet.MethodSpec; +import com.squareup.javapoet.ParameterSpec; +import com.squareup.javapoet.TypeName; +import de.uka.ilkd.key.logic.sort.Sort; + import java.util.List; -import de.uka.ilkd.key.logic.sort.Sort; -import de.uka.ilkd.key.testgen.TestCaseGenerator; +import static de.uka.ilkd.key.testgen.template.Constants.TAB; public class OracleMethod { @@ -45,9 +50,27 @@ public String getBody() { return body; } + public MethodSpec build() { + TypeName retType = TypeName.BOOLEAN; + if (returnType != null) { + retType = ClassName.get("", returnType.name().toString()); + } + + Iterable params = args.stream().map( + it -> ParameterSpec.builder(ClassName.get("", it.sort().name().toString()), + it.name().toString()).build() + ).toList(); + + var m = MethodSpec.methodBuilder(methodName) + .returns(retType) + .addParameters(params) + .addStatement(body); + return m.build(); + } + @Override public String toString() { - String tab = TestCaseGenerator.TAB; + String tab = TAB; StringBuilder argString = new StringBuilder(); for (OracleVariable var : args) { @@ -62,7 +85,7 @@ public String toString() { retType = returnType.name().toString(); } return tab + "public " + retType + " " + methodName + "(" + argString + "){\n" + tab + tab - + body + "\n" + tab + "}"; + + body + "\n" + tab + "}"; } } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethodCall.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethodCall.java index ca6f7638383..5cfa9ad6476 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethodCall.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethodCall.java @@ -3,27 +3,16 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.testgen.oracle; -import java.util.List; - -public class OracleMethodCall implements OracleTerm { +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; - private final OracleMethod method; - private final List args; - private final OracleTerm caller; +import java.util.List; +public record OracleMethodCall(OracleMethod method, List args, + @Nullable OracleTerm caller) + implements OracleTerm { public OracleMethodCall(OracleMethod method, List args) { - super(); - this.method = method; - this.args = args; - caller = null; - } - - public OracleMethodCall(OracleMethod method, List args, - OracleTerm caller) { - super(); - this.method = method; - this.args = args; - this.caller = caller; + this(method, args, null); } public String toString() { @@ -41,5 +30,4 @@ public String toString() { return methodName + "(" + aString + ")"; } } - } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleTerm.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleTerm.java index 98eb962b668..0a703870df5 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleTerm.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleTerm.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.testgen.oracle; -public interface OracleTerm { +public sealed interface OracleTerm + permits OracleBinTerm, OracleConstant, OracleMethodCall, OracleType, OracleUnaryTerm, OracleVariable { } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleType.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleType.java index 7eeffd84192..4e4146f6fcb 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleType.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleType.java @@ -6,11 +6,7 @@ import de.uka.ilkd.key.logic.sort.Sort; public record OracleType(Sort s) implements OracleTerm { - public String toString() { - return s.name().toString(); - } - } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleUnaryTerm.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleUnaryTerm.java index 11760e05f72..0e1772073fa 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleUnaryTerm.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleUnaryTerm.java @@ -26,6 +26,6 @@ public enum Op { public String toString() { - return op2String.get(op) + sub.toString(); + return op2String.get(op) + sub; } } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleVariable.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleVariable.java index 6eafc200f14..b176dfa3234 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleVariable.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleVariable.java @@ -6,36 +6,7 @@ import de.uka.ilkd.key.logic.sort.Sort; public record OracleVariable(String name, Sort sort) implements OracleTerm { - - @Override - public boolean equals(Object obj) { - if (this == obj) { - return true; - } - if (obj == null) { - return false; - } - if (getClass() != obj.getClass()) { - return false; - } - OracleVariable other = (OracleVariable) obj; - if (name == null) { - if (other.name != null) { - return false; - } - } else if (!name.equals(other.name)) { - return false; - } - if (sort == null) { - return other.sort == null; - } else { - return sort.equals(other.sort); - } - } - public String toString() { return name; } - - } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/package-info.java new file mode 100644 index 00000000000..3974d21dcd2 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/package-info.java @@ -0,0 +1,4 @@ +@NullMarked +package de.uka.ilkd.key.testgen.oracle; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/package-info.java new file mode 100644 index 00000000000..ec7115ab415 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/package-info.java @@ -0,0 +1,3 @@ +@NullMarked package de.uka.ilkd.key.testgen; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/settings/TestGenerationSettings.java similarity index 92% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/settings/TestGenerationSettings.java index 96d99994211..da3fd6469b5 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/settings/TestGenerationSettings.java @@ -1,11 +1,16 @@ /* 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.settings; +package de.uka.ilkd.key.testgen.settings; import java.io.File; import java.util.Properties; +import de.uka.ilkd.key.settings.AbstractSettings; +import de.uka.ilkd.key.settings.Configuration; +import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.settings.SettingsConverter; +import de.uka.ilkd.key.testgen.Format; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; @@ -18,7 +23,7 @@ public class TestGenerationSettings extends AbstractSettings { System.getProperty("user.home") + File.separator + "testFiles"; private static final boolean DEFAULT_REMOVEDUPLICATES = true; private static final boolean DEFAULT_USERFL = false; - private static final boolean DEFAULT_USEJUNIT = false; + private static final Format DEFAULT_USEJUNIT = Format.Plain; private static final boolean DEFAULT_INVARIANTFORALL = true; private static final String DEFAULT_OPENJMLPATH = "."; private static final String DEFAULT_OBJENESISPATH = "."; @@ -49,7 +54,7 @@ public class TestGenerationSettings extends AbstractSettings { private String objenesisPath; private boolean removeDuplicates; private boolean useRFL; - private boolean useJunit; + private Format format; private int concurrentProcesses; private boolean invariantForAll; private boolean includePostCondition; @@ -61,7 +66,7 @@ public TestGenerationSettings() { outputPath = DEFAULT_OUTPUTPATH; removeDuplicates = DEFAULT_REMOVEDUPLICATES; useRFL = DEFAULT_USERFL; - useJunit = DEFAULT_USEJUNIT; + format = Format.Plain; concurrentProcesses = DEFAULT_CONCURRENTPROCESSES; invariantForAll = DEFAULT_INVARIANTFORALL; openjmlPath = DEFAULT_OPENJMLPATH; @@ -74,7 +79,7 @@ public TestGenerationSettings(TestGenerationSettings data) { maxUnwinds = data.maxUnwinds; outputPath = data.outputPath; removeDuplicates = data.removeDuplicates; - useJunit = data.useJunit; + format = data.format; useRFL = data.useRFL; concurrentProcesses = data.concurrentProcesses; invariantForAll = data.invariantForAll; @@ -136,7 +141,7 @@ public void readSettings(Properties props) { setRemoveDuplicates(SettingsConverter.read(props, prefix + PROP_REMOVE_DUPLICATES, DEFAULT_REMOVEDUPLICATES)); setRFL(SettingsConverter.read(props, prefix + PROP_USE_RFL, DEFAULT_USERFL)); - setUseJunit(SettingsConverter.read(props, prefix + PROP_USE_JUNIT, DEFAULT_USEJUNIT)); + setFormat(Format.valueOf(SettingsConverter.read(props, prefix + PROP_USE_JUNIT, DEFAULT_USEJUNIT.name()))); setConcurrentProcesses(SettingsConverter.read(props, prefix + PROP_CONCURRENT_PROCESSES, DEFAULT_CONCURRENTPROCESSES)); setInvariantForAll(SettingsConverter.read(props, @@ -198,10 +203,10 @@ public void setRFL(boolean useRFL) { } - public void setUseJunit(boolean useJunit) { - var old = this.useJunit; - this.useJunit = useJunit; - firePropertyChange(PROP_USE_JUNIT, old, this.useJunit); + public void setFormat(Format format) { + var old = this.format; + this.format = format; + firePropertyChange(PROP_USE_JUNIT, old, this.format); } @@ -230,8 +235,8 @@ public boolean useRFL() { return useRFL; } - public boolean useJunit() { - return useJunit; + public Format useJunit() { + return format; } @@ -246,7 +251,7 @@ public void writeSettings(Properties props) { SettingsConverter.store(props, prefix + PROP_OUTPUT_PATH, outputPath); SettingsConverter.store(props, prefix + PROP_REMOVE_DUPLICATES, removeDuplicates); SettingsConverter.store(props, prefix + PROP_USE_RFL, useRFL); - SettingsConverter.store(props, prefix + PROP_USE_JUNIT, useJunit); + SettingsConverter.store(props, prefix + PROP_USE_JUNIT, format); SettingsConverter.store(props, prefix + PROP_OPENJML_PATH, openjmlPath); SettingsConverter.store(props, prefix + PROP_OBJENESIS_PATH, objenesisPath); SettingsConverter.store(props, prefix + PROP_INCLUDE_POST_CONDITION, includePostCondition); @@ -263,7 +268,7 @@ public void readSettings(Configuration props) { setOutputPath(cat.getString(PROP_OUTPUT_PATH, DEFAULT_OUTPUTPATH)); setRemoveDuplicates(cat.getBool(PROP_REMOVE_DUPLICATES, DEFAULT_REMOVEDUPLICATES)); setRFL(cat.getBool(PROP_USE_RFL, DEFAULT_USERFL)); - setUseJunit(cat.getBool(PROP_USE_JUNIT, DEFAULT_USEJUNIT)); + setFormat(cat.getEnum(PROP_USE_JUNIT, Format.Plain)); setConcurrentProcesses(cat.getInt(PROP_CONCURRENT_PROCESSES, DEFAULT_CONCURRENTPROCESSES)); setInvariantForAll(cat.getBool(PROP_INVARIANT_FOR_ALL, DEFAULT_INVARIANTFORALL)); setOpenjmlPath(cat.getString(PROP_OPENJML_PATH, DEFAULT_OPENJMLPATH)); @@ -283,7 +288,7 @@ public void writeSettings(Configuration props) { cat.set(PROP_OUTPUT_PATH, outputPath); cat.set(PROP_REMOVE_DUPLICATES, removeDuplicates); cat.set(PROP_USE_RFL, useRFL); - cat.set(PROP_USE_JUNIT, useJunit); + cat.set(PROP_USE_JUNIT, format); cat.set(PROP_OPENJML_PATH, openjmlPath); cat.set(PROP_OBJENESIS_PATH, objenesisPath); cat.set(PROP_INCLUDE_POST_CONDITION, includePostCondition); diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/settings/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/settings/package-info.java new file mode 100644 index 00000000000..06e6b9410f2 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/settings/package-info.java @@ -0,0 +1,3 @@ +@NullMarked package de.uka.ilkd.key.testgen.settings; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractCounterExampleGenerator.java similarity index 98% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractCounterExampleGenerator.java index 61546a95392..ec09a9a3400 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractCounterExampleGenerator.java @@ -1,7 +1,7 @@ /* 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.smt.counterexample; +package de.uka.ilkd.key.testgen.smt.counterexample; import java.util.LinkedList; import java.util.List; @@ -9,7 +9,7 @@ import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; -import de.uka.ilkd.key.macros.SemanticsBlastingMacro; +import de.uka.ilkd.key.testgen.macros.SemanticsBlastingMacro; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.prover.ProverTaskListener; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractSideProofCounterExampleGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractSideProofCounterExampleGenerator.java similarity index 96% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractSideProofCounterExampleGenerator.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractSideProofCounterExampleGenerator.java index 4345c938cb4..1b824ad3067 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractSideProofCounterExampleGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractSideProofCounterExampleGenerator.java @@ -1,7 +1,7 @@ /* 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.smt.counterexample; +package de.uka.ilkd.key.testgen.smt.counterexample; import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.logic.Choice; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/package-info.java new file mode 100644 index 00000000000..566669ee8e9 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/package-info.java @@ -0,0 +1,3 @@ +@NullMarked package de.uka.ilkd.key.testgen.smt.counterexample; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/AbstractTestGenerator.java similarity index 94% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/AbstractTestGenerator.java index 2fbfc7b1ce4..2bf7f0ea5f4 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/AbstractTestGenerator.java @@ -1,22 +1,12 @@ /* 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.smt.testgen; - -import java.io.IOException; -import java.util.*; +package de.uka.ilkd.key.testgen.smt.testgen; import de.uka.ilkd.key.control.UserInterfaceControl; -import de.uka.ilkd.key.logic.Choice; -import de.uka.ilkd.key.logic.JavaBlock; -import de.uka.ilkd.key.logic.Semisequent; -import de.uka.ilkd.key.logic.Sequent; -import de.uka.ilkd.key.logic.SequentFormula; -import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.UpdateApplication; import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; -import de.uka.ilkd.key.macros.SemanticsBlastingMacro; -import de.uka.ilkd.key.macros.TestGenMacro; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; @@ -28,25 +18,26 @@ import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; import de.uka.ilkd.key.rule.OneStepSimplifier; import de.uka.ilkd.key.rule.RuleApp; -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.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.TestGenerationSettings; +import de.uka.ilkd.key.settings.*; import de.uka.ilkd.key.smt.*; import de.uka.ilkd.key.smt.model.Model; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; import de.uka.ilkd.key.testgen.TestCaseGenerator; +import de.uka.ilkd.key.testgen.TestgenUtils; +import de.uka.ilkd.key.testgen.macros.SemanticsBlastingMacro; +import de.uka.ilkd.key.testgen.macros.TestGenMacro; +import de.uka.ilkd.key.testgen.settings.TestGenerationSettings; +import de.uka.ilkd.key.testgen.template.Templates; import de.uka.ilkd.key.util.ProofStarter; import de.uka.ilkd.key.util.SideProofUtil; - import org.key_project.util.collection.ImmutableList; - import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import java.io.IOException; +import java.util.*; + /** * Implementations of this class are used generate test cases or a given {@link Proof}. *

@@ -114,7 +105,7 @@ public void generateTestCases(final StopRequest stopRequest, final TestGeneratio log.writeln("No test data constraints were extracted."); } final Collection problems = new LinkedList<>(); - log.writeln("Test data generation: appling semantic blasting macro on proofs"); + log.writeln("Test data generation: applying semantic blasting macro on proofs"); try { for (final Proof proof : proofs) { if (stopRequest != null && stopRequest.shouldStop()) { @@ -326,7 +317,7 @@ protected Proof createProof(UserInterfaceControl ui, Proof oldProof, String newN private boolean hasModalities(Term t, boolean checkUpdates) { final JavaBlock jb = t.javaBlock(); - if (jb != null && !jb.isEmpty()) { + if (!jb.isEmpty()) { return true; } if (t.op() == UpdateApplication.UPDATE_APPLICATION && checkUpdates) { @@ -334,7 +325,7 @@ private boolean hasModalities(Term t, boolean checkUpdates) { } boolean res = false; for (int i = 0; i < t.arity() && !res; i++) { - res |= hasModalities(t.sub(i), checkUpdates); + res = hasModalities(t.sub(i), checkUpdates); } return res; } @@ -365,7 +356,7 @@ protected void handleLauncherStopped(SolverLauncher launcher, protected void generateFiles(Collection problemSolvers, TestGenerationLog log, Proof originalProof) throws IOException { - final TestCaseGenerator tg = new TestCaseGenerator(originalProof); + final TestCaseGenerator tg = new TestCaseGenerator(originalProof, Templates.TEMPLATE_JUNIT4); tg.setLogger(log); tg.generateJUnitTestSuite(problemSolvers); @@ -402,7 +393,7 @@ public Collection filterSolverResultsAndShowSolverStatistics( solvedPaths++; if (solver.getSocket().getQuery() != null) { final Model m = solver.getSocket().getQuery().getModel(); - if (TestCaseGenerator.modelIsOK(m)) { + if (TestgenUtils.modelIsOK(m)) { output.add(solver); } else { problem++; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/MemoryTestGenerationLog.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/MemoryTestGenerationLog.java similarity index 82% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/MemoryTestGenerationLog.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/MemoryTestGenerationLog.java index 9edcd12b5da..0e9ab0d9379 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/MemoryTestGenerationLog.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/MemoryTestGenerationLog.java @@ -1,9 +1,9 @@ /* 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.smt.testgen; +package de.uka.ilkd.key.testgen.smt.testgen; -import de.uka.ilkd.key.testgen.TestCaseGenerator; +import static de.uka.ilkd.key.testgen.template.Constants.NEW_LINE; /** * Implementation of {@link TestGenerationLog} which stores the log in memory. @@ -22,7 +22,7 @@ public class MemoryTestGenerationLog implements TestGenerationLog { @Override public void writeln(String string) { sb.append(string); - sb.append(TestCaseGenerator.NEW_LINE); + sb.append(NEW_LINE); } /** @@ -31,7 +31,7 @@ public void writeln(String string) { @Override public void write(String string) { sb.append(string); - sb.append(TestCaseGenerator.NEW_LINE); + sb.append(NEW_LINE); } /** @@ -40,7 +40,7 @@ public void write(String string) { @Override public void writeException(Throwable t) { sb.append(t.getMessage()); - sb.append(TestCaseGenerator.NEW_LINE); + sb.append(NEW_LINE); } /** diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/StopRequest.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/StopRequest.java similarity index 83% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/StopRequest.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/StopRequest.java index 1907bae9a00..cafa74721ee 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/StopRequest.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/StopRequest.java @@ -1,7 +1,7 @@ /* 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.smt.testgen; +package de.uka.ilkd.key.testgen.smt.testgen; public interface StopRequest { boolean shouldStop(); diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/TestGenerationLog.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/TestGenerationLog.java similarity index 88% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/TestGenerationLog.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/TestGenerationLog.java index 76a3881c74d..589c38e881e 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/TestGenerationLog.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/TestGenerationLog.java @@ -1,7 +1,7 @@ /* 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.smt.testgen; +package de.uka.ilkd.key.testgen.smt.testgen; public interface TestGenerationLog { void writeln(String string); diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/package-info.java new file mode 100644 index 00000000000..93ec5eb8f07 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/package-info.java @@ -0,0 +1,3 @@ +@NullMarked package de.uka.ilkd.key.testgen.smt.testgen; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Constants.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Constants.java new file mode 100644 index 00000000000..5b2e7dc80da --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Constants.java @@ -0,0 +1,29 @@ +package de.uka.ilkd.key.testgen.template; + +import org.key_project.util.java.StringUtil; + +public interface Constants { + + /** + * Constant for the line break which is used by the operating system. + *

+ * Do not use {@code \n}! + */ + String NEW_LINE = StringUtil.NEW_LINE; + String NULLABLE = "/*@ nullable */"; + String ALL_OBJECTS = "allObjects"; + String ALL_INTS = "allInts"; + String ALL_BOOLS = "allBools"; + String ALL_HEAPS = "allHeaps"; + String ALL_FIELDS = "allFields"; + String ALL_SEQ = "allSeq"; + String ALL_LOCSETS = "allLocSets"; + + String OBJENESIS_NAME = "objenesis-2.2.jar"; + + String OLDMap = "old"; + + String TAB = " "; + + String DUMMY_POSTFIX = "DummyImpl"; +} diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/JUnit4Template.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/JUnit4Template.java new file mode 100644 index 00000000000..15102178df4 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/JUnit4Template.java @@ -0,0 +1,5 @@ +package de.uka.ilkd.key.testgen.template; + +public class JUnit4Template extends PlainTemplate { + +} \ No newline at end of file diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/PlainTemplate.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/PlainTemplate.java new file mode 100644 index 00000000000..67f7ac45760 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/PlainTemplate.java @@ -0,0 +1,75 @@ +package de.uka.ilkd.key.testgen.template; + +import static de.uka.ilkd.key.testgen.template.Constants.OBJENESIS_NAME; + +public class PlainTemplate implements Template { + @Override + public String shCompileWithOpenJML() { + return """ + #!/bin/bash + + if [ -e "openjml.jar" ]; then + java -jar openjml.jar -cp "." -rac *.java + else + echo "openjml.jar not found!" + echo "Download openJML from http://sourceforge.net/projects/jmlspecs/files/"%s + echo "Copy openjml.jar into the directory with test files." + """; + } + + @Override + public String shCompileWithOpenJML(String openJMLPath, String objenesisPath) { + return """ + #!/bin/bash + if [ -e %s/openjml.jar ]; then + if [ -e %s ]; then + java -jar openJMLPath/openjml.jar -cp "." %s + " -rac *" + JAVA_FILE_EXTENSION_WITH_DOT + NEW_LINE + " else" + NEW_LINE + echo "objenesis-2.2.jar not found! + fi + else + echo "openjml.jar not found!" + echo "Download openJML from http://sourceforge.net/projects/jmlspecs/files/" + echo "Copy openjml.jar into the directory with test files." + fi""".formatted( + openJMLPath, objenesisPath, objenesisPath + "/" + OBJENESIS_NAME); + } + + + @Override + public String shExecuteWithOpenJML(String path, String objenesisPath) { + return """ + #!/bin/bash + if [ ! -e path/jmlruntime.jar ]; then + echo "jmlruntime.jar not found!" + echo "Download openJML from http://sourceforge.net/projects/jmlspecs/files/"" + echo "Copy jmlruntime.jar into the directory with test files."" + exit 1 + fi + + if [ ! -e path/jmlspecs.jar" ]; then + echo "jmlspecs.jar not found!" + echo "Download openJML from http://sourceforge.net/projects/jmlspecs/files/" + echo "Copy jmlspecs.jar into the directory with test files." + exit 2 + fi + + if [ ! -e "" + objenesisPath/OBJENESIS_NAME ]; then + echo "objenesis-2.2.jar not found!" + exit 3 + fi + + + if [ "$1" = "" ] ; then + echo "Provide the test driver as an argument (without + JAVA_FILE_EXTENSION_WITH_DOT + " postfix). For example:"" + NEW_LINE + echo " executeWithOpenJML.sh TestGeneric0 " + echo "Make sure that jmlruntime.jar and jmlspecs.jar are in the"" + echo "current directory." + exit 4 + fi + + java -cp " + objenesisPath/OBJENESIS_NAME + ":" + path / "jmlruntime.jar:"/ "jmlspecs.jar:. $1 + """; + } + +} diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Template.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Template.java new file mode 100644 index 00000000000..89c3596437c --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Template.java @@ -0,0 +1,9 @@ +package de.uka.ilkd.key.testgen.template; + +public interface Template { + String shCompileWithOpenJML(); + + String shCompileWithOpenJML(String openJMLPath, String objenesisPath); + + String shExecuteWithOpenJML(String path, String objenesisPath); +} diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Templates.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Templates.java new file mode 100644 index 00000000000..29838db060b --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/Templates.java @@ -0,0 +1,5 @@ +package de.uka.ilkd.key.testgen.template; + +public class Templates { + public static final Template TEMPLATE_JUNIT4 = new JUnit4Template(); +} diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/package-info.java new file mode 100644 index 00000000000..08c7e8ca93c --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/template/package-info.java @@ -0,0 +1,3 @@ +@NullMarked package de.uka.ilkd.key.testgen.template; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file diff --git a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCE.java b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCE.java index 4c6b368f59f..3ba5df5d0a4 100644 --- a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCE.java +++ b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCE.java @@ -8,7 +8,7 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.macros.FinishSymbolicExecutionMacro; -import de.uka.ilkd.key.macros.SemanticsBlastingMacro; +import de.uka.ilkd.key.testgen.macros.SemanticsBlastingMacro; import de.uka.ilkd.key.macros.TryCloseMacro; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; @@ -138,7 +138,7 @@ public void testMiddle() throws Exception { TryCloseMacro close = new TryCloseMacro(); close.applyTo(env.getUi(), proof, proof.openEnabledGoals(), null, null); // should not be provable - assertTrue(proof.openGoals().size() > 0); + assertTrue(!proof.openGoals().isEmpty()); // there should be a counterexample for each goal... for (Goal g : proof.openGoals()) { SemanticsBlastingMacro sb = new SemanticsBlastingMacro(); diff --git a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/testgen/TestTestgen.java b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/testgen/TestTestgen.java index 210a8b84db9..5ded65d639e 100644 --- a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/testgen/TestTestgen.java +++ b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/testgen/TestTestgen.java @@ -7,7 +7,7 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; -import de.uka.ilkd.key.macros.TestGenMacro; +import de.uka.ilkd.key.testgen.macros.TestGenMacro; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java index a3b4c5deb74..adcd1f4514d 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java @@ -18,13 +18,13 @@ import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.smt.SolverListener; import de.uka.ilkd.key.logic.Sequent; -import de.uka.ilkd.key.macros.SemanticsBlastingMacro; +import de.uka.ilkd.key.testgen.macros.SemanticsBlastingMacro; import de.uka.ilkd.key.proof.*; import de.uka.ilkd.key.settings.DefaultSMTSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.smt.SolverLauncherListener; -import de.uka.ilkd.key.smt.counterexample.AbstractCounterExampleGenerator; -import de.uka.ilkd.key.smt.counterexample.AbstractSideProofCounterExampleGenerator; +import de.uka.ilkd.key.testgen.smt.counterexample.AbstractCounterExampleGenerator; +import de.uka.ilkd.key.testgen.smt.counterexample.AbstractSideProofCounterExampleGenerator; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; import org.slf4j.Logger; diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java index 087e4c5d59f..9bd2aa7d82a 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java @@ -10,7 +10,7 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; -import de.uka.ilkd.key.smt.testgen.TestGenerationLog; +import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLog; import de.uka.ilkd.key.util.ThreadUtilities; import org.slf4j.Logger; diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java index e89942b18ac..8ba1c060031 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java @@ -18,8 +18,8 @@ import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; -import de.uka.ilkd.key.smt.testgen.AbstractTestGenerator; -import de.uka.ilkd.key.smt.testgen.StopRequest; +import de.uka.ilkd.key.testgen.smt.testgen.AbstractTestGenerator; +import de.uka.ilkd.key.testgen.smt.testgen.StopRequest; /** * The worker must be started using method {@link TGWorker#start()} and not diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenExtension.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenExtension.java index a870a2441d4..a2020f4b520 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenExtension.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenExtension.java @@ -16,7 +16,7 @@ import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeSettings; import de.uka.ilkd.key.gui.settings.SettingsProvider; -import de.uka.ilkd.key.macros.TestGenMacro; +import de.uka.ilkd.key.testgen.macros.TestGenMacro; import org.jspecify.annotations.NonNull; diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java index 886cae40008..b748d8d39f1 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java @@ -8,7 +8,8 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.settings.SettingsPanel; import de.uka.ilkd.key.gui.settings.SettingsProvider; -import de.uka.ilkd.key.settings.TestGenerationSettings; +import de.uka.ilkd.key.testgen.Format; +import de.uka.ilkd.key.testgen.settings.TestGenerationSettings; public class TestgenOptionsPanel extends SettingsPanel implements SettingsProvider { private static final long serialVersionUID = -2170118134719823425L; @@ -59,7 +60,7 @@ public class TestgenOptionsPanel extends SettingsPanel implements SettingsProvid private final JSpinner maxProcesses; private final JSpinner maxUnwinds; private final JCheckBox symbolicEx; - private final JCheckBox useJUnit; + private final JComboBox useJUnit; private final JCheckBox invariantForAll; private final JCheckBox includePostCondition; private final JCheckBox removeDuplicates; @@ -115,10 +116,10 @@ private JTextField getObjenesisPanel() { }); } - private JCheckBox getJUnitPanel() { - return addCheckBox("Generate JUnit and test oracle", INFO_USE_JUNIT, false, val -> { - settings.setUseJunit(val); - }); + private JComboBox getJUnitPanel() { + return addComboBox("Set the format", INFO_USE_JUNIT, 0, val -> { + settings.setFormat(val); + }, Format.values()); } private JCheckBox getRemoveDuplicatesPanel() { @@ -162,7 +163,7 @@ public JPanel getPanel(MainWindow window) { settings = new TestGenerationSettings(TestGenerationSettings.getInstance()); includePostCondition.setSelected(settings.includePostCondition()); invariantForAll.setSelected(settings.invariantForAll()); - useJUnit.setSelected(settings.useJunit()); + useJUnit.setSelectedItem(settings.useJunit()); symbolicEx.setSelected(settings.getApplySymbolicExecution()); removeDuplicates.setSelected(settings.removeDuplicates()); checkboxRFL.setSelected(settings.useRFL());