localVars, @Nullable @Nullable JTerm result, @Nullable @Nullable JTerm exception,
+ JTerm heap) {
this(self, localVars, result, exception, heap, null);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java
index 6de244087d5..e23e918811a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java
@@ -3,21 +3,35 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.informationflow.rule;
+import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Objects;
+import de.uka.ilkd.key.informationflow.po.BlockExecutionPO;
import de.uka.ilkd.key.informationflow.po.IFProofObligationVars;
+import de.uka.ilkd.key.informationflow.po.SymbolicExecutionPO;
+import de.uka.ilkd.key.informationflow.po.snippet.InfFlowPOSnippetFactory;
+import de.uka.ilkd.key.informationflow.po.snippet.POSnippetFactory;
+import de.uka.ilkd.key.informationflow.proof.InfFlowCheckInfo;
import de.uka.ilkd.key.informationflow.proof.InfFlowProof;
+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.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.reference.ExecutionContext;
+import de.uka.ilkd.key.java.statement.JavaStatement;
import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.logic.ProgramElementName;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.TermServices;
+import de.uka.ilkd.key.logic.label.ParameterlessTermLabel;
+import de.uka.ilkd.key.logic.op.JFunction;
import de.uka.ilkd.key.logic.op.LocationVariable;
import de.uka.ilkd.key.logic.op.ProgramVariable;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit;
+import de.uka.ilkd.key.proof.init.FunctionalBlockContractPO;
import de.uka.ilkd.key.proof.init.ProofObligationVars;
import de.uka.ilkd.key.rule.AuxiliaryContractBuilders.ConditionsAndClausesBuilder;
import de.uka.ilkd.key.rule.AuxiliaryContractBuilders.GoalsConfigurator;
@@ -35,9 +49,13 @@
import org.key_project.logic.op.Function;
import org.key_project.prover.sequent.PosInOccurrence;
import org.key_project.prover.sequent.SequentFormula;
+import org.key_project.util.collection.DefaultImmutableSet;
import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSLList;
import org.key_project.util.collection.ImmutableSet;
+import org.jspecify.annotations.Nullable;
+
/**
*
* Rule for the application of {@link BlockContract}s.
@@ -166,7 +184,7 @@ private static JTerm[] createUpdates(final JTerm contextUpdate,
* @param services services.
* @return a list containing the new goals.
*/
- private static ImmutableList splitIntoGoals(final Goal goal, final BlockContract contract,
+ protected ImmutableList splitIntoGoals(final Goal goal, final BlockContract contract,
final List heaps,
final ImmutableSet localInVariables,
final Map anonymisationHeaps,
@@ -223,7 +241,6 @@ public BlockContractInternalBuiltInRuleApp createApp(final PosInOccurrence occur
* Sets up the validity goal as the first goal in the list.
*
* @param result the new goals.
- * @param isInfFlow whether or not this is an information flow proof.
* @param contract the block contract being applied.
* @param application the rule application.
* @param instantiation the instantiation.
@@ -241,7 +258,7 @@ public BlockContractInternalBuiltInRuleApp createApp(final PosInOccurrence occur
* @param services services.
*/
@Override
- protected void setUpValidityGoal(final ImmutableList result, final boolean isInfFlow,
+ protected void setUpValidityGoal(final ImmutableList result,
final BlockContract contract, final BlockContractInternalBuiltInRuleApp application,
final Instantiation instantiation, final List heaps,
final Map anonymisationHeaps,
@@ -254,6 +271,7 @@ protected void setUpValidityGoal(final ImmutableList result, final boolean
final Services services) {
Goal validityGoal = result.tail().tail().head();
assert validityGoal != null;
+ var app = (InfFlowBlockContractInternalBuiltInRuleApp) application;
final ProgramVariable exceptionParameter =
createLocalVariable("e", variables.exception.getKeYJavaType(), services);
@@ -268,7 +286,7 @@ protected void setUpValidityGoal(final ImmutableList result, final boolean
// set up information flow validity goal
InfFlowValidityData infFlowValidityData = setUpInfFlowValidityGoal(validityGoal,
contract, anonymisationHeaps, services, variables, exceptionParameter, heaps,
- localInVariables, localOutVariables, application, instantiation);
+ localInVariables, localOutVariables, app, instantiation);
// do additional inf flow preparations on the usage goal
setUpInfFlowPartOfUsageGoal(Objects.requireNonNull(result.head()), infFlowValidityData,
updates[0],
@@ -286,7 +304,7 @@ protected InfFlowValidityData setUpInfFlowValidityGoal(final Goal infFlowGoal,
final ProgramVariable exceptionParameter, final List heaps,
final ImmutableSet localInVariables,
final ImmutableSet localOutVariables,
- final BlockContractInternalBuiltInRuleApp application,
+ final InfFlowBlockContractInternalBuiltInRuleApp application,
final Instantiation instantiation) {
assert heaps.size() == 1 && anonymisationHeaps.size() <= 1
: "information flow extension is at the moment not "
@@ -348,6 +366,214 @@ protected void setUpInfFlowPartOfUsageGoal(final Goal usageGoal,
usageGoal.addFormula(new SequentFormula(uAssumptions), true, false);
}
+ /**
+ *
+ * @param contract a block contract.
+ * @param goal the current goal.
+ * @return {@code true} if the contract has already been applied.
+ */
+ protected static boolean contractApplied(final BlockContract contract, final Goal goal) {
+ var po = getAppliedProofObligation(contract, goal);
+ return switch (po) {
+ case FunctionalBlockContractPO functionalBlockContractPO when contract.getBlock()
+ .equals(functionalBlockContractPO.getBlock()) ->
+ true;
+ case SymbolicExecutionPO symbolicExecutionPO -> {
+ Goal initiatingGoal = symbolicExecutionPO.getInitiatingGoal();
+ yield contractApplied(contract, initiatingGoal);
+ }
+ case BlockExecutionPO blockExecutionPO -> {
+ Goal initiatingGoal = blockExecutionPO.getInitiatingGoal();
+ yield contractApplied(contract, initiatingGoal);
+ }
+ case null, default -> false;
+ };
+ }
+
+
+ static SequentFormula buildBodyPreservesSequent(
+ InfFlowPOSnippetFactory f, InfFlowProof proof) {
+ JTerm selfComposedExec =
+ f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_BLOCK_WITH_PRE_RELATION);
+ JTerm post = f.create(InfFlowPOSnippetFactory.Snippet.INF_FLOW_INPUT_OUTPUT_RELATION);
+ final TermBuilder tb = proof.getServices().getTermBuilder();
+
+ final JTerm finalTerm =
+ tb.imp(tb.label(selfComposedExec, ParameterlessTermLabel.SELF_COMPOSITION_LABEL), post);
+ proof.addLabeledIFSymbol(selfComposedExec);
+
+ return new SequentFormula(finalTerm);
+ }
+
+ protected static ProofObligationVars generateProofObligationVariables(
+ final AuxiliaryContract.Variables variables, final ProgramVariable exceptionParameter,
+ final LocationVariable baseHeap, final ImmutableList localVarsAtPre,
+ final ImmutableList localVarsAtPost, final Services services,
+ final TermBuilder tb) {
+ final boolean hasSelf = variables.self != null;
+ final boolean hasRes = variables.result != null;
+ final boolean hasExc = variables.exception != null;
+
+ final JTerm heapAtPre = tb.var(variables.remembranceHeaps.get(baseHeap));
+ final Name heapAtPostName = new Name(tb.newName("heap_After_BLOCK"));
+ final JTerm heapAtPost = tb.func(new JFunction(heapAtPostName, heapAtPre.sort(), true));
+ final JTerm selfAtPre = hasSelf ? tb.var(variables.self) : tb.NULL();
+ final JTerm selfAtPost = hasSelf ? buildAfterVar(selfAtPre, "BLOCK", services) : tb.NULL();
+
+ JTerm resultAtPre = hasRes ? tb.var(variables.result) : tb.NULL();
+ final JTerm resultAtPost =
+ hasRes ? buildAfterVar(resultAtPre, "BLOCK", services) : tb.NULL();
+ final JTerm exceptionAtPre = hasExc ? tb.var(variables.exception) : tb.NULL();
+ final JTerm exceptionAtPost =
+ hasExc ? buildAfterVar(exceptionAtPre, "BLOCK", services) : tb.NULL();
+
+ // generate proof obligation variables
+ final StateVars instantiationPreVars = new StateVars(hasSelf ? selfAtPre : null,
+ localVarsAtPre, hasRes ? resultAtPre : null, hasExc ? exceptionAtPre : null, heapAtPre);
+ final StateVars instantiationPostVars =
+ new StateVars(hasSelf ? selfAtPost : null, localVarsAtPost,
+ hasRes ? resultAtPost : null, hasExc ? exceptionAtPost : null, heapAtPost);
+ final ProofObligationVars instantiationVars = new ProofObligationVars(instantiationPreVars,
+ instantiationPostVars, tb.var(exceptionParameter), null, tb);
+ return instantiationVars;
+ }
+
+ protected static void addProofObligation(final Goal infFlowGoal, final InfFlowProof proof,
+ final BlockContract contract, final IFProofObligationVars ifVars,
+ final ExecutionContext ec, final Services services) {
+ // create proof obligation
+ InfFlowPOSnippetFactory infFlowFactory =
+ POSnippetFactory.getInfFlowFactory(contract, ifVars.c1, ifVars.c2, ec, services);
+
+ final SequentFormula poFormula =
+ buildBodyPreservesSequent(infFlowFactory, proof);
+
+ // add proof obligation to goal
+ infFlowGoal.addFormula(poFormula, false, true);
+ }
+
+ /**
+ *
+ * @param collectedContracts a set of block contracts.
+ * @param goal the current goal.
+ * @return the set with all non-applicable contracts filtered out.
+ */
+ protected static ImmutableSet filterAppliedContracts(
+ final ImmutableSet collectedContracts, final Goal goal) {
+ ImmutableSet result = DefaultImmutableSet.nil();
+ for (BlockContract contract : collectedContracts) {
+ if (!contractApplied(contract, goal) || InfFlowCheckInfo.isInfFlow(goal)) {
+ result = result.add(contract);
+ }
+ }
+ return result;
+ }
+
+ /*
+ * Factory methods for information flow contracts.
+ *
+ * TODO These could be moved into a separate class (like BlockContractBuilders) to allow them to
+ * be reused in other classes.
+ */
+ protected static @Nullable JTerm buildAfterVar(JTerm varTerm, String suffix,
+ Services services) {
+ if (varTerm == null) {
+ return null;
+ }
+ assert varTerm.op() instanceof LocationVariable;
+
+ final TermBuilder tb = services.getTermBuilder();
+ KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType();
+ if (!suffix.equalsIgnoreCase("")) {
+ suffix = "_" + suffix;
+ }
+ String name = tb.newName(varTerm + "_After" + suffix);
+ LocationVariable varAtPostVar =
+ new LocationVariable(new ProgramElementName(name), resultType);
+ register(varAtPostVar, services);
+ JTerm varAtPost = tb.var(varAtPostVar);
+ return varAtPost;
+ }
+
+
+ protected static ImmutableList buildLocalOutsAtPre(ImmutableList varTerms,
+ Services services) {
+ if (varTerms == null || varTerms.isEmpty()) {
+ return varTerms;
+ }
+ final TermBuilder tb = services.getTermBuilder();
+ ImmutableList renamedLocalOuts = ImmutableSLList.nil();
+ for (JTerm varTerm : varTerms) {
+ assert varTerm.op() instanceof LocationVariable;
+
+ KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType();
+
+ String name = tb.newName(varTerm + "_Before");
+ LocationVariable varAtPostVar =
+ new LocationVariable(new ProgramElementName(name), resultType);
+ register(varAtPostVar, services);
+ JTerm varAtPost = tb.var(varAtPostVar);
+ renamedLocalOuts = renamedLocalOuts.append(varAtPost);
+ }
+ return renamedLocalOuts;
+ }
+
+ protected static ImmutableList buildLocalOutsAtPost(ImmutableList varTerms,
+ Services services) {
+ if (varTerms == null || varTerms.isEmpty()) {
+ return varTerms;
+ }
+ final TermBuilder tb = services.getTermBuilder();
+ ImmutableList renamedLocalOuts = ImmutableSLList.nil();
+ for (JTerm varTerm : varTerms) {
+ assert varTerm.op() instanceof LocationVariable;
+
+ KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType();
+
+ String name = tb.newName(varTerm + "_After");
+ LocationVariable varAtPostVar =
+ new LocationVariable(new ProgramElementName(name), resultType);
+ register(varAtPostVar, services);
+ JTerm varAtPost = tb.var(varAtPostVar);
+ renamedLocalOuts = renamedLocalOuts.append(varAtPost);
+ }
+ return renamedLocalOuts;
+ }
+
+ protected static JTerm buildInfFlowPreAssumption(ProofObligationVars instVars,
+ ImmutableList localOuts, ImmutableList localOutsAtPre, JTerm baseHeap,
+ final TermBuilder tb) {
+ JTerm beforeAssumptions = tb.equals(instVars.pre.heap, baseHeap);
+ Iterator outsAtPre = localOutsAtPre.iterator();
+ for (JTerm locOut : localOuts) {
+ beforeAssumptions = tb.and(beforeAssumptions, tb.equals(outsAtPre.next(), locOut));
+ }
+ return beforeAssumptions;
+ }
+
+ protected static JTerm buildInfFlowPostAssumption(ProofObligationVars instVars,
+ ImmutableList localOuts, ImmutableList localOutsAtPost, JTerm baseHeap,
+ JTerm applPredTerm, final TermBuilder tb) {
+ JTerm resultEq =
+ instVars.pre.result != null ? tb.equals(instVars.post.result, instVars.pre.result)
+ : tb.tt();
+ JTerm exceptionEq = instVars.pre.exception != null
+ ? tb.equals(instVars.post.exception, instVars.pre.exception)
+ : tb.tt();
+ JTerm selfEq =
+ instVars.pre.self != null ? tb.equals(instVars.post.self, instVars.pre.self) : tb.tt();
+ JTerm afterAssumptions =
+ tb.and(tb.equals(instVars.post.heap, baseHeap), selfEq, resultEq, exceptionEq);
+ Iterator outAtPost = localOutsAtPost.iterator();
+ for (JTerm locOut : localOuts) {
+ afterAssumptions = tb.and(afterAssumptions, tb.equals(outAtPost.next(), locOut));
+ }
+ afterAssumptions = tb.and(afterAssumptions, applPredTerm);
+
+ return afterAssumptions;
+ }
+
+
protected static class InfFlowValidityData {
final JTerm preAssumption;
@@ -361,4 +587,44 @@ public InfFlowValidityData(final JTerm preAssumption, final JTerm postAssumption
this.taclet = taclet;
}
}
+
+ public static class InfFlowBlockContractInternalBuiltInRuleApp
+ extends BlockContractInternalBuiltInRuleApp {
+ public InfFlowBlockContractInternalBuiltInRuleApp(InfFlowBlockContractInternalRule rule,
+ PosInOccurrence occurrence) {
+ super(rule, occurrence);
+ }
+
+ public InfFlowBlockContractInternalBuiltInRuleApp(InfFlowBlockContractInternalRule rule,
+ PosInOccurrence occurrence,
+ @Nullable ImmutableList ifInstantiations,
+ @Nullable JavaStatement statement, @Nullable BlockContract contract,
+ @Nullable List heaps) {
+ super(rule, occurrence, ifInstantiations, statement, contract, heaps);
+ }
+
+ /**
+ * @see #getInformationFlowProofObligationVars()
+ */
+ protected IFProofObligationVars infFlowVars;
+
+ /**
+ *
+ * @return set of four sets of ProofObligationVars necessary for information flow proofs.
+ */
+ public IFProofObligationVars getInformationFlowProofObligationVars() {
+ return infFlowVars;
+ }
+
+ /**
+ * Sets the proof obligation variables and execution context to new values.
+ *
+ * @param vars new proof obligation variables.
+ * @param context new execution context.
+ */
+ public void update(IFProofObligationVars vars, ExecutionContext context) {
+ this.infFlowVars = vars;
+ this.context = context;
+ }
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowLoopInvariantBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowLoopInvariantBuiltInRuleApp.java
new file mode 100644
index 00000000000..b343254c613
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowLoopInvariantBuiltInRuleApp.java
@@ -0,0 +1,52 @@
+/* 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.informationflow.rule;
+
+import java.util.List;
+
+import de.uka.ilkd.key.informationflow.po.IFProofObligationVars;
+import de.uka.ilkd.key.logic.TermServices;
+import de.uka.ilkd.key.logic.op.LocationVariable;
+import de.uka.ilkd.key.rule.AbstractLoopInvariantRule;
+import de.uka.ilkd.key.rule.LoopInvariantBuiltInRuleApp;
+import de.uka.ilkd.key.speclang.LoopSpecification;
+
+import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.util.collection.ImmutableList;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (7/28/25)
+ */
+public class InfFlowLoopInvariantBuiltInRuleApp
+ extends LoopInvariantBuiltInRuleApp {
+
+ private IFProofObligationVars infFlowVars;
+
+ protected InfFlowLoopInvariantBuiltInRuleApp(T rule, PosInOccurrence pio,
+ @Nullable ImmutableList ifInsts, @Nullable LoopSpecification inv,
+ @Nullable List heapContext, TermServices services) {
+ super(rule, pio, ifInsts, inv, heapContext, services);
+ }
+
+ protected InfFlowLoopInvariantBuiltInRuleApp(T rule, PosInOccurrence pio, LoopSpecification inv,
+ TermServices services) {
+ super(rule, pio, inv, services);
+ }
+
+ public InfFlowLoopInvariantBuiltInRuleApp(T rule, PosInOccurrence pos, TermServices services) {
+ super(rule, pos, services);
+ }
+
+ public void setInformationFlowProofObligationVars(IFProofObligationVars vars) {
+ this.infFlowVars = vars;
+ }
+
+ public IFProofObligationVars getInformationFlowProofObligationVars() {
+ return infFlowVars;
+ }
+
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantHook.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantHook.java
index ba07fe1b198..79052dd4c92 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantHook.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantHook.java
@@ -53,7 +53,7 @@
public class InfFlowWhileInvariantHook implements WhileInvariantRule.WhileInvariantHook {
@Override
public void rewriteStandardGoals(Services services, Goal init, Goal preserve, Goal terminate,
- Instantiation inst, LoopInvariantBuiltInRuleApp loopRuleApp,
+ Instantiation inst, InfFlowLoopInvariantBuiltInRuleApp> loopRuleApp,
JavaBlock guardJb,
ImmutableSet localIns,
ImmutableSet localOuts,
@@ -74,7 +74,7 @@ public void rewriteStandardGoals(Services services, Goal init, Goal preserve, Go
}
private static InfFlowData setUpInfFlowValidityGoal(Goal infFlowGoal,
- LoopInvariantBuiltInRuleApp ruleApp, Instantiation inst,
+ InfFlowLoopInvariantBuiltInRuleApp> ruleApp, Instantiation inst,
JavaBlock guardJb,
ImmutableSet localIns,
ImmutableSet localOuts,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProofObligationVars.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProofObligationVars.java
index d1c5bb7ac91..b58cde1966b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProofObligationVars.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProofObligationVars.java
@@ -14,6 +14,7 @@
import de.uka.ilkd.key.logic.label.TermLabel;
import de.uka.ilkd.key.logic.op.*;
+import org.jspecify.annotations.Nullable;
import org.key_project.logic.Namespace;
import org.key_project.logic.op.Function;
import org.key_project.util.collection.ImmutableArray;
@@ -76,7 +77,7 @@ public ProofObligationVars(StateVars pre, StateVars post, JTerm exceptionParamet
}
public ProofObligationVars(StateVars pre, StateVars post, JTerm exceptionParameter,
- ImmutableList formalParams, TermBuilder tb) {
+ @Nullable ImmutableList formalParams, TermBuilder tb) {
this.pre = pre;
this.post = post;
this.exceptionParameter = exceptionParameter;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractBuiltInRuleApp.java
index b78a718f720..2941cc62454 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractBuiltInRuleApp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractBuiltInRuleApp.java
@@ -5,7 +5,6 @@
import java.util.List;
-import de.uka.ilkd.key.informationflow.po.IFProofObligationVars;
import de.uka.ilkd.key.java.reference.ExecutionContext;
import de.uka.ilkd.key.java.statement.JavaStatement;
import de.uka.ilkd.key.logic.op.LocationVariable;
@@ -15,27 +14,27 @@
import org.key_project.prover.sequent.PosInOccurrence;
import org.key_project.util.collection.ImmutableList;
+import org.jspecify.annotations.Nullable;
+
/**
* Application for {@link AbstractAuxiliaryContractRule}.
*
* @author wacker, lanzinger
*/
-public abstract class AbstractAuxiliaryContractBuiltInRuleApp extends AbstractBuiltInRuleApp {
+public abstract class AbstractAuxiliaryContractBuiltInRuleApp
+ extends AbstractBuiltInRuleApp {
/**
* @see #getStatement()
*/
- private JavaStatement statement;
+ private @Nullable JavaStatement statement;
/**
* @see #getHeapContext()
+ * FIXME weigl: should this not be {@link ImmutableList}?
*/
- protected List heaps;
+ protected @Nullable List heaps;
- /**
- * @see #getInformationFlowProofObligationVars()
- */
- protected IFProofObligationVars infFlowVars;
/**
* @see #getExecutionContext()
@@ -48,8 +47,8 @@ public abstract class AbstractAuxiliaryContractBuiltInRuleApp extends AbstractBu
* @param occurrence the position at which the rule is applied.
* @param ifInstantiations if instantiations.
*/
- protected AbstractAuxiliaryContractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence,
- ImmutableList ifInstantiations) {
+ protected AbstractAuxiliaryContractBuiltInRuleApp(T rule, PosInOccurrence occurrence,
+ @Nullable ImmutableList ifInstantiations) {
super(rule, occurrence, ifInstantiations);
}
@@ -57,7 +56,7 @@ protected AbstractAuxiliaryContractBuiltInRuleApp(BuiltInRule rule, PosInOccurre
*
* @param s the statement (block or loop) which the applied contract belongs to.
*/
- public void setStatement(JavaStatement s) {
+ public void setStatement(@Nullable JavaStatement s) {
this.statement = s;
}
@@ -75,13 +74,6 @@ public JavaStatement getStatement() {
*/
public abstract AuxiliaryContract getContract();
- /**
- *
- * @return set of four sets of ProofObligationVars necessary for information flow proofs.
- */
- public IFProofObligationVars getInformationFlowProofObligationVars() {
- return infFlowVars;
- }
/**
*
@@ -114,14 +106,5 @@ public boolean cannotComplete(final Goal goal) {
return !builtInRule.isApplicable(goal, pio);
}
- /**
- * Sets the proof obligation variables and execution context to new values.
- *
- * @param vars new proof obligation variables.
- * @param context new execution context.
- */
- public void update(IFProofObligationVars vars, ExecutionContext context) {
- this.infFlowVars = vars;
- this.context = context;
- }
+
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractBuiltInRuleApp.java
index 439456f5adf..9ca2926c3cf 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractBuiltInRuleApp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractBuiltInRuleApp.java
@@ -19,18 +19,20 @@
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSet;
+import org.jspecify.annotations.Nullable;
+
/**
* Application of {@link AbstractBlockContractRule}.
*
* @author wacker, lanzinger
*/
-public abstract class AbstractBlockContractBuiltInRuleApp
- extends AbstractAuxiliaryContractBuiltInRuleApp {
+public abstract class AbstractBlockContractBuiltInRuleApp
+ extends AbstractAuxiliaryContractBuiltInRuleApp {
/**
* @see #getContract()
*/
- protected BlockContract contract;
+ protected @Nullable BlockContract contract;
/**
*
@@ -38,13 +40,13 @@ public abstract class AbstractBlockContractBuiltInRuleApp
* @param occurrence the position at which the rule is applied.
* @param ifInstantiations if instantiations.
*/
- protected AbstractBlockContractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence,
- ImmutableList ifInstantiations) {
+ protected AbstractBlockContractBuiltInRuleApp(T rule, PosInOccurrence occurrence,
+ @Nullable ImmutableList ifInstantiations) {
super(rule, occurrence, ifInstantiations);
}
@Override
- public BlockContract getContract() {
+ public @Nullable BlockContract getContract() {
return contract;
}
@@ -54,7 +56,7 @@ public BlockContract getContract() {
* @param rule the rule being applied.
* @return this.
*/
- public AbstractBlockContractBuiltInRuleApp tryToInstantiate(final Goal goal,
+ public AbstractBlockContractBuiltInRuleApp tryToInstantiate(final Goal goal,
final AbstractBlockContractRule rule) {
if (complete() || cannotComplete(goal)) {
return this;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java
index a7ce89f09a0..604d4720b17 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java
@@ -3,49 +3,33 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.rule;
-import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.Map;
-import de.uka.ilkd.key.informationflow.po.BlockExecutionPO;
-import de.uka.ilkd.key.informationflow.po.IFProofObligationVars;
-import de.uka.ilkd.key.informationflow.po.SymbolicExecutionPO;
-import de.uka.ilkd.key.informationflow.po.snippet.InfFlowPOSnippetFactory;
-import de.uka.ilkd.key.informationflow.po.snippet.POSnippetFactory;
-import de.uka.ilkd.key.informationflow.proof.InfFlowCheckInfo;
-import de.uka.ilkd.key.informationflow.proof.InfFlowProof;
-import de.uka.ilkd.key.informationflow.proof.init.StateVars;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.StatementBlock;
-import de.uka.ilkd.key.java.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.reference.ExecutionContext;
import de.uka.ilkd.key.java.statement.JavaStatement;
import de.uka.ilkd.key.logic.JTerm;
-import de.uka.ilkd.key.logic.ProgramElementName;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.TermServices;
-import de.uka.ilkd.key.logic.label.ParameterlessTermLabel;
import de.uka.ilkd.key.logic.op.*;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.init.FunctionalBlockContractPO;
import de.uka.ilkd.key.proof.init.ProofOblInput;
-import de.uka.ilkd.key.proof.init.ProofObligationVars;
import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
-import de.uka.ilkd.key.speclang.AuxiliaryContract;
import de.uka.ilkd.key.speclang.BlockContract;
import org.key_project.logic.Name;
import org.key_project.logic.op.Function;
import org.key_project.prover.rules.RuleApp;
import org.key_project.prover.sequent.PosInOccurrence;
-import org.key_project.prover.sequent.SequentFormula;
import org.key_project.util.collection.DefaultImmutableSet;
-import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
import org.key_project.util.collection.ImmutableSet;
+import org.jspecify.annotations.Nullable;
+
/**
*
* Rule for the application of {@link BlockContract}s.
@@ -64,7 +48,7 @@ public abstract class AbstractBlockContractRule extends AbstractAuxiliaryContrac
* @param services services.
* @return all applicable block contracts for the instantiation.
*/
- public static ImmutableSet getApplicableContracts(
+ public static @Nullable ImmutableSet getApplicableContracts(
final Instantiation instantiation, final Goal goal, final Services services) {
if (instantiation == null) {
return DefaultImmutableSet.nil();
@@ -80,7 +64,7 @@ public static ImmutableSet getApplicableContracts(
* @param goal the current goal.
* @return all applicable block contracts for the block from the repository.
*/
- public static ImmutableSet getApplicableContracts(
+ public static @Nullable ImmutableSet getApplicableContracts(
final SpecificationRepository specifications, final JavaStatement statement,
final JModality.JavaModalityKind modalityKind, final Goal goal) {
if (statement instanceof StatementBlock block) {
@@ -112,7 +96,7 @@ protected static ImmutableSet filterAppliedContracts(
final ImmutableSet collectedContracts, final Goal goal) {
ImmutableSet result = DefaultImmutableSet.nil();
for (BlockContract contract : collectedContracts) {
- if (!contractApplied(contract, goal) || InfFlowCheckInfo.isInfFlow(goal)) {
+ if (!contractApplied(contract, goal) /* || InfFlowCheckInfo.isInfFlow(goal) */) {
result = result.add(contract);
}
}
@@ -126,6 +110,23 @@ protected static ImmutableSet filterAppliedContracts(
* @return {@code true} if the contract has already been applied.
*/
protected static boolean contractApplied(final BlockContract contract, final Goal goal) {
+ final var po = getAppliedProofObligation(contract, goal);
+ if (po == null)
+ return true;
+
+ return po instanceof FunctionalBlockContractPO functionalBlockContractPO
+ && contract.getBlock().equals(functionalBlockContractPO.getBlock());
+ }
+
+ /// Searches backwards for a [{@link BlockContractInternalBuiltInRuleApp] on the parent path of
+ /// `goal`.
+ /// @param contract a block contract.
+ /// @param goal the current goal.
+ /// @return the proof obligation for the contract on the proof if the contract has already been
+ /// applied,
+ /// otherwise `null`.
+ protected static @Nullable ProofOblInput getAppliedProofObligation(BlockContract contract,
+ Goal goal) {
Node selfOrParentNode = goal.node();
Node previousNode = null;
while (selfOrParentNode != null) {
@@ -137,7 +138,7 @@ protected static boolean contractApplied(final BlockContract contract, final Goa
// but not in other branches, e.g., do-while
// loops might need to apply the same contract
// twice in its usage branch
- return true;
+ return null;
}
}
previousNode = selfOrParentNode;
@@ -146,22 +147,7 @@ protected static boolean contractApplied(final BlockContract contract, final Goa
Services services = goal.proof().getServices();
Proof proof = goal.proof();
- ProofOblInput po = services.getSpecificationRepository().getProofOblInput(proof);
-
- if (po instanceof FunctionalBlockContractPO
- && contract.getBlock().equals(((FunctionalBlockContractPO) po).getBlock())) {
- return true;
- }
-
- if (po instanceof SymbolicExecutionPO) {
- Goal initiatingGoal = ((SymbolicExecutionPO) po).getInitiatingGoal();
- return contractApplied(contract, initiatingGoal);
- } else if (po instanceof BlockExecutionPO) {
- Goal initiatingGoal = ((BlockExecutionPO) po).getInitiatingGoal();
- return contractApplied(contract, initiatingGoal);
- } else {
- return false;
- }
+ return services.getSpecificationRepository().getProofOblInput(proof);
}
/**
@@ -189,169 +175,6 @@ protected static Map createAndRegisterAnonymisationV
return result;
}
- /*
- * Factory methods for information flow contracts.
- *
- * TODO These could be moved into a separate class (like BlockContractBuilders) to allow them to
- * be reused in other classes.
- */
-
- protected static JTerm buildAfterVar(JTerm varTerm, String suffix, Services services) {
- if (varTerm == null) {
- return null;
- }
- assert varTerm.op() instanceof LocationVariable;
-
- final TermBuilder tb = services.getTermBuilder();
- KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType();
- if (!suffix.equalsIgnoreCase("")) {
- suffix = "_" + suffix;
- }
- String name = tb.newName(varTerm + "_After" + suffix);
- LocationVariable varAtPostVar =
- new LocationVariable(new ProgramElementName(name), resultType);
- register(varAtPostVar, services);
- JTerm varAtPost = tb.var(varAtPostVar);
- return varAtPost;
- }
-
- protected static ImmutableList buildLocalOutsAtPre(ImmutableList varTerms,
- Services services) {
- if (varTerms == null || varTerms.isEmpty()) {
- return varTerms;
- }
- final TermBuilder tb = services.getTermBuilder();
- ImmutableList renamedLocalOuts = ImmutableSLList.nil();
- for (JTerm varTerm : varTerms) {
- assert varTerm.op() instanceof LocationVariable;
-
- KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType();
-
- String name = tb.newName(varTerm + "_Before");
- LocationVariable varAtPostVar =
- new LocationVariable(new ProgramElementName(name), resultType);
- register(varAtPostVar, services);
- JTerm varAtPost = tb.var(varAtPostVar);
- renamedLocalOuts = renamedLocalOuts.append(varAtPost);
- }
- return renamedLocalOuts;
- }
-
- protected static ImmutableList buildLocalOutsAtPost(ImmutableList varTerms,
- Services services) {
- if (varTerms == null || varTerms.isEmpty()) {
- return varTerms;
- }
- final TermBuilder tb = services.getTermBuilder();
- ImmutableList renamedLocalOuts = ImmutableSLList.nil();
- for (JTerm varTerm : varTerms) {
- assert varTerm.op() instanceof LocationVariable;
-
- KeYJavaType resultType = ((LocationVariable) varTerm.op()).getKeYJavaType();
-
- String name = tb.newName(varTerm + "_After");
- LocationVariable varAtPostVar =
- new LocationVariable(new ProgramElementName(name), resultType);
- register(varAtPostVar, services);
- JTerm varAtPost = tb.var(varAtPostVar);
- renamedLocalOuts = renamedLocalOuts.append(varAtPost);
- }
- return renamedLocalOuts;
- }
-
- protected static JTerm buildInfFlowPreAssumption(ProofObligationVars instVars,
- ImmutableList localOuts, ImmutableList localOutsAtPre, JTerm baseHeap,
- final TermBuilder tb) {
- JTerm beforeAssumptions = tb.equals(instVars.pre.heap, baseHeap);
- Iterator outsAtPre = localOutsAtPre.iterator();
- for (JTerm locOut : localOuts) {
- beforeAssumptions = tb.and(beforeAssumptions, tb.equals(outsAtPre.next(), locOut));
- }
- return beforeAssumptions;
- }
-
- protected static JTerm buildInfFlowPostAssumption(ProofObligationVars instVars,
- ImmutableList localOuts, ImmutableList localOutsAtPost, JTerm baseHeap,
- JTerm applPredTerm, final TermBuilder tb) {
- JTerm resultEq =
- instVars.pre.result != null ? tb.equals(instVars.post.result, instVars.pre.result)
- : tb.tt();
- JTerm exceptionEq = instVars.pre.exception != null
- ? tb.equals(instVars.post.exception, instVars.pre.exception)
- : tb.tt();
- JTerm selfEq =
- instVars.pre.self != null ? tb.equals(instVars.post.self, instVars.pre.self) : tb.tt();
- JTerm afterAssumptions =
- tb.and(tb.equals(instVars.post.heap, baseHeap), selfEq, resultEq, exceptionEq);
- Iterator outAtPost = localOutsAtPost.iterator();
- for (JTerm locOut : localOuts) {
- afterAssumptions = tb.and(afterAssumptions, tb.equals(outAtPost.next(), locOut));
- }
- afterAssumptions = tb.and(afterAssumptions, applPredTerm);
-
- return afterAssumptions;
- }
-
- static SequentFormula buildBodyPreservesSequent(
- InfFlowPOSnippetFactory f, InfFlowProof proof) {
- JTerm selfComposedExec =
- f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_BLOCK_WITH_PRE_RELATION);
- JTerm post = f.create(InfFlowPOSnippetFactory.Snippet.INF_FLOW_INPUT_OUTPUT_RELATION);
- final TermBuilder tb = proof.getServices().getTermBuilder();
-
- final JTerm finalTerm =
- tb.imp(tb.label(selfComposedExec, ParameterlessTermLabel.SELF_COMPOSITION_LABEL), post);
- proof.addLabeledIFSymbol(selfComposedExec);
-
- return new SequentFormula(finalTerm);
- }
-
- protected static ProofObligationVars generateProofObligationVariables(
- final AuxiliaryContract.Variables variables, final ProgramVariable exceptionParameter,
- final LocationVariable baseHeap, final ImmutableList localVarsAtPre,
- final ImmutableList localVarsAtPost, final Services services,
- final TermBuilder tb) {
- final boolean hasSelf = variables.self != null;
- final boolean hasRes = variables.result != null;
- final boolean hasExc = variables.exception != null;
-
- final JTerm heapAtPre = tb.var(variables.remembranceHeaps.get(baseHeap));
- final Name heapAtPostName = new Name(tb.newName("heap_After_BLOCK"));
- final JTerm heapAtPost = tb.func(new JFunction(heapAtPostName, heapAtPre.sort(), true));
- final JTerm selfAtPre = hasSelf ? tb.var(variables.self) : tb.NULL();
- final JTerm selfAtPost = hasSelf ? buildAfterVar(selfAtPre, "BLOCK", services) : tb.NULL();
-
- JTerm resultAtPre = hasRes ? tb.var(variables.result) : tb.NULL();
- final JTerm resultAtPost =
- hasRes ? buildAfterVar(resultAtPre, "BLOCK", services) : tb.NULL();
- final JTerm exceptionAtPre = hasExc ? tb.var(variables.exception) : tb.NULL();
- final JTerm exceptionAtPost =
- hasExc ? buildAfterVar(exceptionAtPre, "BLOCK", services) : tb.NULL();
-
- // generate proof obligation variables
- final StateVars instantiationPreVars = new StateVars(hasSelf ? selfAtPre : null,
- localVarsAtPre, hasRes ? resultAtPre : null, hasExc ? exceptionAtPre : null, heapAtPre);
- final StateVars instantiationPostVars =
- new StateVars(hasSelf ? selfAtPost : null, localVarsAtPost,
- hasRes ? resultAtPost : null, hasExc ? exceptionAtPost : null, heapAtPost);
- final ProofObligationVars instantiationVars = new ProofObligationVars(instantiationPreVars,
- instantiationPostVars, tb.var(exceptionParameter), null, tb);
- return instantiationVars;
- }
-
- protected static void addProofObligation(final Goal infFlowGoal, final InfFlowProof proof,
- final BlockContract contract, final IFProofObligationVars ifVars,
- final ExecutionContext ec, final Services services) {
- // create proof obligation
- InfFlowPOSnippetFactory infFlowFactory =
- POSnippetFactory.getInfFlowFactory(contract, ifVars.c1, ifVars.c2, ec, services);
-
- final SequentFormula poFormula =
- buildBodyPreservesSequent(infFlowFactory, proof);
-
- // add proof obligation to goal
- infFlowGoal.addFormula(poFormula, false, true);
- }
@Override
public boolean isApplicable(final Goal goal, final PosInOccurrence occurrence) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java
index 922529f64cf..0a2ec7e7f0e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java
@@ -16,25 +16,28 @@
import org.key_project.util.collection.ImmutableSLList;
import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
-public abstract class AbstractBuiltInRuleApp implements IBuiltInRuleApp {
+@NullMarked
+public abstract class AbstractBuiltInRuleApp implements IBuiltInRuleApp {
public static final AtomicLong PERF_EXECUTE = new AtomicLong();
public static final AtomicLong PERF_SET_SEQUENT = new AtomicLong();
- protected final BuiltInRule builtInRule;
+ protected final T builtInRule;
protected final PosInOccurrence pio;
- protected ImmutableList ifInsts;
+ protected @Nullable ImmutableList ifInsts;
- protected AbstractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio,
- ImmutableList ifInsts) {
+ protected AbstractBuiltInRuleApp(T rule, PosInOccurrence pio,
+ @Nullable ImmutableList ifInsts) {
this.builtInRule = rule;
this.pio = pio;
this.ifInsts = (ifInsts == null ? ImmutableSLList.nil() : ifInsts);
}
- protected AbstractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio) {
+ protected AbstractBuiltInRuleApp(T rule, PosInOccurrence pio) {
this(rule, pio, null);
}
@@ -51,7 +54,7 @@ public void setMutable(ImmutableList ifInsts) {
* returns the rule of this rule application
*/
@Override
- public BuiltInRule rule() {
+ public T rule() {
return builtInRule;
}
@@ -75,7 +78,7 @@ public void checkApplicability() {}
@Override
public void registerSkolemConstants(Namespace<@NonNull Function> fns) {}
- public abstract AbstractBuiltInRuleApp replacePos(PosInOccurrence newPos);
+ public abstract AbstractBuiltInRuleApp replacePos(PosInOccurrence newPos);
@Override
public abstract IBuiltInRuleApp setAssumesInsts(ImmutableList ifInsts);
@@ -91,10 +94,10 @@ public ImmutableList assumesInsts() {
* @see de.uka.ilkd.key.rule.IBuiltInRuleApp#tryToInstantiate(de.uka.ilkd.key.proof.Goal)
*/
@Override
- public abstract AbstractBuiltInRuleApp tryToInstantiate(Goal goal);
+ public abstract AbstractBuiltInRuleApp tryToInstantiate(Goal goal);
@Override
- public AbstractBuiltInRuleApp forceInstantiate(Goal goal) {
+ public AbstractBuiltInRuleApp forceInstantiate(Goal goal) {
return tryToInstantiate(goal);
}
@@ -125,7 +128,7 @@ public boolean complete() {
@Override
public String toString() {
- return "BuiltInRule: " + rule().name() + " at pos " + pio.subTerm();
+ return "BuiltInRule: %s at pos %s".formatted(rule().name(), pio.subTerm());
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractBuiltInRuleApp.java
index fd8cea8baa0..7f46ae5ccab 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractBuiltInRuleApp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractBuiltInRuleApp.java
@@ -19,18 +19,20 @@
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSet;
+import org.jspecify.annotations.Nullable;
+
/**
* Application of {@link AbstractLoopContractRule}.
*
* @author lanzinger
*/
-public abstract class AbstractLoopContractBuiltInRuleApp
- extends AbstractAuxiliaryContractBuiltInRuleApp {
+public abstract class AbstractLoopContractBuiltInRuleApp
+ extends AbstractAuxiliaryContractBuiltInRuleApp {
/**
* @see #getContract()
*/
- protected LoopContract contract;
+ protected @Nullable LoopContract contract;
/**
*
@@ -38,13 +40,13 @@ public abstract class AbstractLoopContractBuiltInRuleApp
* @param occurrence the position at which the rule is applied.
* @param ifInstantiations if instantiations.
*/
- protected AbstractLoopContractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence,
- ImmutableList ifInstantiations) {
+ protected AbstractLoopContractBuiltInRuleApp(T rule, PosInOccurrence occurrence,
+ @Nullable ImmutableList ifInstantiations) {
super(rule, occurrence, ifInstantiations);
}
@Override
- public LoopContract getContract() {
+ public @Nullable LoopContract getContract() {
return contract;
}
@@ -54,7 +56,7 @@ public LoopContract getContract() {
* @param rule the rule being applied.
* @return this.
*/
- public AbstractLoopContractBuiltInRuleApp tryToInstantiate(final Goal goal,
+ public AbstractLoopContractBuiltInRuleApp tryToInstantiate(final Goal goal,
final AbstractLoopContractRule rule) {
if (complete() || cannotComplete(goal)) {
return this;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java
index 385a0ae63dc..94d0d9b5d18 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java
@@ -6,7 +6,6 @@
import java.util.LinkedHashMap;
import java.util.Map;
-import de.uka.ilkd.key.informationflow.po.SymbolicExecutionPO;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.StatementBlock;
import de.uka.ilkd.key.java.statement.JavaStatement;
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 436e929ac85..f85b161a1ec 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
@@ -7,7 +7,6 @@
import java.util.Map.Entry;
import java.util.stream.Collectors;
-import de.uka.ilkd.key.informationflow.proof.InfFlowCheckInfo;
import de.uka.ilkd.key.java.*;
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
import de.uka.ilkd.key.java.expression.literal.BooleanLiteral;
@@ -38,8 +37,8 @@
import de.uka.ilkd.key.speclang.LoopContract;
import de.uka.ilkd.key.util.LinkedHashMap;
import de.uka.ilkd.key.util.MiscTools;
-import de.uka.ilkd.key.wd.BlockWellDefinedness;
+import org.jspecify.annotations.Nullable;
import org.key_project.logic.Name;
import org.key_project.logic.Namespace;
import org.key_project.logic.op.Function;
@@ -1363,9 +1362,9 @@ private static JTerm createAbruptTerms(final AuxiliaryContract.Terms terms,
* @param localIns all free local variables in the block.
* @return the well-definedness formula.
*/
- public JTerm setUpWdGoal(final Goal goal, final BlockContract contract, final JTerm update,
- final JTerm anonUpdate, final LocationVariable heap, final Function anonHeap,
- final ImmutableSet localIns) {
+ public JTerm setUpWdGoal(final @Nullable Goal goal, final BlockContract contract, final JTerm update,
+ final JTerm anonUpdate, final LocationVariable heap, final Function anonHeap,
+ final ImmutableSet localIns) {
// FIXME: Handling of \old-references needs to be investigated,
// however only completeness is lost, soundness is guaranteed
final BlockWellDefinedness bwd =
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractExternalBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractExternalBuiltInRuleApp.java
index 3adcd09603d..1a11fc36460 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractExternalBuiltInRuleApp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractExternalBuiltInRuleApp.java
@@ -13,19 +13,24 @@
import org.key_project.prover.sequent.PosInOccurrence;
import org.key_project.util.collection.ImmutableList;
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
/**
* Application of {@link BlockContractExternalRule}.
*
* @author lanzinger
*/
-public class BlockContractExternalBuiltInRuleApp extends AbstractBlockContractBuiltInRuleApp {
+@NullMarked
+public class BlockContractExternalBuiltInRuleApp
+ extends AbstractBlockContractBuiltInRuleApp {
/**
*
* @param rule the rule being applied.
* @param occurrence the position at which the rule is applied.
*/
- public BlockContractExternalBuiltInRuleApp(final BuiltInRule rule,
+ public BlockContractExternalBuiltInRuleApp(final T rule,
final PosInOccurrence occurrence) {
this(rule, occurrence, null, null, null, null);
}
@@ -39,14 +44,14 @@ public BlockContractExternalBuiltInRuleApp(final BuiltInRule rule,
* @param contract the contract being applied.
* @param heaps the heap context.
*/
- public BlockContractExternalBuiltInRuleApp(final BuiltInRule rule,
+ public BlockContractExternalBuiltInRuleApp(final T rule,
final PosInOccurrence occurrence,
- final ImmutableList ifInstantiations,
- final JavaStatement statement, final BlockContract contract,
- final List heaps) {
+ @Nullable final ImmutableList ifInstantiations,
+ @Nullable final JavaStatement statement,
+ @Nullable final BlockContract contract,
+ @Nullable final List