Merge remote-tracking branch 'origin/main' into toolbarCleanup

codecov.yml

@@ -0,0 +1,9 @@
+github_checks:
+  annotations: false
+
+ignore:
+  - "key.ui/"  
+  - "keyext.ui.testgen/"  
+  - "key.removegenerics/"  
+  - "key.core.symbolic_execution.example/"  
+  - "key.core.example/"    

gradle/key_checks.xml

@@ -70,7 +70,9 @@
 	<property name="authorFormat" value="\S"/>
       </module>
 
-      <module name="JavadocVariable"/>
+      <module name="JavadocVariable">
+        <property name="ignoreNamePattern" value="LOGGER"/>
+      </module>
       <module name="JavadocStyle">
 	<property name="checkFirstSentence" value="false" />
       </module>

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

@@ -233,13 +233,14 @@ CONTAINERTYPE : '\\containerType';
 //BIGINT : '\\bigint';
 
 // Unicode symbols for special functions/predicates
-UTF_PRECEDES : '\u227A';
-UTF_IN : '\u220A';
-UTF_EMPTY : '\u2205';
-UTF_UNION : '\u222A';
-UTF_INTERSECT : '\u2229';
-UTF_SUBSET : '\u2286';
-UTF_SETMINUS : '\u2216';
+UTF_PRECEDES  : '\u227A' /*≺*/ | '\\precedes';
+UTF_IN        : '\u220A' /*∊*/ | '\\in';
+UTF_EMPTY     : '\u2205' /*∅*/ | '\\emptyset';
+UTF_UNION     : '\u222A' /*∪*/ | '\\cup';
+UTF_INTERSECT : '\u2229' /*∩*/ | '\\cap';
+UTF_SUBSET_EQ : '\u2286' /*⊆*/ | '\\subseteq';
+UTF_SUBSEQ    : '\u2282' /*⊂*/ | '\\subset';
+UTF_SETMINUS  : '\u2216' /*∖*/ | '\\setminus';
 
 fragment
 VOCAB
@@ -374,15 +375,13 @@ GREATEREQUAL
 :   '>' '=' | '\u2265'
       ;
 
-RGUILLEMETS
-      :   '>' '>'
-      ;
-
+
 WS:  [ \t\n\r\u00a0]+ -> channel(HIDDEN); //U+00A0 = non breakable whitespace
 STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ;
 LESS: '<';
 LESSEQUAL: '<' '=' | '\u2264';
-LGUILLEMETS: '<' '<';
+LGUILLEMETS: '<' '<' | '«' | '‹';
+RGUILLEMETS: '>''>' | '»' | '›';
 IMPLICIT_IDENT: '<' (LETTER)+ '>' ('$lmtd')? -> type(IDENT);
 
 EQV:	'<->' | '\u2194';

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

@@ -99,7 +99,7 @@ one_sort_decl
 
 simple_ident_dots
 :
-  simple_ident (DOT simple_ident)* | INT_LITERAL
+  simple_ident (DOT simple_ident)*
 ;
 
 simple_ident_dots_comma_list
@@ -304,7 +304,7 @@ id_declaration
 
 funcpred_name
 :
-  (sortId DOUBLECOLON)? name=simple_ident_dots
+  (sortId DOUBLECOLON)? (name=simple_ident_dots|num=INT_LITERAL)
 ;
 
 
@@ -327,9 +327,11 @@ literals:
   | integer
   | floatnum
   | string_literal
+  | emptyset
 ;
 
-term: parallel_term;
+emptyset: UTF_EMPTY;
+term: parallel_term; // weigl: should normally be equivalence_term
 //labeled_term: a=parallel_term (LGUILLEMETS labels=label RGUILLEMETS)?;
 parallel_term: a=elementary_update_term (PARALLEL b=elementary_update_term)*;
 elementary_update_term: a=equivalence_term (ASSIGN b=equivalence_term)?;
@@ -344,11 +346,12 @@ unary_formula:
   | MODALITY sub=term60                           #modality_term
 ;
 equality_term: a=comparison_term ((NOT_EQUALS|EQUALS) b=comparison_term)?;
-comparison_term: a=weak_arith_term ((LESS|LESSEQUAL|GREATER|GREATEREQUAL) b=weak_arith_term)?;
-weak_arith_term: a=strong_arith_term_1 (op+=(PLUS|MINUS) b+=strong_arith_term_1)*;
+comparison_term: a=weak_arith_term ((LESS|LESSEQUAL|GREATER|GREATEREQUAL|UTF_PRECEDES|UTF_SUBSET_EQ|UTF_SUBSEQ|UTF_IN) b=weak_arith_term)?;
+weak_arith_term: a=strong_arith_term_1 (op+=(PLUS|MINUS|UTF_UNION|UTF_INTERSECT|UTF_SETMINUS) b+=strong_arith_term_1)*;
 strong_arith_term_1: a=strong_arith_term_2 (STAR b+=strong_arith_term_2)*;
-strong_arith_term_2: a=atom_prefix ((PERCENT|SLASH) b=strong_arith_term_2)?;
-update_term: (LBRACE u=term RBRACE) (atom_prefix | unary_formula);
+strong_arith_term_2: a=atom_prefix (op+=(PERCENT|SLASH) b+=atom_prefix)*;
+update_term: (LBRACE u=parallel_term RBRACE) (atom_prefix | unary_formula);
+
 substitution_term:
  LBRACE SUBST  bv=one_bound_variable SEMI
      replacement=comparison_term RBRACE
@@ -383,7 +386,7 @@ primitive_term:
   | abbreviation
   | accessterm
   | literals
-;
+  ;
 
 /*
 weigl, 2021-03-12:
@@ -442,8 +445,16 @@ term
  */
 accessterm
 :
+  // OLD
   (sortId DOUBLECOLON)?
   firstName=simple_ident
+
+  /*Faster version
+  simple_ident_dots
+  ( EMPTYBRACKETS*
+    DOUBLECOLON
+    simple_ident
+  )?*/
   call?
   ( attribute )*
 ;
@@ -522,8 +533,9 @@ argument_list
     RPAREN
 ;
 
+integer_with_minux: MINUS? integer;
 integer:
-  (MINUS)? (INT_LITERAL | HEX_LITERAL | BIN_LITERAL)
+  (INT_LITERAL | HEX_LITERAL | BIN_LITERAL)
 ;
 
 floatnum: // called floatnum because "float" collide with the Java language
@@ -665,8 +677,9 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier.
 
 varexp_argument
 :
-    sortId //also covers possible varId
-  | TYPEOF LPAREN y=varId RPAREN
+    //weigl: Ambguity between term (which can also contain simple_ident_dots and sortId)
+    //       suggestion add an explicit keyword to request the sort by name or manually resolve later in builder
+    TYPEOF LPAREN y=varId RPAREN
   | CONTAINERTYPE LPAREN y=varId RPAREN
   | DEPENDINGON LPAREN y=varId RPAREN
   | term
@@ -691,8 +704,7 @@ option
 option_list
 :
   LPAREN
-    ( (option (COMMA option)*)
-      | option_expr)
+    (option_expr (COMMA option_expr)*)
   RPAREN
 ;
 

key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java

@@ -17,6 +17,8 @@
 import de.uka.ilkd.key.proof.io.RuleSource;
 
 import org.antlr.v4.runtime.*;
+import org.antlr.v4.runtime.atn.PredictionMode;
+import org.antlr.v4.runtime.misc.ParseCancellationException;
 import org.antlr.v4.runtime.tree.TerminalNode;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -121,7 +123,20 @@ public static KeyAst.File parseFile(File file) throws IOException {
 
     public static KeyAst.File parseFile(CharStream stream) {
         KeYParser p = createParser(stream);
-        KeYParser.FileContext ctx = p.file();
+
+        p.getInterpreter().setPredictionMode(PredictionMode.SLL);
+        // we don't want error messages or recovery during first try
+        p.removeErrorListeners();
+        p.setErrorHandler(new BailErrorStrategy());
+        KeYParser.FileContext ctx;
+        try {
+            ctx = p.file();
+        } catch (ParseCancellationException ex) {
+            LOGGER.warn("SLL was not enough");
+            p = createParser(stream);
+            ctx = p.file();
+        }
+
         p.getErrorReporter().throwException();
         return new KeyAst.File(ctx);
     }

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java

@@ -4,6 +4,7 @@
 import java.util.Iterator;
 import java.util.LinkedList;
 import java.util.List;
+import java.util.Objects;
 import java.util.function.Supplier;
 import java.util.stream.Collectors;
 import javax.annotation.Nullable;
@@ -19,6 +20,7 @@
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.logic.sort.ProgramSVSort;
 import de.uka.ilkd.key.logic.sort.Sort;
+import de.uka.ilkd.key.nparser.KeYLexer;
 import de.uka.ilkd.key.nparser.KeYParser;
 import de.uka.ilkd.key.nparser.KeYParser.DoubleLiteralContext;
 import de.uka.ilkd.key.nparser.KeYParser.FloatLiteralContext;
@@ -326,17 +328,34 @@ public Object visitComparison_term(KeYParser.Comparison_termContext ctx) {
 
     @Override
     public Object visitWeak_arith_term(KeYParser.Weak_arith_termContext ctx) {
-        Term termL = accept(ctx.a);
+        Term termL = Objects.requireNonNull(accept(ctx.a));
         if (ctx.op.isEmpty()) {
             return updateOrigin(termL, ctx);
         }
 
         List<Term> terms = mapOf(ctx.b);
         Term last = termL;
         for (int i = 0; i < terms.size(); i++) {
-            final String opTok = ctx.op.get(i).getText();
-            // it's either + or -.
-            String opname = opTok.equals("+") ? "add" : "sub";
+            String opname = "";
+            switch (ctx.op.get(i).getType()) {
+            case KeYLexer.UTF_INTERSECT:
+                opname = "intersect";
+                break;
+            case KeYLexer.UTF_SETMINUS:
+                opname = "setMinus";
+                break;
+            case KeYLexer.UTF_UNION:
+                opname = "union";
+                break;
+            case KeYLexer.PLUS:
+                opname = "add";
+                break;
+            case KeYLexer.MINUS:
+                opname = "sub";
+                break;
+            default:
+                semanticError(ctx, "Unexpected token: %s", ctx.op.get(i));
+            }
             Term cur = terms.get(i);
             last = binaryLDTSpecificTerm(ctx, opname, last, cur);
         }
@@ -375,16 +394,47 @@ public Object visitStrong_arith_term_1(KeYParser.Strong_arith_term_1Context ctx)
         return last;
     }
 
+    @Override
+    public Object visitEmptyset(KeYParser.EmptysetContext ctx) {
+        var op = services.getTypeConverter().getLocSetLDT().getEmpty();
+        return updateOrigin(getTermFactory().createTerm(op), ctx);
+    }
+
     @Override
     public Object visitStrong_arith_term_2(KeYParser.Strong_arith_term_2Context ctx) {
-        Term termL = accept(ctx.a);
-        if (ctx.b == null) {
-            return termL;
+        if (ctx.b.isEmpty()) { // fast path
+            return accept(ctx.a);
         }
 
-        Term termR = accept(ctx.b);
-        String opName = ctx.SLASH() != null ? "div" : "mod";
-        return binaryLDTSpecificTerm(ctx, opName, termL, termR);
+        List<Term> termL = mapOf(ctx.b);
+        // List<String> opName = ctx.op.stream().map(it -> it.getType()== KeYLexer.PERCENT ? "mod" :
+        // "div").collect(Collectors.toList());
+
+        Term term = accept(ctx.a);
+        var sort = term.sort();
+        if (sort == null) {
+            semanticError(ctx, "No sort for term '%s'", term);
+        }
+
+        var ldt = services.getTypeConverter().getLDTFor(sort);
+
+        if (ldt == null) {
+            // falling back to integer ldt (for instance for untyped schema variables)
+            ldt = services.getTypeConverter().getIntegerLDT();
+        }
+
+        assert ctx.op.size() == ctx.b.size();
+
+        for (int i = 0; i < termL.size(); i++) {
+            var opName = ctx.op.get(i).getType() == KeYLexer.PERCENT ? "mod" : "div";
+            Function op = ldt.getFunctionFor(opName, services);
+            if (op == null) {
+                semanticError(ctx, "Could not find function symbol '%s' for sort '%s'.", opName,
+                    sort);
+            }
+            term = binaryTerm(ctx, op, term, termL.get(i));
+        }
+        return term;
     }
 
     protected Term capsulateTf(ParserRuleContext ctx, Supplier<Term> termSupplier) {
@@ -1142,8 +1192,8 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) {
         List<String> parts = mapOf(ctx.name.simple_ident());
         String varfuncid = ctx.name.getText();
 
-        if (ctx.name.INT_LITERAL() != null) {// number
-            return toZNotation(ctx.name.INT_LITERAL().getText(), functions());
+        if (ctx.INT_LITERAL() != null) {// number
+            return toZNotation(ctx.INT_LITERAL().getText(), functions());
         }
 
         assert parts != null && varfuncid != null;
@@ -1172,7 +1222,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) {
             }
         } else {
             String firstName =
-                ctx.name.simple_ident().size() == 0 ? ctx.name.INT_LITERAL().getText()
+                ctx.name == null ? ctx.INT_LITERAL().getText()
                         : ctx.name.simple_ident(0).getText();
             op = lookupVarfuncId(ctx, firstName,
                 ctx.sortId() != null ? ctx.sortId().getText() : null, sortId);
@@ -1346,7 +1396,7 @@ private Term handleAttributes(Term current, List<KeYParser.AttributeContext> att
                     if (isCall) {
                         String classRef = current.sort().name().toString();
                         KeYJavaType kjt = getTypeByClassName(classRef); // Why not direct use of
-                                                                        // Sort?
+                        // Sort?
                         if (kjt == null) {
                             semanticError(ctxSuffix, "Could not find sort for %s", classRef);
                         }