java-backend: support SMTLIB translation for KVar binders (#1237)

runtimeverification · Apr 27, 2020 · 0ac45da · 0ac45da
1 parent fb3c282
commit 0ac45da
Show file tree

Hide file tree

Showing 5 changed files with 81 additions and 0 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
@@ -38,6 +38,7 @@
 import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Set;
+import java.util.Stack;
 
 
 public class    KILtoSMTLib extends CopyOnWriteTransformer {
@@ -243,6 +244,7 @@ public static CharSequence translateImplication(
     private final LinkedHashSet<Variable> variables;
     private final LinkedHashMap<Term, Variable> termAbstractionMap;
     private final LinkedHashMap<UninterpretedToken, Integer> tokenEncoding;
+    private final Stack<Term> binders;
 
     private KILtoSMTLib(boolean allowNewVars, GlobalContext global) {
         this(allowNewVars, global.getDefinition(), global.krunOptions, global, new LinkedHashMap<>());
@@ -267,6 +269,7 @@ private KILtoSMTLib(boolean allowNewVars, Definition definition, KRunOptions kru
         this.termAbstractionMap = termAbstractionMap;
         variables = new LinkedHashSet<>();
         tokenEncoding = new LinkedHashMap<>();
+        binders = new Stack<>();
     }
 
     private SMTLibTerm translate(JavaSymbolicObject object) {
@@ -524,6 +527,29 @@ public SMTLibTerm transform(KItem kItem) {
             throw new UnsupportedOperationException();
         }
 
+        if (kLabel.isBinder()) {
+            for (Integer keyIndex : kLabel.getBinderMap().keySet()) {
+                Term binderKVar = kList.get(keyIndex);
+                if (binderKVar instanceof UninterpretedToken && binderKVar.sort() == Sort.KVARIABLE) {
+                    binders.push(binderKVar);
+                } else {
+                    throw new UnsupportedOperationException();
+                }
+            }
+        }
+        SMTLibTerm smtLibTerm = transformSupportedKItem(kItem);
+        if (kLabel.isBinder()) {
+            for (Integer keyIndex : kLabel.getBinderMap().keySet()) {
+                binders.pop();
+            }
+        }
+        return smtLibTerm;
+    }
+
+    private SMTLibTerm transformSupportedKItem(KItem kItem) {
+        KLabelConstant kLabel = (KLabelConstant) kItem.kLabel();
+        KList kList = (KList) kItem.kList();
+
         String label = kLabel.smtlib();
         if (kLabel.label().equals("Map:lookup") && krunOptions.experimental.smt.mapAsIntArray) {
             label = "select";
@@ -656,6 +682,13 @@ public SMTLibTerm transform(BitVector bitVector) {
 
     @Override
     public SMTLibTerm transform(UninterpretedToken uninterpretedToken) {
+        if (uninterpretedToken.sort() == Sort.KVARIABLE) {
+            if (binders.contains(uninterpretedToken)) {
+                return new SMTLibTerm(uninterpretedToken.javaBackendValue());
+            } else {
+                throw new SMTTranslationFailure("unbounded K variable: " + uninterpretedToken);
+            }
+        }
         if (tokenEncoding.get(uninterpretedToken) == null) {
             tokenEncoding.put(uninterpretedToken, tokenEncoding.size());
         }

diff --git a/k-distribution/tests/regression-new/smtlib-forall/Makefile b/k-distribution/tests/regression-new/smtlib-forall/Makefile
@@ -0,0 +1,9 @@
+DEF=a
+EXT=a
+KOMPILE_FLAGS=--syntax-module A
+KOMPILE_BACKEND?=java
+KPROVE_FLAGS=
+
+TESTDIR=.
+
+include ../../../include/ktest.mak
diff --git a/k-distribution/tests/regression-new/smtlib-forall/a-spec.k b/k-distribution/tests/regression-new/smtlib-forall/a-spec.k
@@ -0,0 +1,13 @@
+module A-SPEC
+
+imports A
+
+rule <k> foo(L) => 0 ... </k>
+requires forall(x, L, x >Int 10)
+ ensures forall(x, L, x >Int 0)
+
+rule <k> bar(L1, L2) => 0 ... </k>
+requires forall(x, L1, forall(y, L2, x >Int y))
+ ensures forall(x, L2, forall(y, L1, x <Int y))
+
+endmodule
diff --git a/k-distribution/tests/regression-new/smtlib-forall/a-spec.k.out b/k-distribution/tests/regression-new/smtlib-forall/a-spec.k.out
@@ -0,0 +1 @@
+#True
diff --git a/k-distribution/tests/regression-new/smtlib-forall/a.k b/k-distribution/tests/regression-new/smtlib-forall/a.k
@@ -0,0 +1,25 @@
+require "substitution.k"
+
+module A
+
+imports INT
+imports SUBSTITUTION
+
+syntax Int ::= KVar
+syntax Bool ::= forall(KVar, IntList, Bool) [binder, function, smtlib((forall ((#1 Int)) (=> (inI #1 #2) #3)))]
+rule forall(X, V Vs, E) => E[V / X] andBool forall(X, Vs, E)
+rule forall(_, .IntList, _) => true
+
+syntax IntList ::= List{Int,""}
+syntax Bool ::= Int "inI" IntList [function, smtlib(inI)]
+
+syntax KItem ::= foo(IntList)
+rule foo(L) => 0
+
+syntax KItem ::= bar(IntList, IntList)
+rule bar(L1, L2) => 0
+
+syntax KVar ::= "x" [token]
+              | "y" [token]
+
+endmodule