From 1aee1f42fec34159ef53ab0ad4ac5c6697f38f14 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Thu, 5 Aug 2021 14:15:02 -0700 Subject: [PATCH] Normalize val in BitVector(val_str, base) (#6955) Fixes cpp API's mkBitVector(val_str, base) constructor. --- src/api/cpp/cvc5.cpp | 3 ++- src/api/cpp/cvc5.h | 3 ++- src/util/bitvector.h | 4 ++++ test/unit/api/solver_black.cpp | 9 +++++++++ test/unit/util/bitvector_black.cpp | 5 +++++ 5 files changed, 22 insertions(+), 2 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index aca5fa981..60ef49cb4 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5044,6 +5044,8 @@ Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const CVC5_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; CVC5_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base) << "base 2, 10, or 16"; + CVC5_API_ARG_CHECK_EXPECTED(s[0] != '-', s) + << "a positive value (since no size is specified)"; //////// all checks before this line return mkValHelper(cvc5::BitVector(s, base)); } @@ -5071,7 +5073,6 @@ Term Solver::mkBVFromStrHelper(uint32_t size, << "Overflow in bitvector construction (specified bitvector size " << size << " too small to hold value " << s << ")"; } - return mkValHelper(cvc5::BitVector(size, val)); } diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 25057ff2f..a232f9c7e 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3288,7 +3288,8 @@ class CVC5_EXPORT Solver * - base 16: the max. size required to represent the hexadecimal as a * bit-vector (4 * size of the given value string) * - * @param s the string representation of the constant + * @param s The string representation of the constant. + * This cannot be negative. * @param base the base of the string representation (2, 10, or 16) * @return the bit-vector constant */ diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 6e194ad41..cd0870722 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -76,12 +76,16 @@ class BitVector * bit-vector (4 * size of the given value string) * * @param num The value of the bit-vector in string representation. + * This cannot be a negative value. * @param base The base of the string representation. */ BitVector(const std::string& num, unsigned base = 2) { CheckArgument(base == 2 || base == 10 || base == 16, base); + CheckArgument(num[0] != '-', num); d_value = Integer(num, base); + CheckArgument(d_value == d_value.abs(), num); + // Compute the length, *without* any negative sign. switch (base) { case 10: d_size = d_value.length(); break; diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 453ef1d24..0c4007411 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -323,6 +323,15 @@ TEST_F(TestApiBlackSolver, mkBitVector) ASSERT_THROW(d_solver.mkBitVector("20", 2), CVC5ApiException); ASSERT_THROW(d_solver.mkBitVector(8, "101010101", 2), CVC5ApiException); ASSERT_THROW(d_solver.mkBitVector(8, "-256", 10), CVC5ApiException); + // No size and negative string -> error + ASSERT_THROW(d_solver.mkBitVector("-1", 2), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector("-1", 10), CVC5ApiException); + ASSERT_THROW(d_solver.mkBitVector("-f", 16), CVC5ApiException); + // size and negative string -> ok + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 2), d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 16), d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 10), d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10)); ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10)); ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("a", 16)); ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101"); diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp index 2450747cd..98331cc7f 100644 --- a/test/unit/util/bitvector_black.cpp +++ b/test/unit/util/bitvector_black.cpp @@ -65,6 +65,11 @@ TEST_F(TestUtilBlackBitVector, string_constructor) ASSERT_EQ("000000011010", b4.toString()); ASSERT_EQ("26", b4.toString(10)); ASSERT_EQ("1a", b4.toString(16)); + + ASSERT_THROW(BitVector("-4", 10), IllegalArgumentException); + ASSERT_THROW(BitVector("-0010", 2), IllegalArgumentException); + ASSERT_THROW(BitVector("-3210", 4), IllegalArgumentException); + ASSERT_EQ(3, BitVector("4", 10).getSize()); } TEST_F(TestUtilBlackBitVector, conversions) -- 2.30.2