From e46b239e3155e6bd70dbdcb2b5492d514670b526 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 10 Dec 2024 08:40:21 +0100 Subject: [PATCH] final field code validator and tests thanks to Richard for hinting at the needed infrastructure --- .../proof/init/FinalFieldCodeValidator.java | 40 ++++++---- .../proof/init/FinalFieldsPOExtension.java | 8 +- .../init/FinalFieldCodeValidatorTest.java | 74 +++++++++++++++++++ .../init/final/shouldfail/FinalProblem1.java | 17 +++++ .../FinalReadBeforeWriteIndirect.java | 17 +++++ .../init/final/shouldfail/LeakThis1.java | 17 +++++ .../init/final/shouldfail/LeakThis2.java | 23 ++++++ .../proof/init/final/shouldfail/Subclass.java | 23 ++++++ .../shouldparse/SecondaryConstructor.java | 15 ++++ .../key/gui/WindowUserInterfaceControl.java | 2 +- 10 files changed, 216 insertions(+), 20 deletions(-) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidatorTest.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalProblem1.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalReadBeforeWriteIndirect.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/LeakThis1.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/LeakThis2.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/Subclass.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldparse/SecondaryConstructor.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java index 7a8d15a3760..2961573c233 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java +++ b/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,10 +80,7 @@ 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; @@ -92,8 +88,10 @@ private void validate(IProgramMethod 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) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldsPOExtension.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldsPOExtension.java index 1a2872fceee..4054aed70f5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldsPOExtension.java +++ b/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)); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidatorTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidatorTest.java new file mode 100644 index 00000000000..83dcf87b94a --- /dev/null +++ b/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 testCodeValidatorParse() throws ProblemLoaderException { + return testContracts(false, "final/shouldparse"); + } + + //@TestFactory + public Stream testCodeValidatorFail() throws ProblemLoaderException { + return testContracts(true, "final/shouldfail"); + } + + private Stream 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 env = KeYEnvironment.load(dir, null, null, null); + + Set kjts = env.getJavaInfo().getAllKeYJavaTypes(); + Set 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; + } + } +} \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalProblem1.java b/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalProblem1.java new file mode 100644 index 00000000000..8829d75a723 --- /dev/null +++ b/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; + } +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalReadBeforeWriteIndirect.java b/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/FinalReadBeforeWriteIndirect.java new file mode 100644 index 00000000000..8829d75a723 --- /dev/null +++ b/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; + } +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/LeakThis1.java b/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/LeakThis1.java new file mode 100644 index 00000000000..6cef6781e2c --- /dev/null +++ b/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; + } +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/LeakThis2.java b/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/LeakThis2.java new file mode 100644 index 00000000000..74f263194ca --- /dev/null +++ b/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; + } +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/Subclass.java b/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldfail/Subclass.java new file mode 100644 index 00000000000..d26818cee4d --- /dev/null +++ b/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; + } +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldparse/SecondaryConstructor.java b/key.core/src/test/resources/de/uka/ilkd/key/proof/init/final/shouldparse/SecondaryConstructor.java new file mode 100644 index 00000000000..80239df2f8c --- /dev/null +++ b/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; + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index fa0578538d8..4680d6139b9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/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