diff --git a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/ProofObligationVars.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/ProofObligationVars.java index 58e1766f0c7..247543753b0 100644 --- a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/ProofObligationVars.java +++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/ProofObligationVars.java @@ -7,6 +7,8 @@ import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.reference.TypeRef; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.TermBuilder; @@ -46,16 +48,15 @@ public class ProofObligationVars { private final TermBuilder tb; - public ProofObligationVars(IProgramMethod pm, KeYJavaType kjt, Services services) { - this.pre = StateVars.buildMethodContractPreVars(pm, kjt, services); - this.post = StateVars.buildMethodContractPostVars(this.pre, pm, kjt, services); + public ProofObligationVars(IProgramMethod pm, TypeReference typeRef, Services services) { + this.pre = StateVars.buildMethodContractPreVars(pm, typeRef, services); + this.post = StateVars.buildMethodContractPostVars(this.pre, pm, typeRef, services); this.tb = services.getTermBuilder(); this.exceptionParameter = buildExceptionParameter(services); this.formalParams = buildFormalParamVars(services); this.postfix = ""; } - public ProofObligationVars(ProofObligationVars orig, String postfix, Services services) { this.pre = StateVars.buildInfFlowPreVars(orig.pre, postfix, services); this.post = StateVars.buildInfFlowPostVars(orig.pre, orig.post, pre, postfix, services); @@ -65,7 +66,6 @@ public ProofObligationVars(ProofObligationVars orig, String postfix, Services se this.postfix = postfix; } - public ProofObligationVars(StateVars pre, StateVars post, JTerm exceptionParameter, ImmutableList formalParams, Services services) { this.pre = pre; @@ -113,7 +113,6 @@ public ProofObligationVars labelHeapAtPreAsAnonHeapFunc() { } } - /** * Build variable for try statement. * @@ -124,7 +123,7 @@ private JTerm buildExceptionParameter(Services services) { JavaInfo javaInfo = services.getJavaInfo(); final KeYJavaType eType = javaInfo.getTypeByClassName("java.lang.Exception"); final ProgramElementName ePEN = new ProgramElementName("e"); - return tb.var(new LocationVariable(ePEN, eType)); + return tb.var(new LocationVariable(ePEN, new TypeRef(eType))); } /** @@ -138,7 +137,8 @@ private ImmutableList buildFormalParamVars(Services services) for (JTerm param : pre.localVars) { ProgramVariable paramVar = param.op(ProgramVariable.class); ProgramElementName pen = new ProgramElementName("_" + paramVar.name()); - LocationVariable formalParamVar = new LocationVariable(pen, paramVar.getKeYJavaType()); + LocationVariable formalParamVar = + new LocationVariable(pen, paramVar.getTypeReference()); register(formalParamVar, services); JTerm formalParam = tb.var(formalParamVar); formalParamVars = formalParamVars.append(formalParam); diff --git a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java index fb2dd1b66f5..19adc1096aa 100644 --- a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java +++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java @@ -12,6 +12,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.StatementBlock; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.IProgramMethod; import de.uka.ilkd.key.logic.op.JModality; @@ -50,7 +51,8 @@ public InfFlowContractPO(InitConfig initConfig, InformationFlowContract contract // generate proof obligation variables final IProgramMethod pm = contract.getTarget(); - symbExecVars = new ProofObligationVars(pm, contract.getKJT(), environmentServices); + symbExecVars = + new ProofObligationVars(pm, new TypeRef(contract.getKJT()), environmentServices); assert (symbExecVars.pre.self == null) == (pm.isStatic()); ifVars = new IFProofObligationVars(symbExecVars, environmentServices); diff --git a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/proof/init/StateVars.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/proof/init/StateVars.java index c3a3f454046..ed11f00d8d2 100644 --- a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/proof/init/StateVars.java +++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/proof/init/StateVars.java @@ -6,7 +6,7 @@ import java.util.Iterator; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.JTerm; @@ -85,13 +85,11 @@ public StateVars(JTerm self, JTerm guard, ImmutableList localVars, JTerm paddedTermList = allTerms; } - public StateVars(JTerm self, ImmutableList localVars, JTerm result, JTerm exception, JTerm heap, JTerm mbyAtPre) { this(self, null, localVars, result, exception, heap, mbyAtPre); } - private ImmutableList appendIfNotNull(ImmutableList list, JTerm t) { if (t != null) { return list.append(t); @@ -100,7 +98,6 @@ private ImmutableList appendIfNotNull(ImmutableList list, JTerm t) } } - private ImmutableList appendIfNotNull(ImmutableList list, ImmutableList list2) { ImmutableList result = list; @@ -110,30 +107,25 @@ private ImmutableList appendIfNotNull(ImmutableList list, return result; } - public StateVars(JTerm self, JTerm guard, ImmutableList localVars, JTerm heap) { this(self, guard, localVars, null, null, heap, null); } - public StateVars(JTerm self, JTerm guard, ImmutableList localVars, JTerm result, JTerm exception, JTerm heap) { this(self, guard, localVars, result, exception, heap, null); } - public StateVars(@Nullable JTerm self, ImmutableList localVars, @Nullable JTerm result, @Nullable JTerm exception, JTerm heap) { this(self, localVars, result, exception, heap, null); } - public StateVars(JTerm self, ImmutableList localVars, JTerm heap) { this(self, localVars, null, null, heap); } - public StateVars(StateVars orig, String postfix, Services services) { this(copyVariable(orig.self, postfix, services), copyVariable(orig.guard, postfix, services), @@ -144,7 +136,6 @@ public StateVars(StateVars orig, String postfix, Services services) { copyFunction(orig.mbyAtPre, postfix, services)); } - private static ImmutableList copyVariables(ImmutableList ts, String postfix, Services services) { ImmutableList result = ImmutableList.nil(); @@ -154,7 +145,6 @@ private static ImmutableList copyVariables(ImmutableList ts, Strin return result; } - private static JTerm copyVariable(JTerm t, String postfix, Services services) { if (t != null) { final TermBuilder tb = services.getTermBuilder(); @@ -167,7 +157,6 @@ private static JTerm copyVariable(JTerm t, String postfix, Services services) { } } - private static JTerm newVariable(JTerm t, String name, Services services) { if (t == null) { return null; @@ -184,7 +173,6 @@ private static JTerm newVariable(JTerm t, String name, Services services) { return tb.var(newVar); } - private static JTerm copyHeapSymbol(JTerm t, String postfix, Services services) { if (t != null) { final TermBuilder tb = services.getTermBuilder(); @@ -197,7 +185,6 @@ private static JTerm copyHeapSymbol(JTerm t, String postfix, Services services) } } - private static JTerm newHeapSymbol(JTerm t, String name, Services services) { if (t == null) { return null; @@ -215,7 +202,6 @@ private static JTerm newHeapSymbol(JTerm t, String name, Services services) { } } - private static JTerm newFunction(JTerm t, String name, Services services) { if (t == null) { return null; @@ -226,7 +212,6 @@ private static JTerm newFunction(JTerm t, String name, Services services) { return tb.func(newFunc); } - private static JTerm copyFunction(JTerm t, String postfix, Services services) { if (t != null) { final TermBuilder tb = services.getTermBuilder(); @@ -239,33 +224,30 @@ private static JTerm copyFunction(JTerm t, String postfix, Services services) { } } - - public static StateVars buildMethodContractPreVars(IProgramMethod pm, KeYJavaType kjt, + public static StateVars buildMethodContractPreVars(IProgramMethod pm, TypeReference typeRef, Services services) { ImmutableArray heapLabels = new ImmutableArray<>(ParameterlessTermLabel.ANON_HEAP_LABEL); - return new StateVars(buildSelfVar(services, pm, kjt, ""), buildParamVars(services, "", pm), + return new StateVars(buildSelfVar(services, pm, typeRef, ""), + buildParamVars(services, "", pm), buildResultVar(pm, services, ""), buildExceptionVar(services, "", pm), buildHeapFunc("AtPre", heapLabels, services), buildMbyVar("", services)); } - public static StateVars buildMethodContractPostVars(StateVars preVars, IProgramMethod pm, - KeYJavaType kjt, Services services) { + TypeReference typeRef, Services services) { final String postfix = "AtPost"; // preVars.localVars: no local out variables - return new StateVars(buildSelfVar(services, pm, kjt, postfix), preVars.localVars, + return new StateVars(buildSelfVar(services, pm, typeRef, postfix), preVars.localVars, buildResultVar(pm, services, postfix), buildExceptionVar(services, postfix, pm), buildHeapFunc(postfix, new ImmutableArray<>(), services), preVars.mbyAtPre); } - public static StateVars buildInfFlowPreVars(StateVars origPreVars, String postfix, Services services) { return new StateVars(origPreVars, postfix, services); } - public static StateVars buildInfFlowPostVars(StateVars origPreVars, StateVars origPostVars, StateVars preVars, String postfix, Services services) { // create new post vars if original pre and original post var differ; @@ -296,19 +278,17 @@ public static StateVars buildInfFlowPostVars(StateVars origPreVars, StateVars or return new StateVars(self, guard, localPostVars, result, exception, heap, mbyAtPre); } - - private static JTerm buildSelfVar(Services services, IProgramMethod pm, KeYJavaType kjt, + private static JTerm buildSelfVar(Services services, IProgramMethod pm, TypeReference typeRef, String postfix) { if (pm.isStatic()) { return null; } final TermBuilder tb = services.getTermBuilder(); - JTerm selfVar = tb.var(tb.selfVar(pm, kjt, true, postfix)); + JTerm selfVar = tb.var(tb.selfVar(pm, typeRef, true, postfix)); register(selfVar.op(ProgramVariable.class), services); return selfVar; } - private static ImmutableList buildParamVars(Services services, String postfix, IProgramMethod pm) { final TermBuilder tb = services.getTermBuilder(); @@ -317,7 +297,6 @@ private static ImmutableList buildParamVars(Services services, String pos return paramVars; } - private static JTerm buildResultVar(IProgramMethod pm, Services services, String postfix) { if (pm.isVoid() || pm.isConstructor()) { return null; @@ -328,7 +307,6 @@ private static JTerm buildResultVar(IProgramMethod pm, Services services, String return resultVar; } - private static JTerm buildHeapFunc(String postfix, ImmutableArray labels, Services services) { HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); @@ -344,7 +322,6 @@ private static JTerm buildHeapFunc(String postfix, ImmutableArray lab } } - private static JTerm buildExceptionVar(Services services, String postfix, IProgramMethod pm) { final TermBuilder tb = services.getTermBuilder(); JTerm excVar = tb.var(tb.excVar("exc" + postfix, pm, true)); @@ -352,7 +329,6 @@ private static JTerm buildExceptionVar(Services services, String postfix, IProgr return excVar; } - private static JTerm buildMbyVar(String postfix, Services services) { final TermBuilder tb = services.getTermBuilder(); final Sort intSort = services.getTypeConverter().getIntegerLDT().targetSort(); @@ -362,7 +338,6 @@ private static JTerm buildMbyVar(String postfix, Services services) { return tb.func(mbyAtPreFunc); } - static void register(ProgramVariable pv, Services services) { Namespace progVarNames = services.getNamespaces().programVariables(); if (pv != null && progVarNames.lookup(pv.name()) == null) { @@ -370,14 +345,12 @@ static void register(ProgramVariable pv, Services services) { } } - static void register(ImmutableList pvs, Services services) { for (ProgramVariable pv : pvs) { register(pv, services); } } - static void register(Function f, Services services) { Namespace functionNames = services.getNamespaces().functions(); if (f != null && functionNames.lookup(f.name()) == null) { @@ -386,7 +359,6 @@ static void register(Function f, Services services) { } } - static ImmutableList ops(ImmutableList terms, Class opClass) throws IllegalArgumentException { ImmutableList ops = ImmutableList.nil(); @@ -396,7 +368,6 @@ static ImmutableList ops(ImmutableList terms, Class opClass) return ops; } - @Override public String toString() { return termList.toString(); diff --git a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java index dce83519c86..9769f2db1a3 100644 --- a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java +++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java @@ -19,8 +19,8 @@ import de.uka.ilkd.key.informationflow.proof.init.StateVars; import de.uka.ilkd.key.informationflow.rule.tacletbuilder.InfFlowBlockContractTacletBuilder; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.java.ast.statement.JavaStatement; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.ProgramElementName; @@ -161,7 +161,7 @@ protected void setUpValidityGoal(final ImmutableList result, var app = (InfFlowBlockContractInternalBuiltInRuleApp) application; final ProgramVariable exceptionParameter = - createLocalVariable("e", variables.exception.getKeYJavaType(), services); + createLocalVariable("e", variables.exception.getTypeReference(), services); validityGoal.setBranchLabel("Information Flow Validity"); // clear goal @@ -372,7 +372,7 @@ protected static ImmutableSet filterAppliedContracts( assert varTerm.op() instanceof LocationVariable; final TermBuilder tb = services.getTermBuilder(); - KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType(); + TypeReference resultType = ((LocationVariable) varTerm.op()).getTypeReference(); if (!suffix.equalsIgnoreCase("")) { suffix = "_" + suffix; } @@ -395,7 +395,7 @@ protected static ImmutableList buildLocalOutsAtPre(ImmutableList v for (JTerm varTerm : varTerms) { assert varTerm.op() instanceof LocationVariable; - KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType(); + TypeReference resultType = ((LocationVariable) varTerm.op()).getTypeReference(); String name = tb.newName(varTerm + "_Before"); LocationVariable varAtPostVar = @@ -417,7 +417,7 @@ protected static ImmutableList buildLocalOutsAtPost(ImmutableList for (JTerm varTerm : varTerms) { assert varTerm.op() instanceof LocationVariable; - KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType(); + TypeReference resultType = ((LocationVariable) varTerm.op()).getTypeReference(); String name = tb.newName(varTerm + "_After"); LocationVariable varAtPostVar = diff --git a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantRule.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantRule.java index 6eecc350626..e1b623dbb19 100644 --- a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantRule.java +++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantRule.java @@ -15,7 +15,7 @@ import de.uka.ilkd.key.informationflow.proof.init.StateVars; import de.uka.ilkd.key.informationflow.rule.tacletbuilder.InfFlowLoopInvariantTacletBuilder; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.label.ParameterlessTermLabel; @@ -250,7 +250,7 @@ private static JTerm buildAtPostVar(JTerm varTerm, String suffix, Services servi assert varTerm.op() instanceof LocationVariable; final TermBuilder tb = services.getTermBuilder(); - final KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType(); + final TypeReference resultType = ((LocationVariable) varTerm.op()).getTypeReference(); if (!suffix.equalsIgnoreCase("")) { suffix = "_" + suffix; } @@ -268,7 +268,7 @@ private static JTerm buildBeforeVar(JTerm varTerm, Services services) { assert varTerm.op() instanceof LocationVariable; final TermBuilder tb = services.getTermBuilder(); - final KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType(); + final TypeReference resultType = ((LocationVariable) varTerm.op()).getTypeReference(); final String name = tb.newName(varTerm + "_Before"); final LocationVariable varAtPreVar = new LocationVariable(new ProgramElementName(name), resultType); @@ -283,7 +283,7 @@ private static JTerm buildAfterVar(JTerm varTerm, Services services) { assert varTerm.op() instanceof LocationVariable; final TermBuilder tb = services.getTermBuilder(); - final KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType(); + final TypeReference resultType = ((LocationVariable) varTerm.op()).getTypeReference(); final String name = tb.newName(varTerm + "_After"); final LocationVariable varAtPostVar = new LocationVariable(new ProgramElementName(name), resultType); @@ -301,7 +301,7 @@ private static ImmutableList buildLocalOutsAtPre(ImmutableList var for (final JTerm varTerm : varTerms) { assert varTerm.op() instanceof LocationVariable; - final KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType(); + final TypeReference resultType = ((LocationVariable) varTerm.op()).getTypeReference(); final String name = tb.newName(varTerm + "_Before"); final LocationVariable varAtPostVar = @@ -323,7 +323,7 @@ private static ImmutableList buildLocalOutsAtPost(ImmutableList va for (final JTerm varTerm : varTerms) { assert varTerm.op() instanceof LocationVariable; - final KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType(); + final TypeReference resultType = ((LocationVariable) varTerm.op()).getTypeReference(); final String name = tb.newName(varTerm + "_After"); final LocationVariable varAtPostVar = diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WellDefinednessPO.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WellDefinednessPO.java index 2170e060659..a60ca1a8614 100644 --- a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WellDefinednessPO.java +++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WellDefinednessPO.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.label.ParameterlessTermLabel; @@ -83,9 +84,9 @@ private static Function createAnonHeap(LocationVariable heap, Services services) private static LocationVariable createSelf(IProgramMethod pm, KeYJavaType selfKJT, TermServices services) { if (pm == null) { - return services.getTermBuilder().selfVar(selfKJT, false); + return services.getTermBuilder().selfVar(new TypeRef(selfKJT), false); } else { - return services.getTermBuilder().selfVar(pm, selfKJT, true); + return services.getTermBuilder().selfVar(pm, new TypeRef(selfKJT), true); } } diff --git a/key.core/src/main/antlr4/JavaKeYLexer.g4 b/key.core/src/main/antlr4/JavaKeYLexer.g4 index 9ea0ac834ee..0db9a8b65cf 100644 --- a/key.core/src/main/antlr4/JavaKeYLexer.g4 +++ b/key.core/src/main/antlr4/JavaKeYLexer.g4 @@ -55,6 +55,9 @@ NEW_DEPENDING_ON: '\\newDependingOn'; NEW_LOCAL_VARS: '\\newLocalVars'; NEWLABEL : '\\newLabel'; CONTAINS_ASSIGNMENT : '\\containsAssignment'; +HAS_ANNOTATION : '\\hasAnnotation'; +ADD_ANNOTATION : '\\addAnnotation'; +REMOVE_ANNOTATION : '\\removeAnnotation'; // label occurs again for character `!' NOTFREEIN : '\\notFreeIn'; STATIC : '\\static'; diff --git a/key.core/src/main/antlr4/JavaKeYParser.g4 b/key.core/src/main/antlr4/JavaKeYParser.g4 index f7942db1562..2fdd0536b76 100644 --- a/key.core/src/main/antlr4/JavaKeYParser.g4 +++ b/key.core/src/main/antlr4/JavaKeYParser.g4 @@ -259,6 +259,9 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier. | GET_VARIANT | IS_LABELED | ISINSTRICTFP + | HAS_ANNOTATION + | ADD_ANNOTATION + | REMOVE_ANNOTATION ; varexp_argument diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJPMapping.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJPMapping.java index 9afb9eaf61c..faa3de8d3d0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJPMapping.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJPMapping.java @@ -261,24 +261,24 @@ public ResolvedTypeWrapper(ResolvedType resolvedType) { @Override public boolean equals(Object o) { if (o instanceof ResolvedTypeWrapper other) { - final boolean eq = resolvedType.equals(other.resolvedType); - if (eq && resolvedType.isReferenceType()) { + if (resolvedType.isReferenceType()) { if (!other.resolvedType.isReferenceType()) { return false; // should not be reachable as then eq is false, but ... } return resolvedType.asReferenceType().getQualifiedName() .equals(other.resolvedType.asReferenceType().getQualifiedName()); } - return eq; + + return resolvedType.equals(other.resolvedType); } return false; } @Override public int hashCode() { - return resolvedType.hashCode() + (resolvedType.isReferenceType() + return resolvedType.isReferenceType() ? resolvedType.asReferenceType().getQualifiedName().hashCode() - : 0); + : resolvedType.hashCode(); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java index 0523878dbb1..148d4d24928 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java @@ -6,6 +6,7 @@ import java.util.List; import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.Annotation; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.abstraction.Type; import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration; @@ -73,6 +74,7 @@ import org.key_project.logic.Name; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.ImmutableList; import org.jspecify.annotations.Nullable; @@ -103,7 +105,6 @@ public static CopyAssignment assign(Expression lhs, Expression rhs, PositionInfo * @return a new {@link CopyAssignment} as defined by parameters */ public static CopyAssignment assign(final ExtList parameters) { - return new CopyAssignment(parameters); } @@ -114,14 +115,6 @@ public static Expression attribute(ReferencePrefix prefix, ProgramVariable field return new FieldReference(field, prefix); } - /** - * creates a local variable declaration typeRef name; - */ - public static LocalVariableDeclaration declare(ProgramElementName name, TypeReference typeRef) { - return new LocalVariableDeclaration(typeRef, - new VariableSpecification(new LocationVariable(name, typeRef.getKeYJavaType()))); - } - /** * Create a local variable declaration without initialization. * @@ -131,15 +124,14 @@ public static LocalVariableDeclaration declare(ProgramElementName name, TypeRefe * * @param name * the {@link ProgramElementName} of the variable to be declared - * @param type - * the static {@link KeYJavaType} of the variable to be declared + * @param typeRef + * the static {@link TypeReference} of the variable to be declared * @return a new {@link LocalVariableDeclaration} of a variable with static type * type and name name */ public static LocalVariableDeclaration declare(final ProgramElementName name, - final KeYJavaType type) { - - return declare(name, null, type); + final TypeReference typeRef) { + return declare(name, null, typeRef); } /** @@ -149,9 +141,10 @@ public static LocalVariableDeclaration declare(final ProgramElementName name, */ public static LocalVariableDeclaration declare(ProgramElementName name, @Nullable Expression init, - KeYJavaType type) { - return new LocalVariableDeclaration(new TypeRef(type), - new VariableSpecification(new LocationVariable(name, type), init, type)); + TypeReference typeRef) { + return new LocalVariableDeclaration(typeRef, + new VariableSpecification(new LocationVariable(name, typeRef), init, + typeRef.getKeYJavaType())); } /** @@ -165,14 +158,14 @@ public static LocalVariableDeclaration declare(ProgramElementName name, * the named and typed {@link IProgramVariable} to be declared * @param init * the {@link Expression} var is initialized with - * @param type - * the static {@link KeYJavaType} of var + * @param typeRef + * the static {@link TypeReference} of var * @return a {@link LocalVariableDeclaration} of var with static type * type and initial value init */ public static LocalVariableDeclaration declare(IProgramVariable var, Expression init, - KeYJavaType type) { - return declare(new Modifier[0], var, init, type); + TypeReference typeRef) { + return declare(new Modifier[0], var, init, typeRef); } /** @@ -189,17 +182,17 @@ public static LocalVariableDeclaration declare(IProgramVariable var, Expression * the {@link String} on which the variable's unique name is based * @param initializer * the {@link Expression} the declared variable is initialized with - * @param type - * the static {@link KeYJavaType} of the to be declared variable + * @param typeRef + * the static {@link TypeReference} of the to be declared variable * @return a {@link LocalVariableDeclaration} of variable named uniquely after name * with static type type and initial value initializer */ public static LocalVariableDeclaration declare(final Services services, final String name, - final Expression initializer, final KeYJavaType type) { + final Expression initializer, final TypeReference typeRef) { final ProgramElementName uniqueName = services.getVariableNamer().getTemporaryNameProposal(name); - return declare(uniqueName, initializer, type); + return declare(uniqueName, initializer, typeRef); } /** @@ -211,31 +204,31 @@ public static LocalVariableDeclaration declare(final Services services, final St * * @param var * the named and typed {@link IProgramVariable} to be declared - * @param type - * the static {@link KeYJavaType} of var + * @param typeRef + * the static {@link TypeReference} of var * @return a {@link LocalVariableDeclaration} of var with static type * type */ - public static LocalVariableDeclaration declare(IProgramVariable var, KeYJavaType type) { - return declare(var, null, type); + public static LocalVariableDeclaration declare(IProgramVariable var, TypeReference typeRef) { + return declare(var, null, typeRef); } /** * create a local variable declaration */ - public static LocalVariableDeclaration declare(String name, KeYJavaType type) { - return new LocalVariableDeclaration(new TypeRef(type), - new VariableSpecification(new LocationVariable(new ProgramElementName(name), type))); + public static LocalVariableDeclaration declare(String name, TypeReference typeRef) { + return new LocalVariableDeclaration(typeRef, + new VariableSpecification(new LocationVariable(new ProgramElementName(name), typeRef))); } /** * create a parameter declaration */ - - public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo, KeYJavaType kjt, + public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo, + TypeReference typeRef, String name) { - return new ParameterDeclaration(new Modifier[0], javaInfo.createTypeReference(kjt), - new VariableSpecification(localVariable(name, kjt)), false); + return new ParameterDeclaration(new Modifier[0], typeRef, + new VariableSpecification(localVariable(name, typeRef)), false); } /** @@ -253,17 +246,18 @@ public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo, KeYJa * the named and typed {@link IProgramVariable} to be declared as parameter * @return a {@link ParameterDeclaration} of var with static type kjt */ - public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo, KeYJavaType kjt, + public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo, + TypeReference typeRef, IProgramVariable var) { - return new ParameterDeclaration(new Modifier[0], javaInfo.createTypeReference(kjt), + return new ParameterDeclaration(new Modifier[0], typeRef, new VariableSpecification(var), false); } public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo, String type, String name) { - KeYJavaType kjt = javaInfo.getKeYJavaType(type); - return new ParameterDeclaration(new Modifier[0], javaInfo.createTypeReference(kjt), - new VariableSpecification(localVariable(name, kjt)), false); + TypeReference typeRef = new TypeRef(javaInfo.getKeYJavaType(type)); + return new ParameterDeclaration(new Modifier[0], typeRef, + new VariableSpecification(localVariable(name, typeRef)), false); } /** @@ -297,15 +291,15 @@ public static PassiveExpression passiveExpression(final Expression expression) { /** * create a local variable */ - public static ProgramVariable localVariable(String name, KeYJavaType kjt) { - return localVariable(new ProgramElementName(name), kjt); + public static ProgramVariable localVariable(String name, TypeReference typeRef) { + return localVariable(new ProgramElementName(name), typeRef); } /** * create a local variable */ - public static LocationVariable localVariable(ProgramElementName name, KeYJavaType kjt) { - return new LocationVariable(name, kjt); + public static LocationVariable localVariable(ProgramElementName name, TypeReference typeRef) { + return new LocationVariable(name, typeRef); } /** @@ -315,26 +309,26 @@ public static LocationVariable localVariable(ProgramElementName name, KeYJavaTyp * the {@link Services} whose {@link VariableNamer} is used * @param name * the {@link String} on which the variable's unique name is based - * @param type - * the variable's static {@link KeYJavaType} + * @param typeRef + * the variable's static {@link TypeReference} * @return a new {@link ProgramVariable} of static type type and with a unique name * based on name */ public static ProgramVariable localVariable(final Services services, final String name, - final KeYJavaType type) { + final TypeReference typeRef) { // first check for a saved name for this variable final NameRecorder nameRecorder = services.getNameRecorder(); for (var prop : nameRecorder.getSetProposals()) { if (prop.toString().startsWith(name + VariableNamer.TEMP_INDEX_SEPARATOR)) { return localVariable(new ProgramElementName(prop.toString()), - type); + typeRef); } } final ProgramElementName uniqueName = services.getVariableNamer().getTemporaryNameProposal(name); nameRecorder.addProposal(new Name(uniqueName.getProgramName())); - return localVariable(uniqueName, type); + return localVariable(uniqueName, typeRef); } /** @@ -429,17 +423,16 @@ public static Catch catchClause(final ParameterDeclaration parameter, * the {@link JavaInfo} containing kjt * @param param * the {@link String} name of the exception object variable - * @param kjt - * the {@link KeYJavaType} of the exception object variable + * @param typeRef + * the {@link TypeReference} of the exception object variable * @param body * the {@link StatementBlock} catch clause body * @return a new {@link Catch} with parameter param of static type kjt * and body body */ - public static Catch catchClause(JavaInfo javaInfo, String param, KeYJavaType kjt, + public static Catch catchClause(JavaInfo javaInfo, String param, TypeReference typeRef, StatementBlock body) { - - return new Catch(parameterDeclaration(javaInfo, kjt, param), body); + return new Catch(parameterDeclaration(javaInfo, typeRef, param), body); } /** @@ -464,8 +457,7 @@ public static Catch catchClause(JavaInfo javaInfo, String param, KeYJavaType kjt */ public static Catch catchClause(JavaInfo javaInfo, String param, String type, StatementBlock body) { - - return catchClause(javaInfo, param, javaInfo.getKeYJavaType(type), body); + return catchClause(javaInfo, param, new TypeRef(javaInfo.getKeYJavaType(type)), body); } /** @@ -941,18 +933,18 @@ public static Instanceof instanceOf(final Expression expression, final KeYJavaTy * type variable = 0; * * - * @param type - * the static {@link KeYJavaType} of variable + * @param typeRef + * the static {@link TypeReference} of variable * @param variable * the named and typed {@link IProgramVariable} to be declared * @return a new {@link LocalVariableDeclaration} of variable with static type * type and initial value zero */ - public static LocalVariableDeclaration declareZero(final KeYJavaType type, + public static LocalVariableDeclaration declareZero(final TypeReference typeRef, final IProgramVariable variable) { final IntLiteral zeroLiteral = zeroLiteral(); - return declare(variable, zeroLiteral, type); + return declare(variable, zeroLiteral, typeRef); } /** @@ -962,8 +954,8 @@ public static LocalVariableDeclaration declareZero(final KeYJavaType type, * type variable = reference.method(); * * - * @param type - * the static {@link KeYJavaType} of variable + * @param typeRef + * the static {@link TypeReference} of variable * @param variable * the named and typed {@link IProgramVariable} to be declared * @param reference @@ -973,11 +965,11 @@ public static LocalVariableDeclaration declareZero(final KeYJavaType type, * @return a new {@link LocalVariableDeclaration} of variable with static type * type and initial value reference.method() */ - public static LocalVariableDeclaration declareMethodCall(final KeYJavaType type, + public static LocalVariableDeclaration declareMethodCall(final TypeReference typeRef, final IProgramVariable variable, final ReferencePrefix reference, final String method) { final MethodReference call = methodCall(reference, method); - return declare(variable, call, type); + return declare(variable, call, typeRef); } /** @@ -1150,15 +1142,16 @@ public static ILoopInit loopInit(final LoopInitializer init) { * type variable = 0 * * - * @param type - * the static {@link KeYJavaType} of variable + * @param typeRef + * the static {@link TypeReference} of variable * @param variable * the named and typed {@link IProgramVariable} to be declared * @return a new {@link ILoopInit} that declares variable variable with static type * type and initial value zero */ - public static ILoopInit loopInitZero(final KeYJavaType type, final IProgramVariable variable) { - final LoopInitializer initializer = declareZero(type, variable); + public static ILoopInit loopInitZero(final TypeReference typeRef, + final IProgramVariable variable) { + final LoopInitializer initializer = declareZero(typeRef, variable); return loopInit(initializer); } @@ -1498,7 +1491,6 @@ public static CopyAssignment assignArrayField(final ProgramVariable variable, * @return a new {@link LocalVariableDeclaration} as defined by parameters */ public static LocalVariableDeclaration declare(final ExtList parameters) { - return new LocalVariableDeclaration(parameters); } @@ -1517,7 +1509,6 @@ public static LocalVariableDeclaration declare(final ExtList parameters) { * @return a new {@link LocalVariableDeclaration} of variable */ public static LocalVariableDeclaration declare(final IProgramVariable variable) { - return declare(variable, (Expression) null); } @@ -1539,9 +1530,9 @@ public static LocalVariableDeclaration declare(final IProgramVariable variable) */ public static LocalVariableDeclaration declare(final IProgramVariable variable, final Expression init) { - final KeYJavaType type = variable.getKeYJavaType(); + final TypeReference typeRef = variable.getTypeReference(); - return declare(variable, init, type); + return declare(variable, init, typeRef); } /** @@ -1557,16 +1548,16 @@ public static LocalVariableDeclaration declare(final IProgramVariable variable, * the named and typed {@link IProgramVariable} to be declared * @param init * the {@link Expression} variable is initialized with - * @param type - * the static {@link KeYJavaType} of variable + * @param typeRef + * the static {@link TypeReference} of variable * @return a new {@link LocalVariableDeclaration} of variable with static type * type and initial value init */ public static LocalVariableDeclaration declare(final Modifier modifier, - final IProgramVariable variable, final Expression init, final KeYJavaType type) { + final IProgramVariable variable, final Expression init, final TypeReference typeRef) { final ImmutableArray modifiers = new ImmutableArray<>(modifier); - return declare(modifiers, variable, init, type); + return declare(modifiers, variable, init, typeRef); } /** @@ -1582,41 +1573,16 @@ public static LocalVariableDeclaration declare(final Modifier modifier, * the named and typed {@link IProgramVariable} to be declared * @param init * the {@link Expression} variable is initialized with - * @param type - * the static {@link KeYJavaType} of variable + * @param typeRef + * the static {@link TypeReference} of variable * @return a new {@link LocalVariableDeclaration} of variable with static type * type and initial value init */ public static LocalVariableDeclaration declare(final Modifier[] modifiers, - final IProgramVariable variable, final Expression init, final KeYJavaType type) { + final IProgramVariable variable, final Expression init, final TypeReference typeRef) { final ImmutableArray m = new ImmutableArray<>(modifiers); - return declare(m, variable, init, type); - } - - /** - * Create a local variable declaration with an arbitrary number of modifiers. - * - * 
-     * modifiers type variable = init;
-     *
- * - * @param modifiers - * the {@link Modifier}s - * @param variable - * the named and typed {@link IProgramVariable} to be declared - * @param init - * the {@link Expression} variable is initialized with - * @param type - * the static {@link KeYJavaType} of variable - * @return a new {@link LocalVariableDeclaration} of variable with static type - * type and initial value init - */ - public static LocalVariableDeclaration declare(final ImmutableArray modifiers, - final IProgramVariable variable, final Expression init, final KeYJavaType type) { - final TypeRef typeRef = new TypeRef(type); - - return declare(modifiers, variable, init, typeRef); + return declare(m, variable, init, typeRef); } /** @@ -1996,6 +1962,8 @@ public static Finally finallyBlock(final StatementBlock body) { * the type's {@link ProgramElementName} * @param dimensions * the type's dimensions + * @param annotations + * the type's annotations * @param typePrefix * the type's {@link ReferencePrefix} * @param baseType @@ -2006,8 +1974,10 @@ public static Finally finallyBlock(final StatementBlock body) { public static ProgramElement declare(final ImmutableArray modifiers, final IProgramVariable variable, final Expression init, final ProgramElementName typeName, final int dimensions, + final ImmutableList annotations, final ReferencePrefix typePrefix, final KeYJavaType baseType) { - final TypeRef typeRef = new TypeRef(typeName, dimensions, typePrefix, baseType); + final TypeRef typeRef = + new TypeRef(typeName, annotations, dimensions, typePrefix, baseType); return declare(modifiers, variable, init, typeRef); } @@ -2700,11 +2670,13 @@ public static TypeRef typeRef(final KeYJavaType type) { * the base {@link KeYJavaType} * @param dimensions * the number of dimensions + * @param annotations + * the {@link ImmutableArray} of {@link AnnotationExpression}s * @return a new {@link TypeRef} for dimensions dimensions of type */ - public static TypeRef typeRef(final KeYJavaType type, final int dimensions) { - - return new TypeRef(type, dimensions); + public static TypeRef typeRef(final KeYJavaType type, final int dimensions, + final ImmutableList annotations) { + return new TypeRef(type, annotations, dimensions); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java index 713b62828a3..d8f4e968017 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java @@ -41,6 +41,7 @@ import com.github.javaparser.resolution.types.ResolvedReferenceType; import com.github.javaparser.resolution.types.ResolvedType; import com.github.javaparser.symbolsolver.javaparsermodel.declarations.DefaultConstructorDeclaration; +import com.github.javaparser.symbolsolver.javaparsermodel.declarations.JavaParserAnnotationDeclaration; import com.github.javaparser.symbolsolver.javaparsermodel.declarations.JavaParserMethodDeclaration; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; @@ -91,7 +92,11 @@ public Collection allTypes() { private List getAllMethods(KeYJavaType kjt) { var type = rec2key().resolveType(kjt); if (type.isReferenceType()) { - return type.asReferenceType().getAllMethods(); + var tr = type.asReferenceType(); + + if (!tr.getTypeDeclaration().orElseThrow().isAnnotation()) { + return tr.getAllMethods(); + } } return Collections.emptyList(); } @@ -164,6 +169,10 @@ public boolean isFinal(KeYJavaType kjt) { // Interfaces can't be final return false; } + if (td.isAnnotation()) { + // Interfaces can't be final + return false; + } if (td instanceof ResolvedLogicalType) { // Logic types are not final? Just following primitive types here return false; @@ -224,7 +233,18 @@ public List getAllProgramMethodsLocallyDeclared(KeYJavaType ct) { if (!type.isReferenceType()) { return result; } - var rml = type.asReferenceType().getDeclaredMethods(); + + var refType = type.asReferenceType(); + + // methods for annotation declarations are currently not implemented in + // javaparser + if (refType.getTypeDeclaration() + .map(d -> d instanceof JavaParserAnnotationDeclaration) + .orElse(false)) { + return result; + } + + var rml = refType.getDeclaredMethods(); result.ensureCapacity(rml.size()); for (MethodUsage methodUsage : rml) { if (methodUsage.getDeclaration() instanceof JavaParserMethodDeclaration) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/Annotation.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/Annotation.java new file mode 100644 index 00000000000..bc44148f377 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/Annotation.java @@ -0,0 +1,33 @@ +/* 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.java.ast; + +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.visitor.Visitor; + +public abstract class Annotation extends JavaNonTerminalProgramElement { + protected final KeYJavaType type; + + public Annotation(KeYJavaType type) { + this.type = type; + } + + @Override + public void visit(Visitor v) { + v.performActionOnAnnotation(this); + } + + public KeYJavaType getKeyJavaType() { + return type; + } + + @Override + public boolean equals(Object o) { + if (this == o) + return true; + if (o == null || getClass() != o.getClass()) + return false; + return ((Annotation) o).type.equals(type) && super.equals(o); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/KeYJavaType.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/KeYJavaType.java index f949de575e1..58f73eed2bf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/KeYJavaType.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/KeYJavaType.java @@ -97,7 +97,7 @@ public void markInternal() { * * @return the default value of the given type according to JLS Sect. 4.5.5 */ - public Literal getDefaultValue() { + public @Nullable Literal getDefaultValue() { if (javaType == null) { return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/NullType.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/NullType.java index 36fa7c46194..9d0f4ee5e2d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/NullType.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/NullType.java @@ -198,7 +198,6 @@ public Package getPackage() { return null; } - /** * returns the default value of the given type according to JLS Sect. 4.5.5 * diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/Type.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/Type.java index 50f31843bd7..4d458734394 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/Type.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/Type.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.ast.abstraction; + import de.uka.ilkd.key.java.ast.expression.literal.Literal; /** @@ -19,5 +20,4 @@ public interface Type extends ProgramModelElement { * @return the default value of the given type according to JLS Sect. 4.5.5 */ Literal getDefaultValue(); - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/annotation/MarkerAnnotation.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/annotation/MarkerAnnotation.java new file mode 100644 index 00000000000..43c885802f4 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/annotation/MarkerAnnotation.java @@ -0,0 +1,28 @@ +/* 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.java.ast.annotation; + +import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; + +public class MarkerAnnotation extends Annotation { + public MarkerAnnotation(KeYJavaType type) { + super(type); + } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public ProgramElement getChildAt(int index) { + throw new ArrayIndexOutOfBoundsException(); + } + + @Override + public String toString() { + return "@" + type.getJavaType().toString(); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/AnnotationInterfaceDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/AnnotationInterfaceDeclaration.java new file mode 100644 index 00000000000..3afdd89cf4b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/AnnotationInterfaceDeclaration.java @@ -0,0 +1,92 @@ +/* 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.java.ast.declaration; + +import java.util.List; + +import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.logic.ProgramElementName; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; + +import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.NonNull; + + +public class AnnotationInterfaceDeclaration extends TypeDeclaration { + public AnnotationInterfaceDeclaration( + PositionInfo pi, List comments, + @NonNull ImmutableArray modArray, + ProgramElementName name, ProgramElementName fullName, + ImmutableArray members, boolean parentIsInterfaceDeclaration, + boolean isLibrary, List jmlAttachments) { + super(pi, comments, modArray, name, fullName, members, parentIsInterfaceDeclaration, + isLibrary, ImmutableList.fromList(jmlAttachments)); + } + + /** + * returns the local declared supertypes + */ + public ImmutableList getSupertypes() { + return ImmutableList.of(); + } + + /** + * calls the corresponding method of a visitor in order to + * perform some action/transformation on this element + * + * @param v the Visitor + */ + public void visit(Visitor v) { + v.performActionOnAnnotationInterfaceDeclaration(this); + } + + /** + * Returns the number of children of this node. + * + * @return an int giving the number of children of this node + */ + public int getChildCount() { + int result = 0; + if (modArray != null) + result += modArray.size(); + if (name != null) + result++; + if (members != null) + result += members.size(); + return result; + } + + /** + * Returns the child at the specified index in this node's "virtual" child array + * + * @param index an index into this node's "virtual" child array + * @return the program element at the given position + * @throws ArrayIndexOutOfBoundsException if index is out of bounds + */ + public ProgramElement getChildAt(int index) { + int len; + if (modArray != null) { + len = modArray.size(); + if (len > index) + return modArray.get(index); + index -= len; + } + if (name != null) { + if (index == 0) + return name; + index--; + } + if (members != null) + return members.get(index); + throw new ArrayIndexOutOfBoundsException(); + } + + public boolean isInterface() { + return true; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/AnnotationInterfaceMemberDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/AnnotationInterfaceMemberDeclaration.java new file mode 100644 index 00000000000..132926048c8 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/AnnotationInterfaceMemberDeclaration.java @@ -0,0 +1,86 @@ +/* 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.java.ast.declaration; + +import de.uka.ilkd.key.java.ast.ProgramElement; +import de.uka.ilkd.key.java.ast.reference.TypeReference; +import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.logic.ProgramElementName; + +import org.key_project.util.collection.ImmutableArray; + +public class AnnotationInterfaceMemberDeclaration extends JavaDeclaration + implements MemberDeclaration { + private final TypeReference typeRef; + + private final ProgramElementName name; + + public AnnotationInterfaceMemberDeclaration(TypeReference typeRef, ProgramElementName name, + ImmutableArray modifiers) { + super(modifiers); + + this.typeRef = typeRef; + this.name = name; + } + + @Override + public int getChildCount() { + int result = 0; + + if (modArray != null) + result += modArray.size(); + if (name != null) + result++; + if (typeRef != null) + result++; + + return result; + } + + @Override + public ProgramElement getChildAt(int index) { + int len; + if (modArray != null) { + len = modArray.size(); + if (len > index) { + return modArray.get(index); + } + index -= len; + } + if (name != null) { + if (index == 0) + return name; + index--; + } + if (typeRef != null) { + if (index == 0) + return typeRef; + index--; + } + throw new ArrayIndexOutOfBoundsException(); + } + + @Override + public void visit(Visitor v) { + v.performActionOnAnnotationInterfaceMemberDeclaration(this); + } + + public TypeReference getTypeRef() { + return typeRef; + } + + public ProgramElementName getProgramElementName() { + return name; + } + + public boolean isPrivate() { return false; } + + public boolean isProtected() { return false; } + + public boolean isPublic() { return true; } + + public boolean isStatic() { return false; } + + public boolean isStrictFp() { return false; } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ArrayDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ArrayDeclaration.java index 1558d5e4c08..3b4234f72c6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ArrayDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ArrayDeclaration.java @@ -13,6 +13,9 @@ import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableList; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * KeY used to model arrays using only the {@link ArrayType}. As * the only attribute of an array has been the length attribute, it has been handled in a different @@ -26,6 +29,7 @@ public class ArrayDeclaration extends TypeDeclaration implements ArrayType { + private static final Logger LOGGER = LoggerFactory.getLogger(ArrayDeclaration.class); /** * reference to the type the elements of this array must subclass @@ -212,13 +216,14 @@ public static ProgramElementName createName(TypeReference basetype) { return null; } - public String getAlternativeNameRepresentation() { if (altNameRepresentation == null) { final StringBuilder alt = new StringBuilder(); Type baseType = this.baseType.getKeYJavaType().getJavaType(); - if (baseType instanceof ArrayType) { + if (baseType == null) { + alt.append(this.baseType.getKeYJavaType().getName()); + } else if (baseType instanceof ArrayType) { alt.append(((ArrayType) baseType).getAlternativeNameRepresentation()); } else { if (baseType instanceof ClassType) { @@ -233,7 +238,6 @@ public String getAlternativeNameRepresentation() { return altNameRepresentation; } - /** * returns the local declared supertypes */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java index f7a6fe67fc9..7e5b68cc415 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java @@ -18,6 +18,9 @@ import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * There are several types of class declarations: *
    @@ -58,6 +61,7 @@ */ public class ClassDeclaration extends TypeDeclaration implements Statement { + private static final Logger LOGGER = LoggerFactory.getLogger(ClassDeclaration.class); protected final Extends extending; @@ -256,9 +260,11 @@ public ImmutableList getSupertypes() { types = types.prepend(implementing.getTypeReferenceAt(i).getKeYJavaType()); } } + if (extending != null && !extending.getSupertypes().isEmpty()) { types = types.prepend(extending.getSupertypes().get(0).getKeYJavaType()); } + return types; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InheritanceSpecification.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InheritanceSpecification.java index ab6c9c82942..eff8e37b286 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InheritanceSpecification.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InheritanceSpecification.java @@ -12,6 +12,9 @@ import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * Inheritance specification. * @@ -21,6 +24,8 @@ public abstract class InheritanceSpecification extends JavaNonTerminalProgramElement implements TypeReferenceContainer { + private static final Logger LOGGER = LoggerFactory.getLogger(InheritanceSpecification.class); + /** * Supertypes. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java index db4cbe55210..dc16c283ec0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.Annotation; import de.uka.ilkd.key.java.ast.abstraction.*; import de.uka.ilkd.key.java.ast.abstraction.Package; import de.uka.ilkd.key.java.ast.expression.literal.NullLiteral; @@ -167,6 +168,16 @@ public NullLiteral getDefaultValue() { return NullLiteral.NULL; } + /** + * returns the annotations of the type resulting from the type declaration, + * which is no annotations. + * + * @return the annotations of the type declaration + */ + public ImmutableArray getAnnotations() { + return new ImmutableArray<>(); + } + /** * Get ProgramElementName. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/VariableDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/VariableDeclaration.java index 6a930c899c4..01dcec2f178 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/VariableDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/VariableDeclaration.java @@ -28,7 +28,6 @@ public abstract class VariableDeclaration extends JavaDeclaration /** * Type reference. */ - protected final TypeReference typeReference; /** @@ -41,7 +40,6 @@ public abstract class VariableDeclaration extends JavaDeclaration /** * Variable declaration. */ - protected VariableDeclaration() { typeReference = null; parentIsInterfaceDeclaration = false; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/AnnotationUseSpecification.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/AnnotationUseSpecification.java deleted file mode 100644 index 28acee43b25..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/AnnotationUseSpecification.java +++ /dev/null @@ -1,46 +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.java.ast.declaration.modifier; - -import de.uka.ilkd.key.java.ast.ProgramElement; -import de.uka.ilkd.key.java.ast.declaration.Modifier; -import de.uka.ilkd.key.java.ast.reference.TypeReference; -import de.uka.ilkd.key.java.ast.reference.TypeReferenceContainer; - -public class AnnotationUseSpecification extends Modifier implements TypeReferenceContainer { - - protected final TypeReference tr; - - public AnnotationUseSpecification(TypeReference tr) { - super(); - this.tr = tr; - } - - protected String getSymbol() { - return "@" + tr.toString(); - } - - public TypeReference getTypeReferenceAt(int index) { - if (index == 0) { - return tr; - } - throw new ArrayIndexOutOfBoundsException(); - } - - public int getTypeReferenceCount() { - return 1; - } - - public ProgramElement getChildAt(int index) { - if (index == 0) { - return tr; - } - throw new ArrayIndexOutOfBoundsException(); - } - - public int getChildCount() { - return 1; - } - -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/package-info.java index 573a2c02dcc..3f9cca9abe8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/package-info.java @@ -1,6 +1,4 @@ /** - * This package collects all Java modifiers. The sole abstraction beneath - * the parent {@link recoder.java.declaration.Modifier} is the - * {@link recoder.java.declaration.modifier.VisibilityModifier}. + * This package collects all Java modifiers. */ -package de.uka.ilkd.key.java.declaration.modifier; +package de.uka.ilkd.key.java.ast.declaration.modifier; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/DLEmbeddedExpression.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/DLEmbeddedExpression.java index db245659e60..a4bf74b4c80 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/DLEmbeddedExpression.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/DLEmbeddedExpression.java @@ -25,6 +25,7 @@ import org.key_project.logic.sort.Sort; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.ImmutableList; import org.jspecify.annotations.NonNull; @@ -121,7 +122,7 @@ public void check(Services javaServ, KeYJavaType containingClass) throws Convert final ProgramElementName programName = qualifier.isEmpty() ? new ProgramElementName(name) : new ProgramElementName(name, qualifier); - TypeRef tr = new TypeRef(programName, 0, null, containingClass); + TypeRef tr = new TypeRef(programName, ImmutableList.of(), 0, null, containingClass); ExecutionContext ec = new ExecutionContext(tr, null, null); for (int i = 0; i < actual; i++) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/New.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/New.java index 4f803d4aa11..38a083f527d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/New.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/New.java @@ -80,7 +80,6 @@ public New(ExtList children, ReferencePrefix rp, PositionInfo pi) { accessPath = rp; } - /** * Constructor for the transformation of COMPOST ASTs to KeY. * @@ -210,6 +209,7 @@ public ProgramElement getChildAt(int index) { if (index == 0) { return anonymousClass; } + index--; } throw new ArrayIndexOutOfBoundsException(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/NewArray.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/NewArray.java index 6f8621e366f..355314b54ba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/NewArray.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/NewArray.java @@ -210,6 +210,7 @@ public ProgramElement getChildAt(int index) { if (index == 0) { return arrayInitializer; } + index--; } throw new ArrayIndexOutOfBoundsException(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/TypeOperator.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/TypeOperator.java index 2612257790f..59ea05c30a8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/TypeOperator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/TypeOperator.java @@ -31,7 +31,6 @@ public abstract class TypeOperator extends Operator implements TypeReferenceCont */ protected final TypeReference typeReference; - /** * Constructor for the transformation of COMPOST ASTs to KeY. * @@ -121,6 +120,4 @@ public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) { public KeYJavaType getKeYJavaType(Services javaServ) { return getTypeReference().getKeYJavaType(); } - - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/ReferencePrefix.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/ReferencePrefix.java index c99cac7c3a1..ad00443a7a5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/ReferencePrefix.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/ReferencePrefix.java @@ -13,5 +13,4 @@ public interface ReferencePrefix extends ProgramElement { ReferencePrefix getReferencePrefix(); - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SchemaTypeReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SchemaTypeReference.java index 8f1211de06b..10ac56ef4e2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SchemaTypeReference.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SchemaTypeReference.java @@ -12,13 +12,15 @@ import de.uka.ilkd.key.rule.AbstractProgramElement; import de.uka.ilkd.key.rule.MatchConditions; +import org.key_project.util.collection.ImmutableList; + public class SchemaTypeReference extends TypeReferenceImp implements AbstractProgramElement { private final String fullName; public SchemaTypeReference(ProgramElementName name, int dimension, ReferencePrefix prefix) { - super(name, dimension, prefix); + super(name, ImmutableList.of(), dimension, prefix); final StringBuilder sb = new StringBuilder(); // as no inner classes prefix must be package reference @@ -31,6 +33,7 @@ public SchemaTypeReference(ProgramElementName name, int dimension, ReferencePref fullName = sb.toString(); } + @Override public KeYJavaType getKeYJavaType() { return null; } @@ -42,10 +45,12 @@ public KeYJavaType getKeYJavaType(Services services) { return kjt; } + @Override public ProgramElement getConcreteProgramElement(Services services) { return new TypeRef(getKeYJavaType(services)); } + @Override public MatchConditions match(SourceData source, MatchConditions matchCond) { ProgramElement t = source.getSource(); if (t instanceof TypeReference) { @@ -65,6 +70,7 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { * @param v * the Visitor */ + @Override public void visit(Visitor v) { v.performActionOnAbstractProgramElement(this); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SchematicFieldReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SchematicFieldReference.java index 0a83f703864..39fae03c8bc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SchematicFieldReference.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SchematicFieldReference.java @@ -22,8 +22,7 @@ * * @author AutoDoc */ -public class SchematicFieldReference extends FieldReference - implements MemberReference, ReferenceSuffix, TypeReferenceContainer, ExpressionContainer { +public class SchematicFieldReference extends FieldReference { private static final ProgramVariable SCHEMA_VARIABLE = new LocationVariable(new ProgramElementName("SCHEMA_VARIABLE_IGNORE"), JavaDLTheory.ANY); @@ -95,7 +94,6 @@ public ReferenceSuffix getReferenceSuffix() { return (ProgramSV) schemaVariable; } - /** * Set reference prefix. * @@ -105,7 +103,6 @@ public ReferencePrefix setReferencePrefix(ReferencePrefix rp) { return new SchematicFieldReference(schemaVariable, rp); } - /** * Return the type reference at the specified index in this node's "virtual" type reference * array. @@ -164,7 +161,6 @@ public void visit(Visitor v) { v.performActionOnSchematicFieldReference(this); } - public MatchConditions match(SourceData source, MatchConditions matchCond) { ProgramElement src = source.getSource(); if (!(src instanceof FieldReference)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeRef.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeRef.java index a008f4a6170..29b2a3e8355 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeRef.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeRef.java @@ -4,13 +4,14 @@ package de.uka.ilkd.key.java.ast.reference; - import java.util.Objects; +import de.uka.ilkd.key.java.ast.Annotation; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.logic.ProgramElementName; import org.key_project.util.ExtList; +import org.key_project.util.collection.ImmutableList; import org.jspecify.annotations.NonNull; @@ -21,33 +22,36 @@ public class TypeRef extends TypeReferenceImp { /** * creates a type reference for the given KeYJavaType with dimension 0 and creates a suitable * package reference prefix from the KeYJavaType. If this is not desired use the constructor - * TypeRef(ProgramElementName, int, ReferencePrefix, KeYJavaType) and take null as last + * TypeRef(ProgramElementName, ImmutableArray, int, ReferencePrefix, + * KeYJavaType) and take null as last * argument. */ public TypeRef(@NonNull KeYJavaType kjt) { - this(kjt, 0); + this(kjt, ImmutableList.of(), 0); } /** * creates a type reference for the given KeYJavaType and the given dimension and creates a * suitable package reference prefix from the KeYJavaType. If this is not desired use the - * constructor TypeRef(ProgramElementName, int, ReferencePrefix, KeYJavaType) and take null as + * constructor TypeRef(ProgramElementName, ImmutableArray, int, + * ReferencePrefix, KeYJavaType) and take null as * last argument. */ - public TypeRef(@NonNull KeYJavaType kjt, int dim) { - super(new ProgramElementName(kjt.getName()), dim, kjt.createPackagePrefix()); + public TypeRef(@NonNull KeYJavaType kjt, ImmutableList annotations, + int dim) { + super(new ProgramElementName(kjt.getName()), annotations, dim, kjt.createPackagePrefix()); this.kjt = kjt; } - public TypeRef(ExtList children, KeYJavaType kjt, int dim) { super(children, dim); this.kjt = kjt; } - public TypeRef(ProgramElementName name, int dimension, ReferencePrefix prefix, + public TypeRef(ProgramElementName name, ImmutableList annotations, + int dimension, ReferencePrefix prefix, KeYJavaType kjt) { - super(name, dimension, prefix); + super(name, annotations, dimension, prefix); this.kjt = kjt; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReference.java index e28114bea09..5f379e7e45d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReference.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReference.java @@ -3,11 +3,12 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.ast.reference; -import de.uka.ilkd.key.java.ast.NonTerminalProgramElement; -import de.uka.ilkd.key.java.ast.SourceElement; +import de.uka.ilkd.key.java.ast.Annotation; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.logic.ProgramElementName; +import org.key_project.util.collection.ImmutableList; + /** * TypeReferences reference Types by name. A TypeReference can refer to * an outer or inner type and hence can also be a {@link MemberReference}, but does not have to. A @@ -16,7 +17,7 @@ * {@link TypeReferenceContainer}. */ public interface TypeReference extends TypeReferenceInfix, TypeReferenceContainer, - PackageReferenceContainer, MemberReference, NonTerminalProgramElement, SourceElement { + PackageReferenceContainer, MemberReference { String getName(); @@ -27,4 +28,6 @@ public interface TypeReference extends TypeReferenceInfix, TypeReferenceContaine int getDimensions(); KeYJavaType getKeYJavaType(); + + ImmutableList getAnnotations(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReferenceImp.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReferenceImp.java index a0d4f71f143..796a9af466e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReferenceImp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReferenceImp.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.java.ast.reference; import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.Annotation; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.visitor.Visitor; @@ -11,6 +12,7 @@ import de.uka.ilkd.key.rule.MatchConditions; import org.key_project.util.ExtList; +import org.key_project.util.collection.ImmutableList; /** * TypeReferences reference Types by name. A TypeReference can refer to @@ -23,7 +25,6 @@ public abstract class TypeReferenceImp extends JavaNonTerminalProgramElement implements TypeReference { - /** * Prefix. */ @@ -39,6 +40,11 @@ public abstract class TypeReferenceImp extends JavaNonTerminalProgramElement */ protected final ProgramElementName name; + /** + * Annotations. + */ + protected final ImmutableList annotations; + /** * Constructor for the transformation of RECODER ASTs to KeY. @@ -54,21 +60,27 @@ protected TypeReferenceImp(ExtList children, int dim) { super(children); prefix = children.get(ReferencePrefix.class); name = children.get(ProgramElementName.class); + annotations = ImmutableList.of(children.collect(Annotation.class)); dimensions = dim; } protected TypeReferenceImp(ProgramElementName name) { - this(name, 0, null); + this(name, ImmutableList.of(), 0, null); } - protected TypeReferenceImp(ProgramElementName name, int dimension, ReferencePrefix prefix) { + protected TypeReferenceImp( + ProgramElementName name, + ImmutableList annotations, + int dimension, + ReferencePrefix prefix) { this.name = name; + this.annotations = annotations; this.dimensions = dimension; this.prefix = prefix; } - + @Override public SourceElement getFirstElement() { return (prefix == null) ? name : prefix.getFirstElement(); } @@ -83,6 +95,7 @@ public SourceElement getFirstElementIncludingBlocks() { * * @return an int giving the number of children of this node */ + @Override public int getChildCount() { int result = 0; if (prefix != null) { @@ -103,6 +116,7 @@ public int getChildCount() { * @exception ArrayIndexOutOfBoundsException * if index is out of bounds */ + @Override public ProgramElement getChildAt(int index) { if (prefix != null) { if (index == 0) { @@ -118,11 +132,17 @@ public ProgramElement getChildAt(int index) { throw new ArrayIndexOutOfBoundsException(); } + @Override + public ImmutableList getAnnotations() { + return annotations; + } + /** * Get the number of type references in this container. * * @return the number of type references. */ + @Override public int getTypeReferenceCount() { return (prefix instanceof TypeReference) ? 1 : 0; } @@ -137,6 +157,7 @@ public int getTypeReferenceCount() { * * @exception ArrayIndexOutOfBoundsException if index is out of bounds. */ + @Override public TypeReference getTypeReferenceAt(int index) { if (prefix instanceof TypeReference && index == 0) { return (TypeReference) prefix; @@ -149,6 +170,7 @@ public TypeReference getTypeReferenceAt(int index) { * * @return the number of expressions. */ + @Override public int getExpressionCount() { return (prefix instanceof Expression) ? 1 : 0; } @@ -162,6 +184,7 @@ public int getExpressionCount() { * * @exception ArrayIndexOutOfBoundsException if index is out of bounds. */ + @Override public Expression getExpressionAt(int index) { if (prefix instanceof Expression && index == 0) { return (Expression) prefix; @@ -174,6 +197,7 @@ public Expression getExpressionAt(int index) { * * @return the reference prefix. */ + @Override public ReferencePrefix getReferencePrefix() { return prefix; } @@ -183,6 +207,7 @@ public ReferencePrefix getReferencePrefix() { * * @return the package reference. */ + @Override public PackageReference getPackageReference() { return (prefix instanceof PackageReference) ? (PackageReference) prefix : null; } @@ -192,6 +217,7 @@ public PackageReference getPackageReference() { * * @return the int value. */ + @Override public int getDimensions() { return dimensions; } @@ -201,10 +227,12 @@ public int getDimensions() { * * @return the string. */ + @Override public final String getName() { return (name == null) ? null : name.toString(); } + @Override public abstract KeYJavaType getKeYJavaType(); /** @@ -212,12 +240,11 @@ public final String getName() { * * @return the identifier. */ - + @Override public ProgramElementName getProgramElementName() { return name; } - /** * calls the corresponding method of a visitor in order to perform some action/transformation on * this element @@ -225,17 +252,28 @@ public ProgramElementName getProgramElementName() { * @param v * the Visitor */ + @Override public void visit(Visitor v) { v.performActionOnTypeReference(this); } + @Override + public boolean equals(Object obj) { + if (obj == this) + return true; + if (obj instanceof TypeReference tr) { + return tr.getDimensions() == getDimensions() + && tr.getAnnotations().equals(getAnnotations()); + } + return false; + } + + @Override public MatchConditions match(SourceData source, MatchConditions matchCond) { final ProgramElement pe = source.getSource(); - if (!(pe instanceof TypeReference) - || ((TypeReference) pe).getDimensions() != getDimensions()) { + if (!equals(pe)) return null; - } return super.match(source, matchCond); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/CreateArrayMethodBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/CreateArrayMethodBuilder.java index 1384ec2d953..6df9cdfd581 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/CreateArrayMethodBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/CreateArrayMethodBuilder.java @@ -51,12 +51,16 @@ import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * This class creates the <createArray> method for array creation and in * particular its helper method <createArrayHelper>. This class should be * replaced by a recoder transformation as soon as we port our array data structures to RecodeR. */ public final class CreateArrayMethodBuilder extends KeYJavaASTFactory { + public static final Logger LOGGER = LoggerFactory.getLogger(CreateArrayMethodBuilder.class); public static final String IMPLICIT_ARRAY_CREATE = "$createArray"; @@ -70,7 +74,7 @@ public final class CreateArrayMethodBuilder extends KeYJavaASTFactory { /** * keeps the currently used integer type */ - private final KeYJavaType integerType; + private final TypeReference integerType; /** * stores the currently used object type @@ -86,7 +90,7 @@ public final class CreateArrayMethodBuilder extends KeYJavaASTFactory { /** create the method builder for array implict creation methods */ public CreateArrayMethodBuilder(KeYJavaType integerType, KeYJavaType objectType, Sort heapSort, int heapCount) { - this.integerType = integerType; + this.integerType = new TypeRef(integerType); this.objectType = objectType; this.heapSort = heapSort; this.heapCount = heapCount; @@ -217,7 +221,7 @@ public IProgramMethod getArrayInstanceAllocatorMethod(TypeReference arrayTypeRef new LocationVariable(new ProgramElementName("length"), integerType, true); final ParameterDeclaration param = new ParameterDeclaration(new Modifier[0], - new TypeRef(integerType), new VariableSpecification(paramLength), false); + integerType, new VariableSpecification(paramLength), false); final MethodDeclaration md = new MethodDeclaration(modifiers, arrayTypeReference, new ProgramElementName(PipelineConstants.IMPLICIT_INSTANCE_ALLOCATE), @@ -340,7 +344,7 @@ public IProgramMethod getCreateArrayMethod(TypeReference arrayTypeReference, new LocationVariable(new ProgramElementName("length"), integerType); final ParameterDeclaration param = new ParameterDeclaration(new Modifier[0], - new TypeRef(integerType), new VariableSpecification(paramLength), false); + integerType, new VariableSpecification(paramLength), false); final MethodDeclaration md = new MethodDeclaration(modifiers, arrayTypeReference, new ProgramElementName(IMPLICIT_ARRAY_CREATE), new ParameterDeclaration[] { param }, diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java index 994c0a25d3e..75d016606e2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.java.ast.CompilationUnit; import de.uka.ilkd.key.java.ast.Statement; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.annotation.MarkerAnnotation; import de.uka.ilkd.key.java.ast.ccatch.*; import de.uka.ilkd.key.java.ast.declaration.*; import de.uka.ilkd.key.java.ast.declaration.TypeDeclaration; @@ -76,7 +77,6 @@ import com.github.javaparser.resolution.declarations.ResolvedValueDeclaration; import com.github.javaparser.resolution.model.typesystem.ReferenceTypeImpl; import com.github.javaparser.resolution.types.ResolvedType; -import com.github.javaparser.resolution.types.ResolvedVoidType; import com.github.javaparser.symbolsolver.JavaSymbolSolver; import com.github.javaparser.symbolsolver.javaparsermodel.declarations.JavaParserFieldDeclaration; import com.github.javaparser.symbolsolver.javaparsermodel.declarations.JavaParserVariableDeclaration; @@ -185,7 +185,7 @@ public Object visit(ArrayAccessExpr n, Void arg) { public Object visit(ArrayCreationExpr n, Void arg) { PositionInfo pi = createPositionInfo(n); List c = createComments(n); - TypeReference type = accept(n.getElementType()); + TypeReference type = requireTypeReference(n.getElementType()); // TODO javaparser how should int[5][4][][] be encoded in the key ast? ArrayInitializer ai; ImmutableArray children; @@ -354,7 +354,6 @@ public Object visit(ClassOrInterfaceDeclaration n, Void arg) { Extends extending = new Extends(e); Implements implementing = new Implements(i); - TypeDeclaration td; if (n.isInterface()) { td = new InterfaceDeclaration( @@ -375,7 +374,7 @@ private KeYJavaType createOrCachedKeyJavaType(ReferenceTypeImpl ref) { if (kjt != null) { return kjt; } - return typeConverter.addReferenceType(ref); + return typeConverter.addReferenceType(ref.asReferenceType()); } @NonNull @@ -394,6 +393,10 @@ private boolean parentIsInterface(@NonNull Node n) { if (parent instanceof ClassOrInterfaceDeclaration) { return ((ClassOrInterfaceDeclaration) parent).isInterface(); } + + if (parent instanceof AnnotationDeclaration) { + return false; + } } return false; } @@ -419,15 +422,6 @@ public Object visit(ClassOrInterfaceType n, Void arg) { return reportError(n, "Type arguments found."); } - final var name = n.getNameAsString(); - if (name.startsWith("\\")) { - JavaInfo ji = services.getJavaInfo(); - KeYJavaType type = ji.getPrimitiveKeYJavaType(name); - if (type == null) { - return reportError(n, "Unresolved KeY type"); - } - return new TypeRef(type); - } return getKeYJavaType(n); } @@ -731,10 +725,10 @@ public Object visit(FieldAccessExpr n, Void arg) { public Object visit(TypeExpr n, Void arg) { ResolvedType rt = n.calculateResolvedType(); KeYJavaType kjt = getKeYJavaType(rt); - return new TypeRef(kjt); + ImmutableArray annots = map(n.getType().getAnnotations()); + return new TypeRef(kjt, annots.toImmutableList(), 0); } - private KeYJavaType getCachedKeYJavaType(ResolvedType rtype) { return typeConverter.getKeYJavaType(rtype, true); } @@ -1076,12 +1070,6 @@ public Object visit(NameExpr n, Void arg) { return reportUnsupportedElement(target.toAst().get()); } - @Override - public Object visit(NormalAnnotationExpr n, Void arg) { - // TODO - return super.visit(n, arg); - } - @Override public Object visit(NullLiteralExpr n, Void arg) { PositionInfo pi = createPositionInfo(n); @@ -1158,7 +1146,8 @@ private static ReferencePrefix convertScopeToReferencePrefix(ClassOrInterfaceTyp type.getScope().map(JP2KeYVisitor::convertScopeToReferencePrefix).orElse(null); ProgramElementName name = createProgramElementName(type.getName()); KeYJavaType resolvedType = getKeYJavaType(type.resolve()); - return new TypeRef(name, 0, prefix, resolvedType); + ImmutableArray annots = map(type.getAnnotations()); + return new TypeRef(name, annots.toImmutableList(), 0, prefix, resolvedType); } private ParameterDeclaration visitNoMap(Parameter n) { @@ -1181,7 +1170,7 @@ private ParameterDeclaration visitNoMap(Parameter n) { pv = (IProgramVariable) lookupSchemaVariable(n.getName()); } else { ProgramElementName name = VariableNamer.parseName(n.getName().asString()); - pv = new LocationVariable(name, type.getKeYJavaType(), n.isFinal()); + pv = new LocationVariable(name, type, n.isFinal()); } VariableSpecification spec = new VariableSpecification(pi, c, null, pv, 0, type.getKeYJavaType()); @@ -1198,7 +1187,8 @@ public Object visit(Parameter n, Void arg) { @Override public TypeReference visit(PrimitiveType n, Void arg) { - return new TypeRef(getKeYJavaType(n.resolve())); + ImmutableArray annots = map(n.getAnnotations()); + return new TypeRef(getKeYJavaType(n.resolve()), annots.toImmutableList(), 0); } @Override @@ -1223,7 +1213,9 @@ public Object visit(ArrayType n, Void arg) { } catch (IllegalStateException e) { System.out.println(e); } - return new TypeRef(getKeYJavaType(n.resolve())); + + ImmutableArray annots = map(n.getAnnotations()); + return new TypeRef(getKeYJavaType(n.resolve()), annots.toImmutableList(), 0); } @Override @@ -1249,11 +1241,6 @@ public Object visit(ReturnStmt n, Void arg) { return new Return(expr, pi, c); } - @Override - public Object visit(SingleMemberAnnotationExpr n, Void arg) { - return reportUnsupportedElement(n); - } - @Override public Object visit(StringLiteralExpr n, Void arg) { PositionInfo pi = createPositionInfo(n); @@ -1407,16 +1394,16 @@ private VariableSpecification visitVariableSpecification(TypeReference type, List c = createComments(v); Expression init = accepto(v.getInitializer()); IProgramVariable pv; - KeYJavaType kjt = type.getKeYJavaType(); if (v.getNameAsString().startsWith("#")) { pv = (IProgramVariable) lookupSchemaVariable(v.getNameAsString(), v); } else { ProgramElementName name = VariableNamer.parseName(v.getNameAsString()); - pv = new LocationVariable(name, kjt, modifiers.hasModifier(JML_GHOST), + pv = new LocationVariable(name, type, modifiers.hasModifier(JML_GHOST), modifiers.hasModifier(FINAL)); } - return addToMapping(v, new VariableSpecification(pi, c, init, pv, 0, kjt)); + return addToMapping(v, + new VariableSpecification(pi, c, init, pv, 0, type.getKeYJavaType())); } /** @@ -1491,22 +1478,26 @@ private ProgramVariable getProgramVariableForFieldSpecification(FullVariableDecl VariableDeclarator spec = decl.decl; ProgramElement varSpec = mapping.nodeToKeY(spec); if (varSpec == null) { - ResolvedType t = spec.getType().resolve(); - ClassOrInterfaceDeclaration classNode = findContainingClass(spec).orElseThrow(); - ReferenceTypeImpl classType = new ReferenceTypeImpl(classNode.resolve()); + Type t = spec.getType(); + var containing = (com.github.javaparser.ast.body.TypeDeclaration) findParent(spec, + n -> n instanceof ClassOrInterfaceDeclaration + || n instanceof AnnotationDeclaration) + .orElseThrow(); + + ReferenceTypeImpl refType = new ReferenceTypeImpl(containing.resolve()); final ProgramElementName pen = new ProgramElementName(spec.getName().asString(), - classNode.getFullyQualifiedName().orElseThrow()); + (String) containing.getFullyQualifiedName().orElseThrow()); final Literal compileTimeConstant = getCompileTimeConstantInitializer(decl); if (compileTimeConstant == null) { - pv = new LocationVariable(pen, getKeYJavaType(t), - getKeYJavaType(classType), decl.isStatic, decl.isModel, + pv = new LocationVariable(pen, accept(t), + getKeYJavaType(refType), decl.isStatic, decl.isModel, decl.isGhost, decl.isFinal); } else { - pv = new ProgramConstant(pen, getKeYJavaType(t), - getKeYJavaType(classType), decl.isStatic, + pv = new ProgramConstant(pen, accept(t), + getKeYJavaType(refType), decl.isStatic, compileTimeConstant); } } else { @@ -1518,11 +1509,6 @@ private ProgramVariable getProgramVariableForFieldSpecification(FullVariableDecl return pv; } - private static Optional findContainingClass(Node node) { - return findParent(node, n -> n instanceof ClassOrInterfaceDeclaration) - .map(c -> (ClassOrInterfaceDeclaration) c); - } - private static Optional findParent(Node node, Predicate filter) { Optional n = Optional.of(node); while (n.isPresent() && !filter.test(n.get())) { @@ -1535,7 +1521,7 @@ private FieldSpecification visitFieldSpecification(FullVariableDeclarator v) { PositionInfo pi = createPositionInfo(v.decl); List c = createComments(v.decl); Expression init = accepto(v.decl.getInitializer()); - KeYJavaType type = getKeYJavaType(v.decl.getType().resolve()); + KeYJavaType type = requireTypeReference(v.decl.getType()).getKeYJavaType(); ProgramVariable pv = getProgramVariableForFieldSpecification(v); return new FieldSpecification(pi, c, init, pv, 0, type); } @@ -1548,7 +1534,8 @@ public Object visit(VariableDeclarator n, Void arg) { @Override public Object visit(VoidType n, Void arg) { - return new TypeRef(getKeYJavaType(ResolvedVoidType.INSTANCE)); + ImmutableArray annots = map(n.annotations()); + return new TypeRef(getKeYJavaType(n.resolve()), annots.toImmutableList(), 0); } @Override @@ -1580,8 +1567,7 @@ public Object visit(ImportDeclaration n, Void arg) { // TODO: is the lookup correct? Seems to work in small examples ... String typename = n.getName().asString(); KeYJavaType kjt = typeConverter.getKeYJavaType(typename); - TypeReference typeRef = new TypeRef(kjt); - return new Import(typeRef, n.isAsterisk(), pi, c); + return new Import(new TypeRef(kjt), n.isAsterisk(), pi, c); } } @@ -2084,19 +2070,47 @@ public Object visit(TypeParameter n, Void arg) { @Override public Object visit(AnnotationDeclaration n, Void arg) { - return reportUnsupportedElement(n); + final var ref = new ReferenceTypeImpl(n.resolve()); + var kjt = createOrCachedKeyJavaType(ref); + + var pi = createPositionInfo(n); + var c = createComments(n); + ProgramElementName name = createProgramElementName(n.getName()); + ProgramElementName fullName = new ProgramElementName(n.getFullyQualifiedName().get()); + boolean isLibrary = mapping.isParsingLibraries(); + ImmutableArray modArray = + map(n.getModifiers()); + ImmutableArray members = map(n.getMembers()); + boolean parentIsInterface = false; + + TypeDeclaration td = new AnnotationInterfaceDeclaration( + pi, c, modArray, name, fullName, members, + parentIsInterface, isLibrary, getClassSpec(n)); + kjt.setJavaType(td); + mapping.registerType(ref, kjt); + return addToMapping(n, td); } @Override public Object visit(AnnotationMemberDeclaration n, Void arg) { - return reportUnsupportedElement(n); + var existing = mapping.nodeToKeY(n); + if (existing != null) { + return existing; + } + + TypeReference typeRef = requireTypeReference(n.getType()); + ImmutableArray modifiers = + map(n.getModifiers()); + ProgramElementName name = createProgramElementName(n.getName()); + var decl = new AnnotationInterfaceMemberDeclaration(typeRef, name, modifiers); + return addToMapping(n, decl); } @Override public Object visit(ClassExpr n, Void arg) { PositionInfo pi = createPositionInfo(n); List c = createComments(n); - TypeReference rt = accept(n.getType()); + TypeReference rt = requireTypeReference(n.getType()); return new MetaClassReference(pi, c, rt); } @@ -2119,6 +2133,18 @@ public Object visit(TraditionalJavadocComment n, Void arg) { @Override public Object visit(MarkerAnnotationExpr n, Void arg) { + final var ref = new ReferenceTypeImpl(n.resolve()); + var kjt = createOrCachedKeyJavaType(ref); + return new MarkerAnnotation(kjt); + } + + @Override + public Object visit(NormalAnnotationExpr n, Void arg) { + return reportUnsupportedElement(n); + } + + @Override + public Object visit(SingleMemberAnnotationExpr n, Void arg) { return reportUnsupportedElement(n); } @@ -2186,7 +2212,8 @@ public Object visit(ReceiverParameter n, Void arg) { @Override public Object visit(VarType n, Void arg) { var kjt = getKeYJavaType(n.resolve()); - return new TypeRef(kjt); + ImmutableArray annots = map(n.getAnnotations()); + return new TypeRef(kjt, annots.toImmutableList(), 0); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYTypeConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYTypeConverter.java index 45a492db86e..7ab7e79eb30 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYTypeConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYTypeConverter.java @@ -183,7 +183,6 @@ public KeYJavaType createKeYJavaType(ReferenceTypeImpl ref) { return getObjectType(); } - { // lookup in the cache var kjt = jp2KeY.resolvedTypeToKeY(type, services.getJavaService()); @@ -398,7 +397,7 @@ private ArrayDeclaration createArrayType(KeYJavaType baseType, KeYJavaType array baseTypeRef = new TypeRef(baseType); } else { baseTypeRef = new TypeRef(new ProgramElementName(baseType.getSort().name().toString()), - 0, null, baseType); + ImmutableList.of(), 0, null, baseType); } ExtList members = new ExtList(); @@ -421,7 +420,7 @@ private KeYJavaType createSuperArrayType() { var superArrayType = new KeYJavaType(); var specLength = new FieldSpecification(new LocationVariable(new ProgramElementName("length"), - integerType, superArrayType, false, false, false, true)); + new TypeRef(integerType), superArrayType, false, false, false, true)); var f = new FieldDeclaration(new Modifier[] { new Public(), new Final() }, new TypeRef(integerType), new FieldSpecification[] { specLength }, false); superArrayType.setJavaType(new SuperArrayDeclaration(f)); @@ -442,7 +441,7 @@ private void addImplicitArrayMembers(ExtList members, KeYJavaType parent, KeYJav int dimension = base instanceof ArrayType ? ((ArrayType) base).getDimension() + 1 : 1; TypeRef parentReference = new TypeRef(new ProgramElementName(String.valueOf(parent.getSort().name())), - dimension, null, parent); + ImmutableList.of(), dimension, null, parent); // add methods // the only situation where base can be null is in case of a diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java index cf90a5109b2..ff0e5b2b5fc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java @@ -55,8 +55,9 @@ public static KeYJavaPipeline createDefault(TransformationPipelineServices pipel p.add(new CreateObjectBuilder(pipelineServices)); p.add(new LocalClassTransformation(pipelineServices)); // Below is an expensive transformation as it has to traverse down - // to an expression level. + // to an expression level p.add(new ConstantStringExpressionEvaluator(pipelineServices)); + p.add(new UniverseMethodContractAdder(pipelineServices)); return p; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassInitializeMethodBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassInitializeMethodBuilder.java index b95e50aa311..4917d2bc9d3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassInitializeMethodBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassInitializeMethodBuilder.java @@ -294,6 +294,8 @@ private MethodDeclaration createInitializeMethod(TypeDeclaration td) { */ @Override public void apply(TypeDeclaration td) { + if (td.isAnnotationDeclaration()) + return; td.addMember(createInitializeMethod(td)); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassPreparationMethodBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassPreparationMethodBuilder.java index c6b7bd3e40b..c3941da6628 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassPreparationMethodBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassPreparationMethodBuilder.java @@ -158,6 +158,8 @@ private MethodDeclaration createPrepareMethod(TypeDeclaration td) { * the TypeDeclaration */ public void apply(TypeDeclaration td) { + if (td.isAnnotationDeclaration()) + return; td.addMember(createPrepareMethod(td)); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java index d4aab99e260..c753dfb3bb1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java @@ -278,27 +278,28 @@ private ConstructorDeclaration attachConstructorDecl(TypeDeclaration td) { * the TypeDeclaration */ public void apply(TypeDeclaration td) { - if (td instanceof ClassOrInterfaceDeclaration) { - var cd = (ClassOrInterfaceDeclaration) td; - if (cd.isInterface()) { - return; - } - var constructors = new ArrayList<>(td.getConstructors()); - ConstructorDeclaration anonConstr = null; - if (cd.getName() == null) { - anonConstr = attachConstructorDecl(td); - } - if (anonConstr != null) - constructors.add(anonConstr); + if (!td.isClassOrInterfaceDeclaration()) + return; - if (constructors.isEmpty()) { - final ConstructorDeclaration defaultConstructor = attachDefaultConstructor(cd); - constructors.add(defaultConstructor); - } + var cd = (ClassOrInterfaceDeclaration) td; + if (cd.isInterface()) { + return; + } + var constructors = new ArrayList<>(td.getConstructors()); + ConstructorDeclaration anonConstr = null; + if (cd.getName() == null) { + anonConstr = attachConstructorDecl(td); + } + if (anonConstr != null) + constructors.add(anonConstr); - for (ConstructorDeclaration constructor : constructors) { - normalform(cd, constructor); - } + if (constructors.isEmpty()) { + final ConstructorDeclaration defaultConstructor = attachDefaultConstructor(cd); + constructors.add(defaultConstructor); + } + + for (ConstructorDeclaration constructor : constructors) { + normalform(cd, constructor); } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateBuilder.java index c525e3eea82..2e523339072 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateBuilder.java @@ -90,9 +90,10 @@ modifiers, new ClassOrInterfaceType(null, services.getId(type)), * the TypeDeclaration */ public void apply(TypeDeclaration td) { - if (td instanceof ClassOrInterfaceDeclaration - && ((ClassOrInterfaceDeclaration) td).isInterface()) { - // Interfaces can't have fields, so nothing to set + if (td.isAnnotationDeclaration() + || td.isClassOrInterfaceDeclaration() + && ((ClassOrInterfaceDeclaration) td).isInterface()) { + // Interfaces and Annotations can't have fields, so nothing to set return; } td.addMember(createMethod(td)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ImplicitFieldAdder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ImplicitFieldAdder.java index d3f58684bb3..6a73da12ac7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ImplicitFieldAdder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ImplicitFieldAdder.java @@ -217,6 +217,9 @@ private void addFieldsForFinalVars(TypeDeclaration td) { } public void apply(TypeDeclaration td) { + if (td.isAnnotationDeclaration()) + return; + addImplicitFields(td); addFieldsForFinalVars(td); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java index 6db5f5ed9ed..437997c38c2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java @@ -63,7 +63,7 @@ /// /// You can access attached JML information using the {@link DataKey} in /// [JMLTransformer#KEY_SPEC_CASE], -/// [JMLTransformer#KEY_SPEC_CASE], and [JMLTransformer#KEY_SPEC_CASE]. +/// [JMLTransformer#KEY_CLASS_SPEC], and [JMLTransformer#KEY_LOOP_SPEC]. /// /// JMLModifier are reduced to *normal* modifier of /// {@link com.github.javaparser.ast.Modifier.DefaultKeyword}. diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/UniverseMethodContractAdder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/UniverseMethodContractAdder.java new file mode 100644 index 00000000000..015aa7455a9 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/UniverseMethodContractAdder.java @@ -0,0 +1,118 @@ +/* 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.java.transformations.pipeline; + +import java.util.Arrays; +import java.util.List; + +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase.ClauseHd; +import de.uka.ilkd.key.speclang.njml.JmlFacade; +import de.uka.ilkd.key.speclang.njml.LabeledParserRuleContext; + +import com.github.javaparser.ast.CompilationUnit; +import com.github.javaparser.ast.NodeList; +import com.github.javaparser.ast.body.ConstructorDeclaration; +import com.github.javaparser.ast.body.MethodDeclaration; +import com.github.javaparser.ast.body.Parameter; +import com.github.javaparser.ast.expr.AnnotationExpr; +import com.github.javaparser.ast.type.Type; +import org.jspecify.annotations.NonNull; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import static de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase.ClauseHd.ACCESSIBLE; +import static de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase.ClauseHd.ASSIGNABLE_FREE; + +public class UniverseMethodContractAdder extends JavaTransformerAbstract { + public final static Logger LOGGER = LoggerFactory.getLogger(UniverseMethodContractAdder.class); + + public final static String[] OWNERSHIP = new String[] { "Rep", "Peer", "Dom" }; + public final static String[] REPONLY = new String[] { "RepOnly" }; + + public UniverseMethodContractAdder(@NonNull TransformationPipelineServices services) { + super(services); + } + + @Override + public void apply(CompilationUnit cu) { + cu.walk(it -> { + if (!(it instanceof MethodDeclaration || + it instanceof ConstructorDeclaration)) + return; + + Type returnT = null; + AnnotationExpr returnAnnot = null; + boolean isRepOnly = false; + NodeList params = null; + + if (it instanceof MethodDeclaration meth) { + returnT = meth.getType(); + if (returnT.isVoidType()) + returnT = null; + + returnAnnot = filterAnnots(meth.getAnnotations(), OWNERSHIP); + isRepOnly = filterAnnots(meth.getAnnotations(), REPONLY) != null; + params = meth.getParameters(); + } + + if (it instanceof ConstructorDeclaration cons) { + isRepOnly = filterAnnots(cons.getAnnotations(), REPONLY) != null; + params = cons.getParameters(); + } + + List specList = TransformationPipelineServices.getSpec(it); + for (TextualJMLConstruct spec : specList) { + if (!(spec instanceof TextualJMLSpecCase)) + continue; + var sc = (TextualJMLSpecCase) spec; + + if (isRepOnly) { + var context = new LabeledParserRuleContext( + JmlFacade.parseExpr("\\dl_createdRepfp(this)")); + sc.addClause(ASSIGNABLE_FREE, null, context); + + if (returnT != null) { + sc.addClause(ACCESSIBLE, null, context); + } + } + + if (returnAnnot != null) { + sc.addClause(ClauseHd.ENSURES_FREE, + getOwnershipContext("\\result", returnAnnot)); + } + + for (Parameter param : params) { + AnnotationExpr annot = filterAnnots(param.annotations(), OWNERSHIP); + if (annot == null) + continue; + sc.addClause(ClauseHd.REQUIRES_FREE, + getOwnershipContext(param.getNameAsString(), annot)); + } + } + }); + } + + private static LabeledParserRuleContext getOwnershipContext(String varName, + AnnotationExpr annot) { + String fstring = annot.getNameAsString().equals("Rep") + ? "%1$s != null ==> this == \\dl_owner(%1$s)" + : annot.getNameAsString().equals("Peer") + ? "%1$s != null ==> \\dl_owner(this) == \\dl_owner(%1$s)" + : "%1$s != null ==> \\dl_dominates(this, %1$s)"; + String expr = String.format(fstring, varName); + return new LabeledParserRuleContext(JmlFacade.parseExpr(expr)); + } + + private static AnnotationExpr filterAnnots(NodeList annots, String[] allowed) { + if (annots == null) + return null; + return annots.stream() + .filter(annot -> Arrays.stream(allowed) + .anyMatch(val -> annot.getName().toString().equals(val))) + .findFirst() + .orElse(null); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java index 247791dc88c..f88ade93e0b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java @@ -5,6 +5,7 @@ import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.Annotation; import de.uka.ilkd.key.java.ast.ccatch.*; import de.uka.ilkd.key.java.ast.declaration.*; import de.uka.ilkd.key.java.ast.expression.ArrayInitializer; @@ -471,6 +472,17 @@ public void performActionOnInterfaceDeclaration(InterfaceDeclaration x) { doDefaultAction(x); } + @Override + public void performActionOnAnnotationInterfaceDeclaration(AnnotationInterfaceDeclaration x) { + doDefaultAction(x); + } + + @Override + public void performActionOnAnnotationInterfaceMemberDeclaration( + AnnotationInterfaceMemberDeclaration x) { + doDefaultAction(x); + } + @Override public void performActionOnIntLiteral(IntLiteral x) { doDefaultAction(x); @@ -634,6 +646,11 @@ public void performActionOnParenthesizedExpression(ParenthesizedExpression x) { doDefaultAction(x); } + @Override + public void performActionOnAnnotation(Annotation x) { + doDefaultAction(x); + } + @Override public void performActionOnPassiveExpression(PassiveExpression x) { doDefaultAction(x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java index 1890954ca7a..3f10903b512 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java @@ -448,7 +448,7 @@ public void performActionOnFinally(final Finally x) { // Remember current flags. for (Entry entry : oldFlags.entrySet()) { newStatements.add(KeYJavaASTFactory.declare(entry.getValue(), entry.getKey(), - entry.getValue().getKeYJavaType())); + entry.getValue().getTypeReference())); } // Reset flags. @@ -479,7 +479,7 @@ private void addOldFlag(Map oldFlags, ProgramV new LocationVariable( new ProgramElementName( flag.getProgramElementName().toString() + "__BEFORE_FINALLY"), - flag.getKeYJavaType())); + flag.getTypeReference())); } private void changed() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java index c776d93e82d..1d935bcc656 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.java.visitor; import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.Annotation; import de.uka.ilkd.key.java.ast.ccatch.*; import de.uka.ilkd.key.java.ast.declaration.*; import de.uka.ilkd.key.java.ast.expression.ArrayInitializer; @@ -120,6 +121,11 @@ public interface Visitor { void performActionOnInterfaceDeclaration(InterfaceDeclaration x); + void performActionOnAnnotationInterfaceDeclaration(AnnotationInterfaceDeclaration x); + + void performActionOnAnnotationInterfaceMemberDeclaration( + AnnotationInterfaceMemberDeclaration x); + void performActionOnFieldDeclaration(FieldDeclaration x); void performActionOnLocalVariableDeclaration(LocalVariableDeclaration x); @@ -328,6 +334,8 @@ public interface Visitor { void performActionOnLoopInit(LoopInit x); + void performActionOnAnnotation(Annotation annot); + void performActionOnAssert(Assert assert1); void performActionOnProgramConstant(ProgramConstant constant); diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java index 3f841bfd2a5..84592744eed 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java @@ -23,7 +23,7 @@ import org.key_project.util.collection.ImmutableList; /** - * The JavaDL theory class provides access to function symvols, sorts that are part of the core + * The JavaDL theory class provides access to function symbols, sorts that are part of the core * logic * like cast or instanceof functions. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/InnerVariableNamer.java b/key.core/src/main/java/de/uka/ilkd/key/logic/InnerVariableNamer.java index eb0edc7087c..f3fb7ee33a2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/InnerVariableNamer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/InnerVariableNamer.java @@ -69,7 +69,7 @@ public LocationVariable rename(LocationVariable var, Goal goal, PosInOccurrence LocationVariable newvar = var; if (!newname.equals(name)) { - newvar = new LocationVariable(newname, var.getKeYJavaType()); + newvar = new LocationVariable(newname, var.getTypeReference()); map.put(var, newvar); renamingHistory = map; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java index c290f920b27..fa904b57afa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java @@ -13,6 +13,8 @@ import de.uka.ilkd.key.java.TypeConverter; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.ast.reference.TypeRef; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.ldt.*; import de.uka.ilkd.key.logic.label.OriginTermLabel; import de.uka.ilkd.key.logic.label.OriginTermLabelFactory; @@ -39,6 +41,8 @@ import org.key_project.logic.sort.Sort; import org.key_project.util.collection.*; +import static de.uka.ilkd.key.java.KeYJavaASTFactory.typeRef; + /** *

    * Use this class if you intend to build complex terms by hand. It is more convenient than @@ -208,38 +212,40 @@ public String newName(Sort sort) { /** * Creates a program variable for "self". Take care to register it in the namespaces! */ - public LocationVariable selfVar(KeYJavaType kjt, boolean makeNameUnique) { - return selfVar(kjt, makeNameUnique, ""); + public LocationVariable selfVar(TypeReference typeRef, boolean makeNameUnique) { + return selfVar(typeRef, makeNameUnique, ""); } /** * Creates a program variable for "self". Take care to register it in the namespaces! */ - public LocationVariable selfVar(KeYJavaType kjt, boolean makeNameUnique, String postfix) { + public LocationVariable selfVar(TypeReference typeRef, boolean makeNameUnique, String postfix) { String name = "self" + postfix; - return locationVariable(name, kjt, makeNameUnique); + return locationVariable(name, typeRef, makeNameUnique); } /** * Creates a program variable for "self". Take care to register it in the namespaces! */ - public LocationVariable selfVar(IProgramMethod pm, KeYJavaType kjt, boolean makeNameUnique, + public LocationVariable selfVar(IProgramMethod pm, TypeReference typeRef, + boolean makeNameUnique, String postfix) { if (pm.isStatic()) { return null; } else { - return selfVar(kjt, makeNameUnique, postfix); + return selfVar(typeRef, makeNameUnique, postfix); } } /** * Creates a program variable for "self". Take care to register it in the namespaces! */ - public LocationVariable selfVar(IProgramMethod pm, KeYJavaType kjt, boolean makeNameUnique) { + public LocationVariable selfVar(IProgramMethod pm, TypeReference typeRef, + boolean makeNameUnique) { if (pm.isStatic()) { return null; } else { - return selfVar(kjt, makeNameUnique); + return selfVar(typeRef, makeNameUnique); } } @@ -258,7 +264,8 @@ public ImmutableList paramVars(IObserverFunction obs, } else { name = String.valueOf(paramType.getSort().name().toString().charAt(0)); } - final LocationVariable paramVar = locationVariable(name, paramType, makeNamesUnique); + final LocationVariable paramVar = + locationVariable(name, new TypeRef(paramType), makeNamesUnique); result = result.append(paramVar); } return result; @@ -273,7 +280,8 @@ public ImmutableList paramVars(String postfix, IObserverFuncti ImmutableList result = ImmutableList.nil(); for (LocationVariable paramVar : paramVars) { ProgramElementName pen = new ProgramElementName(paramVar.name() + postfix); - LocationVariable formalParamVar = new LocationVariable(pen, paramVar.getKeYJavaType()); + LocationVariable formalParamVar = + new LocationVariable(pen, paramVar.getTypeReference()); result = result.append(formalParamVar); } return result; @@ -295,7 +303,7 @@ public LocationVariable resultVar(String name, IProgramMethod pm, boolean makeNa return null; } else { name += "_" + pm.getName(); - return locationVariable(name, pm.getReturnType(), makeNameUnique); + return locationVariable(name, new TypeRef(pm.getReturnType()), makeNameUnique); } } @@ -313,7 +321,8 @@ public LocationVariable excVar(IProgramMethod pm, boolean makeNameUnique) { */ public LocationVariable excVar(String name, IProgramMethod pm, boolean makeNameUnique) { return locationVariable(name, - services.getJavaInfo().getTypeByClassName(JAVA_LANG_THROWABLE), makeNameUnique); + new TypeRef(services.getJavaInfo().getTypeByClassName(JAVA_LANG_THROWABLE)), + makeNameUnique); } /** @@ -338,7 +347,7 @@ public LocationVariable atPreVar(String baseName, Sort sort, boolean makeNameUni if (kjt == null) { kjt = new KeYJavaType(sort); } - return atPreVar(baseName, kjt, makeNameUnique); + return atPreVar(baseName, new TypeRef(kjt), makeNameUnique); } /** @@ -346,12 +355,13 @@ public LocationVariable atPreVar(String baseName, Sort sort, boolean makeNameUni * namespaces. * * @param baseName the base name to use - * @param kjt the type of the variable + * @param typeRef the type of the variable * @param makeNameUnique whether to change the base name to be unique * @return a location variable for the given name and type */ - public LocationVariable atPreVar(String baseName, KeYJavaType kjt, boolean makeNameUnique) { - return locationVariable(baseName + "AtPre", kjt, makeNameUnique); + public LocationVariable atPreVar(String baseName, TypeReference typeRef, + boolean makeNameUnique) { + return locationVariable(baseName + "AtPre", typeRef, makeNameUnique); } /** @@ -364,7 +374,7 @@ public LocationVariable atPreVar(String baseName, KeYJavaType kjt, boolean makeN * @return a location variable for the given name and type */ public LocationVariable locationVariable(String baseName, Sort sort, boolean makeNameUnique) { - return locationVariable(baseName, new KeYJavaType(sort), makeNameUnique); + return locationVariable(baseName, new TypeRef(new KeYJavaType(sort)), makeNameUnique); } /** @@ -372,16 +382,16 @@ public LocationVariable locationVariable(String baseName, Sort sort, boolean mak * the namespaces. * * @param baseName the base name to use - * @param kjt the type of the variable + * @param typeRef the type of the variable * @param makeNameUnique whether to change the base name to be unique * @return a location variable for the given name and type */ - public LocationVariable locationVariable(String baseName, KeYJavaType kjt, + public LocationVariable locationVariable(String baseName, TypeReference typeRef, boolean makeNameUnique) { if (makeNameUnique) { baseName = newName(baseName); } - return new LocationVariable(new ProgramElementName(baseName), kjt); + return new LocationVariable(new ProgramElementName(baseName), typeRef); } // ------------------------------------------------------------------------- diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IProgramVariable.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IProgramVariable.java index 68c4d837564..a6726f5fc6c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IProgramVariable.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IProgramVariable.java @@ -7,16 +7,17 @@ import de.uka.ilkd.key.java.ast.TerminalProgramElement; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.ast.reference.TypeReference; -import org.key_project.logic.op.Operator; import org.key_project.logic.op.SortedOperator; - public interface IProgramVariable - extends TerminalProgramElement, SortedOperator, Operator { + extends TerminalProgramElement, SortedOperator { KeYJavaType getKeYJavaType(); KeYJavaType getKeYJavaType(Services javaServ); KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec); + + TypeReference getTypeReference(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/JAbstractSortedOperator.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/JAbstractSortedOperator.java index 3375c5108fe..15917981e89 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/JAbstractSortedOperator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/JAbstractSortedOperator.java @@ -11,7 +11,6 @@ import org.key_project.logic.TermCreationException; import org.key_project.logic.op.AbstractSortedOperator; import org.key_project.logic.op.Modifier; -import org.key_project.logic.op.Operator; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; @@ -20,7 +19,7 @@ * Abstract sorted operator class offering some common functionality. */ public abstract class JAbstractSortedOperator extends AbstractSortedOperator - implements Sorted, Operator { + implements Sorted { protected JAbstractSortedOperator(Name name, ImmutableArray argSorts, Sort sort, ImmutableArray whereToBind, Modifier modifier) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/JOperatorSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/JOperatorSV.java index 98ecfdfd983..b8ae89c1f07 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/JOperatorSV.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/JOperatorSV.java @@ -4,11 +4,9 @@ package de.uka.ilkd.key.logic.op; import org.key_project.logic.Name; -import org.key_project.logic.Named; import org.key_project.logic.Term; import org.key_project.logic.TermCreationException; import org.key_project.logic.op.sv.OperatorSV; -import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; @@ -16,7 +14,7 @@ * Abstract base class for schema variables. */ public abstract class JOperatorSV extends JAbstractSortedOperator - implements OperatorSV, SchemaVariable, Named { + implements OperatorSV { private final boolean isStrict; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java index 3406cbc3ac1..57bfadc61a3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java @@ -5,6 +5,7 @@ import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.ProgramElementName; @@ -16,29 +17,30 @@ * description of the superclass ProgramVariable for more information. */ public final class LocationVariable extends ProgramVariable implements UpdateableOperator { - public LocationVariable(ProgramElementName name, KeYJavaType t, KeYJavaType containingType, + public LocationVariable(ProgramElementName name, TypeReference t, KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost, boolean isFinal) { - super(name, t.getSort(), t, containingType, isStatic, isModel, isGhost, isFinal); + super(name, t.getKeYJavaType().getSort(), t, containingType, isStatic, isModel, isGhost, + isFinal); } - public LocationVariable(ProgramElementName name, KeYJavaType t, KeYJavaType containingType, + public LocationVariable(ProgramElementName name, TypeReference t, KeYJavaType containingType, boolean isStatic, boolean isModel) { - super(name, t.getSort(), t, containingType, isStatic, isModel, false); + super(name, t.getKeYJavaType().getSort(), t, containingType, isStatic, isModel, false); } - public LocationVariable(ProgramElementName name, KeYJavaType t) { - super(name, t.getSort(), t, null, false, false, false); + public LocationVariable(ProgramElementName name, TypeReference t) { + super(name, t.getKeYJavaType().getSort(), t, null, false, false, false); } - public LocationVariable(ProgramElementName name, KeYJavaType t, boolean isFinal) { - super(name, t.getSort(), t, null, false, false, false, isFinal); + public LocationVariable(ProgramElementName name, TypeReference t, boolean isFinal) { + super(name, t.getKeYJavaType().getSort(), t, null, false, false, false, isFinal); } - public LocationVariable(ProgramElementName name, KeYJavaType t, boolean isGhost, + public LocationVariable(ProgramElementName name, TypeReference t, boolean isGhost, boolean isFinal) { - super(name, t.getSort(), t, null, false, false, isGhost, isFinal); + super(name, t.getKeYJavaType().getSort(), t, null, false, false, isGhost, isFinal); } @@ -61,7 +63,7 @@ public void visit(Visitor v) { */ public static LocationVariable fromProgramVariable(ProgramVariable variable, ProgramElementName name) { - return new LocationVariable(name, variable.getKeYJavaType(), variable.getContainerType(), + return new LocationVariable(name, variable.getTypeReference(), variable.getContainerType(), variable.isStatic(), variable.isModel(), variable.isGhost(), variable.isFinal()); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramConstant.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramConstant.java index e07d49745ca..de2dc97452e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramConstant.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramConstant.java @@ -5,6 +5,7 @@ import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.expression.literal.Literal; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.ProgramElementName; @@ -19,13 +20,12 @@ public final class ProgramConstant extends ProgramVariable { // a compile-time constant, null otherwise private final Literal compileTimeConstant; - public ProgramConstant(ProgramElementName name, KeYJavaType t, KeYJavaType containingType, + public ProgramConstant(ProgramElementName name, TypeReference t, KeYJavaType containingType, boolean isStatic, Literal compileTimeConstant) { - super(name, t.getSort(), t, containingType, isStatic, false, false); + super(name, t.getKeYJavaType().getSort(), t, containingType, isStatic, false, false); this.compileTimeConstant = compileTimeConstant; } - /** * @return the value of the initializer as a literal, if this variable is a compile-time * constant, null otherwise @@ -34,7 +34,6 @@ public Literal getCompileTimeConstant() { return compileTimeConstant; } - @Override public void visit(Visitor v) { v.performActionOnProgramConstant(this); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java index f84dcf8a650..ecdb3b8e22a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.Annotation; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.declaration.*; import de.uka.ilkd.key.java.ast.expression.Expression; @@ -105,6 +106,11 @@ public ReferencePrefix getReferencePrefix() { return null; } + @Override + public ImmutableList getAnnotations() { + return ImmutableList.of(); + } + @Override public int getDimensions() { return 0; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java index ee3efad25de..f911f443a77 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java @@ -44,7 +44,7 @@ public abstract class ProgramVariable extends JAbstractSortedOperator ParsableVariable, ReferenceSuffix, ProgramInLogic { public static final Logger LOGGER = LoggerFactory.getLogger(ProgramVariable.class); - private final KeYJavaType type; + private final TypeReference type; private final boolean isStatic; private final boolean isModel; private final boolean isGhost; @@ -54,10 +54,10 @@ public abstract class ProgramVariable extends JAbstractSortedOperator // the program variable denotes a field private final KeYJavaType containingType; - protected ProgramVariable(ProgramElementName name, Sort s, KeYJavaType t, + protected ProgramVariable(ProgramElementName name, Sort s, TypeReference t, KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost, boolean isFinal) { - super(name, s == null ? t.getSort() : s, false); + super(name, s == null ? t.getKeYJavaType().getSort() : s, false); this.type = t; this.containingType = containingType; this.isStatic = isStatic; @@ -70,18 +70,16 @@ protected ProgramVariable(ProgramElementName name, Sort s, KeYJavaType t, assert sort() != JavaDLTheory.UPDATE; } - protected ProgramVariable(ProgramElementName name, Sort s, KeYJavaType t, + protected ProgramVariable(ProgramElementName name, Sort s, TypeReference t, KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost) { this(name, s, t, containingType, isStatic, isModel, isGhost, false); } - /** @return name of the ProgramVariable */ public ProgramElementName getProgramElementName() { return (ProgramElementName) name(); } - /** * returns true iff the program variable has been declared as static */ @@ -89,7 +87,6 @@ public boolean isStatic() { return isStatic; } - /** * returns true iff the program variable has been declared as model */ @@ -104,7 +101,6 @@ public boolean isGhost() { return isGhost; } - /** * returns true iff the program variable has been declared as final */ @@ -112,7 +108,6 @@ public boolean isFinal() { return isFinal; } - /** * returns true iff the program variable is a member */ @@ -120,7 +115,6 @@ public boolean isMember() { return containingType != null; } - /** * returns the KeYJavaType where the program variable is declared or null if the program * variable denotes not a field @@ -129,7 +123,6 @@ public KeYJavaType getContainerType() { return containingType; } - @Override public SourceElement getFirstElement() { return this; @@ -145,19 +138,16 @@ public SourceElement getLastElement() { return this; } - @Override public Comment[] getComments() { return new Comment[0]; } - @Override public void visit(Visitor v) { v.performActionOnProgramVariable(this); } - @Override public Position getStartPosition() { return Position.UNDEFINED; @@ -175,33 +165,29 @@ public PositionInfo getPositionInfo() { return PositionInfo.UNDEFINED; } - @Override - public KeYJavaType getKeYJavaType() { + public TypeReference getTypeReference() { return type; } + @Override + public KeYJavaType getKeYJavaType() { + return type != null ? type.getKeYJavaType() : null; + } @Override public KeYJavaType getKeYJavaType(Services javaServ) { return getKeYJavaType(); } - @Override public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) { return getKeYJavaType(); } - - /** - * We do not have a prefix, so fake it! This way we implement ReferencePrefix - * - * @author VK - */ @Override public ReferencePrefix getReferencePrefix() { - return null; + return type.getReferencePrefix(); } @Override @@ -213,16 +199,15 @@ public Expression convertToProgram(JTerm t, ExtList l) { } } - public String proofToString() { - final Type javaType = type.getJavaType(); + final Type javaType = getKeYJavaType().getJavaType(); final String typeName; if (javaType instanceof ArrayType) { typeName = ((ArrayType) javaType).getAlternativeNameRepresentation(); } else if (javaType != null) { typeName = javaType.getFullName(); } else { - typeName = type.getSort().name().toString(); + typeName = getKeYJavaType().getSort().name().toString(); } return typeName + " " + name() + ";\n"; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/HeapSimplificationMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/HeapSimplificationMacro.java index 4df46543999..27ca065334f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/HeapSimplificationMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/HeapSimplificationMacro.java @@ -63,6 +63,35 @@ public String getDescription() { "wellFormedAnonEQ", "wellFormedMemsetArrayObjectEQ", "wellFormedMemsetArrayPrimitiveEQ", "wellFormedMemsetObjectEQ", "wellFormedMemsetLocSetEQ", "wellFormedMemsetPrimitiveEQ", + // universe rules + "createdRepfpElement", + + "dismissSelectOfDominatedObject", "dismissSelectOfDominatingObject", + "dismissSelectOfDominatedAnon", "dismissSelectOfDominatedCreatedAnon", + + "dismissSelectOfSelfRepfpComplementAnon", "dismissSelectOfSelfCreatedRepfpComplementAnon", + "dismissSelectOfDominatingRepfpComplementAnon", + "dismissSelectOfDominatingCreatedRepfpComplementAnon", + + "dismissSelectOfDominatedObjectEQ", "dismissSelectOfDominatingObjectEQ", + "dismissSelectOfDominatedAnonEQ", "dismissSelectOfDominatedCreatedAnonEQ", + + "dismissSelectOfSelfRepfpComplementAnonEQ", + "dismissSelectOfSelfCreatedRepfpComplementAnonEQ", + "dismissSelectOfDominatingRepfpComplementAnonEQ", + "dismissSelectOfDominatingCreatedRepfpComplementAnonEQ", + + "simplifySelectOfDominatedAnon", "simplifySelectOfDominatedCreatedAnon", + "simplifySelectOfSelfRepfpComplementAnon", "simplifySelectOfSelfCreatedRepfpComplementAnon", + "simplifySelectOfDominatingRepfpComplementAnon", + "simplifySelectOfDominatingCreatedRepfpComplementAnon", + + "simplifySelectOfDominatedAnonEQ", "simplifySelectOfDominatedCreatedAnonEQ", + "simplifySelectOfSelfRepfpComplementAnonEQ", + "simplifySelectOfSelfCreatedRepfpComplementAnonEQ", + "simplifySelectOfDominatingRepfpComplementAnonEQ", + "simplifySelectOfDominatingCreatedRepfpComplementAnonEQ", + // locset rules "elementOfEmpty", "elementOfAllLocs", "elementOfSingleton", "elementOfUnion", "elementOfIntersect", "elementOfSetMinus", "elementOfAllFields", "elementOfAllObjects", diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index 7d608d9c74f..30ffb21695e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -13,6 +13,7 @@ import java.util.List; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.nparser.builder.BuilderHelpers; @@ -245,7 +246,8 @@ public Void visitProofCmd(JmlParser.ProofCmdContext ctx) { if (ctx.obtain != null) { KeYJavaType type = io.translateType(ctx.typespec()); ProgramElementName name = new ProgramElementName(ctx.var.getText()); - collectedVars = collectedVars.prepend(new LocationVariable(name, type, true)); + collectedVars = + collectedVars.prepend(new LocationVariable(name, new TypeRef(type), true)); } return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java index 6567e9b903b..e64857303a1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.LocationVariable; @@ -110,10 +111,10 @@ public Object visitProg_var_decls(JavaKeYParser.Prog_var_declsContext ctx) { // getColumn()) if (!(name instanceof ProgramVariable pv) || !(pv.getKeYJavaType().equals(kjt))) { - programVariables().add(new LocationVariable(pvName, kjt)); + programVariables().add(new LocationVariable(pvName, new TypeRef(kjt))); } } else { - programVariables().add(new LocationVariable(pvName, kjt)); + programVariables().add(new LocationVariable(pvName, new TypeRef(kjt))); } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java index 67065ce497c..442eb07d7f1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java @@ -270,6 +270,12 @@ public VariableCondition build(Object[] arguments, List parameters, new ConstructorBasedBuilder("static", StaticReferenceCondition.class, SV); public static final TacletBuilderCommand DIFFERENT_FIELDS = new ConstructorBasedBuilder("differentFields", DifferentFields.class, SV, SV); + public static final AbstractConditionBuilder ADD_ANNOTATION = + new ConstructorBasedBuilder("addAnnotation", AddAnnotation.class, SV, SV, S); + public static final AbstractConditionBuilder REMOVE_ANNOTATION = + new ConstructorBasedBuilder("removeAnnotation", RemoveAnnotation.class, SV, SV, S); + public static final AbstractConditionBuilder HAS_ANNOTATION = + new ConstructorBasedBuilder("hasAnnotation", HasAnnotationCondition.class, SV, S); public static final AbstractConditionBuilder SAME_OBSERVER = new ConstructorBasedBuilder("sameObserver", SameObserverCondition.class, PV, PV); public static final AbstractConditionBuilder applyUpdateOnRigid = new ConstructorBasedBuilder( @@ -382,7 +388,8 @@ public IsLabeledCondition build(Object[] arguments, List parameters, applyUpdateOnRigid, DROP_EFFECTLESS_ELEMENTARIES, SIMPLIFY_ITE_UPDATE, SUBFORMULAS, STATIC_FIELD, MODEL_FIELD, SUBFORMULA, DROP_EFFECTLESS_STORES, EQUAL_UNIQUE, META_DISJOINT, - IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP); + IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP, + HAS_ANNOTATION, ADD_ANNOTATION, REMOVE_ANNOTATION); register(STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, GET_INVARIANT, GET_FREE_INVARIANT, GET_VARIANT, IS_LABELED); loadWithServiceLoader(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java index 289ab09a240..f8a28675bc9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java @@ -174,7 +174,7 @@ protected static String encodeUnicodeChars(String str) { * * @param list a program element list. */ - protected void writeKeywordList(ImmutableArray list) { + protected void writeKeywordList(ImmutableArray list) { for (int i = 0; i < list.size(); i++) { if (i != 0) { layouter.brk(); @@ -621,8 +621,18 @@ public void performActionOnTypeReference(TypeReference x) { public void performActionOnTypeReference(TypeReference x, boolean fullTypeNames) { if (x.getKeYJavaType() != null && x.getKeYJavaType().getJavaType() instanceof ArrayDeclaration) { + for (Annotation annot : x.getAnnotations()) { + performActionOnAnnotation(annot); + layouter.print(" "); + } + performActionOnArrayDeclaration((ArrayDeclaration) x.getKeYJavaType().getJavaType()); } else if (x.getProgramElementName() != null) { + for (Annotation expr : x.getAnnotations()) { + performActionOnAnnotation(expr); + layouter.print(" "); + } + printTypeReference(x.getReferencePrefix(), x.getKeYJavaType(), x.getProgramElementName(), fullTypeNames); } @@ -740,6 +750,49 @@ public void performActionOnClassDeclaration(ClassDeclaration x) { performActionOnMemberDeclarations(x.getMembers()); } + @Override + public void performActionOnAnnotationInterfaceMemberDeclaration( + AnnotationInterfaceMemberDeclaration x) { + layouter.beginI(); + ImmutableArray mods = x.getModifiers(); + boolean hasMods = mods != null && !mods.isEmpty(); + if (hasMods) { + writeKeywordList(mods); + layouter.print(" "); + } + + performActionOnTypeReference(x.getTypeRef()); + layouter.print(" "); + performActionOnProgramElementName(x.getProgramElementName()); + layouter.end(); + } + + @Override + public void performActionOnAnnotationInterfaceDeclaration(AnnotationInterfaceDeclaration x) { + layouter.beginC(); + layouter.beginC(0); + ImmutableArray mods = x.getModifiers(); + boolean hasMods = mods != null && !mods.isEmpty(); + if (hasMods) { + writeKeywordList(mods); + } + if (x.getProgramElementName() != null) { + if (hasMods) { + layouter.print(" "); + } + layouter.keyWord("@interface").print(" "); + performActionOnProgramElementName(x.getProgramElementName()); + } + layouter.end(); + // not an anonymous class + if (x.getProgramElementName() != null) { + layouter.print(" "); + } + layouter.end(); + + performActionOnMemberDeclarations(x.getMembers()); + } + private void performActionOnMemberDeclarations( @Nullable ImmutableArray members) { if (members != null && !members.isEmpty()) { @@ -1458,6 +1511,7 @@ public void performActionOnNewArray(NewArray x) { if (addParentheses) { layouter.print("("); } + layouter.print("new "); x.getTypeReference().visit(this); @@ -1718,6 +1772,12 @@ public void performActionOnThen(Then x) { handleBlockOrSingleStatement(x.getBody()); } + @Override + public void performActionOnAnnotation(Annotation x) { + layouter.print("@"); + layouter.print(x.getKeyJavaType().getFullName()); + } + @Override public void performActionOnElse(Else x) { layouter.keyWord("else"); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java index c2a5305e33e..09743ec4890 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java @@ -16,6 +16,7 @@ import de.uka.ilkd.key.java.ast.declaration.VariableSpecification; import de.uka.ilkd.key.java.ast.expression.literal.NullLiteral; import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.java.ast.statement.Try; @@ -40,6 +41,8 @@ import com.github.javaparser.ast.key.KeyTransactionStatement; import org.jspecify.annotations.Nullable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; /** *

    @@ -78,6 +81,7 @@ * @author Martin Hentschel */ public abstract class AbstractOperationPO extends AbstractPO { + private static final Logger LOGGER = LoggerFactory.getLogger(AbstractOperationPO.class); private static final String JAVA_LANG_THROWABLE = "java.lang.Throwable"; protected InitConfig proofConfig; @@ -397,7 +401,8 @@ public void readProblem() throws ProofInputException { // prepare variables, program method boolean makeNamesUnique = isMakeNamesUnique(); final ImmutableList paramVars = tb.paramVars(pm, makeNamesUnique); - final LocationVariable selfVar = tb.selfVar(pm, getCalleeKeYJavaType(), makeNamesUnique); + final LocationVariable selfVar = + tb.selfVar(pm, new TypeRef(getCalleeKeYJavaType()), makeNamesUnique); final LocationVariable resultVar = tb.resultVar(pm, makeNamesUnique); final LocationVariable exceptionVar = tb.excVar(pm, makeNamesUnique); @@ -898,7 +903,7 @@ protected JavaBlock buildJavaBlock(ImmutableList formalParVars final KeYJavaType eType = javaInfo.getTypeByClassName(JAVA_LANG_THROWABLE); final TypeReference excTypeRef = javaInfo.createTypeReference(eType); final ProgramElementName ePEN = new ProgramElementName("e"); - final ProgramVariable eVar = new LocationVariable(ePEN, eType); + final ProgramVariable eVar = new LocationVariable(ePEN, new TypeRef(eType)); final StatementBlock sb2; if (exceptionVar == null) { @@ -1009,7 +1014,7 @@ private ImmutableList createFormalParamVars( if (isCopyOfMethodArgumentsUsed()) { ProgramElementName pen = new ProgramElementName("_" + paramVar.name()); LocationVariable formalParamVar = - new LocationVariable(pen, paramVar.getKeYJavaType()); + new LocationVariable(pen, paramVar.getTypeReference()); formalParamVars = formalParamVars.append(formalParamVar); register(formalParamVar, proofServices); } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java index 55a967969b4..83b1de3f4fa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java @@ -31,11 +31,14 @@ import org.key_project.util.collection.ImmutableSet; import org.key_project.util.collection.Pair; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; /** * An abstract proof obligation implementing common functionality. */ public abstract class AbstractPO implements IPersistablePO { + private static final Logger LOGGER = LoggerFactory.getLogger(AbstractPO.class); protected TermBuilder tb; protected final InitConfig environmentConfig; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java index 06d7558df20..d983d1c6f29 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.label.ParameterlessTermLabel; @@ -133,7 +134,8 @@ public void readProblem() throws ProofInputException { // prepare variables final LocationVariable selfVar = - !contract.getTarget().isStatic() ? tb.selfVar(contract.getKJT(), true) : null; + !contract.getTarget().isStatic() ? tb.selfVar(new TypeRef(contract.getKJT()), true) + : null; final ImmutableList paramVars = tb.paramVars(target, true); final boolean twoState = (contract.getTarget().getStateCount() == 2); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java index 4531162a8e3..eb277a42f76 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java @@ -31,6 +31,7 @@ import org.key_project.logic.Name; import org.key_project.logic.op.Function; +import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; import org.key_project.util.java.ArrayUtil; @@ -272,7 +273,8 @@ public void readProblem() { final IProgramMethod pm = getProgramMethod(); final StatementBlock block = getBlock(); - final LocationVariable selfVar = tb.selfVar(pm, getCalleeKeYJavaType(), makeNamesUnique); + final LocationVariable selfVar = + tb.selfVar(pm, new TypeRef(getCalleeKeYJavaType()), makeNamesUnique); register(selfVar, services); final JTerm selfTerm = selfVar == null ? null : tb.var(selfVar); @@ -296,7 +298,7 @@ public void readProblem() { .createAndRegister(selfTerm, false, contract.getBlock()); final ProgramVariable exceptionParameter = KeYJavaASTFactory.localVariable( services.getVariableNamer().getTemporaryNameProposal("e"), - variables.exception.getKeYJavaType()); + variables.exception.getTypeReference()); final ConditionsAndClausesBuilder conditionsAndClausesBuilder = new ConditionsAndClausesBuilder(contract.getAuxiliaryContract(), heaps, variables, @@ -394,7 +396,8 @@ private GoalsConfigurator setUpGoalConfigurator(final StatementBlock block, final BlockContract.Variables variables, final Services services, final TermBuilder tb) { final KeYJavaType kjt = getCalleeKeYJavaType(); - final TypeRef typeRef = new TypeRef(new ProgramElementName(kjt.getName()), 0, selfVar, kjt); + final TypeRef typeRef = new TypeRef(new ProgramElementName(kjt.getName()), + ImmutableList.of(), 0, selfVar, kjt); final ExecutionContext ec = new ExecutionContext(typeRef, getProgramMethod(), selfVar); JModality.JavaModalityKind kind = contract.getModalityKind(); JavaBlock jb = JavaBlock.createJavaBlock(new StatementBlock()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java index 544cd1da17d..821c2c8c8c1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java @@ -31,6 +31,7 @@ import org.key_project.logic.Name; import org.key_project.logic.op.Function; +import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; import org.key_project.util.java.ArrayUtil; @@ -131,7 +132,8 @@ public void readProblem() { contract.replaceEnhancedForVariables(services); - final LocationVariable selfVar = tb.selfVar(pm, getCalleeKeYJavaType(), makeNamesUnique); + final LocationVariable selfVar = + tb.selfVar(pm, new TypeRef(getCalleeKeYJavaType()), makeNamesUnique); register(selfVar, services); final JTerm selfTerm = selfVar == null ? null : tb.var(selfVar); @@ -368,7 +370,8 @@ private GoalsConfigurator createGoalConfigurator(final ProgramVariable selfVar, final TermBuilder tb) { final TermLabelState termLabelState = new TermLabelState(); final KeYJavaType kjt = getCalleeKeYJavaType(); - final TypeRef ref = new TypeRef(new ProgramElementName(kjt.getName()), 0, selfVar, kjt); + final TypeRef ref = new TypeRef(new ProgramElementName(kjt.getName()), + ImmutableList.of(), 0, selfVar, kjt); final ExecutionContext ec = new ExecutionContext(ref, getProgramMethod(), selfVar); // TODO (DD): HACK @@ -413,7 +416,7 @@ private JTerm setUpValidityGoal(final JTerm selfTerm, final List */ public class FunctionalOperationContractPO extends AbstractOperationPO implements ContractPO { + private static final Logger LOGGER = + LoggerFactory.getLogger(FunctionalOperationContractPO.class); public static final Map TRANSACTION_TAGS = new LinkedHashMap<>(); @@ -150,7 +154,7 @@ protected ImmutableList buildOperationBlocks( // construct what would be produced from rule instanceCreationAssignment final Expression init = (Expression) (new CreateObject(n)).transform(n, services, svInst)[0]; - final Statement assignTmp = declare(selfVar, init, type); + final Statement assignTmp = declare(selfVar, init, new TypeRef(type)); result[0] = new StatementBlock(assignTmp); // try block diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java index aeb778dd272..c3814644b5b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java @@ -16,6 +16,7 @@ import de.uka.ilkd.key.java.ast.declaration.ClassDeclaration; import de.uka.ilkd.key.java.ast.declaration.modifier.Private; import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.java.ast.statement.LoopStatement; import de.uka.ilkd.key.java.ast.statement.MergePointStatement; import de.uka.ilkd.key.logic.*; @@ -873,7 +874,7 @@ public synchronized ImmutableSet getClassAxioms(KeYJavaType selfKjt) continue; // only non-private classes } final ImmutableSet myInvs = getClassInvariants(kjt); - final LocationVariable selfVar = tb.selfVar(kjt, false); + final LocationVariable selfVar = tb.selfVar(new TypeRef(kjt), false); JTerm invDef = tb.tt(); JTerm staticInvDef = tb.tt(); @@ -965,7 +966,8 @@ private ImmutableSet getModelMethodAxioms() { ImmutableSet result = DefaultImmutableSet.nil(); for (KeYJavaType kjt : services.getJavaInfo().getAllKeYJavaTypes()) { for (IProgramMethod pm : services.getJavaInfo().getAllProgramMethods(kjt)) { - final LocationVariable selfVar = pm.isStatic() ? null : tb.selfVar(kjt, false); + final LocationVariable selfVar = + pm.isStatic() ? null : tb.selfVar(new TypeRef(kjt), false); if (!pm.isVoid() && pm.isModel()) { pm = services.getJavaInfo().getToplevelPM(kjt, pm); ImmutableList paramVars = tb.paramVars(pm, false); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java index 790dafb48d8..4f09f6028f7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java @@ -7,8 +7,8 @@ import de.uka.ilkd.key.java.KeYJavaASTFactory; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.*; -import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.JTerm; @@ -139,14 +139,14 @@ protected static JTerm createLocalAnonUpdate(ImmutableSet loca /** * * @param nameBase a base name. - * @param type a type. + * @param typeRef a {@link TypeReference}. * @param services services. * @return a new local variable with the specified base name of the specified type. */ protected static LocationVariable createLocalVariable(final String nameBase, - final KeYJavaType type, final Services services) { + final TypeReference typeRef, final Services services) { return KeYJavaASTFactory.localVariable( - services.getVariableNamer().getTemporaryNameProposal(nameBase), type); + services.getVariableNamer().getTemporaryNameProposal(nameBase), typeRef); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java index 950134bfca8..0b41254be4f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java @@ -195,7 +195,8 @@ protected static JTerm createBeforeLoopUpdate(Services services, for (ProgramVariable pv : localOuts) { final String pvBeforeLoopName = tb.newName(pv.name() + "Before_LOOP"); final LocationVariable pvBeforeLoop = - new LocationVariable(new ProgramElementName(pvBeforeLoopName), pv.getKeYJavaType()); + new LocationVariable(new ProgramElementName(pvBeforeLoopName), + pv.getTypeReference()); progVarNS.addSafely(pvBeforeLoop); beforeLoopUpdate = tb.parallel(beforeLoopUpdate, tb.elementary(pvBeforeLoop, tb.var(pv))); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java index 00b8a0cd7ab..a6ce4d5ebd1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java @@ -17,6 +17,8 @@ import de.uka.ilkd.key.java.ast.expression.literal.*; import de.uka.ilkd.key.java.ast.expression.literal.BooleanLiteral; import de.uka.ilkd.key.java.ast.expression.operator.NotEquals; +import de.uka.ilkd.key.java.ast.reference.TypeRef; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.java.ast.statement.Catch; import de.uka.ilkd.key.java.ast.statement.LabeledStatement; @@ -178,7 +180,7 @@ private void declareFlagsFalse() { statements.add(KeYJavaASTFactory.assign(flag, BooleanLiteral.FALSE)); } else { statements.add(KeYJavaASTFactory.declare(flag, BooleanLiteral.FALSE, - services.getJavaInfo().getKeYJavaType("boolean"))); + new TypeRef(services.getJavaInfo().getKeYJavaType("boolean")))); } } @@ -187,7 +189,7 @@ private void declareFlagsFalse() { statements.add(KeYJavaASTFactory.assign(flag, BooleanLiteral.FALSE)); } else { statements.add(KeYJavaASTFactory.declare(flag, BooleanLiteral.FALSE, - services.getJavaInfo().getKeYJavaType("boolean"))); + new TypeRef(services.getJavaInfo().getKeYJavaType("boolean")))); } } if (variables.returnFlag != null) { @@ -196,7 +198,8 @@ private void declareFlagsFalse() { KeYJavaASTFactory.assign(variables.returnFlag, BooleanLiteral.FALSE)); } else { statements.add(KeYJavaASTFactory.declare(variables.returnFlag, - BooleanLiteral.FALSE, services.getJavaInfo().getKeYJavaType("boolean"))); + BooleanLiteral.FALSE, + new TypeRef(services.getJavaInfo().getKeYJavaType("boolean")))); } } } @@ -212,9 +215,9 @@ private void declareResultDefault() { statements.add( KeYJavaASTFactory.assign(variables.result, resultType.getDefaultValue())); } else { - KeYJavaType resultType = variables.result.getKeYJavaType(); + TypeReference resultType = variables.result.getTypeReference(); statements.add(KeYJavaASTFactory.declare(variables.result, - resultType.getDefaultValue(), resultType)); + resultType.getKeYJavaType().getDefaultValue(), resultType)); } } } @@ -236,7 +239,7 @@ private void declareExceptionNull() { statements.add(KeYJavaASTFactory.assign(variables.exception, NullLiteral.NULL)); } else { statements.add(KeYJavaASTFactory.declare(variables.exception, NullLiteral.NULL, - variables.exception.getKeYJavaType())); + variables.exception.getTypeReference())); } } @@ -292,7 +295,7 @@ private Statement wrapInTryCatch(final Statement labeledBlock, final ProgramVariable exceptionParameter) { Catch katch = KeYJavaASTFactory.catchClause( KeYJavaASTFactory.parameterDeclaration(services.getJavaInfo(), - exceptionParameter.getKeYJavaType(), exceptionParameter), + exceptionParameter.getTypeReference(), exceptionParameter), new StatementBlock( KeYJavaASTFactory.assign(variables.exception, exceptionParameter))); return new Try(new StatementBlock(labeledBlock), new Branch[] { katch }); @@ -440,7 +443,7 @@ private Map appendSuffix(final Map String newName = services.getTermBuilder().newName(value.name() + suffix); LocationVariable newValue = - new LocationVariable(new ProgramElementName(newName), value.getKeYJavaType()); + new LocationVariable(new ProgramElementName(newName), value.getTypeReference()); result.put(key, newValue); } @@ -490,7 +493,7 @@ private LocationVariable createAndRegisterVariable( String newName = services.getTermBuilder().newName(placeholderVariable.name().toString()); LocationVariable newVariable = new LocationVariable(new ProgramElementName(newName), - placeholderVariable.getKeYJavaType()); + placeholderVariable.getTypeReference()); if (goal != null) { goal.addProgramVariable(newVariable); @@ -1190,14 +1193,15 @@ public GoalsConfigurator(final AbstractAuxiliaryContractBuiltInRuleApp applicati */ private static LocationVariable[] createLoopVariables(final Services services) { LocationVariable conditionVariable = AbstractAuxiliaryContractRule.createLocalVariable( - "cond", services.getJavaInfo().getKeYJavaType("boolean"), services); + "cond", new TypeRef(services.getJavaInfo().getKeYJavaType("boolean")), services); LocationVariable brokeLoopVariable = AbstractAuxiliaryContractRule.createLocalVariable( - "brokeLoop", services.getJavaInfo().getKeYJavaType("boolean"), services); + "brokeLoop", new TypeRef(services.getJavaInfo().getKeYJavaType("boolean")), + services); LocationVariable continuedLoopVariable = AbstractAuxiliaryContractRule.createLocalVariable("continuedLoop", - services.getJavaInfo().getKeYJavaType("boolean"), services); + new TypeRef(services.getJavaInfo().getKeYJavaType("boolean")), services); final LocationVariable[] loopVariables = { conditionVariable, brokeLoopVariable, continuedLoopVariable }; return loopVariables; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java index 4dacc71a2db..e94f13a7261 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java @@ -322,7 +322,7 @@ protected void setUpValidityGoal(final ImmutableList result, final Services services) { Goal validityGoal = result.tail().tail().head(); final ProgramVariable exceptionParameter = - createLocalVariable("e", variables.exception.getKeYJavaType(), services); + createLocalVariable("e", variables.exception.getTypeReference(), services); configurator.setUpValidityGoal(validityGoal, new JTerm[] { updates[0], updates[1] }, preconditions, new JTerm[] { assumptions[0], frameCondition }, exceptionParameter, conditionsAndClausesBuilder.terms); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalRule.java index ad03ac20f4e..3d3366e7fd4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalRule.java @@ -328,7 +328,7 @@ public LoopContractInternalBuiltInRuleApp createApp(final PosInOccurrence occurr configurator.setUpUsageGoal(result.head(), updates, ArrayUtil.add(usageAssumptions, freePostcondition)); final LocationVariable exceptionParameter = - createLocalVariable("e", vars[0].exception.getKeYJavaType(), services); + createLocalVariable("e", vars[0].exception.getTypeReference(), services); configurator.setUpLoopValidityGoal(goal, contract, context, updates[1], nextRemembranceUpdate, anonOutHeaps, modifiableClauses, freeModifiableClauses, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java index 9a1a248c4e6..3fe1b72ff3c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.java.ast.Statement; import de.uka.ilkd.key.java.ast.StatementBlock; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.java.ast.statement.LabeledStatement; import de.uka.ilkd.key.java.ast.statement.LoopScopeBlock; import de.uka.ilkd.key.java.ast.statement.While; @@ -249,7 +250,8 @@ private ProgramVariable loopScopeIdxVar(Services services) { final ProgramVariable loopScopeIdxVar = // KeYJavaASTFactory.localVariable( // - services.getVariableNamer().getTemporaryNameProposal("x"), booleanType); + services.getVariableNamer().getTemporaryNameProposal("x"), + new TypeRef(booleanType)); return loopScopeIdxVar; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java b/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java index acaa6663159..e68453a6f12 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java @@ -165,12 +165,14 @@ public Pair queryEvalTerm(Services services, JTerm query, callee = null; offset = 0; } else { - callee = new LocationVariable(new ProgramElementName(calleeName), calleeType); + callee = + new LocationVariable(new ProgramElementName(calleeName), new TypeRef(calleeType)); offset = 1; } final ProgramVariable result = - new LocationVariable(new ProgramElementName(progResultName), progResultType); + new LocationVariable(new ProgramElementName(progResultName), + new TypeRef(progResultType)); final MethodReference mr = @@ -206,7 +208,7 @@ public Pair queryEvalTerm(Services services, JTerm query, ArrayList stmnt = new ArrayList<>(); - stmnt.add(KeYJavaASTFactory.declare(result, progResultType)); + stmnt.add(KeYJavaASTFactory.declare(result, new TypeRef(progResultType))); final CopyAssignment assignment = new CopyAssignment(result, mr); @@ -264,7 +266,7 @@ private ImmutableArray getRegisteredArgumentVariables( final String newName = services.getTermBuilder().newName(baseName); final ProgramElementName argVarName = new ProgramElementName(newName); args[i] = new LocationVariable(argVarName, - pdecl.getVariableSpecification().getProgramVariable().getKeYJavaType()); + pdecl.getVariableSpecification().getProgramVariable().getTypeReference()); progvarsNS.addSafely(args[i]); i++; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java index e2fbc3746ab..b45323806a2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java @@ -12,6 +12,7 @@ import de.uka.ilkd.key.java.ast.ProgramElement; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.ClashFreeSubst.VariableCollectVisitor; @@ -1164,13 +1165,13 @@ public ProgramElement getProgramElement(String instantiation, ProgramSV sv, } else if (svSort == ProgramSVSort.VARIABLE) { final NewVarcond nvc = (NewVarcond) taclet.varDeclaredNew(sv); if (nvc != null) { - KeYJavaType kjt; + TypeReference typeRef; Object o = nvc.getTypeDefiningObject(); if (o instanceof SchemaVariable peerSV) { final TypeConverter tc = services.getTypeConverter(); final Object peerInst = instantiations().getInstantiation(peerSV); if (peerInst instanceof TypeReference) { - kjt = ((TypeReference) peerInst).getKeYJavaType(); + typeRef = (TypeReference) peerInst; } else { Expression peerInstExpr; if (peerInst instanceof JTerm peerTerm) { @@ -1178,14 +1179,14 @@ public ProgramElement getProgramElement(String instantiation, ProgramSV sv, } else { peerInstExpr = (Expression) peerInst; } - kjt = tc.getKeYJavaType(peerInstExpr, - instantiations().getContextInstantiation().activeStatementContext()); + typeRef = new TypeRef(tc.getKeYJavaType(peerInstExpr, + instantiations().getContextInstantiation().activeStatementContext())); } } else { - kjt = (KeYJavaType) o; + typeRef = new TypeRef((KeYJavaType) o); } - assert kjt != null : "could not find kjt for: " + o; - return new LocationVariable(VariableNamer.parseName(instantiation), kjt); + assert typeRef != null : "could not find TypeReference for: " + o; + return new LocationVariable(VariableNamer.parseName(instantiation), typeRef); } } return null; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java index 6bfb360d7f2..3b6e5b9d64e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java @@ -143,13 +143,14 @@ private static Pair getMethodCall(Java } } - private static KeYJavaType getStaticPrefixType(MethodOrConstructorReference mr, + private static TypeReference getStaticPrefixType(MethodOrConstructorReference mr, Services services, ExecutionContext ec) { if (mr instanceof MethodReference) { - return ((MethodReference) mr).determineStaticPrefixType(services, ec); + return new TypeRef( + ((MethodReference) mr).determineStaticPrefixType(services, ec)); } else { New n = (New) mr; - return n.getKeYJavaType(services, ec); + return n.getTypeReference(); } } @@ -231,7 +232,8 @@ public static ImmutableSet getApplicableContracts( } // there must be applicable contracts for the operation - return getApplicableContracts(services, inst.pm, inst.staticType, inst.modality.kind()); + return getApplicableContracts(services, inst.pm, inst.staticType.getKeYJavaType(), + inst.modality.kind()); } /** @@ -436,9 +438,9 @@ public static StatementBlock replaceStatement(JavaBlock jb, StatementBlock repla } // collect further information - final KeYJavaType staticType = getStaticPrefixType(mr, services, ec); + final TypeReference staticType = getStaticPrefixType(mr, services, ec); assert staticType != null; - final IProgramMethod pm = getProgramMethod(mr, staticType, ec, services); + final IProgramMethod pm = getProgramMethod(mr, staticType.getKeYJavaType(), ec, services); assert pm != null : "Getting program method failed.\nReference: " + mr + ", static type: " + staticType + ", execution context: " + ec; final JTerm actualSelf = getActualSelf(mr, pm, ec, services); @@ -476,8 +478,8 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) { // there must be applicable contracts for the operation final ImmutableSet contracts = - getApplicableContracts(goal.proof().getServices(), inst.pm, inst.staticType, - inst.modality.kind()); + getApplicableContracts(goal.proof().getServices(), inst.pm, + inst.staticType.getKeYJavaType(), inst.modality.kind()); if (contracts.isEmpty()) { return false; } @@ -538,7 +540,7 @@ public String toString() { */ public record Instantiation(JTerm u, JTerm progPost, JModality modality, Expression actualResult, JTerm actualSelf, - KeYJavaType staticType, MethodOrConstructorReference mr, IProgramMethod pm, + TypeReference staticType, MethodOrConstructorReference mr, IProgramMethod pm, ImmutableList actualParams, boolean transaction) { /** * Creates a new instantiation for the contract rule and the given variables. @@ -818,8 +820,8 @@ public UseOperationContractRuleApplier(Goal goal, RuleApp ruleApp) { excNull = tb.equals(tb.var(excVar), tb.NULL()); excCreated = tb.created(tb.var(excVar)); - freePost = getFreePost(heapContext, inst.pm, inst.staticType, contractResult, - contractSelf, atPres, freeSpecPost, services); + freePost = getFreePost(heapContext, inst.pm, inst.staticType.getKeYJavaType(), + contractResult, contractSelf, atPres, freeSpecPost, services); freeExcPost = inst.pm.isConstructor() ? freePost : tb.tt(); postAssumption = tb.applySequential(new JTerm[] { inst.u, atPreUpdates }, tb.and(anonAssumption, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java index ba6d0d0c1c2..e4cea5f3c61 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java @@ -301,7 +301,7 @@ public WhileInvariantRuleApplier(Goal goal, LoopInvariantBuiltInRuleApp ruleA final String pvBeforeLoopName = tb.newName(pv.name() + "Before_LOOP"); final LocationVariable pvBeforeLoop = new LocationVariable(new ProgramElementName(pvBeforeLoopName), - pv.getKeYJavaType()); + pv.getTypeReference()); services.getNamespaces().programVariables().addSafely(pvBeforeLoop); beforeLoopUpdate = tb.parallel(beforeLoopUpdate, tb.elementary(pvBeforeLoop, tb.var(pv))); @@ -606,7 +606,8 @@ protected Guard prepareGuard(final Instantiation inst, final TermServices services) { final TermBuilder tb = services.getTermBuilder(); final ProgramElementName guardVarName = new ProgramElementName(tb.newName("b")); - final LocationVariable guardVar = new LocationVariable(guardVarName, booleanKJT); + final LocationVariable guardVar = + new LocationVariable(guardVarName, new TypeRef(booleanKJT)); services.getNamespaces().programVariables().addSafely(guardVar); loopRuleApp.setGuard(tb.var(guardVar)); final VariableSpecification guardVarSpec = diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AddAnnotation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AddAnnotation.java new file mode 100644 index 00000000000..184af071928 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AddAnnotation.java @@ -0,0 +1,160 @@ +/* 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.rule.conditions; + +import java.util.Arrays; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.Annotation; +import de.uka.ilkd.key.java.ast.annotation.MarkerAnnotation; +import de.uka.ilkd.key.java.ast.expression.operator.New; +import de.uka.ilkd.key.java.ast.reference.TypeRef; +import de.uka.ilkd.key.java.ast.reference.TypeReference; +import de.uka.ilkd.key.logic.op.LocationVariable; +import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.logic.sort.ProgramSVSort; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.logic.sort.Sort; +import org.key_project.prover.rules.VariableCondition; +import org.key_project.prover.rules.instantiation.MatchResultInfo; + +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + + +/** + * This variable condition can be used to create a copy of a {@link SchemaVariable} + * that has an additional {@link Annotation} in its {@link TypeReference}. + * + * @author Daniel Grévent + */ +public final class AddAnnotation implements VariableCondition { + private static final Logger LOGGER = LoggerFactory.getLogger(AddAnnotation.class); + private static final Sort[] ALLOWED = { + ProgramSVSort.SIMPLE_NEW, + ProgramSVSort.LOCALVARIABLE, ProgramSVSort.VARIABLE + }; + + private final SchemaVariable read, store; + private final String annot; + + /** + * create an instance of the variable condition. + * + * @param store the {@link SchemaVariable} in which the new copy is stored + * @param read the {@link SchemaVariable} that gets copied + * @param annot the fully qualified name of the {@link Annotation} to add + * + * @throws IllegalArgumentException if `read` is not one of the {@link Sort}s + * in the `ALLOWED` array or the {@link Sort} of write is not compatible with + * that of `read`, so they do not correspond to the same kind of AST type. + */ + public AddAnnotation(SchemaVariable store, SchemaVariable read, String annot) { + if (!equivalent(store.sort(), read.sort())) { + throw new IllegalArgumentException( + "Expected left and right to have an equivalent sort!"); + } + + if (!Arrays.stream(ALLOWED).anyMatch(read.sort()::equals)) { + throw new IllegalArgumentException( + "Unsupported sort: " + read.sort() + ", supported: " + + Arrays.stream(ALLOWED).map(s -> s.toString()).reduce("", + (a, b) -> a + " " + b)); + } + + this.read = read; + this.store = store; + this.annot = annot; + } + + /* + * check that two sorts that are part of `ALLOWED` are correspond to a same + * underlying type + */ + private static boolean equivalent(Sort a, Sort b) { + if (a == b) + return true; + if (a == ProgramSVSort.VARIABLE && b == ProgramSVSort.LOCALVARIABLE + || b == ProgramSVSort.VARIABLE && a == ProgramSVSort.LOCALVARIABLE) + return true; + + return false; + } + + @Override + public MatchResultInfo check(@Nullable SchemaVariable var, + @Nullable SyntaxElement instCandidate, + @NonNull MatchResultInfo matchCond, @NonNull LogicServices logicServices) { + + final var svInst = (SVInstantiations) matchCond.getInstantiations(); + + if (svInst.getInstantiation(store) != null || + svInst.getInstantiation(read) == null) { + return matchCond; + } + + Object inst = svInst.getInstantiation(read); + + Annotation annotation = build((Services) logicServices); + if (inst instanceof ProgramVariable variable) { + TypeReference tRef = addAnnotation(variable.getTypeReference(), annotation); + LocationVariable replacement = newFromTypeRef( + variable, (Services) logicServices, tRef); + + return matchCond.setInstantiations( + svInst.add(store, replacement, logicServices)); + } else if (inst instanceof New cons) { + TypeReference tRef = addAnnotation(cons.getTypeReference(), annotation); + New replacement = newFromTypeRef(cons, tRef); + + return matchCond.setInstantiations( + svInst.add(store, replacement, logicServices)); + } + + return matchCond; + } + + private Annotation build(Services services) { + return new MarkerAnnotation(services.getJavaInfo().getTypeByName(annot)); + } + + private static TypeReference addAnnotation(TypeReference tRef, Annotation annotation) { + return new TypeRef( + tRef.getProgramElementName(), + tRef.getAnnotations().append(annotation), + tRef.getDimensions(), + tRef.getReferencePrefix(), + tRef.getKeYJavaType()); + } + + private static LocationVariable newFromTypeRef(ProgramVariable v, Services services, + TypeReference tRef) { + return new LocationVariable( + services.getVariableNamer().getTemporaryNameProposal(v.name().toString()), + tRef, + v.getContainerType(), + v.isStatic(), + v.isModel(), v.isGhost(), v.isFinal()); + } + + private static New newFromTypeRef(New n, TypeReference tRef) { + return new New( + n.getPositionInfo(), + Arrays.asList(n.getComments()), + n.getArguments(), + tRef, + n.getClassDeclaration()); + } + + @Override + public String toString() { + return "\\addAnnotation(" + store + ", " + read + ", " + annot + ")"; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasAnnotationCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasAnnotationCondition.java new file mode 100644 index 00000000000..26332b039c3 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasAnnotationCondition.java @@ -0,0 +1,127 @@ +/* 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.rule.conditions; + +import java.util.Arrays; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.Field; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.declaration.*; +import de.uka.ilkd.key.java.ast.expression.operator.New; +import de.uka.ilkd.key.java.ast.reference.TypeReference; +import de.uka.ilkd.key.ldt.HeapLDT; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.logic.sort.ProgramSVSort; +import de.uka.ilkd.key.rule.VariableConditionAdapter; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.op.Function; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.logic.sort.Sort; +import org.key_project.util.collection.ImmutableList; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * This variable condition can be used to check if the {@link TypeReference} of a + * {@link SchemaVariable} contains a specific {@link Annotation}. + * + * @author Daniel Grévent + */ +public final class HasAnnotationCondition extends VariableConditionAdapter { + private static final Logger LOGGER = LoggerFactory.getLogger(HasAnnotationCondition.class); + + private static final Sort[] ALLOWED = { + ProgramSVSort.SIMPLE_NEW, + ProgramSVSort.LOCALVARIABLE, ProgramSVSort.VARIABLE, + }; + + private final SchemaVariable variable; + private final String annot; + + /** + * create an instance of the variable condition. + * + * @param variable the variable whos {@link TypeReference} is to check for + * {@link Annotation}s. + * @param annot the fully qualified name of the {@link Annotation} to check for + * + * @throws IllegalArgumentException if `variable` is not one of the {@link Sort}s + * in the `ALLOWED` array or the {@link Sort} has the name `Field`. + */ + public HasAnnotationCondition(SchemaVariable variable, String annot) { + if (!Arrays.stream(ALLOWED).anyMatch(variable.sort()::equals) && + !variable.sort().toString().equals("Field")) { + throw new IllegalArgumentException( + "Unsupported sort: " + variable.sort() + ", supported: " + + Arrays.stream(ALLOWED).map(s -> s.toString()).reduce("", + (a, b) -> a + " " + b)); + } + + this.variable = variable; + this.annot = annot; + } + + @Override + public boolean check(SchemaVariable var, SyntaxElement subst, + SVInstantiations svInst, Services services) { + + if (var != variable) + return true; + + Object inst = svInst.getInstantiation(variable); + + if (inst instanceof New n) { + return matchesTypeAnnots(n.getTypeReference()); + } else if (inst instanceof ProgramVariable variable) { + return matchesTypeAnnots(variable.getTypeReference()); + } else if (inst instanceof JTerm term && + term.op().arity() == 0 && + term.op() instanceof Function func) { + return matchesTypeAnnots(getFieldType(services, func)); + } + + return false; + } + + private TypeReference getFieldType(Services services, Function op) { + HeapLDT.SplitFieldName name = HeapLDT.trySplitFieldName(op); + + if (name == null) + return null; + + KeYJavaType classType = services.getJavaInfo().getTypeByName(name.className()); + + if (classType != null + && classType.getJavaType() instanceof ClassDeclaration classDecl) { + ImmutableList fields = classDecl.getAllFields(services); + + return fields.stream() + .filter(f -> f.getName().split("::")[1].equals(name.attributeName())) + .findFirst() + .map(f -> f.getProgramVariable().getTypeReference()) + .orElse(null); + } + + + return null; + } + + private boolean matchesTypeAnnots(TypeReference typeRef) { + if (typeRef == null) + return false; + + return typeRef.getAnnotations().stream() + .anyMatch(a -> a.getKeyJavaType().getFullName().equals(annot)); + } + + @Override + public String toString() { + return "\\hasAnnotation(" + variable + ", " + annot + ")"; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java index 39cb9991e3d..46dddd94b29 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java @@ -11,9 +11,8 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.ProgramElement; import de.uka.ilkd.key.java.ast.Statement; -import de.uka.ilkd.key.java.ast.abstraction.*; import de.uka.ilkd.key.java.ast.declaration.*; -import de.uka.ilkd.key.java.ast.reference.TypeRef; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.TermBuilder; @@ -98,14 +97,10 @@ public MatchResultInfo check(SchemaVariable var, SyntaxElement instCandidate, // mismatch (e.g. k_before#0 vs. k_before#1) breaks the slicing mechanism, which // relies on formula equivalence across reloads. See issue #3834. final var newName = uniqueBeforeName(v.name() + "_before", services, reserved); - KeYJavaType type = v.getKeYJavaType(); - var locVar = new LocationVariable(newName, type); + TypeReference typeRef = v.getTypeReference(); + var locVar = new LocationVariable(newName, typeRef); var spec = new VariableSpecification(locVar); - int dim = 0; - if (type.getJavaType() instanceof ArrayType at) { - dim = at.getDimension(); - } - decls.add(new LocalVariableDeclaration(new TypeRef(type, dim), spec)); + decls.add(new LocalVariableDeclaration(typeRef, spec)); updatesBefore = updatesBefore.append(tb.elementary(tb.var(locVar), tb.var(v))); updatesFrame = updatesFrame.append(tb.elementary(tb.var(v), tb.var(locVar))); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/RemoveAnnotation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/RemoveAnnotation.java new file mode 100644 index 00000000000..8d3ed2f5104 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/RemoveAnnotation.java @@ -0,0 +1,121 @@ +/* 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.rule.conditions; + +import java.util.Arrays; + +import de.uka.ilkd.key.java.ast.Annotation; +import de.uka.ilkd.key.java.ast.expression.operator.New; +import de.uka.ilkd.key.java.ast.reference.TypeRef; +import de.uka.ilkd.key.java.ast.reference.TypeReference; +import de.uka.ilkd.key.logic.sort.ProgramSVSort; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.logic.sort.Sort; +import org.key_project.prover.rules.VariableCondition; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + + +/** + * This variable condition can be used to create a copy of a {@link SchemaVariable} + * that has all instances of an {@link Annotation} removed from its + * {@link TypeReference}. + * + * @author Daniel Grévent + */ +public final class RemoveAnnotation implements VariableCondition { + private static final Logger LOGGER = LoggerFactory.getLogger(RemoveAnnotation.class); + + private static final Sort[] ALLOWED = { ProgramSVSort.SIMPLE_NEW }; + + private final SchemaVariable read, store; + private final String annot; + + /** + * create an instance of the variable condition. + * + * @param store the {@link SchemaVariable} in which the new copy is stored + * @param read the {@link SchemaVariable} that gets copied + * @param annot the fully qualified name of the {@link Annotation} to remove + * + * @throws IllegalArgumentException if `read` is not one of the {@link Sort}s in the + * `ALLOWED` array or the {@link Sort} of write is not the same as to {@link Sort} + * of `read`, so they do not correspond to the same kind of AST type. + */ + public RemoveAnnotation(SchemaVariable store, SchemaVariable read, String annot) { + if (!store.sort().equals(read.sort())) { + throw new RuntimeException("Expected left and right to have the same sort!"); + } + + if (!Arrays.stream(ALLOWED).anyMatch(read.sort()::equals)) { + throw new RuntimeException( + "Unsupported sort: " + read.sort() + ", supported: " + + Arrays.stream(ALLOWED).map(s -> s.toString()).reduce("", + (a, b) -> a + " " + b)); + } + + this.read = read; + this.store = store; + this.annot = annot; + } + + @Override + public MatchResultInfo check(@Nullable SchemaVariable var, + @Nullable SyntaxElement instCandidate, + @NonNull MatchResultInfo matchCond, @NonNull LogicServices logicServices) { + + final var svInst = (SVInstantiations) matchCond.getInstantiations(); + + if (svInst.getInstantiation(store) != null || + svInst.getInstantiation(read) == null) { + return matchCond; + } + + if (svInst.getInstantiation(read) instanceof New n) { + TypeReference tRef = removeAnnotation(n.getTypeReference()); + New replacement = newFromTypeRef(n, tRef); + + return matchCond.setInstantiations( + svInst.add(store, replacement, logicServices)); + } + + return matchCond; + } + + private TypeReference removeAnnotation(TypeReference tRef) { + Annotation[] filtered = tRef.getAnnotations() + .stream() + .filter(a -> !a.getKeyJavaType().getFullName().equals(annot)) + .toArray(Annotation[]::new); + + return new TypeRef( + tRef.getProgramElementName(), + ImmutableList.of(filtered), tRef.getDimensions(), + tRef.getReferencePrefix(), + tRef.getKeYJavaType()); + } + + private static New newFromTypeRef(New n, TypeReference tRef) { + return new New( + n.getPositionInfo(), + Arrays.asList(n.getComments()), + n.getArguments(), + tRef, + n.getClassDeclaration()); + } + + @Override + public String toString() { + return "\\addAnnotation(" + store + ", " + read + ", " + annot + ")"; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramSVInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramSVInstruction.java index 59ab748a117..b07f3ba92ac 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramSVInstruction.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramSVInstruction.java @@ -108,4 +108,9 @@ protected MatchResultInfo match(JTerm instantiationCandidate, MatchResultInfo mc } return null; } + + @Override + public String toString() { + return "MatchProgramSVInstruction"; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchTermLabelInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchTermLabelInstruction.java index 051cb016ce6..6606fd1e90d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchTermLabelInstruction.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchTermLabelInstruction.java @@ -72,4 +72,9 @@ public MatchResultInfo match(SyntaxElement actualElement, MatchResultInfo matchC return result; } + @Override + public String toString() { + return "MatchTermLabelInstruction"; + } + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchVariableSVInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchVariableSVInstruction.java index 0496eb4f4b8..491b7ce8100 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchVariableSVInstruction.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchVariableSVInstruction.java @@ -35,5 +35,4 @@ protected MatchResultInfo match(JTerm instantiationCandidate, MatchResultInfo mc } return null; } - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayPostDecl.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayPostDecl.java index 4d332418ce1..1162c798325 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayPostDecl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayPostDecl.java @@ -43,6 +43,7 @@ public ProgramElement[] transform(ProgramElement pe, Services services, return new ProgramElement[] { KeYJavaASTFactory.declare(modifiers, variable, var.getInitializer(), originalTypeReference.getProgramElementName(), originalTypeReference.getDimensions() + var.getDimensions(), + originalTypeReference.getAnnotations(), originalTypeReference.getReferencePrefix(), variable.getKeYJavaType()) }; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnhancedForElimination.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnhancedForElimination.java index 7a3bafe873a..fc558d01217 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnhancedForElimination.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnhancedForElimination.java @@ -193,14 +193,15 @@ private ProgramElement makeArrayForLoop(EnhancedFor enhancedFor, TransformationD final JavaInfo ji = services.getJavaInfo(); // T[] arr = exp; - final KeYJavaType arrayType = expression.getKeYJavaType(services, data.execContext()); + final TypeReference arrayType = + new TypeRef(expression.getKeYJavaType(services, data.execContext())); final ProgramVariable arrayVar = KeYJavaASTFactory.localVariable(services, ARR, arrayType); final Statement arrAssignment = KeYJavaASTFactory.declare(arrayVar, expression); data.setHead(KeYJavaASTFactory.block(arrAssignment)); // for(int i; i < arr.length; i++) - final KeYJavaType intType = ji.getPrimitiveKeYJavaType("int"); + final TypeReference intType = new TypeRef(ji.getPrimitiveKeYJavaType("int")); data.setIndexVariable(KeYJavaASTFactory.localVariable(services, INDEX, intType)); final ILoopInit inits = KeYJavaASTFactory.loopInitZero(intType, data.indexVariable()); final IGuard guard = @@ -243,13 +244,13 @@ private ProgramElement makeIterableForLoop(EnhancedFor enhancedFor, Transformati ImmutableList.nil(), data.execContext().getTypeReference().getKeYJavaType()); // local variable "it" - final KeYJavaType iteratorType = iteratorMethod.getReturnType(); + final TypeReference iteratorType = new TypeRef(iteratorMethod.getReturnType()); ProgramVariable iteratorVariable = KeYJavaASTFactory.localVariable(services, IT, iteratorType); // local variable "values" - final KeYJavaType seqType = - services.getTypeConverter().getKeYJavaType(PrimitiveType.JAVA_SEQ); + final TypeReference seqType = + new TypeRef(services.getTypeConverter().getKeYJavaType(PrimitiveType.JAVA_SEQ)); data.setValuesVariable(KeYJavaASTFactory.localVariable(services, VALUES, seqType)); // ghost \seq values = \seq_empty diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EvaluateArgs.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EvaluateArgs.java index 647738134c8..180feb48ccf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EvaluateArgs.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EvaluateArgs.java @@ -11,7 +11,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.ProgramElement; import de.uka.ilkd.key.java.ast.Statement; -import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration; import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment; @@ -24,6 +23,8 @@ import de.uka.ilkd.key.java.ast.reference.SuperReference; import de.uka.ilkd.key.java.ast.reference.ThisConstructorReference; import de.uka.ilkd.key.java.ast.reference.ThisReference; +import de.uka.ilkd.key.java.ast.reference.TypeRef; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.VariableNamer; import de.uka.ilkd.key.logic.op.ProgramVariable; @@ -60,7 +61,7 @@ public static ProgramVariable evaluate(Expression e, List bodyStmnts, Expressio services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_INT); final ProgramElementName name = varNamer.getTemporaryNameProposal("i"); final LocalVariableDeclaration forInit = - KeYJavaASTFactory.declare(name, KeYJavaASTFactory.zeroLiteral(), intType); + KeYJavaASTFactory.declare(name, KeYJavaASTFactory.zeroLiteral(), + new TypeRef(intType)); final ProgramVariable pv = (ProgramVariable) forInit.getVariables().get(0).getProgramVariable(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java index 86a6ba85cf9..dec5c6c2906 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java @@ -271,7 +271,7 @@ public void addNeededVariables(Collection variables) { continue; } final LocationVariable l = tb.locationVariable(var.name() + "Before_" + methodName, - var.getKeYJavaType(), true); + var.getTypeReference(), true); services.getNamespaces().programVariables().addSafely(l); final JTerm u = tb.elementary(l, tb.var(var)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MethodCall.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MethodCall.java index 29f37c93033..1dacc69f0d2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MethodCall.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MethodCall.java @@ -349,7 +349,7 @@ private Statement makeMbs(KeYJavaType t, Services services) { if (newContextAsExp.getKeYJavaType(services, execContext) != targetType) { castedThisVar = KeYJavaASTFactory.declare( new ProgramElementName(services.getTermBuilder().newName("target")), - KeYJavaASTFactory.cast(newContextAsExp, targetType), targetType); + KeYJavaASTFactory.cast(newContextAsExp, targetType), new TypeRef(targetType)); localContext = (ReferencePrefix) castedThisVar.getVariableSpecifications().get(0) .getProgramVariable(); @@ -402,7 +402,7 @@ private VariableSpecification[] createParamSpecs(Services services) { final IProgramVariable paramVar = KeYJavaASTFactory.localVariable(services, originalParamVar.getProgramElementName().toString(), - originalParamVar.getKeYJavaType()); + originalParamVar.getTypeReference()); // this condition checks whether this is the last formal parameter // and is used diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ProgramTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ProgramTransformer.java index d1b8368b0ae..4ced705e2a6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ProgramTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ProgramTransformer.java @@ -5,6 +5,7 @@ import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.Annotation; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.ast.reference.ExecutionContext; @@ -154,6 +155,7 @@ public ProgramElement getChildAt(int index) { // -------------some methods to pretend being a type reference -------- + @Override public ReferencePrefix getReferencePrefix() { return null; } @@ -162,37 +164,49 @@ public ReferencePrefix setReferencePrefix(ReferencePrefix r) { return this; } + @Override + public ImmutableList getAnnotations() { + return ImmutableList.of(); + } + @Override public int getDimensions() { return 0; } + @Override public int getTypeReferenceCount() { return 0; } + @Override public TypeReference getTypeReferenceAt(int index) { return this; } + @Override public PackageReference getPackageReference() { return null; } + @Override public int getExpressionCount() { return 0; } + @Override public Expression getExpressionAt(int index) { return null; } + @Override public ProgramElementName getProgramElementName() { return new ProgramElementName(toString()); } + @Override public String getName() { return toString(); } @@ -203,15 +217,18 @@ public String getName() { * * @param v the Visitor */ + @Override public void visit(Visitor v) { v.performActionOnProgramMetaConstruct(this); } /** to String */ + @Override public String toString() { return name + "( " + body + ");"; } + @Override public KeYJavaType getKeYJavaType() { return null; } @@ -220,6 +237,7 @@ public KeYJavaType getKeYJavaType(TermServices javaServ) { return getKeYJavaType(); } + @Override public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) { return getKeYJavaType(); } @@ -244,5 +262,4 @@ public ImmutableList needs() { public ImmutableList neededInstantiations(SVInstantiations svInst) { return ImmutableList.nil(); } - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java index dea977c4653..0742e3a0786 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java @@ -18,6 +18,7 @@ import de.uka.ilkd.key.java.ast.expression.operator.Equals; import de.uka.ilkd.key.java.ast.expression.operator.New; import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.VariableNamer; @@ -59,9 +60,11 @@ public ProgramElement[] transform(ProgramElement pe, Services services, final ExecutionContext ec = insts.getExecutionContext(); ProgramVariable exV = - KeYJavaASTFactory.localVariable(name, sw.getExpression().getKeYJavaType(services, ec)); + KeYJavaASTFactory.localVariable(name, + new TypeRef(sw.getExpression().getKeYJavaType(services, ec))); Statement s = - KeYJavaASTFactory.declare(name, sw.getExpression().getKeYJavaType(services, ec)); + KeYJavaASTFactory.declare(name, + new TypeRef(sw.getExpression().getKeYJavaType(services, ec))); final var changeBreakResult = changeBreaks(sw, newBreak, true); sw = (Switch) changeBreakResult.result; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/TypeOf.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/TypeOf.java index 1cc9337ecb3..2faebab0035 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/TypeOf.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/TypeOf.java @@ -5,6 +5,7 @@ import de.uka.ilkd.key.java.KeYJavaASTFactory; import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.Annotation; import de.uka.ilkd.key.java.ast.ProgramElement; import de.uka.ilkd.key.java.ast.abstraction.ArrayType; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; @@ -14,6 +15,8 @@ import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.util.collection.ImmutableList; + public class TypeOf extends ProgramTransformer { /** @@ -23,7 +26,6 @@ public class TypeOf extends ProgramTransformer { */ public TypeOf(ProgramElement pe) { super("#typeof", pe); - } @Override @@ -36,21 +38,25 @@ public ProgramElement[] transform(ProgramElement pe, Services services, ec = insts.getContextInstantiation().activeStatementContext(); } KeYJavaType kjt = null; + ImmutableList annotations = null; if (pe instanceof Expression) { kjt = services.getTypeConverter().getKeYJavaType((Expression) pe, ec); } else { kjt = ((TypeRef) pe).getKeYJavaType(); + annotations = ((TypeRef) pe).getAnnotations(); } + annotations = annotations == null ? ImmutableList.of() : annotations; + assert kjt != null; if (!(kjt.getJavaType() instanceof PrimitiveType)) { if (kjt.getJavaType() instanceof ArrayType) { return new ProgramElement[] { KeYJavaASTFactory.typeRef(kjt, - ((ArrayType) kjt.getJavaType()).getDimension()) }; + ((ArrayType) kjt.getJavaType()).getDimension(), annotations) }; } } - return new ProgramElement[] { KeYJavaASTFactory.typeRef(kjt) }; + return new ProgramElement[] { KeYJavaASTFactory.typeRef(kjt, 0, annotations) }; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformation.java index 69e2d642d23..912d1e00a66 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformation.java @@ -10,6 +10,7 @@ import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.ast.expression.literal.BooleanLiteral; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.op.ProgramVariable; @@ -234,7 +235,8 @@ public void performActionOnWhile(While x) { Catch ctch = KeYJavaASTFactory.catchClause(KeYJavaASTFactory.parameterDeclaration(javaInfo, - javaInfo.getKeYJavaType("java.lang.Throwable"), excParam), catchStatements); + new TypeRef(javaInfo.getKeYJavaType("java.lang.Throwable")), excParam), + catchStatements); Branch[] branch = { ctch }; Statement res = KeYJavaASTFactory.tryBlock(newBody, branch); @@ -298,7 +300,8 @@ public void performActionOnEnhancedFor(EnhancedFor x) { Catch ctch = KeYJavaASTFactory.catchClause(KeYJavaASTFactory.parameterDeclaration(javaInfo, - javaInfo.getKeYJavaType("java.lang.Throwable"), excParam), catchStatements); + new TypeRef(javaInfo.getKeYJavaType("java.lang.Throwable")), excParam), + catchStatements); addChild(KeYJavaASTFactory.tryBlock(body, ctch)); changed(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java index 2a1f35ab326..f38c9f89924 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.java.ast.StatementBlock; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.expression.literal.BooleanLiteral; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.java.ast.statement.If; import de.uka.ilkd.key.java.ast.statement.MethodFrame; import de.uka.ilkd.key.java.ast.statement.TransactionStatement; @@ -144,7 +145,7 @@ public JTerm transform(TermLabelState termLabelState, Rule rule, getNewLocalvariable("break_" + breakCounter++, "boolean", services); b.setProgramVariable(newVar); stmnt.add(KeYJavaASTFactory.declare(newVar, BooleanLiteral.FALSE, - javaInfo.getKeYJavaType("boolean"))); + new TypeRef(javaInfo.getKeYJavaType("boolean")))); numberOfBreaks++; Statement s; if (b.getBreak().getLabel() != null) { @@ -182,7 +183,7 @@ public JTerm transform(TermLabelState termLabelState, Rule rule, post, rule, ruleApp, goal, applicationPos, services)); if (returnType != null) { - stmnt.add(KeYJavaASTFactory.declare(returnExpression, returnType)); + stmnt.add(KeYJavaASTFactory.declare(returnExpression, new TypeRef(returnType))); } } @@ -196,10 +197,10 @@ public JTerm transform(TermLabelState termLabelState, Rule rule, // we catch all exceptions stmnt.add(KeYJavaASTFactory.declare(excFlag, BooleanLiteral.FALSE, - javaInfo.getKeYJavaType("boolean"))); + new TypeRef(javaInfo.getKeYJavaType("boolean")))); excFlagTerm = typeConv.convertToLogicElement(excFlag); stmnt.add(KeYJavaASTFactory.declare(thrownException, - javaInfo.getKeYJavaType("java.lang.Throwable"))); + new TypeRef(javaInfo.getKeYJavaType("java.lang.Throwable")))); resultSubterms.add(normalCaseAndContinue(termLabelState, services, applicationPos, rule, ruleApp, goal, applicationSequent, contFlagTerm, returnFlagTerm, breakFlagTerm, @@ -286,7 +287,8 @@ private ProgramVariable getNewLocalvariable(String varNameBase, String varType, private ProgramVariable getNewLocalvariable(String varNameBase, KeYJavaType varType, Services services) { return KeYJavaASTFactory.localVariable( - services.getVariableNamer().getTemporaryNameProposal(varNameBase), varType); + services.getVariableNamer().getTemporaryNameProposal(varNameBase), + new TypeRef(varType)); } @@ -330,7 +332,7 @@ private JTerm createLongJunctorTerm(Junctor junctor, ArrayList terms) { private Statement returnFlagDecl(ProgramVariable returnFlag, SVInstantiations svInst) { return KeYJavaASTFactory.declare(returnFlag, BooleanLiteral.FALSE, - javaInfo.getKeYJavaType("boolean")); + new TypeRef(javaInfo.getKeYJavaType("boolean"))); } private JTerm returnCase(TermLabelState termLabelState, ProgramVariable returnFlag, @@ -353,12 +355,12 @@ private JTerm returnCase(TermLabelState termLabelState, ProgramVariable returnFl private Statement breakFlagDecl(ProgramVariable breakFlag) { return KeYJavaASTFactory.declare(breakFlag, BooleanLiteral.FALSE, - javaInfo.getKeYJavaType("boolean")); + new TypeRef(javaInfo.getKeYJavaType("boolean"))); } private Statement contFlagDecl(ProgramVariable contFlag) { return KeYJavaASTFactory.declare(contFlag, BooleanLiteral.FALSE, - javaInfo.getKeYJavaType("boolean")); + new TypeRef(javaInfo.getKeYJavaType("boolean"))); } private JTerm breakCase(TermLabelState termLabelState, ProgramVariable breakFlag, JTerm post, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java index 0916c85fedc..3da5064a04a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java @@ -246,6 +246,11 @@ public ImmutableSet generateFunctionalRepresentsTaclets(Name name, final Pair> limited = limitTerm(schemaRhs, toLimit, services); final JTerm limitedRhs = limited.first; result = result.union(limited.second); + final TermAndBoundVarPair schemaRepresentsLimited = + new TermAndBoundVarPair( + OpReplacer.replace(schemaRepresents.term.sub(1), limitedRhs, schemaRepresents.term, + services.getTermFactory()), + schemaRepresents.boundVars); // create if sequent final boolean finalClass = kjt.getJavaType() instanceof ClassDeclaration @@ -327,7 +332,7 @@ public ImmutableSet generateFunctionalRepresentsTaclets(Name name, if (satisfiability) { tacletBuilder.addRuleSet(new RuleSet(new Name("split"))); } - for (VariableSV boundSV : schemaRepresents.boundVars) { + for (VariableSV boundSV : schemaRepresentsLimited.boundVars) { for (SchemaVariable heapSV : heapSVs) { tacletBuilder.addVarsNotFreeIn(boundSV, heapSV); } @@ -344,7 +349,7 @@ public ImmutableSet generateFunctionalRepresentsTaclets(Name name, if (satisfiability) { functionalRepresentsAddSatisfiabilityBranch(target, services, heapSVs, selfSV, paramSVs, - schemaRepresents, tacletBuilder); + schemaRepresentsLimited, tacletBuilder); } tacletBuilder.setApplicationRestriction( new ApplicationRestriction(ApplicationRestriction.SAME_UPDATE_LEVEL)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java index 9246f032b7f..b80fcb8375b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java @@ -17,6 +17,8 @@ import de.uka.ilkd.key.java.ast.SourceElement; import de.uka.ilkd.key.java.ast.StatementBlock; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.reference.TypeRef; +import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.java.ast.statement.Break; import de.uka.ilkd.key.java.ast.statement.Continue; import de.uka.ilkd.key.java.ast.statement.For; @@ -1020,7 +1022,8 @@ public VariablesCreator(final JavaStatement statement, final List