Floating Point rules for casts

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

@@ -3,7 +3,6 @@
 import java.util.LinkedHashMap;
 import java.util.Map;
 
-import de.uka.ilkd.key.java.expression.operator.BinaryOperator;
 import de.uka.ilkd.key.java.Expression;
 import de.uka.ilkd.key.java.Label;
 import de.uka.ilkd.key.java.NamedProgramElement;
@@ -20,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;
@@ -1097,7 +1092,7 @@ public boolean canStandFor(ProgramElement check, ExecutionContext ec, Services s
 
     /**
      * A schema variable for a binary operation in which at least one floating
-     * point type is involved.
+     * point type is involved and both arguments are simple expressions.
      * Needed for numeric promotion with floating point types.
      *
      * @see de.uka.ilkd.key.rule.conditions.FloatingPointBalancedCondition
@@ -1110,10 +1105,14 @@ public FloatingPointBinaryExprSort(String name) {
 
         @Override
         public boolean canStandFor(ProgramElement check, ExecutionContext ec, Services services) {
-            if (!(check instanceof BinaryOperator)) {
+            if (!(check instanceof BinaryOperator || check instanceof ComparativeOperator)) {
+                return false;
+            }
+            Operator bin = (Operator) check;
+            if (!SIMPLEEXPRESSION.canStandFor(bin.getChildAt(0), ec, services) ||
+                    !SIMPLEEXPRESSION.canStandFor(bin.getChildAt(1), ec, services)) {
                 return false;
             }
-            BinaryOperator bin = (BinaryOperator) check;
             KeYJavaType t1 = getKeYJavaType(bin.getChildAt(0), ec, services);
             KeYJavaType t2 = getKeYJavaType(bin.getChildAt(1), ec, services);
 

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

@@ -1,31 +1,25 @@
 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.Term;
-import de.uka.ilkd.key.logic.TermServices;
-import de.uka.ilkd.key.logic.op.ElementaryUpdate;
-import de.uka.ilkd.key.logic.op.LocationVariable;
 import de.uka.ilkd.key.logic.op.SVSubstitute;
 import de.uka.ilkd.key.logic.op.SchemaVariable;
-import de.uka.ilkd.key.logic.op.UpdateApplication;
-import de.uka.ilkd.key.logic.op.UpdateJunctor;
 import de.uka.ilkd.key.logic.sort.Sort;
-import de.uka.ilkd.key.proof.TermProgramVariableCollector;
 import de.uka.ilkd.key.rule.MatchConditions;
 import de.uka.ilkd.key.rule.VariableCondition;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 
-import javax.annotation.Nullable;
-import java.util.Set;
-
 
 /**
  * This variable condition adds required numeric promotions to Java operations
@@ -64,13 +58,18 @@ public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, Mat
             Services services) {
 
         SVInstantiations svInst = mc.getInstantiations();
-        BinaryOperator inInst = (BinaryOperator) svInst.getInstantiation(unbalanced);
+        Object untypedInstantiation = svInst.getInstantiation(unbalanced);
+        if (!(untypedInstantiation instanceof BinaryOperator
+                || untypedInstantiation instanceof ComparativeOperator)) {
+            return null;
+        }
+        Operator inInst = (Operator) untypedInstantiation;
         JavaProgramElement outInst = (JavaProgramElement) svInst.getInstantiation(balanced);
         if (inInst == null) {
             return mc;
         }
 
-        BinaryOperator properResultInst = balance(inInst, services);
+        Operator properResultInst = balance(inInst, services);
         if (properResultInst == null) {
             return null;
         } else if (outInst == null) {
@@ -103,7 +102,7 @@ private static KeYJavaType getKeYJavaType(ProgramElement pe, Services services)
      * @return null if already same types. Otherwise a binary operator which
      *         has an added cast compared to the input
      */
-    private static @Nullable BinaryOperator balance(BinaryOperator inInst, Services services) {
+    private static @Nullable Operator balance(Operator inInst, Services services) {
 
         ProgramElement child0 = inInst.getChildAt(0);
         ProgramElement child1 = inInst.getChildAt(1);
@@ -142,12 +141,12 @@ private static KeYJavaType getKeYJavaType(ProgramElement pe, Services services)
      * @return a binary operation similar to the input, but with one
      *         cast added to child childNo.
      */
-    private static BinaryOperator cast(BinaryOperator inInst, int childNo, KeYJavaType kjt,
+    private static Operator cast(Operator inInst, int childNo, KeYJavaType kjt,
             Services services) {
         Expression child = (Expression) inInst.getChildAt(childNo);
         TypeCast cast = new TypeCast(child, new TypeRef(kjt));
         ProgramElementReplacer per = new ProgramElementReplacer(inInst, services);
         ProgramElement result = per.replace(child, cast);
-        return (BinaryOperator) result;
+        return (Operator) result;
     }
 }

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;
         }