more of everything

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/java/SpecialJavaPrinter.java

@@ -28,7 +28,6 @@
 import com.github.javaparser.symbolsolver.resolution.typesolvers.CombinedTypeSolver;
 import com.google.common.cache.Cache;
 import com.google.common.cache.CacheBuilder;
-import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.NullMarked;
 import org.jspecify.annotations.Nullable;
 

key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java

@@ -4,15 +4,15 @@
 package de.uka.ilkd.key.java.transformations.pipeline;
 
 
+import javax.annotation.processing.Generated;
+
 import com.github.javaparser.ast.CompilationUnit;
 import com.github.javaparser.ast.Node;
 import com.github.javaparser.ast.body.TypeDeclaration;
 import com.github.javaparser.ast.expr.StringLiteralExpr;
 import com.github.javaparser.ast.nodeTypes.NodeWithAnnotations;
 import org.jspecify.annotations.NullMarked;
 
-import javax.annotation.processing.Generated;
-
 /**
  * The JavaDL requires some implicit fields, that are available in each
  * Java class. The name of the implicit fields starts usually with a dollar sign.
@@ -90,7 +90,7 @@ public static RuntimeException reportError(Node node, String message, Object...
 
     protected void addGenerated(NodeWithAnnotations<?> node) {
         node.addSingleMemberAnnotation(
-                Generated.class.getName(),
-                new StringLiteralExpr(this.getClass().getSimpleName()));
+            Generated.class.getName(),
+            new StringLiteralExpr(this.getClass().getSimpleName()));
     }
 }

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JavaTransformer.java

@@ -3,24 +3,26 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java.transformations.pipeline;
 
+import java.util.Arrays;
+import java.util.List;
+import java.util.stream.Collectors;
+
 import com.github.javaparser.StaticJavaParser;
 import com.github.javaparser.ast.CompilationUnit;
+import com.github.javaparser.ast.Modifier;
 import com.github.javaparser.ast.NodeList;
 import com.github.javaparser.ast.body.*;
 import com.github.javaparser.ast.expr.*;
 import com.github.javaparser.ast.key.JmlDocModifier;
 import com.github.javaparser.ast.nodeTypes.NodeWithSimpleName;
-import com.github.javaparser.ast.stmt.BlockStmt;
 import com.github.javaparser.ast.stmt.ReturnStmt;
+import com.github.javaparser.ast.type.PrimitiveType;
 import com.github.javaparser.ast.type.Type;
 import org.jspecify.annotations.Nullable;
 
-import java.util.Arrays;
-import java.util.List;
-import java.util.stream.Collectors;
-
 import static com.github.javaparser.ast.Modifier.DefaultKeyword.*;
-import static de.uka.ilkd.key.java.transformations.AstFactory.*;
+import static de.uka.ilkd.key.java.transformations.AstFactory.assign;
+import static de.uka.ilkd.key.java.transformations.AstFactory.attributeThis;
 
 /// This transformation is made to transform any found [RecordDeclaration] into a corresponding
 /// [ClassOrInterfaceDeclaration].
@@ -52,11 +54,9 @@ private ClassOrInterfaceDeclaration transform(RecordDeclaration recordDeclaratio
         clazz.addExtendedType(java.lang.Record.class);
         addGenerated(clazz);
 
-        services.attachTypeSpec(clazz,
-                equalFieldsEqualRecords(recordDeclaration));
-
         for (Parameter parameter : recordDeclaration.getParameters()) {
-            FieldDeclaration field = clazz.addField(parameter.type(), parameter.getNameAsString(), PRIVATE, FINAL);
+            FieldDeclaration field =
+                clazz.addField(parameter.type(), parameter.getNameAsString(), PRIVATE, FINAL);
             field.getModifiers().addAll(parameter.getModifiers());
             addGenerated(field);
 
@@ -71,21 +71,50 @@ private ClassOrInterfaceDeclaration transform(RecordDeclaration recordDeclaratio
                         getter.getModifiers().add(mod.clone());
                     }
                 }
-                getter.getBody().get().addStatement(new ReturnStmt(parameter.getNameAsExpression()));
+                getter.getBody().get()
+                        .addStatement(new ReturnStmt(parameter.getNameAsExpression()));
                 addGenerated(getter);
             }
         }
 
         createConstructor(recordDeclaration, clazz);
 
-        createEquals(recordDeclaration, clazz);
-        createHashCode(recordDeclaration, clazz);
+        var generated =
+            createEquals(recordDeclaration, clazz) && createHashCode(recordDeclaration, clazz);
+
+        if (generated) {
+            services.attachTypeSpec(clazz,
+                equalFieldsEqualRecords(recordDeclaration));
+
+            services.attachTypeSpec(clazz,
+                "public static invariant_free (\\forall %s a; a.equals(a));"
+                        .formatted(recordDeclaration.getNameAsString()));
+
+            services.attachTypeSpec(clazz,
+                "public static invariant_free (\\forall %s a,b; a.equals(b); b.equals(a));"
+                        .formatted(recordDeclaration.getNameAsString()));
+
+            services.attachTypeSpec(clazz,
+                "public static invariant_free (\\forall %s a,b,c; a.equals(b) && b.equals(c); a.equals(c));"
+                        .formatted(recordDeclaration.getNameAsString()));
+
+            services.attachTypeSpec(clazz,
+                "public static invariant_free (\\forall %s a,b; a.equals(b); a.hashCode() == b.hashCode());"
+                        .formatted(recordDeclaration.getNameAsString()));
+
+            services.attachTypeSpec(clazz,
+                "public static invariant_free (\\forall %s a,b; a.hashCode() != b.hashCode(); !a.equals(b));"
+                        .formatted(recordDeclaration.getNameAsString()));
+        }
+
         createToString(recordDeclaration, clazz);
+
         clazz.getMembers().addAll(recordDeclaration.getMembers());
         return clazz;
     }
 
-    private void createConstructor(RecordDeclaration recordDeclaration, ClassOrInterfaceDeclaration clazz) {
+    private void createConstructor(RecordDeclaration recordDeclaration,
+            ClassOrInterfaceDeclaration clazz) {
         String[] paramTypes = recordDeclaration.getParameters().stream()
                 .map(it -> it.getType().asString())
                 .toArray(String[]::new);
@@ -102,8 +131,21 @@ private void createConstructor(RecordDeclaration recordDeclaration, ClassOrInter
             for (var parameter : recordDeclaration.getParameters()) {
                 final var p = parameter.clone();
                 fullConstructor.addParameter(p);
-                body.addStatement(assign(attributeThis(p.getNameAsString()), p.getNameAsExpression()));
+                body.addStatement(
+                    assign(attributeThis(p.getNameAsString()), p.getNameAsExpression()));
             }
+
+            var fieldParamEqual = recordDeclaration.getParameters()
+                    .stream()
+                    .map(NodeWithSimpleName::getNameAsString)
+                    .map(it -> "ensures this.%s == %s;".formatted(it, it))
+                    .collect(Collectors.joining("\n"));
+            services.attachSpec(fullConstructor, """
+                    public normal_behavior
+                    requires true;
+                    %s
+                    """.formatted(fieldParamEqual));
+
         }
 
         for (var compactConstructor : recordDeclaration.getCompactConstructors()) {
@@ -113,7 +155,8 @@ private void createConstructor(RecordDeclaration recordDeclaration, ClassOrInter
         clazz.addMember(fullConstructor);
     }
 
-    private void createToString(RecordDeclaration recordDeclaration, ClassOrInterfaceDeclaration clazz) {
+    private void createToString(RecordDeclaration recordDeclaration,
+            ClassOrInterfaceDeclaration clazz) {
         boolean hasNoToString = recordDeclaration.getMethodsBySignature("toString").isEmpty();
         if (hasNoToString) {
             MethodDeclaration toString = clazz.addMethod("toString", PUBLIC, FINAL, JML_NON_NULL);
@@ -136,7 +179,8 @@ private void createToString(RecordDeclaration recordDeclaration, ClassOrInterfac
         }
     }
 
-    private void createHashCode(RecordDeclaration recordDeclaration, ClassOrInterfaceDeclaration clazz) {
+    private boolean createHashCode(RecordDeclaration recordDeclaration,
+            ClassOrInterfaceDeclaration clazz) {
         boolean hasNoHashcode = recordDeclaration.getMethodsBySignature("hashCode").isEmpty();
         if (hasNoHashcode) {
             MethodDeclaration hashCode = clazz.addMethod("hashCode", PUBLIC, FINAL);
@@ -147,40 +191,91 @@ private void createHashCode(RecordDeclaration recordDeclaration, ClassOrInterfac
                     .map(it -> (Expression) it)
                     .toList();
             final Expression call = callObjects("hash", args);
-            hashCode.getBody().get().addStatement(new ReturnStmt(call));
+            // hashCode.getBody().get().addStatement(new ReturnStmt(call));
+            hashCode.setBody(null);
             addGenerated(hashCode);
+
+            services.attachSpec(hashCode, """
+                    public normal_behavior
+                    ensures true; requires true;
+                    assignable \\strictly_nothing;
+                    """);
         }
+        return hasNoHashcode;
     }
 
-    private void createEquals(RecordDeclaration recordDeclaration, ClassOrInterfaceDeclaration clazz) {
-        boolean hasNoEquals = recordDeclaration.getMethodsBySignature("equals", "java.lang.Object").isEmpty()
-                && recordDeclaration.getMethodsBySignature("equals", "Object").isEmpty();
+    private boolean createEquals(RecordDeclaration recordDeclaration,
+            ClassOrInterfaceDeclaration clazz) {
+        boolean hasNoEquals =
+            recordDeclaration.getMethodsBySignature("equals", "java.lang.Object").isEmpty()
+                    && recordDeclaration.getMethodsBySignature("equals", "Object").isEmpty();
         if (hasNoEquals) {
             MethodDeclaration equals = clazz.addMethod("equals", PUBLIC, FINAL);
             equals.addAnnotation(Override.class);
             equals.setType(Boolean.TYPE);
             Type tObject = StaticJavaParser.parseType("java.lang.Object");
-            equals.getParameters().add(new Parameter(tObject, "o"));
-            BlockStmt body = equals.getBody().get();
-            body.addStatement(
-                    mark(services.parseStatement("if(this == o) return true;")));
-            body.addStatement(
-                    mark(services.parseStatement("if(!(o instanceof %s)) return false;".formatted(clazz.getNameAsString()))));
-
-            body.addStatement(
-                    mark(services.parseStatement("final %s that = (%s) o;"
-                            .formatted(clazz.getNameAsString(), clazz.getNameAsString()))));
-
-            Expression equalFields = recordDeclaration.getParameters().stream()
-                    .map(it -> callObjects("equals", it.getNameAsExpression(),
-                            new FieldAccessExpr(new NameExpr("that"), it.getNameAsString())))
-                    .reduce((a, b) -> new BinaryExpr(a, b, BinaryExpr.Operator.AND))
-                    .orElse(new BooleanLiteralExpr(true));
-            body.addStatement(mark(new ReturnStmt(equalFields)));
-
-            body.addStatement(mark(new ReturnStmt(new BooleanLiteralExpr(true))));
+            var mods = new NodeList<>(new Modifier(JML_NULLABLE));
+            equals.getParameters().add(new Parameter(mods, tObject, new SimpleName("o")));
+            equals.setBody(null);
+
+
+            services.attachSpec(equals, """
+                    public normal_behavior
+                    requires true;
+                    ensures (
+                                   (this == o) //equality of identity
+                                || (o instanceof %s && o != null && %s)
+                                || (o instanceof %s && o != null && %s)
+                            ) <==> \\result;
+                    ensures hashCode() != o.hashCode() ==> !\\result;
+                    ensures o == null ==> !\\result;
+                    assignable \\strictly_nothing;
+                    """.formatted(
+                recordDeclaration.getNameAsString(),
+                recordDeclaration.getParameters().stream()
+                        .map(NodeWithSimpleName::getNameAsString)
+                        .map(it -> "this.%s==((%s)o).%s".formatted(it,
+                            recordDeclaration.getNameAsString(), it))
+                        .collect(Collectors.joining(" && ")),
+                recordDeclaration.getNameAsString(),
+                recordDeclaration.getParameters().stream()
+                        .map(it -> {
+                            String pname = it.getNameAsString();
+                            if (it.getType() instanceof PrimitiveType)
+                                return "(%s == ((%s)o).%s)".formatted(pname,
+                                    recordDeclaration.getNameAsString(), pname);
+                            else
+                                return "( this.%s != null ? (this.%s.equals(((%s)o).%s)) : (o.%s == null))"
+                                        .formatted(pname, pname,
+                                            recordDeclaration.getNameAsString(), pname, pname);
+                        })
+                        .collect(Collectors.joining(" && "))));
+
+            /*
+             * Nobody only contract:
+             * BlockStmt body = equals.getBody().get();
+             * body.addStatement(
+             * mark(services.parseStatement("if(this == o) return true;")));
+             * body.addStatement(
+             * mark(services.parseStatement("if(!(o instanceof %s)) return false;".formatted(clazz.
+             * getNameAsString()))));
+             *
+             * body.addStatement(
+             * mark(services.parseStatement("final %s that = (%s) o;"
+             * .formatted(clazz.getNameAsString(), clazz.getNameAsString()))));
+             *
+             * Expression equalFields = recordDeclaration.getParameters().stream()
+             * .map(it -> callObjects("equals", it.getNameAsExpression(),
+             * new FieldAccessExpr(new NameExpr("that"), it.getNameAsString())))
+             * .reduce((a, b) -> new BinaryExpr(a, b, BinaryExpr.Operator.AND))
+             * .orElse(new BooleanLiteralExpr(true));
+             * body.addStatement(mark(new ReturnStmt(equalFields)));
+             *
+             * body.addStatement(mark(new ReturnStmt(new BooleanLiteralExpr(true))));
+             */
             addGenerated(equals);
         }
+        return hasNoEquals;
     }
 
     private static @Nullable String equalFieldsEqualRecords(RecordDeclaration recordDeclaration) {
@@ -193,18 +288,18 @@ private void createEquals(RecordDeclaration recordDeclaration, ClassOrInterfaceD
                 .map(it -> "a.%s == b.%s".formatted(it, it))
                 .collect(Collectors.joining(" && "));
 
-        return "public axiom (\\forall %s a,b; %s; a.equals(b));".formatted(
-                recordDeclaration.getNameAsString(),
-                identityOfFields
-        );
+        return "public invariant_free (\\forall %s a,b; %s; a.equals(b));".formatted(
+            recordDeclaration.getNameAsString(),
+            identityOfFields);
     }
 
     private Expression callObjects(String method, Expression... exprs) {
         return callObjects(method, Arrays.stream(exprs).toList());
     }
 
     private Expression callObjects(String method, List<Expression> exprs) {
-        var objects = new FieldAccessExpr(new FieldAccessExpr(new NameExpr("java"), "lang"), "Objects");
+        var objects =
+            new FieldAccessExpr(new FieldAccessExpr(new NameExpr("java"), "lang"), "Objects");
         return new MethodCallExpr(objects, method, new NodeList<>(exprs));
     }
 

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/RecordClassBuilder.java

@@ -10,11 +10,10 @@
 import de.uka.ilkd.key.java.transformations.ConstantExpressionEvaluator;
 import de.uka.ilkd.key.java.transformations.EvaluationException;
 import de.uka.ilkd.key.speclang.PositionedString;
-
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
 import de.uka.ilkd.key.speclang.njml.PreParser;
-import org.jspecify.annotations.NonNull;
+
 import org.key_project.util.collection.ImmutableList;
 
 import com.github.javaparser.JavaParser;
@@ -32,6 +31,7 @@
 import com.github.javaparser.resolution.model.SymbolReference;
 import com.github.javaparser.resolution.types.ResolvedReferenceType;
 import com.github.javaparser.resolution.types.ResolvedType;
+import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.NullMarked;
 import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
@@ -260,6 +260,7 @@ public List<SymbolReference<? extends ResolvedValueDeclaration>> getUsages(
     /// i = j + 5;
     /// }
     /// ```
+    ///
     /// @param cd the TypeDeclaration of which the initializers have to be collected
     /// @return the list of copy assignments and method references realizing the initializers.`
     public NodeList<Statement> getInitializers(ClassOrInterfaceDeclaration cd) {
@@ -343,12 +344,22 @@ public Statement parseStatement(String code) {
     }
 
     public void attachTypeSpec(TypeDeclaration<?> clazz, @Nullable String spec) {
-        if(spec==null) return;
+        if (spec == null)
+            return;
         PreParser pp = getPreParser();
         ImmutableList<TextualJMLConstruct> specification = pp.parseClassLevel(spec);
         specification.forEach(it -> addClassSpec(clazz, it));
     }
 
+    public void attachSpec(Node node, @Nullable String spec) {
+        if (spec == null)
+            return;
+        PreParser pp = getPreParser();
+        ImmutableList<TextualJMLConstruct> specification = pp.parseClassLevel(spec);
+        specification.forEach(it -> addSpec(node, it));
+        LOGGER.info("Generated specification {} for {}", spec, node);
+    }
+
 
     /**
      * Cache of important data. This is done mainly for performance reasons.

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TransformationPipelineServices.java

@@ -271,7 +271,7 @@ private void readJava(EnvInput envInput, InitConfig initConfig) throws ProofInpu
             } catch (IOException e) {
                 throw new ProofInputException("Failed to read file", e);
             } catch (BuildingExceptions e) {
-                throw new ProofInputException("Failed to parse file: "+ javaPath, e);
+                throw new ProofInputException("Failed to parse file: " + javaPath, e);
             }
         }
         Path initialFile = envInput.getInitialFile();