From 985f3415a46bb1c22c9233a020ea40e4067cb1b5 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 5 Jul 2017 21:47:06 -0500 Subject: [PATCH 1/8] Improve message when IntToken can't be converted to primitave --- .../kframework/backend/java/builtins/IntToken.java | 12 ++++++------ 1 file changed, 6 insertions(+), 6 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 index f4294ff751..8a781ce827 100644 --- 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(); } From ec9975fae7a89cd5d9fe5ed1f6bfb2281f70414a Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 5 Jul 2017 21:48:24 -0500 Subject: [PATCH 2/8] SMTLibTerm: IntToken: Don't covert to string via Long This avoids errors when Long has insufficient precicion to hold the number, when sending it to Z3. --- .../java/org/kframework/backend/java/symbolic/KILtoSMTLib.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 index f92ca70ce7..7ce66cb00c 100644 --- 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 From 7b21b4cddef254592f5e7ca422b8a8763fa56125 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 5 Jul 2017 21:49:58 -0500 Subject: [PATCH 3/8] Z3Wrapper: Print z3 query when --debug is passed and z3 fails This give us something (though not much) to help debugging why they are failing. --- .../java/org/kframework/backend/java/util/Z3Wrapper.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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 index ad49775862..b7ff2f665e 100644 --- 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"); } From cef5b904918229680dc0ab7b860d691e56d8221f Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Mon, 24 Jul 2017 10:48:20 +0530 Subject: [PATCH 4/8] FastRuleMatcher.java: Adds Missing Case - when lhs and term are sets. --- .../org/kframework/backend/java/symbolic/FastRuleMatcher.java | 3 +++ 1 file changed, 3 insertions(+) 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 index fdf5544dcb..e1b22a53ad 100644 --- 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(); From abe14ab1d6149a85137242a0a25c3eff0e6cafc0 Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Wed, 26 Jul 2017 18:04:04 +0530 Subject: [PATCH 5/8] SymbolicRewriter.java: Fork TermContext on case analysis. When a case analysis occurs, i.e. there are multiple results resulting from a single rewrite, the context objects cannot be shared between the terms. Hence, create new copies of TermContext for each term after case analysis. --- .../backend/java/symbolic/SymbolicRewriter.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java index 1e44f0e4a2..a40e817a7d 100644 --- a/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java +++ b/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java @@ -665,13 +665,19 @@ public List proveRule( } for (ConstrainedTerm cterm : results) { + TermContext context; + if(results.size() > 1) { + context = cterm.termContext().fork(); + } else { + context = cterm.termContext(); + } ConstrainedTerm result = new ConstrainedTerm( cterm.term(), cterm.constraint().removeBindings( Sets.difference( cterm.constraint().substitution().keySet(), initialTerm.variableSet())), - cterm.termContext()); + context); if (visited.add(result)) { nextQueue.add(result); } From 470a697b34b4280369d63d76b772ca7485d5aace Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Thu, 27 Jul 2017 00:09:02 +0530 Subject: [PATCH 6/8] FastRuleMatcher.java: Adds case - when subject and pattern are KLists. This should fix the assertion error that appears while proving. --- .../org/kframework/backend/java/symbolic/FastRuleMatcher.java | 2 ++ 1 file changed, 2 insertions(+) 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 index e1b22a53ad..00e8e25fb0 100644 --- 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 @@ -329,6 +329,8 @@ private BitSet match(Term subject, Term pattern, BitSet ruleMask, scala.collecti return subject.equals(pattern) ? ruleMask : empty; } else if (subject instanceof BuiltinSet && pattern instanceof BuiltinSet) { return subject.equals(pattern) ? ruleMask : empty; + } else if (subject instanceof KList && pattern instanceof KList) { + 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(); From cd50fcdb7c256842ebe54d99081aa162de0ee095 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Thu, 27 Jul 2017 21:15:06 -0700 Subject: [PATCH 7/8] Set `topConstraint` in `ConstrainedTerm::evaluateConstraints`. --- .../org/kframework/backend/java/kil/ConstrainedTerm.java | 1 + .../backend/java/symbolic/SymbolicRewriter.java | 8 +------- 2 files changed, 2 insertions(+), 7 deletions(-) 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 index 830ce3115f..a21451766e 100644 --- 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 variables, TermContext context) { + context.setTopConstraint(subjectConstraint); List 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/SymbolicRewriter.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java index a40e817a7d..1e44f0e4a2 100644 --- a/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java +++ b/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java @@ -665,19 +665,13 @@ public List proveRule( } for (ConstrainedTerm cterm : results) { - TermContext context; - if(results.size() > 1) { - context = cterm.termContext().fork(); - } else { - context = cterm.termContext(); - } ConstrainedTerm result = new ConstrainedTerm( cterm.term(), cterm.constraint().removeBindings( Sets.difference( cterm.constraint().substitution().keySet(), initialTerm.variableSet())), - context); + cterm.termContext()); if (visited.add(result)) { nextQueue.add(result); } From c9901e39c6ba4f19a930732e9d660ee5788121cc Mon Sep 17 00:00:00 2001 From: Manasvi Saxena Date: Sat, 29 Jul 2017 19:45:41 +0530 Subject: [PATCH 8/8] Revert "FastRuleMatcher.java: Adds case - when subject and pattern are KLists." This caused Tests to fail, and matcher should never be called with klists. Hence the bug must be somewhere else. This reverts commit 470a697b34b4280369d63d76b772ca7485d5aace. --- .../org/kframework/backend/java/symbolic/FastRuleMatcher.java | 2 -- 1 file changed, 2 deletions(-) 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 index 00e8e25fb0..e1b22a53ad 100644 --- 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 @@ -329,8 +329,6 @@ private BitSet match(Term subject, Term pattern, BitSet ruleMask, scala.collecti return subject.equals(pattern) ? ruleMask : empty; } else if (subject instanceof BuiltinSet && pattern instanceof BuiltinSet) { return subject.equals(pattern) ? ruleMask : empty; - } else if (subject instanceof KList && pattern instanceof KList) { - 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();