Support for JML\TYPE (KeYProject#3465)

key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java

@@ -111,6 +111,10 @@ public SeqLDT getSeqLDT() {
         return (SeqLDT) getLDT(SeqLDT.NAME);
     }
 
+    public SortLDT getSortLDT() {
+        return (SortLDT) getLDT(SortLDT.NAME);
+    }
+
     public MapLDT getMapLDT() {
         return (MapLDT) getLDT(MapLDT.NAME);
     }

key.core/src/main/java/de/uka/ilkd/key/java/abstraction/PrimitiveType.java

@@ -55,6 +55,8 @@ public final class PrimitiveType implements Type {
         new PrimitiveType("\\free", FreeLiteral.INSTANCE, FreeLDT.NAME);
     public static final PrimitiveType JAVA_MAP =
         new PrimitiveType("\\map", EmptyMapLiteral.INSTANCE, MapLDT.NAME);
+    public static final PrimitiveType JAVA_TYPE =
+        new PrimitiveType("\\TYPE", NullLiteral.NULL, SortLDT.NAME);
 
     public static final PrimitiveType PROGRAM_SV = new PrimitiveType("SV", null, null);
 

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Subtype.java

@@ -0,0 +1,54 @@
+/* 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.java.expression.operator;
+
+import de.uka.ilkd.key.java.Expression;
+import de.uka.ilkd.key.java.visitor.Visitor;
+
+import org.key_project.util.ExtList;
+
+/**
+ * Subtype
+ */
+public class Subtype extends BinaryOperator {
+
+    public Subtype(ExtList children) {
+        super(children);
+    }
+
+    public Subtype(Expression lhs, Expression rhs) {
+        super(lhs, rhs);
+    }
+
+
+    /**
+     * Get precedence.
+     *
+     * @return the int value.
+     */
+
+    public int getPrecedence() {
+        return 3;
+    }
+
+    /**
+     * Get notation.
+     *
+     * @return the int value.
+     */
+
+    public int getNotation() {
+        return INFIX;
+    }
+
+    /**
+     * calls the corresponding method of a visitor in order to perform some action/transformation on
+     * this element
+     *
+     * @param v the Visitor
+     */
+    public void visit(Visitor v) {
+        v.performActionOnSubtype(this);
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java

@@ -78,6 +78,7 @@ public Expression getDefaultValue(Type type) {
                 case "\\locset" -> EmptySetLiteral.INSTANCE;
                 case "\\seq" -> EmptySeqLiteral.INSTANCE;
                 case "\\set" -> new DLEmbeddedExpression("emptySet", Collections.emptyList());
+                case "\\TYPE" -> new DLEmbeddedExpression("any::ssort", Collections.emptyList());
                 case "\\free" -> new DLEmbeddedExpression("atom", Collections.emptyList());
                 case "\\map" -> EmptyMapLiteral.INSTANCE;
                 default -> {

key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java

@@ -743,6 +743,11 @@ public void performActionOnStringLiteral(StringLiteral x) {
         doDefaultAction(x);
     }
 
+    @Override
+    public void performActionOnSubtype(Subtype x) {
+        doDefaultAction(x);
+    }
+
     @Override
     public void performActionOnSuperArrayDeclaration(SuperArrayDeclaration x) {
         doDefaultAction(x);

key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java

@@ -406,4 +406,6 @@ void performActionOnCcatchBreakWildcardParameterDeclaration(
      * @param jmlAssert the statement to perform the action on.
      */
     void performActionOnJmlAssert(JmlAssert jmlAssert);
+
+    void performActionOnSubtype(Subtype subtype);
 }

key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java

@@ -135,6 +135,7 @@ public static Map<Name, LDT> getNewLDTInstances(Services s) {
         ret.put(HeapLDT.NAME, new HeapLDT(s));
         ret.put(PermissionLDT.NAME, new PermissionLDT(s));
         ret.put(SeqLDT.NAME, new SeqLDT(s));
+        ret.put(SortLDT.NAME, new SortLDT(s));
         ret.put(FreeLDT.NAME, new FreeLDT(s));
         ret.put(MapLDT.NAME, new MapLDT(s));
         ret.put(FloatLDT.NAME, new FloatLDT(s));

key.core/src/main/java/de/uka/ilkd/key/ldt/SortLDT.java

@@ -0,0 +1,98 @@
+/* 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.ldt;
+
+import de.uka.ilkd.key.java.Expression;
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.abstraction.Type;
+import de.uka.ilkd.key.java.expression.Literal;
+import de.uka.ilkd.key.java.expression.Operator;
+import de.uka.ilkd.key.java.expression.operator.Subtype;
+import de.uka.ilkd.key.java.reference.ExecutionContext;
+import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.logic.TermServices;
+import de.uka.ilkd.key.logic.op.JFunction;
+import de.uka.ilkd.key.logic.op.SortDependingFunction;
+import de.uka.ilkd.key.proof.io.ProofSaver;
+
+import org.key_project.logic.Name;
+import org.key_project.logic.sort.Sort;
+import org.key_project.util.ExtList;
+
+
+public final class SortLDT extends LDT {
+
+    public static final Name NAME = new Name("SORT");
+
+    private final SortDependingFunction ssort;
+    private final JFunction ssubsort;
+
+    public SortLDT(TermServices services) {
+        super(NAME, services);
+        ssort = addSortDependingFunction(services, "ssort");
+        ssubsort = addFunction(services, "ssubsort");
+    }
+
+    public SortDependingFunction getSsort(Sort instanceSort, TermServices services) {
+        return ssort.getInstanceFor(instanceSort, services);
+    }
+
+    public JFunction getSsubsort() {
+        return ssubsort;
+    }
+
+    @Override
+    public boolean isResponsible(Operator op, Term[] subs, Services services, ExecutionContext ec) {
+        return op instanceof Subtype;
+    }
+
+    @Override
+    public boolean isResponsible(Operator op, Term left, Term right, Services services,
+            ExecutionContext ec) {
+        return op instanceof Subtype;
+    }
+
+    @Override
+    public boolean isResponsible(Operator op, Term sub, TermServices services,
+            ExecutionContext ec) {
+        return op instanceof Subtype;
+    }
+
+    @Override
+    public Term translateLiteral(Literal lit, Services services) {
+        assert false;
+        return null;
+    }
+
+    @Override
+    public JFunction getFunctionFor(Operator op, Services services, ExecutionContext ec) {
+        if (op instanceof Subtype) {
+            return ssubsort;
+        }
+
+        assert false;
+        return null;
+    }
+
+    @Override
+    public boolean hasLiteralFunction(JFunction f) {
+        return f instanceof SortDependingFunction sf && sf.isSimilar(ssort);
+    }
+
+    @Override
+    public Expression translateTerm(Term t, ExtList children, Services services) {
+        if (t.op() instanceof SortDependingFunction sf && sf.isSimilar(ssort)) {
+            // TODO
+        }
+
+        throw new IllegalArgumentException(
+            "Could not translate " + ProofSaver.printTerm(t, null) + " to program.");
+    }
+
+    @Override
+    public Type getType(Term t) {
+        assert false;
+        return null;
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java

@@ -592,6 +592,11 @@ public void performActionOnMergeContract(MergeContract x) {
         layouter.print("//@ merge-contract");
     }
 
+    @Override
+    public void performActionOnSubtype(Subtype x) {
+        printOperator(x, "<:");
+    }
+
     @Override
     public void performActionOnArrayDeclaration(ArrayDeclaration type) {
         Type baseType = type.getBaseType().getKeYJavaType().getJavaType();

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java

@@ -72,6 +72,7 @@ class Translator extends JmlParserBaseVisitor<Object> {
     private final HeapLDT heapLDT;
     private final LocSetLDT locSetLDT;
     private final BooleanLDT booleanLDT;
+    private final SortLDT sortLDT;
     private final SLExceptionFactory exc;
     private final JmlTermFactory termFactory;
     private final ProgramVariable selfVar;
@@ -98,6 +99,7 @@ class Translator extends JmlParserBaseVisitor<Object> {
         this.heapLDT = services.getTypeConverter().getHeapLDT();
         this.locSetLDT = services.getTypeConverter().getLocSetLDT();
         this.booleanLDT = services.getTypeConverter().getBooleanLDT();
+        this.sortLDT = services.getTypeConverter().getSortLDT();
         this.exc = new SLExceptionFactory(null, 1, 0);
 
         this.selfVar = self;
@@ -569,11 +571,18 @@ public SLExpression visitEqualityexpr(JmlParser.EqualityexprContext ctx) {
             if (floatResult != null) {
                 return floatResult;
             }
+
+            SLExpression other = expr.get(i);
+            if (other.isType() && !result.isType()) {
+                JFunction ssortFunc = sortLDT.getSsort(other.getType().getSort(), services);
+                other = new SLExpression(tb.func(ssortFunc));
+            }
+
             exc.updatePosition(ctx.getStart());
             if (tok.getText().equals("==")) {
-                result = termFactory.eq(result, expr.get(i));
+                result = termFactory.eq(result, other);
             } else {
-                result = termFactory.neq(result, expr.get(i));
+                result = termFactory.neq(result, other);
             }
         }
         return result;
@@ -621,33 +630,35 @@ public SLExpression visitInstance_of(JmlParser.Instance_ofContext ctx) {
 
     @Override
     public Object visitSt_expr(JmlParser.St_exprContext ctx) {
-        SLExpression result = accept(ctx.shiftexpr(0));
+        SLExpression left = accept(ctx.shiftexpr(0));
         SLExpression right = accept(ctx.shiftexpr(1));
-        assert result != null && right != null;
-
-        if (result.isTerm() || right.isTerm()) {
-            raiseError("Cannot build subtype expression from terms.", ctx);
-        }
-        assert result.isType();
-        assert right.isType();
-        if (result.getTerm() == null) {
-            exc.addIgnoreWarning("subtype expression <: only supported for"
-                + " \\typeof() arguments on the left side.", ctx.ST().getSymbol());
-            final Namespace<JFunction> fns = services.getNamespaces().functions();
-            int x = -1;
-            Name name;
-            do {
-                name = new Name("subtype_" + ++x);
-            } while (fns.lookup(name) != null);
-            final JFunction z = new JFunction(name, JavaDLTheory.FORMULA);
-            fns.add(z);
-            result = new SLExpression(tb.func(z));
+        assert left != null && right != null;
+
+        if (left.isType() && left.getTerm() != null && right.isType()) {
+            Sort os = right.getType().getSort();
+            JFunction ioFunc = services.getJavaDLTheory().getInstanceofSymbol(os, services);
+            left = new SLExpression(tb.equals(tb.func(ioFunc, left.getTerm()), tb.TRUE()));
         } else {
-            final JFunction ioFunc =
-                services.getJavaDLTheory().getInstanceofSymbol(right.getType().getSort(), services);
-            result = new SLExpression(tb.equals(tb.func(ioFunc, result.getTerm()), tb.TRUE()));
+            Term leftSort;
+            if (left.isTerm()) {
+                leftSort = left.getTerm();
+            } else {
+                JFunction ssortFunc = sortLDT.getSsort(left.getType().getSort(), services);
+                leftSort = tb.func(ssortFunc);
+            }
+
+            Term rightSort;
+            if (right.isTerm()) {
+                rightSort = right.getTerm();
+            } else {
+                JFunction ssortFunc = sortLDT.getSsort(right.getType().getSort(), services);
+                rightSort = tb.func(ssortFunc);
+            }
+
+            left = new SLExpression(tb.func(sortLDT.getSsubsort(), leftSort, rightSort));
         }
-        return result;
+
+        return left;
     }
 
 
@@ -1861,7 +1872,7 @@ public Object visitDims(JmlParser.DimsContext ctx) {
     @Override
     public KeYJavaType visitType(JmlParser.TypeContext ctx) {
         if (ctx.TYPE() != null) {
-            raiseError("Only the function \\TYPE is supported", ctx);
+            return javaInfo.getKeYJavaType(PrimitiveType.JAVA_TYPE);
         }
         return oneOf(ctx.builtintype(), ctx.referencetype());
     }

key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java

@@ -77,6 +77,7 @@ public class KeYCrossReferenceSourceInfo extends DefaultCrossReferenceSourceInfo
     private PrimitiveType mapType;
     private PrimitiveType bigintType;
     private PrimitiveType realType;
+    private PrimitiveType typeType;
 
 
     public KeYCrossReferenceSourceInfo(ServiceConfiguration config) {
@@ -106,6 +107,7 @@ public void initialize(ServiceConfiguration cfg) {
         mapType = new PrimitiveType("\\map", this);
         bigintType = new PrimitiveType("\\bigint", this);
         realType = new PrimitiveType("\\real", this);
+        typeType = new PrimitiveType("\\TYPE", this);
 
         // HEAP
         name2primitiveType.put(locsetType.getName(), locsetType);
@@ -118,6 +120,7 @@ public void initialize(ServiceConfiguration cfg) {
         // JML's primitive types
         name2primitiveType.put(bigintType.getName(), bigintType);
         name2primitiveType.put(realType.getName(), realType);
+        name2primitiveType.put(typeType.getName(), typeType);
     }
 
     @Override

key.core/src/main/javacc/de/uka/ilkd/key/parser/proofjava/ProofJavaParser.jj

@@ -503,6 +503,7 @@ TOKEN :
 | < TRANSIENT: "transient" >
 | < TRUE: "true" >
 | < TRY: "try" >
+| < TYPE: "\\TYPE" >
 | < VOID: "void" >
 | < VOLATILE: "volatile" >
 | < WHILE: "while" >
@@ -2028,6 +2029,7 @@ TypeReference PrimitiveType() :
   | "\\seq"
   | "\\free"
   | "\\map"
+  | "\\TYPE"
   | <DL_EMBEDDED_FUNCTION>
   )
   {

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Object.java

@@ -1,7 +1,6 @@
 package java.lang;
 
-public class Object {  
-
+public class Object {
 
     /*@ public normal_behavior
       @   assignable \nothing;

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key

@@ -26,4 +26,5 @@
     map,
     freeADT,
     wellfound,
-    charListHeader;
+    charListHeader,
+    types;