Merge pull request #2324 from kframework/hotfix/verification

Verification Related Fixes
kframework · Aug 10, 2017 · 2a86a8b · 2a86a8b
2 parents 3a4eb22 + c9901e3
commit 2a86a8b
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 9 deletions.
diff --git a/java-backend/src/main/java/org/kframework/backend/java/builtins/IntToken.java b/java-backend/src/main/java/org/kframework/backend/java/builtins/IntToken.java
@@ -68,10 +68,10 @@ public BigInteger bigIntegerValue() {
      */
     public int intValue() {
         if (value.compareTo(BigInteger.valueOf(Integer.MAX_VALUE)) > 0) {
-            throw new ArithmeticException();
+            throw new ArithmeticException("IntToken too large for Int");
         }
         if (value.compareTo(BigInteger.valueOf(Integer.MIN_VALUE)) < 0) {
-            throw new ArithmeticException();
+            throw new ArithmeticException("IntToken too low for Int");
         }
         return (int)value.longValue();
     }
@@ -83,10 +83,10 @@ public int intValue() {
      */
     public long longValue() {
         if (value.compareTo(BigInteger.valueOf(Long.MAX_VALUE)) > 0) {
-            throw new ArithmeticException();
+            throw new ArithmeticException("IntToken too large for Long");
         }
         if (value.compareTo(BigInteger.valueOf(Long.MIN_VALUE)) < 0) {
-            throw new ArithmeticException();
+            throw new ArithmeticException("IntToken too low for Long");
         }
         return value.longValue();
     }
@@ -98,10 +98,10 @@ public long longValue() {
      */
     public byte unsignedByteValue() {
         if (value.compareTo(BigInteger.valueOf(255)) > 0) {
-            throw new ArithmeticException();
+            throw new ArithmeticException("IntToken too large for byte");
         }
         if (value.compareTo(BigInteger.valueOf(0)) < 0) {
-            throw new ArithmeticException();
+            throw new ArithmeticException("IntToken too low for byte");
         }
         return (byte)value.longValue();
     }

diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/ConstrainedTerm.java b/java-backend/src/main/java/org/kframework/backend/java/kil/ConstrainedTerm.java
@@ -201,6 +201,7 @@ public static List<Triple<ConjunctiveFormula, Boolean, Map<scala.collection.immu
             ConjunctiveFormula patternConstraint,
             Set<Variable> variables,
             TermContext context) {
+        context.setTopConstraint(subjectConstraint);
         List<ConjunctiveFormula> candidates = constraint.getDisjunctiveNormalForm().conjunctions().stream()
                 .map(c -> c.addAndSimplify(patternConstraint, context))
                 .filter(c -> !c.isFalse())

diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/FastRuleMatcher.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/FastRuleMatcher.java
@@ -7,6 +7,7 @@
 import org.kframework.backend.java.compile.KOREtoBackendKIL;
 import org.kframework.backend.java.kil.BuiltinList;
 import org.kframework.backend.java.kil.BuiltinMap;
+import org.kframework.backend.java.kil.BuiltinSet;
 import org.kframework.backend.java.kil.ConstrainedTerm;
 import org.kframework.backend.java.kil.GlobalContext;
 import org.kframework.backend.java.kil.InnerRHSRewrite;
@@ -326,6 +327,8 @@ private BitSet match(Term subject, Term pattern, BitSet ruleMask, scala.collecti
         } else if (subject instanceof Token && pattern instanceof Token) {
             // TODO: make tokens unique?
             return subject.equals(pattern) ? ruleMask : empty;
+        } else if (subject instanceof BuiltinSet && pattern instanceof BuiltinSet) {
+            return subject.equals(pattern) ? ruleMask : empty;
         } else {
             assert subject instanceof KItem || subject instanceof BuiltinList || subject instanceof Token || subject instanceof BuiltinMap : "unexpected class at matching: " + subject.getClass();
             assert pattern instanceof KItem || pattern instanceof BuiltinList || pattern instanceof Token : "unexpected class at matching: " + pattern.getClass();

diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/KILtoSMTLib.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/KILtoSMTLib.java
@@ -563,7 +563,7 @@ public ASTNode transform(BoolToken boolToken) {
 
     @Override
     public ASTNode transform(IntToken intToken) {
-        return new SMTLibTerm(Long.toString(intToken.longValue()));
+        return new SMTLibTerm(intToken.javaBackendValue());
     }
 
     @Override

diff --git a/java-backend/src/main/java/org/kframework/backend/java/util/Z3Wrapper.java b/java-backend/src/main/java/org/kframework/backend/java/util/Z3Wrapper.java
@@ -96,7 +96,6 @@ private boolean checkQueryWithExternalProcess(String query, int timeout) {
                 input.flush();
                 result = output.readLine();
                 z3Process.destroy();
-
                 if (result != null) {
                     break;
                 }
@@ -110,7 +109,11 @@ private boolean checkQueryWithExternalProcess(String query, int timeout) {
                 System.err.println("Z3 crashed on query:\n" + SMT_PRELUDE + query + "(check-sat)\n");
             }
         } else if (globalOptions.debug && !Z3_QUERY_RESULTS.contains(result)) {
-            System.err.println("Unexpected Z3 query result:\n" + result);
+            System.err.println("==== Z3: Unexpected query result ===========");
+            System.err.println("== Query:");
+            System.err.println(query + "(check-sat)\n");
+            System.err.println("== Result:");
+            System.err.println(result + "\n");
         }
         return result.equals("unsat");
     }