wip

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.12-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.12.1-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

key.core/src/test/java/de/uka/ilkd/key/macros/scripts/TestProofScriptCommand.java

@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.macros.scripts;
 
+import java.io.File;
 import java.io.FileNotFoundException;
 import java.io.IOException;
 import java.net.URI;
@@ -13,6 +14,7 @@
 import java.util.Arrays;
 import java.util.List;
 
+import com.fasterxml.jackson.dataformat.yaml.YAMLGenerator;
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.control.KeYEnvironment;
 import de.uka.ilkd.key.java.Position;
@@ -31,6 +33,7 @@
 import org.junit.jupiter.params.provider.MethodSource;
 
 import static org.assertj.core.api.Assertions.assertThat;
+import static org.assertj.core.api.Assertions.in;
 import static org.junit.jupiter.api.Assertions.assertTrue;
 
 
@@ -39,7 +42,7 @@
  */
 public class TestProofScriptCommand {
     public record TestInstance(String name, String key, String script, String exception,
-            String[] goals, Integer selectedGoal) {
+                               String[] goals, Integer selectedGoal) {
     }
 
 
@@ -49,9 +52,24 @@ public static List<Arguments> data() throws IOException, URISyntaxException {
             throw new FileNotFoundException("Cannot find resource 'cases'.");
         }
 
-        var objectMapper = new ObjectMapper(new YAMLFactory());
+        var objectMapper = new ObjectMapper(new YAMLFactory()
+                .configure(YAMLGenerator.Feature.INDENT_ARRAYS_WITH_INDICATOR,true)
+                .configure(YAMLGenerator.Feature.INDENT_ARRAYS,true)
+                .configure(YAMLGenerator.Feature.LITERAL_BLOCK_STYLE,true)
+                .configure(YAMLGenerator.Feature.WRITE_DOC_START_MARKER,false)
+                .configure(YAMLGenerator.Feature.USE_PLATFORM_LINE_BREAKS,false)
+                .configure(YAMLGenerator.Feature.MINIMIZE_QUOTES,true));
+
         objectMapper.findAndRegisterModules();
         TestInstance[] instances = objectMapper.readValue(url, TestInstance[].class);
+
+        for (TestInstance instance : instances) {
+            objectMapper.writeValue(new File(
+                    "C:\\Users\\weigl\\IdeaProjects\\key\\key.core\\src\\test\\resources\\de\\uka\\ilkd\\key\\macros\\scripts",
+                    instance.name + ".yml"
+            ), instance);
+        }
+
         return Arrays.stream(instances).map(Arguments::of).toList();
     }
 

key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java

@@ -9,8 +9,10 @@
 import java.nio.charset.StandardCharsets;
 import java.nio.file.Files;
 import java.nio.file.Path;
+import java.nio.file.Paths;
 import java.util.*;
 
+import com.fasterxml.jackson.dataformat.yaml.YAMLGenerator;
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.control.KeYEnvironment;
 import de.uka.ilkd.key.logic.Sequent;
@@ -67,43 +69,50 @@ public class MasterHandlerTest {
 
     public static List<Arguments> data()
             throws IOException, URISyntaxException, ProblemLoaderException {
-        try (var input = MasterHandlerTest.class.getResourceAsStream("cases.yml")) {
-            var om = new ObjectMapper(new YAMLFactory());
-            TypeReference<HashMap<String, TestData>> typeRef = new TypeReference<>() {
-            };
-            Map<String, TestData> preData = om.readValue(input, typeRef);
-            var result = new ArrayList<Arguments>(preData.size());
-            for (var entry : preData.entrySet()) {
-                final var value = entry.getValue();
+        var om = new ObjectMapper(new YAMLFactory());
+        var path = Paths.get("src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/");
+        try (var walker = Files.walk(path)) {
+            var files = walker.filter(it -> it.getFileName().endsWith("yml")).toList();
+            var result = new ArrayList<Arguments>(files.size());
+            for (Path pFile : files) {
+                var file = pFile.toFile();
+
+                TestData value = om.readValue(file, TestData.class);
 
                 if (value.state == TestDataState.IGNORE) {
-                    LOGGER.info("Test {} case has been marked ignore", entry.getKey());
+                    LOGGER.info("Test {} case has been marked ignore", file);
                     continue;
                 }
-
-                final var testData = value.load(entry.getKey());
+                final var testData = value.load(file.getName().replace(".yml", ""));
                 result.add(Arguments.of(testData));
             }
             return result;
         }
     }
 
+    /**
+     * Describes the state of a test instance.
+     */
     public enum TestDataState {
         EMPTY, EXTENDED, IGNORE
     }
 
+    /**
+     * Expected outcome of a test instance.
+     */
     public enum Expectation {
         VALID, FAIL, IRRELEVANT
     }
 
     /**
      * This class contains the information about the test fixtures that is loaded via the YAML.
-     * @param contains a list of strings that are expected in the SMT translation
+     *
+     * @param contains    a list of strings that are expected in the SMT translation
      * @param smtSettings required key/values in the smt settings.
-     * @param expected expected output of Z3
-     * @param state    state of the test
-     * @param javaSrc  path to necessary java sources
-     * @param keySrc   contents of the key file to be loaded.
+     * @param expected    expected output of Z3
+     * @param state       state of the test
+     * @param javaSrc     path to necessary java sources
+     * @param keySrc      contents of the key file to be loaded.
      */
     public record TestData(List<String> contains,
                            Properties smtSettings,
@@ -119,7 +128,7 @@ private LoadedTestData load(String name) throws IOException, ProblemLoaderExcept
                 Path srcDir = Files.createTempDirectory("SMT_key_" + name);
                 Path tmpSrc = srcDir.resolve("src.java");
                 Files.writeString(tmpSrc, javaSrc);
-                keySrc += "\n\\javaSource \"%s\";\n".formatted(srcDir);
+                keySrc += "\n/javaSource \"%s\";\n".formatted(srcDir);
             }
 
             Path tmpKey = Files.createTempFile("SMT_key_%s".formatted(name), ".key");
@@ -170,7 +179,7 @@ void testTranslation(LoadedTestData data) throws Exception {
     void testZ3(LoadedTestData data) throws Exception {
         Assumptions.assumeTrue(Z3_SOLVER != null);
         Assumptions.assumeTrue(Z3_SOLVER.isInstalled(false),
-            "Z3 is not installed, this testcase is ignored.");
+                "Z3 is not installed, this testcase is ignored.");
 
         var expectation = data.data.expected;
         Assumptions.assumeTrue(expectation != null, "No Z3 expectation.");
@@ -187,9 +196,9 @@ void testZ3(LoadedTestData data) throws Exception {
 
         try {
             String lookFor = switch (expectation) {
-            case VALID -> "unsat";
-            case FAIL -> "(sat|timeout)";
-            case IRRELEVANT -> null;
+                case VALID -> "unsat";
+                case FAIL -> "(sat|timeout)";
+                case IRRELEVANT -> null;
             };
 
             if (lookFor != null) {
@@ -205,7 +214,7 @@ void testZ3(LoadedTestData data) throws Exception {
 
             if (!STRICT_TEST) {
                 assumeFalse(data.data.state == TestDataState.EXTENDED,
-                    "This is an extended test (will be run only in strict mode)");
+                        "This is an extended test (will be run only in strict mode)");
             }
 
             if (lookFor != null) {

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/bool1.yml

@@ -0,0 +1,11 @@
+---
+contains:
+  - (assert (not (=> (or (and u_b u_b) u_b) (= (not u_b) (and true false)))))
+smtSettings: null
+expected: VALID
+state: null
+javaSrc: null
+keySrc: |-
+  \predicates { b; }
+
+  \problem { b&b | b -> (!b <-> true & false) }

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/bool2.yml

@@ -0,0 +1,15 @@
+---
+contains:
+  - |-
+    (declare-fun u_p () Bool)
+    (declare-fun u_b () U)
+  - (assert (not (=> (= u_p (= u_b (b2u true))) (= (not u_p) (= u_b (b2u false))))))
+smtSettings: null
+expected: VALID
+state: null
+javaSrc: null
+keySrc: |-
+  \predicates { p; }
+  \functions { boolean b; }
+
+  \problem { (p <-> b=TRUE) -> (!p <-> b=FALSE) }

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/bool3.yml

@@ -0,0 +1,14 @@
+---
+contains:
+  - |-
+    (assert (= (ite (< 2 1) (b2u true) (b2u false))
+               (ite (> 2 1) (b2u true) (b2u false))))
+smtSettings: null
+expected: VALID
+state: null
+javaSrc: null
+keySrc: |-
+  \predicates { p; }
+  \functions { boolean b; }
+
+  \problem { \if(2<1)\then(TRUE)\else(FALSE) != \if(2>1)\then(TRUE)\else(FALSE) }

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/cast1.yml

@@ -0,0 +1,11 @@
+---
+contains:
+  - |-
+    (assert (forall ((x U) (t T)) (! (subtype (typeof (cast x t)) t) :pattern ((cast x t)))))
+    (assert (forall ((x U) (t T)) (! (=> (subtype (typeof x) t) (= (cast x t) x)) :pattern ((cast x t)))))
+  - (assert (not (= (cast (i2u 42) sort_int) (i2u 42))))
+smtSettings: null
+expected: VALID
+state: null
+javaSrc: null
+keySrc: "\\problem { (int)42 = 42 }"

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/cast2.yml

@@ -0,0 +1,12 @@
+---
+contains:
+  - (assert (not (= (cast (k_select u_heap u_o u_FF) sort_int) (cast (k_seqGet u_s
+    (i2u 42)) sort_int))))
+smtSettings: null
+expected: IRRELEVANT
+state: null
+javaSrc: null
+keySrc: |-
+  \functions { Field FF; Seq s; java.lang.Object o; }
+
+  \problem { int::select(heap, o, FF) = int::seqGet(s, 42) }

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/cast3.yml

@@ -0,0 +1,8 @@
+---
+contains:
+  - (assert (not (= (cast (i2u 42) sort_any) (i2u 42))))
+smtSettings: null
+expected: VALID
+state: EXTENDED
+javaSrc: null
+keySrc: "\\problem { (any)42 = 42 }"

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/ex1.yml

@@ -0,0 +1,16 @@
+---
+contains:
+  - |-
+    ; --- Sequent
+    (assert (not (exists ((var_x Int))
+           (= (i2u (* 3 var_x)) (i2u 42)))))
+smtSettings: null
+expected: VALID
+state: null
+javaSrc: null
+keySrc: |-
+  \programVariables { int p; }
+
+  \problem {
+     \exists int x; (3*x = 42)
+  }

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/ex2.yml

@@ -0,0 +1,16 @@
+---
+contains:
+  - |-
+    ; --- Sequent
+    (assert (not (exists ((var_x Int))
+           (= (i2u var_x) (i2u 42)))))
+smtSettings: null
+expected: VALID
+state: null
+javaSrc: null
+keySrc: |-
+  \programVariables { int p; }
+
+  \problem {
+     \exists int x; (x = 42)
+  }

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/float.eq.yml

@@ -0,0 +1,11 @@
+---
+contains:
+  - (assert (not (= (fp.isNaN (u2d u_doubleNaN)) (not (fp.eq (u2d u_doubleNaN) (u2d
+    u_doubleNaN))))))
+smtSettings: null
+expected: VALID
+state: null
+javaSrc: null
+keySrc: |-
+  \programVariables { double doubleNaN; }
+  \problem { doubleIsNaN(doubleNaN) <-> !eqDouble(doubleNaN, doubleNaN) }

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/float.sinDouble.yml

@@ -0,0 +1,9 @@
+---
+contains:
+  - "(assert (not (fp.lt (fp.neg (fp #b0 #b10000000000 #b0000000000000000000000000000000000000000000000000000))\
+    \ (sinDouble (fp #b0 #b10000000001 #b0000000000000000000000000000000000000000000000000000)))))"
+smtSettings: null
+expected: VALID
+state: null
+javaSrc: null
+keySrc: "\\problem { -2d < sinDouble(4.0d) }"

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/float.sqrt1.yml

@@ -0,0 +1,10 @@
+---
+contains:
+  - "(assert (not (= (d2u (fp #b0 #b10000000000 #b0000000000000000000000000000000000000000000000000000))\
+    \ (d2u (fp.sqrt RNE (fp #b0 #b10000000001 #b0000000000000000000000000000000000000000000000000000))))))"
+smtSettings:
+  '[NewSMT]sqrtSMTTranslation': SMT
+expected: VALID
+state: null
+javaSrc: null
+keySrc: "\\problem { 2.0d = sqrtDouble(4.0d) }"

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/float.sqrt2.yml

@@ -0,0 +1,10 @@
+---
+contains:
+  - "(assert (not (= (d2u (fp #b0 #b10000000000 #b0000000000000000000000000000000000000000000000000000))\
+    \ (d2u (sqrtDouble (fp #b0 #b10000000001 #b0000000000000000000000000000000000000000000000000000))))))"
+smtSettings:
+  '[NewSMT]sqrtSMTTranslation': AXIOMS
+expected: FAIL
+state: null
+javaSrc: null
+keySrc: "\\problem { 2.0d = sqrtDouble(4.0d) }"

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/float1.yml

@@ -0,0 +1,9 @@
+---
+contains:
+  - "(assert (not (= (f2u (fp #b0 #b01111111 #b00000000000000000000000)) (f2u (fp\
+    \ #b0 #b10000000 #b00000000000000000000000)))))"
+smtSettings: null
+expected: IRRELEVANT
+state: null
+javaSrc: null
+keySrc: "\\problem { 1.0f = 2.0f }"

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/float2.yml

@@ -0,0 +1,9 @@
+---
+contains:
+  - "(assert (not (= (f2u (fp #b0 #b00000000 #b00000000000000000000000)) (f2u (fp.sub\
+    \ RNE (fp #b0 #b01111111 #b00000000000000000000000) (fp #b0 #b01111111 #b00000000000000000000000))))))"
+smtSettings: null
+expected: VALID
+state: null
+javaSrc: null
+keySrc: "\\problem { 0.0f = subFloat(1.0f, 1.0f) }"

key.core/src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/heap1.yml

@@ -0,0 +1,12 @@
+---
+contains:
+  - (assert (not (=> (not (= u_FF |field_java.lang.Object::<created>|)) (= (k_select
+    (k_store u_heap u_o u_FF (i2u 42)) u_o u_FF) (i2u 42)))))
+smtSettings: null
+expected: VALID
+state: EXTENDED
+javaSrc: null
+keySrc: |-
+  \functions { Field FF; java.lang.Object o; }
+
+  \problem { FF != java.lang.Object::<created> -> any::select(store(heap, o, FF, 42), o, FF) = 42 }