Skip to content

Commit

Permalink
format_expr now prints bv-typed constants
Browse files Browse the repository at this point in the history
This adds formatting for bv-type constants to format_expr.  As the bv type
does not have a numerical representation, the 0/1 bit pattern is printed,
starting with the bit with the highest index.
  • Loading branch information
kroening committed Sep 16, 2024
1 parent 5002f3b commit 2ed72b0
Show file tree
Hide file tree
Showing 2 changed files with 23 additions and 1 deletion.
13 changes: 13 additions & 0 deletions src/util/format_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -186,6 +186,19 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
type == ID_unsignedbv || type == ID_signedbv || type == ID_c_bool ||
type == ID_c_bit_field)
return os << *numeric_cast<mp_integer>(src);
else if(type == ID_bv)
{
// These do not have a numerical interpretation.
// We'll print the 0/1 bit pattern, starting with the bit
// that has the highest index.
auto width = to_bv_type(src.type()).get_width();
std::string result;
result.reserve(width);
auto &value = src.get_value();
for(std::size_t i = 0; i < width; i++)
result += get_bvrep_bit(value, width, width - i - 1) ? '1' : '0';
return os << result;
}
else if(type == ID_integer || type == ID_natural || type == ID_range)
return os << src.get_value();
else if(type == ID_string)
Expand Down
11 changes: 10 additions & 1 deletion unit/util/format_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,10 @@
\*******************************************************************/

#include <util/expr.h>
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/format_expr.h>
#include <util/std_expr.h>

#include <testing-utils/use_catch.h>

Expand All @@ -23,3 +25,10 @@ TEST_CASE(
});
REQUIRE(format_to_string(exprt{custom_id}) == "output");
}

TEST_CASE("Format a bv-typed constant", "[core][util][format_expr]")
{
auto value = make_bvrep(4, [](std::size_t index) { return index != 2; });
auto expr = constant_exprt{value, bv_typet{4}};
REQUIRE(format_to_string(expr) == "1011");
}

0 comments on commit 2ed72b0

Please sign in to comment.