add methods for escaping and unescaping keywords in Strings.

see #26 for discussion.

Author: kfriedberger

src/org/sosy_lab/java_smt/api/FormulaManager.java

@@ -241,4 +241,18 @@ <T extends Formula> T makeApplication(
    * </ul>
    */
   boolean isValidName(String variableName);
+
+  /**
+   * Get an escaped symbol/name for variables or undefined functions, if necessary.
+   *
+   * <p>See {@link #isValidName(String)} for further details.
+   */
+  String escape(String variableName);
+
+  /**
+   * Get an escaped symbol/name for variables or undefined functions, if necessary.
+   *
+   * <p>See {@link #isValidName(String)} for further details.
+   */
+  String unescape(String variableName);
 }

src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java

@@ -24,12 +24,14 @@
 import com.google.common.annotations.VisibleForTesting;
 import com.google.common.base.CharMatcher;
 import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableBiMap;
 import com.google.common.collect.ImmutableMap;
 import com.google.common.collect.ImmutableSet;
 import java.util.Arrays;
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
+import java.util.Map.Entry;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.Appender;
 import org.sosy_lab.java_smt.api.ArrayFormulaManager;
@@ -93,6 +95,15 @@ public abstract class AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDec
    */
   private static final CharMatcher DISALLOWED_CHARACTERS = CharMatcher.anyOf("|\\");
 
+  /** Mapping of disallowed char to their escaped counterparts. */
+  /* Keep this map in sync with {@link #DISALLOWED_CHARACTERS}.
+   * Counterparts can be any unique string. For optimization we could even use plain chars. */
+  @VisibleForTesting
+  public static final ImmutableBiMap<Character, String> DISALLOWED_CHARACTER_REPLACEMENT =
+      ImmutableBiMap.<Character, String>builder().put('|', "pipe").put('\\', "backslash").build();
+
+  private static final char ESCAPE = '$'; // just some allowed symbol, can be any char
+
   private final @Nullable AbstractArrayFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>
       arrayManager;
 
@@ -455,20 +466,78 @@ public static void checkVariableName(final String variableName) {
     Preconditions.checkArgument(
         !variableName.isEmpty(), "Identifier for variable should not be empty.");
     Preconditions.checkArgument(
-        !AbstractFormulaManager.BASIC_OPERATORS.contains(variableName),
+        !BASIC_OPERATORS.contains(variableName),
         "Identifier '%s' should not be a simple operator. %s",
         variableName,
         help);
     Preconditions.checkArgument(
-        !AbstractFormulaManager.SMTLIB2_KEYWORDS.contains(variableName),
+        !SMTLIB2_KEYWORDS.contains(variableName),
         "Identifier '%s' should not be a keyword of SMT-LIB2. %s",
         variableName,
         help);
     Preconditions.checkArgument(
-        AbstractFormulaManager.DISALLOWED_CHARACTERS.matchesNoneOf(variableName),
+        DISALLOWED_CHARACTERS.matchesNoneOf(variableName),
         "Identifier '%s' should contain an escape character %s of SMT-LIB2. %s",
         variableName,
-        DISALLOWED_CHARACTERS, // toString prints UTF8-encoded escape sequence, better than nothing.
+        DISALLOWED_CHARACTER_REPLACEMENT
+            .keySet(), // toString prints UTF8-encoded escape sequence, better than nothing.
         help);
   }
+
+  /* This escaping works for simple escape sequences only, i.e., keywords are unique enough. */
+  @Override
+  public final String escape(String pVar) {
+    // as long as keywords stay simple, this simple escaping is sufficient
+    if (pVar.isEmpty() || BASIC_OPERATORS.contains(pVar) || SMTLIB2_KEYWORDS.contains(pVar)) {
+      return ESCAPE + pVar;
+    }
+    if (pVar.indexOf(ESCAPE) != -1) {
+      pVar = pVar.replace("" + ESCAPE, "" + ESCAPE + ESCAPE);
+    }
+    if (DISALLOWED_CHARACTERS.matchesAnyOf(pVar)) {
+      for (Entry<Character, String> e : DISALLOWED_CHARACTER_REPLACEMENT.entrySet()) {
+        pVar = pVar.replace(e.getKey().toString(), ESCAPE + e.getValue());
+      }
+    }
+    return pVar; // unchanged
+  }
+
+  /* This unescaping works for simple escape sequences only, i.e., keywords are unique enough. */
+  @Override
+  public final String unescape(String pVar) {
+    int idx = pVar.indexOf(ESCAPE);
+    if (idx != -1) {
+      // unescape BASIC_OPERATORS and SMTLIB2_KEYWORDS
+      if (idx == 0) {
+        String tmp = pVar.substring(1);
+        if (tmp.isEmpty() || BASIC_OPERATORS.contains(tmp) || SMTLIB2_KEYWORDS.contains(tmp)) {
+          return tmp;
+        }
+      }
+
+      // unescape DISALLOWED_CHARACTERS
+      StringBuilder str = new StringBuilder();
+      for (int i = 0; i < pVar.length(); i++) {
+        if (pVar.charAt(i) == ESCAPE) {
+          if (pVar.charAt(i + 1) == ESCAPE) {
+            str.append(ESCAPE);
+            i += 1;
+          } else {
+            String rest = pVar.substring(i + 1);
+            for (Entry<Character, String> e : DISALLOWED_CHARACTER_REPLACEMENT.entrySet()) {
+              if (rest.startsWith(e.getValue())) {
+                str.append(e.getKey());
+                i += e.getValue().length();
+                break;
+              }
+            }
+          }
+        } else {
+          str.append(pVar.charAt(i));
+        }
+      }
+      return str.toString();
+    }
+    return pVar; // unchanged
+  }
 }

src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java

@@ -0,0 +1,50 @@
+/*
+ *  JavaSMT is an API wrapper for a collection of SMT solvers.
+ *  This file is part of JavaSMT.
+ *
+ *  Copyright (C) 2007-2018  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package org.sosy_lab.java_smt.test;
+
+import org.junit.Assert;
+import org.junit.Test;
+
+/** inherits many tests from {@link VariableNamesTest}. */
+public class VariableNamesEscaperTest extends VariableNamesTest {
+
+  @Override
+  boolean allowInvalidNames() {
+    return false;
+  }
+
+  @Override
+  String getVarname() {
+    return mgr.escape(super.getVarname());
+  }
+
+  @Test
+  public void testEscapeUnescape() {
+    String var = super.getVarname();
+    Assert.assertEquals(var, mgr.unescape(mgr.escape(var)));
+  }
+
+  @Test
+  public void testDoubleEscapeUnescape() {
+    String var = getVarname();
+    Assert.assertEquals(var, mgr.unescape(mgr.escape(var)));
+  }
+}

src/org/sosy_lab/java_smt/test/VariableNamesTest.java

@@ -191,6 +191,7 @@ public static List<Object[]> getAllCombinations() {
             .addAll(NAMES)
             .addAll(AbstractFormulaManager.BASIC_OPERATORS)
             .addAll(AbstractFormulaManager.SMTLIB2_KEYWORDS)
+            .addAll(AbstractFormulaManager.DISALLOWED_CHARACTER_REPLACEMENT.values())
             .addAll(FURTHER_SMTLIB2_KEYWORDS)
             .addAll(UNSUPPORTED_NAMES)
             .build();
@@ -209,33 +210,41 @@ protected Solvers solverToUse() {
     return solver;
   }
 
+  boolean allowInvalidNames() {
+    return true;
+  }
+
+  String getVarname() {
+    return varname;
+  }
+
   @CanIgnoreReturnValue
-  private <T extends Formula> T createVariableWith(Function<String, T> creator) {
+  private <T extends Formula> T createVariableWith(Function<String, T> creator, String name) {
     final T result;
-    if (!mgr.isValidName(varname)) {
+    if (allowInvalidNames() && !mgr.isValidName(name)) {
       try {
-        result = creator.apply(varname);
+        result = creator.apply(name);
         fail();
       } catch (IllegalArgumentException e) {
         throw new AssumptionViolatedException("unsupported variable name", e);
       }
     } else {
-      result = creator.apply(varname);
+      result = creator.apply(name);
     }
     return result;
   }
 
   @Test
   public void testBoolVariable() {
-    createVariableWith(bmgr::makeVariable);
+    createVariableWith(bmgr::makeVariable, getVarname());
   }
 
   private <T extends Formula> void testName0(
       Function<String, T> creator, BiFunction<T, T, BooleanFormula> eq, boolean isUF)
       throws SolverException, InterruptedException {
 
     // create a variable
-    T var = createVariableWith(creator);
+    T var = createVariableWith(creator, getVarname());
 
     // check whether it exists with the given name
     Map<String, Formula> map = mgr.extractVariables(var);
@@ -244,10 +253,10 @@ private <T extends Formula> void testName0(
       map = mgr.extractVariablesAndUFs(var);
     }
     assertThat(map).hasSize(1);
-    assertThat(map).containsEntry(varname, var);
+    assertThat(map).containsEntry(getVarname(), var);
 
     // check whether we can create the same variable again
-    T var2 = createVariableWith(creator);
+    T var2 = createVariableWith(creator, getVarname());
     // for simple formulas, we can expect a direct equality
     // (for complex formulas this is not satisfied)
     assertThat(var2).isEqualTo(var);
@@ -265,11 +274,12 @@ private <T extends Formula> void testName0(
     @SuppressWarnings("unused")
     String dump = mgr.dumpFormula(eq.apply(var, var)).toString();
 
-    // try to create a new (!) variable with a different name, the escaped previous name.
-    varname = "|" + varname + "|";
-    @SuppressWarnings("unused")
-    T var3 = createVariableWith(creator);
-    fail();
+    if (allowInvalidNames()) {
+      // try to create a new (!) variable with a different name, the escaped previous name.
+      @SuppressWarnings("unused")
+      T var3 = createVariableWith(creator, "|" + getVarname() + "|");
+      fail();
+    }
   }
 
   @Test
@@ -336,7 +346,7 @@ public void testNameUF2Int() throws SolverException, InterruptedException {
   public void testNameExists() {
     requireQuantifiers();
 
-    IntegerFormula var = createVariableWith(imgr::makeVariable);
+    IntegerFormula var = createVariableWith(imgr::makeVariable, getVarname());
     IntegerFormula zero = imgr.makeNumber(0);
     BooleanFormula exists = qmgr.exists(var, imgr.equal(var, zero));
 
@@ -356,7 +366,7 @@ public Void visitQuantifier(
             for (Formula f : pBoundVariables) {
               Map<String, Formula> map = mgr.extractVariables(f);
               assertThat(map).hasSize(1);
-              assertThat(map).containsEntry(varname, f);
+              assertThat(map).containsEntry(getVarname(), f);
             }
             return null;
           }
@@ -370,7 +380,7 @@ protected Void visitDefault(Formula pF) {
 
   @Test
   public void testBoolVariableNameInVisitor() {
-    BooleanFormula var = createVariableWith(bmgr::makeVariable);
+    BooleanFormula var = createVariableWith(bmgr::makeVariable, getVarname());
 
     bmgr.visit(
         var,
@@ -382,65 +392,66 @@ protected Void visitDefault() {
 
           @Override
           public Void visitAtom(BooleanFormula pAtom, FunctionDeclaration<BooleanFormula> pDecl) {
-            assertThat(pDecl.getName()).isEqualTo(varname);
+            assertThat(pDecl.getName()).isEqualTo(getVarname());
             return null;
           }
         });
   }
 
   @Test
   public void testBoolVariableDump() {
-    BooleanFormula var = createVariableWith(bmgr::makeVariable);
+    BooleanFormula var = createVariableWith(bmgr::makeVariable, getVarname());
     @SuppressWarnings("unused")
     String dump = mgr.dumpFormula(var).toString();
   }
 
   @Test
   public void testEqBoolVariableDump() {
-    BooleanFormula var = createVariableWith(bmgr::makeVariable);
+    BooleanFormula var = createVariableWith(bmgr::makeVariable, getVarname());
     @SuppressWarnings("unused")
     String dump = mgr.dumpFormula(bmgr.equivalence(var, var)).toString();
   }
 
   @Test
   public void testIntVariable() {
-    createVariableWith(imgr::makeVariable);
+    createVariableWith(imgr::makeVariable, getVarname());
   }
 
   @Test
   public void testInvalidRatVariable() {
     requireRationals();
-    createVariableWith(rmgr::makeVariable);
+    createVariableWith(rmgr::makeVariable, getVarname());
   }
 
   @Test
   public void testBVVariable() {
     requireBitvectors();
-    createVariableWith(v -> bvmgr.makeVariable(4, v));
+    createVariableWith(v -> bvmgr.makeVariable(4, v), getVarname());
   }
 
   @Test
   public void testInvalidFloatVariable() {
     requireFloats();
     createVariableWith(
-        v -> fpmgr.makeVariable(v, FormulaType.getSinglePrecisionFloatingPointType()));
+        v -> fpmgr.makeVariable(v, FormulaType.getSinglePrecisionFloatingPointType()),
+        getVarname());
   }
 
   @Test
   public void testArrayVariable() {
     requireArrays();
-    createVariableWith(v -> amgr.makeArray(v, IntegerType, IntegerType));
+    createVariableWith(v -> amgr.makeArray(v, IntegerType, IntegerType), getVarname());
   }
 
   @Test
   public void sameBehaviorTest() {
-    if (mgr.isValidName(varname)) {
+    if (mgr.isValidName(getVarname())) {
       // should pass without exception
-      AbstractFormulaManager.checkVariableName(varname);
+      AbstractFormulaManager.checkVariableName(getVarname());
     } else {
       try {
         // should throw exception
-        AbstractFormulaManager.checkVariableName(varname);
+        AbstractFormulaManager.checkVariableName(getVarname());
         fail();
       } catch (IllegalArgumentException e) {
       }