Skip to content

Add array trace printing to incremental SMT2 decision procedure #7078

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.

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
Show file tree
Hide file tree
Changes from all commits
Commits
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
7 changes: 7 additions & 0 deletions regression/cbmc-incr-smt2/arrays_traces/array_read.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
int main()
{
int example_array[1025];
unsigned int index;
__CPROVER_assume(index < 1025);
__CPROVER_assert(example_array[index] != 42, "Array condition");
}
15 changes: 15 additions & 0 deletions regression/cbmc-incr-smt2/arrays_traces/array_read.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
CORE
array_read.c
--trace
Passing problem to incremental SMT2 solving
\[main\.assertion\.1\] line \d+ Array condition: FAILURE
^Trace for main\.assertion\.1
example_array=\{ (\d+, )*42
^EXIT=10$
^SIGNAL=0$
--
--
Test of reading a value at a non-deterministic index of an array.
Similar to the test in ../arrays/array_read.c, but we want to assert
the value of the array that comes back in the trace to make sure we're
observing the correct values.
9 changes: 9 additions & 0 deletions regression/cbmc-incr-smt2/arrays_traces/array_write.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
int main()
{
int example_array[1025];
unsigned int index;
__CPROVER_assume(index < 1025);
example_array[index] = 42;
__CPROVER_assert(example_array[index] == 42, "Array condition");
__CPROVER_assert(example_array[index] != 42, "Array condition");
}
12 changes: 12 additions & 0 deletions regression/cbmc-incr-smt2/arrays_traces/array_write.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
CORE
array_write.c
--trace
Passing problem to incremental SMT2 solving
^Trace for main\.assertion\.2
example_array\[\d{1,4}ll?\]=42
^EXIT=10$
^SIGNAL=0$
--
--
Test of writing a value at a non-deterministic index of an array, then asserting
the value we expect.
64 changes: 64 additions & 0 deletions src/solvers/smt2_incremental/response_or_error.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
// Author: Diffblue Ltd.

#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H

#include <util/invariant.h>
#include <util/optional.h>

#include <string>
#include <vector>

/// Holds either a valid parsed response or response sub-tree of type \tparam
/// smtt or a collection of message strings explaining why the given input was
/// not valid.
template <class smtt>
class response_or_errort final
{
public:
explicit response_or_errort(smtt smt) : smt{std::move(smt)}
{
}

explicit response_or_errort(std::string message)
: messages{std::move(message)}
{
}

explicit response_or_errort(std::vector<std::string> messages)
: messages{std::move(messages)}
{
}

/// \brief Gets the smt response if the response is valid, or returns nullptr
/// otherwise.
const smtt *get_if_valid() const
{
INVARIANT(
smt.has_value() == messages.empty(),
"The response_or_errort class must be in the valid state or error state, "
"exclusively.");
return smt.has_value() ? &smt.value() : nullptr;
}

/// \brief Gets the error messages if the response is invalid, or returns
/// nullptr otherwise.
const std::vector<std::string> *get_if_error() const
{
INVARIANT(
smt.has_value() == messages.empty(),
"The response_or_errort class must be in the valid state or error state, "
"exclusively.");
return smt.has_value() ? nullptr : &messages;
}

private:
// The below two fields could be a single `std::variant` field, if there was
// an implementation of it available in the cbmc repository. However at the
// time of writing we are targeting C++11, `std::variant` was introduced in
// C++17 and we have no backported version.
optionalt<smtt> smt;
std::vector<std::string> messages;
};

#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
142 changes: 115 additions & 27 deletions src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -27,12 +27,13 @@
/// return a success status followed by the actual response of interest.
static smt_responset get_response_to_command(
smt_base_solver_processt &solver_process,
const smt_commandt &command)
const smt_commandt &command,
const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
{
solver_process.send(command);
auto response = solver_process.receive_response();
auto response = solver_process.receive_response(identifier_table);
if(response.cast<smt_success_responset>())
return solver_process.receive_response();
return solver_process.receive_response(identifier_table);
else
return response;
}
Expand Down Expand Up @@ -84,6 +85,7 @@ void smt2_incremental_decision_proceduret::initialize_array_elements(
const array_exprt &array,
const smt_identifier_termt &array_identifier)
{
identifier_table.emplace(array_identifier.identifier(), array_identifier);
const std::vector<exprt> &elements = array.operands();
const typet &index_type = array.type().index_type();
for(std::size_t i = 0; i < elements.size(); ++i)
Expand Down Expand Up @@ -135,13 +137,15 @@ void send_function_definition(
const irep_idt &symbol_identifier,
const std::unique_ptr<smt_base_solver_processt> &solver_process,
std::unordered_map<exprt, smt_identifier_termt, irep_hash>
&expression_identifiers)
&expression_identifiers,
std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
{
const smt_declare_function_commandt function{
smt_identifier_termt(
symbol_identifier, convert_type_to_smt_sort(expr.type())),
{}};
expression_identifiers.emplace(expr, function.identifier());
identifier_table.emplace(symbol_identifier, function.identifier());
solver_process->send(function);
}

Expand Down Expand Up @@ -183,7 +187,8 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
*symbol_expr,
symbol_expr->get_identifier(),
solver_process,
expression_identifiers);
expression_identifiers,
identifier_table);
}
else
{
Expand All @@ -192,6 +197,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
const smt_define_function_commandt function{
symbol->name, {}, convert_expr_to_smt(symbol->value)};
expression_identifiers.emplace(*symbol_expr, function.identifier());
identifier_table.emplace(identifier, function.identifier());
solver_process->send(function);
}
}
Expand All @@ -210,7 +216,8 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
*nondet_symbol,
nondet_symbol->get_identifier(),
solver_process,
expression_identifiers);
expression_identifiers,
identifier_table);
}
to_be_defined.pop();
}
Expand Down Expand Up @@ -263,12 +270,36 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
smt_define_function_commandt function{
"B" + std::to_string(handle_sequence()), {}, convert_expr_to_smt(expr)};
expression_handle_identifiers.emplace(expr, function.identifier());
identifier_table.emplace(
function.identifier().identifier(), function.identifier());
solver_process->send(function);
}

void smt2_incremental_decision_proceduret::define_index_identifiers(
const exprt &expr)
{
expr.visit_pre([&](const exprt &expr_node) {
if(!can_cast_type<array_typet>(expr_node.type()))
return;
if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
{
const auto index_expr = with_expr->where();
const auto index_term = convert_expr_to_smt(index_expr);
const auto index_identifier = "index_" + std::to_string(index_sequence());
const auto index_definition =
smt_define_function_commandt{index_identifier, {}, index_term};
expression_identifiers.emplace(index_expr, index_definition.identifier());
identifier_table.emplace(index_identifier, index_definition.identifier());
solver_process->send(
smt_define_function_commandt{index_identifier, {}, index_term});
}
});
}

smt_termt
smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
{
define_index_identifiers(expr);
const exprt substituted =
substitute_identifiers(expr, expression_identifiers);
track_expression_objects(substituted, ns, object_map);
Expand Down Expand Up @@ -310,13 +341,82 @@ static optionalt<smt_termt> get_identifier(
return {};
}

array_exprt smt2_incremental_decision_proceduret::get_expr(
const smt_termt &array,
const array_typet &type) const
{
INVARIANT(
type.is_complete(), "Array size is required for getting array values.");
const auto size = numeric_cast<std::size_t>(get(type.size()));
INVARIANT(
size,
"Size of array must be convertible to std::size_t for getting array value");
std::vector<exprt> elements;
const auto index_type = type.index_type();
elements.reserve(*size);
for(std::size_t index = 0; index < size; ++index)
{
elements.push_back(get_expr(
smt_array_theoryt::select(
array,
::convert_expr_to_smt(
from_integer(index, index_type),
object_map,
pointer_sizes_map,
object_size_function.make_application)),
type.element_type()));
}
return array_exprt{elements, type};
}

exprt smt2_incremental_decision_proceduret::get_expr(
const smt_termt &descriptor,
const typet &type) const
{
const smt_get_value_commandt get_value_command{descriptor};
const smt_responset response = get_response_to_command(
*solver_process, get_value_command, identifier_table);
const auto get_value_response = response.cast<smt_get_value_responset>();
if(!get_value_response)
{
throw analysis_exceptiont{
"Expected get-value response from solver, but received - " +
response.pretty()};
}
if(get_value_response->pairs().size() > 1)
{
throw analysis_exceptiont{
"Expected single valuation pair in get-value response from solver, but "
"received multiple pairs - " +
response.pretty()};
}
return construct_value_expr_from_smt(
get_value_response->pairs()[0].get().value(), type);
}

exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
{
log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
debug << "`get` - \n " + expr.pretty(2, 0) << messaget::eom;
});
optionalt<smt_termt> descriptor =
get_identifier(expr, expression_handle_identifiers, expression_identifiers);
auto descriptor = [&]() -> optionalt<smt_termt> {
if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
{
const auto array = get_identifier(
index_expr->array(),
expression_handle_identifiers,
expression_identifiers);
const auto index = get_identifier(
index_expr->index(),
expression_handle_identifiers,
expression_identifiers);
if(!array || !index)
return {};
return smt_array_theoryt::select(*array, *index);
}
return get_identifier(
expr, expression_handle_identifiers, expression_identifiers);
}();
if(!descriptor)
{
if(gather_dependent_expressions(expr).empty())
Expand Down Expand Up @@ -349,25 +449,13 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
return expr;
}
}
const smt_get_value_commandt get_value_command{*descriptor};
const smt_responset response =
get_response_to_command(*solver_process, get_value_command);
const auto get_value_response = response.cast<smt_get_value_responset>();
if(!get_value_response)
{
throw analysis_exceptiont{
"Expected get-value response from solver, but received - " +
response.pretty()};
}
if(get_value_response->pairs().size() > 1)
if(const auto array_type = type_try_dynamic_cast<array_typet>(expr.type()))
{
throw analysis_exceptiont{
"Expected single valuation pair in get-value response from solver, but "
"received multiple pairs - " +
response.pretty()};
if(array_type->is_incomplete())
return expr;
return get_expr(*descriptor, *array_type);
}
return construct_value_expr_from_smt(
get_value_response->pairs()[0].get().value(), expr.type());
return get_expr(*descriptor, expr.type());
}

void smt2_incremental_decision_proceduret::print_assignment(
Expand Down Expand Up @@ -464,8 +552,8 @@ decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
{
++number_of_solver_calls;
define_object_sizes();
const smt_responset result =
get_response_to_command(*solver_process, smt_check_sat_commandt{});
const smt_responset result = get_response_to_command(
*solver_process, smt_check_sat_commandt{}, identifier_table);
if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
{
if(check_sat_response->kind().cast<smt_unknown_responset>())
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,12 @@ class smt2_incremental_decision_proceduret final
void push() override;
void pop() override;

/// Gets the value of \p descriptor from the solver and returns the solver
/// response expressed as an exprt of type \p type. This is an implementation
/// detail of the `get(exprt)` member function.
exprt get_expr(const smt_termt &descriptor, const typet &type) const;
array_exprt get_expr(const smt_termt &array, const array_typet &type) const;

protected:
// Implementation of protected decision_proceduret member function.
resultt dec_solve() override;
Expand Down Expand Up @@ -85,6 +91,7 @@ class smt2_incremental_decision_proceduret final
/// \brief Add objects in \p expr to object_map if needed and convert to smt.
/// \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();

Expand Down Expand Up @@ -112,7 +119,7 @@ class smt2_incremental_decision_proceduret final
{
return next_id++;
}
} handle_sequence, array_sequence;
} handle_sequence, array_sequence, index_sequence;
/// When the `handle(exprt)` member function is called, the decision procedure
/// commands the SMT solver to define a new function corresponding to the
/// given expression. The mapping of the expressions to the function
Expand All @@ -131,6 +138,7 @@ class smt2_incremental_decision_proceduret final
/// array expressions when support for them is implemented.
std::unordered_map<exprt, smt_identifier_termt, irep_hash>
expression_identifiers;
std::unordered_map<irep_idt, smt_identifier_termt> identifier_table;
/// This map is used to track object related state. See documentation in
/// object_tracking.h for details.
smt_object_mapt object_map;
Expand Down
Loading