fixing TacletIndex change

* I do not understand why these proofs failed

Author: wadoon

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

@@ -3,9 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.informationflow.macros;
 
-import java.util.Map;
-import java.util.Set;
-
 import de.uka.ilkd.key.informationflow.ProofObligationVars;
 import de.uka.ilkd.key.informationflow.po.IFProofObligationVars;
 import de.uka.ilkd.key.java.Services;
@@ -17,16 +14,15 @@
 import de.uka.ilkd.key.macros.AbstractProofMacro;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
-import de.uka.ilkd.key.rule.NoPosTacletApp;
-import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.util.InfFlowProgVarRenamer;
-
 import org.key_project.logic.Named;
 import org.key_project.logic.Namespace;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableList;
 
+import java.util.Map;
+
 
 /**
  *
@@ -51,9 +47,9 @@ public String getDescription() {
 
     static JTerm calculateResultingTerm(Proof proof, IFProofObligationVars ifVars, Goal initGoal) {
         final JTerm[] goalFormulas1 =
-            buildExecution(ifVars.c1, ifVars.getMapFor(ifVars.c1), proof.openGoals(), initGoal);
+                buildExecution(ifVars.c1, ifVars.getMapFor(ifVars.c1), proof.openGoals(), initGoal);
         final JTerm[] goalFormulas2 =
-            buildExecution(ifVars.c2, ifVars.getMapFor(ifVars.c2), proof.openGoals(), initGoal);
+                buildExecution(ifVars.c2, ifVars.getMapFor(ifVars.c2), proof.openGoals(), initGoal);
         final TermBuilder tb = proof.getServices().getTermBuilder();
         JTerm composedStates = tb.ff();
         for (int i = 0; i < goalFormulas1.length; i++) {
@@ -69,7 +65,7 @@ static JTerm calculateResultingTerm(Proof proof, IFProofObligationVars ifVars, G
      * Merge namespaces.
      *
      * @param initiatingProof the initiating proof
-     * @param sideProof the side proof
+     * @param sideProof       the side proof
      */
     protected final void mergeNamespaces(Proof initiatingProof, Proof sideProof) {
         NamespaceSet initiatingProofNS = initiatingProof.getServices().getNamespaces();
@@ -95,11 +91,11 @@ private final <E extends Named> void mergeNamespace(Namespace<E> tar, Namespace<
     }
 
     private static JTerm[] buildExecution(ProofObligationVars c, Map<JTerm, JTerm> vsMap,
-            ImmutableList<Goal> symbExecGoals, Goal initGoal) {
+                                          ImmutableList<Goal> symbExecGoals, Goal initGoal) {
         Services services = initGoal.proof().getServices();
         final JTerm[] goalFormulas = buildFormulasFromGoals(symbExecGoals);
         final InfFlowProgVarRenamer renamer = new InfFlowProgVarRenamer(goalFormulas, vsMap,
-            c.postfix, initGoal, services.getOverlay(initGoal.getLocalNamespaces()));
+                c.postfix, initGoal, services.getOverlay(initGoal.getLocalNamespaces()));
         final JTerm[] renamedGoalFormulas = renamer.renameVariablesAndSkolemConstants();
         JTerm[] result = new JTerm[renamedGoalFormulas.length];
         final TermBuilder tb = services.getTermBuilder();
@@ -137,13 +133,11 @@ private static JTerm buildFormulaFromGoal(Goal symbExecGoal) {
     protected static void addContractApplicationTaclets(Goal initiatingGoal, Proof symbExecProof) {
         final ImmutableList<Goal> openGoals = symbExecProof.openGoals();
         for (final Goal openGoal : openGoals) {
-            final Set<NoPosTacletApp> ruleApps = openGoal.indexOfTaclets().allNoPosTacletApps();
-            for (final NoPosTacletApp ruleApp : ruleApps) {
-                final Taclet t = ruleApp.taclet();
-                if (t.getSurviveSymbExec()) {
-                    initiatingGoal.addTaclet(t, SVInstantiations.EMPTY_SVINSTANTIATIONS, true);
-                }
-            }
+            openGoal.indexOfTaclets()
+                    .allNoPosTacletAppsStream()
+                    .filter(it -> it.taclet().getSurviveSymbExec())
+                    .forEach(it ->
+                            initiatingGoal.addTaclet(it.taclet(), SVInstantiations.EMPTY_SVINSTANTIATIONS, true));
         }
     }
 }

key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java

@@ -267,7 +267,7 @@ public Object clone() {
 
     @Override
     public Set<NoPosTacletApp> allNoPosTacletApps() {
-        return allNoPosTacletAppsStream().collect(Collectors.toUnmodifiableSet());
+        return new HashSet<>(allNoPosTacletAppsStream().collect(Collectors.toUnmodifiableSet()));
     }
 
     public Stream<NoPosTacletApp> allNoPosTacletAppsStream() {
@@ -506,12 +506,10 @@ public ImmutableList<NoPosTacletApp> getNoFindTaclet(RuleFilter filter,
      */
     @Override
     public NoPosTacletApp lookup(Name name) {
-        for (NoPosTacletApp tacletApp : allNoPosTacletApps()) {
-            if (tacletApp.taclet().name().equals(name)) {
-                return tacletApp;
-            }
-        }
-        return null;
+        return allNoPosTacletAppsStream()
+                .filter(tacletApp -> tacletApp.taclet().name().equals(name))
+                .findAny()
+                .orElse(null);
     }
 
 

key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java

@@ -523,6 +523,9 @@ private TacletApp constructTacletApp(TacletAppIntermediate currInterm, Goal curr
         }
 
         ourApp = constructInsts(ourApp, currGoal, currInterm.getInsts(), services);
+        if(ourApp==null) {
+            System.out.println("§sdsfs");
+        }
 
         ImmutableList<AssumesFormulaInstantiation> ifFormulaList = ImmutableSLList.nil();
         for (String ifFormulaStr : currInterm.getIfSeqFormulaList()) {

key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java

@@ -119,8 +119,7 @@ private ImmutableList<Taclet> tacletsForRuleSet(Proof proof, String ruleSetName,
         ImmutableList<Taclet> result = ImmutableSLList.nil();
 
         // collect apps present in all open goals
-        Set<NoPosTacletApp> allApps = new HashSet<>(
-            proof.openGoals().head().ruleAppIndex().tacletIndex().allNoPosTacletApps());
+        Set<NoPosTacletApp> allApps = proof.openGoals().head().ruleAppIndex().tacletIndex().allNoPosTacletApps();
         for (Goal goal : proof.openGoals().tail()) {
             allApps.retainAll(goal.ruleAppIndex().tacletIndex().allNoPosTacletApps());
         }

key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ValueInjector.java

@@ -183,7 +183,6 @@ private void injectIntoField(ProofScriptArgument meta, ScriptCommandAst args, Ob
 
         if (meta.isFlag()) {
             val = args.namedArgs().get(meta.getName());
-            System.out.println("X" + val + "  " + args.namedArgs() + "  " + meta.getName());
             if (val == null) {
                 // can also be given w/o colon or equal sign, e.g., "command hide;"
                 var stringStream = args.positionalArgs().stream()

key.core/tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof

@@ -1,68 +1,105 @@
 \profile "Java Profile";
 
 \settings {
-"#Proof-Settings-Config-File
-#Wed Apr 12 13:28:59 CEST 2023
-[NewSMT]NoTypeHierarchy=false
-[Labels]UseOriginLabels=true
-[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
-[NewSMT]Presburger=false
-[SMTSettings]invariantForall=false
-[Strategy]ActiveStrategy=JavaCardDLStrategy
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
-[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
-[Choice]DefaultChoices=JavaCard-JavaCard\\:on, Strings-Strings\\:on, assertions-assertions\\:safe, bigint-bigint\\:on, finalFields-finalFields\\:immutable, floatRules-floatRules\\:strictfpOnly, initialisation-initialisation\\:disableStaticInitialisation, intRules-intRules\\:arithmeticSemanticsIgnoringOF, integerSimplificationRules-integerSimplificationRules\\:full, javaLoopTreatment-javaLoopTreatment\\:efficient, mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off, methodExpansion-methodExpansion\\:modularOnly, modelFields-modelFields\\:treatAsAxiom, moreSeqRules-moreSeqRules\\:on, permissions-permissions\\:off, programRules-programRules\\:Java, reach-reach\\:on, runtimeExceptions-runtimeExceptions\\:ban, sequences-sequences\\:on, wdChecks-wdChecks\\:off, wdOperator-wdOperator\\:L
-[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET
-[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
-[SMTSettings]UseBuiltUniqueness=false
-[SMTSettings]explicitTypeHierarchy=false
-[SMTSettings]instantiateHierarchyAssumptions=true
-[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS
-[SMTSettings]SelectedTaclets=
-[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
-[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
-[Strategy]MaximumNumberOfAutomaticApplications=10000
-[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
-[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED
-[SMTSettings]useConstantsForBigOrSmallIntegers=true
-[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
-[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
-[Strategy]Timeout=-1
-[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
-[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
-[SMTSettings]useUninterpretedMultiplication=true
-[NewSMT]sqrtSMTTranslation=SMT
-[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
-[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
-[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
-[NewSMT]identifier=OPEN
-[SMTSettings]maxGenericSorts=2
-[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
-[NewSMT]Axiomatisations=false
-[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
-[SMTSettings]integersMinimum=-2147483645
-[StrategyProperty]VBT_PHASE=VBT_SYM_EX
-[SMTSettings]integersMaximum=2147483645
-"
-}
+    "Choice" : {
+        "JavaCard" : "JavaCard:on",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "finalFields" : "finalFields:immutable",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules:full",
+        "javaLoopTreatment" : "javaLoopTreatment:efficient",
+        "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
+        "methodExpansion" : "methodExpansion:modularOnly",
+        "modelFields" : "modelFields:treatAsAxiom",
+        "moreSeqRules" : "moreSeqRules:on",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "soundDefaultContracts" : "soundDefaultContracts:on",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+    },
+    "Labels" : {
+        "UseOriginLabels" : true
+    },
+    "NewSMT" : {
+        "Axiomatisations" : "false",
+        "NoTypeHierarchy" : "false",
+        "Presburger" : "false",
+        "identifier" : "OPEN",
+        "sqrtSMTTranslation" : "SMT"
+    },
+    "SMTSettings" : {
+        "SelectedTaclets" : [
+            
+        ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+    },
+    "Strategy" : {
+        "ActiveStrategy" : "Modular JavaDL Strategy",
+        "MaximumNumberOfAutomaticApplications" : 10000,
+        "Timeout" : -1,
+        "options" : {
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
+            "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
+            "MPS_OPTIONS_KEY" : "MPS_MERGE",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+        }
+    }
+} 
+
 
-\proofObligation {
-	"name": "disjointArrayRangeAllFields1",
-	"class": "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput",
- }
+
+\proofObligation 
+// 
+{
+    "class" : "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput",
+    "name" : "disjointArrayRangeAllFields1"
+}
 
 \proof {
 (keyLog "0" (keyUser "Julian" ) (keyVersion "80a871ca3bac8bb405ecc216fcb6fa9ef6f8a395"))
+(keyLog "1" (keyUser "weigl" ) (keyVersion "1df32008ebda9fe2684e1a5eb5e44bdd4c398d8f"))
+(keyLog "2" (keyUser "weigl" ) (keyVersion "1df32008ebda9fe2684e1a5eb5e44bdd4c398d8f"))
 
-(autoModeTime "0")
+(autoModeTime "15")
 
 (branch "dummy ID"
 (rule "equiv_right" (formula "1") (newnames "f_o1,f_o2,f_lower2,f_upper2") (userinteraction))
 (branch "Case '->'"
    (rule "notRight" (formula "2"))
    (rule "andLeft" (formula "1"))
-   (rule "equalityToElementOf" (formula "3") (inst "ov=ov") (inst "fv=fv") (userinteraction))
+   (rule "equalityToElementOf" (formula "3") (inst "fv=fv") (inst "ov=ov") (userinteraction))
     (builtin "One Step Simplification" (formula "3"))
    (rule "eqSymm" (formula "1"))
    (rule "inEqSimp_commuteLeq" (formula "2"))
@@ -108,6 +145,8 @@
    (rule "commute_or_2" (formula "3") (term "0,0,0,0"))
    (rule "commute_or_2" (formula "3") (term "0,0,0"))
     (builtin "One Step Simplification" (formula "3"))
+   (rule "castDel" (formula "3") (term "0,0,0,0,0"))
+    (builtin "One Step Simplification" (formula "3"))
    (rule "polySimp_addComm1" (formula "3") (term "1"))
    (rule "add_literals" (formula "3") (term "0,1"))
    (rule "add_zero_left" (formula "3") (term "1"))
@@ -131,16 +170,16 @@
    (rule "polySimp_pullOutFactor1b" (formula "3") (term "0"))
    (rule "add_literals" (formula "3") (term "1,1,0"))
    (rule "times_zero_1" (formula "3") (term "1,0"))
-   (rule "add_zero_right" (formula "3") (term "0"))
+   (rule "add_literals" (formula "3") (term "0"))
    (rule "leq_literals" (formula "3"))
    (rule "closeFalse" (formula "3"))
 )
 (branch "Case '<-'"
-   (rule "equalityToElementOfRight" (formula "2") (inst "ov=ov") (inst "fv=fv") (userinteraction))
+   (rule "equalityToElementOfRight" (formula "2") (inst "fv=fv") (inst "ov=ov") (userinteraction))
     (builtin "One Step Simplification" (formula "2"))
    (rule "notLeft" (formula "1"))
-   (rule "allRight" (formula "2") (inst "sk=ov_0"))
-   (rule "allRight" (formula "2") (inst "sk=fv_0"))
+   (rule "allRight" (formula "2") (inst "sk=ov_0:java.lang.Object"))
+   (rule "allRight" (formula "2") (inst "sk=fv_0:Field"))
    (rule "notRight" (formula "2"))
    (rule "eqSymm" (formula "2") (term "0"))
    (rule "inEqSimp_commuteLeq" (formula "2") (term "1"))
@@ -150,7 +189,7 @@
    (rule "applyEq" (formula "2") (term "0") (ifseqformula "1"))
    (rule "elementOfArrayRange" (formula "2") (inst "iv=iv"))
    (rule "andLeft" (formula "2"))
-   (rule "exLeft" (formula "3") (inst "sk=iv_0"))
+   (rule "exLeft" (formula "3") (inst "sk=iv_0:int"))
    (rule "andLeft" (formula "3"))
    (rule "andLeft" (formula "3"))
    (rule "eqSymm" (formula "2"))