Solving the FP completeness issues in #1723

key.core/src/main/antlr4/KeYLexer.g4

@@ -122,6 +122,7 @@ DEPENDINGON : '\\dependingOn';
 DISJOINTMODULONULL  : '\\disjointModuloNull';
 DROP_EFFECTLESS_ELEMENTARIES : '\\dropEffectlessElementaries';
 DROP_EFFECTLESS_STORES : '\\dropEffectlessStores';
+FLOATING_POINT_BALANCED : '\\floatingPointBalanced';
 SIMPLIFY_IF_THEN_ELSE_UPDATE : '\\simplifyIfThenElseUpdate';
 ENUM_CONST : '\\enumConstant';
 FREELABELIN : '\\freeLabelIn';

key.core/src/main/antlr4/KeYParser.g4

@@ -616,6 +616,7 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier.
   | SAME_OBSERVER
   | DROP_EFFECTLESS_ELEMENTARIES
   | DROP_EFFECTLESS_STORES
+  | FLOATING_POINT_BALANCED
   | DIFFERENTFIELDS
   | SIMPLIFY_IF_THEN_ELSE_UPDATE
   | CONTAINS_ASSIGNMENT

key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java

@@ -19,13 +19,9 @@
 import de.uka.ilkd.key.java.declaration.VariableSpecification;
 import de.uka.ilkd.key.java.expression.ArrayInitializer;
 import de.uka.ilkd.key.java.expression.Literal;
+import de.uka.ilkd.key.java.expression.Operator;
 import de.uka.ilkd.key.java.expression.literal.StringLiteral;
-import de.uka.ilkd.key.java.expression.operator.DLEmbeddedExpression;
-import de.uka.ilkd.key.java.expression.operator.Instanceof;
-import de.uka.ilkd.key.java.expression.operator.Intersect;
-import de.uka.ilkd.key.java.expression.operator.Negative;
-import de.uka.ilkd.key.java.expression.operator.New;
-import de.uka.ilkd.key.java.expression.operator.NewArray;
+import de.uka.ilkd.key.java.expression.operator.*;
 import de.uka.ilkd.key.java.expression.operator.adt.*;
 import de.uka.ilkd.key.java.reference.*;
 import de.uka.ilkd.key.java.statement.Catch;
@@ -232,6 +228,9 @@ public abstract class ProgramSVSort extends AbstractSort {
         new SimpleExpressionExceptingTypeSort("SimpleExpressionNonFloatDouble",
             new PrimitiveType[] { PrimitiveType.JAVA_FLOAT, PrimitiveType.JAVA_DOUBLE });
 
+    public static final ProgramSVSort FLOAT_BINARY_EXP =
+        new FloatingPointBinaryExprSort("FloatingPointBinaryExpression");
+
     // --------------- Specials that can be get rid of perhaps--------------
 
     public static final ProgramSVSort LOOPINIT = new LoopInitSort();
@@ -1091,6 +1090,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.

key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java

@@ -266,6 +266,9 @@ public VariableCondition build(Object[] arguments, List<String> 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);
@@ -366,7 +369,8 @@ public IsLabeledCondition build(Object[] arguments, List<String> parameters,
             CONTAINS_ASSIGNMENT, FIELD_TYPE, STATIC_REFERENCE, DIFFERENT_FIELDS, SAME_OBSERVER,
             applyUpdateOnRigid, DROP_EFFECTLESS_ELEMENTARIES, SIMPLIFY_ITE_UPDATE, SUBFORMULAS,
             STATIC_FIELD, SUBFORMULA, DROP_EFFECTLESS_STORES, EQUAL_UNIQUE, META_DISJOINT,
-            IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP);
+            IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP,
+            FLOATING_POINT_BALANCED);
         register(STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, GET_INVARIANT, GET_FREE_INVARIANT,
             GET_VARIANT, IS_LABELED);
         loadWithServiceLoader();

key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FloatingPointBalancedCondition.java

@@ -0,0 +1,152 @@
+package de.uka.ilkd.key.rule.conditions;
+
+import javax.annotation.Nullable;
+
+import de.uka.ilkd.key.java.Expression;
+import de.uka.ilkd.key.java.JavaProgramElement;
+import de.uka.ilkd.key.java.ProgramElement;
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.expression.Operator;
+import de.uka.ilkd.key.java.expression.operator.BinaryOperator;
+import de.uka.ilkd.key.java.expression.operator.ComparativeOperator;
+import de.uka.ilkd.key.java.expression.operator.TypeCast;
+import de.uka.ilkd.key.java.reference.TypeRef;
+import de.uka.ilkd.key.java.visitor.ProgramElementReplacer;
+import de.uka.ilkd.key.logic.op.SVSubstitute;
+import de.uka.ilkd.key.logic.op.SchemaVariable;
+import de.uka.ilkd.key.logic.sort.Sort;
+import de.uka.ilkd.key.rule.MatchConditions;
+import de.uka.ilkd.key.rule.VariableCondition;
+import de.uka.ilkd.key.rule.inst.SVInstantiations;
+
+
+/**
+ * This variable condition adds required numeric promotions to Java operations
+ * with floating point arguments.
+ *
+ * For example: In the expression 1.0f + 1.0d, the first argument will be implicitly
+ * cast to double like (double)1.0f + 1.0d.
+ *
+ * If such an unbalanced expression occurs in the program, according casts are
+ * introduced by this varcond.
+ *
+ * The varcond is used like \floatingPointBalanced(#unbalanced, #balanced)
+ * where the first argument is the one from the find expression of the rule
+ * and the second one is the one that will be changed.
+ *
+ * @author Mattias Ulbrich
+ * @see de.uka.ilkd.key.logic.sort.ProgramSVSort.FloatingPointBinaryExprSort
+ */
+public final class FloatingPointBalancedCondition implements VariableCondition {
+    /**
+     * The first SV: It holds the unbalanced input expression
+     */
+    private final SchemaVariable unbalanced;
+    /**
+     * The 2nd SV: It holds the balanced computed expression
+     */
+    private final SchemaVariable balanced;
+
+    public FloatingPointBalancedCondition(SchemaVariable unbalanced, SchemaVariable balanced) {
+        this.unbalanced = unbalanced;
+        this.balanced = balanced;
+    }
+
+    @Override
+    public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc,
+            Services services) {
+
+        SVInstantiations svInst = mc.getInstantiations();
+        Object untypedInstantiation = svInst.getInstantiation(unbalanced);
+        if (!(untypedInstantiation instanceof BinaryOperator
+                || untypedInstantiation instanceof ComparativeOperator)) {
+            return null;
+        }
+        Operator inInst = (Operator) untypedInstantiation;
+        JavaProgramElement outInst = (JavaProgramElement) svInst.getInstantiation(balanced);
+        if (inInst == null) {
+            return mc;
+        }
+
+        Operator properResultInst = balance(inInst, services);
+        if (properResultInst == null) {
+            return null;
+        } else if (outInst == null) {
+            svInst = svInst.add(balanced, properResultInst, services);
+            return mc.setInstantiations(svInst);
+        } else if (outInst.equals(properResultInst)) {
+            return mc;
+        } else {
+            return null;
+        }
+    }
+
+    @Override
+    public String toString() {
+        return "\\floatingPointBalanced(" + unbalanced + ", " + balanced + ")";
+    }
+
+    private static KeYJavaType getKeYJavaType(ProgramElement pe, Services services) {
+        return services.getTypeConverter().getKeYJavaType((Expression) pe);
+    }
+
+    /**
+     * Make sure the result is a binary operation with same types on lhs
+     * and rhs. do this by adding cast if needed.
+     *
+     * If no cast is needed, return null.
+     *
+     * @param inInst the binary AST element to balance
+     * @param services as usual ... to lookup everything
+     * @return null if already same types. Otherwise a binary operator which
+     *         has an added cast compared to the input
+     */
+    private static @Nullable 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;
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java

@@ -3,6 +3,7 @@
 import de.uka.ilkd.key.java.Expression;
 import de.uka.ilkd.key.java.ProgramElement;
 import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.expression.operator.BinaryOperator;
 import de.uka.ilkd.key.logic.Name;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.TermServices;
@@ -146,14 +147,17 @@ public Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate,
                 Term gsTerm = null;
                 if (inst instanceof Term) {
                     gsTerm = (Term) inst;
+                    s = gsTerm.sort();
+                } else if (inst instanceof BinaryOperator) {
+                    s = services.getTypeConverter().getKeYJavaType((BinaryOperator) inst).getSort();
                 } else if (inst instanceof ProgramElement) {
                     gsTerm = services.getTypeConverter().convertToLogicElement(
                         (ProgramElement) inst, instMap.getExecutionContext());
+                    s = gsTerm.sort();
                 } else {
                     Debug.fail("Unexpected substitution for sv " + resolveSV + ":" + inst);
                     return null;
                 }
-                s = gsTerm.sort();
             }
             return s;
         }