diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 60113499f8f..db38158abdc 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -116,6 +116,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 5832a7238f7..03561b9801a 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -688,6 +688,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 4e644442ee7..3e7fe409c26 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 @@ -211,6 +211,9 @@ public abstract class ProgramSVSort extends SortImpl { 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(); @@ -1081,6 +1084,43 @@ 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 and both arguments are simple expressions. + * 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 || 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; + } + 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 67065ce497c..1777edb94d6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java @@ -277,6 +277,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); @@ -382,7 +385,8 @@ public IsLabeledCondition build(Object[] arguments, List parameters, applyUpdateOnRigid, DROP_EFFECTLESS_ELEMENTARIES, SIMPLIFY_ITE_UPDATE, SUBFORMULAS, STATIC_FIELD, MODEL_FIELD, SUBFORMULA, DROP_EFFECTLESS_STORES, EQUAL_UNIQUE, META_DISJOINT, - IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP); + 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..d326269232e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java @@ -0,0 +1,158 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.rule.conditions; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.JavaProgramElement; +import de.uka.ilkd.key.java.ast.ProgramElement; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.Operator; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.ast.expression.operator.ComparativeOperator; +import de.uka.ilkd.key.java.ast.expression.operator.TypeCast; +import de.uka.ilkd.key.java.ast.reference.TypeRef; +import de.uka.ilkd.key.java.visitor.ProgramElementReplacer; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.logic.sort.Sort; +import org.key_project.prover.rules.VariableCondition; +import org.key_project.prover.rules.instantiation.MatchResultInfo; + +import org.jspecify.annotations.Nullable; + + +/** + * This variable condition adds required numeric promotions to Java operations + * 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 MatchResultInfo check(SchemaVariable var, SyntaxElement instCandidate, + MatchResultInfo mc, + LogicServices services) { + + var svInst = (SVInstantiations) mc.getInstantiations(); + Object untypedInstantiation = svInst.getInstantiation(unbalanced); + if (!(untypedInstantiation instanceof BinaryOperator + || untypedInstantiation instanceof ComparativeOperator)) { + return null; + } + Operator inInst = (Operator) untypedInstantiation; + JavaProgramElement outInst = svInst.getInstantiation(balanced); + if (inInst == null) { + return mc; + } + + Operator properResultInst = balance(inInst, (Services) 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 Operator balance(Operator 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 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 (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 c538397d384..1255129f598 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.ProgramElement; import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.*; @@ -155,14 +156,17 @@ public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, JTerm gsTerm = null; if (inst instanceof JTerm) { gsTerm = (JTerm) 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/float/floatAssignment2UpdateRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/float/floatAssignment2UpdateRules.key index e3d22435553..3593fddeda8 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/float/floatAssignment2UpdateRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/float/floatAssignment2UpdateRules.key @@ -17,6 +17,7 @@ \program Variable #v; \program NonSimpleExpression #nse; + \program SimpleExpression #se; \formula post; @@ -133,29 +134,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)) @@ -167,7 +190,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)) @@ -179,7 +202,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)) @@ -191,7 +214,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)) @@ -204,7 +227,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)) @@ -216,7 +239,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)) @@ -228,7 +251,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)) @@ -240,7 +263,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)) @@ -254,7 +277,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)) @@ -266,7 +289,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)) @@ -278,7 +301,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)) @@ -290,7 +313,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)) @@ -302,7 +325,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)) @@ -314,7 +337,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)) @@ -326,7 +349,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)) @@ -338,7 +361,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)) @@ -351,6 +374,7 @@ \find(\modality{#normalassign}{.. #loc = #seFloat0 % #seFloat1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float)) \replacewith( {#loc := javaModFloat(#seFloat0, #seFloat1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -362,6 +386,7 @@ \find(\modality{#normalassign}{.. #loc = #seDouble0 % #seDouble1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), double)) \replacewith( {#loc := javaModDouble(#seDouble0, #seDouble1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -369,59 +394,60 @@ \displayname "mod" }; - // Operations on combined float/int + // Typecasts + - intLongToFloatAddition1 { + // KeY integers are not bounded in size, but ints fit inside long + wideningCastLongToFloat { \find(\modality{#normalassign}{.. - #loc = #seLong + #seFloat; + #loc = (float) #seLong; ...}\endmodality (post)) - \replacewith({#loc := javaAddFloat((float)#seLong, #seFloat)} - \modality{#normalassign}{.. ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float)) + \replacewith({#loc := (float)#seLong} + \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) - \displayname "float addition" + \displayname "cast" }; - // For int/short/char/byte, converting to float is the same as - // converting to long first, then float - intToFloatAddition { + wideningCastFloatToDouble { \find(\modality{#normalassign}{.. - #loc = #seCharByteShortInt + #seFloat; + #loc = (double) #seFloat; ...}\endmodality (post)) - \replacewith({#loc := javaAddFloat((float)#seCharByteShortInt, #seFloat)} - \modality{#normalassign}{.. ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), double)) + \replacewith({#loc := (double)#seFloat} + \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) - \displayname "float addition" + \displayname "cast" }; - castLongToFloatAddition2 { + wideningCastIntToFloat { \find(\modality{#normalassign}{.. - #loc = #seFloat + #seLong; + #loc = (float) #seCharByteShortInt; ...}\endmodality (post)) - \replacewith({#loc := javaAddFloat(#seFloat, (float)#seLong)} - \modality{#normalassign}{.. ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float)) + \replacewith({#loc := (float)(#seCharByteShortInt)} + \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) - \displayname "float addition" + \displayname "cast" }; - // Typecasts - - - // KeY integers are not bounded in size, but ints fit inside long - wideningCastLongToFloat { + wideningCastIntToDouble { \find(\modality{#normalassign}{.. - #loc = (float) #seLong; + #loc = (double) #seCharByteShortInt; ...}\endmodality (post)) - \replacewith({#loc := (float)#seLong} + \varcond(\sub(\typeof(#loc), double)) + \replacewith({#loc := (double)(#seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) \displayname "cast" }; - wideningCastIntToFloat { + wideningCastLongToDouble { \find(\modality{#normalassign}{.. - #loc = (float) #seCharByteShortInt; + #loc = (double) #seLong; ...}\endmodality (post)) - \replacewith({#loc := (float)(#seCharByteShortInt)} + \varcond(\sub(\typeof(#loc), double)) + \replacewith({#loc := (double)#seLong} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) \displayname "cast" @@ -431,6 +457,7 @@ \find(\modality{#normalassign}{.. #loc = (float) #seFloat; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float)) \replacewith(\modality{#normalassign}{.. #loc = #seFloat; ...}\endmodality (post)) @@ -442,6 +469,7 @@ \find(\modality{#normalassign}{.. #loc = (double) #seDouble; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), double)) \replacewith(\modality{#normalassign}{.. #loc = #seDouble; ...}\endmodality (post)) @@ -453,16 +481,29 @@ \find(\modality{#normalassign}{.. #loc = (int) #seFloat; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), int)) \replacewith({#loc := (long)(#seFloat)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) \displayname "cast" }; + narrowingCastDoubleToFloat { + \find(\modality{#normalassign}{.. + #loc = (float) #seDouble; + ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), float)) + \replacewith({#loc := (float)(#seDouble)} + \modality{#normalassign}{.. ...}\endmodality (post)) + \heuristics(executeFloatAssignment) + \displayname "cast" + }; + narrowingCastFloatToLong { \find(\modality{#normalassign}{.. #loc = (long) #seFloat; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc), long)) \replacewith({#loc := (long)(#seFloat)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeFloatAssignment) @@ -473,7 +514,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" @@ -481,10 +522,60 @@ 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" }; + 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" + }; + + 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_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_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_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_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" + }; } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerAssignment2UpdateRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerAssignment2UpdateRules.key index 73201f403f7..bbe65f82a8b 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerAssignment2UpdateRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerAssignment2UpdateRules.key @@ -43,6 +43,7 @@ #loc = #seCharByteShortInt0 * #seCharByteShortInt1; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1))) @@ -58,6 +59,7 @@ #loc=#seCharByteShortInt * #seLong; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(mul(#seCharByteShortInt, #seLong))) @@ -73,6 +75,7 @@ #loc=#seLong * #seCharByteShortInt; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(mul(#seLong, #seCharByteShortInt))) @@ -88,6 +91,7 @@ #loc=#seLong0 * #seLong1; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(mul(#seLong0, #seLong1))) @@ -108,6 +112,7 @@ \find( ==> \modality{#normalassign}{.. #loc=#seCharByteShortInt0 / #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( ==> {#loc := javaDivInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)); @@ -120,6 +125,7 @@ \find( ==> \modality{#normalassign}{.. #loc=#se / #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( ==> {#loc := javaDivLong(#se, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)); @@ -132,6 +138,7 @@ \find( ==> \modality{#normalassign}{.. #loc=#seLong / #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( ==> {#loc := javaDivLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)); @@ -148,6 +155,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)); @@ -165,6 +174,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 / #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaDivInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -176,6 +186,7 @@ \find(\modality{#normalassign}{.. #loc=#se / #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaDivLong(#se, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -187,6 +198,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong / #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaDivLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -202,6 +214,7 @@ \find(\modality{#normalassign}{.. #loc=#se0 % #se1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaMod(#se0, #se1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -218,6 +231,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)) @@ -232,6 +246,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)) @@ -246,6 +261,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)) @@ -264,6 +280,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)) @@ -285,6 +302,7 @@ #loc = #seCharByteShortInt0 - #seCharByteShortInt1; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1))) @@ -300,6 +318,7 @@ #loc=#seCharByteShortInt - #seLong; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(sub(#seCharByteShortInt, #seLong))) @@ -315,6 +334,7 @@ #loc=#seLong - #seCharByteShortInt; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(sub(#seLong, #seCharByteShortInt))) @@ -331,6 +351,7 @@ #loc=#seLong0 - #seLong1; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(sub(#seLong0, #seLong1))) @@ -348,6 +369,7 @@ #loc=#seCharByteShortInt0 + #seCharByteShortInt1; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(add(#seCharByteShortInt0, #seCharByteShortInt1))) @@ -364,6 +386,7 @@ #loc=#seCharByteShortInt + #seLong; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(add(#seCharByteShortInt, #seLong))) @@ -380,6 +403,7 @@ #loc=#seLong + #seCharByteShortInt; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(add(#seLong, #seCharByteShortInt))) @@ -396,6 +420,7 @@ #loc=#seLong0 + #seLong1; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(add(#seLong0, #seLong1))) @@ -413,6 +438,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 & #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseAndInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -424,6 +450,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt & #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseAndLong(#seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -435,6 +462,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong & #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseAndLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -446,6 +474,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 & #seLong1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseAndLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -459,6 +488,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 | #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseOrInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -470,6 +500,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt | #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseOrLong(#seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -482,6 +513,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong | #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseOrLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -494,6 +526,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 | #seLong1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseOrLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -507,6 +540,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 ^ #seCharByteShortInt1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseXOrInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -518,6 +552,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt ^ #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseXOrLong(#seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -529,6 +564,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong ^ #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseXOrLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -540,6 +576,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 ^ #seLong1; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith( {#loc := javaBitwiseXOrLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -554,6 +591,7 @@ #loc=#seCharByteShortInt0 >> #se; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(shiftright(#seLong0, #se))) @@ -570,6 +608,7 @@ #loc=#seLong0 >> #se; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(shiftright(#seLong0, #se))) @@ -588,6 +627,7 @@ #loc=#seCharByteShortInt0 << #se; ...} \endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(shiftleft(#seCharByteShortInt0, #se))) @@ -604,6 +644,7 @@ #loc=#seLong0 << #se; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(shiftleft(#seLong0, #se))) @@ -622,6 +663,7 @@ #loc=#seCharByteShortInt0 >>> #se; ...} \endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(unsignedshiftrightJint(#seCharByteShortInt0, #se))) @@ -638,6 +680,7 @@ #loc=#seLong0 >>> #se; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(unsignedshiftrightJlong(#seLong0, #se))) @@ -657,6 +700,7 @@ #loc = - #seCharByteShortInt; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(neg(#seCharByteShortInt))) @@ -672,6 +716,7 @@ #loc = - #seLong; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inLong(neg(#seLong))) @@ -684,6 +729,7 @@ bitwiseNegationInt { \find(\modality{#normalassign}{.. #loc = ~ #seCharByteShortInt; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith({#loc := javaBitwiseNegateInt(#seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeIntegerAssignment) @@ -692,6 +738,7 @@ bitwiseNegationLong { \find(\modality{#normalassign}{.. #loc = ~ #seLong; ...}\endmodality (post)) + \varcond(\sub(\typeof(#loc),int)) \replacewith({#loc := javaBitwiseNegateLong(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) \heuristics(executeIntegerAssignment) @@ -707,6 +754,7 @@ #loc = (byte) #seShort; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inByte(#seShort)) @@ -722,6 +770,7 @@ #loc = (byte) #seInt; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inByte(#seInt)) @@ -737,6 +786,7 @@ #loc = (byte) #seLong; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inByte(#seLong)) @@ -752,6 +802,7 @@ #loc = (short) #seInt; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inShort(#seInt)) @@ -767,6 +818,7 @@ #loc = (short) #seLong; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inShort(#seLong)) @@ -780,6 +832,7 @@ narrowingIntCastLong { \find(\modality{#normalassign}{.. #loc = (int) #seLong; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inInt(#seLong)) @@ -795,6 +848,7 @@ #loc = (char) #seByte; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inChar(#seByte)) @@ -811,6 +865,7 @@ #loc = (char) #seShort; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inChar(#seShort)) @@ -827,6 +882,7 @@ #loc = (char) #seInt; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> inChar(#seInt)) @@ -842,6 +898,7 @@ #loc = (char) #seLong; ...}\endmodality (post)) \sameUpdateLevel + \varcond(\sub(\typeof(#loc),int)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \add(==> 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 97257fcb1b2..bffdc2bf872 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 @@ -290,6 +290,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) }; diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index ffb4cb55fc2..542086b4476 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -1,5 +1,5 @@ # This files contains representation of taclets, which are accepted and revised. -# Date: Wed Nov 19 11:46:34 CET 2025 +# Date: Sat Apr 11 10:11:51 CEST 2026 == abortJavaCardTransactionAPI (abortJavaCardTransactionAPI) ========================================= abortJavaCardTransactionAPI { @@ -17,7 +17,7 @@ abortJavaCardTransactionBox { \find(==>box_transaction|{{ .. #abortJavaCardTransaction; ... }}| (post)) -\replacewith([]==>[update-application(elem-update(heap)(anon(savedHeap,allObjects(java.lang.Object::#$transactionConditionallyUpdated),heap)),box(post))]) +\replacewith([]==>[update-application(elem-update(heap)(anon(savedHeap,allObjects(java.lang.Object::#$transactionConditionallyUpdated),heap)),box(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)} ----------------------------------------------------- @@ -26,7 +26,7 @@ abortJavaCardTransactionDiamond { \find(==>diamond_transaction|{{ .. #abortJavaCardTransaction; ... }}| (post)) -\replacewith([]==>[update-application(elem-update(heap)(anon(savedHeap,allObjects(java.lang.Object::#$transactionConditionallyUpdated),heap)),diamond(post))]) +\replacewith([]==>[update-application(elem-update(heap)(anon(savedHeap,allObjects(java.lang.Object::#$transactionConditionallyUpdated),heap)),diamond(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)} ----------------------------------------------------- @@ -679,7 +679,7 @@ allocateInstance { #lhs = #t.#allocate()@#t; ... }}| (post)) \varcond(\hasSort(#t2 (program Type), alphaObj)) -\add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),equals(boolean::select(heap,#lhs,java.lang.Object::#$created),FALSE))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(create(heap,#lhs)),#allmodal(post))]) +\add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),equals(boolean::select(heap,#lhs,java.lang.Object::#$created),FALSE))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(create(heap,#lhs)),#allmodal(post))]) \heuristics(method_expand) Choices: (programRules:Java & permissions:off)} ----------------------------------------------------- @@ -689,7 +689,7 @@ allocateInstanceWithLength { #lhs = #t.#allocate(#len)@#t; ... }}| (post)) \varcond(\hasSort(#t2 (program Type), alphaObj)) -\add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),and(equals(boolean::select(heap,#lhs,java.lang.Object::#$created),FALSE),equals(length(#lhs),#len)))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(store(store(create(heap,#lhs),#lhs,java.lang.Object::#$transient,Z(0(#))),#lhs,java.lang.Object::#$transactionConditionallyUpdated,FALSE)),#allmodal(post))]) +\add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),and(equals(boolean::select(heap,#lhs,java.lang.Object::#$created),FALSE),equals(length(#lhs),#len)))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(store(store(create(heap,#lhs),#lhs,java.lang.Object::#$transient,Z(0(#))),#lhs,java.lang.Object::#$transactionConditionallyUpdated,FALSE)),#allmodal(post))]) \heuristics(method_expand) Choices: (programRules:Java & permissions:off)} ----------------------------------------------------- @@ -1235,7 +1235,7 @@ Choices: (programRules:Java & assertions:safe)} assignableDefinition { \find(assignable(heapNew,heapOld,locs)) \varcond(\notFreeIn(f (variable), heapNew (Heap term)), \notFreeIn(f (variable), heapOld (Heap term)), \notFreeIn(f (variable), locs (LocSet term)), \notFreeIn(o (variable), heapNew (Heap term)), \notFreeIn(o (variable), heapOld (Heap term)), \notFreeIn(o (variable), locs (LocSet term))) -\replacewith(all{f (variable)}(all{o (variable)}(or(or(elementOf(o,f,locs),and(not(equals(o,null)),not(equals(boolean::select(heapOld,o,java.lang.Object::#$created),TRUE)))),equals(any::select(heapNew,o,f),any::select(heapOld,o,f)))))) +\replacewith(all{f (variable)}(all{o (variable)}(or(or(elementOf(o,f,locs),and(not(equals(o,null)),not(equals(boolean::select(heapOld,o,java.lang.Object::#$created),TRUE)))),equals(any::select(heapNew,o,f),any::select(heapOld,o,f)))))) \heuristics(delayedExpansion) Choices: programRules:Java} ----------------------------------------------------- @@ -1244,6 +1244,7 @@ assignment { \find(#allmodal ((modal operator))|{{ .. #loc = #se; ... }}| (post)) +\varcond(\sub(\typeof(#se (program SimpleExpression)), \typeof(#loc (program Variable)))) \replacewith(update-application(elem-update(#loc (program Variable))(#se),#allmodal(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java} @@ -1271,7 +1272,7 @@ assignmentAdditionDouble { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 + #seDouble1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1281,7 +1282,7 @@ assignmentAdditionDoubleStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 + #seDouble1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(addDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1291,7 +1292,7 @@ assignmentAdditionFloat { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 + #seFloat1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1301,7 +1302,7 @@ assignmentAdditionFloatStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 + #seFloat1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(addFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1311,7 +1312,8 @@ assignmentAdditionInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 + #seCharByteShortInt1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaAddInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1320,7 +1322,8 @@ assignmentAdditionLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt + #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seCharByteShortInt,#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1329,7 +1332,8 @@ assignmentAdditionLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong + #seCharByteShortInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong,#seCharByteShortInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1338,7 +1342,8 @@ assignmentAdditionLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 + #seLong1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong0,#seLong1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1347,6 +1352,7 @@ assignmentBitwiseAndInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 & #seCharByteShortInt1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1356,6 +1362,7 @@ assignmentBitwiseAndLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt & #seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1365,6 +1372,7 @@ assignmentBitwiseAndLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong & #seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1374,6 +1382,7 @@ assignmentBitwiseAndLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 & #seLong1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1383,6 +1392,7 @@ assignmentBitwiseOrInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 | #seCharByteShortInt1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1392,6 +1402,7 @@ assignmentBitwiseOrLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt | #seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1401,6 +1412,7 @@ assignmentBitwiseOrLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong | #seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1410,6 +1422,7 @@ assignmentBitwiseOrLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 | #seLong1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1419,6 +1432,7 @@ assignmentBitwiseXOrInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 ^ #seCharByteShortInt1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1428,6 +1442,7 @@ assignmentBitwiseXOrLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt ^ #seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1437,6 +1452,7 @@ assignmentBitwiseXOrLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong ^ #seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1446,6 +1462,7 @@ assignmentBitwiseXOrLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 ^ #seLong1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -1475,7 +1492,7 @@ assignmentDivisionDouble { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 / #seDouble1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaDivDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1485,7 +1502,7 @@ assignmentDivisionDoubleStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 / #seDouble1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(divDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1495,7 +1512,7 @@ assignmentDivisionFloat { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 / #seFloat1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaDivFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1505,7 +1522,7 @@ assignmentDivisionFloatStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 / #seFloat1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(divFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1515,6 +1532,7 @@ assignmentDivisionInt { \find(==>#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 / #seCharByteShortInt1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith([]==>[not(equals(#seCharByteShortInt1,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1525,6 +1543,7 @@ assignmentDivisionLong { \find(==>#normalassign ((modal operator))|{{ .. #loc = #se / #seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith([]==>[not(equals(#seLong,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivLong(#se,#seLong)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1535,6 +1554,7 @@ assignmentDivisionLong2 { \find(==>#normalassign ((modal operator))|{{ .. #loc = #seLong / #seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith([]==>[not(equals(#seCharByteShortInt,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivLong(#seLong,#seCharByteShortInt)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1545,6 +1565,7 @@ assignmentModDouble { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 % #seDouble1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaModDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1554,6 +1575,7 @@ assignmentModFloat { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 % #seFloat1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaModFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1563,6 +1585,7 @@ assignmentModulo { \find(==>#normalassign ((modal operator))|{{ .. #loc = #se0 % #se1; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int), \sub(\typeof(#loc (program Variable)), int)) \replacewith([]==>[not(equals(#se1,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaMod(#se0,#se1)),#normalassign(post))]) \heuristics(executeIntegerAssignment) @@ -1611,7 +1634,7 @@ assignmentMultiplicationDouble { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 * #seDouble1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1621,7 +1644,7 @@ assignmentMultiplicationDoubleStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 * #seDouble1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(mulDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1631,7 +1654,7 @@ assignmentMultiplicationFloat { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 * #seFloat1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1641,7 +1664,7 @@ assignmentMultiplicationFloatStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 * #seFloat1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(mulFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1651,7 +1674,8 @@ assignmentMultiplicationInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 * #seCharByteShortInt1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaMulInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1660,7 +1684,8 @@ assignmentMultiplicationLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt * #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seCharByteShortInt,#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1669,7 +1694,8 @@ assignmentMultiplicationLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong * #seCharByteShortInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong,#seCharByteShortInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1678,7 +1704,8 @@ assignmentMultiplicationLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 * #seLong1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong0,#seLong1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1687,7 +1714,8 @@ assignmentShiftLeftInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 << #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftInt(#seCharByteShortInt0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1696,7 +1724,8 @@ assignmentShiftLeftLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 << #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftLong(#seLong0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1705,7 +1734,8 @@ assignmentShiftRightInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 >> #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1714,7 +1744,8 @@ assignmentShiftRightLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 >> #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightLong(#seLong0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1741,7 +1772,7 @@ assignmentSubtractionDouble { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 - #seDouble1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1751,7 +1782,7 @@ assignmentSubtractionDoubleStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seDouble0 - #seDouble1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(subDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java} @@ -1761,7 +1792,7 @@ assignmentSubtractionFloat { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 - #seFloat1; ... }}| (post)) -\varcond(\not\isStrictFp) +\varcond(\not\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1771,7 +1802,7 @@ assignmentSubtractionFloatStrictFP { \find(#normalassign ((modal operator))|{{ .. #loc = #seFloat0 - #seFloat1; ... }}| (post)) -\varcond(\isStrictFp) +\varcond(\isStrictFp, \sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(subFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -1781,7 +1812,8 @@ assignmentSubtractionInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 - #seCharByteShortInt1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaSubInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1790,7 +1822,8 @@ assignmentSubtractionLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt - #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seCharByteShortInt,#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1799,7 +1832,8 @@ assignmentSubtractionLong2 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong - #seCharByteShortInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong,#seCharByteShortInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1808,7 +1842,8 @@ assignmentSubtractionLong3 { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 - #seLong1; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong0,#seLong1)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1817,7 +1852,8 @@ assignmentUnsignedShiftRightInt { \find(#normalassign ((modal operator))|{{ .. #loc = #seCharByteShortInt0 >>> #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1826,7 +1862,8 @@ assignmentUnsignedShiftRightLong { \find(#normalassign ((modal operator))|{{ .. #loc = #seLong0 >>> #se; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightLong(#seLong0,#se)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -1955,7 +1992,7 @@ assignment_to_primitive_array_component_transaction { \varcond( \not \isReferenceArray(#v (program Variable))) \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; -\replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),update-application(elem-update(savedHeap)(if-then-else(equals(int::select(heap,#v,java.lang.Object::#$transient),Z(0(#))),store(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated,TRUE),if-then-else(equals(boolean::select(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated),FALSE),store(savedHeap,#v,arr(#se),#se0),savedHeap))),#transaction(post)))]) +\replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),update-application(elem-update(savedHeap)(if-then-else(equals(int::select(heap,#v,java.lang.Object::#$transient),Z(0(#))),store(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated,TRUE),if-then-else(equals(boolean::select(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated),FALSE),store(savedHeap,#v,arr(#se),#se0),savedHeap))),#transaction(post)))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: ((programRules:Java & runtimeExceptions:ban) & JavaCard:on)} ----------------------------------------------------- @@ -1981,7 +2018,7 @@ assignment_to_reference_array_component_transaction { \add [and(and(and(not(equals(#v,null)),lt(#se,length(#v))),geq(#se,Z(0(#)))),not(arrayStoreValid(#v,#se0)))]==>[] \replacewith([]==>[false]) ; \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; -\replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),update-application(elem-update(savedHeap)(if-then-else(equals(int::select(heap,#v,java.lang.Object::#$transient),Z(0(#))),store(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated,TRUE),if-then-else(equals(boolean::select(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated),FALSE),store(savedHeap,#v,arr(#se),#se0),savedHeap))),#transaction(post)))]) +\replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),update-application(elem-update(savedHeap)(if-then-else(equals(int::select(heap,#v,java.lang.Object::#$transient),Z(0(#))),store(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated,TRUE),if-then-else(equals(boolean::select(savedHeap,#v,java.lang.Object::#$transactionConditionallyUpdated),FALSE),store(savedHeap,#v,arr(#se),#se0),savedHeap))),#transaction(post)))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: ((programRules:Java & runtimeExceptions:ban) & JavaCard:on)} ----------------------------------------------------- @@ -2468,6 +2505,7 @@ bitwiseNegationInt { \find(#normalassign ((modal operator))|{{ .. #loc = ~#seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseNegateInt(#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -2477,6 +2515,7 @@ bitwiseNegationLong { \find(#normalassign ((modal operator))|{{ .. #loc = ~#seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseNegateLong(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} @@ -3476,15 +3515,6 @@ castDel2 { Choices: true} ----------------------------------------------------- -== castLongToFloatAddition2 (float addition) ========================================= -castLongToFloatAddition2 { -\find(#normalassign ((modal operator))|{{ .. - #loc = #seFloat + #seLong; -... }}| (post)) -\replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(#seFloat,float::cast(#seLong))),#normalassign(post))) -\heuristics(executeFloatAssignment) -Choices: programRules:Java} ------------------------------------------------------ == castToBoolean (castToBoolean) ========================================= castToBoolean { \find(#allmodal ((modal operator))|{{ .. @@ -4463,7 +4493,7 @@ compound_double_cast_expression { \find(#normalassign ((modal operator))|{{ .. #loc = (double) #nse; ... }}| (post)) -\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), double)) \replacewith(#normalassign ((modal operator))|{{ .. #typeof(#nse) #v = #nse; #loc = (double) #v; @@ -4503,7 +4533,7 @@ compound_float_cast_expression { \find(#normalassign ((modal operator))|{{ .. #loc = (float) #nse; ... }}| (post)) -\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), float)) \replacewith(#normalassign ((modal operator))|{{ .. #typeof(#nse) #v = #nse; #loc = (float) #v; @@ -5163,14 +5193,14 @@ Choices: true} createdInHeapToElementOf { \find(createdInHeap(s,h)) \varcond(\notFreeIn(fv (variable), h (Heap term)), \notFreeIn(fv (variable), s (LocSet term)), \notFreeIn(ov (variable), h (Heap term)), \notFreeIn(ov (variable), s (LocSet term))) -\replacewith(all{ov (variable)}(all{fv (variable)}(imp(elementOf(ov,fv,s),or(equals(ov,null),equals(boolean::select(h,ov,java.lang.Object::#$created),TRUE)))))) +\replacewith(all{ov (variable)}(all{fv (variable)}(imp(elementOf(ov,fv,s),or(equals(ov,null),equals(boolean::select(h,ov,java.lang.Object::#$created),TRUE)))))) \heuristics(classAxiom) Choices: programRules:Java} ----------------------------------------------------- == createdInHeapWithAllFields (createdInHeapWithAllFields) ========================================= createdInHeapWithAllFields { \find(createdInHeap(allFields(o),h)) -\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) +\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -5178,14 +5208,14 @@ Choices: programRules:Java} createdInHeapWithAllFieldsEQ { \assumes ([equals(allFields(o),EQ)]==>[]) \find(createdInHeap(EQ,h)) -\sameUpdateLevel\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) +\sameUpdateLevel\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- == createdInHeapWithArrayRange (createdInHeapWithArrayRange) ========================================= createdInHeapWithArrayRange { \find(createdInHeap(arrayRange(o,lower,upper),h)) -\replacewith(or(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),lt(upper,lower))) +\replacewith(or(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),lt(upper,lower))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -5193,7 +5223,7 @@ Choices: programRules:Java} createdInHeapWithArrayRangeEQ { \assumes ([equals(arrayRange(o,lower,upper),EQ)]==>[]) \find(createdInHeap(EQ,h)) -\sameUpdateLevel\replacewith(or(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),lt(upper,lower))) +\sameUpdateLevel\replacewith(or(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),lt(upper,lower))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -5254,7 +5284,7 @@ Choices: programRules:Java} == createdInHeapWithSingleton (createdInHeapWithSingleton) ========================================= createdInHeapWithSingleton { \find(createdInHeap(singleton(o,f),h)) -\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) +\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -5262,7 +5292,7 @@ Choices: programRules:Java} createdInHeapWithSingletonEQ { \assumes ([equals(singleton(o,f),EQ)]==>[]) \find(createdInHeap(EQ,h)) -\sameUpdateLevel\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) +\sameUpdateLevel\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -5335,7 +5365,7 @@ Choices: true} defInDomainImpliesCreated { \find(inDomainImpliesCreated(m)) \varcond(\notFreeIn(o (variable), m (Map term))) -\replacewith(all{o (variable)}(imp(inDomain(m,o),equals(boolean::select(heap,o,java.lang.Object::#$created),TRUE)))) +\replacewith(all{o (variable)}(imp(inDomain(m,o),equals(boolean::select(heap,o,java.lang.Object::#$created),TRUE)))) \heuristics(simplify_enlarging) Choices: true} ----------------------------------------------------- @@ -5495,7 +5525,7 @@ Choices: true} definitionOfNewOnHeap { \find(==>newOnHeap(h,s)) \varcond(\notFreeIn(i (variable), h (Heap term)), \notFreeIn(i (variable), s (Seq term))) -\replacewith([]==>[all{i (variable)}(imp(and(leq(Z(0(#)),i),lt(i,seqLen(s))),and(imp(equals(java.lang.Object::instance(any::seqGet(s,i)),TRUE),equals(boolean::select(h,java.lang.Object::seqGet(s,i),java.lang.Object::#$created),FALSE)),imp(equals(Seq::instance(any::seqGet(s,i)),TRUE),newOnHeap(h,Seq::seqGet(s,i))))))]) +\replacewith([]==>[all{i (variable)}(imp(and(leq(Z(0(#)),i),lt(i,seqLen(s))),and(imp(equals(java.lang.Object::instance(any::seqGet(s,i)),TRUE),equals(boolean::select(h,java.lang.Object::seqGet(s,i),java.lang.Object::#$created),FALSE)),imp(equals(Seq::instance(any::seqGet(s,i)),TRUE),newOnHeap(h,Seq::seqGet(s,i))))))]) \heuristics(comprehensions) Choices: true} ----------------------------------------------------- @@ -6248,7 +6278,7 @@ Choices: programRules:Java} dynamic_type_for_null { \find(G::exactInstance(null)) \varcond(\not\same(G, Null)) -\replacewith(FALSE) +\replacewith(FALSE) \heuristics(concrete) Choices: programRules:Java} ----------------------------------------------------- @@ -6307,7 +6337,7 @@ Choices: programRules:Java} == elementOfFreshLocs (elementOfFreshLocs) ========================================= elementOfFreshLocs { \find(elementOf(o,f,freshLocs(h))) -\replacewith(and(not(equals(o,null)),not(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)))) +\replacewith(and(not(equals(o,null)),not(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)))) \heuristics(concrete) Choices: programRules:Java} ----------------------------------------------------- @@ -9602,7 +9632,7 @@ getJavaCardTransient { #jcsystemType.#getTransient(#se)@#jcsystemType; ... }}| (post)) \replacewith([]==>[not(equals(#se,null))]) ; -\replacewith([]==>[update-application(elem-update(#lhs (program LeftHandSide))(int::select(heap,#se,java.lang.Object::#$transient)),#allmodal(post))]) +\replacewith([]==>[update-application(elem-update(#lhs (program LeftHandSide))(int::select(heap,#se,java.lang.Object::#$transient)),#allmodal(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)} ----------------------------------------------------- @@ -9949,6 +9979,7 @@ identityCastDouble { \find(#normalassign ((modal operator))|{{ .. #loc = (double) #seDouble; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) \replacewith(#normalassign ((modal operator))|{{ .. #loc = #seDouble; ... }}| (post)) @@ -9960,6 +9991,7 @@ identityCastFloat { \find(#normalassign ((modal operator))|{{ .. #loc = (float) #seFloat; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) \replacewith(#normalassign ((modal operator))|{{ .. #loc = #seFloat; ... }}| (post)) @@ -11307,7 +11339,7 @@ Choices: programRules:Java} insert_constant_string_value { \assumes ([wellFormed(heap)]==>[]) \find(#csv) -\sameUpdateLevel\add [or(equals(#constantvalue(#csv),null),and(not(equals(strPool(Seq::cast(#constantvalue(#csv))),null)),equals(boolean::select(heap,strPool(Seq::cast(#constantvalue(#csv))),java.lang.Object::#$created),TRUE)))]==>[] \replacewith(if-then-else(equals(#constantvalue(#csv),null),null,strPool(Seq::cast(#constantvalue(#csv))))) +\sameUpdateLevel\add [or(equals(#constantvalue(#csv),null),and(not(equals(strPool(Seq::cast(#constantvalue(#csv))),null)),equals(boolean::select(heap,strPool(Seq::cast(#constantvalue(#csv))),java.lang.Object::#$created),TRUE)))]==>[] \replacewith(if-then-else(equals(#constantvalue(#csv),null),null,strPool(Seq::cast(#constantvalue(#csv))))) \heuristics(concrete) Choices: true} ----------------------------------------------------- @@ -11545,24 +11577,6 @@ intDivRem { Choices: true} ----------------------------------------------------- -== intLongToFloatAddition1 (float addition) ========================================= -intLongToFloatAddition1 { -\find(#normalassign ((modal operator))|{{ .. - #loc = #seLong + #seFloat; -... }}| (post)) -\replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(float::cast(#seLong),#seFloat)),#normalassign(post))) -\heuristics(executeFloatAssignment) -Choices: programRules:Java} ------------------------------------------------------ -== intToFloatAddition (float addition) ========================================= -intToFloatAddition { -\find(#normalassign ((modal operator))|{{ .. - #loc = #seCharByteShortInt + #seFloat; -... }}| (post)) -\replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(float::cast(#seCharByteShortInt),#seFloat)),#normalassign(post))) -\heuristics(executeFloatAssignment) -Choices: programRules:Java} ------------------------------------------------------ == int_diff_minus_eq (int_diff_minus_eq) ========================================= int_diff_minus_eq { \find(sub(i0,neg(i1))) @@ -11581,7 +11595,7 @@ Choices: true} == intersectAllFieldsFreshLocs (intersectAllFieldsFreshLocs) ========================================= intersectAllFieldsFreshLocs { \find(equals(intersect(allFields(o),freshLocs(h)),empty)) -\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) +\replacewith(or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify) Choices: programRules:Java} ----------------------------------------------------- @@ -13591,7 +13605,8 @@ narrowingByteCastInt { \find(#normalassign ((modal operator))|{{ .. #loc = (byte) #seInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13600,7 +13615,8 @@ narrowingByteCastLong { \find(#normalassign ((modal operator))|{{ .. #loc = (byte) #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13609,15 +13625,27 @@ narrowingByteCastShort { \find(#normalassign ((modal operator))|{{ .. #loc = (byte) #seShort; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seShort)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seShort)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- +== narrowingCastDoubleToFloat (cast) ========================================= +narrowingCastDoubleToFloat { +\find(#normalassign ((modal operator))|{{ .. + #loc = (float) #seDouble; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) +\replacewith(update-application(elem-update(#loc (program Variable))(float::cast(#seDouble)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == narrowingCastFloatToInt (cast) ========================================= narrowingCastFloatToInt { \find(#normalassign ((modal operator))|{{ .. #loc = (int) #seFloat; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(int::cast(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -13627,6 +13655,7 @@ narrowingCastFloatToLong { \find(#normalassign ((modal operator))|{{ .. #loc = (long) #seFloat; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), int)) \replacewith(update-application(elem-update(#loc (program Variable))(int::cast(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} @@ -13645,7 +13674,8 @@ narrowingCharCastByte { \find(#normalassign ((modal operator))|{{ .. #loc = (char) #seByte; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seByte)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seByte)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13654,7 +13684,8 @@ narrowingCharCastInt { \find(#normalassign ((modal operator))|{{ .. #loc = (char) #seInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13663,7 +13694,8 @@ narrowingCharCastLong { \find(#normalassign ((modal operator))|{{ .. #loc = (char) #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13672,7 +13704,8 @@ narrowingCharCastShort { \find(#normalassign ((modal operator))|{{ .. #loc = (char) #seShort; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seShort)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seShort)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13690,7 +13723,8 @@ narrowingIntCastLong { \find(#normalassign ((modal operator))|{{ .. #loc = (int) #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastInt(#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastInt(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13717,7 +13751,8 @@ narrowingShortCastInt { \find(#normalassign ((modal operator))|{{ .. #loc = (short) #seInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13726,7 +13761,8 @@ narrowingShortCastLong { \find(#normalassign ((modal operator))|{{ .. #loc = (short) #seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -13909,7 +13945,7 @@ Choices: true} ----------------------------------------------------- == nullCreated (nullCreated) ========================================= nullCreated { -\add [or(all{h (variable)}(equals(boolean::select(h,null,java.lang.Object::#$created),TRUE)),all{h (variable)}(equals(boolean::select(h,null,java.lang.Object::#$created),FALSE)))]==>[] +\add [or(all{h (variable)}(equals(boolean::select(h,null,java.lang.Object::#$created),TRUE)),all{h (variable)}(equals(boolean::select(h,null,java.lang.Object::#$created),FALSE)))]==>[] Choices: programRules:Java} ----------------------------------------------------- @@ -13976,7 +14012,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreInLocSets { \assumes ([wellFormed(h)]==>[]) \find(elementOf(o2,f2,LocSet::select(h,o,f))==>) -\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -13984,7 +14020,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreInLocSetsEQ { \assumes ([wellFormed(h),equals(LocSet::select(h,o,f),EQ)]==>[]) \find(elementOf(o2,f2,EQ)==>) -\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -13992,7 +14028,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreInLocSetsEQFinal { \assumes ([wellFormed(h),equals(LocSet::final(o,f),EQ)]==>[]) \find(elementOf(o2,f2,EQ)==>) -\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14000,7 +14036,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreInLocSetsFinal { \assumes ([wellFormed(h)]==>[]) \find(elementOf(o2,f2,LocSet::final(o,f))==>) -\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o2,null),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14008,7 +14044,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreObserved { \find(obs) \sameUpdateLevel\varcond(\isObserver (obs (deltaObject term), h (Heap term))) -\add [or(equals(obs,null),equals(boolean::select(h,obs,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(obs,null),equals(boolean::select(h,obs,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14016,7 +14052,7 @@ Choices: programRules:Java} onlyCreatedObjectsAreObservedInLocSets { \find(elementOf(o,f,obs)==>) \varcond(\isObserver (obs (LocSet term), h (Heap term))) -\add [or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14025,7 +14061,7 @@ onlyCreatedObjectsAreObservedInLocSetsEQ { \assumes ([equals(obs,EQ)]==>[]) \find(elementOf(o,f,EQ)==>) \varcond(\isObserver (obs (LocSet term), h (Heap term))) -\add [or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))]==>[] +\add [or(equals(o,null),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14033,15 +14069,15 @@ Choices: programRules:Java} onlyCreatedObjectsAreReferenced { \assumes ([wellFormed(h)]==>[]) \find(deltaObject::select(h,o,f)) -\sameUpdateLevel\add [or(equals(deltaObject::select(h,o,f),null),equals(boolean::select(h,deltaObject::select(h,o,f),java.lang.Object::#$created),TRUE))]==>[] +\sameUpdateLevel\add [or(equals(deltaObject::select(h,o,f),null),equals(boolean::select(h,deltaObject::select(h,o,f),java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- == onlyCreatedObjectsAreReferencedFinal (onlyCreatedObjectsAreReferencedFinal) ========================================= onlyCreatedObjectsAreReferencedFinal { -\assumes ([wellFormed(h),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)]==>[]) +\assumes ([wellFormed(h),equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)]==>[]) \find(deltaObject::final(o,f)) -\sameUpdateLevel\add [or(equals(deltaObject::final(o,f),null),equals(boolean::select(h,deltaObject::final(o,f),java.lang.Object::#$created),TRUE))]==>[] +\sameUpdateLevel\add [or(equals(deltaObject::final(o,f),null),equals(boolean::select(h,deltaObject::final(o,f),java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: programRules:Java} ----------------------------------------------------- @@ -14049,7 +14085,7 @@ Choices: programRules:Java} only_created_objects_are_reachable { \assumes ([wellFormed(h)]==>[equals(o,null)]) \find(reach(h,s,o,o2,n)==>) -\add [or(not(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] +\add [or(not(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE)),equals(boolean::select(h,o2,java.lang.Object::#$created),TRUE))]==>[] \heuristics(inReachableStateImplication) Choices: reach:on} ----------------------------------------------------- @@ -15186,7 +15222,7 @@ Choices: (programRules:Java & runtimeExceptions:ban)} referencedObjectIsCreatedRighFinalEQ { \assumes ([equals(deltaObject::final(o,f),EQ)]==>[equals(EQ,null)]) \find(==>equals(boolean::select(h,EQ,java.lang.Object::#$created),TRUE)) -\add []==>[or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(o,null))] +\add []==>[or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(o,null))] \heuristics(concrete) Choices: programRules:Java} ----------------------------------------------------- @@ -15210,7 +15246,7 @@ Choices: programRules:Java} referencedObjectIsCreatedRightFinal { \assumes ([]==>[equals(deltaObject::final(o,f),null)]) \find(==>equals(boolean::select(h,deltaObject::final(o,f),java.lang.Object::#$created),TRUE)) -\replacewith([]==>[or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(o,null))]) +\replacewith([]==>[or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(o,null))]) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -15698,14 +15734,14 @@ Choices: true} == selectCreatedOfAnon (selectCreatedOfAnon) ========================================= selectCreatedOfAnon { \find(boolean::select(anon(h,s,h2),o,java.lang.Object::#$created)) -\replacewith(if-then-else(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),TRUE,boolean::select(h2,o,java.lang.Object::#$created))) +\replacewith(if-then-else(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),TRUE,boolean::select(h2,o,java.lang.Object::#$created))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- == selectCreatedOfAnonAsFormula (selectCreatedOfAnonAsFormula) ========================================= selectCreatedOfAnonAsFormula { \find(equals(boolean::select(anon(h,s,h2),o,java.lang.Object::#$created),TRUE)) -\replacewith(or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(boolean::select(h2,o,java.lang.Object::#$created),TRUE))) +\replacewith(or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(boolean::select(h2,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_ENLARGING) Choices: programRules:Java} ----------------------------------------------------- @@ -15713,7 +15749,7 @@ Choices: programRules:Java} selectCreatedOfAnonAsFormulaEQ { \assumes ([equals(anon(h,s,h2),EQ)]==>[]) \find(equals(boolean::select(EQ,o,java.lang.Object::#$created),TRUE)) -\sameUpdateLevel\replacewith(or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(boolean::select(h2,o,java.lang.Object::#$created),TRUE))) +\sameUpdateLevel\replacewith(or(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),equals(boolean::select(h2,o,java.lang.Object::#$created),TRUE))) \heuristics(simplify_ENLARGING) Choices: programRules:Java} ----------------------------------------------------- @@ -15721,14 +15757,14 @@ Choices: programRules:Java} selectCreatedOfAnonEQ { \assumes ([equals(anon(h,s,h2),EQ)]==>[]) \find(boolean::select(EQ,o,java.lang.Object::#$created)) -\sameUpdateLevel\replacewith(if-then-else(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),TRUE,boolean::select(h2,o,java.lang.Object::#$created))) +\sameUpdateLevel\replacewith(if-then-else(equals(boolean::select(h,o,java.lang.Object::#$created),TRUE),TRUE,boolean::select(h2,o,java.lang.Object::#$created))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- == selectOfAnon (selectOfAnon) ========================================= selectOfAnon { \find(beta::select(anon(h,s,h2),o,f)) -\replacewith(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f))) +\replacewith(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f))) \heuristics(semantics_blasting) Choices: programRules:Java} ----------------------------------------------------- @@ -15736,14 +15772,14 @@ Choices: programRules:Java} selectOfAnonEQ { \assumes ([equals(anon(h,s,h2),EQ)]==>[]) \find(beta::select(EQ,o,f)) -\sameUpdateLevel\replacewith(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f))) +\sameUpdateLevel\replacewith(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- == selectOfCreate (selectOfCreate) ========================================= selectOfCreate { \find(beta::select(create(h,o),o2,f)) -\replacewith(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f))) +\replacewith(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f))) \heuristics(semantics_blasting) Choices: programRules:Java} ----------------------------------------------------- @@ -15751,14 +15787,14 @@ Choices: programRules:Java} selectOfCreateEQ { \assumes ([equals(create(h,o),EQ)]==>[]) \find(beta::select(EQ,o2,f)) -\sameUpdateLevel\replacewith(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f))) +\sameUpdateLevel\replacewith(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- == selectOfMemset (selectOfMemset) ========================================= selectOfMemset { \find(beta::select(memset(h,s,x),o,f)) -\replacewith(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o,f))) +\replacewith(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o,f))) \heuristics(semantics_blasting) Choices: programRules:Java} ----------------------------------------------------- @@ -15766,14 +15802,14 @@ Choices: programRules:Java} selectOfMemsetEQ { \assumes ([equals(memset(h,s,x),EQ)]==>[]) \find(beta::select(EQ,o,f)) -\sameUpdateLevel\replacewith(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o,f))) +\sameUpdateLevel\replacewith(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o,f))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- == selectOfStore (selectOfStore) ========================================= selectOfStore { \find(beta::select(store(h,o,f,x),o2,f2)) -\replacewith(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2))) +\replacewith(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2))) \heuristics(semantics_blasting) Choices: programRules:Java} ----------------------------------------------------- @@ -15781,7 +15817,7 @@ Choices: programRules:Java} selectOfStoreEQ { \assumes ([equals(store(h,o,f,x),EQ)]==>[]) \find(beta::select(EQ,o2,f2)) -\sameUpdateLevel\replacewith(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2))) +\sameUpdateLevel\replacewith(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2))) \heuristics(simplify_heap_high_costs) Choices: programRules:Java} ----------------------------------------------------- @@ -16135,7 +16171,7 @@ setJavaCardTransient { #jcsystemType.#setTransient(#se, #se1)@#jcsystemType; ... }}| (post)) \replacewith([]==>[not(equals(#se,null))]) ; -\replacewith([]==>[update-application(elem-update(heap)(store(heap,#se,java.lang.Object::#$transient,#se1)),#allmodal(post))]) +\replacewith([]==>[update-application(elem-update(heap)(store(heap,#se,java.lang.Object::#$transient,#se1)),#allmodal(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)} ----------------------------------------------------- @@ -16345,7 +16381,7 @@ simplifySelectOfAnon { \find(beta::select(anon(h,s,h2),o,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16357,7 +16393,7 @@ simplifySelectOfAnonEQ { \find(beta::select(EQ,o,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(or(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),elementOf(o,f,freshLocs(h))),beta::select(h2,o,f),beta::select(h,o,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16368,7 +16404,7 @@ simplifySelectOfCreate { \find(beta::select(create(h,o),o2,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16380,7 +16416,7 @@ simplifySelectOfCreateEQ { \find(beta::select(EQ,o2,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),not(equals(o,null))),equals(f,java.lang.Object::#$created)),beta::cast(TRUE),beta::select(h,o2,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16391,7 +16427,7 @@ simplifySelectOfMemset { \find(beta::select(memset(h,s,x),o,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),x,beta::select(h,o,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),x,beta::select(h,o,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16403,7 +16439,7 @@ simplifySelectOfMemsetEQ { \find(beta::select(EQ,o,f)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),x,beta::select(h,o,f)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(elementOf(o,f,s),not(equals(f,java.lang.Object::#$created))),x,beta::select(h,o,f)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16414,7 +16450,7 @@ simplifySelectOfStore { \find(beta::select(store(h,o,f,x),o2,f2)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16426,7 +16462,7 @@ simplifySelectOfStoreEQ { \find(beta::select(EQ,o2,f2)) \inSequentState\replacewith(sk) \heuristics(concrete) -Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2)),sk)]==>[]) +Choices: programRules:Java}] \replacewith([equals(if-then-else(and(and(equals(o,o2),equals(f,f2)),not(equals(f,java.lang.Object::#$created))),beta::cast(x),beta::select(h,o2,f2)),sk)]==>[]) \heuristics(simplify_select) Choices: programRules:Java} ----------------------------------------------------- @@ -16759,7 +16795,7 @@ stringAssignment { \find(#normalassign ((modal operator))|{{ .. #v = #slit; ... }}| (post)) -\sameUpdateLevel\add [not(equals(strPool(#slit),null)),equals(boolean::select(heap,strPool(#slit),java.lang.Object::#$created),TRUE)]==>[] \replacewith(update-application(elem-update(#v (program Variable))(strPool(#slit)),#normalassign(post))) +\sameUpdateLevel\add [not(equals(strPool(#slit),null)),equals(boolean::select(heap,strPool(#slit),java.lang.Object::#$created),TRUE)]==>[] \replacewith(update-application(elem-update(#v (program Variable))(strPool(#slit)),#normalassign(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: true} ----------------------------------------------------- @@ -18313,25 +18349,52 @@ unaryMinusDouble { \find(#normalassign ((modal operator))|{{ .. #loc = -#seDouble; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusDouble(#seDouble)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} ----------------------------------------------------- +== unaryMinusDouble_cast (cast) ========================================= +unaryMinusDouble_cast { +\find(#normalassign ((modal operator))|{{ .. + #loc = -#se; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), \not\sub(\typeof(#se (program SimpleExpression)), double)) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = (double) (-#se); +... }}| (post)) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == unaryMinusFloat (unaryMinus) ========================================= unaryMinusFloat { \find(#normalassign ((modal operator))|{{ .. #loc = -#seFloat; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusFloat(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} ----------------------------------------------------- +== unaryMinusFloat_cast (cast) ========================================= +unaryMinusFloat_cast { +\find(#normalassign ((modal operator))|{{ .. + #loc = -#se; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), \not\sub(\typeof(#se (program SimpleExpression)), float)) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = (float) (-#se); +... }}| (post)) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == unaryMinusInt (unaryMinus) ========================================= unaryMinusInt { \find(#normalassign ((modal operator))|{{ .. #loc = -#seCharByteShortInt; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusInt(#seCharByteShortInt)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusInt(#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- @@ -18340,10 +18403,85 @@ unaryMinusLong { \find(#normalassign ((modal operator))|{{ .. #loc = -#seLong; ... }}| (post)) -\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusLong(#seLong)),#normalassign(post))) +\sameUpdateLevel\varcond(\sub(\typeof(#loc (program Variable)), int)) +\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusLong(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java} ----------------------------------------------------- +== unbalanced_float_expression (cast) ========================================= +unbalanced_float_expression { +\find(#normalassign ((modal operator))|{{ .. + #loc = #unbalancedFloat; +... }}| (post)) +\varcond(\floatingPointBalanced(#unbalancedFloat (program FloatingPointBinaryExpression), #balancedFloat (program FloatingPointBinaryExpression))) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = #balancedFloat; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_nonsimple_nonfloat_to_double_assignment (cast) ========================================= +unbalanced_nonsimple_nonfloat_to_double_assignment { +\find(#normalassign ((modal operator))|{{ .. + #loc = #nse; +... }}| (post)) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), double), \not\sub(\typeof(#nse (program NonSimpleExpression)), double)) +\replacewith(#normalassign ((modal operator))|{{ .. + #typeof(#nse) #v = #nse; + #loc = (double) #v; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_nonsimple_nonfloat_to_float_assignment (cast) ========================================= +unbalanced_nonsimple_nonfloat_to_float_assignment { +\find(#normalassign ((modal operator))|{{ .. + #loc = #nse; +... }}| (post)) +\varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression))), \sub(\typeof(#loc (program Variable)), float), \not\sub(\typeof(#nse (program NonSimpleExpression)), float)) +\replacewith(#normalassign ((modal operator))|{{ .. + #typeof(#nse) #v = #nse; + #loc = (float) #v; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_simple_double_assignment (cast) ========================================= +unbalanced_simple_double_assignment { +\find(#normalassign ((modal operator))|{{ .. + #loc = #se; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double), \sub(\typeof(#se (program SimpleExpression)), int)) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = (double) #se; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_simple_float_assignment (cast) ========================================= +unbalanced_simple_float_assignment { +\find(#normalassign ((modal operator))|{{ .. + #loc = #se; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float), \sub(\typeof(#se (program SimpleExpression)), int)) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = (float) #se; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- +== unbalanced_simple_float_to_double_assignment (cast) ========================================= +unbalanced_simple_float_to_double_assignment { +\find(#normalassign ((modal operator))|{{ .. + #loc = #seFloat; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) +\replacewith(#normalassign ((modal operator))|{{ .. + #loc = (double) #seFloat; +... }}| (post)) +\heuristics(simplify_prog) +Choices: programRules:Java} +----------------------------------------------------- == unionEqualsEmpty (unionEqualsEmpty) ========================================= unionEqualsEmpty { \find(equals(union(s,s2),empty)) @@ -18599,7 +18737,7 @@ Choices: programRules:Java} wellFormedMemsetArrayObject { \find(wellFormed(memset(h,arrayRange(ar,lo,up),x))) \succedentPolarity\varcond(\hasSort(\elemSort(ar (java.lang.Object term)), alpha)) -\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),arrayStoreValid(ar,x))))) +\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),arrayStoreValid(ar,x))))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -18615,7 +18753,7 @@ Choices: programRules:Java} wellFormedStoreArray { \find(wellFormed(store(h,o,arr(idx),x))) \succedentPolarity\varcond(\hasSort(\elemSort(o (java.lang.Object term)), alpha)) -\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),arrayStoreValid(o,x))))) +\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),arrayStoreValid(o,x))))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -18639,7 +18777,7 @@ Choices: programRules:Java} wellFormedStoreObject { \find(wellFormed(store(h,o,f,x))) \succedentPolarity\varcond(\fieldType(f (Field term), alpha)) -\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),equals(alpha::instance(x),TRUE))))) +\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),equals(alpha::instance(x),TRUE))))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -18648,7 +18786,7 @@ wellFormedStoreObjectEQ { \assumes ([equals(store(h,o,f,x),EQ)]==>[]) \find(wellFormed(EQ)) \sameUpdateLevel\succedentPolarity\varcond(\fieldType(f (Field term), alpha)) -\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),equals(alpha::instance(x),TRUE))))) +\replacewith(and(wellFormed(h),or(equals(x,null),and(equals(boolean::select(h,x,java.lang.Object::#$created),TRUE),equals(alpha::instance(x),TRUE))))) \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- @@ -18677,20 +18815,52 @@ wellFormedStorePrimitiveEQ { \heuristics(concrete) Choices: programRules:Java} ----------------------------------------------------- +== wideningCastFloatToDouble (cast) ========================================= +wideningCastFloatToDouble { +\find(#normalassign ((modal operator))|{{ .. + #loc = (double) #seFloat; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) +\replacewith(update-application(elem-update(#loc (program Variable))(double::cast(#seFloat)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- +== wideningCastIntToDouble (cast) ========================================= +wideningCastIntToDouble { +\find(#normalassign ((modal operator))|{{ .. + #loc = (double) #seCharByteShortInt; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) +\replacewith(update-application(elem-update(#loc (program Variable))(double::cast(#seCharByteShortInt)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == wideningCastIntToFloat (cast) ========================================= wideningCastIntToFloat { \find(#normalassign ((modal operator))|{{ .. #loc = (float) #seCharByteShortInt; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(float::cast(#seCharByteShortInt)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java} ----------------------------------------------------- +== wideningCastLongToDouble (cast) ========================================= +wideningCastLongToDouble { +\find(#normalassign ((modal operator))|{{ .. + #loc = (double) #seLong; +... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), double)) +\replacewith(update-application(elem-update(#loc (program Variable))(double::cast(#seLong)),#normalassign(post))) +\heuristics(executeFloatAssignment) +Choices: programRules:Java} +----------------------------------------------------- == wideningCastLongToFloat (cast) ========================================= wideningCastLongToFloat { \find(#normalassign ((modal operator))|{{ .. #loc = (float) #seLong; ... }}| (post)) +\varcond(\sub(\typeof(#loc (program Variable)), float)) \replacewith(update-application(elem-update(#loc (program Variable))(float::cast(#seLong)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}