Fix incorrect priority attribute on :/=K (runtimeverification#364)

dwightguth · web-flow · commit 525915b0aff4 · 2019-03-20T10:14:23.000-05:00
* fix priority of ==K

* test for ambiguity

* fix for w2e on parsing warnings

* add test for fatal ambiguity

* fix display as error not warning

* another typo

* add regression test
diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k
@@ -786,8 +786,8 @@ module K-EQUAL
       change in the future).*/
 
   syntax Bool ::= left:
-                  K ":=K" K           [function, functional, klabel(_:=K_), symbol, equalsEqualsK]
-                | K ":/=K" K          [function, functional, klabel(_:/=K_), symbol, notEqualsEqualsK]
+                  K ":=K" K           [function, functional, klabel(_:=K_), symbol, equalEqualK]
+                | K ":/=K" K          [function, functional, klabel(_:/=K_), symbol, notEqualEqualK]
 
   syntax priorities equalEqualK notEqualEqualK > boolOperation mlOp
   rule K1:K =/=K K2:K => notBool (K1 ==K K2)
diff --git a/k-distribution/tests/regression-new/equals-pattern/Makefile b/k-distribution/tests/regression-new/equals-pattern/Makefile
@@ -2,5 +2,6 @@ DEF=test
 EXT=test
 TESTDIR=.
 KOMPILE_BACKEND?=llvm
+KOMPILE_FLAGS=-w2e
 
 include ../../../include/ktest.mak
diff --git a/k-distribution/tests/regression-new/equals-pattern/test.k b/k-distribution/tests/regression-new/equals-pattern/test.k
@@ -1,9 +1,10 @@
 // Copyright (c) 2019 K Team. All Rights Reserved.
-module TEST
+
+module TEST-SYNTAX
   imports INT
   imports K-EQUAL
 
-syntax KItem ::= foo(Int) | bar(Int) | baz(KItem)
+syntax KItem ::= foo(Int) | bar(Int) | baz(KItem) | stuff(K) | StringLiteral(K) | WStringLiteral(K)
 
 rule I:Int => foo(_) :=K foo(I)
   requires I ==Int 0
@@ -19,4 +20,14 @@ rule baz(A:KItem) => #fun(baz(B) => baz(bar(_)) :=K baz(B))(baz(A))
   requires baz(_) :/=K A
 rule baz(baz(A:KItem)) => #fun(baz(B) => baz(A) :=K baz(B))(baz(A))
 
+rule stuff(K) => 1
+          requires StringLiteral(...) :/=K K
+               andBool WStringLiteral(...) :/=K K
+rule stuff(K) => 1
+          requires StringLiteral(...) :=K K
+               andBool WStringLiteral(...) :=K K
+endmodule
+
+module TEST
+  imports TEST-SYNTAX
 endmodule
diff --git a/k-distribution/tests/regression-new/fatalWarnings/test2.k b/k-distribution/tests/regression-new/fatalWarnings/test2.k
@@ -0,0 +1,12 @@
+module TEST2-SYNTAX
+
+endmodule
+
+module TEST2
+  imports TEST2-SYNTAX
+
+  syntax Foo ::= "foo" [klabel(foo), symbol]
+  syntax Bar ::= "foo" [klabel(bar), symbol]
+
+  rule foo => 0
+endmodule
diff --git a/k-distribution/tests/regression-new/fatalWarnings/test2.k.out b/k-distribution/tests/regression-new/fatalWarnings/test2.k.out
@@ -0,0 +1,8 @@
+[Error] Compiler: Had 1 parsing errors.
+[Error] Inner Parser: Parsing ambiguity. Arbitrarily choosing the first.
+1: syntax Bar ::= "foo"
+    bar(.KList)
+2: syntax Foo ::= "foo"
+    foo(.KList)
+	Source(test2.k)
+	Location(11,8,11,11)
diff --git a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java
@@ -31,6 +31,7 @@
 import org.kframework.utils.errorsystem.KEMException;
 import org.kframework.utils.errorsystem.KExceptionManager;
 import org.kframework.utils.errorsystem.ParseFailedException;
+import org.kframework.utils.errorsystem.KException.ExceptionType;
 import org.kframework.utils.file.FileUtil;
 import scala.Option;
 import scala.Tuple2;
@@ -392,7 +393,15 @@ private Stream<? extends K> performParse(Map<String, ParsedSentence> cache, Pars
         }
         result = parser.parseString(b.contents(), START_SYMBOL, scanner, source, startLine, startColumn, !b.att().contains("macro") && !b.att().contains("alias"));
         parsedBubbles.getAndIncrement();
-        kem.addAllKException(result._2().stream().map(e -> e.getKException()).collect(Collectors.toList()));
+        if (kem.options.warnings2errors && !result._2().isEmpty()) {
+          for (KEMException err : result._2()) {
+            if (kem.options.warnings.includesExceptionType(err.exception.getType())) {
+              errors.add(KEMException.asError(err));
+            }
+          }
+        } else {
+          kem.addAllKException(result._2().stream().map(e -> e.getKException()).collect(Collectors.toList()));
+        }
         if (result._1().isRight()) {
             KApply k = (KApply) new TreeNodesToKORE(Outer::parseSort, isStrict).down(result._1().right().get());
             k = KApply(k.klabel(), k.klist(), k.att().addAll(b.att().remove("contentStartLine").remove("contentStartColumn").remove(Source.class).remove(Location.class)));
diff --git a/kore/src/main/java/org/kframework/utils/errorsystem/KEMException.java b/kore/src/main/java/org/kframework/utils/errorsystem/KEMException.java
@@ -94,6 +94,10 @@ public static KEMException outerParserError(String message, Throwable e, Source
         return create(ExceptionType.ERROR, KExceptionGroup.OUTER_PARSER, message, e, location, source);
     }
 
+    public static KEMException asError(KEMException warning) {
+        return new KEMException(warning.exception, ExceptionType.ERROR);
+    }
+
     @Override
     public String getMessage() {
         return exception.toString();
