28#include <unordered_set>
35 const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
37 solver_process.
send(command);
52 return "SMT solver returned an error message - " +
57 return {
"SMT solver does not support given command."};
76 std::vector<exprt> dependent_expressions;
78 std::stack<const exprt *> stack;
79 stack.push(&root_expr);
83 const exprt &expr_node = *stack.top();
92 dependent_expressions.push_back(expr_node);
102 for(
auto &operand : expr_node.
operands())
103 stack.push(&operand);
105 return dependent_expressions;
113 const std::vector<exprt> &elements = array.
operands();
115 for(std::size_t i = 0; i < elements.size(); ++i)
136 {array_index_identifier},
150template <
typename t_exprt>
152 const t_exprt &array)
157 "Converting array typed expression to SMT should result in a term of array "
169 const std::unique_ptr<smt_base_solver_processt> &solver_process,
170 std::unordered_map<exprt, smt_identifier_termt, irep_hash>
171 &expression_identifiers,
172 std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
178 expression_identifiers.emplace(expr, function.identifier());
179 identifier_table.emplace(symbol_identifier, function.identifier());
180 solver_process->send(function);
188 std::unordered_set<exprt, irep_hash> seen_expressions =
190 .map([](
const std::pair<exprt, smt_identifier_termt> &expr_identifier) {
191 return expr_identifier.first;
193 std::stack<exprt> to_be_defined;
194 const auto push_dependencies_needed = [&](
const exprt &expr) {
198 if(!seen_expressions.insert(dependency).second)
201 to_be_defined.push(dependency);
205 push_dependencies_needed(expr);
206 while(!to_be_defined.empty())
208 const exprt current = to_be_defined.top();
209 if(push_dependencies_needed(current))
213 const irep_idt &identifier = symbol_expr->get_identifier();
214 const symbolt *symbol =
nullptr;
219 symbol_expr->get_identifier(),
227 if(push_dependencies_needed(lowered))
249 const auto nondet_symbol =
254 nondet_symbol->get_identifier(),
267 const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
268 &expression_identifiers)
271 auto find_result = expression_identifiers.find(node);
272 if(find_result == expression_identifiers.cend())
274 const auto type = find_result->first.type();
275 node =
symbol_exprt{find_result->second.identifier(), type};
282 std::unique_ptr<smt_base_solver_processt> _solver_process,
285 number_of_solver_calls{0},
286 solver_process(
std::move(_solver_process)),
287 log{message_handler},
302 auto prophecy_r_or_w_ok =
308 auto prophecy_pointer_in_range =
311 expr =
simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
318 const exprt &in_expr)
336 function.identifier().identifier(), function.identifier());
348 for(
auto operand_ite = ++with_expr->operands().begin();
349 operand_ite != with_expr->operands().end();
352 const auto index_expr = *operand_ite;
354 const auto index_identifier =
356 const auto index_definition =
359 index_expr, index_definition.identifier());
361 index_identifier, index_definition.identifier());
399 return ::convert_expr_to_smt(
410 debug <<
"`handle` -\n " << expr.pretty(2, 0) << messaget::eom;
422 return handle_find_result->second;
425 return expr_find_result->second;
429 const auto lowered_handle_find_result =
432 return lowered_handle_find_result->second;
433 const auto lowered_expr_find_result =
436 return lowered_expr_find_result->second;
445 type.
is_complete(),
"Array size is required for getting array values.");
449 "Size of array must be convertible to std::size_t for getting array value");
450 std::vector<exprt> elements;
452 elements.reserve(*size);
453 for(std::size_t index = 0; index < size; ++index)
465 elements.push_back(std::move(*element));
474 const auto encoded_result =
483 const typet &type)
const
487 if(array_type->is_incomplete())
489 return get_expr(descriptor, *array_type);
493 return get_expr(descriptor, *struct_type);
499 if(!get_value_response)
502 "Expected get-value response from solver, but received - " +
505 if(get_value_response->pairs().size() > 1)
508 "Expected single valuation pair in get-value response from solver, but "
509 "received multiple pairs - " +
513 get_value_response->pairs()[0].get().value(), type,
ns);
531 exprt eval_op = decision_procedure.
get(op);
534 op = std::move(eval_op);
542 debug <<
"`get` - \n " + expr.pretty(2, 0) << messaget::eom;
555 return identifier_descriptor;
562 "Objects in expressions being read should already be tracked from "
563 "point of being set/handled.");
564 return ::convert_expr_to_smt(
577 "symbol expressions must have a known value",
582 return std::move(*result);
587 std::ostream &out)
const
605 const exprt &in_expr,
609 debug <<
"`set_to` (" << std::string{value ?
"true" :
"false"} <<
") -\n "
612 const exprt lowered_expr = lower(in_expr);
615 define_dependent_functions(lowered_expr);
616 auto converted_term = [&]() ->
smt_termt {
617 const auto expression_handle_identifier =
618 expression_handle_identifiers.
find(lowered_expr);
619 if(expression_handle_identifier != expression_handle_identifiers.cend())
620 return expression_handle_identifier->second;
630 const std::vector<exprt> &assumptions)
632 for(
const auto &assumption : assumptions)
635 "pushing of assumption:\n " + assumption.pretty(2, 0));
677 object.unique_id,
object.is_dynamic));
687 if(lowered != expression)
688 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...
bitvector_typet index_type()
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 exprt & size() const
const typet & element_type() const
The type of the elements of the array.
resultt
Result of running the decision procedure.
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
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...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
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,...
resultt dec_solve() override
Run the decision procedure to solve the problem.
optionalt< smt_termt > get_identifier(const exprt &expr) const
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.
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.
optionalt< 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...
class smt2_incremental_decision_proceduret::sequencet padding_sequence
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.
class smt2_incremental_decision_proceduret::sequencet index_sequence
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
virtual const std::string & description()=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)
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
The type of an expression, extends irept.
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.
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
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.
nonstd::optional< T > optionalt
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 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 exprt build_expr_based_on_getting_operands(const exprt &expr, const stack_decision_proceduret &decision_procedure)
static optionalt< 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 NODISCARD decision_proceduret::resultt lookup_decision_procedure_result(const smt_check_sat_response_kindt &response_kind)
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...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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)
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.