final field code validator and tests

thanks to Richard for hinting at the needed infrastructure

key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java

@@ -6,6 +6,7 @@
 import de.uka.ilkd.key.java.expression.Assignment;
 import de.uka.ilkd.key.java.reference.*;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
+import de.uka.ilkd.key.logic.op.ProgramMethod;
 import de.uka.ilkd.key.logic.op.ProgramVariable;
 import org.key_project.logic.SyntaxElement;
 import org.key_project.util.collection.IdentityHashSet;
@@ -27,6 +28,9 @@
  * Potential for relaxaions:
  * - Final fields may be read after initialization (locally and in called methods)
  * This requires a lot more bookkeeping, though.
+ * - Effective finalness can be relaxed: If every constructor is subject to this treatment,
+ * corresponding expansion of the methods would reveal any illegal reads. ... if the super(...)
+ * calls are expanded for analysis.
  *
  * If this is a secondary constructor (referring to another constructor via this()), there are no restrictions.
  */
@@ -40,9 +44,9 @@ public FinalFieldCodeValidator(InitConfig initConfig) {
         this.initConfig = initConfig;
     }
 
-    public static void validateFinalFields(IProgramMethod constructor, InitConfig initConfig) {
+    public static void validateFinalFields(ProgramMethod constructor, InitConfig initConfig) {
         var validator = new FinalFieldCodeValidator(initConfig);
-        validator.enclosingClass = null; // constructor.getEnclosingClass(); // TODO!
+        validator.enclosingClass = constructor.getContainerType();
         if(isSecondaryConstructor(constructor)) {
             // secondary constructors are fine!
             return;
@@ -61,12 +65,7 @@ private static boolean isSecondaryConstructor(IProgramMethod constructor) {
         }
 
         var firstStatement = body.getStatementAt(0);
-        if (firstStatement instanceof MethodOrConstructorReference methodReference) {
-            // check that this is a reference of the form this(...)
-            return true;
-        }
-
-        return false;
+        return firstStatement instanceof ThisConstructorReference;
     }
 
     private void validate(IProgramMethod method) {
@@ -81,19 +80,18 @@ private void validate(IProgramMethod method) {
             throw new FinalViolationException("Method " + method.getFullName() + " has no body.");
         }
 
-        for(int i = 0; i < body.getStatementCount(); i++) {
-            var statement = body.getStatementAt(i);
-            validateProgramElement(statement);
-        }
+       validateProgramElement(body);
 
         var popped = methodStack.pop();
         assert popped == method;
         validatedMethods.add(method);
     }
 
     private void validateProgramElement(SyntaxElement element) {
-        if(element instanceof MethodOrConstructorReference methodReference) {
+        if(element instanceof MethodReference methodReference) {
             validateMethodReference(methodReference);
+        } else if (element instanceof ConstructorReference constructorReference) {
+            validateConstructorReference(constructorReference);
         } else if(element instanceof FieldReference fieldReference) {
             validateFieldReference(fieldReference);
         } else if(element instanceof Assignment assignment) {
@@ -107,7 +105,16 @@ private void validateProgramElement(SyntaxElement element) {
         }
     }
 
-    private void validateMethodReference(MethodOrConstructorReference methodReference) {
+    private void validateConstructorReference(ConstructorReference methodReference) {
+        // TODO We have to make sure that on non-static subclass is instantiated here
+        var hasThisArgument = methodReference.getArguments().stream().anyMatch(ThisReference.class::isInstance);
+
+        if(hasThisArgument) {
+            throw new FinalViolationException("Method call " + methodReference + " leaks 'this' to called method.", methodReference);
+        }
+    }
+
+    private void validateMethodReference(MethodReference methodReference) {
         ReferencePrefix referencePrefix = methodReference.getReferencePrefix();
         var calledOnThis = referencePrefix == null || referencePrefix instanceof ThisReference;
         var hasThisArgument = methodReference.getArguments().stream().anyMatch(ThisReference.class::isInstance);
@@ -131,12 +138,13 @@ private void validateMethodReference(MethodOrConstructorReference methodReferenc
         }
     }
 
-    private IProgramMethod findMethod(MethodOrConstructorReference methodReference) {
+    private IProgramMethod findMethod(MethodReference methodReference) {
         // return the program method for the method reference
         // YOu can use enclosingClass to get the class in which the method is defined
         // The method is guaranteed to be defined in the enclosing class not in a superclass.
         // One can also peek the method stack if needed ...
-        throw new UnsupportedOperationException("Not implemented yet.");
+        ExecutionContext ec = new ExecutionContext(new TypeRef(enclosingClass), methodStack.peek(), methodReference.getReferencePrefix());
+        return         methodReference.method(initConfig.getServices(), methodReference.determineStaticPrefixType(initConfig.getServices(), ec), ec);
     }
 
     private void validateAssignment(Assignment assignment) {

key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldsPOExtension.java

@@ -13,6 +13,7 @@
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
 import de.uka.ilkd.key.logic.op.LogicVariable;
+import de.uka.ilkd.key.logic.op.ProgramMethod;
 import de.uka.ilkd.key.logic.op.ProgramVariable;
 
 import org.key_project.logic.Name;
@@ -40,13 +41,14 @@ public Term modifyPostTerm(AbstractOperationPO abstractPO, InitConfig proofConfi
 
         // We know this holds because of isPOSupported:
         FunctionalOperationContractPO fpo = (FunctionalOperationContractPO) abstractPO;
-        IProgramMethod constructor = fpo.getProgramMethod();
-        assert constructor.isConstructor();
+        IProgramMethod iconstructor = fpo.getProgramMethod();
+        assert iconstructor instanceof ProgramMethod : "Contracts cannot have schema ";
+        ProgramMethod constructor = (ProgramMethod) iconstructor;
 
         FinalFieldCodeValidator.validateFinalFields(constructor, proofConfig);
 
         TermBuilder tb = services.getTermBuilder();
-        LogicVariable fv = new LogicVariable(new Name("o"),
+        LogicVariable fv = new LogicVariable(new Name("fld"),
             services.getTypeConverter().getHeapLDT().getFieldSort());
         Term self = tb.var(selfVar);
         Term sel = tb.dot(JavaDLTheory.ANY, self, tb.var(fv));

key.core/src/test/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidatorTest.java

@@ -0,0 +1,74 @@
+package de.uka.ilkd.key.proof.init;
+
+import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
+import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.logic.op.ProgramMethod;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
+import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
+import de.uka.ilkd.key.speclang.Contract;
+import de.uka.ilkd.key.util.KeYTypeUtil;
+import org.junit.jupiter.api.Assertions;
+import org.junit.jupiter.api.DynamicTest;
+import org.junit.jupiter.api.TestFactory;
+
+import java.io.File;
+import java.net.URL;
+import java.util.HashSet;
+import java.util.Set;
+import java.util.stream.Stream;
+
+class FinalFieldCodeValidatorTest {
+
+    @TestFactory
+    public Stream<DynamicTest> testCodeValidatorParse() throws ProblemLoaderException {
+       return testContracts(false, "final/shouldparse");
+    }
+
+    //@TestFactory
+    public Stream<DynamicTest> testCodeValidatorFail() throws ProblemLoaderException {
+        return testContracts(true, "final/shouldfail");
+    }
+
+    private Stream<DynamicTest> testContracts(boolean shouldfail, String directory) throws ProblemLoaderException {
+        URL url = getClass().getResource(directory);
+        assert url != null : directory + " not found.";
+        assert "file".equals(url.getProtocol()): "Test cases must be in file system";
+        File dir = new File(url.getPath());
+        KeYEnvironment<DefaultUserInterfaceControl> env = KeYEnvironment.load(dir, null, null, null);
+
+        Set<KeYJavaType> kjts = env.getJavaInfo().getAllKeYJavaTypes();
+        Set<Contract> contracts = new HashSet<>();
+        for (KeYJavaType type : kjts) {
+            if (!KeYTypeUtil.isLibraryClass(type)) {
+                SpecificationRepository specRepo = env.getSpecificationRepository();
+                for(Contract c: specRepo.getAllContracts()) {
+                    var target = c.getTarget();
+                    if (target instanceof ProgramMethod pm &&
+                            pm.isConstructor() &&
+                            !KeYTypeUtil.isLibraryClass(pm.getContainerType())) {
+                        contracts.add(c);
+                    }
+                }
+            }
+        }
+        if(shouldfail)
+        return contracts.stream().map(c -> DynamicTest.dynamicTest("Illegal constructor " + c.getName(),
+                () -> Assertions.assertThrowsExactly(FinalFieldCodeValidator.FinalViolationException.class,
+                        () -> testConstructor(c, env))));
+        else return contracts.stream().map(c -> DynamicTest.dynamicTest("Legal constructor " + c.getName(),
+                ()->testConstructor(c, env)));
+    }
+
+    private void testConstructor(Contract c, KeYEnvironment<?> env) throws ProofInputException {
+        try {
+            // System.out.println("Contract id: " + c.getName());
+            ContractPO po = c.createProofObl(env.getInitConfig());
+            env.createProof(po);
+        } catch(FinalFieldCodeValidator.FinalViolationException fex) {
+            System.err.println("Position: " + fex.getPosition());
+            fex.printStackTrace();
+            throw fex;
+        }
+    }
+}

key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalProblem1.java

@@ -0,0 +1,17 @@
+class FinalReadBeforeWriteIndirect {
+    final int finalField;
+
+    //@ ensures b;
+    FinalReadBeforeWriteIndirect(boolean b) {
+        int before = getFinalField();
+        finalField = 42;
+        int after = getFinalField();
+    }
+
+    /*@ normal_behaviour
+      @  ensures \result == finalField;
+      @*/
+    private int getFinalField() {
+        return finalField;
+    }
+}

key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalReadBeforeWriteIndirect.java

@@ -0,0 +1,17 @@
+class FinalReadBeforeWriteIndirect {
+    final int finalField;
+
+    //@ ensures b;
+    FinalReadBeforeWriteIndirect(boolean b) {
+        int before = getFinalField();
+        finalField = 42;
+        int after = getFinalField();
+    }
+
+    /*@ normal_behaviour
+      @  ensures \result == finalField;
+      @*/
+    private int getFinalField() {
+        return finalField;
+    }
+}

key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/LeakThis1.java

@@ -0,0 +1,17 @@
+class LeakThis1 {
+    final int finalField;
+
+    //@ ensures b;
+    LeakThis1(boolean b) {
+        int before = getFinalField(this);
+        finalField = 42;
+        int after = getFinalField(this);
+    }
+
+    /*@ normal_behaviour
+      @  ensures \result == x.finalField;
+      @*/
+    private int getFinalField(LeakThis1 x) {
+        return x.finalField;
+    }
+}

key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/LeakThis2.java

@@ -0,0 +1,23 @@
+class LeakThis2 {
+    final int finalField;
+    LeakThis2 other;
+
+    //@ ensures b;
+    LeakThis2(boolean b) {
+        leakThis();
+        int before = getFinalField();
+        finalField = 42;
+        int after = getFinalField();
+    }
+
+    private LeakThis2 leakThis() {
+        other = true ? this : this;
+    }
+
+    /*@ normal_behaviour
+      @  ensures \result == finalField;
+      @*/
+    int getFinalField() {
+        return other.finalField;
+    }
+}

key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/Subclass.java

@@ -0,0 +1,23 @@
+class Subclass {
+    final int finalField;
+
+    //@ ensures b;
+    Subclass(boolean b) {
+        int before = getFinalField();
+        finalField = 42;
+        int after = getFinalField();
+    }
+
+    int getFinalField() {
+        return 0;
+    }
+}
+
+class Subsubclass extends Subclass {
+    /*@ normal_behaviour
+      @  ensures \result == finalField;
+      @*/
+    int getFinalField() {
+        return finalField;
+    }
+}

key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldparse/SecondaryConstructor.java

@@ -0,0 +1,15 @@
+class SecondaryConstructor {
+    final int finalField;
+
+    boolean b;
+
+    //@ ensures b;
+    SecondaryConstructor(int v) {
+        finalField = v;
+    }
+
+    SecondaryCosntructor() {
+        this(42);
+        int x = finalField;
+    }
+}

key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java

@@ -134,7 +134,7 @@ public void progressStopped(Object sender) {
 
     @Override
     public void reportException(Object sender, ProofOblInput input, Exception e) {
-        reportStatus(sender, input.name() + " failed");
+        IssueDialog.showExceptionDialog(mainWindow, e);
     }
 
     @Override