diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index be28f5eef2e..2b0aac06ac4 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -18,8 +18,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include +#include +#include + /// Map bytes according to the configured endianness. The key difference to /// endianness_mapt is that bv_endianness_mapt is aware of the bit-level /// encoding of types, which need not co-incide with the bit layout at @@ -911,112 +915,214 @@ bvt bv_pointerst::add_addr(const exprt &expr) return encode(a, type); } -void bv_pointerst::do_postponed( - const postponedt &postponed) +std::pair bv_pointerst::prepare_postponed_is_dynamic_object( + std::vector &placeholders) const { - if(postponed.expr.id() == ID_is_dynamic_object) + PRECONDITION(placeholders.empty()); + + const auto &objects = pointer_logic.objects; + std::size_t number = 0; + + exprt::operandst dynamic_objects_ops, not_dynamic_objects_ops; + dynamic_objects_ops.reserve(objects.size()); + not_dynamic_objects_ops.reserve(objects.size()); + + for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number) { - const auto &type = - to_pointer_type(to_unary_expr(postponed.expr).op().type()); - const auto &objects = pointer_logic.objects; - std::size_t number=0; + const exprt &expr = *it; - for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number) + // only compare object part + pointer_typet pt = pointer_type(expr.type()); + bvt bv = object_literals(encode(number, pt), pt); + + exprt::operandst conjuncts; + conjuncts.reserve(bv.size()); + placeholders.reserve(bv.size()); + for(std::size_t i = 0; i < bv.size(); ++i) { - const exprt &expr=*it; + if(placeholders.size() <= i) + placeholders.push_back(symbol_exprt{std::to_string(i), bool_typet{}}); + + POSTCONDITION(bv[i].is_constant()); + if(bv[i].is_true()) + conjuncts.emplace_back(placeholders[i]); + else + conjuncts.emplace_back(not_exprt{placeholders[i]}); + } - bool is_dynamic=pointer_logic.is_dynamic_object(expr); + if(pointer_logic.is_dynamic_object(expr)) + dynamic_objects_ops.push_back(conjunction(conjuncts)); + else + not_dynamic_objects_ops.push_back(conjunction(conjuncts)); + } - // only compare object part - pointer_typet pt = pointer_type(expr.type()); - bvt bv = object_literals(encode(number, pt), type); + exprt dynamic_objects = disjunction(dynamic_objects_ops); + exprt not_dynamic_objects = disjunction(not_dynamic_objects_ops); - bvt saved_bv = object_literals(postponed.op, type); + bdd_exprt bdd_converter; + bddt dyn_bdd = bdd_converter.from_expr(dynamic_objects); + bddt not_dyn_bdd = bdd_converter.from_expr(not_dynamic_objects); - POSTCONDITION(bv.size()==saved_bv.size()); - PRECONDITION(postponed.bv.size()==1); + return {bdd_converter.as_expr(dyn_bdd), bdd_converter.as_expr(not_dyn_bdd)}; +} - literalt l1=bv_utils.equal(bv, saved_bv); - literalt l2=postponed.bv.front(); +std::unordered_map +bv_pointerst::prepare_postponed_object_size( + std::vector &placeholders) const +{ + PRECONDITION(placeholders.empty()); - if(!is_dynamic) - l2=!l2; + const auto &objects = pointer_logic.objects; + std::size_t number = 0; - prop.l_set_to_true(prop.limplies(l1, l2)); - } - } - else if( - const auto postponed_object_size = - expr_try_dynamic_cast(postponed.expr)) + std::unordered_map per_size_object_ops; + + for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number) { - const auto &type = to_pointer_type(postponed_object_size->pointer().type()); - const auto &objects = pointer_logic.objects; - std::size_t number=0; + const exprt &expr = *it; + + if(expr.id() != ID_symbol && expr.id() != ID_string_constant) + continue; - for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++number) + const auto size_expr = size_of_expr(expr.type(), ns); + if(!size_expr.has_value()) + continue; + + // only compare object part + pointer_typet pt = pointer_type(expr.type()); + bvt bv = object_literals(encode(number, pt), pt); + + exprt::operandst conjuncts; + conjuncts.reserve(bv.size()); + placeholders.reserve(bv.size()); + for(std::size_t i = 0; i < bv.size(); ++i) { - const exprt &expr=*it; + if(placeholders.size() <= i) + placeholders.push_back(symbol_exprt{std::to_string(i), bool_typet{}}); + + POSTCONDITION(bv[i].is_constant()); + if(bv[i].is_true()) + conjuncts.emplace_back(placeholders[i]); + else + conjuncts.emplace_back(not_exprt{placeholders[i]}); + } - if(expr.id() != ID_symbol && expr.id() != ID_string_constant) - continue; + per_size_object_ops[size_expr.value()].push_back(conjunction(conjuncts)); + } - const auto size_expr = size_of_expr(expr.type(), ns); + std::unordered_map result; + for(const auto &size_entry : per_size_object_ops) + { + exprt all_objects_this_size = disjunction(size_entry.second); + bdd_exprt bdd_converter; + bddt bdd = bdd_converter.from_expr(all_objects_this_size); - if(!size_expr.has_value()) - continue; + result.emplace(size_entry.first, bdd_converter.as_expr(bdd)); + } - const exprt object_size = typecast_exprt::conditional_cast( - size_expr.value(), postponed_object_size->type()); + return result; +} - // only compare object part - pointer_typet pt = pointer_type(expr.type()); - bvt bv = object_literals(encode(number, pt), type); +void bv_pointerst::finish_eager_conversion() +{ + // post-processing arrays may yield further objects, do this first + SUB::finish_eager_conversion(); - bvt saved_bv = object_literals(postponed.op, type); + // it would seem nicer to use `optionalt` here, but GCC >= 12 produces + // spurious warnings about accessing uninitialized objects + std::pair is_dynamic_expr = {nil_exprt{}, nil_exprt{}}; + std::vector is_dynamic_placeholders; - bvt size_bv = convert_bv(object_size); + std::unordered_map object_sizes; + std::vector object_size_placeholders; - POSTCONDITION(bv.size()==saved_bv.size()); - PRECONDITION(postponed.bv.size()>=1); - PRECONDITION(size_bv.size() == postponed.bv.size()); + for(const postponedt &postponed : postponed_list) + { + if(postponed.expr.id() == ID_is_dynamic_object) + { + if(is_dynamic_expr.first.is_nil()) + is_dynamic_expr = + prepare_postponed_is_dynamic_object(is_dynamic_placeholders); - literalt l1=bv_utils.equal(bv, saved_bv); - if(l1.is_true()) + const auto &type = + to_pointer_type(to_unary_expr(postponed.expr).op().type()); + bvt saved_bv = object_literals(postponed.op, type); + POSTCONDITION(saved_bv.size() == is_dynamic_placeholders.size()); + replace_mapt replacements; + for(std::size_t i = 0; i < saved_bv.size(); ++i) { - for(std::size_t i = 0; i < postponed.bv.size(); ++i) - prop.set_equal(postponed.bv[i], size_bv[i]); - break; + replacements.emplace( + is_dynamic_placeholders[i], literal_exprt{saved_bv[i]}); } - else if(l1.is_false()) + exprt is_dyn = is_dynamic_expr.first; + replace_expr(replacements, is_dyn); + exprt is_not_dyn = is_dynamic_expr.second; + replace_expr(replacements, is_not_dyn); + + PRECONDITION(postponed.bv.size() == 1); + prop.l_set_to_true( + prop.limplies(convert_bv(is_dyn)[0], postponed.bv.front())); + prop.l_set_to_true( + prop.limplies(convert_bv(is_not_dyn)[0], !postponed.bv.front())); + } + else if( + const auto postponed_object_size = + expr_try_dynamic_cast(postponed.expr)) + { + if(object_sizes.empty()) + object_sizes = prepare_postponed_object_size(object_size_placeholders); + + // we might not have any usable objects + if(object_size_placeholders.empty()) continue; + + const auto &type = + to_pointer_type(postponed_object_size->pointer().type()); + bvt saved_bv = object_literals(postponed.op, type); + POSTCONDITION(saved_bv.size() == object_size_placeholders.size()); + replace_mapt replacements; + for(std::size_t i = 0; i < saved_bv.size(); ++i) + { + replacements.emplace( + object_size_placeholders[i], literal_exprt{saved_bv[i]}); + } + + for(const auto &object_size_entry : object_sizes) + { + const exprt object_size = typecast_exprt::conditional_cast( + object_size_entry.first, postponed_object_size->type()); + bvt size_bv = convert_bv(object_size); + POSTCONDITION(size_bv.size() == postponed.bv.size()); + + exprt all_objects_this_size = object_size_entry.second; + replace_expr(replacements, all_objects_this_size); + + literalt l1 = convert_bv(all_objects_this_size)[0]; + if(l1.is_true()) + { + for(std::size_t i = 0; i < postponed.bv.size(); ++i) + prop.set_equal(postponed.bv[i], size_bv[i]); + break; + } + else if(l1.is_false()) + continue; #define COMPACT_OBJECT_SIZE_EQ #ifndef COMPACT_OBJECT_SIZE_EQ - literalt l2=bv_utils.equal(postponed.bv, size_bv); + literalt l2 = bv_utils.equal(postponed.bv, size_bv); - prop.l_set_to_true(prop.limplies(l1, l2)); + prop.l_set_to_true(prop.limplies(l1, l2)); #else - for(std::size_t i = 0; i < postponed.bv.size(); ++i) - { - prop.lcnf({!l1, !postponed.bv[i], size_bv[i]}); - prop.lcnf({!l1, postponed.bv[i], !size_bv[i]}); - } + for(std::size_t i = 0; i < postponed.bv.size(); ++i) + { + prop.lcnf({!l1, !postponed.bv[i], size_bv[i]}); + prop.lcnf({!l1, postponed.bv[i], !size_bv[i]}); + } #endif + } } + else + UNREACHABLE; } - else - UNREACHABLE; -} - -void bv_pointerst::finish_eager_conversion() -{ - // post-processing arrays may yield further objects, do this first - SUB::finish_eager_conversion(); - - for(postponed_listt::const_iterator - it=postponed_list.begin(); - it!=postponed_list.end(); - it++) - do_postponed(*it); // Clear the list to avoid re-doing in case of incremental usage. postponed_list.clear(); diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index e165c510d79..5317bde6a8b 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -92,7 +92,16 @@ class bv_pointerst:public boolbvt typedef std::list postponed_listt; postponed_listt postponed_list; - void do_postponed(const postponedt &postponed); + /// Create Boolean functions describing all dynamic and all not-dynamic object + /// encodings over \p placeholders as input Boolean variables representing + /// object bits. + std::pair prepare_postponed_is_dynamic_object( + std::vector &placeholders) const; + + /// Create Boolean functions describing all objects of each known object size + /// over \p placeholders as input Boolean variables representing object bits. + std::unordered_map + prepare_postponed_object_size(std::vector &placeholders) const; /// Given a pointer encoded in \p bv, extract the literals identifying the /// object that the pointer points to.