Back translation for Princess rewrites

src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java

@@ -13,11 +13,10 @@
 import ap.parser.ITerm;
 import ap.theories.bitvectors.ModuloArithmetic$;
 import ap.types.Sort;
-import ap.types.Sort$;
-import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableList;
 import java.math.BigInteger;
 import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager;
-import scala.Option;
+import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorToIntegerDeclaration;
 
 class PrincessBitvectorFormulaManager
     extends AbstractBitvectorFormulaManager<
@@ -137,29 +136,11 @@ protected IExpression makeBitvectorImpl(int pLength, IExpression pIntegerFormula
 
   @Override
   protected IExpression toIntegerFormulaImpl(IExpression pBVFormula, boolean signed) {
-    final Sort sort = Sort$.MODULE$.sortOf((ITerm) pBVFormula);
-    final Option<Object> bitWidth = PrincessEnvironment.getBitWidth(sort);
-    Preconditions.checkArgument(bitWidth.isDefined());
-    final int size = (Integer) bitWidth.get();
-
-    // compute range for integer value,
-    // example: bitWidth=4 => signed_range=[-8;7] and unsigned_range=[0;15]
-    final BigInteger min;
-    final BigInteger max;
-    if (signed) {
-      min = BigInteger.ONE.shiftLeft(size - 1).negate();
-      max = BigInteger.ONE.shiftLeft(size - 1).subtract(BigInteger.ONE);
-    } else {
-      min = BigInteger.ZERO;
-      max = BigInteger.ONE.shiftLeft(size).subtract(BigInteger.ONE);
-    }
-
-    ITerm bvInRange =
-        ModuloArithmetic$.MODULE$.cast2Interval(
-            IdealInt.apply(min), IdealInt.apply(max), (ITerm) pBVFormula);
-
-    // Princess can not directly convert from BV to INT. However, adding zero helps. Ugly.
-    return IExpression.i(0).$plus(bvInRange);
+    var decl =
+        signed
+            ? PrincessBitvectorToIntegerDeclaration.SIGNED
+            : PrincessBitvectorToIntegerDeclaration.UNSIGNED;
+    return decl.makeApp(getFormulaCreator().getEnv(), ImmutableList.of(pBVFormula));
   }
 
   @Override
@@ -194,10 +175,8 @@ protected IExpression extract(IExpression pNumber, int pMsb, int pLsb) {
 
   @Override
   protected IExpression extend(IExpression pNumber, int pExtensionBits, boolean pSigned) {
-    if (pSigned) {
-      return ModuloArithmetic$.MODULE$.sign_extend(pExtensionBits, (ITerm) pNumber);
-    } else {
-      return ModuloArithmetic$.MODULE$.zero_extend(pExtensionBits, (ITerm) pNumber);
-    }
+    return new PrincessFunctionDeclaration.PrincessBitvectorExtendDeclaration(
+            pExtensionBits, pSigned)
+        .makeApp(getFormulaCreator().getEnv(), ImmutableList.of(pNumber));
   }
 }

src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java

@@ -12,6 +12,7 @@
 import static scala.collection.JavaConverters.collectionAsScalaIterableConverter;
 
 import ap.api.SimpleAPI;
+import ap.basetypes.IdealInt;
 import ap.parameters.GlobalSettings;
 import ap.parser.BooleanCompactifier;
 import ap.parser.Environment.EnvironmentException;
@@ -22,6 +23,8 @@
 import ap.parser.IFunApp;
 import ap.parser.IFunction;
 import ap.parser.IIntFormula;
+import ap.parser.IIntLit;
+import ap.parser.IIntRelation;
 import ap.parser.IPlus;
 import ap.parser.ITerm;
 import ap.parser.ITermITE;
@@ -33,7 +36,6 @@
 import ap.parser.SMTTypes.SMTType;
 import ap.terfor.ConstantTerm;
 import ap.terfor.preds.Predicate;
-import ap.theories.arrays.ExtArray;
 import ap.theories.arrays.ExtArray.ArraySort;
 import ap.theories.bitvectors.ModuloArithmetic;
 import ap.theories.rationals.Rationals$;
@@ -53,8 +55,6 @@
 import java.io.File;
 import java.io.IOException;
 import java.io.StringReader;
-import java.lang.reflect.InvocationTargetException;
-import java.lang.reflect.Method;
 import java.nio.file.Path;
 import java.util.ArrayDeque;
 import java.util.ArrayList;
@@ -176,6 +176,8 @@ class PrincessEnvironment {
 
   private final Map<String, IFunction> functionsCache = new HashMap<>();
 
+  private final Map<FormulaType<?>, Map<ITerm, ITerm>> constArrayCache = new HashMap<>();
+
   private final int randomSeed;
   private final @Nullable PathCounterTemplate basicLogfile;
   private final ShutdownNotifier shutdownNotifier;
@@ -337,6 +339,15 @@ public List<? extends IExpression> parseStringToTerms(String s, PrincessFormulaC
         IFunction fun = ((IFunApp) var).fun();
         functionsCache.put(fun.name(), fun);
         addFunction(fun);
+      } else if (var instanceof IIntFormula
+          && ((IIntFormula) var).rel().equals(IIntRelation.EqZero())
+          && ((IIntFormula) var).apply(0) instanceof IFunApp) {
+        // Functions with return type Bool are wrapped in a predicate as (=0 (uf ...))
+        IFunction fun = ((IFunApp) var.apply(0)).fun();
+        functionsCache.put(fun.name(), fun);
+        addFunction(fun);
+      } else {
+        throw new IllegalArgumentException();
       }
     }
     return formulas;
@@ -581,6 +592,18 @@ static FormulaType<?> getFormulaType(IExpression pFormula) {
       FormulaType<?> t1 = getFormulaType(plus.left());
       FormulaType<?> t2 = getFormulaType(plus.right());
       return mergeFormulaTypes(t1, t2);
+    } else if (pFormula instanceof IFunApp
+        && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_extract())) {
+      IIntLit upper = (IIntLit) pFormula.apply(0);
+      IIntLit lower = (IIntLit) pFormula.apply(1);
+      IdealInt bwResult = upper.value().$minus(lower.value());
+      return FormulaType.getBitvectorTypeWithSize(bwResult.intValue() + 1);
+    } else if (pFormula instanceof IFunApp
+        && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_concat())) {
+      IIntLit upper = (IIntLit) pFormula.apply(0);
+      IIntLit lower = (IIntLit) pFormula.apply(1);
+      IdealInt bwResult = upper.value().$plus(lower.value());
+      return FormulaType.getBitvectorTypeWithSize(bwResult.intValue());
     } else {
       final Sort sort = Sort$.MODULE$.sortOf((ITerm) pFormula);
       try {
@@ -669,7 +692,14 @@ public IExpression makeVariable(Sort type, String varname) {
       }
     } else {
       if (sortedVariablesCache.containsKey(varname)) {
-        return sortedVariablesCache.get(varname);
+        ITerm found = sortedVariablesCache.get(varname);
+        Preconditions.checkArgument(
+            getFormulaType(found).equals(getFormulaTypeFromSort(type)),
+            "Can't declare variable \"%s\" with type %s. It has already been declared with type %s",
+            varname,
+            getFormulaTypeFromSort(type),
+            getFormulaType(found));
+        return found;
       } else {
         ITerm var = api.createConstant(varname, type);
         addSymbol(var);
@@ -682,6 +712,7 @@ public IExpression makeVariable(Sort type, String varname) {
   /** This function declares a new functionSymbol with the given argument types and result. */
   public IFunction declareFun(String name, Sort returnType, List<Sort> args) {
     if (functionsCache.containsKey(name)) {
+      // FIXME Check that the old declaration has the right type
       return functionsCache.get(name);
     } else {
       IFunction funcDecl =
@@ -705,20 +736,32 @@ public ITerm makeStore(ITerm array, ITerm index, ITerm value) {
     return new IFunApp(arraySort.theory().store(), toSeq(args));
   }
 
-  public ITerm makeConstArray(ArraySort arraySort, ITerm elseTerm) {
-    // return new IFunApp(arraySort.theory().const(), elseTerm); // I love Scala! So simple! ;-)
-
-    // Scala uses keywords that are illegal in Java. Thus, we use reflection to access the method.
-    // TODO we should contact the developers of Princess and ask for a renaming.
-    final IFunction constArrayOp;
-    try {
-      Method constMethod = ExtArray.class.getMethod("const");
-      constArrayOp = (IFunction) constMethod.invoke(arraySort.theory());
-    } catch (IllegalAccessException | NoSuchMethodException | InvocationTargetException exception) {
-      throw new RuntimeException(exception);
-    }
+  void cacheConstArray(ArraySort arraySort, ITerm elseTerm, ITerm constArray) {
+    constArrayCache.compute(
+        getFormulaTypeFromSort(arraySort),
+        (sort, maps) -> {
+          if (maps == null) {
+            maps = new HashMap<>();
+          }
+          maps.putIfAbsent(elseTerm, constArray);
+          return maps;
+        });
+  }
 
-    return new IFunApp(constArrayOp, toSeq(ImmutableList.of(elseTerm)));
+  public ITerm makeConstArray(ArraySort arraySort, ITerm elseTerm) {
+    constArrayCache.compute(
+        getFormulaTypeFromSort(arraySort),
+        (sort, maps) -> {
+          if (maps == null) {
+            maps = new HashMap<>();
+          }
+          maps.computeIfAbsent(
+              elseTerm,
+              term ->
+                  new IFunApp(arraySort.theory().constArray(), toSeq(ImmutableList.of(elseTerm))));
+          return maps;
+        });
+    return constArrayCache.get(getFormulaTypeFromSort(arraySort)).get(elseTerm);
   }
 
   public boolean hasArrayType(IExpression exp) {