Modularization: InfFlow and WD as separate modules

.github/workflows/tests.yml

@@ -80,7 +80,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs ]
+        test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testRunAllWdProofs ]
         os: [ ubuntu-latest ]
         java: [ 21 ]
     runs-on: ${{ matrix.os }}

key.core.infflow/build.gradle

@@ -0,0 +1,25 @@
+
+
+dependencies {
+    api(project(":key.core"))
+    testImplementation(project(":key.core").sourceSets.test.output)
+}
+
+
+tasks.register('testRunAllInfProofs', Test) {
+    description = 'Prove/reload all keyfiles tagged for regression testing'
+    group = "verification"
+    filter {
+        includeTestsMatching "RunAllProofsInfFlow"
+    }
+}
+
+
+def rapDir = layout.buildDirectory.dir("generated-src/rap/").getOrNull()
+sourceSets.test.java.srcDirs(rapDir)
+
+tasks.register('generateRAPUnitTests', JavaExec) {
+    classpath = sourceSets.test.runtimeClasspath
+    mainClass.set("de.uka.ilkd.key.informationflow.GenerateUnitTests")
+    args(rapDir)
+}

key.core.infflow/src/main/java/de/uka/ilkd/key/InfFlowStatistics.java

@@ -0,0 +1,58 @@
+/* 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;
+
+import java.util.List;
+
+import de.uka.ilkd.key.informationflow.proof.InfFlowProof;
+import de.uka.ilkd.key.informationflow.proof.SideProofStatistics;
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.Statistics;
+
+import org.jspecify.annotations.NullMarked;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (8/3/25)
+ */
+@NullMarked
+public class InfFlowStatistics extends Statistics {
+    private boolean sideProofs;
+    private Statistics stat;
+
+    protected InfFlowStatistics(int nodes, int branches, int cachedBranches, int interactiveSteps,
+            int symbExApps, int quantifierInstantiations, int ossApps, int mergeRuleApps,
+            int totalRuleApps, int smtSolverApps, int dependencyContractApps,
+            int operationContractApps, int blockLoopContractApps, int loopInvApps,
+            long autoModeTimeInMillis, long timeInMillis, float timePerStepInMillis) {
+        super(nodes, branches, cachedBranches, interactiveSteps, symbExApps,
+            quantifierInstantiations, ossApps, mergeRuleApps, totalRuleApps, smtSolverApps,
+            dependencyContractApps, operationContractApps, blockLoopContractApps, loopInvApps,
+            autoModeTimeInMillis, timeInMillis, timePerStepInMillis);
+    }
+
+    public InfFlowStatistics(List<Node> startNodes) {
+        super(startNodes);
+    }
+
+    @Override
+    protected void generateSummary(Proof proof) {
+        super.generateSummary(proof);
+        if (proof instanceof InfFlowProof ifp) { // TODO: get rid of that instanceof by subclassing
+            generateSummary(ifp);
+        }
+    }
+
+    protected void generateSummary(InfFlowProof proof) {
+        sideProofs = proof.hasSideProofs();
+        if (sideProofs) {
+            final long autoTime = proof.getAutoModeTime()
+                    + proof.getSideProofStatistics().autoModeTimeInMillis;
+            final SideProofStatistics side = proof.getSideProofStatistics()
+                    .add(this).setAutoModeTime(autoTime);
+            stat = create(side, proof.getCreationTime());
+        }
+    }
+}

key.core.infflow/src/main/java/de/uka/ilkd/key/InfFlowUseOperationContractRule.java

@@ -0,0 +1,123 @@
+/* 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;
+
+import de.uka.ilkd.key.informationflow.ProofObligationVars;
+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.InfFlowMethodContractTacletBuilder;
+import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.rules.ComplexJustificationable;
+import de.uka.ilkd.key.rule.Taclet;
+import de.uka.ilkd.key.rule.UseOperationContractRule;
+import de.uka.ilkd.key.rule.inst.SVInstantiations;
+
+import org.key_project.logic.Name;
+import org.key_project.prover.rules.RuleApp;
+import org.key_project.prover.sequent.SequentFormula;
+import org.key_project.util.collection.ImmutableList;
+
+import org.jspecify.annotations.NullMarked;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (8/3/25)
+ */
+@NullMarked
+public class InfFlowUseOperationContractRule extends UseOperationContractRule
+        implements ComplexJustificationable {
+    private static final Name NAME = new Name("InfFlow Use Operation Contract");
+
+    public static InfFlowUseOperationContractRule INSTANCE = new InfFlowUseOperationContractRule();
+
+    protected InfFlowUseOperationContractRule() {
+    }
+
+    @Override
+    public Name name() {
+        return NAME;
+    }
+
+    @Override
+    public ImmutableList<Goal> apply(Goal goal, RuleApp ruleApp) {
+        return new InfFlowUseOperationContractRuleApplier(goal, ruleApp).apply();
+    }
+
+    protected static class InfFlowUseOperationContractRuleApplier
+            extends UseOperationContractRuleApplier {
+        protected InfFlowUseOperationContractRuleApplier(Goal goal, RuleApp ruleApp) {
+            super(goal, ruleApp);
+        }
+
+        @Override
+        protected JTerm getFinalPreTerm() {
+            // termination has already been shown in the functional proof,
+            // thus we do not need to show it again in information flow proofs.
+            return tb.applySequential(new JTerm[] { inst.u(), atPreUpdates },
+                tb.and(new JTerm[] { pre, reachableState }));
+        }
+
+        private void applyInfFlow(Goal goal) {
+            if (!InfFlowCheckInfo.isInfFlow(goal)) {
+                return;
+            }
+
+            var exception = tb.var(excVar);
+
+            // prepare information flow analysis
+            assert anonUpdateDatas.size() == 1
+                    : "information flow extension " + "is at the moment not "
+                        + "compatible with the " + "non-base-heap setting";
+            AnonUpdateData anonUpdateData = anonUpdateDatas.head();
+
+            final JTerm heapAtPre = anonUpdateData.methodHeapAtPre();
+            final JTerm heapAtPost = anonUpdateData.methodHeap();
+
+            // generate proof obligation variables
+            final boolean hasSelf = contractSelf != null;
+            final boolean hasRes = contractResult != null;
+            final boolean hasExc = exception != null;
+
+            final StateVars preVars = new StateVars(hasSelf ? contractSelf : null, contractParams,
+                hasRes ? contractResult : null, hasExc ? exception : null, heapAtPre, mby);
+            final StateVars postVars = new StateVars(hasSelf ? contractSelf : null, contractParams,
+                hasRes ? contractResult : null, hasExc ? exception : null, heapAtPost, mby);
+            final ProofObligationVars poVars = new ProofObligationVars(preVars, postVars, services);
+
+            // generate information flow contract application predicate
+            // and associated taclet
+            InfFlowMethodContractTacletBuilder ifContractBuilder =
+                new InfFlowMethodContractTacletBuilder(services);
+            ifContractBuilder.setContract(contract);
+            ifContractBuilder.setContextUpdate(atPreUpdates, inst.u());
+            ifContractBuilder.setProofObligationVars(poVars);
+
+            JTerm contractApplPredTerm = ifContractBuilder.buildContractApplPredTerm();
+            Taclet informationFlowContractApp = ifContractBuilder.buildTaclet(goal);
+
+            // add term and taclet to post goal
+            goal.addFormula(new SequentFormula(contractApplPredTerm), true, false);
+            goal.addTaclet(informationFlowContractApp, SVInstantiations.EMPTY_SVINSTANTIATIONS,
+                true);
+
+            // information flow proofs might get easier if we add the (proved)
+            // method contract precondition as an assumption to the post goal
+            // (in case the precondition cannot be proved easily)
+            goal.addFormula(new SequentFormula(finalPreTerm), true, false);
+            final InfFlowProof proof = (InfFlowProof) goal.proof();
+            proof.addIFSymbol(contractApplPredTerm);
+            proof.addIFSymbol(informationFlowContractApp);
+            proof.addGoalTemplates(informationFlowContractApp);
+        }
+
+
+        @Override
+        protected void createPostGoal(Goal postGoal) {
+            super.createPostGoal(postGoal);
+            applyInfFlow(postGoal);
+        }
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FocusIsSubFormulaOfInfFlowContractAppFeature.java → key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/FocusIsSubFormulaOfInfFlowContractAppFeature.java

@@ -1,11 +1,12 @@
 /* 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.strategy.feature;
+package de.uka.ilkd.key.informationflow;
 
 import de.uka.ilkd.key.informationflow.rule.executor.InfFlowContractAppTacletExecutor;
 import de.uka.ilkd.key.logic.DefaultVisitor;
 import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.logic.equality.RenamingTermProperty;
 import de.uka.ilkd.key.rule.TacletApp;
 
 import org.key_project.logic.Term;
@@ -21,7 +22,6 @@
 
 import org.jspecify.annotations.NonNull;
 
-import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
 
 
 /**
@@ -90,7 +90,8 @@ public SubFormulaVisitor(Term potentialSub) {
 
         @Override
         public void visit(Term visited) {
-            isSubFormula |= RENAMING_TERM_PROPERTY.equalsModThisProperty(visited, potentialSub);
+            isSubFormula |= RenamingTermProperty.RENAMING_TERM_PROPERTY
+                    .equalsModThisProperty(visited, potentialSub);
         }
 
 

key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java → key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/InfFlowContractAppFeature.java

@@ -1,7 +1,7 @@
 /* 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.strategy.feature;
+package de.uka.ilkd.key.informationflow;
 
 import java.util.ArrayList;
 import java.util.Iterator;

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/InfFlowProfileResolver.java

@@ -0,0 +1,19 @@
+/* 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;
+
+import de.uka.ilkd.key.proof.init.DefaultProfileResolver;
+import de.uka.ilkd.key.proof.init.Profile;
+
+public class InfFlowProfileResolver implements DefaultProfileResolver {
+    @Override
+    public String getProfileName() {
+        return JavaInfFlowProfile.PROFILE_ID;
+    }
+
+    @Override
+    public Profile getDefaultProfile() {
+        return new JavaInfFlowProfile();
+    }
+}

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/JavaInfFlowProfile.java

@@ -0,0 +1,62 @@
+/* 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;
+
+import de.uka.ilkd.key.InfFlowUseOperationContractRule;
+import de.uka.ilkd.key.informationflow.rule.InfFlowBlockContractInternalRule;
+import de.uka.ilkd.key.informationflow.rule.InfFlowWhileInvariantRule;
+import de.uka.ilkd.key.proof.init.JavaProfile;
+import de.uka.ilkd.key.rule.*;
+
+import org.key_project.util.collection.ImmutableList;
+
+/**
+ * This profile sets up KeY for verification of JavaCard programs.
+ */
+public class JavaInfFlowProfile extends JavaProfile {
+    public static final String NAME = "Java InfFlow Profile";
+    public static final String PROFILE_ID = "java-infflow";
+
+    @Override
+    public String ident() {
+        return PROFILE_ID;
+    }
+
+    @Override
+    public String displayName() {
+        return NAME;
+    }
+
+    @Override
+    public String description() {
+        return "Profile with Built-In rules for Information Flow proofs. " +
+            "Required for 'non-inference' proof obligations.";
+    }
+
+    @Override
+    public UseOperationContractRule getUseOperationContractRule() {
+        return InfFlowUseOperationContractRule.INSTANCE;
+    }
+
+    @Override
+    protected ImmutableList<BuiltInRule> initBuiltInRules() {
+        var rules = super.initBuiltInRules();
+        return rules.map(it -> {
+            if (it == BlockContractInternalRule.INSTANCE) {
+                return InfFlowBlockContractInternalRule.INSTANCE;
+            }
+            if (it instanceof UseOperationContractRule) {
+                return InfFlowUseOperationContractRule.INSTANCE;
+            }
+            if (it instanceof WhileInvariantRule) {
+                return InfFlowWhileInvariantRule.INSTANCE;
+            }
+
+            return it;
+        })
+                .filter(it -> it != BlockContractExternalRule.INSTANCE)
+                .filter(it -> !(it instanceof LoopScopeInvariantRule))
+                .filter(it -> !(it instanceof LoopContractExternalRule));
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/proof/init/ProofObligationVars.java → key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/ProofObligationVars.java

@@ -1,7 +1,7 @@
 /* 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.proof.init;
+package de.uka.ilkd.key.informationflow;
 
 import de.uka.ilkd.key.informationflow.proof.init.StateVars;
 import de.uka.ilkd.key.java.JavaInfo;
@@ -20,6 +20,8 @@
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
+import org.jspecify.annotations.Nullable;
+
 
 /**
  *
@@ -76,7 +78,7 @@ public ProofObligationVars(StateVars pre, StateVars post, JTerm exceptionParamet
     }
 
     public ProofObligationVars(StateVars pre, StateVars post, JTerm exceptionParameter,
-            ImmutableList<JTerm> formalParams, TermBuilder tb) {
+            @Nullable ImmutableList<JTerm> formalParams, TermBuilder tb) {
         this.pre = pre;
         this.post = post;
         this.exceptionParameter = exceptionParameter;

key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java → key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/impl/InformationFlowContractImpl.java

@@ -1,7 +1,7 @@
 /* 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.speclang;
+package de.uka.ilkd.key.informationflow.impl;
 
 import java.util.Iterator;
 import java.util.List;
@@ -21,6 +21,9 @@
 import de.uka.ilkd.key.proof.init.ContractPO;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.ProofOblInput;
+import de.uka.ilkd.key.speclang.Contract;
+import de.uka.ilkd.key.speclang.ContractFactory;
+import de.uka.ilkd.key.speclang.infflow.InformationFlowContract;
 import de.uka.ilkd.key.util.InfFlowSpec;
 
 import org.key_project.util.collection.ImmutableList;