CBMC
Loading...
Searching...
No Matches
smt2_incremental_decision_procedure.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
4
5#include <util/arith_tools.h>
8#include <util/c_types.h>
9#include <util/range.h>
10#include <util/simplify_expr.h>
11#include <util/std_expr.h>
13
25
26#include <stack>
27#include <unordered_set>
28
32 smt_base_solver_processt &solver_process,
33 const smt_commandt &command,
34 const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
35{
36 solver_process.send(command);
37 auto response = solver_process.receive_response(identifier_table);
39 return solver_process.receive_response(identifier_table);
40 else
41 return response;
42}
43
46static std::optional<std::string>
48{
49 if(const auto error = response.cast<smt_error_responset>())
50 {
51 return "SMT solver returned an error message - " +
52 id2string(error->message());
53 }
55 {
56 return {"SMT solver does not support given command."};
57 }
58 return {};
59}
60
73static std::vector<exprt> gather_dependent_expressions(const exprt &root_expr)
74{
75 std::vector<exprt> dependent_expressions;
76
77 std::stack<const exprt *> stack;
78 stack.push(&root_expr);
79
80 while(!stack.empty())
81 {
82 const exprt &expr_node = *stack.top();
83 stack.pop();
84 if(
90 {
92 }
93 // The decision procedure does not depend on the values inside address of
94 // code typed expressions. We can build the address without knowing the
95 // value at that memory location. In this case the hypothetical compiled
96 // machine instructions at the address are not relevant to solving, only
97 // representing *which* function a pointer points to is needed.
99 if(address_of && can_cast_type<code_typet>(address_of->object().type()))
100 continue;
101 for(auto &operand : expr_node.operands())
102 stack.push(&operand);
103 }
105}
106
108 const array_exprt &array,
110{
112 const std::vector<exprt> &elements = array.operands();
113 const typet &index_type = array.type().index_type();
114 for(std::size_t i = 0; i < elements.size(); ++i)
115 {
116 const smt_termt index = convert_expr_to_smt(from_integer(i, index_type));
119 convert_expr_to_smt(elements.at(i)))};
121 }
122}
123
141
148
149template <typename t_exprt>
151 const t_exprt &array)
152{
153 const smt_sortt array_sort = convert_type_to_smt_sort(array.type());
154 INVARIANT(
156 "Converting array typed expression to SMT should result in a term of array "
157 "sort.");
159 "array_" + std::to_string(array_sequence()), array_sort};
163}
164
166 const exprt &expr,
168 const std::unique_ptr<smt_base_solver_processt> &solver_process,
169 std::unordered_map<exprt, smt_identifier_termt, irep_hash>
170 &expression_identifiers,
171 std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
172{
173 const smt_declare_function_commandt function{
176 {}};
177 expression_identifiers.emplace(expr, function.identifier());
178 identifier_table.emplace(symbol_identifier, function.identifier());
179 solver_process->send(function);
180}
181
185 const exprt &expr)
186{
187 std::unordered_set<exprt, irep_hash> seen_expressions =
189 .map([](const std::pair<exprt, smt_identifier_termt> &expr_identifier) {
190 return expr_identifier.first;
191 });
192 std::stack<exprt> to_be_defined;
193 const auto push_dependencies_needed = [&](const exprt &expr) {
194 bool result = false;
195 for(const auto &dependency : gather_dependent_expressions(expr))
196 {
197 if(!seen_expressions.insert(dependency).second)
198 continue;
199 result = true;
201 }
202 return result;
203 };
205 while(!to_be_defined.empty())
206 {
207 const exprt current = to_be_defined.top();
208 if(push_dependencies_needed(current))
209 continue;
210 if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
211 {
213 *symbol_expr,
214 symbol_expr->get_identifier(),
218 }
219 else if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
221 else if(
223 {
225 }
226 else if(
227 const auto string = expr_try_dynamic_cast<string_constantt>(current))
228 {
229 define_array_function(*string);
230 }
231 else if(
232 const auto nondet_symbol =
234 {
237 nondet_symbol->get_identifier(),
241 }
242 to_be_defined.pop();
243 }
244}
245
249 exprt expr,
250 const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
251 &expression_identifiers)
252{
253 expr.visit_pre([&](exprt &node) -> void {
254 auto find_result = expression_identifiers.find(node);
255 if(find_result == expression_identifiers.cend())
256 return;
257 const auto type = find_result->first.type();
258 node = symbol_exprt{find_result->second.identifier(), type};
259 });
260 return expr;
261}
262
264 const namespacet &_ns,
265 std::unique_ptr<smt_base_solver_processt> _solver_process,
266 message_handlert &message_handler)
267 : ns{_ns},
268 number_of_solver_calls{0},
269 solver_process(std::move(_solver_process)),
270 log{message_handler},
271 object_map{initial_smt_object_map()},
272 struct_encoding{_ns}
273{
274 solver_process->send(
279}
280
282{
283 expr.visit_pre([&ns](exprt &expr) {
284 if(
285 auto prophecy_r_or_w_ok =
287 {
288 expr = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns);
289 }
290 else if(
293 {
294 expr = simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
295 }
296 });
297 return expr;
298}
299
301{
302 expr.visit_pre([](exprt &expr) {
303 if(auto zero_extend = expr_try_dynamic_cast<zero_extend_exprt>(expr))
304 {
305 expr = zero_extend->lower();
306 }
307 });
308 return expr;
309}
310
312 const exprt &in_expr)
313{
314 if(
317 {
318 return;
319 }
320
322
325 "B" + std::to_string(handle_sequence()),
326 {},
328 expression_handle_identifiers.emplace(in_expr, function.identifier());
329 identifier_table.emplace(
330 function.identifier().identifier(), function.identifier());
331 solver_process->send(function);
332}
333
335 const exprt &expr)
336{
337 expr.visit_post(
338 [&](const exprt &expr_node)
339 {
341 return;
343 {
344 const auto index_expr = with_expr->where();
346 const auto index_identifier =
347 "index_" + std::to_string(index_sequence());
348 const auto index_definition =
351 index_expr, index_definition.identifier());
352 identifier_table.emplace(
353 index_identifier, index_definition.identifier());
354 solver_process->send(
356 }
357 });
358}
359
362{
363 root_expr.visit_pre([&](exprt &node) {
365 {
366 const auto instance = "padding_" + std::to_string(padding_sequence());
367 const auto term =
370 node = symbol_exprt{instance, node.type()};
371 }
372 });
373 return root_expr;
374}
375
397
399{
401 debug << "`handle` -\n " << expr.pretty(2, 0) << messaget::eom;
402 });
404 return expr;
405}
406
407std::optional<smt_termt>
409{
410 // Lookup the non-lowered form first.
413 return handle_find_result->second;
414 const auto expr_find_result = expression_identifiers.find(expr);
416 return expr_find_result->second;
417
418 // If that didn't yield any results, then try the lowered form.
419 const exprt lowered_expr = lower(expr);
420 const auto lowered_handle_find_result =
423 return lowered_handle_find_result->second;
424 const auto lowered_expr_find_result =
427 return lowered_expr_find_result->second;
428 return {};
429}
430
432 const smt_termt &array,
433 const array_typet &type) const
434{
435 INVARIANT(
436 type.is_complete(), "Array size is required for getting array values.");
437 const auto size = numeric_cast<std::size_t>(get(type.size()));
438 INVARIANT(
439 size,
440 "Size of array must be convertible to std::size_t for getting array value");
441 std::vector<exprt> elements;
442 const auto index_type = type.index_type();
443 elements.reserve(*size);
444 for(std::size_t index = 0; index < size; ++index)
445 {
447 from_integer(index, index_type),
452 auto element = get_expr(
454 if(!element)
455 return {};
456 elements.push_back(std::move(*element));
457 }
458 return array_exprt{elements, type};
459}
460
462 const smt_termt &struct_term,
463 const struct_tag_typet &type) const
464{
465 const auto encoded_result =
467 if(!encoded_result)
468 return {};
469 return {struct_encoding.decode(*encoded_result, type)};
470}
471
473 const smt_termt &union_term,
474 const union_tag_typet &type) const
475{
476 const auto encoded_result =
478 if(!encoded_result)
479 return {};
480 return {struct_encoding.decode(*encoded_result, type)};
481}
482
484 const smt_termt &descriptor,
485 const typet &type) const
486{
488 {
489 if(array_type->is_incomplete())
490 return {};
491 return get_expr(descriptor, *array_type);
492 }
494 {
495 return get_expr(descriptor, *struct_type);
496 }
498 {
499 return get_expr(descriptor, *union_type);
500 }
506 {
508 "Expected get-value response from solver, but received - " +
509 response.pretty()};
510 }
511 if(get_value_response->pairs().size() > 1)
512 {
514 "Expected single valuation pair in get-value response from solver, but "
515 "received multiple pairs - " +
516 response.pretty()};
517 }
519 get_value_response->pairs()[0].get().value(), type, ns);
520}
521
522// This is a fall back which builds resulting expression based on getting the
523// values of its operands. It is used during trace building in the case where
524// certain kinds of expression appear on the left hand side of an
525// assignment. For example in the following trace assignment -
526// `byte_extract_little_endian(x, offset) = 1`
527// `::get` will be called on `byte_extract_little_endian(x, offset)` and
528// we build a resulting expression where `x` and `offset` are substituted
529// with their values.
531 const exprt &expr,
532 const stack_decision_proceduret &decision_procedure)
533{
534 exprt copy = expr;
535 for(auto &op : copy.operands())
536 {
537 exprt eval_op = decision_procedure.get(op);
538 if(eval_op.is_nil())
539 return nil_exprt{};
540 op = std::move(eval_op);
541 }
542 return copy;
543}
544
546{
548 debug << "`get` - \n " + expr.pretty(2, 0) << messaget::eom;
549 });
550 auto descriptor = [&]() -> std::optional<smt_termt> {
552 {
553 const auto array = get_identifier(index_expr->array());
554 const auto index = get_identifier(index_expr->index());
555 if(!array || !index)
556 return {};
557 return smt_array_theoryt::select(*array, *index);
558 }
560 {
562 }
563 const exprt lowered = lower(expr);
565 {
566 INVARIANT(
568 "Objects in expressions being read should already be tracked from "
569 "point of being set/handled.");
570 return ::convert_expr_to_smt(
571 lowered,
576 }
577 return {};
578 }();
579 if(!descriptor)
580 {
583 "symbol expressions must have a known value",
585 return build_expr_based_on_getting_operands(expr, *this);
586 }
587 if(auto result = get_expr(*descriptor, expr.type()))
588 return std::move(*result);
589 return expr;
590}
591
593 std::ostream &out) const
594{
595 UNIMPLEMENTED_FEATURE("printing of assignments.");
596}
597
598std::string
600{
601 return "incremental SMT2 solving via " + solver_process->description();
602}
603
604std::size_t
609
611 const exprt &in_expr,
612 bool value)
613{
615 debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n "
616 << in_expr.pretty(2, 0) << messaget::eom;
617 });
618 const exprt lowered_expr = lower(in_expr);
620
621 define_dependent_functions(lowered_expr);
622 auto converted_term = [&]() -> smt_termt {
624 expression_handle_identifiers.find(lowered_expr);
625 if(expression_handle_identifier != expression_handle_identifiers.cend())
626 return expression_handle_identifier->second;
627 else
629 }();
630 if(!value)
632 solver_process->send(smt_assert_commandt{converted_term});
633}
634
636 const std::vector<exprt> &assumptions)
637{
638 for(const auto &assumption : assumptions)
639 {
641 "pushing of assumption:\n " + assumption.pretty(2, 0));
642 }
643 UNIMPLEMENTED_FEATURE("`push` of empty assumptions.");
644}
645
650
655
668
670{
672 for(const auto &key_value : object_map)
673 {
674 const decision_procedure_objectt &object = key_value.second;
675 if(object_properties_defined[object.unique_id])
676 continue;
677 else
678 object_properties_defined[object.unique_id] = true;
679 define_dependent_functions(object.size);
681 object.unique_id, convert_expr_to_smt(object.size)));
683 object.unique_id, object.is_dynamic));
684 }
685}
686
688{
692 ns),
693 ns));
695 if(lowered != expression)
696 debug << "lowered to -\n " << lowered.pretty(2, 0) << messaget::eom;
697 });
698 return lowered;
699}
700
703{
708 if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
709 {
710 if(check_sat_response->kind().cast<smt_unknown_responset>())
711 log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
713 }
714 if(const auto problem = get_problem_messages(result))
716 throw analysis_exceptiont{"Unexpected kind of response from SMT solver."};
717}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes for bitvectors.
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...
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Array constructor from list of elements.
Definition std_expr.h:1621
const array_typet & type() const
Definition std_expr.h:1628
Array constructor from single element.
Definition std_expr.h:1558
const array_typet & type() const
Definition std_expr.h:1565
exprt & what()
Definition std_expr.h:1575
Arrays with given size.
Definition std_types.h:807
typet index_type() const
The type of the index expressions into any instance of this type.
Definition std_types.cpp:34
bool is_complete() const
Definition std_types.h:852
const exprt & size() const
Definition std_types.h:840
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
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.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
typet & type()
Return the type of the expression.
Definition expr.h:84
void visit_post(std::function< void(exprt &)>)
These are post-order traversal visitors, i.e., the visitor is executed on a node after its children h...
Definition expr.cpp:198
operandst & operands()
Definition expr.h:94
mstreamt & error() const
Definition message.h:391
mstreamt & debug() const
Definition message.h:421
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...
Definition message.cpp:139
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3209
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,...
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...
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.
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.
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'.
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
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.
Definition smt_terms.h:93
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.
Definition std_types.h:493
Expression to hold a symbol (variable)
Definition std_expr.h:131
The type of an expression, extends irept.
Definition type.h:29
A union tag type, i.e., union_typet with an identifier.
Definition c_types.h:199
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)
Definition irep.h:44
double log(double x)
Definition math.c:2449
STL namespace.
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)
Definition padding.cpp:154
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
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 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 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...
static exprt lower_zero_extend(exprt expr, const namespacet &ns)
Decision procedure with incremental SMT2 solving.
#define UNIMPLEMENTED_FEATURE(FEATURE)
Definition invariant.h:549
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#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...
Definition invariant.h:437
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1665
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.