diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java index 722fcaf05f..83b5f4e486 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java @@ -9,21 +9,21 @@ package org.sosy_lab.java_smt.solvers.bitwuzla; import com.google.common.base.Preconditions; +import com.google.common.collect.FluentIterable; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Collection; import java.util.Deque; -import java.util.HashSet; import java.util.List; -import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.java_smt.basicimpl.AbstractModel; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Kind; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Sort; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Term; +import org.sosy_lab.java_smt.solvers.bitwuzla.api.TermManager; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Term; class BitwuzlaModel extends AbstractModel { @@ -82,7 +82,7 @@ public ImmutableList asList() { variablesBuilder.add(getSimpleAssignment(term)); } else if (sort.is_array() && term.is_const()) { - variablesBuilder.addAll(getArrayAssignment(term)); + variablesBuilder.addAll(buildArrayAssignment(term, bitwuzlaEnv.get_value(term))); } else { for (Term child : children) { @@ -108,94 +108,95 @@ private ValueAssignment getSimpleAssignment(Term pTerm) { argumentInterpretation); } - private Collection getArrayAssignment(Term pTerm) { - return getArrayAssignments(pTerm, ImmutableList.of()); + /** Takes a (nested) select statement and returns its indices. */ + private Iterable getArgs(Term array) { + if (array.kind().equals(Kind.ARRAY_SELECT)) { + return FluentIterable.concat(getArgs(array.get(0)), ImmutableList.of(array.get(1))); + } else { + return ImmutableList.of(); + } } - // TODO: check this in detail. I think this might be incomplete. - // We should add more Model tests in general. As most are parsing and int based! - private Collection getArrayAssignments(Term pTerm, List upperIndices) { - // Array children for store are structured in the following way: - // {starting array, index, value} in "we add value at index to array" - // Selections are structured: {starting array, index} - // Just declared (empty) arrays return an empty array - - // Example Formula: (SELECT ARRAY INDEX) - // new ValueAssignment((SELECT ARRAY INDEX), value formula of INDEX, (SELECT ARRAY INDEX) = - // value of index, name of INDEX, actual java value of index, {return java value of the - // formula}) - - // TODO: Array equals value - Term array = pTerm; - Collection assignments = new ArrayList<>(); - Set indices = new HashSet<>(); - while (array.sort().is_array()) { - // Here we either have STORE; SELECT or an empty Array - Vector_Term children = array.children(); - List innerIndices = new ArrayList<>(upperIndices); - String name = getArrayName(array); - Preconditions.checkNotNull(name, "unexpected array %s without name", array); - if (children.isEmpty()) { - // Empty array - return assignments; - } else if (children.size() == 2) { - // SELECT expression - Term index = children.get(1); - if (!indices.add(index)) { - continue; - } - - Term indexValue = bitwuzlaEnv.get_value(index); - innerIndices.add(evaluateImpl(indexValue)); - - // The value of an SELECT is equal to the content - Term valueTerm = bitwuzlaEnv.get_value(array); - - assignments.add( - new ValueAssignment( - bitwuzlaCreator.encapsulateWithTypeOf(array), - bitwuzlaCreator.encapsulateWithTypeOf(valueTerm), - creator.encapsulateBoolean(buildEqForTwoTerms(array, valueTerm)), - name, - evaluateImpl(valueTerm), - innerIndices)); - array = children.get(0); - - } else { - // STORE expression - assert children.size() == 3; - Term index = children.get(1); - Term content = children.get(2); - - if (!indices.add(index)) { - continue; - } - - Term indexValue = bitwuzlaEnv.get_value(index); - Term contentValue = bitwuzlaEnv.get_value(content); - innerIndices.add(evaluateImpl(indexValue)); - assignments.add( - new ValueAssignment( - bitwuzlaCreator.encapsulateWithTypeOf(array), - bitwuzlaCreator.encapsulateWithTypeOf(content), - creator.encapsulateBoolean(buildEqForTwoTerms(array, contentValue)), - name, - evaluateImpl(contentValue), - innerIndices)); - - array = children.get(0); - assignments.addAll(getArrayAssignments(array, innerIndices)); - } + /** Takes a select statement with multiple indices and returns the variable name at the bottom. */ + private String getVar(Term array) { + if (array.kind().equals(Kind.ARRAY_SELECT)) { + return getVar(array.get(0)); + } else { + return array.symbol(); } - return assignments; } - private String getArrayName(Term array) { - String name = array.symbol(); - if (name != null) { - return name; + /** Build assignment for an array value. */ + private Iterable buildArrayAssignment(Term expr, Term value) { + // Bitwuzla returns values such as "(Store (Store ... i1,1 e1,1) i1,0 e1,0)" where the i1,x + // match the first index of the array and the elements e1,Y can again be arrays (if there is + // more than one index). We need "pattern match" this values to extract assignments from it. + // Initially we have: + // arr = (Store (Store ... i1,1 e1,1) i1,0 e1,0) + // where 'arr' is the name of the variable. By applying (Select i1,0 ...) to both side we get: + // (Select i1,0 arr) = (Select i1,0 (Store (Store ... i1,1 e1,1) i1,0 e1,0)) + // The right side simplifies to e1,0 as the index matches. We need to continue with this for + // all other matches to the first index, that is + // (Select i1,1 arr) = (Select i1,0 (Store (Store ... i1,1 e1,1) i1,0 e1,0)) + // = (Select i1,0 (Store ... i1,1 e1,1)) + // = e1,1 + // until all matches are explored and the bottom of the Store chain is reached. If the array + // has more than one dimension we also have to descend into the elements to apply the next + // index there. For instance, let's consider a 2-dimensional array with type (Array Int -> + // (Array Int -> Int)). After matching the first index just as in the above example we might + // have: + // (Select i1,0 arr) = (Select i1,0 (Store (Store ... i1,1 e1,1) i1,0 e1,0)) = e1,0 + // In this case e1,0 is again a Store chain, let's say e1,0 := (Store (Store ... i2,1 e2,1) + // i2,0 e2,0), and we now continue with the second index: + // (Select i2,1 (Select i1,0 arr)) = (Select i2,1 (Store (Store ... i2,1 e2,1) i2,0 e2,0)) = + // = e2,1 + // This again has to be done for all possible matches. + // Once we've reached the last index, the successor element will be a non-array value. We + // then create the final assignments and return: + // (Select iK,mK ... (Select i2,1 (Select i1,0 arr)) = eik,mK + if (value.kind().equals(Kind.ARRAY_STORE)) { + // This is a Store node for the current index. We need to follow the chain downwards to + // match this index, while also exploring the successor for the other indices + Term index = value.get(1); + Term element = value.get(2); + + TermManager termManager = bitwuzlaCreator.getTermManager(); + Term select = termManager.mk_term(Kind.ARRAY_SELECT, expr, index); + + Iterable current; + if (expr.sort().array_element().is_array()) { + current = buildArrayAssignment(select, element); + } else { + Term equation = termManager.mk_term(Kind.EQUAL, select, element); + + current = + FluentIterable.of( + new ValueAssignment( + creator.encapsulate(creator.getFormulaType(element), select), + creator.encapsulate(creator.getFormulaType(element), element), + creator.encapsulateBoolean(equation), + getVar(expr), + creator.convertValue(element, element), + FluentIterable.from(getArgs(select)) + .transform(creator::convertValue) + .toList())); + } + return FluentIterable.concat(current, buildArrayAssignment(expr, value.get(0))); + + } else if (value.kind().equals(Kind.CONST_ARRAY)) { + // We've reached the end of the Store chain + return ImmutableList.of(); + + } else { + // Should be unreachable + // We assume that array values are made up of "const" and "store" nodes with non-array + // constants as leaves + throw new AssertionError( + String.format( + "Can't process model value for variable '%s'. Please report this issue to the " + + "JavaSMT developers", + getVar(expr))); } - return getArrayName(array.get(0)); } private Term buildEqForTwoTerms(Term left, Term right) { diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 40213bd4e0..d35ae7f11e 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -16,7 +16,9 @@ import static org.sosy_lab.java_smt.api.FormulaType.IntegerType; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; +import com.google.common.collect.FluentIterable; import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; import com.google.common.collect.Iterables; import java.io.IOException; import java.math.BigInteger; @@ -24,6 +26,7 @@ import java.nio.file.Path; import java.util.ArrayList; import java.util.List; +import java.util.Map; import java.util.function.Function; import java.util.stream.Collectors; import org.checkerframework.checker.nullness.qual.Nullable; @@ -42,6 +45,7 @@ import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.FunctionDeclarationKind; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; @@ -49,6 +53,7 @@ import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; /** Test that values from models are appropriately parsed. */ public class ModelTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @@ -2243,7 +2248,7 @@ public void arrayTest5() assume() .withMessage("Solver is quite slow for this example") .that(solverToUse()) - .isNotEqualTo(Solvers.PRINCESS); + .isNoneOf(Solvers.PRINCESS, Solvers.BITWUZLA); BooleanFormula formula = context @@ -2254,6 +2259,312 @@ public void arrayTest5() checkModelIteration(formula, false); } + /** Returns the arguments of an UF or array definition from the model. */ + private Iterable getFunctionArgs(Formula pValue) { + requireVisitor(); + return mgr.visit( + pValue, + new DefaultFormulaVisitor<>() { + @Override + protected Iterable visitDefault(Formula f) { + throw new IllegalArgumentException(); + } + + @Override + public Iterable visitFreeVariable(Formula f, String name) { + // Base case for array values + return ImmutableList.of(); + } + + @Override + public Iterable visitFunction( + Formula f, List args, FunctionDeclaration functionDeclaration) { + if (functionDeclaration.getKind().equals(FunctionDeclarationKind.SELECT)) { + return FluentIterable.concat( + getFunctionArgs(args.get(0)), ImmutableList.of(args.get(1))); + } else { + // Assume its an UF value + return args; + } + } + }); + } + + /** Evaluate the UF or array constraint and check that the model contains the expected values. */ + private void checkModelContains( + BooleanFormula pFormula, String pVar, Map, Formula> expected) { + requireArrayModel(); + + try (var prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + prover.addConstraint(pFormula); + assertThat(prover.isUnsat()).isFalse(); + + ImmutableMap.Builder, Formula> builder = ImmutableMap.builder(); + try (var model = prover.getModel()) { + for (var assignment : model.asList()) { + if (assignment.getName().equals(pVar)) { + builder.put( + ImmutableList.copyOf(getFunctionArgs(assignment.getKey())), + assignment.getValueAsFormula()); + } + } + } + var model = builder.buildOrThrow(); + assertThat(model).containsAtLeastEntriesIn(expected); + + } catch (SolverException | InterruptedException e) { + throw new RuntimeException(e); + } + } + + @Test + public void testArray1Bv() { + requireArrays(); + requireBitvectors(); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var array = amgr.makeArray("array", bitvectorType, bitvectorType); + + var idx = bvmgr.makeBitvector(8, 1); + var val = bvmgr.makeBitvector(8, 10); + + checkModelContains( + bvmgr.equal(amgr.select(array, idx), val), + "array", + ImmutableMap.of(ImmutableList.of(idx), val)); + } + + @Test + public void testArray2Bv() { + requireArrays(); + requireBitvectors(); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var array = amgr.makeArray("array", bitvectorType, bitvectorType); + + var idxA = bvmgr.makeBitvector(8, 1); + var valA = bvmgr.makeBitvector(8, 10); + + var idxB = bvmgr.makeBitvector(8, 2); + var valB = bvmgr.makeBitvector(8, 5); + + checkModelContains( + bmgr.and( + bvmgr.equal(amgr.select(array, idxA), valA), + bvmgr.equal(amgr.select(array, idxB), valB)), + "array", + ImmutableMap.of(ImmutableList.of(idxA), valA, ImmutableList.of(idxB), valB)); + } + + @Test + public void testArray1BvBV() { + requireArrays(); + requireBitvectors(); + + // Boolector doesn't support multiple indices + assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var array = + amgr.makeArray( + "array", bitvectorType, FormulaType.getArrayType(bitvectorType, bitvectorType)); + + var idxA = bvmgr.makeBitvector(8, 1); + var idxB = bvmgr.makeBitvector(8, 7); + var val = bvmgr.makeBitvector(8, 10); + + checkModelContains( + bvmgr.equal(amgr.select(amgr.select(array, idxA), idxB), val), + "array", + ImmutableMap.of(ImmutableList.of(idxA, idxB), val)); + } + + @Test + public void testArray2BvBv() { + requireArrays(); + requireBitvectors(); + + // Boolector doesn't support multiple indices + assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var array = + amgr.makeArray( + "array", bitvectorType, FormulaType.getArrayType(bitvectorType, bitvectorType)); + + var idxA1 = bvmgr.makeBitvector(8, 1); + var idxA2 = bvmgr.makeBitvector(8, 7); + var valA = bvmgr.makeBitvector(8, 10); + + var idxB1 = bvmgr.makeBitvector(8, 3); + var idxB2 = bvmgr.makeBitvector(8, 2); + var valB = bvmgr.makeBitvector(8, 5); + + checkModelContains( + bmgr.and( + bvmgr.equal(amgr.select(amgr.select(array, idxA1), idxA2), valA), + bvmgr.equal(amgr.select(amgr.select(array, idxB1), idxB2), valB)), + "array", + ImmutableMap.of( + ImmutableList.of(idxA1, idxA2), valA, ImmutableList.of(idxB1, idxB2), valB)); + } + + @Test + public void testArrayStore1BvBvBv() { + // Test for 3d bitvector arrays with exactly one element + // array = (Store (const ...) idxA (Store (const ..) idxB (Store (const ...) idx C val)) + requireArrays(); + requireBitvectors(); + + // Boolector doesn't support multiple indices + assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); + + var scalarType = FormulaType.getBitvectorTypeWithSize(8); + + var array1Type = FormulaType.getArrayType(scalarType, scalarType); + var array2Type = FormulaType.getArrayType(scalarType, array1Type); + var array3Type = FormulaType.getArrayType(scalarType, array2Type); + + var array = amgr.makeArray("array", array3Type.getIndexType(), array3Type.getElementType()); + + var idxA = bvmgr.makeBitvector(scalarType.getSize(), 1); + var idxB = bvmgr.makeBitvector(scalarType.getSize(), 7); + var idxC = bvmgr.makeBitvector(scalarType.getSize(), 2); + var val = bvmgr.makeBitvector(scalarType.getSize(), 10); + + var scalarConst = bvmgr.makeBitvector(scalarType.getSize(), 0); + var array1Const = amgr.makeArray(array1Type, scalarConst); + var array2Const = amgr.makeArray(array2Type, array1Const); + var array3Const = amgr.makeArray(array3Type, array2Const); + + var array1Value = amgr.store(array1Const, idxC, val); + var array2Value = amgr.store(array2Const, idxB, array1Value); + var array3Value = amgr.store(array3Const, idxA, array2Value); + + checkModelContains( + amgr.equivalence(array, array3Value), + "array", + ImmutableMap.of(ImmutableList.of(idxA, idxB, idxC), val)); + } + + @Test + public void testArray1Int() { + requireArrays(); + requireArrayModel(); + requireIntegers(); + + var array = amgr.makeArray("array", IntegerType, IntegerType); + + var idx = imgr.makeNumber(1); + var val = imgr.makeNumber(10); + + checkModelContains( + imgr.equal(amgr.select(array, idx), val), + "array", + ImmutableMap.of(ImmutableList.of(idx), val)); + } + + @Test + public void testArray2Int() { + requireArrays(); + requireArrayModel(); + requireIntegers(); + + var array = amgr.makeArray("array", IntegerType, IntegerType); + + var idxA = imgr.makeNumber(1); + var valA = imgr.makeNumber(10); + + var idxB = imgr.makeNumber(2); + var valB = imgr.makeNumber(5); + + checkModelContains( + bmgr.and( + imgr.equal(amgr.select(array, idxA), valA), imgr.equal(amgr.select(array, idxB), valB)), + "array", + ImmutableMap.of(ImmutableList.of(idxA), valA, ImmutableList.of(idxB), valB)); + } + + @Test + public void testArray1IntInt() { + requireArrays(); + requireArrayModel(); + requireIntegers(); + + var array = + amgr.makeArray("array", IntegerType, FormulaType.getArrayType(IntegerType, IntegerType)); + + var idxA = imgr.makeNumber(1); + var idxB = imgr.makeNumber(7); + var val = imgr.makeNumber(10); + + checkModelContains( + imgr.equal(amgr.select(amgr.select(array, idxA), idxB), val), + "array", + ImmutableMap.of(ImmutableList.of(idxA, idxB), val)); + } + + @Test + public void testArrayStore1IntIntInt() { + // Test for 3d integer arrays with exactly one element + // array = (Store (const ...) idxA (Store (const ..) idxB (Store (const ...) idx C val)) + requireArrays(); + requireIntegers(); + + var scalarType = FormulaType.IntegerType; + + var array1Type = FormulaType.getArrayType(scalarType, scalarType); + var array2Type = FormulaType.getArrayType(scalarType, array1Type); + var array3Type = FormulaType.getArrayType(scalarType, array2Type); + + var array = amgr.makeArray("array", array3Type.getIndexType(), array3Type.getElementType()); + + var idxA = imgr.makeNumber(1); + var idxB = imgr.makeNumber(7); + var idxC = imgr.makeNumber(2); + var val = imgr.makeNumber(10); + + var scalarConst = imgr.makeNumber(0); + var array1Const = amgr.makeArray(array1Type, scalarConst); + var array2Const = amgr.makeArray(array2Type, array1Const); + var array3Const = amgr.makeArray(array3Type, array2Const); + + var array1Value = amgr.store(array1Const, idxC, val); + var array2Value = amgr.store(array2Const, idxB, array1Value); + var array3Value = amgr.store(array3Const, idxA, array2Value); + + checkModelContains( + amgr.equivalence(array, array3Value), + "array", + ImmutableMap.of(ImmutableList.of(idxA, idxB, idxC), val)); + } + + @Test + public void testArray2IntInt() { + requireArrays(); + requireArrayModel(); + requireIntegers(); + + var array = + amgr.makeArray("array", IntegerType, FormulaType.getArrayType(IntegerType, IntegerType)); + + var idxA1 = imgr.makeNumber(1); + var idxA2 = imgr.makeNumber(7); + var valA = imgr.makeNumber(10); + + var idxB1 = imgr.makeNumber(3); + var idxB2 = imgr.makeNumber(2); + var valB = imgr.makeNumber(5); + + checkModelContains( + bmgr.and( + imgr.equal(amgr.select(amgr.select(array, idxA1), idxA2), valA), + imgr.equal(amgr.select(amgr.select(array, idxB1), idxB2), valB)), + "array", + ImmutableMap.of( + ImmutableList.of(idxA1, idxA2), valA, ImmutableList.of(idxB1, idxB2), valB)); + } + @Test @SuppressWarnings("resource") public void multiCloseTest() throws SolverException, InterruptedException {