26 #include <unordered_set>
33 const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
35 solver_process.
send(command);
45 static std::optional<std::string>
50 return "SMT solver returned an error message - " +
55 return {
"SMT solver does not support given command."};
74 std::vector<exprt> dependent_expressions;
76 std::stack<const exprt *> stack;
77 stack.push(&root_expr);
81 const exprt &expr_node = *stack.top();
90 dependent_expressions.push_back(expr_node);
97 const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr_node);
100 for(
auto &operand : expr_node.
operands())
101 stack.push(&operand);
103 return dependent_expressions;
111 const std::vector<exprt> &elements = array.
operands();
113 for(std::size_t i = 0; i < elements.size(); ++i)
134 {array_index_identifier},
148 template <
typename t_exprt>
150 const t_exprt &array)
155 "Converting array typed expression to SMT should result in a term of array "
167 const std::unique_ptr<smt_base_solver_processt> &solver_process,
168 std::unordered_map<exprt, smt_identifier_termt, irep_hash>
169 &expression_identifiers,
170 std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
176 expression_identifiers.emplace(expr,
function.identifier());
177 identifier_table.emplace(symbol_identifier,
function.identifier());
178 solver_process->send(
function);
186 std::unordered_set<exprt, irep_hash> seen_expressions =
188 .map([](
const std::pair<exprt, smt_identifier_termt> &expr_identifier) {
189 return expr_identifier.first;
191 std::stack<exprt> to_be_defined;
192 const auto push_dependencies_needed = [&](
const exprt &expr) {
196 if(!seen_expressions.insert(dependency).second)
199 to_be_defined.push(dependency);
203 push_dependencies_needed(expr);
204 while(!to_be_defined.empty())
206 const exprt current = to_be_defined.top();
207 if(push_dependencies_needed(current))
209 if(
const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
213 symbol_expr->get_identifier(),
218 else if(
const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
221 const auto array_of_expr = expr_try_dynamic_cast<array_of_exprt>(current))
226 const auto string = expr_try_dynamic_cast<string_constantt>(current))
231 const auto nondet_symbol =
232 expr_try_dynamic_cast<nondet_symbol_exprt>(current))
236 nondet_symbol->get_identifier(),
249 const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
250 &expression_identifiers)
253 auto find_result = expression_identifiers.find(node);
254 if(find_result == expression_identifiers.cend())
256 const auto type = find_result->first.type();
257 node =
symbol_exprt{find_result->second.identifier(), type};
264 std::unique_ptr<smt_base_solver_processt> _solver_process,
267 number_of_solver_calls{0},
268 solver_process(std::move(_solver_process)),
269 log{message_handler},
284 auto prophecy_r_or_w_ok =
285 expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
290 auto prophecy_pointer_in_range =
291 expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
293 expr =
simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
300 const exprt &in_expr)
318 function.identifier().identifier(),
function.identifier());
328 if(
const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
330 for(auto operand_ite = ++with_expr->operands().begin();
331 operand_ite != with_expr->operands().end();
334 const auto index_expr = *operand_ite;
335 const auto index_term = convert_expr_to_smt(index_expr);
336 const auto index_identifier =
337 "index_" + std::to_string(index_sequence());
338 const auto index_definition =
339 smt_define_function_commandt{index_identifier, {}, index_term};
340 expression_identifiers.emplace(
341 index_expr, index_definition.identifier());
342 identifier_table.emplace(
343 index_identifier, index_definition.identifier());
344 solver_process->send(
345 smt_define_function_commandt{index_identifier, {}, index_term});
355 if(
const auto pad = expr_try_dynamic_cast<nondet_padding_exprt>(node))
392 debug <<
"`handle` -\n " << expr.pretty(2, 0) << messaget::eom;
398 std::optional<smt_termt>
404 return handle_find_result->second;
407 return expr_find_result->second;
411 const auto lowered_handle_find_result =
414 return lowered_handle_find_result->second;
415 const auto lowered_expr_find_result =
418 return lowered_expr_find_result->second;
427 type.
is_complete(),
"Array size is required for getting array values.");
428 const auto size = numeric_cast<std::size_t>(
get(type.
size()));
431 "Size of array must be convertible to std::size_t for getting array value");
432 std::vector<exprt> elements;
434 elements.reserve(*size);
435 for(std::size_t index = 0; index < size; ++index)
447 elements.push_back(std::move(*element));
456 const auto encoded_result =
467 const auto encoded_result =
476 const typet &type)
const
478 if(
const auto array_type = type_try_dynamic_cast<array_typet>(type))
480 if(array_type->is_incomplete())
482 return get_expr(descriptor, *array_type);
484 if(
const auto struct_type = type_try_dynamic_cast<struct_tag_typet>(type))
486 return get_expr(descriptor, *struct_type);
488 if(
const auto union_type = type_try_dynamic_cast<union_tag_typet>(type))
490 return get_expr(descriptor, *union_type);
496 if(!get_value_response)
499 "Expected get-value response from solver, but received - " +
502 if(get_value_response->pairs().size() > 1)
505 "Expected single valuation pair in get-value response from solver, but "
506 "received multiple pairs - " +
510 get_value_response->pairs()[0].get().value(), type,
ns);
528 exprt eval_op = decision_procedure.
get(op);
531 op = std::move(eval_op);
539 debug <<
"`get` - \n " + expr.pretty(2, 0) << messaget::eom;
541 auto descriptor = [&]() -> std::optional<smt_termt> {
542 if(
const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
552 return identifier_descriptor;
559 "Objects in expressions being read should already be tracked from "
560 "point of being set/handled.");
574 "symbol expressions must have a known value",
579 return std::move(*result);
584 std::ostream &out)
const
592 return "incremental SMT2 solving via " +
solver_process->description();
602 const exprt &in_expr,
606 debug <<
"`set_to` (" << std::string{value ?
"true" :
"false"} <<
") -\n "
609 const exprt lowered_expr = lower(in_expr);
612 define_dependent_functions(lowered_expr);
613 auto converted_term = [&]() ->
smt_termt {
614 const auto expression_handle_identifier =
615 expression_handle_identifiers.
find(lowered_expr);
616 if(expression_handle_identifier != expression_handle_identifiers.cend())
617 return expression_handle_identifier->second;
627 const std::vector<exprt> &assumptions)
629 for(
const auto &assumption : assumptions)
632 "pushing of assumption:\n " + assumption.pretty(2, 0));
674 object.unique_id,
object.is_dynamic));
684 if(lowered != expression)
685 debug <<
"lowered to -\n " << lowered.pretty(2, 0) << messaget::eom;
Expression classes for byte-level operators.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Array constructor from list of elements.
const array_typet & type() const
Array constructor from single element.
const array_typet & type() const
typet index_type() const
The type of the index expressions into any instance of this type.
const typet & element_type() const
The type of the elements of the array.
const exprt & size() const
virtual exprt get(const exprt &) const =0
Return expr with variables replaced by values from satisfying assignment if available.
resultt
Result of running the decision procedure.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
void visit_pre(std::function< void(exprt &)>)
typet & type()
Return the type of the expression.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
smt_object_sizet object_size_function
Implementation of the SMT formula for the object size function.
size_t number_of_solver_calls
The number of times dec_solve() has been called.
std::unordered_map< exprt, smt_identifier_termt, irep_hash > expression_identifiers
As part of the decision procedure's overall translation of CBMCs exprts into SMT terms,...
void define_index_identifiers(const exprt &expr)
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
exprt lower(exprt expression) const
Performs a combination of transformations which reduces the set of possible expression forms by expre...
struct_encodingt struct_encoding
exprt substitute_defined_padding(exprt expr)
In the case where lowering passes insert instances of the anonymous nondet_padding_exprt,...
std::optional< exprt > get_expr(const smt_termt &descriptor, const typet &type) const
Gets the value of descriptor from the solver and returns the solver response expressed as an exprt of...
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
smt_is_dynamic_objectt is_dynamic_object_function
Implementation of the SMT formula for the dynamic object status lookup function.
void ensure_handle_for_expr_defined(const exprt &expr)
If a function has not been defined for handling expr, then a new function is defined.
void define_dependent_functions(const exprt &expr)
Defines any functions which expr depends on, which have not yet been defined, along with their depend...
void initialize_array_elements(const array_exprt &array, const smt_identifier_termt &array_identifier)
Generate and send to the SMT solver clauses asserting that each array element is as specified by arra...
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
resultt dec_solve(const exprt &) override
Implementation of the decision procedure.
void push() override
Push a new context on the stack This context becomes a child context nested in the current context.
messaget log
For reporting errors, warnings and debugging information back to the user.
void pop() override
Pop whatever is on top of the stack.
class smt2_incremental_decision_proceduret::sequencet padding_sequence
std::optional< smt_termt > get_identifier(const exprt &expr) const
std::unordered_map< irep_idt, smt_identifier_termt > identifier_table
This maps from the unsorted/untyped string/symbol for the identifiers which we have declared in SMT s...
smt_object_mapt object_map
This map is used to track object related state.
class smt2_incremental_decision_proceduret::sequencet array_sequence
std::vector< bool > object_properties_defined
The size of each object and the dynamic object stus is separately defined as a pre-solving step.
void define_object_properties()
Sends the solver the definitions of the object sizes and dynamic memory statuses.
smt_termt convert_expr_to_smt(const exprt &expr)
Add objects in expr to object_map if needed and convert to smt.
const namespacet & ns
Namespace for looking up the expressions which symbol_exprts relate to.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
type_size_mapt pointer_sizes_map
Precalculated type sizes used for pointer arithmetic.
std::unordered_map< exprt, smt_identifier_termt, irep_hash > expression_handle_identifiers
When the handle(exprt) member function is called, the decision procedure commands the SMT solver to d...
std::unique_ptr< smt_base_solver_processt > solver_process
For handling the lifetime of and communication with the separate SMT solver process.
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
class smt2_incremental_decision_proceduret::sequencet handle_sequence
smt2_incremental_decision_proceduret(const namespacet &_ns, std::unique_ptr< smt_base_solver_processt > solver_process, message_handlert &message_handler)
void define_array_function(const t_exprt &array)
Defines a function of array sort and asserts the element values from array_exprt or array_of_exprt.
static const smt_function_application_termt::factoryt< selectt > select
virtual void send(const smt_commandt &command)=0
Converts given SMT2 command to SMT2 string and sends it to the solver process.
virtual smt_responset receive_response(const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)=0
const sub_classt * cast() const &
static const smt_function_application_termt::factoryt< equalt > equal
static const smt_function_application_termt::factoryt< nott > make_not
Stores identifiers in unescaped and unquoted form.
irep_idt identifier() const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const sub_classt * cast() const &
const sub_classt * cast() const &
typet encode(typet type) const
exprt decode(const exprt &encoded, const struct_tag_typet &original_type) const
Reconstructs a struct expression of the original_type using the data from the bit vector encoded expr...
A struct tag type, i.e., struct_typet with an identifier.
Expression to hold a symbol (variable)
The type of an expression, extends irept.
A union tag type, i.e., union_typet with an identifier.
exprt construct_value_expr_from_smt(const smt_termt &value_term, const typet &type_to_construct, const namespacet &ns)
Given a value_term and a type_to_construct, this function constructs a value exprt with a value based...
static smt_sortt convert_type_to_smt_sort(const bool_typet &type)
static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
exprt lower_enum(exprt expr, const namespacet &ns)
Function to lower expr and its sub-expressions containing enum types.
const std::string & id2string(const irep_idt &d)
Expressions for use in incremental SMT2 decision procedure.
void track_expression_objects(const exprt &expression, const namespacet &ns, smt_object_mapt &object_map)
Finds all the object expressions in the given expression and adds them to the object map for cases wh...
bool objects_are_already_tracked(const exprt &expression, const smt_object_mapt &object_map)
Finds whether all base object expressions in the given expression are already tracked in the given ob...
smt_object_mapt initial_smt_object_map()
Constructs an initial object map containing the null object.
static struct_typet::componentst::iterator pad(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
exprt simplify_expr(exprt src, const namespacet &ns)
static std::optional< std::string > get_problem_messages(const smt_responset &response)
Returns a message string describing the problem in the case where the response from the solver is an ...
static exprt lower_rw_ok_pointer_in_range(exprt expr, const namespacet &ns)
void send_function_definition(const exprt &expr, 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, std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)
static exprt substitute_identifiers(exprt expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
Replaces the sub expressions of expr which have been defined as separate functions in the smt solver,...
static decision_proceduret::resultt lookup_decision_procedure_result(const smt_check_sat_response_kindt &response_kind)
static exprt build_expr_based_on_getting_operands(const exprt &expr, const stack_decision_proceduret &decision_procedure)
static std::vector< exprt > gather_dependent_expressions(const exprt &root_expr)
Find all sub expressions of the given expr which need to be expressed as separate smt commands.
static smt_responset get_response_to_command(smt_base_solver_processt &solver_process, const smt_commandt &command, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)
Issues a command to the solving process which is expected to optionally return a success status follo...
Decision procedure with incremental SMT2 solving.
#define UNIMPLEMENTED_FEATURE(FEATURE)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
API to expression classes.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
bool can_cast_expr< array_of_exprt >(const exprt &base)
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
bool can_cast_expr< symbol_exprt >(const exprt &base)
bool can_cast_expr< array_exprt >(const exprt &base)
bool can_cast_type< bool_typet >(const typet &base)
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
bool can_cast_expr< string_constantt >(const exprt &base)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Information the decision procedure holds about each object.
make_applicationt make_application
smt_declare_function_commandt declaration
The command for declaring the is_dynamic_object function.
smt_commandt make_definition(std::size_t unique_id, bool is_dynamic_object) const
Makes the command to define the resulting is_dynamic_object status for calls to the is_dynamic_object...
make_applicationt make_application
smt_commandt make_definition(std::size_t unique_id, smt_termt size) const
Makes the command to define the resulting size of calling the object size function with unique_id.
smt_declare_function_commandt declaration
The command for declaring the object size function.
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_is_dynamic_objectt::make_applicationt &is_dynamic_object)
This function populates the (pointer) type -> size map.
Utilities for making a map of types to associated sizes.