From 5fcf6463880e872899e98c8bc4bfdc5a6a1e2cb5 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 5 Feb 2023 16:00:02 +0100 Subject: [PATCH 01/11] this contributed to solving the FP completeness issues in #1723 --- key.core/src/main/antlr4/KeYLexer.g4 | 1 + key.core/src/main/antlr4/KeYParser.g4 | 1 + .../ilkd/key/logic/sort/ProgramSVSort.java | 37 +++++ .../varexp/TacletBuilderManipulators.java | 6 +- .../FloatingPointBalancedCondition.java | 153 ++++++++++++++++++ .../rules/floatAssignment2UpdateRules.key | 30 ++++ 6 files changed, 227 insertions(+), 1 deletion(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 7625122760c..6e8bf2995f5 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -122,6 +122,7 @@ DEPENDINGON : '\\dependingOn'; DISJOINTMODULONULL : '\\disjointModuloNull'; DROP_EFFECTLESS_ELEMENTARIES : '\\dropEffectlessElementaries'; DROP_EFFECTLESS_STORES : '\\dropEffectlessStores'; +FLOATING_POINT_BALANCED : '\\floatingPointBalanced'; SIMPLIFY_IF_THEN_ELSE_UPDATE : '\\simplifyIfThenElseUpdate'; ENUM_CONST : '\\enumConstant'; FREELABELIN : '\\freeLabelIn'; diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index 27376efbf98..dc23adfa0fe 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -618,6 +618,7 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier. | SAME_OBSERVER | DROP_EFFECTLESS_ELEMENTARIES | DROP_EFFECTLESS_STORES + | FLOATING_POINT_BALANCED | DIFFERENTFIELDS | SIMPLIFY_IF_THEN_ELSE_UPDATE | CONTAINS_ASSIGNMENT diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index b298ff7cc74..7d505062f73 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java @@ -3,6 +3,7 @@ import java.util.LinkedHashMap; import java.util.Map; +import de.uka.ilkd.key.java.expression.operator.BinaryOperator; import org.key_project.util.ExtList; import org.key_project.util.collection.DefaultImmutableSet; @@ -231,6 +232,9 @@ public abstract class ProgramSVSort extends AbstractSort { new SimpleExpressionExceptingTypeSort("SimpleExpressionNonFloatDouble", new PrimitiveType[] { PrimitiveType.JAVA_FLOAT, PrimitiveType.JAVA_DOUBLE }); + public static final ProgramSVSort FLOAT_BINARY_EXP = + new FloatingPointBinaryExprSort("FloatingPointBinaryExpression"); + // --------------- Specials that can be get rid of perhaps-------------- public static final ProgramSVSort LOOPINIT = new LoopInitSort(); @@ -1093,6 +1097,39 @@ public boolean canStandFor(ProgramElement check, ExecutionContext ec, Services s } } + /** + * A schema variable for a binary operation in which at least one floating + * point type is involved. + * Needed for numeric promotion with floating point types. + * + * @see de.uka.ilkd.key.rule.conditions.FloatingPointBalancedCondition + */ + private static final class FloatingPointBinaryExprSort extends ExpressionSort { + + public FloatingPointBinaryExprSort(String name) { + super(new Name(name)); + } + + @Override + public boolean canStandFor(ProgramElement check, ExecutionContext ec, Services services) { + if (!(check instanceof BinaryOperator)) { + return false; + } + BinaryOperator bin = (BinaryOperator) check; + KeYJavaType t1 = getKeYJavaType(bin.getChildAt(0), ec, services); + KeYJavaType t2 = getKeYJavaType(bin.getChildAt(1), ec, services); + + Sort floatSort = services.getTypeConverter().getFloatLDT().targetSort(); + Sort doubleSort = services.getTypeConverter().getDoubleLDT().targetSort(); + if (t1.getSort() != floatSort && t1.getSort() != doubleSort && + t2.getSort() != floatSort && t2.getSort() != doubleSort) { + return false; + } + + return true; + } + } + /** * This sort represents a type of program schema variables that match on simple expressions, * except if they match a special primitive type. diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java index 20f31457e9b..82e5c21fa86 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java @@ -259,6 +259,9 @@ public VariableCondition build(Object[] arguments, List parameters, public static final AbstractConditionBuilder DROP_EFFECTLESS_ELEMENTARIES = new ConstructorBasedBuilder("dropEffectlessElementaries", DropEffectlessElementariesCondition.class, USV, SV, SV); + public static final AbstractConditionBuilder FLOATING_POINT_BALANCED = + new ConstructorBasedBuilder("floatingPointBalanced", + FloatingPointBalancedCondition.class, SV, SV); public static final AbstractConditionBuilder SIMPLIFY_ITE_UPDATE = new ConstructorBasedBuilder("simplifyIfThenElseUpdate", SimplifyIfThenElseUpdateCondition.class, FSV, USV, USV, FSV, SV); @@ -359,7 +362,8 @@ public IsLabeledCondition build(Object[] arguments, List parameters, CONTAINS_ASSIGNMENT, FIELD_TYPE, STATIC_REFERENCE, DIFFERENT_FIELDS, SAME_OBSERVER, applyUpdateOnRigid, DROP_EFFECTLESS_ELEMENTARIES, SIMPLIFY_ITE_UPDATE, SUBFORMULAS, STATIC_FIELD, SUBFORMULA, DROP_EFFECTLESS_STORES, EQUAL_UNIQUE, META_DISJOINT, - IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP); + IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP, + FLOATING_POINT_BALANCED); register(STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, GET_INVARIANT, GET_FREE_INVARIANT, GET_VARIANT, IS_LABELED); loadWithServiceLoader(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java new file mode 100644 index 00000000000..098af3a30e9 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java @@ -0,0 +1,153 @@ +package de.uka.ilkd.key.rule.conditions; + +import de.uka.ilkd.key.java.Expression; +import de.uka.ilkd.key.java.JavaProgramElement; +import de.uka.ilkd.key.java.ProgramElement; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.expression.operator.TypeCast; +import de.uka.ilkd.key.java.reference.TypeRef; +import de.uka.ilkd.key.java.visitor.ProgramElementReplacer; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.TermServices; +import de.uka.ilkd.key.logic.op.ElementaryUpdate; +import de.uka.ilkd.key.logic.op.LocationVariable; +import de.uka.ilkd.key.logic.op.SVSubstitute; +import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.UpdateApplication; +import de.uka.ilkd.key.logic.op.UpdateJunctor; +import de.uka.ilkd.key.logic.sort.Sort; +import de.uka.ilkd.key.proof.TermProgramVariableCollector; +import de.uka.ilkd.key.rule.MatchConditions; +import de.uka.ilkd.key.rule.VariableCondition; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import javax.annotation.Nullable; +import java.util.Set; + + +/** + * This variable condition adds required numeric promotions to Java operations + * with floating point arguments. + * + * For example: In the expression 1.0f + 1.0d, the first argument will be implicitly + * cast to double like (double)1.0f + 1.0d. + * + * If such an unbalanced expression occurs in the program, according casts are + * introduced by this varcond. + * + * The varcond is used like \floatingPointBalanced(#unbalanced, #balanced) + * where the first argument is the one from the find expression of the rule + * and the second one is the one that will be changed. + * + * @author Mattias Ulbrich + * @see de.uka.ilkd.key.logic.sort.ProgramSVSort.FloatingPointBinaryExprSort + */ +public final class FloatingPointBalancedCondition implements VariableCondition { + /** + * The first SV: It holds the unbalanced input expression + */ + private final SchemaVariable unbalanced; + /** + * The 2nd SV: It holds the balanced computed expression + */ + private final SchemaVariable balanced; + + public FloatingPointBalancedCondition(SchemaVariable unbalanced, SchemaVariable balanced) { + this.unbalanced = unbalanced; + this.balanced = balanced; + } + + @Override + public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, + Services services) { + + SVInstantiations svInst = mc.getInstantiations(); + BinaryOperator inInst = (BinaryOperator) svInst.getInstantiation(unbalanced); + JavaProgramElement outInst = (JavaProgramElement) svInst.getInstantiation(balanced); + if (inInst == null) { + return mc; + } + + BinaryOperator properResultInst = balance(inInst, services); + if (properResultInst == null) { + return null; + } else if (outInst == null) { + svInst = svInst.add(balanced, properResultInst, services); + return mc.setInstantiations(svInst); + } else if (outInst.equals(properResultInst)) { + return mc; + } else { + return null; + } + } + + @Override + public String toString() { + return "\\floatingPointBalanced(" + unbalanced + ", " + balanced + ")"; + } + + private static KeYJavaType getKeYJavaType(ProgramElement pe, Services services) { + return services.getTypeConverter().getKeYJavaType((Expression) pe); + } + + /** + * Make sure the result is a binary operation with same types on lhs + * and rhs. do this by adding cast if needed. + * + * If no cast is needed, return null. + * + * @param inInst the binary AST element to balance + * @param services as usual ... to lookup everything + * @return null if already same types. Otherwise a binary operator which + * has an added cast compared to the input + */ + private static @Nullable BinaryOperator balance(BinaryOperator inInst, Services services) { + + ProgramElement child0 = inInst.getChildAt(0); + ProgramElement child1 = inInst.getChildAt(1); + + KeYJavaType type0 = getKeYJavaType(child0, services); + KeYJavaType type1 = getKeYJavaType(child1, services); + if (type0.getSort() == type1.getSort()) { + // nothing to be done ... same type + return null; + } + + Sort doubleSort = services.getTypeConverter().getDoubleLDT().targetSort(); + Sort floatSort = services.getTypeConverter().getFloatLDT().targetSort(); + if (type0.getSort() == doubleSort) { + return cast(inInst, 1, type0, services); + } + if (type1.getSort() == doubleSort) { + return cast(inInst, 0, type1, services); + } + if (type0.getSort() == floatSort) { + return cast(inInst, 1, type0, services); + } + if (type1.getSort() == floatSort) { + return cast(inInst, 0, type1, services); + } + return null; + } + + /** + * Add a cast to a binary operation. + * + * @param inInst the tree to modify + * @param childNo the child to which a cast is to be added + * @param kjt the type to which to cast + * @param services as usual + * @return a binary operation similar to the input, but with one + * cast added to child childNo. + */ + private static BinaryOperator cast(BinaryOperator inInst, int childNo, KeYJavaType kjt, + Services services) { + Expression child = (Expression) inInst.getChildAt(childNo); + TypeCast cast = new TypeCast(child, new TypeRef(kjt)); + ProgramElementReplacer per = new ProgramElementReplacer(inInst, services); + ProgramElement result = per.replace(child, cast); + return (BinaryOperator) result; + } +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key index 7f696fb5390..691744ccf4b 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key @@ -427,6 +427,16 @@ \displayname "cast" }; + wideningCastFloatToDouble { + \find(\modality{#normalassign}{.. + #loc = (double) #seFloat; + ...}\endmodality (post)) + \replacewith({#loc := (double)#seFloat} + \modality{#normalassign}{.. ...}\endmodality (post)) + \heuristics(executeFloatAssignment) + \displayname "cast" + }; + wideningCastIntToFloat { \find(\modality{#normalassign}{.. #loc = (float) #seCharByteShortInt; @@ -469,6 +479,16 @@ \displayname "cast" }; + narrowingCastDoubleToFloat { + \find(\modality{#normalassign}{.. + #loc = (float) #seDouble; + ...}\endmodality (post)) + \replacewith({#loc := (float)(#seDouble)} + \modality{#normalassign}{.. ...}\endmodality (post)) + \heuristics(executeFloatAssignment) + \displayname "cast" + }; + narrowingCastFloatToLong { \find(\modality{#normalassign}{.. #loc = (long) #seFloat; @@ -497,4 +517,14 @@ \displayname "cast" }; + unbalanced_float_expression { + \schemaVar \program FloatingPointBinaryExpression #unbalancedFloat; + \schemaVar \program FloatingPointBinaryExpression #balancedFloat; + + \find(\modality{#normalassign}{.. #loc = #unbalancedFloat; ...}\endmodality (post)) + \varcond(\floatingPointBalanced(#unbalancedFloat, #balancedFloat)) + \replacewith(\modality{#normalassign}{.. #loc = #balancedFloat; ...}\endmodality (post)) + \heuristics(simplify_prog) + \displayname "cast" + }; } From bd9d05429422bee1cc4864c5ccb79234b387882e Mon Sep 17 00:00:00 2001 From: Samuel Teuber Date: Thu, 9 Mar 2023 15:44:57 +0100 Subject: [PATCH 02/11] First try in fixing cast assignments --- .../rules/floatAssignment2UpdateRules.key | 40 +++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key index 691744ccf4b..02383d8dd21 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key @@ -527,4 +527,44 @@ \heuristics(simplify_prog) \displayname "cast" }; + + unbalanced_double_float_assignment { + \find(\modality{#normalassign}{.. #loc = #seFloat; ...}\endmodality(post)) + \varcond(\sub(\typeof(#loc),double)) + \replacewith(\modality{#normalassign}{.. #loc = (double) #seFloat; ...}\endmodality(post)) + \heuristics(simplify_prog) + \displayname "cast" + }; + + unbalanced_double_int_assignment { + \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt; ...}\endmodality(post)) + \varcond(\sub(\typeof(#loc),double)) + \replacewith(\modality{#normalassign}{.. #loc = (double) #seCharByteShortInt; ...}\endmodality(post)) + \heuristics(simplify_prog) + \displayname "cast" + }; + + unbalanced_double_long_assignment { + \find(\modality{#normalassign}{.. #loc = #seLong; ...}\endmodality(post)) + \varcond(\sub(\typeof(#loc),double)) + \replacewith(\modality{#normalassign}{.. #loc = (double) #seLong; ...}\endmodality(post)) + \heuristics(simplify_prog) + \displayname "cast" + }; + + unbalanced_float_int_assignment { + \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt; ...}\endmodality(post)) + \varcond(\sub(\typeof(#loc),float)) + \replacewith(\modality{#normalassign}{.. #loc = (float) #seCharByteShortInt; ...}\endmodality(post)) + \heuristics(simplify_prog) + \displayname "cast" + }; + + unbalanced_float_long_assignment { + \find(\modality{#normalassign}{.. #loc = #seLong; ...}\endmodality(post)) + \varcond(\sub(\typeof(#loc),float)) + \replacewith(\modality{#normalassign}{.. #loc = (float) #seLong; ...}\endmodality(post)) + \heuristics(simplify_prog) + \displayname "cast" + }; } From 89cfded9fa29503b57444046d7f99c2bd1e06df2 Mon Sep 17 00:00:00 2001 From: Samuel Teuber Date: Thu, 9 Mar 2023 15:56:46 +0100 Subject: [PATCH 03/11] Added Int/Long to Double casting rules --- .../rules/floatAssignment2UpdateRules.key | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key index 02383d8dd21..fec4075b743 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key @@ -447,6 +447,26 @@ \displayname "cast" }; + wideningCastIntToDouble { + \find(\modality{#normalassign}{.. + #loc = (double) #seCharByteShortInt; + ...}\endmodality (post)) + \replacewith({#loc := (double)(#seCharByteShortInt)} + \modality{#normalassign}{.. ...}\endmodality (post)) + \heuristics(executeFloatAssignment) + \displayname "cast" + }; + + wideningCastLongToDouble { + \find(\modality{#normalassign}{.. + #loc = (double) #seLong; + ...}\endmodality (post)) + \replacewith({#loc := (double)#seLong} + \modality{#normalassign}{.. ...}\endmodality (post)) + \heuristics(executeFloatAssignment) + \displayname "cast" + }; + identityCastFloat { \find(\modality{#normalassign}{.. #loc = (float) #seFloat; From 085614eca43526a7302a581ddb9b13e0e1f31a87 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 5 Feb 2023 16:00:02 +0100 Subject: [PATCH 04/11] this contributed to solving the FP completeness issues in #1723 --- key.core/src/main/antlr4/KeYLexer.g4 | 1 + key.core/src/main/antlr4/KeYParser.g4 | 1 + .../ilkd/key/logic/sort/ProgramSVSort.java | 37 +++++ .../varexp/TacletBuilderManipulators.java | 6 +- .../FloatingPointBalancedCondition.java | 153 ++++++++++++++++++ .../rules/floatAssignment2UpdateRules.key | 30 ++++ 6 files changed, 227 insertions(+), 1 deletion(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 7625122760c..6e8bf2995f5 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -122,6 +122,7 @@ DEPENDINGON : '\\dependingOn'; DISJOINTMODULONULL : '\\disjointModuloNull'; DROP_EFFECTLESS_ELEMENTARIES : '\\dropEffectlessElementaries'; DROP_EFFECTLESS_STORES : '\\dropEffectlessStores'; +FLOATING_POINT_BALANCED : '\\floatingPointBalanced'; SIMPLIFY_IF_THEN_ELSE_UPDATE : '\\simplifyIfThenElseUpdate'; ENUM_CONST : '\\enumConstant'; FREELABELIN : '\\freeLabelIn'; diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index a1c35e56f72..58d762e25ed 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -616,6 +616,7 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier. | SAME_OBSERVER | DROP_EFFECTLESS_ELEMENTARIES | DROP_EFFECTLESS_STORES + | FLOATING_POINT_BALANCED | DIFFERENTFIELDS | SIMPLIFY_IF_THEN_ELSE_UPDATE | CONTAINS_ASSIGNMENT diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index b298ff7cc74..7d505062f73 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java @@ -3,6 +3,7 @@ import java.util.LinkedHashMap; import java.util.Map; +import de.uka.ilkd.key.java.expression.operator.BinaryOperator; import org.key_project.util.ExtList; import org.key_project.util.collection.DefaultImmutableSet; @@ -231,6 +232,9 @@ public abstract class ProgramSVSort extends AbstractSort { new SimpleExpressionExceptingTypeSort("SimpleExpressionNonFloatDouble", new PrimitiveType[] { PrimitiveType.JAVA_FLOAT, PrimitiveType.JAVA_DOUBLE }); + public static final ProgramSVSort FLOAT_BINARY_EXP = + new FloatingPointBinaryExprSort("FloatingPointBinaryExpression"); + // --------------- Specials that can be get rid of perhaps-------------- public static final ProgramSVSort LOOPINIT = new LoopInitSort(); @@ -1093,6 +1097,39 @@ public boolean canStandFor(ProgramElement check, ExecutionContext ec, Services s } } + /** + * A schema variable for a binary operation in which at least one floating + * point type is involved. + * Needed for numeric promotion with floating point types. + * + * @see de.uka.ilkd.key.rule.conditions.FloatingPointBalancedCondition + */ + private static final class FloatingPointBinaryExprSort extends ExpressionSort { + + public FloatingPointBinaryExprSort(String name) { + super(new Name(name)); + } + + @Override + public boolean canStandFor(ProgramElement check, ExecutionContext ec, Services services) { + if (!(check instanceof BinaryOperator)) { + return false; + } + BinaryOperator bin = (BinaryOperator) check; + KeYJavaType t1 = getKeYJavaType(bin.getChildAt(0), ec, services); + KeYJavaType t2 = getKeYJavaType(bin.getChildAt(1), ec, services); + + Sort floatSort = services.getTypeConverter().getFloatLDT().targetSort(); + Sort doubleSort = services.getTypeConverter().getDoubleLDT().targetSort(); + if (t1.getSort() != floatSort && t1.getSort() != doubleSort && + t2.getSort() != floatSort && t2.getSort() != doubleSort) { + return false; + } + + return true; + } + } + /** * This sort represents a type of program schema variables that match on simple expressions, * except if they match a special primitive type. diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java index 20f31457e9b..82e5c21fa86 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java @@ -259,6 +259,9 @@ public VariableCondition build(Object[] arguments, List parameters, public static final AbstractConditionBuilder DROP_EFFECTLESS_ELEMENTARIES = new ConstructorBasedBuilder("dropEffectlessElementaries", DropEffectlessElementariesCondition.class, USV, SV, SV); + public static final AbstractConditionBuilder FLOATING_POINT_BALANCED = + new ConstructorBasedBuilder("floatingPointBalanced", + FloatingPointBalancedCondition.class, SV, SV); public static final AbstractConditionBuilder SIMPLIFY_ITE_UPDATE = new ConstructorBasedBuilder("simplifyIfThenElseUpdate", SimplifyIfThenElseUpdateCondition.class, FSV, USV, USV, FSV, SV); @@ -359,7 +362,8 @@ public IsLabeledCondition build(Object[] arguments, List parameters, CONTAINS_ASSIGNMENT, FIELD_TYPE, STATIC_REFERENCE, DIFFERENT_FIELDS, SAME_OBSERVER, applyUpdateOnRigid, DROP_EFFECTLESS_ELEMENTARIES, SIMPLIFY_ITE_UPDATE, SUBFORMULAS, STATIC_FIELD, SUBFORMULA, DROP_EFFECTLESS_STORES, EQUAL_UNIQUE, META_DISJOINT, - IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP); + IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP, + FLOATING_POINT_BALANCED); register(STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, GET_INVARIANT, GET_FREE_INVARIANT, GET_VARIANT, IS_LABELED); loadWithServiceLoader(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java new file mode 100644 index 00000000000..098af3a30e9 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java @@ -0,0 +1,153 @@ +package de.uka.ilkd.key.rule.conditions; + +import de.uka.ilkd.key.java.Expression; +import de.uka.ilkd.key.java.JavaProgramElement; +import de.uka.ilkd.key.java.ProgramElement; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.expression.operator.TypeCast; +import de.uka.ilkd.key.java.reference.TypeRef; +import de.uka.ilkd.key.java.visitor.ProgramElementReplacer; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.TermServices; +import de.uka.ilkd.key.logic.op.ElementaryUpdate; +import de.uka.ilkd.key.logic.op.LocationVariable; +import de.uka.ilkd.key.logic.op.SVSubstitute; +import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.UpdateApplication; +import de.uka.ilkd.key.logic.op.UpdateJunctor; +import de.uka.ilkd.key.logic.sort.Sort; +import de.uka.ilkd.key.proof.TermProgramVariableCollector; +import de.uka.ilkd.key.rule.MatchConditions; +import de.uka.ilkd.key.rule.VariableCondition; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import javax.annotation.Nullable; +import java.util.Set; + + +/** + * This variable condition adds required numeric promotions to Java operations + * with floating point arguments. + * + * For example: In the expression 1.0f + 1.0d, the first argument will be implicitly + * cast to double like (double)1.0f + 1.0d. + * + * If such an unbalanced expression occurs in the program, according casts are + * introduced by this varcond. + * + * The varcond is used like \floatingPointBalanced(#unbalanced, #balanced) + * where the first argument is the one from the find expression of the rule + * and the second one is the one that will be changed. + * + * @author Mattias Ulbrich + * @see de.uka.ilkd.key.logic.sort.ProgramSVSort.FloatingPointBinaryExprSort + */ +public final class FloatingPointBalancedCondition implements VariableCondition { + /** + * The first SV: It holds the unbalanced input expression + */ + private final SchemaVariable unbalanced; + /** + * The 2nd SV: It holds the balanced computed expression + */ + private final SchemaVariable balanced; + + public FloatingPointBalancedCondition(SchemaVariable unbalanced, SchemaVariable balanced) { + this.unbalanced = unbalanced; + this.balanced = balanced; + } + + @Override + public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, + Services services) { + + SVInstantiations svInst = mc.getInstantiations(); + BinaryOperator inInst = (BinaryOperator) svInst.getInstantiation(unbalanced); + JavaProgramElement outInst = (JavaProgramElement) svInst.getInstantiation(balanced); + if (inInst == null) { + return mc; + } + + BinaryOperator properResultInst = balance(inInst, services); + if (properResultInst == null) { + return null; + } else if (outInst == null) { + svInst = svInst.add(balanced, properResultInst, services); + return mc.setInstantiations(svInst); + } else if (outInst.equals(properResultInst)) { + return mc; + } else { + return null; + } + } + + @Override + public String toString() { + return "\\floatingPointBalanced(" + unbalanced + ", " + balanced + ")"; + } + + private static KeYJavaType getKeYJavaType(ProgramElement pe, Services services) { + return services.getTypeConverter().getKeYJavaType((Expression) pe); + } + + /** + * Make sure the result is a binary operation with same types on lhs + * and rhs. do this by adding cast if needed. + * + * If no cast is needed, return null. + * + * @param inInst the binary AST element to balance + * @param services as usual ... to lookup everything + * @return null if already same types. Otherwise a binary operator which + * has an added cast compared to the input + */ + private static @Nullable BinaryOperator balance(BinaryOperator inInst, Services services) { + + ProgramElement child0 = inInst.getChildAt(0); + ProgramElement child1 = inInst.getChildAt(1); + + KeYJavaType type0 = getKeYJavaType(child0, services); + KeYJavaType type1 = getKeYJavaType(child1, services); + if (type0.getSort() == type1.getSort()) { + // nothing to be done ... same type + return null; + } + + Sort doubleSort = services.getTypeConverter().getDoubleLDT().targetSort(); + Sort floatSort = services.getTypeConverter().getFloatLDT().targetSort(); + if (type0.getSort() == doubleSort) { + return cast(inInst, 1, type0, services); + } + if (type1.getSort() == doubleSort) { + return cast(inInst, 0, type1, services); + } + if (type0.getSort() == floatSort) { + return cast(inInst, 1, type0, services); + } + if (type1.getSort() == floatSort) { + return cast(inInst, 0, type1, services); + } + return null; + } + + /** + * Add a cast to a binary operation. + * + * @param inInst the tree to modify + * @param childNo the child to which a cast is to be added + * @param kjt the type to which to cast + * @param services as usual + * @return a binary operation similar to the input, but with one + * cast added to child childNo. + */ + private static BinaryOperator cast(BinaryOperator inInst, int childNo, KeYJavaType kjt, + Services services) { + Expression child = (Expression) inInst.getChildAt(childNo); + TypeCast cast = new TypeCast(child, new TypeRef(kjt)); + ProgramElementReplacer per = new ProgramElementReplacer(inInst, services); + ProgramElement result = per.replace(child, cast); + return (BinaryOperator) result; + } +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key index 7f696fb5390..691744ccf4b 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key @@ -427,6 +427,16 @@ \displayname "cast" }; + wideningCastFloatToDouble { + \find(\modality{#normalassign}{.. + #loc = (double) #seFloat; + ...}\endmodality (post)) + \replacewith({#loc := (double)#seFloat} + \modality{#normalassign}{.. ...}\endmodality (post)) + \heuristics(executeFloatAssignment) + \displayname "cast" + }; + wideningCastIntToFloat { \find(\modality{#normalassign}{.. #loc = (float) #seCharByteShortInt; @@ -469,6 +479,16 @@ \displayname "cast" }; + narrowingCastDoubleToFloat { + \find(\modality{#normalassign}{.. + #loc = (float) #seDouble; + ...}\endmodality (post)) + \replacewith({#loc := (float)(#seDouble)} + \modality{#normalassign}{.. ...}\endmodality (post)) + \heuristics(executeFloatAssignment) + \displayname "cast" + }; + narrowingCastFloatToLong { \find(\modality{#normalassign}{.. #loc = (long) #seFloat; @@ -497,4 +517,14 @@ \displayname "cast" }; + unbalanced_float_expression { + \schemaVar \program FloatingPointBinaryExpression #unbalancedFloat; + \schemaVar \program FloatingPointBinaryExpression #balancedFloat; + + \find(\modality{#normalassign}{.. #loc = #unbalancedFloat; ...}\endmodality (post)) + \varcond(\floatingPointBalanced(#unbalancedFloat, #balancedFloat)) + \replacewith(\modality{#normalassign}{.. #loc = #balancedFloat; ...}\endmodality (post)) + \heuristics(simplify_prog) + \displayname "cast" + }; } From f5970f11d88c8a4a419b45d05d1615d030770c22 Mon Sep 17 00:00:00 2001 From: Samuel Teuber Date: Mon, 3 Apr 2023 15:29:45 +0200 Subject: [PATCH 05/11] Added type constraint to assignment and int assignment rules --- .../rules/integerAssignment2UpdateRules.key | 57 +++++++++++++++++++ .../de/uka/ilkd/key/proof/rules/javaRules.key | 1 + 2 files changed, 58 insertions(+) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key index adb269dad33..2fe7f671a8d 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key @@ -38,6 +38,7 @@ \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt0 * #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1))) @@ -52,6 +53,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt * #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(mul(#seCharByteShortInt, #seLong))) @@ -66,6 +68,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong * #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(mul(#seLong, #seCharByteShortInt))) @@ -80,6 +83,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 * #seLong1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(mul(#seLong0, #seLong1))) @@ -100,6 +104,7 @@ \find( ==> \modality{#normalassign}{.. #loc=#seCharByteShortInt0 / #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( ==> {#loc := javaDivInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)); @@ -112,6 +117,7 @@ \find( ==> \modality{#normalassign}{.. #loc=#se / #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( ==> {#loc := javaDivLong(#se, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)); @@ -124,6 +130,7 @@ \find( ==> \modality{#normalassign}{.. #loc=#seLong / #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( ==> {#loc := javaDivLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)); @@ -140,6 +147,8 @@ \find( ==> \modality{#normalassign}{.. #loc=#se0 % #se1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( ==> {#loc := javaMod(#se0, #se1)} \modality{#normalassign}{.. ...}\endmodality (post)); @@ -157,6 +166,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 / #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaDivInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -168,6 +178,7 @@ \find(\modality{#normalassign}{.. #loc=#se / #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaDivLong(#se, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -179,6 +190,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong / #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaDivLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -194,6 +206,7 @@ \find(\modality{#normalassign}{.. #loc=#se0 % #se1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaMod(#se0, #se1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -210,6 +223,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 / #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith(\if(#seCharByteShortInt1 != 0) \then({#loc := javaDivInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -224,6 +238,7 @@ \find(\modality{#normalassign}{.. #loc=#se / #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith(\if(#seLong != 0) \then({#loc := javaDivLong(#se, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -238,6 +253,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong / #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith(\if(#seCharByteShortInt != 0) \then({#loc := javaDivLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -256,6 +272,7 @@ \find(\modality{#normalassign}{.. #loc=#se0 % #se1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith(\if(#se1 != 0) \then({#loc := javaMod(#se0, #se1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -276,6 +293,7 @@ \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt0 - #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1))) @@ -290,6 +308,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt - #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(sub(#seCharByteShortInt, #seLong))) @@ -304,6 +323,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong - #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(sub(#seLong, #seCharByteShortInt))) @@ -319,6 +339,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 - #seLong1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(sub(#seLong0, #seLong1))) @@ -335,6 +356,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 + #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inInt(add(#seCharByteShortInt0, #seCharByteShortInt1))) @@ -350,6 +372,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt + #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(add(#seCharByteShortInt, #seLong))) @@ -365,6 +388,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong + #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(add(#seLong, #seCharByteShortInt))) @@ -380,6 +404,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 + #seLong1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(add(#seLong0, #seLong1))) @@ -397,6 +422,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 & #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseAndInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -408,6 +434,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt & #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseAndLong(#seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -419,6 +446,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong & #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseAndLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -430,6 +458,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 & #seLong1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseAndLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -443,6 +472,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 | #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseOrInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -454,6 +484,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt | #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseOrLong(#seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -466,6 +497,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong | #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseOrLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -478,6 +510,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 | #seLong1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseOrLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -491,6 +524,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 ^ #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseXOrInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -502,6 +536,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt ^ #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseXOrLong(#seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -513,6 +548,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong ^ #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseXOrLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -524,6 +560,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 ^ #seLong1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseXOrLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -537,6 +574,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 >> #se; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inInt(shiftright(#seLong0, #se))) @@ -552,6 +590,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 >> #se; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inInt(shiftright(#seLong0, #se))) @@ -569,6 +608,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 << #se; ...} \endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inInt(shiftleft(#seCharByteShortInt0, #se))) @@ -584,6 +624,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 << #se; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(shiftleft(#seLong0, #se))) @@ -601,6 +642,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 >>> #se; ...} \endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(unsignedshiftrightJint(#seCharByteShortInt0, #se))) @@ -616,6 +658,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 >>> #se; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(unsignedshiftrightJlong(#seLong0, #se))) @@ -634,6 +677,7 @@ \find(\modality{#normalassign}{.. #loc = - #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inInt(neg(#seCharByteShortInt))) @@ -648,6 +692,7 @@ \find(\modality{#normalassign}{.. #loc = - #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inLong(neg(#seLong))) @@ -660,6 +705,7 @@ bitwiseNegationInt { \find(\modality{#normalassign}{.. #loc = ~ #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith({#loc := javaBitwiseNegateInt(#se)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeIntegerAssignment) @@ -668,6 +714,7 @@ bitwiseNegationLong { \find(\modality{#normalassign}{.. #loc = ~ #se; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith({#loc := javaBitwiseNegateLong(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeIntegerAssignment) @@ -682,6 +729,7 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seShort; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inByte(#seShort)) @@ -696,6 +744,7 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inByte(#seInt)) @@ -710,6 +759,7 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inByte(#seLong)) @@ -724,6 +774,7 @@ \find(\modality{#normalassign}{.. #loc = (short) #seInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inShort(#seInt)) @@ -738,6 +789,7 @@ \find(\modality{#normalassign}{.. #loc = (short) #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inShort(#seLong)) @@ -750,6 +802,7 @@ narrowingIntCastLong { \find(\modality{#normalassign}{.. #loc = (int) #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inInt(#seLong)) @@ -764,6 +817,7 @@ \find(\modality{#normalassign}{.. #loc = (char) #seByte; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inChar(#seByte)) @@ -779,6 +833,7 @@ \find(\modality{#normalassign}{.. #loc = (char) #seShort; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inChar(#seShort)) @@ -794,6 +849,7 @@ \find(\modality{#normalassign}{.. #loc = (char) #seInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inChar(#seInt)) @@ -808,6 +864,7 @@ \find(\modality{#normalassign}{.. #loc = (char) #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) (intRules:checkedOverflow) { "Overflow check": \replacewith(inChar(#seLong)) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key index 8e37234a818..13b3724ee45 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key @@ -294,6 +294,7 @@ assignment { \find(\modality{#allmodal}{.. #loc = #se; ...}\endmodality (post)) + \varcond(\sub(\typeof(#se),\typeof(#loc))) \replacewith({#loc := #se}\modality{#allmodal}{.. ...}\endmodality (post)) \heuristics(simplify_prog, simplify_prog_subset) }; From 1595a2e287768879e49f7b561d63ef1cbbffac79 Mon Sep 17 00:00:00 2001 From: Samuel Teuber Date: Tue, 4 Apr 2023 18:04:49 +0200 Subject: [PATCH 06/11] Might have fixed completeness bug w.r.t. casts --- .../ilkd/key/logic/sort/ProgramSVSort.java | 22 +-- .../FloatingPointBalancedCondition.java | 16 +- .../key/rule/conditions/TypeResolver.java | 6 +- .../rules/floatAssignment2UpdateRules.key | 157 +++++++++--------- 4 files changed, 107 insertions(+), 94 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index 554c6af60c6..056e782efa7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java @@ -3,7 +3,9 @@ import java.util.LinkedHashMap; import java.util.Map; -import de.uka.ilkd.key.java.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.expression.Operator; +import de.uka.ilkd.key.java.expression.operator.*; + import de.uka.ilkd.key.java.Expression; import de.uka.ilkd.key.java.Label; import de.uka.ilkd.key.java.NamedProgramElement; @@ -21,12 +23,6 @@ import de.uka.ilkd.key.java.expression.ArrayInitializer; import de.uka.ilkd.key.java.expression.Literal; import de.uka.ilkd.key.java.expression.literal.StringLiteral; -import de.uka.ilkd.key.java.expression.operator.DLEmbeddedExpression; -import de.uka.ilkd.key.java.expression.operator.Instanceof; -import de.uka.ilkd.key.java.expression.operator.Intersect; -import de.uka.ilkd.key.java.expression.operator.Negative; -import de.uka.ilkd.key.java.expression.operator.New; -import de.uka.ilkd.key.java.expression.operator.NewArray; import de.uka.ilkd.key.java.expression.operator.adt.*; import de.uka.ilkd.key.java.reference.*; import de.uka.ilkd.key.java.statement.Catch; @@ -1100,7 +1096,7 @@ public boolean canStandFor(ProgramElement check, ExecutionContext ec, Services s /** * A schema variable for a binary operation in which at least one floating - * point type is involved. + * point type is involved and both arguments are simple expressions. * Needed for numeric promotion with floating point types. * * @see de.uka.ilkd.key.rule.conditions.FloatingPointBalancedCondition @@ -1113,10 +1109,16 @@ public FloatingPointBinaryExprSort(String name) { @Override public boolean canStandFor(ProgramElement check, ExecutionContext ec, Services services) { - if (!(check instanceof BinaryOperator)) { + if (!(check instanceof BinaryOperator || check instanceof ComparativeOperator)) { + return false; + } + Operator bin = (Operator) check; + if ( + !SIMPLEEXPRESSION.canStandFor(bin.getChildAt(0), ec, services) || + !SIMPLEEXPRESSION.canStandFor(bin.getChildAt(1), ec, services) + ) { return false; } - BinaryOperator bin = (BinaryOperator) check; KeYJavaType t1 = getKeYJavaType(bin.getChildAt(0), ec, services); KeYJavaType t2 = getKeYJavaType(bin.getChildAt(1), ec, services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java index 098af3a30e9..338590a5218 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java @@ -5,7 +5,9 @@ import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.expression.Operator; import de.uka.ilkd.key.java.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.expression.operator.ComparativeOperator; import de.uka.ilkd.key.java.expression.operator.TypeCast; import de.uka.ilkd.key.java.reference.TypeRef; import de.uka.ilkd.key.java.visitor.ProgramElementReplacer; @@ -64,13 +66,17 @@ public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, Mat Services services) { SVInstantiations svInst = mc.getInstantiations(); - BinaryOperator inInst = (BinaryOperator) svInst.getInstantiation(unbalanced); + Object untypedInstantiation = svInst.getInstantiation(unbalanced); + if (!(untypedInstantiation instanceof BinaryOperator || untypedInstantiation instanceof ComparativeOperator)) { + return null; + } + Operator inInst = (Operator) untypedInstantiation; JavaProgramElement outInst = (JavaProgramElement) svInst.getInstantiation(balanced); if (inInst == null) { return mc; } - BinaryOperator properResultInst = balance(inInst, services); + Operator properResultInst = balance(inInst, services); if (properResultInst == null) { return null; } else if (outInst == null) { @@ -103,7 +109,7 @@ private static KeYJavaType getKeYJavaType(ProgramElement pe, Services services) * @return null if already same types. Otherwise a binary operator which * has an added cast compared to the input */ - private static @Nullable BinaryOperator balance(BinaryOperator inInst, Services services) { + private static @Nullable Operator balance(Operator inInst, Services services) { ProgramElement child0 = inInst.getChildAt(0); ProgramElement child1 = inInst.getChildAt(1); @@ -142,12 +148,12 @@ private static KeYJavaType getKeYJavaType(ProgramElement pe, Services services) * @return a binary operation similar to the input, but with one * cast added to child childNo. */ - private static BinaryOperator cast(BinaryOperator inInst, int childNo, KeYJavaType kjt, + private static Operator cast(Operator inInst, int childNo, KeYJavaType kjt, Services services) { Expression child = (Expression) inInst.getChildAt(childNo); TypeCast cast = new TypeCast(child, new TypeRef(kjt)); ProgramElementReplacer per = new ProgramElementReplacer(inInst, services); ProgramElement result = per.replace(child, cast); - return (BinaryOperator) result; + return (Operator) result; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java index 00ad418d85e..f93db74eb76 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java @@ -3,6 +3,7 @@ import de.uka.ilkd.key.java.Expression; import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.expression.operator.BinaryOperator; import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermServices; @@ -146,14 +147,17 @@ public Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate, Term gsTerm = null; if (inst instanceof Term) { gsTerm = (Term) inst; + s = gsTerm.sort(); + } else if (inst instanceof BinaryOperator) { + s = services.getTypeConverter().getKeYJavaType((BinaryOperator) inst).getSort(); } else if (inst instanceof ProgramElement) { gsTerm = services.getTypeConverter().convertToLogicElement( (ProgramElement) inst, instMap.getExecutionContext()); + s = gsTerm.sort(); } else { Debug.fail("Unexpected substitution for sv " + resolveSV + ":" + inst); return null; } - s = gsTerm.sort(); } return s; } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key index fec4075b743..30375a11fbc 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key @@ -27,6 +27,7 @@ \program Variable #v; \program NonSimpleExpression #nse; + \program SimpleExpression #se; \formula post; @@ -143,29 +144,51 @@ \find(\modality{#normalassign}{.. #loc = - #seFloat; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float)) \replacewith({#loc := javaUnaryMinusFloat(#seFloat)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) \displayname "unaryMinus" }; + unaryMinusFloat_cast { + \find(\modality{#normalassign}{.. + #loc = - #se; + ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float),\not\sub(\typeof(#se), float)) + \replacewith(\modality{#normalassign}{.. #loc = (float) (- #se); ...}\endmodality (post)) + \heuristics(executeFloatAssignment) + \displayname "cast" + }; + unaryMinusDouble { \find(\modality{#normalassign}{.. #loc = - #seDouble; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), double)) \replacewith({#loc := javaUnaryMinusDouble(#seDouble)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) \displayname "unaryMinus" }; + unaryMinusDouble_cast { + \find(\modality{#normalassign}{.. + #loc = - #se; + ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), double),\not\sub(\typeof(#se), double)) + \replacewith(\modality{#normalassign}{.. #loc = (double) (- #se); ...}\endmodality (post)) + \heuristics(executeFloatAssignment) + \displayname "cast" + }; + // ------------- Arithmetic operations with strictfp // float assignmentAdditionFloatStrictFP { \find(\modality{#normalassign}{.. #loc=#seFloat0 + #seFloat1; ...}\endmodality (post)) - \varcond(\isInStrictFp) + \varcond(\isInStrictFp, \sub(\typeof(#loc), float)) \replacewith( {#loc := addFloat(#seFloat0, #seFloat1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -177,7 +200,7 @@ \find(\modality{#normalassign}{.. #loc = #seFloat0 - #seFloat1; ...}\endmodality (post)) - \varcond(\isInStrictFp) + \varcond(\isInStrictFp, \sub(\typeof(#loc), float)) \replacewith( {#loc := subFloat(#seFloat0, #seFloat1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -189,7 +212,7 @@ \find(\modality{#normalassign}{.. #loc = #seFloat0 * #seFloat1; ...}\endmodality (post)) - \varcond(\isInStrictFp) + \varcond(\isInStrictFp, \sub(\typeof(#loc), float)) \replacewith( {#loc := mulFloat(#seFloat0, #seFloat1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -201,7 +224,7 @@ \find(\modality{#normalassign}{.. #loc = #seFloat0 / #seFloat1; ...}\endmodality (post)) - \varcond(\isInStrictFp) + \varcond(\isInStrictFp, \sub(\typeof(#loc), float)) \replacewith( {#loc := divFloat(#seFloat0, #seFloat1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -214,7 +237,7 @@ \find(\modality{#normalassign}{.. #loc=#seDouble0 + #seDouble1; ...}\endmodality (post)) - \varcond(\isInStrictFp) + \varcond(\isInStrictFp, \sub(\typeof(#loc), double)) \replacewith( {#loc := addDouble(#seDouble0, #seDouble1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -226,7 +249,7 @@ \find(\modality{#normalassign}{.. #loc = #seDouble0 - #seDouble1; ...}\endmodality (post)) - \varcond(\isInStrictFp) + \varcond(\isInStrictFp, \sub(\typeof(#loc), double)) \replacewith( {#loc := subDouble(#seDouble0, #seDouble1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -238,7 +261,7 @@ \find(\modality{#normalassign}{.. #loc = #seDouble0 * #seDouble1; ...}\endmodality (post)) - \varcond(\isInStrictFp) + \varcond(\isInStrictFp, \sub(\typeof(#loc), double)) \replacewith( {#loc := mulDouble(#seDouble0, #seDouble1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -250,7 +273,7 @@ \find(\modality{#normalassign}{.. #loc = #seDouble0 / #seDouble1; ...}\endmodality (post)) - \varcond(\isInStrictFp) + \varcond(\isInStrictFp, \sub(\typeof(#loc), double)) \replacewith( {#loc := divDouble(#seDouble0, #seDouble1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -264,7 +287,7 @@ \find(\modality{#normalassign}{.. #loc=#seFloat0 + #seFloat1; ...}\endmodality (post)) - \varcond(\not \isInStrictFp) + \varcond(\not \isInStrictFp,\sub(\typeof(#loc), float)) \replacewith( {#loc := javaAddFloat(#seFloat0, #seFloat1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -276,7 +299,7 @@ \find(\modality{#normalassign}{.. #loc=#seDouble0 + #seDouble1; ...}\endmodality (post)) - \varcond(\not \isInStrictFp) + \varcond(\not \isInStrictFp,\sub(\typeof(#loc), double)) \replacewith( {#loc := javaAddDouble(#seDouble0, #seDouble1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -288,7 +311,7 @@ \find(\modality{#normalassign}{.. #loc = #seFloat0 - #seFloat1; ...}\endmodality (post)) - \varcond(\not \isInStrictFp) + \varcond(\not \isInStrictFp, \sub(\typeof(#loc), float)) \replacewith( {#loc := javaSubFloat(#seFloat0, #seFloat1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -300,7 +323,7 @@ \find(\modality{#normalassign}{.. #loc = #seDouble0 - #seDouble1; ...}\endmodality (post)) - \varcond(\not \isInStrictFp) + \varcond(\not \isInStrictFp, \sub(\typeof(#loc), double)) \replacewith( {#loc := javaSubDouble(#seDouble0, #seDouble1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -312,7 +335,7 @@ \find(\modality{#normalassign}{.. #loc = #seFloat0 * #seFloat1; ...}\endmodality (post)) - \varcond(\not \isInStrictFp) + \varcond(\not \isInStrictFp, \sub(\typeof(#loc), float)) \replacewith( {#loc := javaMulFloat(#seFloat0, #seFloat1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -324,7 +347,7 @@ \find(\modality{#normalassign}{.. #loc = #seDouble0 * #seDouble1; ...}\endmodality (post)) - \varcond(\not \isInStrictFp) + \varcond(\not \isInStrictFp, \sub(\typeof(#loc), double)) \replacewith( {#loc := javaMulDouble(#seDouble0, #seDouble1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -336,7 +359,7 @@ \find(\modality{#normalassign}{.. #loc = #seFloat0 / #seFloat1; ...}\endmodality (post)) - \varcond(\not \isInStrictFp) + \varcond(\not \isInStrictFp, \sub(\typeof(#loc), float)) \replacewith( {#loc := javaDivFloat(#seFloat0, #seFloat1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -348,7 +371,7 @@ \find(\modality{#normalassign}{.. #loc = #seDouble0 / #seDouble1; ...}\endmodality (post)) - \varcond(\not \isInStrictFp) + \varcond(\not \isInStrictFp, \sub(\typeof(#loc), double)) \replacewith( {#loc := javaDivDouble(#seDouble0, #seDouble1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -361,6 +384,7 @@ \find(\modality{#normalassign}{.. #loc = #seFloat0 % #seFloat1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float)) \replacewith( {#loc := javaModFloat(#seFloat0, #seFloat1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -372,6 +396,7 @@ \find(\modality{#normalassign}{.. #loc = #seDouble0 % #seDouble1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), double)) \replacewith( {#loc := javaModDouble(#seDouble0, #seDouble1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -379,40 +404,6 @@ \displayname "mod" }; - // Operations on combined float/int - - intLongToFloatAddition1 { - \find(\modality{#normalassign}{.. - #loc = #seLong + #seFloat; - ...}\endmodality (post)) - \replacewith({#loc := javaAddFloat((float)#seLong, #seFloat)} - \modality{#normalassign}{.. ...}\endmodality (post)) - \heuristics(executeFloatAssignment) - \displayname "float addition" - }; - - // For int/short/char/byte, converting to float is the same as - // converting to long first, then float - intToFloatAddition { - \find(\modality{#normalassign}{.. - #loc = #seCharByteShortInt + #seFloat; - ...}\endmodality (post)) - \replacewith({#loc := javaAddFloat((float)#seCharByteShortInt, #seFloat)} - \modality{#normalassign}{.. ...}\endmodality (post)) - \heuristics(executeFloatAssignment) - \displayname "float addition" - }; - - castLongToFloatAddition2 { - \find(\modality{#normalassign}{.. - #loc = #seFloat + #seLong; - ...}\endmodality (post)) - \replacewith({#loc := javaAddFloat(#seFloat, (float)#seLong)} - \modality{#normalassign}{.. ...}\endmodality (post)) - \heuristics(executeFloatAssignment) - \displayname "float addition" - }; - // Typecasts @@ -421,6 +412,7 @@ \find(\modality{#normalassign}{.. #loc = (float) #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float)) \replacewith({#loc := (float)#seLong} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) @@ -431,6 +423,7 @@ \find(\modality{#normalassign}{.. #loc = (double) #seFloat; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), double)) \replacewith({#loc := (double)#seFloat} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) @@ -441,6 +434,7 @@ \find(\modality{#normalassign}{.. #loc = (float) #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float)) \replacewith({#loc := (float)(#seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) @@ -451,6 +445,7 @@ \find(\modality{#normalassign}{.. #loc = (double) #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), double)) \replacewith({#loc := (double)(#seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) @@ -461,6 +456,7 @@ \find(\modality{#normalassign}{.. #loc = (double) #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), double)) \replacewith({#loc := (double)#seLong} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) @@ -471,6 +467,7 @@ \find(\modality{#normalassign}{.. #loc = (float) #seFloat; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float)) \replacewith(\modality{#normalassign}{.. #loc = #seFloat; ...}\endmodality (post)) @@ -482,6 +479,7 @@ \find(\modality{#normalassign}{.. #loc = (double) #seDouble; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), double)) \replacewith(\modality{#normalassign}{.. #loc = #seDouble; ...}\endmodality (post)) @@ -493,6 +491,7 @@ \find(\modality{#normalassign}{.. #loc = (int) #seFloat; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), int)) \replacewith({#loc := (long)(#seFloat)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) @@ -503,6 +502,7 @@ \find(\modality{#normalassign}{.. #loc = (float) #seDouble; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float)) \replacewith({#loc := (float)(#seDouble)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) @@ -513,6 +513,7 @@ \find(\modality{#normalassign}{.. #loc = (long) #seFloat; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), long)) \replacewith({#loc := (long)(#seFloat)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) @@ -523,7 +524,7 @@ compound_float_cast_expression { \find(\modality{#normalassign}{.. #loc = (float) #nse; ...}\endmodality (post)) - \varcond(\newTypeOf(#v, #nse)) + \varcond(\newTypeOf(#v, #nse), \sub(\typeof(#loc), float)) \replacewith(\modality{#normalassign}{.. #typeof(#nse) #v = #nse; #loc = (float) #v; ...}\endmodality (post)) \heuristics(simplify_prog) \displayname "cast" @@ -531,7 +532,7 @@ compound_double_cast_expression { \find(\modality{#normalassign}{.. #loc = (double) #nse; ...}\endmodality (post)) - \varcond(\newTypeOf(#v, #nse)) + \varcond(\newTypeOf(#v, #nse),\sub(\typeof(#loc), double)) \replacewith(\modality{#normalassign}{.. #typeof(#nse) #v = #nse; #loc = (double) #v; ...}\endmodality (post)) \heuristics(simplify_prog) \displayname "cast" @@ -548,42 +549,42 @@ \displayname "cast" }; - unbalanced_double_float_assignment { - \find(\modality{#normalassign}{.. #loc = #seFloat; ...}\endmodality(post)) - \varcond(\sub(\typeof(#loc),double)) - \replacewith(\modality{#normalassign}{.. #loc = (double) #seFloat; ...}\endmodality(post)) - \heuristics(simplify_prog) - \displayname "cast" - }; + unbalanced_simple_double_assignment { + \find(\modality{#normalassign}{.. #loc = #se; ...}\endmodality(post)) + \varcond(\sub(\typeof(#loc),double), \sub(\typeof(#se),int)) + \replacewith(\modality{#normalassign}{.. #loc = (double) #se; ...}\endmodality(post)) + \heuristics(simplify_prog) + \displayname "cast" + }; - unbalanced_double_int_assignment { - \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt; ...}\endmodality(post)) - \varcond(\sub(\typeof(#loc),double)) - \replacewith(\modality{#normalassign}{.. #loc = (double) #seCharByteShortInt; ...}\endmodality(post)) + unbalanced_simple_float_assignment { + \find(\modality{#normalassign}{.. #loc = #se; ...}\endmodality(post)) + \varcond(\sub(\typeof(#loc),float), \sub(\typeof(#se),int)) + \replacewith(\modality{#normalassign}{.. #loc = (float) #se; ...}\endmodality(post)) \heuristics(simplify_prog) \displayname "cast" }; - unbalanced_double_long_assignment { - \find(\modality{#normalassign}{.. #loc = #seLong; ...}\endmodality(post)) - \varcond(\sub(\typeof(#loc),double)) - \replacewith(\modality{#normalassign}{.. #loc = (double) #seLong; ...}\endmodality(post)) - \heuristics(simplify_prog) - \displayname "cast" - }; + unbalanced_simple_float_to_double_assignment { + \find(\modality{#normalassign}{.. #loc = #seFloat; ...}\endmodality(post)) + \varcond(\sub(\typeof(#loc),double)) + \replacewith(\modality{#normalassign}{.. #loc = (double) #seFloat; ...}\endmodality(post)) + \heuristics(simplify_prog) + \displayname "cast" + }; - unbalanced_float_int_assignment { - \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt; ...}\endmodality(post)) - \varcond(\sub(\typeof(#loc),float)) - \replacewith(\modality{#normalassign}{.. #loc = (float) #seCharByteShortInt; ...}\endmodality(post)) + unbalanced_nonsimple_nonfloat_to_float_assignment { + \find(\modality{#normalassign}{.. #loc = #nse; ...}\endmodality(post)) + \varcond(\sub(\typeof(#loc),float), \not\sub(\typeof(#nse),float), \newTypeOf(#v, #nse)) + \replacewith(\modality{#normalassign}{.. #typeof(#nse) #v = #nse; #loc = (float) #v; ...}\endmodality(post)) \heuristics(simplify_prog) \displayname "cast" }; - unbalanced_float_long_assignment { - \find(\modality{#normalassign}{.. #loc = #seLong; ...}\endmodality(post)) - \varcond(\sub(\typeof(#loc),float)) - \replacewith(\modality{#normalassign}{.. #loc = (float) #seLong; ...}\endmodality(post)) + unbalanced_nonsimple_nonfloat_to_double_assignment { + \find(\modality{#normalassign}{.. #loc = #nse; ...}\endmodality(post)) + \varcond(\sub(\typeof(#loc),double), \not\sub(\typeof(#nse),double), \newTypeOf(#v, #nse)) + \replacewith(\modality{#normalassign}{.. #typeof(#nse) #v = #nse; #loc = (double) #v; ...}\endmodality(post)) \heuristics(simplify_prog) \displayname "cast" }; From b6603d4f1c59c18555e515c95ec64933c2471e97 Mon Sep 17 00:00:00 2001 From: Samuel Teuber Date: Tue, 4 Apr 2023 18:28:30 +0200 Subject: [PATCH 07/11] Rebuilt test oracle --- .../de/uka/ilkd/key/nparser/taclets.old.txt | 332 +++++++++++++----- 1 file changed, 251 insertions(+), 81 deletions(-) diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index 084552d436d..1985cadeedc 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -1,5 +1,5 @@ # This files contains representation of taclets, which are accepted and revised. -# Date: Mon Mar 20 13:56:02 CET 2023 +# Date: Tue Apr 04 18:24:45 CEST 2023 == abortJavaCardTransactionAPI (abortJavaCardTransactionAPI) ========================================= abortJavaCardTransactionAPI { @@ -1229,6 +1229,7 @@ assignment { \find(#allmodal ( (modal operator))\[{ .. #loc = #se; ... }\] (post)) +\varcond(\sub(\typeof(#se (program SimpleExpression)), \typeof(#loc (program Variable))), ) \replacewith(update-application(elem-update(#loc (program Variable))(#se),#allmodal(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java} @@ -1256,7 +1257,7 @@ assignmentAdditionDouble { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 + #seDouble1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1266,7 +1267,7 @@ assignmentAdditionDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 + #seDouble1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double), ) \replacewith(update-application(elem-update(#loc (program Variable))(addDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1276,7 +1277,7 @@ assignmentAdditionFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 + #seFloat1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1286,7 +1287,7 @@ assignmentAdditionFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 + #seFloat1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(addFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1296,6 +1297,7 @@ assignmentAdditionInt { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt0 + #seCharByteShortInt1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1305,6 +1307,7 @@ assignmentAdditionLong { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt + #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1314,6 +1317,7 @@ assignmentAdditionLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong + #seCharByteShortInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1323,6 +1327,7 @@ assignmentAdditionLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong0 + #seLong1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1332,6 +1337,7 @@ assignmentBitwiseAndInt { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt0 & #seCharByteShortInt1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1341,6 +1347,7 @@ assignmentBitwiseAndLong { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt & #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1350,6 +1357,7 @@ assignmentBitwiseAndLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong & #seCharByteShortInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1359,6 +1367,7 @@ assignmentBitwiseAndLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong0 & #seLong1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1368,6 +1377,7 @@ assignmentBitwiseOrInt { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt0 | #seCharByteShortInt1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1377,6 +1387,7 @@ assignmentBitwiseOrLong { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt | #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1386,6 +1397,7 @@ assignmentBitwiseOrLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong | #seCharByteShortInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1395,6 +1407,7 @@ assignmentBitwiseOrLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong0 | #seLong1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1404,6 +1417,7 @@ assignmentBitwiseXOrInt { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt0 ^ #seCharByteShortInt1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1413,6 +1427,7 @@ assignmentBitwiseXOrLong { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt ^ #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1422,6 +1437,7 @@ assignmentBitwiseXOrLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong ^ #seCharByteShortInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1431,6 +1447,7 @@ assignmentBitwiseXOrLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong0 ^ #seLong1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1460,7 +1477,7 @@ assignmentDivisionDouble { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 / #seDouble1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaDivDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1470,7 +1487,7 @@ assignmentDivisionDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 / #seDouble1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double), ) \replacewith(update-application(elem-update(#loc (program Variable))(divDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1480,7 +1497,7 @@ assignmentDivisionFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 / #seFloat1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaDivFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1490,7 +1507,7 @@ assignmentDivisionFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 / #seFloat1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(divFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1500,6 +1517,7 @@ assignmentDivisionInt { \find(==>#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt0 / #seCharByteShortInt1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith([]==>[not(equals(#seCharByteShortInt1,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1510,6 +1528,7 @@ assignmentDivisionLong { \find(==>#normalassign ( (modal operator))\[{ .. #loc = #se / #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith([]==>[not(equals(#seLong,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivLong(#se,#seLong)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1520,6 +1539,7 @@ assignmentDivisionLong2 { \find(==>#normalassign ( (modal operator))\[{ .. #loc = #seLong / #seCharByteShortInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith([]==>[not(equals(#seCharByteShortInt,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivLong(#seLong,#seCharByteShortInt)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1530,6 +1550,7 @@ assignmentModDouble { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 % #seDouble1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaModDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1539,6 +1560,7 @@ assignmentModFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 % #seFloat1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaModFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1548,6 +1570,7 @@ assignmentModulo { \find(==>#normalassign ( (modal operator))\[{ .. #loc = #se0 % #se1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), \sub(\typeof(#loc (program Variable)), int), ) \replacewith([]==>[not(equals(#se1,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaMod(#se0,#se1)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1596,7 +1619,7 @@ assignmentMultiplicationDouble { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 * #seDouble1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1606,7 +1629,7 @@ assignmentMultiplicationDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 * #seDouble1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double), ) \replacewith(update-application(elem-update(#loc (program Variable))(mulDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1616,7 +1639,7 @@ assignmentMultiplicationFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 * #seFloat1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1626,7 +1649,7 @@ assignmentMultiplicationFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 * #seFloat1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(mulFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1636,6 +1659,7 @@ assignmentMultiplicationInt { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt0 * #seCharByteShortInt1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1645,6 +1669,7 @@ assignmentMultiplicationLong { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt * #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1654,6 +1679,7 @@ assignmentMultiplicationLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong * #seCharByteShortInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1663,6 +1689,7 @@ assignmentMultiplicationLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong0 * #seLong1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1672,6 +1699,7 @@ assignmentShiftLeftInt { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt0 << #se; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1681,6 +1709,7 @@ assignmentShiftLeftLong { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong0 << #se; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1690,6 +1719,7 @@ assignmentShiftRightInt { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt0 >> #se; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1699,6 +1729,7 @@ assignmentShiftRightLong { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong0 >> #se; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1726,7 +1757,7 @@ assignmentSubtractionDouble { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 - #seDouble1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1736,7 +1767,7 @@ assignmentSubtractionDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seDouble0 - #seDouble1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double), ) \replacewith(update-application(elem-update(#loc (program Variable))(subDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1746,7 +1777,7 @@ assignmentSubtractionFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 - #seFloat1; ... }\] (post)) -\varcond(\not\isStrictFp, ) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1756,7 +1787,7 @@ assignmentSubtractionFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc = #seFloat0 - #seFloat1; ... }\] (post)) -\varcond(\isStrictFp, ) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(subFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1766,6 +1797,7 @@ assignmentSubtractionInt { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt0 - #seCharByteShortInt1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1775,6 +1807,7 @@ assignmentSubtractionLong { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt - #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1784,6 +1817,7 @@ assignmentSubtractionLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong - #seCharByteShortInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1793,6 +1827,7 @@ assignmentSubtractionLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong0 - #seLong1; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1802,6 +1837,7 @@ assignmentUnsignedShiftRightInt { \find(#normalassign ( (modal operator))\[{ .. #loc = #seCharByteShortInt0 >>> #se; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1811,6 +1847,7 @@ assignmentUnsignedShiftRightLong { \find(#normalassign ( (modal operator))\[{ .. #loc = #seLong0 >>> #se; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -2422,6 +2459,7 @@ bitwiseNegationInt { \find(#normalassign ( (modal operator))\[{ .. #loc = ~#seCharByteShortInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseNegateInt(#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -2431,6 +2469,7 @@ bitwiseNegationLong { \find(#normalassign ( (modal operator))\[{ .. #loc = ~#se; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseNegateLong(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -3430,15 +3469,6 @@ castDel2 { Choices: true} ----------------------------------------------------- -== castLongToFloatAddition2 (float addition) ========================================= -castLongToFloatAddition2 { -\find(#normalassign ( (modal operator))\[{ .. - #loc = #seFloat + #seLong; -... }\] (post)) -\replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(#seFloat,float::cast(#seLong))),#normalassign(post))) -\heuristics(executeFloatAssignment) -Choices: programRules:Java} ------------------------------------------------------ == castToBoolean (castToBoolean) ========================================= castToBoolean { \find(#allmodal ( (modal operator))\[{ .. @@ -4417,7 +4447,7 @@ compound_double_cast_expression { \find(#normalassign ( (modal operator))\[{ .. #loc = (double) #nse; ... }\] (post)) -\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), double), ) \replacewith(#normalassign ( (modal operator))\[{ .. #typeof(#nse) #v = #nse; #loc = (double) #v; @@ -4457,7 +4487,7 @@ compound_float_cast_expression { \find(#normalassign ( (modal operator))\[{ .. #loc = (float) #nse; ... }\] (post)) -\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), float), ) \replacewith(#normalassign ( (modal operator))\[{ .. #typeof(#nse) #v = #nse; #loc = (float) #v; @@ -9207,6 +9237,34 @@ expIsZero { \heuristics(userTaclets1) Choices: true} ----------------------------------------------------- +== expandInByte (expandInByte) ========================================= +expandInByte { +\find(inByte(i)) +\replacewith(true) +\heuristics(concrete) +Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} +----------------------------------------------------- +== expandInChar (expandInChar) ========================================= +expandInChar { +\find(inChar(i)) +\replacewith(true) +\heuristics(concrete) +Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} +----------------------------------------------------- +== expandInInt (expandInInt) ========================================= +expandInInt { +\find(inInt(i)) +\replacewith(true) +\heuristics(concrete) +Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} +----------------------------------------------------- +== expandInLong (expandInLong) ========================================= +expandInLong { +\find(inLong(i)) +\replacewith(true) +\heuristics(concrete) +Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} +----------------------------------------------------- == expandInRangeByte (expandInRangeByte) ========================================= expandInRangeByte { \find(inRangeByte(i)) @@ -9242,6 +9300,13 @@ expandInRangeShort { \heuristics(delayedExpansion, defOps_expandRanges) Choices: true} ----------------------------------------------------- +== expandInShort (expandInShort) ========================================= +expandInShort { +\find(inShort(i)) +\replacewith(true) +\heuristics(concrete) +Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} +----------------------------------------------------- == expand_addJint (expand_addJint) ========================================= expand_addJint { \find(addJint(i,i1)) @@ -9270,41 +9335,6 @@ expand_divJlong { \heuristics(defOps_expandJNumericOp) Choices: true} ----------------------------------------------------- -== expandInByte (expandInByte) ========================================= -expandInByte { -\find(inByte(i)) -\replacewith(true) -\heuristics(concrete) -Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} ------------------------------------------------------ -== expandInChar (expandInChar) ========================================= -expandInChar { -\find(inChar(i)) -\replacewith(true) -\heuristics(concrete) -Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} ------------------------------------------------------ -== expandInInt (expandInInt) ========================================= -expandInInt { -\find(inInt(i)) -\replacewith(true) -\heuristics(concrete) -Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} ------------------------------------------------------ -== expandInLong (expandInLong) ========================================= -expandInLong { -\find(inLong(i)) -\replacewith(true) -\heuristics(concrete) -Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} ------------------------------------------------------ -== expandInShort (expandInShort) ========================================= -expandInShort { -\find(inShort(i)) -\replacewith(true) -\heuristics(concrete) -Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} ------------------------------------------------------ == expand_modJint (expand_modJint) ========================================= expand_modJint { \find(modJint(i,i1)) @@ -9860,6 +9890,7 @@ identityCastDouble { \find(#normalassign ( (modal operator))\[{ .. #loc = (double) #seDouble; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), ) \replacewith(#normalassign ( (modal operator))\[{ .. #loc = #seDouble; ... }\] (post)) @@ -9871,6 +9902,7 @@ identityCastFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = (float) #seFloat; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), ) \replacewith(#normalassign ( (modal operator))\[{ .. #loc = #seFloat; ... }\] (post)) @@ -11447,24 +11479,6 @@ intDivRem { Choices: true} ----------------------------------------------------- -== intLongToFloatAddition1 (float addition) ========================================= -intLongToFloatAddition1 { -\find(#normalassign ( (modal operator))\[{ .. - #loc = #seLong + #seFloat; -... }\] (post)) -\replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(float::cast(#seLong),#seFloat)),#normalassign(post))) -\heuristics(executeFloatAssignment) -Choices: programRules:Java} ------------------------------------------------------ -== intToFloatAddition (float addition) ========================================= -intToFloatAddition { -\find(#normalassign ( (modal operator))\[{ .. - #loc = #seCharByteShortInt + #seFloat; -... }\] (post)) -\replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(float::cast(#seCharByteShortInt),#seFloat)),#normalassign(post))) -\heuristics(executeFloatAssignment) -Choices: programRules:Java} ------------------------------------------------------ == int_diff_minus_eq (int_diff_minus_eq) ========================================= int_diff_minus_eq { \find(sub(i0,neg(i1))) @@ -13464,6 +13478,7 @@ narrowingByteCastInt { \find(#normalassign ( (modal operator))\[{ .. #loc = (byte) #seInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -13473,6 +13488,7 @@ narrowingByteCastLong { \find(#normalassign ( (modal operator))\[{ .. #loc = (byte) #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -13482,15 +13498,27 @@ narrowingByteCastShort { \find(#normalassign ( (modal operator))\[{ .. #loc = (byte) #seShort; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seShort)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- +== narrowingCastDoubleToFloat (cast) ========================================= +narrowingCastDoubleToFloat { +\find(#normalassign ( (modal operator))\[{ .. + #loc = (float) #seDouble; +... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), ) +\replacewith(update-application(elem-update(#loc (program Variable))(float::cast(#seDouble)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == narrowingCastFloatToInt (cast) ========================================= narrowingCastFloatToInt { \find(#normalassign ( (modal operator))\[{ .. #loc = (int) #seFloat; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(int::cast(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -13500,6 +13528,7 @@ narrowingCastFloatToLong { \find(#normalassign ( (modal operator))\[{ .. #loc = (long) #seFloat; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(int::cast(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -13518,6 +13547,7 @@ narrowingCharCastByte { \find(#normalassign ( (modal operator))\[{ .. #loc = (char) #seByte; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seByte)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -13527,6 +13557,7 @@ narrowingCharCastInt { \find(#normalassign ( (modal operator))\[{ .. #loc = (char) #seInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -13536,6 +13567,7 @@ narrowingCharCastLong { \find(#normalassign ( (modal operator))\[{ .. #loc = (char) #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -13545,6 +13577,7 @@ narrowingCharCastShort { \find(#normalassign ( (modal operator))\[{ .. #loc = (char) #seShort; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seShort)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -13563,6 +13596,7 @@ narrowingIntCastLong { \find(#normalassign ( (modal operator))\[{ .. #loc = (int) #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastInt(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -13590,6 +13624,7 @@ narrowingShortCastInt { \find(#normalassign ( (modal operator))\[{ .. #loc = (short) #seInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -13599,6 +13634,7 @@ narrowingShortCastLong { \find(#normalassign ( (modal operator))\[{ .. #loc = (short) #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -18110,24 +18146,51 @@ unaryMinusDouble { \find(#normalassign ( (modal operator))\[{ .. #loc = -#seDouble; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusDouble(#seDouble)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} ----------------------------------------------------- +== unaryMinusDouble_cast (cast) ========================================= +unaryMinusDouble_cast { +\find(#normalassign ( (modal operator))\[{ .. + #loc = -#se; +... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), \not\sub(\typeof(#se (program SimpleExpression)), double), ) +\replacewith(#normalassign ( (modal operator))\[{ .. + #loc = (double) (-#se); +... }\] (post)) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == unaryMinusFloat (unaryMinus) ========================================= unaryMinusFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = -#seFloat; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusFloat(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} ----------------------------------------------------- +== unaryMinusFloat_cast (cast) ========================================= +unaryMinusFloat_cast { +\find(#normalassign ( (modal operator))\[{ .. + #loc = -#se; +... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), \not\sub(\typeof(#se (program SimpleExpression)), float), ) +\replacewith(#normalassign ( (modal operator))\[{ .. + #loc = (float) (-#se); +... }\] (post)) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == unaryMinusInt (unaryMinus) ========================================= unaryMinusInt { \find(#normalassign ( (modal operator))\[{ .. #loc = -#seCharByteShortInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusInt(#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -18137,10 +18200,85 @@ unaryMinusLong { \find(#normalassign ( (modal operator))\[{ .. #loc = -#seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), ) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusLong(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- +== unbalanced_float_expression (cast) ========================================= +unbalanced_float_expression { +\find(#normalassign ( (modal operator))\[{ .. + #loc = #unbalancedFloat; +... }\] (post)) +\varcond(\floatingPointBalanced(#unbalancedFloat (program FloatingPointBinaryExpression), #balancedFloat (program FloatingPointBinaryExpression)), ) +\replacewith(#normalassign ( (modal operator))\[{ .. + #loc = #balancedFloat; +... }\] (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_nonsimple_nonfloat_to_double_assignment (cast) ========================================= +unbalanced_nonsimple_nonfloat_to_double_assignment { +\find(#normalassign ( (modal operator))\[{ .. + #loc = #nse; +... }\] (post)) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), double), \not\sub(\typeof(#nse (program NonSimpleExpression)), double), ) +\replacewith(#normalassign ( (modal operator))\[{ .. + #typeof(#nse) #v = #nse; + #loc = (double) #v; +... }\] (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_nonsimple_nonfloat_to_float_assignment (cast) ========================================= +unbalanced_nonsimple_nonfloat_to_float_assignment { +\find(#normalassign ( (modal operator))\[{ .. + #loc = #nse; +... }\] (post)) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), float), \not\sub(\typeof(#nse (program NonSimpleExpression)), float), ) +\replacewith(#normalassign ( (modal operator))\[{ .. + #typeof(#nse) #v = #nse; + #loc = (float) #v; +... }\] (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_simple_double_assignment (cast) ========================================= +unbalanced_simple_double_assignment { +\find(#normalassign ( (modal operator))\[{ .. + #loc = #se; +... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), \sub(\typeof(#se (program SimpleExpression)), int), ) +\replacewith(#normalassign ( (modal operator))\[{ .. + #loc = (double) #se; +... }\] (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_simple_float_assignment (cast) ========================================= +unbalanced_simple_float_assignment { +\find(#normalassign ( (modal operator))\[{ .. + #loc = #se; +... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), \sub(\typeof(#se (program SimpleExpression)), int), ) +\replacewith(#normalassign ( (modal operator))\[{ .. + #loc = (float) #se; +... }\] (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_simple_float_to_double_assignment (cast) ========================================= +unbalanced_simple_float_to_double_assignment { +\find(#normalassign ( (modal operator))\[{ .. + #loc = #seFloat; +... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), ) +\replacewith(#normalassign ( (modal operator))\[{ .. + #loc = (double) #seFloat; +... }\] (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- == unionEqualsEmpty (unionEqualsEmpty) ========================================= unionEqualsEmpty { \find(equals(union(s,s2),empty)) @@ -18467,20 +18605,52 @@ wellFormedStorePrimitiveEQ { \heuristics(concrete) Choices: programRules:Java} ----------------------------------------------------- +== wideningCastFloatToDouble (cast) ========================================= +wideningCastFloatToDouble { +\find(#normalassign ( (modal operator))\[{ .. + #loc = (double) #seFloat; +... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), ) +\replacewith(update-application(elem-update(#loc (program Variable))(double::cast(#seFloat)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- +== wideningCastIntToDouble (cast) ========================================= +wideningCastIntToDouble { +\find(#normalassign ( (modal operator))\[{ .. + #loc = (double) #seCharByteShortInt; +... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), ) +\replacewith(update-application(elem-update(#loc (program Variable))(double::cast(#seCharByteShortInt)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == wideningCastIntToFloat (cast) ========================================= wideningCastIntToFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = (float) #seCharByteShortInt; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(float::cast(#seCharByteShortInt)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} ----------------------------------------------------- +== wideningCastLongToDouble (cast) ========================================= +wideningCastLongToDouble { +\find(#normalassign ( (modal operator))\[{ .. + #loc = (double) #seLong; +... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), ) +\replacewith(update-application(elem-update(#loc (program Variable))(double::cast(#seLong)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == wideningCastLongToFloat (cast) ========================================= wideningCastLongToFloat { \find(#normalassign ( (modal operator))\[{ .. #loc = (float) #seLong; ... }\] (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), ) \replacewith(update-application(elem-update(#loc (program Variable))(float::cast(#seLong)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} From d05f402c4f03f1ed5f34941354671c27c1f48701 Mon Sep 17 00:00:00 2001 From: Samuel Teuber Date: Wed, 5 Apr 2023 13:36:43 +0200 Subject: [PATCH 08/11] Fix spotless --- .../de/uka/ilkd/key/logic/sort/ProgramSVSort.java | 10 ++++------ .../FloatingPointBalancedCondition.java | 15 ++++----------- 2 files changed, 8 insertions(+), 17 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index baf08f61d53..2f823d2ee9a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java @@ -3,8 +3,6 @@ import java.util.LinkedHashMap; import java.util.Map; -import de.uka.ilkd.key.java.expression.Operator; -import de.uka.ilkd.key.java.expression.operator.*; import de.uka.ilkd.key.java.Expression; import de.uka.ilkd.key.java.Label; import de.uka.ilkd.key.java.NamedProgramElement; @@ -21,7 +19,9 @@ import de.uka.ilkd.key.java.declaration.VariableSpecification; import de.uka.ilkd.key.java.expression.ArrayInitializer; import de.uka.ilkd.key.java.expression.Literal; +import de.uka.ilkd.key.java.expression.Operator; import de.uka.ilkd.key.java.expression.literal.StringLiteral; +import de.uka.ilkd.key.java.expression.operator.*; import de.uka.ilkd.key.java.expression.operator.adt.*; import de.uka.ilkd.key.java.reference.*; import de.uka.ilkd.key.java.statement.Catch; @@ -1109,10 +1109,8 @@ public boolean canStandFor(ProgramElement check, ExecutionContext ec, Services s return false; } Operator bin = (Operator) check; - if ( - !SIMPLEEXPRESSION.canStandFor(bin.getChildAt(0), ec, services) || - !SIMPLEEXPRESSION.canStandFor(bin.getChildAt(1), ec, services) - ) { + if (!SIMPLEEXPRESSION.canStandFor(bin.getChildAt(0), ec, services) || + !SIMPLEEXPRESSION.canStandFor(bin.getChildAt(1), ec, services)) { return false; } KeYJavaType t1 = getKeYJavaType(bin.getChildAt(0), ec, services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java index 338590a5218..923944e8d4a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java @@ -1,5 +1,7 @@ package de.uka.ilkd.key.rule.conditions; +import javax.annotation.Nullable; + import de.uka.ilkd.key.java.Expression; import de.uka.ilkd.key.java.JavaProgramElement; import de.uka.ilkd.key.java.ProgramElement; @@ -11,23 +13,13 @@ import de.uka.ilkd.key.java.expression.operator.TypeCast; import de.uka.ilkd.key.java.reference.TypeRef; import de.uka.ilkd.key.java.visitor.ProgramElementReplacer; -import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.TermServices; -import de.uka.ilkd.key.logic.op.ElementaryUpdate; -import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; -import de.uka.ilkd.key.logic.op.UpdateApplication; -import de.uka.ilkd.key.logic.op.UpdateJunctor; import de.uka.ilkd.key.logic.sort.Sort; -import de.uka.ilkd.key.proof.TermProgramVariableCollector; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.VariableCondition; import de.uka.ilkd.key.rule.inst.SVInstantiations; -import javax.annotation.Nullable; -import java.util.Set; - /** * This variable condition adds required numeric promotions to Java operations @@ -67,7 +59,8 @@ public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, Mat SVInstantiations svInst = mc.getInstantiations(); Object untypedInstantiation = svInst.getInstantiation(unbalanced); - if (!(untypedInstantiation instanceof BinaryOperator || untypedInstantiation instanceof ComparativeOperator)) { + if (!(untypedInstantiation instanceof BinaryOperator + || untypedInstantiation instanceof ComparativeOperator)) { return null; } Operator inInst = (Operator) untypedInstantiation; From 3bac17756d200b136cb8e6f3f77a0672d9508562 Mon Sep 17 00:00:00 2001 From: Drodt Date: Fri, 10 Apr 2026 15:27:29 +0200 Subject: [PATCH 09/11] Fix merge errors --- .../varexp/TacletBuilderManipulators.java | 3 +- .../FloatingPointBalancedCondition.java | 48 +++++++++++-------- .../key/rule/conditions/TypeResolver.java | 1 + 3 files changed, 30 insertions(+), 22 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java index 82a1131b458..1777edb94d6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java @@ -385,7 +385,8 @@ public IsLabeledCondition build(Object[] arguments, List parameters, applyUpdateOnRigid, DROP_EFFECTLESS_ELEMENTARIES, SIMPLIFY_ITE_UPDATE, SUBFORMULAS, STATIC_FIELD, MODEL_FIELD, SUBFORMULA, DROP_EFFECTLESS_STORES, EQUAL_UNIQUE, META_DISJOINT, - IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP, FLOATING_POINT_BALANCED); + IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP, + FLOATING_POINT_BALANCED); register(STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, GET_INVARIANT, GET_FREE_INVARIANT, GET_VARIANT, IS_LABELED); loadWithServiceLoader(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java index 923944e8d4a..d326269232e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java @@ -1,25 +1,30 @@ +/* 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.rule.conditions; -import javax.annotation.Nullable; - -import de.uka.ilkd.key.java.Expression; -import de.uka.ilkd.key.java.JavaProgramElement; -import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.java.abstraction.KeYJavaType; -import de.uka.ilkd.key.java.expression.Operator; -import de.uka.ilkd.key.java.expression.operator.BinaryOperator; -import de.uka.ilkd.key.java.expression.operator.ComparativeOperator; -import de.uka.ilkd.key.java.expression.operator.TypeCast; -import de.uka.ilkd.key.java.reference.TypeRef; +import de.uka.ilkd.key.java.ast.JavaProgramElement; +import de.uka.ilkd.key.java.ast.ProgramElement; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.Operator; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.ast.expression.operator.ComparativeOperator; +import de.uka.ilkd.key.java.ast.expression.operator.TypeCast; +import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.java.visitor.ProgramElementReplacer; -import de.uka.ilkd.key.logic.op.SVSubstitute; -import de.uka.ilkd.key.logic.op.SchemaVariable; -import de.uka.ilkd.key.logic.sort.Sort; -import de.uka.ilkd.key.rule.MatchConditions; -import de.uka.ilkd.key.rule.VariableCondition; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.logic.sort.Sort; +import org.key_project.prover.rules.VariableCondition; +import org.key_project.prover.rules.instantiation.MatchResultInfo; + +import org.jspecify.annotations.Nullable; + /** * This variable condition adds required numeric promotions to Java operations @@ -54,22 +59,23 @@ public FloatingPointBalancedCondition(SchemaVariable unbalanced, SchemaVariable } @Override - public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, - Services services) { + public MatchResultInfo check(SchemaVariable var, SyntaxElement instCandidate, + MatchResultInfo mc, + LogicServices services) { - SVInstantiations svInst = mc.getInstantiations(); + var svInst = (SVInstantiations) mc.getInstantiations(); Object untypedInstantiation = svInst.getInstantiation(unbalanced); if (!(untypedInstantiation instanceof BinaryOperator || untypedInstantiation instanceof ComparativeOperator)) { return null; } Operator inInst = (Operator) untypedInstantiation; - JavaProgramElement outInst = (JavaProgramElement) svInst.getInstantiation(balanced); + JavaProgramElement outInst = svInst.getInstantiation(balanced); if (inInst == null) { return mc; } - Operator properResultInst = balance(inInst, services); + Operator properResultInst = balance(inInst, (Services) services); if (properResultInst == null) { return null; } else if (outInst == null) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java index 7d763dc22de..1255129f598 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.ProgramElement; import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.*; From 593ffacb421111820c1108f67acca9d59a58bf5a Mon Sep 17 00:00:00 2001 From: Drodt Date: Fri, 10 Apr 2026 15:39:56 +0200 Subject: [PATCH 10/11] Fix rules --- .../integer/integerAssignment2UpdateRules.key | 63 +++++++++---------- 1 file changed, 31 insertions(+), 32 deletions(-) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerAssignment2UpdateRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerAssignment2UpdateRules.key index 2f5489e7d81..bbe65f82a8b 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerAssignment2UpdateRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerAssignment2UpdateRules.key @@ -42,8 +42,8 @@ \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt0 * #seCharByteShortInt1; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1))) @@ -58,8 +58,8 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt * #seLong; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(mul(#seCharByteShortInt, #seLong))) @@ -74,8 +74,8 @@ \find(\modality{#normalassign}{.. #loc=#seLong * #seCharByteShortInt; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(mul(#seLong, #seCharByteShortInt))) @@ -90,8 +90,8 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 * #seLong1; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(mul(#seLong0, #seLong1))) @@ -301,8 +301,8 @@ \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt0 - #seCharByteShortInt1; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1))) @@ -317,8 +317,8 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt - #seLong; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(sub(#seCharByteShortInt, #seLong))) @@ -333,8 +333,8 @@ \find(\modality{#normalassign}{.. #loc=#seLong - #seCharByteShortInt; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(sub(#seLong, #seCharByteShortInt))) @@ -350,8 +350,8 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 - #seLong1; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(sub(#seLong0, #seLong1))) @@ -368,8 +368,8 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 + #seCharByteShortInt1; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(add(#seCharByteShortInt0, #seCharByteShortInt1))) @@ -385,8 +385,8 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt + #seLong; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(add(#seCharByteShortInt, #seLong))) @@ -402,8 +402,8 @@ \find(\modality{#normalassign}{.. #loc=#seLong + #seCharByteShortInt; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(add(#seLong, #seCharByteShortInt))) @@ -419,8 +419,8 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 + #seLong1; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(add(#seLong0, #seLong1))) @@ -590,8 +590,8 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 >> #se; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(shiftright(#seLong0, #se))) @@ -607,8 +607,8 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 >> #se; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(shiftright(#seLong0, #se))) @@ -626,8 +626,8 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 << #se; ...} \endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(shiftleft(#seCharByteShortInt0, #se))) @@ -643,8 +643,8 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 << #se; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(shiftleft(#seLong0, #se))) @@ -662,8 +662,8 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 >>> #se; ...} \endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(unsignedshiftrightJint(#seCharByteShortInt0, #se))) @@ -679,8 +679,8 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 >>> #se; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(unsignedshiftrightJlong(#seLong0, #se))) @@ -699,8 +699,8 @@ \find(\modality{#normalassign}{.. #loc = - #seCharByteShortInt; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(neg(#seCharByteShortInt))) @@ -715,8 +715,8 @@ \find(\modality{#normalassign}{.. #loc = - #seLong; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(neg(#seLong))) @@ -737,9 +737,8 @@ }; bitwiseNegationLong { - \find(\modality{#normalassign}{.. #loc = ~ #se; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \find(\modality{#normalassign}{.. #loc = ~ #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith({#loc := javaBitwiseNegateLong(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeIntegerAssignment) @@ -754,8 +753,8 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seShort; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inByte(#seShort)) @@ -770,8 +769,8 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seInt; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inByte(#seInt)) @@ -786,8 +785,8 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seLong; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inByte(#seLong)) @@ -802,8 +801,8 @@ \find(\modality{#normalassign}{.. #loc = (short) #seInt; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inShort(#seInt)) @@ -818,8 +817,8 @@ \find(\modality{#normalassign}{.. #loc = (short) #seLong; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inShort(#seLong)) @@ -832,8 +831,8 @@ narrowingIntCastLong { \find(\modality{#normalassign}{.. #loc = (int) #seLong; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(#seLong)) @@ -848,8 +847,8 @@ \find(\modality{#normalassign}{.. #loc = (char) #seByte; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inChar(#seByte)) @@ -865,8 +864,8 @@ \find(\modality{#normalassign}{.. #loc = (char) #seShort; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inChar(#seShort)) @@ -882,8 +881,8 @@ \find(\modality{#normalassign}{.. #loc = (char) #seInt; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inChar(#seInt)) @@ -898,8 +897,8 @@ \find(\modality{#normalassign}{.. #loc = (char) #seLong; ...}\endmodality (post)) - \varcond(\sub(\typeof(#loc),int)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inChar(#seLong)) From 1a8be8d05e291cf4a530136fbefc9bb1f820ac78 Mon Sep 17 00:00:00 2001 From: Drodt Date: Sat, 11 Apr 2026 10:13:59 +0200 Subject: [PATCH 11/11] Regenerate taclets.old.txt --- .../de/uka/ilkd/key/nparser/taclets.old.txt | 444 ++++++++++++------ 1 file changed, 307 insertions(+), 137 deletions(-) diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index ffb4cb55fc2..542086b4476 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -1,5 +1,5 @@ # This files contains representation of taclets, which are accepted and revised. -# Date: Wed Nov 19 11:46:34 CET 2025 +# Date: Sat Apr 11 10:11:51 CEST 2026 == abortJavaCardTransactionAPI (abortJavaCardTransactionAPI) ========================================= abortJavaCardTransactionAPI { @@ -17,7 +17,7 @@ abortJavaCardTransactionBox { \find(==>box_transaction|{{ .. #abortJavaCardTransaction; ... }}| (post)) -\replacewith([]==>[update-application(elem-update(heap)(anon(savedHeap,allObjects(java.lang.Object::#$transactionConditionallyUpdated),heap)),box(post))]) +\replacewith([]==>[update-application(elem-update(heap)(anon(savedHeap,allObjects(java.lang.Object::#$transactionConditionallyUpdated),heap)),box(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)} ----------------------------------------------------- @@ -26,7 +26,7 @@ abortJavaCardTransactionDiamond { \find(==>diamond_transaction|{{ .. #abortJavaCardTransaction; ... }}| (post)) -\replacewith([]==>[update-application(elem-update(heap)(anon(savedHeap,allObjects(java.lang.Object::#$transactionConditionallyUpdated),heap)),diamond(post))]) +\replacewith([]==>[update-application(elem-update(heap)(anon(savedHeap,allObjects(java.lang.Object::#$transactionConditionallyUpdated),heap)),diamond(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)} ----------------------------------------------------- @@ -679,7 +679,7 @@ allocateInstance { #lhs = #t.#allocate()@#t; ... }}| (post)) \varcond(\hasSort(#t2 (program Type), alphaObj)) -\add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),equals(boolean::select(heap,#lhs,java.lang.Object::#$created),FALSE))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(create(heap,#lhs)),#allmodal(post))]) +\add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),equals(boolean::select(heap,#lhs,java.lang.Object::#$created),FALSE))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(create(heap,#lhs)),#allmodal(post))]) \heuristics(method_expand) Choices: (programRules:Java & permissions:off)} ----------------------------------------------------- @@ -689,7 +689,7 @@ allocateInstanceWithLength { #lhs = #t.#allocate(#len)@#t; ... }}| (post)) \varcond(\hasSort(#t2 (program Type), alphaObj)) -\add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),and(equals(boolean::select(heap,#lhs,java.lang.Object::#$created),FALSE),equals(length(#lhs),#len)))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(store(store(create(heap,#lhs),#lhs,java.lang.Object::#$transient,Z(0(#))),#lhs,java.lang.Object::#$transactionConditionallyUpdated,FALSE)),#allmodal(post))]) +\add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),and(equals(boolean::select(heap,#lhs,java.lang.Object::#$created),FALSE),equals(length(#lhs),#len)))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(store(store(create(heap,#lhs),#lhs,java.lang.Object::#$transient,Z(0(#))),#lhs,java.lang.Object::#$transactionConditionallyUpdated,FALSE)),#allmodal(post))]) \heuristics(method_expand) Choices: (programRules:Java & permissions:off)} ----------------------------------------------------- @@ -1235,7 +1235,7 @@ Choices: (programRules:Java & assertions:safe)} assignableDefinition { \find(assignable(heapNew,heapOld,locs)) \varcond(\notFreeIn(f (variable), heapNew (Heap term)), \notFreeIn(f (variable), heapOld (Heap term)), \notFreeIn(f (variable), locs (LocSet term)), \notFreeIn(o (variable), heapNew (Heap term)), \notFreeIn(o (variable), heapOld (Heap term)), \notFreeIn(o (variable), locs (LocSet term))) -\replacewith(all{f (variable)}(all{o (variable)}(or(or(elementOf(o,f,locs),and(not(equals(o,null)),not(equals(boolean::select(heapOld,o,java.lang.Object::#$created),TRUE)))),equals(any::select(heapNew,o,f),any::select(heapOld,o,f)))))) +\replacewith(all{f (variable)}(all{o (variable)}(or(or(elementOf(o,f,locs),and(not(equals(o,null)),not(equals(boolean::select(heapOld,o,java.lang.Object::#$created),TRUE)))),equals(any::select(heapNew,o,f),any::select(heapOld,o,f)))))) \heuristics(delayedExpansion) Choices: programRules:Java} ----------------------------------------------------- @@ -1244,6 +1244,7 @@ assignment { \find(#allmodal ((modal operator))|{{ .. #loc = #se; ... }}| (post)) +\varcond(\sub(\typeof(#se (program SimpleExpression)), \typeof(#loc (program Variable)))) \replacewith(update-application(elem-update(#loc (program Variable))(#se),#allmodal(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java} @@ -1271,7 +1272,7 @@ assignmentAdditionDouble { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 + #seDouble1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1281,7 +1282,7 @@ assignmentAdditionDoubleStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 + #seDouble1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(addDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1291,7 +1292,7 @@ assignmentAdditionFloat { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 + #seFloat1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1301,7 +1302,7 @@ assignmentAdditionFloatStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 + #seFloat1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(addFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1311,7 +1312,8 @@ assignmentAdditionInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 + #seCharByteShortInt1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaAddInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1320,7 +1322,8 @@ assignmentAdditionLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt + #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seCharByteShortInt,#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1329,7 +1332,8 @@ assignmentAdditionLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong + #seCharByteShortInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong,#seCharByteShortInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1338,7 +1342,8 @@ assignmentAdditionLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 + #seLong1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong0,#seLong1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1347,6 +1352,7 @@ assignmentBitwiseAndInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 & #seCharByteShortInt1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1356,6 +1362,7 @@ assignmentBitwiseAndLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt & #seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1365,6 +1372,7 @@ assignmentBitwiseAndLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong & #seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1374,6 +1382,7 @@ assignmentBitwiseAndLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 & #seLong1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1383,6 +1392,7 @@ assignmentBitwiseOrInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 | #seCharByteShortInt1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1392,6 +1402,7 @@ assignmentBitwiseOrLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt | #seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1401,6 +1412,7 @@ assignmentBitwiseOrLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong | #seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1410,6 +1422,7 @@ assignmentBitwiseOrLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 | #seLong1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1419,6 +1432,7 @@ assignmentBitwiseXOrInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 ^ #seCharByteShortInt1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1428,6 +1442,7 @@ assignmentBitwiseXOrLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt ^ #seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1437,6 +1452,7 @@ assignmentBitwiseXOrLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong ^ #seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1446,6 +1462,7 @@ assignmentBitwiseXOrLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 ^ #seLong1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1475,7 +1492,7 @@ assignmentDivisionDouble { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 / #seDouble1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaDivDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1485,7 +1502,7 @@ assignmentDivisionDoubleStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 / #seDouble1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(divDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1495,7 +1512,7 @@ assignmentDivisionFloat { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 / #seFloat1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaDivFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1505,7 +1522,7 @@ assignmentDivisionFloatStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 / #seFloat1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(divFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1515,6 +1532,7 @@ assignmentDivisionInt { \find(==>#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 / #seCharByteShortInt1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith([]==>[not(equals(#seCharByteShortInt1,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1525,6 +1543,7 @@ assignmentDivisionLong { \find(==>#normalassign ((modal operator))|{{ .. #loc = #se / #seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith([]==>[not(equals(#seLong,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivLong(#se,#seLong)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1535,6 +1554,7 @@ assignmentDivisionLong2 { \find(==>#normalassign ((modal operator))|{{ .. #loc = #seLong / #seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith([]==>[not(equals(#seCharByteShortInt,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivLong(#seLong,#seCharByteShortInt)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1545,6 +1565,7 @@ assignmentModDouble { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 % #seDouble1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaModDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1554,6 +1575,7 @@ assignmentModFloat { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 % #seFloat1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaModFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1563,6 +1585,7 @@ assignmentModulo { \find(==>#normalassign ((modal operator))|{{ .. #loc = #se0 % #se1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), \sub(\typeof(#loc (program Variable)), int)) \replacewith([]==>[not(equals(#se1,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaMod(#se0,#se1)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1611,7 +1634,7 @@ assignmentMultiplicationDouble { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 * #seDouble1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1621,7 +1644,7 @@ assignmentMultiplicationDoubleStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 * #seDouble1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(mulDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1631,7 +1654,7 @@ assignmentMultiplicationFloat { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 * #seFloat1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1641,7 +1664,7 @@ assignmentMultiplicationFloatStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 * #seFloat1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(mulFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1651,7 +1674,8 @@ assignmentMultiplicationInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 * #seCharByteShortInt1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaMulInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1660,7 +1684,8 @@ assignmentMultiplicationLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt * #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seCharByteShortInt,#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1669,7 +1694,8 @@ assignmentMultiplicationLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong * #seCharByteShortInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong,#seCharByteShortInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1678,7 +1704,8 @@ assignmentMultiplicationLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 * #seLong1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong0,#seLong1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1687,7 +1714,8 @@ assignmentShiftLeftInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 << #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftInt(#seCharByteShortInt0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1696,7 +1724,8 @@ assignmentShiftLeftLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 << #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftLong(#seLong0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1705,7 +1734,8 @@ assignmentShiftRightInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 >> #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1714,7 +1744,8 @@ assignmentShiftRightLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 >> #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightLong(#seLong0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1741,7 +1772,7 @@ assignmentSubtractionDouble { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 - #seDouble1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1751,7 +1782,7 @@ assignmentSubtractionDoubleStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 - #seDouble1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(subDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1761,7 +1792,7 @@ assignmentSubtractionFloat { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 - #seFloat1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1771,7 +1802,7 @@ assignmentSubtractionFloatStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 - #seFloat1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(subFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1781,7 +1812,8 @@ assignmentSubtractionInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 - #seCharByteShortInt1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaSubInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1790,7 +1822,8 @@ assignmentSubtractionLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt - #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seCharByteShortInt,#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1799,7 +1832,8 @@ assignmentSubtractionLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong - #seCharByteShortInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong,#seCharByteShortInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1808,7 +1842,8 @@ assignmentSubtractionLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 - #seLong1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong0,#seLong1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1817,7 +1852,8 @@ assignmentUnsignedShiftRightInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 >>> #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1826,7 +1862,8 @@ assignmentUnsignedShiftRightLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 >>> #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightLong(#seLong0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1955,7 +1992,7 @@ assignment_to_primitive_array_component_transaction { \varcond( \not \isReferenceArray(#v (program Variable))) \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; -\replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),update-application(elem-update(savedHeap)(if-then-else(equals(int::select(heap,#v,java.lang.Object::#$transient),Z(0(#))),store(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated,TRUE),if-then-else(equals(boolean::select(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated),FALSE),store(savedHeap,#v,arr(#se),#se0),savedHeap))),#transaction(post)))]) +\replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),update-application(elem-update(savedHeap)(if-then-else(equals(int::select(heap,#v,java.lang.Object::#$transient),Z(0(#))),store(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated,TRUE),if-then-else(equals(boolean::select(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated),FALSE),store(savedHeap,#v,arr(#se),#se0),savedHeap))),#transaction(post)))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: ((programRules:Java & runtimeExceptions:ban) & JavaCard:on)} ----------------------------------------------------- @@ -1981,7 +2018,7 @@ assignment_to_reference_array_component_transaction { \add [and(and(and(not(equals(#v,null)),lt(#se,length(#v))),geq(#se,Z(0(#)))),not(arrayStoreValid(#v,#se0)))]==>[] \replacewith([]==>[false]) ; \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; -\replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),update-application(elem-update(savedHeap)(if-then-else(equals(int::select(heap,#v,java.lang.Object::#$transient),Z(0(#))),store(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated,TRUE),if-then-else(equals(boolean::select(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated),FALSE),store(savedHeap,#v,arr(#se),#se0),savedHeap))),#transaction(post)))]) +\replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),update-application(elem-update(savedHeap)(if-then-else(equals(int::select(heap,#v,java.lang.Object::#$transient),Z(0(#))),store(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated,TRUE),if-then-else(equals(boolean::select(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated),FALSE),store(savedHeap,#v,arr(#se),#se0),savedHeap))),#transaction(post)))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: ((programRules:Java & runtimeExceptions:ban) & JavaCard:on)} ----------------------------------------------------- @@ -2468,6 +2505,7 @@ bitwiseNegationInt { \find(#normalassign ((modal operator))|{{ .. #loc = ~#seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseNegateInt(#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -2477,6 +2515,7 @@ bitwiseNegationLong { \find(#normalassign ((modal operator))|{{ .. #loc = ~#seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseNegateLong(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -3476,15 +3515,6 @@ castDel2 { Choices: true} ----------------------------------------------------- -== castLongToFloatAddition2 (float addition) ========================================= -castLongToFloatAddition2 { -\find(#normalassign ((modal operator))|{{ .. - #loc = #seFloat + #seLong; -... }}| (post)) -\replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(#seFloat,float::cast(#seLong))),#normalassign(post))) -\heuristics(executeFloatAssignment) -Choices: programRules:Java} ------------------------------------------------------ == castToBoolean (castToBoolean) ========================================= castToBoolean { \find(#allmodal ((modal operator))|{{ .. @@ -4463,7 +4493,7 @@ compound_double_cast_expression { \find(#normalassign ((modal operator))|{{ .. #loc = (double) #nse; ... }}| (post)) -\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), double)) \replacewith(#normalassign ((modal operator))|{{ .. #typeof(#nse) #v = #nse; #loc = (double) #v; @@ -4503,7 +4533,7 @@ compound_float_cast_expression { \find(#normalassign ((modal operator))|{{ .. #loc = (float) #nse; ... }}| (post)) -\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), float)) \replacewith(#normalassign ((modal operator))|{{ .. #typeof(#nse) #v = #nse; #loc = (float) #v; @@ -5163,14 +5193,14 @@ Choices: true} createdInHeapToElementOf { \find(createdInHeap(s,h)) \varcond(\notFreeIn(fv (variable), h (Heap term)), \notFreeIn(fv (variable), s (LocSet term)), \notFreeIn(ov (variable), h (Heap term)), \notFreeIn(ov (variable), s (LocSet term))) -\replacewith(all{ov (variable)}(all{fv (variable)}(imp(elementOf(ov,fv,s),or(equals(ov,null),equals(boolean::select(h,ov,java.lang.Object::#$created),TRUE)))))) +\replacewith(all{ov (variable)}(all{fv (variable)}(imp(elementOf(ov,fv,s),or(equals(ov,null),equals(boolean::select(h,ov,java.lang.Object::#$created),TRUE)))))) \heuristics(classAxiom) Choices: programRules:Java} ----------------------------------------------------- == createdInHeapWithAllFields (createdInHeapWithAllFields) ========================================= createdInHeapWithAllFields { \find(createdInHeap(allFields(o),h)) -\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) +\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -5178,14 +5208,14 @@ Choices: programRules:Java} createdInHeapWithAllFieldsEQ { \assumes ([equals(allFields(o),EQ)]==>[]) \find(createdInHeap(EQ,h)) -\sameUpdateLevel\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) +\sameUpdateLevel\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- == createdInHeapWithArrayRange (createdInHeapWithArrayRange) ========================================= createdInHeapWithArrayRange { \find(createdInHeap(arrayRange(o,lower,upper),h)) -\replacewith(or(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),lt(upper,lower))) +\replacewith(or(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),lt(upper,lower))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -5193,7 +5223,7 @@ Choices: programRules:Java} createdInHeapWithArrayRangeEQ { \assumes ([equals(arrayRange(o,lower,upper),EQ)]==>[]) \find(createdInHeap(EQ,h)) -\sameUpdateLevel\replacewith(or(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),lt(upper,lower))) +\sameUpdateLevel\replacewith(or(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),lt(upper,lower))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -5254,7 +5284,7 @@ Choices: programRules:Java} == createdInHeapWithSingleton (createdInHeapWithSingleton) ========================================= createdInHeapWithSingleton { \find(createdInHeap(singleton(o,f),h)) -\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) +\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -5262,7 +5292,7 @@ Choices: programRules:Java} createdInHeapWithSingletonEQ { \assumes ([equals(singleton(o,f),EQ)]==>[]) \find(createdInHeap(EQ,h)) -\sameUpdateLevel\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) +\sameUpdateLevel\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -5335,7 +5365,7 @@ Choices: true} defInDomainImpliesCreated { \find(inDomainImpliesCreated(m)) \varcond(\notFreeIn(o (variable), m (Map term))) -\replacewith(all{o (variable)}(imp(inDomain(m,o),equals(boolean::select(heap,o,java.lang.Object::#$created),TRUE)))) +\replacewith(all{o (variable)}(imp(inDomain(m,o),equals(boolean::select(heap,o,java.lang.Object::#$created),TRUE)))) \heuristics(simplify_enlarging) Choices: true} ----------------------------------------------------- @@ -5495,7 +5525,7 @@ Choices: true} definitionOfNewOnHeap { \find(==>newOnHeap(h,s)) \varcond(\notFreeIn(i (variable), h (Heap term)), \notFreeIn(i (variable), s (Seq term))) -\replacewith([]==>[all{i (variable)}(imp(and(leq(Z(0(#)),i),lt(i,seqLen(s))),and(imp(equals(java.lang.Object::instance(any::seqGet(s,i)),TRUE),equals(boolean::select(h,java.lang.Object::seqGet(s,i),java.lang.Object::#$created),FALSE)),imp(equals(Seq::instance(any::seqGet(s,i)),TRUE),newOnHeap(h,Seq::seqGet(s,i))))))]) +\replacewith([]==>[all{i (variable)}(imp(and(leq(Z(0(#)),i),lt(i,seqLen(s))),and(imp(equals(java.lang.Object::instance(any::seqGet(s,i)),TRUE),equals(boolean::select(h,java.lang.Object::seqGet(s,i),java.lang.Object::#$created),FALSE)),imp(equals(Seq::instance(any::seqGet(s,i)),TRUE),newOnHeap(h,Seq::seqGet(s,i))))))]) \heuristics(comprehensions) Choices: true} ----------------------------------------------------- @@ -6248,7 +6278,7 @@ Choices: programRules:Java} dynamic_type_for_null { \find(G::exactInstance(null)) \varcond(\not\same(G, Null)) -\replacewith(FALSE) +\replacewith(FALSE) \heuristics(concrete) Choices: programRules:Java} ----------------------------------------------------- @@ -6307,7 +6337,7 @@ Choices: programRules:Java} == elementOfFreshLocs (elementOfFreshLocs) ========================================= elementOfFreshLocs { \find(elementOf(o,f,freshLocs(h))) -\replacewith(and(not(equals(o,null)),not(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)))) +\replacewith(and(not(equals(o,null)),not(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)))) \heuristics(concrete) Choices: programRules:Java} ----------------------------------------------------- @@ -9602,7 +9632,7 @@ getJavaCardTransient { #jcsystemType.#getTransient(#se)@#jcsystemType; ... }}| (post)) \replacewith([]==>[not(equals(#se,null))]) ; -\replacewith([]==>[update-application(elem-update(#lhs (program LeftHandSide))(int::select(heap,#se,java.lang.Object::#$transient)),#allmodal(post))]) +\replacewith([]==>[update-application(elem-update(#lhs (program LeftHandSide))(int::select(heap,#se,java.lang.Object::#$transient)),#allmodal(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)} ----------------------------------------------------- @@ -9949,6 +9979,7 @@ identityCastDouble { \find(#normalassign ((modal operator))|{{ .. #loc = (double) #seDouble; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) \replacewith(#normalassign ((modal operator))|{{ .. #loc = #seDouble; ... }}| (post)) @@ -9960,6 +9991,7 @@ identityCastFloat { \find(#normalassign ((modal operator))|{{ .. #loc = (float) #seFloat; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) \replacewith(#normalassign ((modal operator))|{{ .. #loc = #seFloat; ... }}| (post)) @@ -11307,7 +11339,7 @@ Choices: programRules:Java} insert_constant_string_value { \assumes ([wellFormed(heap)]==>[]) \find(#csv) -\sameUpdateLevel\add [or(equals(#constantvalue(#csv),null),and(not(equals(strPool(Seq::cast(#constantvalue(#csv))),null)),equals(boolean::select(heap,strPool(Seq::cast(#constantvalue(#csv))),java.lang.Object::#$created),TRUE)))]==>[] \replacewith(if-then-else(equals(#constantvalue(#csv),null),null,strPool(Seq::cast(#constantvalue(#csv))))) +\sameUpdateLevel\add [or(equals(#constantvalue(#csv),null),and(not(equals(strPool(Seq::cast(#constantvalue(#csv))),null)),equals(boolean::select(heap,strPool(Seq::cast(#constantvalue(#csv))),java.lang.Object::#$created),TRUE)))]==>[] \replacewith(if-then-else(equals(#constantvalue(#csv),null),null,strPool(Seq::cast(#constantvalue(#csv))))) \heuristics(concrete) Choices: true} ----------------------------------------------------- @@ -11545,24 +11577,6 @@ intDivRem { Choices: true} ----------------------------------------------------- -== intLongToFloatAddition1 (float addition) ========================================= -intLongToFloatAddition1 { -\find(#normalassign ((modal operator))|{{ .. - #loc = #seLong + #seFloat; -... }}| (post)) -\replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(float::cast(#seLong),#seFloat)),#normalassign(post))) -\heuristics(executeFloatAssignment) -Choices: programRules:Java} ------------------------------------------------------ -== intToFloatAddition (float addition) ========================================= -intToFloatAddition { -\find(#normalassign ((modal operator))|{{ .. - #loc = #seCharByteShortInt + #seFloat; -... }}| (post)) -\replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(float::cast(#seCharByteShortInt),#seFloat)),#normalassign(post))) -\heuristics(executeFloatAssignment) -Choices: programRules:Java} ------------------------------------------------------ == int_diff_minus_eq (int_diff_minus_eq) ========================================= int_diff_minus_eq { \find(sub(i0,neg(i1))) @@ -11581,7 +11595,7 @@ Choices: true} == intersectAllFieldsFreshLocs (intersectAllFieldsFreshLocs) ========================================= intersectAllFieldsFreshLocs { \find(equals(intersect(allFields(o),freshLocs(h)),empty)) -\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) +\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify) Choices: programRules:Java} ----------------------------------------------------- @@ -13591,7 +13605,8 @@ narrowingByteCastInt { \find(#normalassign ((modal operator))|{{ .. #loc = (byte) #seInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13600,7 +13615,8 @@ narrowingByteCastLong { \find(#normalassign ((modal operator))|{{ .. #loc = (byte) #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13609,15 +13625,27 @@ narrowingByteCastShort { \find(#normalassign ((modal operator))|{{ .. #loc = (byte) #seShort; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seShort)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seShort)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- +== narrowingCastDoubleToFloat (cast) ========================================= +narrowingCastDoubleToFloat { +\find(#normalassign ((modal operator))|{{ .. + #loc = (float) #seDouble; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) +\replacewith(update-application(elem-update(#loc (program Variable))(float::cast(#seDouble)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == narrowingCastFloatToInt (cast) ========================================= narrowingCastFloatToInt { \find(#normalassign ((modal operator))|{{ .. #loc = (int) #seFloat; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(int::cast(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -13627,6 +13655,7 @@ narrowingCastFloatToLong { \find(#normalassign ((modal operator))|{{ .. #loc = (long) #seFloat; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(int::cast(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -13645,7 +13674,8 @@ narrowingCharCastByte { \find(#normalassign ((modal operator))|{{ .. #loc = (char) #seByte; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seByte)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seByte)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13654,7 +13684,8 @@ narrowingCharCastInt { \find(#normalassign ((modal operator))|{{ .. #loc = (char) #seInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13663,7 +13694,8 @@ narrowingCharCastLong { \find(#normalassign ((modal operator))|{{ .. #loc = (char) #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13672,7 +13704,8 @@ narrowingCharCastShort { \find(#normalassign ((modal operator))|{{ .. #loc = (char) #seShort; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seShort)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seShort)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13690,7 +13723,8 @@ narrowingIntCastLong { \find(#normalassign ((modal operator))|{{ .. #loc = (int) #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastInt(#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastInt(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13717,7 +13751,8 @@ narrowingShortCastInt { \find(#normalassign ((modal operator))|{{ .. #loc = (short) #seInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13726,7 +13761,8 @@ narrowingShortCastLong { \find(#normalassign ((modal operator))|{{ .. #loc = (short) #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13909,7 +13945,7 @@ Choices: true} ----------------------------------------------------- == nullCreated (nullCreated) ========================================= nullCreated { -\add [or(all{h (variable)}(equals(boolean::select(h,null,java.lang.Object::#$created),TRUE)),all{h (variable)}(equals(boolean::select(h,null,java.lang.Object::#$created),FALSE)))]==>[] +\add [or(all{h (variable)}(equals(boolean::select(h,null,java.lang.Object::#$created),TRUE)),all{h (variable)}(equals(boolean::select(h,null,java.lang.Object::#$created),FALSE)))]==>[] Choices: programRules:Java} ----------------------------------------------------- @@ -13976,7 +14012,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreInLocSets { \assumes ([wellFormed(h)]==>[]) \find(elementOf(o2,f2,LocSet::select(h,o,f))==>) -\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -13984,7 +14020,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreInLocSetsEQ { \assumes ([wellFormed(h),equals(LocSet::select(h,o,f),EQ)]==>[]) \find(elementOf(o2,f2,EQ)==>) -\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -13992,7 +14028,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreInLocSetsEQFinal { \assumes ([wellFormed(h),equals(LocSet::final(o,f),EQ)]==>[]) \find(elementOf(o2,f2,EQ)==>) -\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14000,7 +14036,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreInLocSetsFinal { \assumes ([wellFormed(h)]==>[]) \find(elementOf(o2,f2,LocSet::final(o,f))==>) -\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14008,7 +14044,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreObserved { \find(obs) \sameUpdateLevel\varcond(\isObserver (obs (deltaObject term), h (Heap term))) -\add [or(equals(obs,null),equals(boolean::select(h,obs,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(obs,null),equals(boolean::select(h,obs,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14016,7 +14052,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreObservedInLocSets { \find(elementOf(o,f,obs)==>) \varcond(\isObserver (obs (LocSet term), h (Heap term))) -\add [or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14025,7 +14061,7 @@ onlyCreatedObjectsAreObservedInLocSetsEQ { \assumes ([equals(obs,EQ)]==>[]) \find(elementOf(o,f,EQ)==>) \varcond(\isObserver (obs (LocSet term), h (Heap term))) -\add [or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14033,15 +14069,15 @@ Choices: programRules:Java} onlyCreatedObjectsAreReferenced { \assumes ([wellFormed(h)]==>[]) \find(deltaObject::select(h,o,f)) -\sameUpdateLevel\add [or(equals(deltaObject::select(h,o,f),null),equals(boolean::select(h,deltaObject::select(h,o,f),java.lang.Object::#$created),TRUE))]==>[] +\sameUpdateLevel\add [or(equals(deltaObject::select(h,o,f),null),equals(boolean::select(h,deltaObject::select(h,o,f),java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- == onlyCreatedObjectsAreReferencedFinal (onlyCreatedObjectsAreReferencedFinal) ========================================= onlyCreatedObjectsAreReferencedFinal { -\assumes ([wellFormed(h),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)]==>[]) +\assumes ([wellFormed(h),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)]==>[]) \find(deltaObject::final(o,f)) -\sameUpdateLevel\add [or(equals(deltaObject::final(o,f),null),equals(boolean::select(h,deltaObject::final(o,f),java.lang.Object::#$created),TRUE))]==>[] +\sameUpdateLevel\add [or(equals(deltaObject::final(o,f),null),equals(boolean::select(h,deltaObject::final(o,f),java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14049,7 +14085,7 @@ Choices: programRules:Java} only_created_objects_are_reachable { \assumes ([wellFormed(h)]==>[equals(o,null)]) \find(reach(h,s,o,o2,n)==>) -\add [or(not(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] +\add [or(not(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: reach:on} ----------------------------------------------------- @@ -15186,7 +15222,7 @@ Choices: (programRules:Java & runtimeExceptions:ban)} referencedObjectIsCreatedRighFinalEQ { \assumes ([equals(deltaObject::final(o,f),EQ)]==>[equals(EQ,null)]) \find(==>equals(boolean::select(h,EQ,java.lang.Object::#$created),TRUE)) -\add []==>[or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(o,null))] +\add []==>[or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(o,null))] \heuristics(concrete) Choices: programRules:Java} ----------------------------------------------------- @@ -15210,7 +15246,7 @@ Choices: programRules:Java} referencedObjectIsCreatedRightFinal { \assumes ([]==>[equals(deltaObject::final(o,f),null)]) \find(==>equals(boolean::select(h,deltaObject::final(o,f),java.lang.Object::#$created),TRUE)) -\replacewith([]==>[or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(o,null))]) +\replacewith([]==>[or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(o,null))]) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -15698,14 +15734,14 @@ Choices: true} == selectCreatedOfAnon (selectCreatedOfAnon) ========================================= selectCreatedOfAnon { \find(boolean::select(anon(h,s,h2),o,java.lang.Object::#$created)) -\replacewith(if-then-else(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),TRUE,boolean::select(h2,o,java.lang.Object::#$created))) +\replacewith(if-then-else(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),TRUE,boolean::select(h2,o,java.lang.Object::#$created))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- == selectCreatedOfAnonAsFormula (selectCreatedOfAnonAsFormula) ========================================= selectCreatedOfAnonAsFormula { \find(equals(boolean::select(anon(h,s,h2),o,java.lang.Object::#$created),TRUE)) -\replacewith(or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(boolean::select(h2,o,java.lang.Object::#$created),TRUE))) +\replacewith(or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(boolean::select(h2,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_ENLARGING) Choices: programRules:Java} ----------------------------------------------------- @@ -15713,7 +15749,7 @@ Choices: programRules:Java} selectCreatedOfAnonAsFormulaEQ { \assumes ([equals(anon(h,s,h2),EQ)]==>[]) \find(equals(boolean::select(EQ,o,java.lang.Object::#$created),TRUE)) -\sameUpdateLevel\replacewith(or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(boolean::select(h2,o,java.lang.Object::#$created),TRUE))) +\sameUpdateLevel\replacewith(or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(boolean::select(h2,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_ENLARGING) Choices: programRules:Java} ----------------------------------------------------- @@ -15721,14 +15757,14 @@ Choices: programRules:Java} selectCreatedOfAnonEQ { \assumes ([equals(anon(h,s,h2),EQ)]==>[]) \find(boolean::select(EQ,o,java.lang.Object::#$created)) -\sameUpdateLevel\replacewith(if-then-else(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),TRUE,boolean::select(h2,o,java.lang.Object::#$created))) +\sameUpdateLevel\replacewith(if-then-else(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),TRUE,boolean::select(h2,o,java.lang.Object::#$created))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- == selectOfAnon (selectOfAnon) ========================================= selectOfAnon { \find(beta::select(anon(h,s,h2),o,f)) -\replacewith(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f))) +\replacewith(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f))) \heuristics(semantics_blasting) Choices: programRules:Java} ----------------------------------------------------- @@ -15736,14 +15772,14 @@ Choices: programRules:Java} selectOfAnonEQ { \assumes ([equals(anon(h,s,h2),EQ)]==>[]) \find(beta::select(EQ,o,f)) -\sameUpdateLevel\replacewith(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f))) +\sameUpdateLevel\replacewith(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- == selectOfCreate (selectOfCreate) ========================================= selectOfCreate { \find(beta::select(create(h,o),o2,f)) -\replacewith(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f))) +\replacewith(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f))) \heuristics(semantics_blasting) Choices: programRules:Java} ----------------------------------------------------- @@ -15751,14 +15787,14 @@ Choices: programRules:Java} selectOfCreateEQ { \assumes ([equals(create(h,o),EQ)]==>[]) \find(beta::select(EQ,o2,f)) -\sameUpdateLevel\replacewith(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f))) +\sameUpdateLevel\replacewith(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- == selectOfMemset (selectOfMemset) ========================================= selectOfMemset { \find(beta::select(memset(h,s,x),o,f)) -\replacewith(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o,f))) +\replacewith(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o,f))) \heuristics(semantics_blasting) Choices: programRules:Java} ----------------------------------------------------- @@ -15766,14 +15802,14 @@ Choices: programRules:Java} selectOfMemsetEQ { \assumes ([equals(memset(h,s,x),EQ)]==>[]) \find(beta::select(EQ,o,f)) -\sameUpdateLevel\replacewith(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o,f))) +\sameUpdateLevel\replacewith(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o,f))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- == selectOfStore (selectOfStore) ========================================= selectOfStore { \find(beta::select(store(h,o,f,x),o2,f2)) -\replacewith(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2))) +\replacewith(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2))) \heuristics(semantics_blasting) Choices: programRules:Java} ----------------------------------------------------- @@ -15781,7 +15817,7 @@ Choices: programRules:Java} selectOfStoreEQ { \assumes ([equals(store(h,o,f,x),EQ)]==>[]) \find(beta::select(EQ,o2,f2)) -\sameUpdateLevel\replacewith(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2))) +\sameUpdateLevel\replacewith(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- @@ -16135,7 +16171,7 @@ setJavaCardTransient { #jcsystemType.#setTransient(#se, #se1)@#jcsystemType; ... }}| (post)) \replacewith([]==>[not(equals(#se,null))]) ; -\replacewith([]==>[update-application(elem-update(heap)(store(heap,#se,java.lang.Object::#$transient,#se1)),#allmodal(post))]) +\replacewith([]==>[update-application(elem-update(heap)(store(heap,#se,java.lang.Object::#$transient,#se1)),#allmodal(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)} ----------------------------------------------------- @@ -16345,7 +16381,7 @@ simplifySelectOfAnon { \find(beta::select(anon(h,s,h2),o,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16357,7 +16393,7 @@ simplifySelectOfAnonEQ { \find(beta::select(EQ,o,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16368,7 +16404,7 @@ simplifySelectOfCreate { \find(beta::select(create(h,o),o2,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16380,7 +16416,7 @@ simplifySelectOfCreateEQ { \find(beta::select(EQ,o2,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16391,7 +16427,7 @@ simplifySelectOfMemset { \find(beta::select(memset(h,s,x),o,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),x,beta::select(h,o,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),x,beta::select(h,o,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16403,7 +16439,7 @@ simplifySelectOfMemsetEQ { \find(beta::select(EQ,o,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),x,beta::select(h,o,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),x,beta::select(h,o,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16414,7 +16450,7 @@ simplifySelectOfStore { \find(beta::select(store(h,o,f,x),o2,f2)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16426,7 +16462,7 @@ simplifySelectOfStoreEQ { \find(beta::select(EQ,o2,f2)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16759,7 +16795,7 @@ stringAssignment { \find(#normalassign ((modal operator))|{{ .. #v = #slit; ... }}| (post)) -\sameUpdateLevel\add [not(equals(strPool(#slit),null)),equals(boolean::select(heap,strPool(#slit),java.lang.Object::#$created),TRUE)]==>[] \replacewith(update-application(elem-update(#v (program Variable))(strPool(#slit)),#normalassign(post))) +\sameUpdateLevel\add [not(equals(strPool(#slit),null)),equals(boolean::select(heap,strPool(#slit),java.lang.Object::#$created),TRUE)]==>[] \replacewith(update-application(elem-update(#v (program Variable))(strPool(#slit)),#normalassign(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: true} ----------------------------------------------------- @@ -18313,25 +18349,52 @@ unaryMinusDouble { \find(#normalassign ((modal operator))|{{ .. #loc = -#seDouble; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusDouble(#seDouble)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} ----------------------------------------------------- +== unaryMinusDouble_cast (cast) ========================================= +unaryMinusDouble_cast { +\find(#normalassign ((modal operator))|{{ .. + #loc = -#se; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), \not\sub(\typeof(#se (program SimpleExpression)), double)) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = (double) (-#se); +... }}| (post)) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == unaryMinusFloat (unaryMinus) ========================================= unaryMinusFloat { \find(#normalassign ((modal operator))|{{ .. #loc = -#seFloat; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusFloat(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} ----------------------------------------------------- +== unaryMinusFloat_cast (cast) ========================================= +unaryMinusFloat_cast { +\find(#normalassign ((modal operator))|{{ .. + #loc = -#se; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), \not\sub(\typeof(#se (program SimpleExpression)), float)) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = (float) (-#se); +... }}| (post)) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == unaryMinusInt (unaryMinus) ========================================= unaryMinusInt { \find(#normalassign ((modal operator))|{{ .. #loc = -#seCharByteShortInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusInt(#seCharByteShortInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusInt(#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -18340,10 +18403,85 @@ unaryMinusLong { \find(#normalassign ((modal operator))|{{ .. #loc = -#seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusLong(#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusLong(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- +== unbalanced_float_expression (cast) ========================================= +unbalanced_float_expression { +\find(#normalassign ((modal operator))|{{ .. + #loc = #unbalancedFloat; +... }}| (post)) +\varcond(\floatingPointBalanced(#unbalancedFloat (program FloatingPointBinaryExpression), #balancedFloat (program FloatingPointBinaryExpression))) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = #balancedFloat; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_nonsimple_nonfloat_to_double_assignment (cast) ========================================= +unbalanced_nonsimple_nonfloat_to_double_assignment { +\find(#normalassign ((modal operator))|{{ .. + #loc = #nse; +... }}| (post)) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), double), \not\sub(\typeof(#nse (program NonSimpleExpression)), double)) +\replacewith(#normalassign ((modal operator))|{{ .. + #typeof(#nse) #v = #nse; + #loc = (double) #v; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_nonsimple_nonfloat_to_float_assignment (cast) ========================================= +unbalanced_nonsimple_nonfloat_to_float_assignment { +\find(#normalassign ((modal operator))|{{ .. + #loc = #nse; +... }}| (post)) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), float), \not\sub(\typeof(#nse (program NonSimpleExpression)), float)) +\replacewith(#normalassign ((modal operator))|{{ .. + #typeof(#nse) #v = #nse; + #loc = (float) #v; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_simple_double_assignment (cast) ========================================= +unbalanced_simple_double_assignment { +\find(#normalassign ((modal operator))|{{ .. + #loc = #se; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), \sub(\typeof(#se (program SimpleExpression)), int)) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = (double) #se; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_simple_float_assignment (cast) ========================================= +unbalanced_simple_float_assignment { +\find(#normalassign ((modal operator))|{{ .. + #loc = #se; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), \sub(\typeof(#se (program SimpleExpression)), int)) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = (float) #se; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_simple_float_to_double_assignment (cast) ========================================= +unbalanced_simple_float_to_double_assignment { +\find(#normalassign ((modal operator))|{{ .. + #loc = #seFloat; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = (double) #seFloat; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- == unionEqualsEmpty (unionEqualsEmpty) ========================================= unionEqualsEmpty { \find(equals(union(s,s2),empty)) @@ -18599,7 +18737,7 @@ Choices: programRules:Java} wellFormedMemsetArrayObject { \find(wellFormed(memset(h,arrayRange(ar,lo,up),x))) \succedentPolarity\varcond(\hasSort(\elemSort(ar (java.lang.Object term)), alpha)) -\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),arrayStoreValid(ar,x))))) +\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),arrayStoreValid(ar,x))))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -18615,7 +18753,7 @@ Choices: programRules:Java} wellFormedStoreArray { \find(wellFormed(store(h,o,arr(idx),x))) \succedentPolarity\varcond(\hasSort(\elemSort(o (java.lang.Object term)), alpha)) -\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),arrayStoreValid(o,x))))) +\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),arrayStoreValid(o,x))))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -18639,7 +18777,7 @@ Choices: programRules:Java} wellFormedStoreObject { \find(wellFormed(store(h,o,f,x))) \succedentPolarity\varcond(\fieldType(f (Field term), alpha)) -\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),equals(alpha::instance(x),TRUE))))) +\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),equals(alpha::instance(x),TRUE))))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -18648,7 +18786,7 @@ wellFormedStoreObjectEQ { \assumes ([equals(store(h,o,f,x),EQ)]==>[]) \find(wellFormed(EQ)) \sameUpdateLevel\succedentPolarity\varcond(\fieldType(f (Field term), alpha)) -\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),equals(alpha::instance(x),TRUE))))) +\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),equals(alpha::instance(x),TRUE))))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -18677,20 +18815,52 @@ wellFormedStorePrimitiveEQ { \heuristics(concrete) Choices: programRules:Java} ----------------------------------------------------- +== wideningCastFloatToDouble (cast) ========================================= +wideningCastFloatToDouble { +\find(#normalassign ((modal operator))|{{ .. + #loc = (double) #seFloat; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) +\replacewith(update-application(elem-update(#loc (program Variable))(double::cast(#seFloat)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- +== wideningCastIntToDouble (cast) ========================================= +wideningCastIntToDouble { +\find(#normalassign ((modal operator))|{{ .. + #loc = (double) #seCharByteShortInt; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) +\replacewith(update-application(elem-update(#loc (program Variable))(double::cast(#seCharByteShortInt)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == wideningCastIntToFloat (cast) ========================================= wideningCastIntToFloat { \find(#normalassign ((modal operator))|{{ .. #loc = (float) #seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(float::cast(#seCharByteShortInt)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} ----------------------------------------------------- +== wideningCastLongToDouble (cast) ========================================= +wideningCastLongToDouble { +\find(#normalassign ((modal operator))|{{ .. + #loc = (double) #seLong; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) +\replacewith(update-application(elem-update(#loc (program Variable))(double::cast(#seLong)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == wideningCastLongToFloat (cast) ========================================= wideningCastLongToFloat { \find(#normalassign ((modal operator))|{{ .. #loc = (float) #seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(float::cast(#seLong)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}