diff --git a/regression/cbmc-incr-smt2/dynamic-memory/assert_dynamic.c b/regression/cbmc-incr-smt2/dynamic-memory/assert_dynamic.c new file mode 100644 index 00000000000..3cda96e2682 --- /dev/null +++ b/regression/cbmc-incr-smt2/dynamic-memory/assert_dynamic.c @@ -0,0 +1,17 @@ +#include +#include +#include + +bool nondet_bool(); + +void main() +{ + char local; + void *pointer = &local; + const bool make_dynamic = nondet_bool(); + if(make_dynamic) + { + pointer = malloc(1); + } + assert(__CPROVER_DYNAMIC_OBJECT(pointer)); +} diff --git a/regression/cbmc-incr-smt2/dynamic-memory/assert_dynamic.desc b/regression/cbmc-incr-smt2/dynamic-memory/assert_dynamic.desc new file mode 100644 index 00000000000..23804df57da --- /dev/null +++ b/regression/cbmc-incr-smt2/dynamic-memory/assert_dynamic.desc @@ -0,0 +1,11 @@ +CORE +assert_dynamic.c +--trace +Passing problem to incremental SMT2 solving +line 16 assertion __CPROVER_DYNAMIC_OBJECT\(pointer\)\: FAILURE +make_dynamic\=FALSE +^EXIT=10$ +^SIGNAL=0$ +-- +make_dynamic\=TRUE +-- diff --git a/regression/cbmc-incr-smt2/dynamic-memory/assert_not_dynamic.c b/regression/cbmc-incr-smt2/dynamic-memory/assert_not_dynamic.c new file mode 100644 index 00000000000..3bc68e448ef --- /dev/null +++ b/regression/cbmc-incr-smt2/dynamic-memory/assert_not_dynamic.c @@ -0,0 +1,17 @@ +#include +#include +#include + +bool nondet_bool(); + +void main() +{ + char local; + void *pointer = &local; + const bool make_dynamic = nondet_bool(); + if(make_dynamic) + { + pointer = malloc(1); + } + assert(!__CPROVER_DYNAMIC_OBJECT(pointer)); +} diff --git a/regression/cbmc-incr-smt2/dynamic-memory/assert_not_dynamic.desc b/regression/cbmc-incr-smt2/dynamic-memory/assert_not_dynamic.desc new file mode 100644 index 00000000000..84544c5dbcd --- /dev/null +++ b/regression/cbmc-incr-smt2/dynamic-memory/assert_not_dynamic.desc @@ -0,0 +1,11 @@ +CORE +assert_not_dynamic.c +--trace +Passing problem to incremental SMT2 solving +line 16 assertion \!__CPROVER_DYNAMIC_OBJECT\(pointer\)\: FAILURE +make_dynamic\=TRUE +^EXIT=10$ +^SIGNAL=0$ +-- +make_dynamic\=FALSE +-- diff --git a/regression/cbmc-incr-smt2/dynamic-memory/valid.c b/regression/cbmc-incr-smt2/dynamic-memory/valid.c new file mode 100644 index 00000000000..331ce28d3d5 --- /dev/null +++ b/regression/cbmc-incr-smt2/dynamic-memory/valid.c @@ -0,0 +1,17 @@ +#include +#include +#include + +bool nondet_bool(); + +void main() +{ + char local; + void *pointer = &local; + const bool make_dynamic = nondet_bool(); + if(make_dynamic) + { + pointer = malloc(1); + } + assert(make_dynamic || !__CPROVER_DYNAMIC_OBJECT(pointer)); +} diff --git a/regression/cbmc-incr-smt2/dynamic-memory/valid.desc b/regression/cbmc-incr-smt2/dynamic-memory/valid.desc new file mode 100644 index 00000000000..f6499f97255 --- /dev/null +++ b/regression/cbmc-incr-smt2/dynamic-memory/valid.desc @@ -0,0 +1,10 @@ +CORE +valid.c +--trace +Passing problem to incremental SMT2 solving +line 16 assertion make_dynamic \|\| \!__CPROVER_DYNAMIC_OBJECT\(pointer\)\: SUCCESS +VERIFICATION SUCCESSFUL +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/src/solvers/Makefile b/src/solvers/Makefile index fdeed7e705c..5e22bbcb236 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -204,6 +204,7 @@ SRC = $(BOOLEFORCE_SRC) \ smt2_incremental/convert_expr_to_smt.cpp \ smt2_incremental/object_tracking.cpp \ smt2_incremental/type_size_mapping.cpp \ + smt2_incremental/smt_is_dynamic_object.cpp \ smt2_incremental/smt_object_size.cpp \ smt2_incremental/smt_response_validation.cpp \ smt2_incremental/smt_solver_process.cpp \ diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 37d664bb85b..ed900fa0703 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1042,11 +1042,18 @@ static smt_termt convert_expr_to_smt( static smt_termt convert_expr_to_smt( const is_dynamic_object_exprt &is_dynamic_object, - const sub_expression_mapt &converted) + const sub_expression_mapt &converted, + const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object) { - UNIMPLEMENTED_FEATURE( - "Generation of SMT formula for is dynamic object expression: " + - is_dynamic_object.pretty()); + const smt_termt &pointer = converted.at(is_dynamic_object.address()); + const auto pointer_sort = pointer.get_sort().cast(); + INVARIANT( + pointer_sort, "Pointers should be encoded as bit vector sorted terms."); + const std::size_t pointer_width = pointer_sort->bit_width(); + return apply_is_dynamic_object( + std::vector{smt_bit_vector_theoryt::extract( + pointer_width - 1, + pointer_width - config.bv_encoding.object_bits)(pointer)}); } static smt_termt convert_expr_to_smt( @@ -1458,7 +1465,8 @@ static smt_termt dispatch_expr_to_smt_conversion( const sub_expression_mapt &converted, const smt_object_mapt &object_map, const type_size_mapt &pointer_sizes, - const smt_object_sizet::make_applicationt &call_object_size) + const smt_object_sizet::make_applicationt &call_object_size, + const smt_is_dynamic_objectt::make_applicationt &apply_is_dynamic_object) { if(const auto symbol = expr_try_dynamic_cast(expr)) { @@ -1660,7 +1668,8 @@ static smt_termt dispatch_expr_to_smt_conversion( const auto is_dynamic_object = expr_try_dynamic_cast(expr)) { - return convert_expr_to_smt(*is_dynamic_object, converted); + return convert_expr_to_smt( + *is_dynamic_object, converted, apply_is_dynamic_object); } if( const auto is_invalid_pointer = @@ -1837,7 +1846,8 @@ smt_termt convert_expr_to_smt( const exprt &expr, const smt_object_mapt &object_map, const type_size_mapt &pointer_sizes, - const smt_object_sizet::make_applicationt &object_size) + const smt_object_sizet::make_applicationt &object_size, + const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object) { #ifndef CPROVER_INVARIANT_DO_NOT_CHECK static bool in_conversion = false; @@ -1856,7 +1866,12 @@ smt_termt convert_expr_to_smt( if(find_result != sub_expression_map.cend()) return; smt_termt term = dispatch_expr_to_smt_conversion( - expr, sub_expression_map, object_map, pointer_sizes, object_size); + expr, + sub_expression_map, + object_map, + pointer_sizes, + object_size, + is_dynamic_object); sub_expression_map.emplace_hint(find_result, expr, std::move(term)); }); return std::move(sub_expression_map.at(lowered_expr)); diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.h b/src/solvers/smt2_incremental/convert_expr_to_smt.h index c6e64a55444..163607edb38 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.h +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.h @@ -6,6 +6,7 @@ #include #include #include +#include #include #include @@ -27,6 +28,7 @@ smt_termt convert_expr_to_smt( const exprt &expression, const smt_object_mapt &object_map, const type_size_mapt &pointer_sizes, - const smt_object_sizet::make_applicationt &object_size); + const smt_object_sizet::make_applicationt &object_size, + const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object); #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H diff --git a/src/solvers/smt2_incremental/object_tracking.cpp b/src/solvers/smt2_incremental/object_tracking.cpp index e88bfb22837..eda891d985d 100644 --- a/src/solvers/smt2_incremental/object_tracking.cpp +++ b/src/solvers/smt2_incremental/object_tracking.cpp @@ -5,6 +5,8 @@ #include #include #include +#include +#include #include #include #include @@ -49,6 +51,7 @@ static decision_procedure_objectt make_null_object() null_object.unique_id = 0; null_object.base_expression = null_pointer_exprt{pointer_type(void_type())}; null_object.size = from_integer(0, size_type()); + null_object.is_dynamic = false; return null_object; } @@ -60,6 +63,7 @@ static decision_procedure_objectt make_invalid_pointer_object() invalid_pointer_object.unique_id = 1; invalid_pointer_object.base_expression = make_invalid_pointer_expr(); invalid_pointer_object.size = from_integer(0, size_type()); + invalid_pointer_object.is_dynamic = false; return invalid_pointer_object; } @@ -77,6 +81,23 @@ smt_object_mapt initial_smt_object_map() return object_map; } +/// This function returns true for heap allocated objects or false for stack +/// allocated objects. +static bool is_dynamic(const exprt &object) +{ + // This check corresponds to the symbols created in + // `goto_symext::symex_allocate`, which implements the `__CPROVER_allocate` + // intrinsic function used by the standard library models. + const bool dynamic_type = object.type().get_bool(ID_C_dynamic); + if(dynamic_type) + return true; + const auto symbol = expr_try_dynamic_cast(object); + bool symbol_is_dynamic = + symbol && + has_prefix(id2string(symbol->get_identifier()), SYMEX_DYNAMIC_PREFIX); + return symbol_is_dynamic; +} + void track_expression_objects( const exprt &expression, const namespacet &ns, @@ -93,6 +114,7 @@ void track_expression_objects( object.base_expression = object_base; object.unique_id = object_map.size(); object.size = *size; + object.is_dynamic = is_dynamic(object_base); object_map.emplace_hint(find_result, object_base, std::move(object)); }); } diff --git a/src/solvers/smt2_incremental/object_tracking.h b/src/solvers/smt2_incremental/object_tracking.h index e39b238ab39..24563e7abd2 100644 --- a/src/solvers/smt2_incremental/object_tracking.h +++ b/src/solvers/smt2_incremental/object_tracking.h @@ -43,9 +43,11 @@ struct decision_procedure_objectt /// to deferencing a pointer to this object with a zero offset. exprt base_expression; /// Number which uniquely identifies this particular object. - std::size_t unique_id; + std::size_t unique_id = 0; /// Expression which evaluates to the size of the object in bytes. exprt size; + /// This is true for heap allocated objects and false for stack allocated. + bool is_dynamic = false; }; /// The model of addresses we use consists of a unique object identifier and an diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index f1d0d2e52c4..d05ec7add47 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -255,6 +255,7 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret( smt_set_option_commandt{smt_option_produce_modelst{true}}); solver_process->send(smt_set_logic_commandt{smt_logic_allt{}}); solver_process->send(object_size_function.declaration); + solver_process->send(is_dynamic_object_function.declaration); } void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined( @@ -321,12 +322,14 @@ smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr) ns, pointer_sizes_map, object_map, - object_size_function.make_application); + object_size_function.make_application, + is_dynamic_object_function.make_application); return ::convert_expr_to_smt( substituted, object_map, pointer_sizes_map, - object_size_function.make_application); + object_size_function.make_application, + is_dynamic_object_function.make_application); } exprt smt2_incremental_decision_proceduret::handle(const exprt &expr) @@ -376,7 +379,8 @@ array_exprt smt2_incremental_decision_proceduret::get_expr( from_integer(index, index_type), object_map, pointer_sizes_map, - object_size_function.make_application)), + object_size_function.make_application, + is_dynamic_object_function.make_application)), type.element_type())); } return array_exprt{elements, type}; @@ -442,7 +446,8 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const expr, object_map, pointer_sizes_map, - object_size_function.make_application); + object_size_function.make_application, + is_dynamic_object_function.make_application); } else { @@ -548,26 +553,28 @@ static decision_proceduret::resultt lookup_decision_procedure_result( UNREACHABLE; } -void smt2_incremental_decision_proceduret::define_object_sizes() +void smt2_incremental_decision_proceduret::define_object_properties() { - object_size_defined.resize(object_map.size()); + object_properties_defined.resize(object_map.size()); for(const auto &key_value : object_map) { const decision_procedure_objectt &object = key_value.second; - if(object_size_defined[object.unique_id]) + if(object_properties_defined[object.unique_id]) continue; else - object_size_defined[object.unique_id] = true; + object_properties_defined[object.unique_id] = true; define_dependent_functions(object.size); solver_process->send(object_size_function.make_definition( object.unique_id, convert_expr_to_smt(object.size))); + solver_process->send(is_dynamic_object_function.make_definition( + object.unique_id, object.is_dynamic)); } } decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve() { ++number_of_solver_calls; - define_object_sizes(); + define_object_properties(); const smt_responset result = get_response_to_command( *solver_process, smt_check_sat_commandt{}, identifier_table); if(const auto check_sat_response = result.cast()) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h index b4017ce5943..cec582f543a 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h @@ -11,6 +11,7 @@ #include #include +#include #include #include #include @@ -92,8 +93,9 @@ class smt2_incremental_decision_proceduret final /// \note This function is non-const because it mutates the object_map. smt_termt convert_expr_to_smt(const exprt &expr); void define_index_identifiers(const exprt &expr); - /// Sends the solver the definitions of the object sizes. - void define_object_sizes(); + /// Sends the solver the definitions of the object sizes and dynamic memory + /// statuses. + void define_object_properties(); /// Namespace for looking up the expressions which symbol_exprts relate to. /// This includes the symbols defined outside of the decision procedure but @@ -149,16 +151,21 @@ class smt2_incremental_decision_proceduret final /// This map is used to track object related state. See documentation in /// object_tracking.h for details. smt_object_mapt object_map; - /// The size of each object is separately defined as a pre-solving step. - /// `object_size_defined[object ID]` is set to true for objects where the size - /// has been defined. This is used to avoid defining the size of the same - /// object multiple times in the case where multiple rounds of solving are - /// carried out. - std::vector object_size_defined; + /// The size of each object and the dynamic object stus is separately defined + /// as a pre-solving step. `object_properties_defined[object ID]` is set to + /// true for objects where the size has been defined. This is used to avoid + /// defining the size of the same object multiple times in the case where + /// multiple rounds of solving are carried out. + std::vector object_properties_defined; /// Implementation of the SMT formula for the object size function. This is /// stateful because it depends on the configuration of the number of object /// bits and how many bits wide the size type is configured to be. smt_object_sizet object_size_function; + /// Implementation of the SMT formula for the dynamic object status lookup + /// function. This is stateful because it depends on the configuration of the + /// number of object bits and how many bits wide the size type is configured + /// to be. + smt_is_dynamic_objectt is_dynamic_object_function; /// Precalculated type sizes used for pointer arithmetic. type_size_mapt pointer_sizes_map; }; diff --git a/src/solvers/smt2_incremental/smt_is_dynamic_object.cpp b/src/solvers/smt2_incremental/smt_is_dynamic_object.cpp new file mode 100644 index 00000000000..f98e1aed19a --- /dev/null +++ b/src/solvers/smt2_incremental/smt_is_dynamic_object.cpp @@ -0,0 +1,36 @@ +// Author: Diffblue Ltd. + +#include "smt_is_dynamic_object.h" + +#include +#include + +#include + +static smt_declare_function_commandt +make_is_dynamic_object_function_declaration() +{ + return smt_declare_function_commandt{ + smt_identifier_termt{"is_dynamic_object", smt_bool_sortt{}}, + {smt_bit_vector_sortt{config.bv_encoding.object_bits}}}; +} + +smt_is_dynamic_objectt::smt_is_dynamic_objectt() + : declaration{make_is_dynamic_object_function_declaration()}, + make_application{smt_command_functiont{declaration}} +{ +} + +smt_commandt smt_is_dynamic_objectt::make_definition( + std::size_t unique_id, + bool is_dynamic_object) const +{ + const auto id_sort = + declaration.parameter_sorts().at(0).get().cast(); + INVARIANT(id_sort, "Object identifiers are expected to have bit vector sort"); + const auto bit_vector_of_id = + smt_bit_vector_constant_termt{unique_id, *id_sort}; + return smt_assert_commandt{smt_core_theoryt::equal( + make_application(std::vector{bit_vector_of_id}), + smt_bool_literal_termt{is_dynamic_object})}; +} diff --git a/src/solvers/smt2_incremental/smt_is_dynamic_object.h b/src/solvers/smt2_incremental/smt_is_dynamic_object.h new file mode 100644 index 00000000000..556846c71ce --- /dev/null +++ b/src/solvers/smt2_incremental/smt_is_dynamic_object.h @@ -0,0 +1,31 @@ +// Author: Diffblue Ltd. + +#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H +#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H + +#include +#include + +/// Specifics of how the dynamic object status lookup is implemented in SMT +/// terms. This uses an uninterpreted function as a lookup. Because these +/// functions must return the same result for a specific input, we can just +/// assert the value of the function output for the inputs where we want to +/// define specific ID input / dynamic_object output pairs. +struct smt_is_dynamic_objectt final +{ + smt_is_dynamic_objectt(); + /// The command for declaring the is_dynamic_object function. The defined + /// function takes a bit vector encoded unique object identifier and returns + /// a boolean value. + smt_declare_function_commandt declaration; + /// Function which makes applications of the smt function. + using make_applicationt = + smt_function_application_termt::factoryt; + make_applicationt make_application; + /// Makes the command to define the resulting \p is_dynamic_object status for + /// calls to the `is_dynamic_object` function with \p unique_id. + smt_commandt + make_definition(std::size_t unique_id, bool is_dynamic_object) const; +}; + +#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H diff --git a/src/solvers/smt2_incremental/type_size_mapping.cpp b/src/solvers/smt2_incremental/type_size_mapping.cpp index 8baa2695149..f9ee1aefe85 100644 --- a/src/solvers/smt2_incremental/type_size_mapping.cpp +++ b/src/solvers/smt2_incremental/type_size_mapping.cpp @@ -15,7 +15,8 @@ void associate_pointer_sizes( const namespacet &ns, type_size_mapt &type_size_map, const smt_object_mapt &object_map, - const smt_object_sizet::make_applicationt &object_size) + const smt_object_sizet::make_applicationt &object_size, + const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object) { expression.visit_pre([&](const exprt &sub_expression) { if( @@ -42,7 +43,11 @@ void associate_pointer_sizes( pointer_size_expr = pointer_size_opt.value(); } auto pointer_size_term = convert_expr_to_smt( - pointer_size_expr, object_map, type_size_map, object_size); + pointer_size_expr, + object_map, + type_size_map, + object_size, + is_dynamic_object); type_size_map.emplace_hint( find_result, pointer_type->base_type(), pointer_size_term); } diff --git a/src/solvers/smt2_incremental/type_size_mapping.h b/src/solvers/smt2_incremental/type_size_mapping.h index 3ec707e3e6a..a5e7f030ef1 100644 --- a/src/solvers/smt2_incremental/type_size_mapping.h +++ b/src/solvers/smt2_incremental/type_size_mapping.h @@ -10,6 +10,7 @@ #include #include +#include #include #include @@ -28,11 +29,13 @@ using type_size_mapt = std::unordered_map; /// from \p expression which are not already keys in the map. /// \param object_map: passed through to convert_expr_to_smt /// \param object_size: passed through to convert_expr_to_smt +/// \param is_dynamic_object: passed through to convert_expr_to_smt void associate_pointer_sizes( const exprt &expression, const namespacet &ns, type_size_mapt &type_size_map, const smt_object_mapt &object_map, - const smt_object_sizet::make_applicationt &object_size); + const smt_object_sizet::make_applicationt &object_size, + const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object); #endif diff --git a/unit/Makefile b/unit/Makefile index fb02559566d..66385d55656 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -110,6 +110,7 @@ SRC += analyses/ai/ai.cpp \ solvers/smt2_incremental/convert_expr_to_smt.cpp \ solvers/smt2_incremental/object_tracking.cpp \ solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp \ + solvers/smt2_incremental/smt_is_dynamic_object.cpp \ solvers/smt2_incremental/smt_object_size.cpp \ solvers/smt2_incremental/smt_response_validation.cpp \ solvers/smt2_incremental/smt_to_smt2_string.cpp \ diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 3ebc3f1097c..e9e7b3d1b2b 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -59,6 +59,7 @@ struct expr_to_smt_conversion_test_environmentt smt_object_mapt object_map; smt_object_sizet object_size_function; + smt_is_dynamic_objectt is_dynamic_object_function; type_size_mapt pointer_sizes; private: @@ -94,7 +95,8 @@ expr_to_smt_conversion_test_environmentt::convert(const exprt &expression) const expression, object_map, pointer_sizes, - object_size_function.make_application); + object_size_function.make_application, + is_dynamic_object_function.make_application); } TEST_CASE("\"array_typet\" to smt sort conversion", "[core][smt2_incremental]") @@ -471,7 +473,8 @@ TEST_CASE( ns, test.pointer_sizes, test.object_map, - test.object_size_function.make_application); + test.object_size_function.make_application, + test.is_dynamic_object_function.make_application); INFO("Input expr: " + pointer_arith_expr.pretty(2, 0)); const auto constructed_term = test.convert(pointer_arith_expr); @@ -546,7 +549,8 @@ TEST_CASE( ns, test.pointer_sizes, test.object_map, - test.object_size_function.make_application); + test.object_size_function.make_application, + test.is_dynamic_object_function.make_application); INFO("Input expr: " + pointer_arith_expr.pretty(2, 0)); const auto constructed_term = test.convert(pointer_arith_expr); @@ -577,7 +581,8 @@ TEST_CASE( ns, test.pointer_sizes, test.object_map, - test.object_size_function.make_application); + test.object_size_function.make_application, + test.is_dynamic_object_function.make_application); INFO("Input expr: " + pointer_arith_expr.pretty(2, 0)); const auto constructed_term = test.convert(pointer_arith_expr); const auto expected_term = smt_bit_vector_theoryt::subtract( @@ -614,7 +619,8 @@ TEST_CASE( ns, test.pointer_sizes, test.object_map, - test.object_size_function.make_application); + test.object_size_function.make_application, + test.is_dynamic_object_function.make_application); INFO("Input expr: " + pointer_subtraction.pretty(2, 0)); const auto constructed_term = test.convert(pointer_subtraction); const auto expected_term = smt_bit_vector_theoryt::signed_divide( @@ -1673,6 +1679,30 @@ TEST_CASE( smt_bit_vector_theoryt::concat(object, offset))})); } +TEST_CASE( + "expr to smt conversion for is_dynamic_object expressions", + "[core][smt2_incremental]") +{ + auto test = + expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64); + const symbol_tablet symbol_table; + const namespacet ns{symbol_table}; + const symbol_exprt foo{"foo", unsignedbv_typet{32}}; + const is_dynamic_object_exprt is_dynamic_object{address_of_exprt{foo}}; + track_expression_objects(is_dynamic_object, ns, test.object_map); + const auto foo_id = 2; + CHECK(test.object_map.at(foo).unique_id == foo_id); + const auto object_bits = config.bv_encoding.object_bits; + const auto object = smt_bit_vector_constant_termt{foo_id, object_bits}; + const auto offset = smt_bit_vector_constant_termt{0, 64 - object_bits}; + INFO("Expression " + is_dynamic_object.pretty(1, 0)); + CHECK( + test.convert(is_dynamic_object) == + test.is_dynamic_object_function.make_application(std::vector{ + smt_bit_vector_theoryt::extract(63, 64 - object_bits)( + smt_bit_vector_theoryt::concat(object, offset))})); +} + TEST_CASE( "lower_address_of_array_index works correctly", "[core][smt2_incremental]") @@ -1718,7 +1748,8 @@ TEST_CASE( ns, test.pointer_sizes, test.object_map, - test.object_size_function.make_application); + test.object_size_function.make_application, + test.is_dynamic_object_function.make_application); const smt_termt expected = smt_core_theoryt::equal( smt_identifier_termt(symbol.get_identifier(), smt_bit_vector_sortt{64}), smt_bit_vector_theoryt::add( diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp index 522fe102265..4dc716c5eb4 100644 --- a/unit/solvers/smt2_incremental/object_tracking.cpp +++ b/unit/solvers/smt2_incremental/object_tracking.cpp @@ -4,6 +4,7 @@ #include #include #include +#include #include #include @@ -199,3 +200,32 @@ TEST_CASE("Tracking object sizes.", "[core][smt2_incremental]") REQUIRE(object != object_map.end()); REQUIRE(object->second.size == expected_size); } + +static typet make_type_dynamic(typet base_type) +{ + base_type.set(ID_C_dynamic, true); + return base_type; +} + +TEST_CASE("Tracking dynamic object status.", "[core][smt2_incremental]") +{ + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_x86_64(); + smt_object_mapt object_map = initial_smt_object_map(); + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + exprt base_object; + bool expected_dynamic_status; + using rowt = + std::pair; + std::tie(base_object, expected_dynamic_status) = GENERATE_REF( + rowt{from_integer(0, unsignedbv_typet{(8)}), false}, + rowt{symbol_exprt{"foo", bool_typet{}}, false}, + rowt{symbol_exprt{SYMEX_DYNAMIC_PREFIX "bar", bool_typet{}}, true}, + rowt{from_integer(42, make_type_dynamic(signedbv_typet{16})), true}); + INFO("base_object is - " + base_object.pretty(1, 0)); + track_expression_objects(address_of_exprt{base_object}, ns, object_map); + const auto object = object_map.find(base_object); + REQUIRE(object != object_map.end()); + REQUIRE(object->second.is_dynamic == expected_dynamic_status); +} diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 7c560cda794..5f4a35f6fa2 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -113,6 +113,7 @@ struct decision_procedure_test_environmentt final std::vector sent_commands; null_message_handlert message_handler; smt_object_sizet object_size_function; + smt_is_dynamic_objectt is_dynamic_object_function; smt2_incremental_decision_proceduret procedure{ ns, util_make_unique( @@ -177,7 +178,8 @@ TEST_CASE( std::vector{ smt_set_option_commandt{smt_option_produce_modelst{true}}, smt_set_logic_commandt{smt_logic_allt{}}, - test.object_size_function.declaration}); + test.object_size_function.declaration, + test.is_dynamic_object_function.declaration}); test.sent_commands.clear(); SECTION("Set symbol to true.") { @@ -464,6 +466,10 @@ TEST_CASE( const auto invalid_pointer_object_size_definition = test.object_size_function.make_definition( 1, smt_bit_vector_constant_termt{0, 32}); + const auto null_object_dynamic_definition = + test.is_dynamic_object_function.make_definition(0, false); + const auto invalid_pointer_object_dynamic_definition = + test.is_dynamic_object_function.make_definition(1, false); const symbolt foo = make_test_symbol("foo", signedbv_typet{16}); const smt_identifier_termt foo_term{"foo", smt_bit_vector_sortt{16}}; const exprt expr_42 = from_integer({42}, signedbv_typet{16}); @@ -480,6 +486,8 @@ TEST_CASE( smt_assert_commandt{smt_core_theoryt::equal(foo_term, term_42)}, invalid_pointer_object_size_definition, null_object_size_definition, + null_object_dynamic_definition, + invalid_pointer_object_dynamic_definition, smt_check_sat_commandt{}}; REQUIRE( (test.sent_commands.size() == expected_commands.size() && diff --git a/unit/solvers/smt2_incremental/smt_is_dynamic_object.cpp b/unit/solvers/smt2_incremental/smt_is_dynamic_object.cpp new file mode 100644 index 00000000000..9a2f1e0a1a8 --- /dev/null +++ b/unit/solvers/smt2_incremental/smt_is_dynamic_object.cpp @@ -0,0 +1,53 @@ +// Author: Diffblue Ltd. + +#include +#include + +#include +#include +#include + +TEST_CASE("Test smt_is_dynamic_objectt", "[core][smt2_incremental]") +{ + const std::size_t object_bits = GENERATE(8, 16); + INFO("Using " + std::to_string(object_bits) + " object id bits."); + // Configuration needs to be set because smt_is_dynamic_objectt uses it. + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_x86_64(); + config.bv_encoding.object_bits = object_bits; + const smt_is_dynamic_objectt is_dynamic_object; + SECTION("Declare function") + { + CHECK( + is_dynamic_object.declaration == + smt_declare_function_commandt{ + smt_identifier_termt{"is_dynamic_object", smt_bool_sortt{}}, + {smt_bit_vector_sortt{object_bits}}}); + } + SECTION("Apply function") + { + const smt_identifier_termt object_id{ + "foo", smt_bit_vector_sortt{object_bits}}; + const smt_function_application_termt function_application = + is_dynamic_object.make_application(std::vector{object_id}); + CHECK( + function_application.function_identifier() == + smt_identifier_termt{"is_dynamic_object", smt_bool_sortt{}}); + REQUIRE(function_application.arguments().size() == 1); + REQUIRE(function_application.arguments().at(0).get() == object_id); + } + SECTION("Define result") + { + const bool dynamic_status = GENERATE(true, false); + INFO( + "Testing for dynamic status of " + + std::string(dynamic_status ? "true" : "false")); + const smt_commandt definition = + is_dynamic_object.make_definition(42, dynamic_status); + CHECK( + definition == smt_assert_commandt{smt_core_theoryt::equal( + is_dynamic_object.make_application(std::vector{ + smt_bit_vector_constant_termt{42, object_bits}}), + smt_bool_literal_termt{dynamic_status})}); + } +}