Fix overflow checking (#3353)

KeYProject · Jun 24, 2024 · 64126d9 · 64126d9
2 parents ab3a340 + fb3a5b1
commit 64126d9
Show file tree

Hide file tree

Showing 7 changed files with 143 additions and 68 deletions.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java
@@ -681,6 +681,18 @@ public ChoiceExpr visitOption_expr_paren(KeYParser.Option_expr_parenContext ctx)
 
     @Override
     public ChoiceExpr visitOption_expr_prop(KeYParser.Option_expr_propContext ctx) {
+        String category = ctx.option().cat.getText();
+        String value = ctx.option().value.getText();
+        String choiceStr = category + ":" + value;
+        /*
+         * Make sure that the choice (category and value!) is known to KeY, i.e. that it is declared
+         * in the file `optionsDeclarations.key`. This prevents from accidentally deactivating
+         * (parts of) taclets due to non-existing choices (see
+         * https://github.com/KeYProject/key/issues/3352).
+         */
+        if (choices().lookup(choiceStr) == null) {
+            semanticError(ctx, "Could not find choice: %s", category + ":" + choiceStr);
+        }
         return ChoiceExpr.variable(ctx.option().cat.getText(), ctx.option().value.getText());
     }
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java
@@ -166,6 +166,8 @@ public Taclet generateRelationalRepresentsTaclet(Name tacletName, Term originalA
             new RewriteTacletGoalTemplate(addedSeq, ImmutableSLList.nil(), findTerm);
 
         // choices, rule set
+        // Be careful that the choices used here is actually declared (see optionsDeclarations.key),
+        // otherwise the taclet will be unusable!
         var choice = ChoiceExpr.variable("modelFields",
             satisfiabilityGuard ? "showSatisfiability" : "treatAsAxiom");
         final RuleSet ruleSet = new RuleSet(

diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key
@@ -119,7 +119,7 @@
 // --------------------------------------------------------------------------
 // Axioms defining the integer translation functions
 // --------------------------------------------------------------------------
-\rules(programRules:Java, intRules:javaSemantics) {
+\rules(programRules:Java & (intRules:javaSemantics | intRules:arithmeticSemanticsCheckingOF)) {
     expandInByte {
         \find(inByte(i))
         \replacewith(inRangeByte(i))
@@ -149,7 +149,9 @@
         \replacewith(inRangeLong(i))
         \heuristics(concrete)
     };
+}
 
+\rules(programRules:Java, intRules:javaSemantics) {
     translateJavaUnaryMinusInt {
         \find(javaUnaryMinusInt(left))
         \replacewith(unaryMinusJint(left))

diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key
@@ -15,7 +15,7 @@
     \term numbers iz, jz;
 }
 
-\rules(programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF)) {
+\rules(programRules:Java & intRules:arithmeticSemanticsIgnoringOF) {
 
     // ------------------------------------------------------------------------
     // Rules to expand the predicates inByte, inShort, inInt, and inLong
@@ -50,6 +50,9 @@
         \replacewith(true)
         \heuristics(concrete)
     };
+}
+
+\rules(programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF)) {
 
     // --------------------------------------------------------------------------
     // Axioms defining the integer translation functions