|
| 1 | +package de.uka.ilkd.key.rule.conditions; |
| 2 | + |
| 3 | +import de.uka.ilkd.key.java.Expression; |
| 4 | +import de.uka.ilkd.key.java.JavaProgramElement; |
| 5 | +import de.uka.ilkd.key.java.ProgramElement; |
| 6 | +import de.uka.ilkd.key.java.Services; |
| 7 | +import de.uka.ilkd.key.java.abstraction.KeYJavaType; |
| 8 | +import de.uka.ilkd.key.java.expression.operator.BinaryOperator; |
| 9 | +import de.uka.ilkd.key.java.expression.operator.TypeCast; |
| 10 | +import de.uka.ilkd.key.java.reference.TypeRef; |
| 11 | +import de.uka.ilkd.key.java.visitor.ProgramElementReplacer; |
| 12 | +import de.uka.ilkd.key.logic.Term; |
| 13 | +import de.uka.ilkd.key.logic.TermServices; |
| 14 | +import de.uka.ilkd.key.logic.op.ElementaryUpdate; |
| 15 | +import de.uka.ilkd.key.logic.op.LocationVariable; |
| 16 | +import de.uka.ilkd.key.logic.op.SVSubstitute; |
| 17 | +import de.uka.ilkd.key.logic.op.SchemaVariable; |
| 18 | +import de.uka.ilkd.key.logic.op.UpdateApplication; |
| 19 | +import de.uka.ilkd.key.logic.op.UpdateJunctor; |
| 20 | +import de.uka.ilkd.key.logic.sort.Sort; |
| 21 | +import de.uka.ilkd.key.proof.TermProgramVariableCollector; |
| 22 | +import de.uka.ilkd.key.rule.MatchConditions; |
| 23 | +import de.uka.ilkd.key.rule.VariableCondition; |
| 24 | +import de.uka.ilkd.key.rule.inst.SVInstantiations; |
| 25 | + |
| 26 | +import javax.annotation.Nullable; |
| 27 | +import java.util.Set; |
| 28 | + |
| 29 | + |
| 30 | +/** |
| 31 | + * This variable condition adds required numeric promotions to Java operations |
| 32 | + * with floating point arguments. |
| 33 | + * |
| 34 | + * For example: In the expression 1.0f + 1.0d, the first argument will be implicitly |
| 35 | + * cast to double like (double)1.0f + 1.0d. |
| 36 | + * |
| 37 | + * If such an unbalanced expression occurs in the program, according casts are |
| 38 | + * introduced by this varcond. |
| 39 | + * |
| 40 | + * The varcond is used like \floatingPointBalanced(#unbalanced, #balanced) |
| 41 | + * where the first argument is the one from the find expression of the rule |
| 42 | + * and the second one is the one that will be changed. |
| 43 | + * |
| 44 | + * @author Mattias Ulbrich |
| 45 | + * @see de.uka.ilkd.key.logic.sort.ProgramSVSort.FloatingPointBinaryExprSort |
| 46 | + */ |
| 47 | +public final class FloatingPointBalancedCondition implements VariableCondition { |
| 48 | + /** |
| 49 | + * The first SV: It holds the unbalanced input expression |
| 50 | + */ |
| 51 | + private final SchemaVariable unbalanced; |
| 52 | + /** |
| 53 | + * The 2nd SV: It holds the balanced computed expression |
| 54 | + */ |
| 55 | + private final SchemaVariable balanced; |
| 56 | + |
| 57 | + public FloatingPointBalancedCondition(SchemaVariable unbalanced, SchemaVariable balanced) { |
| 58 | + this.unbalanced = unbalanced; |
| 59 | + this.balanced = balanced; |
| 60 | + } |
| 61 | + |
| 62 | + @Override |
| 63 | + public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, |
| 64 | + Services services) { |
| 65 | + |
| 66 | + SVInstantiations svInst = mc.getInstantiations(); |
| 67 | + BinaryOperator inInst = (BinaryOperator) svInst.getInstantiation(unbalanced); |
| 68 | + JavaProgramElement outInst = (JavaProgramElement) svInst.getInstantiation(balanced); |
| 69 | + if (inInst == null) { |
| 70 | + return mc; |
| 71 | + } |
| 72 | + |
| 73 | + BinaryOperator properResultInst = balance(inInst, services); |
| 74 | + if (properResultInst == null) { |
| 75 | + return null; |
| 76 | + } else if (outInst == null) { |
| 77 | + svInst = svInst.add(balanced, properResultInst, services); |
| 78 | + return mc.setInstantiations(svInst); |
| 79 | + } else if (outInst.equals(properResultInst)) { |
| 80 | + return mc; |
| 81 | + } else { |
| 82 | + return null; |
| 83 | + } |
| 84 | + } |
| 85 | + |
| 86 | + @Override |
| 87 | + public String toString() { |
| 88 | + return "\\floatingPointBalanced(" + unbalanced + ", " + balanced + ")"; |
| 89 | + } |
| 90 | + |
| 91 | + private static KeYJavaType getKeYJavaType(ProgramElement pe, Services services) { |
| 92 | + return services.getTypeConverter().getKeYJavaType((Expression) pe); |
| 93 | + } |
| 94 | + |
| 95 | + /** |
| 96 | + * Make sure the result is a binary operation with same types on lhs |
| 97 | + * and rhs. do this by adding cast if needed. |
| 98 | + * |
| 99 | + * If no cast is needed, return null. |
| 100 | + * |
| 101 | + * @param inInst the binary AST element to balance |
| 102 | + * @param services as usual ... to lookup everything |
| 103 | + * @return null if already same types. Otherwise a binary operator which |
| 104 | + * has an added cast compared to the input |
| 105 | + */ |
| 106 | + private static @Nullable BinaryOperator balance(BinaryOperator inInst, Services services) { |
| 107 | + |
| 108 | + ProgramElement child0 = inInst.getChildAt(0); |
| 109 | + ProgramElement child1 = inInst.getChildAt(1); |
| 110 | + |
| 111 | + KeYJavaType type0 = getKeYJavaType(child0, services); |
| 112 | + KeYJavaType type1 = getKeYJavaType(child1, services); |
| 113 | + if (type0.getSort() == type1.getSort()) { |
| 114 | + // nothing to be done ... same type |
| 115 | + return null; |
| 116 | + } |
| 117 | + |
| 118 | + Sort doubleSort = services.getTypeConverter().getDoubleLDT().targetSort(); |
| 119 | + Sort floatSort = services.getTypeConverter().getFloatLDT().targetSort(); |
| 120 | + if (type0.getSort() == doubleSort) { |
| 121 | + return cast(inInst, 1, type0, services); |
| 122 | + } |
| 123 | + if (type1.getSort() == doubleSort) { |
| 124 | + return cast(inInst, 0, type1, services); |
| 125 | + } |
| 126 | + if (type0.getSort() == floatSort) { |
| 127 | + return cast(inInst, 1, type0, services); |
| 128 | + } |
| 129 | + if (type1.getSort() == floatSort) { |
| 130 | + return cast(inInst, 0, type1, services); |
| 131 | + } |
| 132 | + return null; |
| 133 | + } |
| 134 | + |
| 135 | + /** |
| 136 | + * Add a cast to a binary operation. |
| 137 | + * |
| 138 | + * @param inInst the tree to modify |
| 139 | + * @param childNo the child to which a cast is to be added |
| 140 | + * @param kjt the type to which to cast |
| 141 | + * @param services as usual |
| 142 | + * @return a binary operation similar to the input, but with one |
| 143 | + * cast added to child childNo. |
| 144 | + */ |
| 145 | + private static BinaryOperator cast(BinaryOperator inInst, int childNo, KeYJavaType kjt, |
| 146 | + Services services) { |
| 147 | + Expression child = (Expression) inInst.getChildAt(childNo); |
| 148 | + TypeCast cast = new TypeCast(child, new TypeRef(kjt)); |
| 149 | + ProgramElementReplacer per = new ProgramElementReplacer(inInst, services); |
| 150 | + ProgramElement result = per.replace(child, cast); |
| 151 | + return (BinaryOperator) result; |
| 152 | + } |
| 153 | +} |
0 commit comments