Fix for slicing in case of dynamic taclet applications and renamings

key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java

@@ -203,6 +203,18 @@ private IBuiltInRuleApp constructBuiltinApp(Node originalStep, Goal currGoal)
         return ourApp;
     }
 
+    private NoPosTacletApp lookupIntroducedTaclet(TacletApp app, Goal goal) {
+        for (Node n = goal.node(); n != null; n = n.parent()) {
+            for (NoPosTacletApp introduced : n.getLocalIntroducedRules()) {
+                if (EqualityModuloProofIrrelevancy.equalsModProofIrrelevancy(introduced,
+                    app)) {
+                    return introduced;
+                }
+            }
+        }
+        return null;
+    }
+
     /**
      * Construct a new taclet application based on a step in the original proof
      *
@@ -228,16 +240,21 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) {
             // find the correct taclet
             for (NoPosTacletApp partialApp : currGoal.indexOfTaclets()
                     .getPartialInstantiatedApps()) {
-                System.out.println();
                 if (EqualityModuloProofIrrelevancy.equalsModProofIrrelevancy(partialApp,
                     originalTacletApp)) {
                     ourApp = partialApp;
                     break;
                 }
             }
+
+            if (ourApp == null) {
+                ourApp = lookupIntroducedTaclet(originalTacletApp, currGoal);
+            }
+
             if (ourApp == null) {
                 ourApp = currGoal.indexOfTaclets().lookup(tacletName);
             }
+
             if (ourApp == null) {
                 throw new IllegalStateException(
                     "proof replayer failed to find dynamically added taclet at original node "

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

@@ -490,6 +490,13 @@ public static boolean equalsModProofIrrelevancy(org.key_project.prover.rules.Tac
             return false;
         }
 
+        if (_this instanceof FindTaclet _thisFind) {
+            final FindTaclet thatFind = (FindTaclet) that;
+            if (!_thisFind.find().equalsModProperty(thatFind.find(), PROOF_IRRELEVANCY_PROPERTY)) {
+                return false;
+            }
+        }
+
         if ((_this.assumesSequent() == null && that.assumesSequent() != null)
                 || (_this.assumesSequent() != null && that.assumesSequent() == null)) {
             return false;
@@ -523,8 +530,16 @@ && equalsModProofIrrelevancy(if1.head(), if2.head())) {
      * @return the hash code modulo proof irrelevancy for the given argument
      */
     public static int hashCodeModProofIrrelevancy(org.key_project.prover.rules.Taclet taclet) {
-        Sequent sequentFormulas = taclet.assumesSequent();
-        return hashCodeModProofIrrelevancy(sequentFormulas.getFormulaByNr(1));
+        int hashCode = 17;
+        hashCode += 17 * (taclet.getChoices().hashCode() + 17 * taclet.goalTemplates().size());
+        if (taclet instanceof final FindTaclet find) {
+            hashCode += 17 * PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(find.find());
+        }
+        final Sequent assumesSequent = taclet.assumesSequent();
+        if (assumesSequent != null && !assumesSequent.isEmpty()) {
+            hashCode += 17 * hashCodeModProofIrrelevancy(assumesSequent.getFormulaByNr(1));
+        }
+        return hashCode;
     }
 
 

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/Random.java

@@ -0,0 +1,96 @@
+package java.util;
+
+public class Random implements java.util.random.RandomGenerator, java.io.Serializable {
+
+    // @Override
+    public void setSeed(long seed);
+
+    // @Override
+    public boolean isDeprecated();
+
+    // @Override
+    public void nextBytes(byte[] bytes);
+
+    // @Override
+    public int nextInt();
+
+    public int nextInt(int bound);
+
+    // @Override
+    public int nextInt(int origin, int bound);
+
+    // @Override
+    public long nextLong();
+    // @Override
+    public long nextLong(long bound);
+
+    // @Override
+    public long nextLong(long origin, long bound);
+
+    // @Override
+    public boolean nextBoolean();
+
+    // @Override
+    public float nextFloat();
+
+    // @Override
+    public float nextFloat(float bound);
+
+    // @Override
+    public float nextFloat(float origin, float bound);
+
+    // @Override
+    public double nextDouble();
+
+    // @Override
+    public double nextDouble(double bound);
+
+    // @Override
+    public double nextDouble(double origin, double bound);
+
+    // @Override
+    public double nextExponential();
+
+    // @Override
+    public double nextGaussian();
+
+    // @Override
+    public double nextGaussian(double mean, double stddev);
+
+//    // @Override
+//    public IntStream ints(long streamSize);
+//
+//    // @Override
+//    public IntStream ints();
+//
+//    // @Override
+//    public IntStream ints(long streamSize, int randomNumberOrigin, int randomNumberBound);
+//
+//    // @Override
+//    public IntStream ints(int randomNumberOrigin, int randomNumberBound);
+//
+//    // @Override
+//    public LongStream longs(long streamSize);
+//
+//    // @Override
+//    public LongStream longs();
+//
+//    // @Override
+//    public LongStream longs(long streamSize, long randomNumberOrigin, long randomNumberBound);
+//
+//    // @Override
+//    public LongStream longs(long randomNumberOrigin, long randomNumberBound);
+//    // @Override
+//    public DoubleStream doubles(long streamSize);
+//
+//    // @Override
+//    public DoubleStream doubles();
+//
+//    // @Override
+//    public DoubleStream doubles(long streamSize, double randomNumberOrigin, double randomNumberBound);
+//    // @Override
+//    public DoubleStream doubles(double randomNumberOrigin, double randomNumberBound);
+
+    // @Override
+    public String toString();
+}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/random/RandomGenerator.java

@@ -0,0 +1,80 @@
+package java.util.random;
+
+public interface RandomGenerator {
+
+//    public static RandomGenerator of(String name);
+//
+//    public static RandomGenerator getDefault();
+
+    public void setSeed(long seed);
+
+    public boolean isDeprecated();
+
+    public void nextBytes(byte[] bytes);
+
+    public int nextInt();
+
+    public int nextInt(int bound);
+
+    public int nextInt(int origin, int bound);
+
+    public long nextLong();
+
+    public long nextLong(long bound);
+
+    public long nextLong(long origin, long bound);
+
+    public boolean nextBoolean();
+
+    public float nextFloat();
+
+    public float nextFloat(float bound);
+
+    public float nextFloat(float origin, float bound);
+
+    public double nextDouble();
+
+    public double nextDouble(double bound);
+
+    public double nextDouble(double origin, double bound);
+
+    public double nextExponential();
+
+    public double nextGaussian();
+
+    public double nextGaussian(double mean, double stddev);
+
+//   
+//    public IntStream ints(long streamSize);
+//
+//    
+//    public IntStream ints();
+//
+//    
+//    public IntStream ints(long streamSize, int randomNumberOrigin, int randomNumberBound);
+//
+//    
+//    public IntStream ints(int randomNumberOrigin, int randomNumberBound);
+//
+//    
+//    public LongStream longs(long streamSize);
+//
+//    
+//    public LongStream longs();
+//
+//    
+//    public LongStream longs(long streamSize, long randomNumberOrigin, long randomNumberBound);
+//
+//    
+//    public LongStream longs(long randomNumberOrigin, long randomNumberBound);
+//    
+//    public DoubleStream doubles(long streamSize);
+//
+//    
+//    public DoubleStream doubles();
+//
+//    
+//    public DoubleStream doubles(long streamSize, double randomNumberOrigin, double randomNumberBound);
+//    
+//    public DoubleStream doubles(double randomNumberOrigin, double randomNumberBound);
+}

key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java

@@ -1213,6 +1213,14 @@ public static ProofCollection automaticJavaDL() throws IOException {
         g.loadable("Java/Records/Use.key");
         g.loadable("Java/Records/Constructor.key");
 
+        g = c.group("StipuLa");
+        g.provable("case-studies/stipula/behavior_run_bet.key");
+        g.provable("case-studies/stipula/behavior_run_bike.key");
+        g.provable("case-studies/stipula/behavior_run_donation.key");
+        g.provable("case-studies/stipula/behavior_run_license.key");
+        g.provable("case-studies/stipula/behavior_run_loanForUse.key");
+
+
         // use for debugging purposes.
         // c.keep("VSTTE10");
         String s = System.getenv(ENV_KEY_RAP_FUN_KEEP);

key.ncore.calculus/src/main/java/org/key_project/prover/sequent/Sequent.java

@@ -502,6 +502,6 @@ public int getChildCount() {
     @Override
     public @NonNull SyntaxElement getChild(int n) {
         // Could also make SequentFormula a SyntaxElement; no special reason for current decision.
-        return getFormulaByNr(n - 1).formula();
+        return getFormulaByNr(n + 1).formula();
     }
 }

key.ui/examples/case-studies/stipula/README.txt

@@ -0,0 +1,7 @@
+These are the input files for the StipuLa case study
+
+Journal Article (currently under review)
+
+The Java files are translations from StipuLa contracts to Java files.
+
+

key.ui/examples/case-studies/stipula/behavior_run_bet.key

@@ -0,0 +1,84 @@
+\profile "Java Profile";
+
+\settings {
+    "Choice" : {
+        "JavaCard" : "JavaCard:off",
+        "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:noRestriction",
+        "modelFields" : "modelFields:treatAsAxiom",
+        "moreSeqRules" : "moreSeqRules:off",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "soundDefaultContracts" : "soundDefaultContracts:on"
+    },
+    "Labels" : {
+        "UseOriginLabels" : true
+    },
+    "NewSMT" : {
+
+    },
+    "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" : 500000,
+        "Timeout" : -1,
+        "options" : {
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
+            "DEP_OPTIONS_KEY" : "DEP_OFF",
+            "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL",
+            "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_OFF",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_NORMAL",
+            "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",
+            "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST",
+            "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"
+        }
+    }
+}
+
+
+\javaSource "./src/";
+
+\proofObligation {
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "Bet[Bet::behavior()].JML normal_behavior operation contract.0",
+    "name" : "Bet[Bet::behavior()].JML normal_behavior operation contract.0"
+}