From 8d558222443ab7ec2b72332e5d1c4f30ef02b01d Mon Sep 17 00:00:00 2001 From: Brandon Moore Date: Fri, 29 Sep 2017 15:44:42 -0500 Subject: [PATCH 1/2] Give Z3 smt label to integer and operation to support ABI verification. --- .../java/org/kframework/backend/java/symbolic/KILtoSMTLib.java | 1 + k-distribution/include/builtin/domains.k | 2 +- 2 files changed, 2 insertions(+), 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 67d02f1bf9..0079403dec 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 @@ -85,6 +85,7 @@ public class KILtoSMTLib extends CopyOnWriteTransformer { "int_max", "int_min", "int_abs", + "int_and", /* extra float theory */ "remainder", "min", diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 67fe96eb8f..d573a3339b 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -312,7 +312,7 @@ module INT Int ">>Int" Int [function, left, latex({#1}\mathrel{\gg_{\scriptstyle\it Int}}{#2}), hook(INT.shr)] | Int "< left: - Int "&Int" Int [function, left, latex({#1}\mathrel{\&_{\scriptstyle\it Int}}{#2}), hook(INT.and)] + Int "&Int" Int [function, left, smtlib(int_and), latex({#1}\mathrel{\&_{\scriptstyle\it Int}}{#2}), hook(INT.and)] > left: Int "xorInt" Int [function, left, latex({#1}\mathrel{\oplus_{\scriptstyle\it Int}}{#2}), hook(INT.xor)] > left: From 1a27de43fd1738384210cf230a38d3642ae4d2e2 Mon Sep 17 00:00:00 2001 From: Brandon Moore Date: Thu, 9 Nov 2017 05:03:08 -0600 Subject: [PATCH 2/2] Add (check-sat) to preprocess context before proving goal --- .../backend/java/symbolic/KILtoSMTLib.java | 6 ++--- .../backend/java/symbolic/SMTOperations.java | 2 +- .../backend/java/util/Z3Wrapper.java | 22 +++++++++++++++++-- 3 files changed, 24 insertions(+), 6 deletions(-) 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 0079403dec..a11741f790 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 @@ -195,9 +195,9 @@ public static String translateImplication( sb.append(leftTransformer.getConstantDeclarations(Sets.difference( Sets.union(leftTransformer.variables(), rightTransformer.variables()), rightHandSideOnlyVariables))); - sb.append("(assert (and "); + sb.append("(assert "); sb.append(leftExpression); - sb.append(" (not "); + sb.append(")\n(check-sat)\n(assert (not "); rightHandSideOnlyVariables = Sets.intersection( rightTransformer.variables(), rightHandSideOnlyVariables); @@ -210,7 +210,7 @@ public static String translateImplication( if (!rightHandSideOnlyVariables.isEmpty()) { sb.append(")"); } - sb.append(")))"); + sb.append("))"); return sb.toString(); } diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/SMTOperations.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/SMTOperations.java index b94a0a0117..155a75cbc6 100644 --- a/java-backend/src/main/java/org/kframework/backend/java/symbolic/SMTOperations.java +++ b/java-backend/src/main/java/org/kframework/backend/java/symbolic/SMTOperations.java @@ -63,7 +63,7 @@ public boolean impliesSMT( Set rightOnlyVariables) { if (smtOptions.smt == SMTSolver.Z3) { try { - return z3.isUnsat( + return z3.isImplication( KILtoSMTLib.translateImplication(left, right, rightOnlyVariables), smtOptions.z3ImplTimeout); } catch (UnsupportedOperationException | SMTTranslationFailure e) { 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 b7ff2f665e..3aaa3d2227 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 @@ -49,7 +49,15 @@ public Z3Wrapper( public synchronized boolean isUnsat(String query, int timeout) { if (options.z3Executable) { - return checkQueryWithExternalProcess(query, timeout); + return checkQueryWithExternalProcess(query, 0, timeout); + } else { + return checkQueryWithLibrary(query, timeout); + } + } + + public synchronized boolean isImplication(String query, int timeout) { + if (options.z3Executable) { + return checkQueryWithExternalProcess(query, 1, timeout); } else { return checkQueryWithLibrary(query, timeout); } @@ -76,7 +84,7 @@ private boolean checkQueryWithLibrary(String query, int timeout) { return result; } - private boolean checkQueryWithExternalProcess(String query, int timeout) { + private boolean checkQueryWithExternalProcess(String query, int intermediateCheckSatCalls, int timeout) { String result = ""; try { for (int i = 0; i < Z3_RESTART_LIMIT; i++) { @@ -94,6 +102,16 @@ private boolean checkQueryWithExternalProcess(String query, int timeout) { z3Process.getInputStream())); input.write(SMT_PRELUDE + query + "(check-sat)\n"); input.flush(); + input.close(); + for (int ignores = 0; ignores < intermediateCheckSatCalls; ++ignores) { + result = output.readLine(); + if (result == null) { + break; + } + if (globalOptions.debug && !Z3_QUERY_RESULTS.contains(result)) { + break; + } + } result = output.readLine(); z3Process.destroy(); if (result != null) {