Skip to content

bv_pointert cleanup #6830

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Apr 26, 2022
Merged

bv_pointert cleanup #6830

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
3653c9b
bv_pointerst: move encoding methods into the .cpp file
kroening Apr 26, 2022
3790406
remove bv_pointerst::bv_pointers_widtht
kroening Apr 26, 2022
3c74995
bv_pointerst: remove obvious declarators
kroening Apr 26, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
83 changes: 43 additions & 40 deletions src/solvers/flattening/bv_pointers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,53 +68,58 @@ void bv_endianness_mapt::build_big_endian(const typet &src)
endianness_mapt
bv_pointerst::endianness_map(const typet &type, bool little_endian) const
{
return bv_endianness_mapt{type, little_endian, ns, bv_pointers_width};
return bv_endianness_mapt{type, little_endian, ns, bv_width};
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That second commit is a part-revert of 5cf2b07. If we go for removing the capability that the commit was trying to add we should ponder a clean revert instead.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We absolutely want to keep the parts of that commit that pass the pointer type around!

}

std::size_t bv_pointerst::bv_pointers_widtht::
operator()(const typet &type) const
{
if(type.id() != ID_pointer)
return boolbv_widtht::operator()(type);

// check or update the cache, just like boolbv_widtht does
std::pair<cachet::iterator, bool> cache_result =
cache.insert(std::pair<typet, entryt>(type, entryt()));

if(cache_result.second)
{
std::size_t &total_width = cache_result.first->second.total_width;

total_width = get_address_width(to_pointer_type(type));
DATA_INVARIANT(total_width > 0, "pointer width shall be greater than zero");
}

return cache_result.first->second.total_width;
}

std::size_t bv_pointerst::bv_pointers_widtht::get_object_width(
const pointer_typet &type) const
std::size_t bv_pointerst::get_object_width(const pointer_typet &) const
{
// not actually type-dependent for now
(void)type;
return config.bv_encoding.object_bits;
}

std::size_t bv_pointerst::bv_pointers_widtht::get_offset_width(
const pointer_typet &type) const
std::size_t bv_pointerst::get_offset_width(const pointer_typet &type) const
{
const std::size_t pointer_width = type.get_width();
const std::size_t object_width = get_object_width(type);
PRECONDITION(pointer_width >= object_width);
return pointer_width - object_width;
}

std::size_t bv_pointerst::bv_pointers_widtht::get_address_width(
const pointer_typet &type) const
std::size_t bv_pointerst::get_address_width(const pointer_typet &type) const
{
return type.get_width();
}

bvt bv_pointerst::object_literals(const bvt &bv, const pointer_typet &type)
const
{
const std::size_t offset_width = get_offset_width(type);
const std::size_t object_width = get_object_width(type);
PRECONDITION(bv.size() >= offset_width + object_width);

return bvt(
bv.begin() + offset_width, bv.begin() + offset_width + object_width);
}

bvt bv_pointerst::offset_literals(const bvt &bv, const pointer_typet &type)
const
{
const std::size_t offset_width = get_offset_width(type);
PRECONDITION(bv.size() >= offset_width);

return bvt(bv.begin(), bv.begin() + offset_width);
}

bvt bv_pointerst::object_offset_encoding(const bvt &object, const bvt &offset)
{
bvt result;
result.reserve(offset.size() + object.size());
result.insert(result.end(), offset.begin(), offset.end());
result.insert(result.end(), object.begin(), object.end());

return result;
}

literalt bv_pointerst::convert_rest(const exprt &expr)
{
PRECONDITION(expr.type().id() == ID_bool);
Expand All @@ -136,8 +141,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
bvt invalid_bv = object_literals(
encode(pointer_logic.get_invalid_object(), type), type);

const std::size_t object_bits =
bv_pointers_width.get_object_width(type);
const std::size_t object_bits = get_object_width(type);

bvt equal_invalid_bv;
equal_invalid_bv.reserve(object_bits);
Expand Down Expand Up @@ -210,8 +214,7 @@ bv_pointerst::bv_pointerst(
message_handlert &message_handler,
bool get_array_constraints)
: boolbvt(_ns, _prop, message_handler, get_array_constraints),
pointer_logic(_ns),
bv_pointers_width(_ns)
pointer_logic(_ns)
{
}

Expand Down Expand Up @@ -460,7 +463,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
count == 1,
"there should be exactly one pointer-type operand in a pointer-type sum");

const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
const std::size_t offset_bits = get_offset_width(type);
bvt sum = bv_utils.build_constant(0, offset_bits);

forall_operands(it, plus_expr)
Expand Down Expand Up @@ -815,8 +818,8 @@ exprt bv_pointerst::bv_get_rec(

bvt bv_pointerst::encode(std::size_t addr, const pointer_typet &type) const
{
const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
const std::size_t object_bits = bv_pointers_width.get_object_width(type);
const std::size_t offset_bits = get_offset_width(type);
const std::size_t object_bits = get_object_width(type);

bvt zero_offset(offset_bits, const_literal(false));

Expand All @@ -834,7 +837,7 @@ bvt bv_pointerst::offset_arithmetic(
const bvt &bv,
const mp_integer &x)
{
const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
const std::size_t offset_bits = get_offset_width(type);

return offset_arithmetic(
type, bv, 1, bv_utils.build_constant(x, offset_bits));
Expand All @@ -852,7 +855,7 @@ bvt bv_pointerst::offset_arithmetic(
index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
bv_utilst::representationt::UNSIGNED;

const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
const std::size_t offset_bits = get_offset_width(type);
bv_index=bv_utils.extension(bv_index, offset_bits, rep);

return offset_arithmetic(type, bv, factor, bv_index);
Expand All @@ -874,7 +877,7 @@ bvt bv_pointerst::offset_arithmetic(
bv_index = bv_utils.signed_multiplier(index, bv_factor);
}

const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
const std::size_t offset_bits = get_offset_width(type);
bv_index = bv_utils.sign_extension(bv_index, offset_bits);

bvt offset_bv = offset_literals(bv, type);
Expand All @@ -889,7 +892,7 @@ bvt bv_pointerst::add_addr(const exprt &expr)
std::size_t a=pointer_logic.add_object(expr);

const pointer_typet type = pointer_type(expr.type());
const std::size_t object_bits = bv_pointers_width.get_object_width(type);
const std::size_t object_bits = get_object_width(type);
const std::size_t max_objects=std::size_t(1)<<object_bits;

if(a==max_objects)
Expand Down
91 changes: 24 additions & 67 deletions src/solvers/flattening/bv_pointers.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,78 +19,57 @@ class bv_pointerst:public boolbvt
{
public:
bv_pointerst(
const namespacet &_ns,
propt &_prop,
message_handlert &message_handler,
const namespacet &,
propt &,
message_handlert &,
bool get_array_constraints = false);

void finish_eager_conversion() override;

std::size_t boolbv_width(const typet &type) const override
{
return bv_pointers_width(type);
}

endianness_mapt
endianness_map(const typet &type, bool little_endian) const override;
endianness_map(const typet &, bool little_endian) const override;

protected:
pointer_logict pointer_logic;

class bv_pointers_widtht : public boolbv_widtht
{
public:
explicit bv_pointers_widtht(const namespacet &_ns) : boolbv_widtht(_ns)
{
}

std::size_t operator()(const typet &type) const override;

std::size_t get_object_width(const pointer_typet &type) const;
std::size_t get_offset_width(const pointer_typet &type) const;
std::size_t get_address_width(const pointer_typet &type) const;
};
bv_pointers_widtht bv_pointers_width;
std::size_t get_object_width(const pointer_typet &) const;
std::size_t get_offset_width(const pointer_typet &) const;
std::size_t get_address_width(const pointer_typet &) const;

// NOLINTNEXTLINE(readability/identifiers)
typedef boolbvt SUB;

NODISCARD
bvt encode(std::size_t object, const pointer_typet &type) const;
bvt encode(std::size_t object, const pointer_typet &) const;

virtual bvt convert_pointer_type(const exprt &expr);
virtual bvt convert_pointer_type(const exprt &);

NODISCARD
virtual bvt add_addr(const exprt &expr);
virtual bvt add_addr(const exprt &);

// overloading
literalt convert_rest(const exprt &expr) override;
bvt convert_bitvector(const exprt &expr) override; // no cache
literalt convert_rest(const exprt &) override;
bvt convert_bitvector(const exprt &) override; // no cache

exprt bv_get_rec(
const exprt &expr,
const bvt &bv,
std::size_t offset,
const typet &type) const override;
exprt
bv_get_rec(const exprt &, const bvt &, std::size_t offset, const typet &)
const override;

NODISCARD
optionalt<bvt> convert_address_of_rec(const exprt &expr);
optionalt<bvt> convert_address_of_rec(const exprt &);

NODISCARD
bvt offset_arithmetic(
const pointer_typet &type,
const bvt &bv,
const mp_integer &x);
bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
NODISCARD
bvt offset_arithmetic(
const pointer_typet &type,
const bvt &bv,
const pointer_typet &,
const bvt &,
const mp_integer &factor,
const exprt &index);
NODISCARD
bvt offset_arithmetic(
const pointer_typet &type,
const bvt &bv,
const pointer_typet &,
const bvt &,
const mp_integer &factor,
const bvt &index_bv);

Expand All @@ -115,43 +94,21 @@ class bv_pointerst:public boolbvt
/// \param bv: Encoded pointer
/// \param type: Type of the encoded pointer
/// \return Vector of literals identifying the object part of \p bv
bvt object_literals(const bvt &bv, const pointer_typet &type) const
{
const std::size_t offset_width = bv_pointers_width.get_offset_width(type);
const std::size_t object_width = bv_pointers_width.get_object_width(type);
PRECONDITION(bv.size() >= offset_width + object_width);

return bvt(
bv.begin() + offset_width, bv.begin() + offset_width + object_width);
}
bvt object_literals(const bvt &bv, const pointer_typet &type) const;

/// Given a pointer encoded in \p bv, extract the literals representing the
/// offset into an object that the pointer points to.
/// \param bv: Encoded pointer
/// \param type: Type of the encoded pointer
/// \return Vector of literals identifying the offset part of \p bv
bvt offset_literals(const bvt &bv, const pointer_typet &type) const
{
const std::size_t offset_width = bv_pointers_width.get_offset_width(type);
PRECONDITION(bv.size() >= offset_width);

return bvt(bv.begin(), bv.begin() + offset_width);
}
bvt offset_literals(const bvt &bv, const pointer_typet &type) const;

/// Construct a pointer encoding from given encodings of \p object and \p
/// offset.
/// \param object: Encoded object
/// \param offset: Encoded offset
/// \return Pointer encoding
static bvt object_offset_encoding(const bvt &object, const bvt &offset)
{
bvt result;
result.reserve(offset.size() + object.size());
result.insert(result.end(), offset.begin(), offset.end());
result.insert(result.end(), object.begin(), object.end());

return result;
}
static bvt object_offset_encoding(const bvt &object, const bvt &offset);
};

#endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H