diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java b/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java index d697fddb34..873508bcf6 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java @@ -29,6 +29,11 @@ public interface FunctionDeclaration { */ String getName(); + /** + * @return List of indices for the function + */ + ImmutableList getIndices(); + /** * @return Sort of the function output. */ diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index 02f1b7281f..8d176adde3 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java @@ -314,5 +314,123 @@ public enum FunctionDeclarationKind { * Solvers support a lot of different built-in theories. We enforce standardization only across a * small subset. */ - OTHER + OTHER; + + public static int getArity(FunctionDeclarationKind pKind) { + // TODO Add missing kinds + switch (pKind) { + case AND: + case OR: + case IFF: + case XOR: + case IMPLIES: + case DISTINCT: + case SUB: + case ADD: + case DIV: + case MUL: + case LT: + case LTE: + case GT: + case GTE: + case EQ: + case BV_CONCAT: + case BV_OR: + case BV_AND: + case BV_XOR: + case BV_SUB: + case BV_ADD: + case BV_MUL: + return -1; + + case NOT: + case UMINUS: + case EQ_ZERO: + case GTE_ZERO: + case FLOOR: + case TO_REAL: + case CONST: + case BV_EXTRACT: + case BV_SIGN_EXTENSION: + case BV_ZERO_EXTENSION: + case BV_NOT: + case BV_NEG: + case BV_ROTATE_LEFT_BY_INT: + case BV_ROTATE_RIGHT_BY_INT: + case FP_NEG: + case FP_ABS: + case FP_IS_NAN: + case FP_IS_INF: + case FP_IS_ZERO: + case FP_IS_NEGATIVE: + case FP_IS_SUBNORMAL: + case FP_IS_NORMAL: + case FP_AS_IEEEBV: + case FP_FROM_IEEEBV: + return 1; + + case SELECT: + case MODULO: + case BV_SDIV: + case BV_UDIV: + case BV_SREM: + case BV_UREM: + case BV_SMOD: + case BV_ULT: + case BV_SLT: + case BV_ULE: + case BV_SLE: + case BV_UGT: + case BV_SGT: + case BV_UGE: + case BV_SGE: + case BV_SHL: + case BV_LSHR: + case BV_ASHR: + case BV_ROTATE_LEFT: + case BV_ROTATE_RIGHT: + case BV_UCASTTO_FP: + case BV_SCASTTO_FP: + case FP_MAX: + case FP_MIN: + case FP_SQRT: + case FP_REM: + case FP_LT: + case FP_LE: + case FP_GE: + case FP_GT: + case FP_EQ: + case FP_ROUND_TO_INTEGRAL: + case FP_CASTTO_FP: + case FP_CASTTO_SBV: + case FP_CASTTO_UBV: + return 2; + + case ITE: + case STORE: + case FP_SUB: + case FP_ADD: + case FP_DIV: + case FP_MUL: + return 3; + + default: + throw new IllegalArgumentException(String.format("Unsupported kind: \"%s\"", pKind)); + } + } + + public static int getNumIndices(FunctionDeclarationKind pKind) { + // TODO Add missing kinds + switch (pKind) { + case BV_ROTATE_LEFT_BY_INT: + case BV_ROTATE_RIGHT_BY_INT: + case BV_SIGN_EXTENSION: + case BV_ZERO_EXTENSION: + return 1; + case BV_EXTRACT: + return 2; + default: + return 0; + } + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java b/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java index 5b276cfa64..5ccb34d291 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java @@ -26,11 +26,26 @@ public abstract class FunctionDeclarationImpl public static FunctionDeclaration of( String name, FunctionDeclarationKind kind, + List pIndices, List> pArgumentTypes, FormulaType pReturnType, T pDeclaration) { return new AutoValue_FunctionDeclarationImpl<>( - kind, name, pReturnType, ImmutableList.copyOf(pArgumentTypes), pDeclaration); + kind, + name, + ImmutableList.copyOf(pIndices), + pReturnType, + ImmutableList.copyOf(pArgumentTypes), + pDeclaration); + } + + public static FunctionDeclaration of( + String name, + FunctionDeclarationKind kind, + List> pArgumentTypes, + FormulaType pReturnType, + T pDeclaration) { + return of(name, kind, ImmutableList.of(), pArgumentTypes, pReturnType, pDeclaration); } /** diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index 1809f4f8ff..8dece6ff17 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -494,7 +494,12 @@ public R visit(FormulaVisitor visitor, Formula formula, Term f) formula, arguments.build(), FunctionDeclarationImpl.of( - name, getDeclarationKind(f), argumentTypes.build(), getFormulaType(f), decl)); + name, + getDeclarationKind(f), + ImmutableList.copyOf(f.indices()), + argumentTypes.build(), + getFormulaType(f), + decl)); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 8357c223b6..f2833dc817 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -449,6 +449,9 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { } else if (f.getKind() == Kind.CONSTANT) { return visitor.visitFreeVariable(formula, dequote(f.toString())); + } else if (f.getKind() == Kind.SEP_NIL) { + return visitor.visitConstant(formula, null); + } else if (f.getKind() == Kind.APPLY_CONSTRUCTOR) { Preconditions.checkState( f.getNumChildren() == 1, "Unexpected formula '%s' with sort '%s'", f, f.getSort()); @@ -463,7 +466,17 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { List> argsTypes = new ArrayList<>(); - // Term operator = normalize(f.getSort()); + // Collect indices + Op operator = f.getOp(); + ImmutableList.Builder indexBuilder = ImmutableList.builder(); + for (int p = 0; p < operator.getNumIndices(); p++) { + Term index = operator.get(p); + if (index.isIntegerValue()) { + indexBuilder.add(index.getIntegerValue().intValueExact()); + } + } + + // Collect arguments Kind kind = f.getKind(); if (sort.isFunction() || kind == Kind.APPLY_UF) { // The arguments are all children except the first one @@ -479,10 +492,6 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { } } - // TODO some operations (BV_SIGN_EXTEND, BV_ZERO_EXTEND, maybe more) encode information as - // part of the operator itself, thus the arity is one too small and there might be no - // possibility to access the information from user side. Should we encode such information - // as additional parameters? We do so for some methods of Princess. if (sort.isFunction()) { return visitor.visitFunction( formula, @@ -505,7 +514,12 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { formula, argsBuilder.build(), FunctionDeclarationImpl.of( - getName(f), getDeclarationKind(f), argsTypes, getFormulaType(f), normalize(f))); + getName(f), + getDeclarationKind(f), + indexBuilder.build(), + argsTypes, + getFormulaType(f), + normalize(f))); } } } catch (CVC5ApiException e) { diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java index 4a56eb58ee..6ab0b2230f 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -119,6 +119,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_repr; import com.google.common.base.Preconditions; +import com.google.common.base.Splitter; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import com.google.common.primitives.Longs; @@ -369,6 +370,18 @@ && msat_is_enum_type(environment, msat_term_get_type(f))) { return visitor.visitFreeVariable(formula, name); } + // Collect indices: We need to extract them from the term name in MathSAT + FunctionDeclarationKind kind = getDeclarationKind(f); + List tokens = + Splitter.on('_') + .splitToList(name.startsWith("`") ? name.substring(1, name.length() - 1) : name); + + ImmutableList.Builder indices = ImmutableList.builder(); + for (int p = 1; p <= FunctionDeclarationKind.getNumIndices(kind); p++) { + indices.add(Integer.valueOf(tokens.get(p))); + } + + // Now collect the arguments ImmutableList.Builder args = ImmutableList.builder(); ImmutableList.Builder> argTypes = ImmutableList.builder(); for (int i = 0; i < arity; i++) { @@ -386,7 +399,8 @@ && msat_is_enum_type(environment, msat_term_get_type(f))) { args.build(), FunctionDeclarationImpl.of( name, - getDeclarationKind(f), + kind, + indices.build(), argTypes.build(), getFormulaType(f), msat_term_get_decl(f))); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index 40aeaecb00..ac4539f504 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/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,7 @@ import ap.parser.IFunApp; import ap.parser.IFunction; import ap.parser.IIntFormula; +import ap.parser.IIntLit; import ap.parser.IPlus; import ap.parser.ITerm; import ap.parser.ITermITE; @@ -581,6 +583,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()); + } 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 { diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 6f325cb173..5827f0a5c2 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -396,6 +396,44 @@ private static boolean isValue(IExpression input) { public R visit(FormulaVisitor visitor, final Formula f, final IExpression input) { if (isValue(input)) { return visitor.visitConstant(f, convertValue(input)); + } else if (input instanceof IFunApp + && ((IFunApp) input).fun().equals(ModuloArithmetic.bv_extract())) { + var kind = FunctionDeclarationKind.BV_EXTRACT; + var upper = ((IIntLit) input.apply(0)).value().intValue(); + var lower = ((IIntLit) input.apply(1)).value().intValue(); + var arg = input.apply(2); + var argType = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg); + + return visitor.visitFunction( + f, + ImmutableList.of(encapsulateWithTypeOf(arg)), + FunctionDeclarationImpl.of( + kind.toString(), + kind, + ImmutableList.of(upper, lower), + ImmutableList.of(argType), + FormulaType.getBitvectorTypeWithSize(upper - lower), + new PrincessFunctionDeclaration.PrincessBitvectorExtractDeclaration(upper, lower))); + + } else if (input instanceof IFunApp + && ((IFunApp) input).fun().equals(ModuloArithmetic.bv_concat())) { + var kind = FunctionDeclarationKind.BV_CONCAT; + var size1 = ((IIntLit) input.apply(0)).value().intValue(); + var size2 = ((IIntLit) input.apply(1)).value().intValue(); + var arg1 = input.apply(2); + var arg2 = input.apply(3); + var arg1Type = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg1); + var arg2Type = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg2); + + return visitor.visitFunction( + f, + ImmutableList.of(encapsulateWithTypeOf(arg1), encapsulateWithTypeOf(arg2)), + FunctionDeclarationImpl.of( + kind.toString(), + kind, + ImmutableList.of(arg1Type, arg2Type), + FormulaType.getBitvectorTypeWithSize(size1 + size2), + new PrincessFunctionDeclaration.PrincessBitvectorConcatDeclaration())); } else if (input instanceof IQuantified) { return visitQuantifier(visitor, (BooleanFormula) f, (IQuantified) input); @@ -469,16 +507,13 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression return visit(visitor, f, ((IIntFormula) input).t()); } - ImmutableList.Builder args = ImmutableList.builder(); - ImmutableList.Builder> argTypes = ImmutableList.builder(); - int arity = input.length(); - int arityStart = 0; + int numSortParameters = getNumSortParameters(kind); + int numIndices = FunctionDeclarationKind.getNumIndices(kind); PrincessFunctionDeclaration solverDeclaration; - if (isBitvectorOperationWithAdditionalArgument(kind)) { + if (numSortParameters > 0) { // the first argument is the bitsize, and it is not relevant for the user. // we do not want type/sort information as arguments. - arityStart = 1; if (input instanceof IAtom) { solverDeclaration = new PrincessBitvectorToBooleanDeclaration(((IAtom) input).pred()); } else if (input instanceof IFunApp) { @@ -499,7 +534,17 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression solverDeclaration = new PrincessByExampleDeclaration(input); } - for (int i = arityStart; i < arity; i++) { + ImmutableList.Builder indices = ImmutableList.builder(); + + for (int i = numSortParameters; i < numSortParameters + numIndices; i++) { + IExpression term = input.apply(i); + indices.add(((IIntLit) term).value().intValue()); + } + + ImmutableList.Builder args = ImmutableList.builder(); + ImmutableList.Builder> argTypes = ImmutableList.builder(); + + for (int i = numSortParameters + numIndices; i < input.length(); i++) { IExpression arg = input.apply(i); FormulaType argumentType = getFormulaType(arg); args.add(encapsulate(argumentType, arg)); @@ -510,7 +555,12 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression f, args.build(), FunctionDeclarationImpl.of( - getName(input), kind, argTypes.build(), getFormulaType(f), solverDeclaration)); + getName(input), + kind, + indices.build(), + argTypes.build(), + getFormulaType(f), + solverDeclaration)); } private R visitQuantifier(FormulaVisitor visitor, BooleanFormula f, IQuantified input) { @@ -550,7 +600,8 @@ private String getFreshVariableNameForBody(IFormula body) { body, k -> "__JAVASMT__BOUND_VARIABLE_" + boundVariableNames.size()); } - private boolean isBitvectorOperationWithAdditionalArgument(FunctionDeclarationKind kind) { + private int getNumSortParameters(FunctionDeclarationKind kind) { + // TODO Check that his is still right switch (kind) { case BV_NOT: case BV_NEG: @@ -574,9 +625,14 @@ private boolean isBitvectorOperationWithAdditionalArgument(FunctionDeclarationKi case BV_UGE: case BV_SGE: case BV_EQ: - return true; + case BV_LSHR: + case BV_ASHR: + case BV_SHL: + return 1; + case BV_CONCAT: + return 2; default: - return false; + return 0; } } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java index 670d2f1521..d33dae2d7c 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -24,6 +24,7 @@ import ap.parser.ITermITE; import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; +import ap.theories.bitvectors.ModuloArithmetic$; import ap.theories.nia.GroebnerMultiplication; import ap.types.MonoSortedIFunction; import ap.types.Sort; @@ -236,4 +237,31 @@ public IExpression makeApp(PrincessEnvironment env, List args) { return GroebnerMultiplication.mult((ITerm) args.get(0), (ITerm) args.get(1)); } } + + static class PrincessBitvectorExtractDeclaration extends PrincessFunctionDeclaration { + private final int upper; + private final int lower; + + PrincessBitvectorExtractDeclaration(int pUpper, int pLower) { + upper = pUpper; + lower = pLower; + } + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + return ModuloArithmetic$.MODULE$.extract(upper, lower, (ITerm) args.get(0)); + } + } + + static class PrincessBitvectorConcatDeclaration extends PrincessFunctionDeclaration { + + PrincessBitvectorConcatDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + return ModuloArithmetic$.MODULE$.concat((ITerm) args.get(0), (ITerm) args.get(1)); + } + } } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index 0f9fdc558c..172e5c61ea 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -23,6 +23,7 @@ import com.microsoft.z3.Z3Exception; import com.microsoft.z3.enumerations.Z3_ast_kind; import com.microsoft.z3.enumerations.Z3_decl_kind; +import com.microsoft.z3.enumerations.Z3_param_kind; import com.microsoft.z3.enumerations.Z3_sort_kind; import com.microsoft.z3.enumerations.Z3_symbol_kind; import java.lang.ref.PhantomReference; @@ -527,7 +528,8 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long return visitor.visitConstant(formula, convertValue(f)); case Z3_APP_AST: int arity = Native.getAppNumArgs(environment, f); - int declKind = Native.getDeclKind(environment, Native.getAppDecl(environment, f)); + long decl = Native.getAppDecl(environment, f); + int declKind = Native.getDeclKind(environment, decl); if (arity == 0) { // constants @@ -573,6 +575,14 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long } } + ImmutableList.Builder indexBuilder = ImmutableList.builder(); + for (int p = 0; p < Native.getDeclNumParameters(environment, decl); p++) { + int kind = Native.getDeclParameterKind(environment, decl, p); + if (kind == Z3_param_kind.Z3_PK_UINT.toInt()) { + indexBuilder.add(Native.getDeclIntParameter(environment, decl, p)); + } + } + // Function application with zero or more parameters ImmutableList.Builder args = ImmutableList.builder(); ImmutableList.Builder> argTypes = ImmutableList.builder(); @@ -588,6 +598,7 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long FunctionDeclarationImpl.of( getAppName(f), getDeclarationKind(f), + indexBuilder.build(), argTypes.build(), getFormulaType(f), Native.getAppDecl(environment, f)));