From 5fcf6463880e872899e98c8bc4bfdc5a6a1e2cb5 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 5 Feb 2023 16:00:02 +0100 Subject: [PATCH 1/8] 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 2/8] 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 3/8] 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 4/8] 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 5/8] 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 6/8] 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 7/8] 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 8/8] 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;