Tipping the foot into InfFlow refactoring

[wadoon]

Related Issue

InfFlow (and WD) are functionalities that tear furrows through the key.core module. Following packages/classes are directly depending on the infflow classes:

Isolating these functionalities could be a great improvement (a) for comprehensibility and (b) for modularity.

Current state: A prototype for evaluating the possible strategies:

Strategy: Hooks

In WileInvariantRule, InfFlow manipulates the "bodyGoal", while WD adds a fourth goal. The new hook WhileInvariantHook allows both functionalities by supplying too many parameters.

    /// A hook for manipulating the execution of the [WhileInvariantRule]. Allows addition or
    /// manipulation of sub-goals.
    ///
    /// @author weigl
    public interface WhileInvariantHook {
        /// This hook allows you to add new sub-goals for the [WhileInvariantRule].
        /// You get too many parameters. If you return a non-null consumer, a goal is created on
        /// which
        /// the returned consumer is applied. This allows for dynamic selection whether an
        /// additional is required.
        ///
        /// @return null if no additional [Goal] should be created.
        @Nullable
        default Consumer<Goal> createGoal(RuleApp ruleApp, Instantiation inst, Services services,
                LoopInvariantBuiltInRuleApp loopRuleApp, JavaBlock guardJb,
                ImmutableSet<LocationVariable> localIns, ImmutableSet<LocationVariable> localOuts,
                ImmutableList<AnonUpdateData> anonUpdateDatas, JTerm anonUpdate,
                List<LocationVariable> heapContext, JTerm anonHeap, JTerm localAnonUpdate) {
            return null;
        }

        /// Allows to rewrite the goals `init`, `preserve`, `terminate` of the [WhileInvariantRule] directly.
        default void rewriteStandardGoals(Services services, Goal init, Goal preserve,
                Goal terminate, Instantiation inst,
                LoopInvariantBuiltInRuleApp loopRuleApp, JavaBlock guardJb,
                ImmutableSet<LocationVariable> localIns,
                ImmutableSet<LocationVariable> localOuts,
                ImmutableList<AnonUpdateData> anonUpdateDatas,
                JTerm anonUpdate) {
        }
    }

In the end, I would propose the following base class:

class WhileInvariantRule : BuiltInRule {
  val hooks = findHooks(WhileInvariantRuleProcessor.class);

  @Override fun ImmutableList<Goal> applyTo(...) = 
       new WhileInvariantRuleProcessor(hooks, ...).call()
}

class WhileInvariantRuleProcessor(val hooks:Hooks, val pio:PIO, val goal:Goal)
   implements Callable<IList<Goals>> {
  // instantiations as member variable 

  init {
    // init instantiation, find heaps, etc...
  }

  @Override fun ImmutableList<Goal> call() {
      hooks.afterInit(this);
      val subGoalsTransformers = listOf(this::init, this::preserve, this:terminate)
                 + hooks.map { it.createGoal(this) }.filterNotNull();
      val subgoals = goal.split(subGoalsTransformers);
      hooks.afterSubGoals(this);
      return subgoals; 
  }
}

Strategy 2: Inheritance + Profile

BlockContractInternalRule had an isolated decision for validity in InfFlow proofs. Here, using inheritance is a good option. The downside is that we now need a "Java InfFlow Profile", because we need to disable the traditional BlockContractInternalRule and activate InfFlowBlockContractInternalRule:

public class JavaInfFlowProfile extends JavaProfile {
    public static final String NAME = "Java InfFlow Profile";

    @Override
    protected ImmutableList<BuiltInRule> initBuiltInRules() {
        var rules = super.initBuiltInRules();
        return rules.map(it -> {
            if (it == BlockContractInternalRule.INSTANCE) {
                return InfFlowBlockContractInternalRule.INSTANCE;
            }
            return it;
        });
    }
}

But in many places, BlockContractInternalRule is directly used:

AuxiliaryContractBuilders.java
BlockContractInternalBuiltInRuleApp.java
BlockContractInternalCompletion.java
BlockContractInternalRule.java
BlockContractValidityTermLabelUpdate.java
CurrentGoalViewMenu.java
InfFlowBlockContractInternalRule.java
JavaInfFlowProfile.java
JavaProfile.java
RemoveInCheckBranchesTermLabelRefactoring.java
StaticFeatureCollection.java
SymbolicExecutionTermLabelUpdate.java

This might result in strange behavior, e.g., the context menu CurrentGoalViewMenu has a special treatment for which it checks for identity with BlockContractInternalRule.INSTANCE.

Discussion

• Option 1:
  • + allows combining multiple extensions together. WD and Infflow can exist side-by-side in the same proof.
  • - increases the variant space of KeY. Extensions can be combined together, s.t. nobody has tested them.
  • - requires rather complex classes/types for handling the variance of built-in rules.
  • + keeps the number of Profiles low.
• Option 2:
  • + is natural option for Java ecosystem.
  • - requires opening/rewriting of built-in rules. Also, comparison of identity (rule == XXX.INSTANCE) needs to be removed.
  • + is also a canonical way for KeY. Profile is already built-in and allows the manipulation of much more than built-in rules, e.g., Taclet Options, Taclet paths, etc.
  • - arbitrary combination of multiple variants (WD, Infflow) is excluded.

Side Observations

• WD is globally in KeY, but it should rather be dependent on the proof settings.

    /**
     * This method checks, if well-definedness checks are generally turned on or off.
     *
     * @return true if on and false if off
     */
    public static boolean isOn() {
        final String setting =
            ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices().get(OPTION);
        if (setting == null) {
            return false;
        }
        if (setting.equals(OPTION + ":on")) {
            return true;
        } else if (setting.equals(OPTION + ":off")) {
            return false;
        } else {
            throw new RuntimeException(
                "The setting for the wdProofs-option is not valid: " + setting);
        }
    }

• Using Profiles can tighten the standardRules.key to the base case.

Intended Change

Isolating InfFlow (and WD) inside core into their own package s.t. these functionalities are concentrated and do not pollute the system architecture. InfFlow/WD was integrated using the "instanceOf" and patch-style, hence, you can find hard dependencies in many Built-in Rules to these classes.

We might not get infflow/wd inside external modules (b/c of cycle dependency to key.core), but an encapsulation should be achievable.

This might also be a great opportunity to sharpen the modularity of key.core.

Plan

• First step: Finding the right strategy

Type of pull request

• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
  • New extension points in key.core for deep functionality manipulation

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: ci
• I have checked that runtime performance has not deteriorated.
• For new Gradle modules: I added the Gradle module to the test matrix in
  .github/workflows/tests.yml