cprover
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>
7#include <util/namespace.h>
8#include <util/nodiscard.h>
9#include <util/range.h>
10#include <util/simplify_expr.h>
11#include <util/std_expr.h>
13#include <util/symbol.h>
14
26
27#include <stack>
28#include <unordered_set>
29
33 smt_base_solver_processt &solver_process,
34 const smt_commandt &command,
35 const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
36{
37 solver_process.send(command);
38 auto response = solver_process.receive_response(identifier_table);
39 if(response.cast<smt_success_responset>())
40 return solver_process.receive_response(identifier_table);
41 else
42 return response;
43}
44
49{
50 if(const auto error = response.cast<smt_error_responset>())
51 {
52 return "SMT solver returned an error message - " +
53 id2string(error->message());
54 }
55 if(response.cast<smt_unsupported_responset>())
56 {
57 return {"SMT solver does not support given command."};
58 }
59 return {};
60}
61
74static std::vector<exprt> gather_dependent_expressions(const exprt &root_expr)
75{
76 std::vector<exprt> dependent_expressions;
77
78 std::stack<const exprt *> stack;
79 stack.push(&root_expr);
80
81 while(!stack.empty())
82 {
83 const exprt &expr_node = *stack.top();
84 stack.pop();
85 if(
86 can_cast_expr<symbol_exprt>(expr_node) ||
87 can_cast_expr<array_exprt>(expr_node) ||
91 {
92 dependent_expressions.push_back(expr_node);
93 }
94 // The decision procedure does not depend on the values inside address of
95 // code typed expressions. We can build the address without knowing the
96 // value at that memory location. In this case the hypothetical compiled
97 // machine instructions at the address are not relevant to solving, only
98 // representing *which* function a pointer points to is needed.
99 const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr_node);
100 if(address_of && can_cast_type<code_typet>(address_of->object().type()))
101 continue;
102 for(auto &operand : expr_node.operands())
103 stack.push(&operand);
104 }
105 return dependent_expressions;
106}
107
109 const array_exprt &array,
110 const smt_identifier_termt &array_identifier)
111{
112 identifier_table.emplace(array_identifier.identifier(), array_identifier);
113 const std::vector<exprt> &elements = array.operands();
114 const typet &index_type = array.type().index_type();
115 for(std::size_t i = 0; i < elements.size(); ++i)
116 {
118 const smt_assert_commandt element_definition{smt_core_theoryt::equal(
119 smt_array_theoryt::select(array_identifier, index),
120 convert_expr_to_smt(elements.at(i)))};
121 solver_process->send(element_definition);
122 }
123}
124
126 const array_of_exprt &array,
127 const smt_identifier_termt &array_identifier)
128{
129 const smt_sortt index_type =
131 const smt_identifier_termt array_index_identifier{
132 id2string(array_identifier.identifier()) + "_index", index_type};
133 const smt_termt element_value = convert_expr_to_smt(array.what());
134
135 const smt_assert_commandt elements_definition{smt_forall_termt{
136 {array_index_identifier},
138 smt_array_theoryt::select(array_identifier, array_index_identifier),
139 element_value)}};
140 solver_process->send(elements_definition);
141}
142
144 const string_constantt &string,
145 const smt_identifier_termt &array_identifier)
146{
147 initialize_array_elements(string.to_array_expr(), array_identifier);
148}
149
150template <typename t_exprt>
152 const t_exprt &array)
153{
154 const smt_sortt array_sort = convert_type_to_smt_sort(array.type());
155 INVARIANT(
156 array_sort.cast<smt_array_sortt>(),
157 "Converting array typed expression to SMT should result in a term of array "
158 "sort.");
159 const smt_identifier_termt array_identifier{
160 "array_" + std::to_string(array_sequence()), array_sort};
161 solver_process->send(smt_declare_function_commandt{array_identifier, {}});
162 initialize_array_elements(array, array_identifier);
163 expression_identifiers.emplace(array, array_identifier);
164}
165
167 const exprt &expr,
168 const irep_idt &symbol_identifier,
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)
173{
174 const smt_declare_function_commandt function{
176 symbol_identifier, convert_type_to_smt_sort(expr.type())),
177 {}};
178 expression_identifiers.emplace(expr, function.identifier());
179 identifier_table.emplace(symbol_identifier, function.identifier());
180 solver_process->send(function);
181}
182
186 const exprt &expr)
187{
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;
192 });
193 std::stack<exprt> to_be_defined;
194 const auto push_dependencies_needed = [&](const exprt &expr) {
195 bool result = false;
196 for(const auto &dependency : gather_dependent_expressions(expr))
197 {
198 if(!seen_expressions.insert(dependency).second)
199 continue;
200 result = true;
201 to_be_defined.push(dependency);
202 }
203 return result;
204 };
205 push_dependencies_needed(expr);
206 while(!to_be_defined.empty())
207 {
208 const exprt current = to_be_defined.top();
209 if(push_dependencies_needed(current))
210 continue;
211 if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
212 {
213 const irep_idt &identifier = symbol_expr->get_identifier();
214 const symbolt *symbol = nullptr;
215 if(ns.lookup(identifier, symbol) || symbol->value.is_nil())
216 {
218 *symbol_expr,
219 symbol_expr->get_identifier(),
223 }
224 else
225 {
226 const exprt lowered = lower(symbol->value);
227 if(push_dependencies_needed(lowered))
228 continue;
229 const smt_define_function_commandt function{
230 symbol->name, {}, convert_expr_to_smt(lowered)};
231 expression_identifiers.emplace(*symbol_expr, function.identifier());
232 identifier_table.emplace(identifier, function.identifier());
233 solver_process->send(function);
234 }
235 }
236 else if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
237 define_array_function(*array_expr);
238 else if(
239 const auto array_of_expr = expr_try_dynamic_cast<array_of_exprt>(current))
240 {
241 define_array_function(*array_of_expr);
242 }
243 else if(
244 const auto string = expr_try_dynamic_cast<string_constantt>(current))
245 {
246 define_array_function(*string);
247 }
248 else if(
249 const auto nondet_symbol =
251 {
253 *nondet_symbol,
254 nondet_symbol->get_identifier(),
258 }
259 to_be_defined.pop();
260 }
261}
262
266 exprt expr,
267 const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
268 &expression_identifiers)
269{
270 expr.visit_pre([&](exprt &node) -> void {
271 auto find_result = expression_identifiers.find(node);
272 if(find_result == expression_identifiers.cend())
273 return;
274 const auto type = find_result->first.type();
275 node = symbol_exprt{find_result->second.identifier(), type};
276 });
277 return expr;
278}
279
281 const namespacet &_ns,
282 std::unique_ptr<smt_base_solver_processt> _solver_process,
283 message_handlert &message_handler)
284 : ns{_ns},
285 number_of_solver_calls{0},
286 solver_process(std::move(_solver_process)),
287 log{message_handler},
288 object_map{initial_smt_object_map()},
289 struct_encoding{_ns}
290{
293 solver_process->send(smt_set_logic_commandt{smt_logic_allt{}});
296}
297
299{
300 expr.visit_pre([&ns](exprt &expr) {
301 if(
302 auto prophecy_r_or_w_ok =
304 {
305 expr = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns);
306 }
307 else if(
308 auto prophecy_pointer_in_range =
310 {
311 expr = simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
312 }
313 });
314 return expr;
315}
316
318 const exprt &in_expr)
319{
320 if(
321 expression_handle_identifiers.find(in_expr) !=
323 {
324 return;
325 }
326
327 const exprt lowered_expr = lower(in_expr);
328
329 define_dependent_functions(lowered_expr);
331 "B" + std::to_string(handle_sequence()),
332 {},
333 convert_expr_to_smt(lowered_expr)};
334 expression_handle_identifiers.emplace(in_expr, function.identifier());
335 identifier_table.emplace(
336 function.identifier().identifier(), function.identifier());
337 solver_process->send(function);
338}
339
341 const exprt &expr)
342{
343 expr.visit_pre([&](const exprt &expr_node) {
344 if(!can_cast_type<array_typet>(expr_node.type()))
345 return;
346 if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
347 {
348 for(auto operand_ite = ++with_expr->operands().begin();
349 operand_ite != with_expr->operands().end();
350 operand_ite += 2)
351 {
352 const auto index_expr = *operand_ite;
353 const auto index_term = convert_expr_to_smt(index_expr);
354 const auto index_identifier =
355 "index_" + std::to_string(index_sequence());
356 const auto index_definition =
357 smt_define_function_commandt{index_identifier, {}, index_term};
359 index_expr, index_definition.identifier());
360 identifier_table.emplace(
361 index_identifier, index_definition.identifier());
363 smt_define_function_commandt{index_identifier, {}, index_term});
364 }
365 }
366 });
367}
368
370 exprt root_expr)
371{
372 root_expr.visit_pre([&](exprt &node) {
374 {
375 const auto instance = "padding_" + std::to_string(padding_sequence());
376 const auto term =
379 node = symbol_exprt{instance, node.type()};
380 }
381 });
382 return root_expr;
383}
384
406
408{
410 debug << "`handle` -\n " << expr.pretty(2, 0) << messaget::eom;
411 });
413 return expr;
414}
415
418{
419 // Lookup the non-lowered form first.
420 const auto handle_find_result = expression_handle_identifiers.find(expr);
421 if(handle_find_result != expression_handle_identifiers.cend())
422 return handle_find_result->second;
423 const auto expr_find_result = expression_identifiers.find(expr);
424 if(expr_find_result != expression_identifiers.cend())
425 return expr_find_result->second;
426
427 // If that didn't yield any results, then try the lowered form.
428 const exprt lowered_expr = lower(expr);
429 const auto lowered_handle_find_result =
430 expression_handle_identifiers.find(lowered_expr);
431 if(lowered_handle_find_result != expression_handle_identifiers.cend())
432 return lowered_handle_find_result->second;
433 const auto lowered_expr_find_result =
434 expression_identifiers.find(lowered_expr);
435 if(lowered_expr_find_result != expression_identifiers.cend())
436 return lowered_expr_find_result->second;
437 return {};
438}
439
441 const smt_termt &array,
442 const array_typet &type) const
443{
444 INVARIANT(
445 type.is_complete(), "Array size is required for getting array values.");
446 const auto size = numeric_cast<std::size_t>(get(type.size()));
447 INVARIANT(
448 size,
449 "Size of array must be convertible to std::size_t for getting array value");
450 std::vector<exprt> elements;
451 const auto index_type = type.index_type();
452 elements.reserve(*size);
453 for(std::size_t index = 0; index < size; ++index)
454 {
455 const auto index_term = ::convert_expr_to_smt(
456 from_integer(index, index_type),
461 auto element = get_expr(
462 smt_array_theoryt::select(array, index_term), type.element_type());
463 if(!element)
464 return {};
465 elements.push_back(std::move(*element));
466 }
467 return array_exprt{elements, type};
468}
469
471 const smt_termt &struct_term,
472 const struct_tag_typet &type) const
473{
474 const auto encoded_result =
475 get_expr(struct_term, struct_encoding.encode(type));
476 if(!encoded_result)
477 return {};
478 return {struct_encoding.decode(*encoded_result, type)};
479}
480
482 const smt_termt &descriptor,
483 const typet &type) const
484{
485 if(const auto array_type = type_try_dynamic_cast<array_typet>(type))
486 {
487 if(array_type->is_incomplete())
488 return {};
489 return get_expr(descriptor, *array_type);
490 }
491 if(const auto struct_type = type_try_dynamic_cast<struct_tag_typet>(type))
492 {
493 return get_expr(descriptor, *struct_type);
494 }
495 const smt_get_value_commandt get_value_command{descriptor};
496 const smt_responset response = get_response_to_command(
497 *solver_process, get_value_command, identifier_table);
498 const auto get_value_response = response.cast<smt_get_value_responset>();
499 if(!get_value_response)
500 {
502 "Expected get-value response from solver, but received - " +
503 response.pretty()};
504 }
505 if(get_value_response->pairs().size() > 1)
506 {
508 "Expected single valuation pair in get-value response from solver, but "
509 "received multiple pairs - " +
510 response.pretty()};
511 }
513 get_value_response->pairs()[0].get().value(), type, ns);
514}
515
516// This is a fall back which builds resulting expression based on getting the
517// values of its operands. It is used during trace building in the case where
518// certain kinds of expression appear on the left hand side of an
519// assignment. For example in the following trace assignment -
520// `byte_extract_little_endian(x, offset) = 1`
521// `::get` will be called on `byte_extract_little_endian(x, offset)` and
522// we build a resulting expression where `x` and `offset` are substituted
523// with their values.
525 const exprt &expr,
526 const stack_decision_proceduret &decision_procedure)
527{
528 exprt copy = expr;
529 for(auto &op : copy.operands())
530 {
531 exprt eval_op = decision_procedure.get(op);
532 if(eval_op.is_nil())
533 return nil_exprt{};
534 op = std::move(eval_op);
535 }
536 return copy;
537}
538
540{
542 debug << "`get` - \n " + expr.pretty(2, 0) << messaget::eom;
543 });
544 auto descriptor = [&]() -> optionalt<smt_termt> {
545 if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
546 {
547 const auto array = get_identifier(index_expr->array());
548 const auto index = get_identifier(index_expr->index());
549 if(!array || !index)
550 return {};
551 return smt_array_theoryt::select(*array, *index);
552 }
553 if(auto identifier_descriptor = get_identifier(expr))
554 {
555 return identifier_descriptor;
556 }
557 const exprt lowered = lower(expr);
558 if(gather_dependent_expressions(lowered).empty())
559 {
560 INVARIANT(
562 "Objects in expressions being read should already be tracked from "
563 "point of being set/handled.");
564 return ::convert_expr_to_smt(
565 lowered,
570 }
571 return {};
572 }();
573 if(!descriptor)
574 {
577 "symbol expressions must have a known value",
579 return build_expr_based_on_getting_operands(expr, *this);
580 }
581 if(auto result = get_expr(*descriptor, expr.type()))
582 return std::move(*result);
583 return expr;
584}
585
587 std::ostream &out) const
588{
589 UNIMPLEMENTED_FEATURE("printing of assignments.");
590}
591
592std::string
594{
595 return "incremental SMT2 solving via " + solver_process->description();
596}
597
598std::size_t
603
605 const exprt &in_expr,
606 bool value)
607{
609 debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n "
610 << in_expr.pretty(2, 0) << messaget::eom;
611 });
612 const exprt lowered_expr = lower(in_expr);
614
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;
621 else
622 return convert_expr_to_smt(lowered_expr);
623 }();
624 if(!value)
625 converted_term = smt_core_theoryt::make_not(converted_term);
626 solver_process->send(smt_assert_commandt{converted_term});
627}
628
630 const std::vector<exprt> &assumptions)
631{
632 for(const auto &assumption : assumptions)
633 {
635 "pushing of assumption:\n " + assumption.pretty(2, 0));
636 }
637 UNIMPLEMENTED_FEATURE("`push` of empty assumptions.");
638}
639
644
649
662
664{
666 for(const auto &key_value : object_map)
667 {
668 const decision_procedure_objectt &object = key_value.second;
669 if(object_properties_defined[object.unique_id])
670 continue;
671 else
672 object_properties_defined[object.unique_id] = true;
673 define_dependent_functions(object.size);
675 object.unique_id, convert_expr_to_smt(object.size)));
677 object.unique_id, object.is_dynamic));
678 }
679}
680
682{
683 const exprt lowered = struct_encoding.encode(lower_enum(
685 ns));
687 if(lowered != expression)
688 debug << "lowered to -\n " << lowered.pretty(2, 0) << messaget::eom;
689 });
690 return lowered;
691}
692
694{
699 if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
700 {
701 if(check_sat_response->kind().cast<smt_unknown_responset>())
702 log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
703 return lookup_decision_procedure_result(check_sat_response->kind());
704 }
705 if(const auto problem = get_problem_messages(result))
706 throw analysis_exceptiont{*problem};
707 throw analysis_exceptiont{"Unexpected kind of response from SMT solver."};
708}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
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()
Definition c_types.cpp:22
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:1563
const array_typet & type() const
Definition std_expr.h:1570
Array constructor from single element.
Definition std_expr.h:1498
const array_typet & type() const
Definition std_expr.h:1505
exprt & what()
Definition std_expr.h:1515
Arrays with given size.
Definition std_types.h:763
typet index_type() const
The type of the index expressions into any instance of this type.
Definition std_types.cpp:33
bool is_complete() const
Definition std_types.h:808
const exprt & size() const
Definition std_types.h:796
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:783
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.
Definition dstring.h:39
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
operandst & operands()
Definition expr.h:94
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:490
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
bool is_nil() const
Definition irep.h:376
mstreamt & error() const
Definition message.h:399
mstreamt & debug() const
Definition message.h:429
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:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3026
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,...
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.
Definition smt_terms.h:94
irep_idt identifier() const
Definition smt_terms.cpp:81
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:490
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.
Definition std_types.h:449
Expression to hold a symbol (variable)
Definition std_expr.h:113
Symbol table entry.
Definition symbol.h:28
irep_idt name
The unique identifier.
Definition symbol.h:40
exprt value
Initial value of symbol.
Definition symbol.h:34
The type of an expression, extends irept.
Definition type.h:29
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.
Definition expr_cast.h:135
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.
Definition expr_cast.h:81
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
STL namespace.
#define NODISCARD
Definition nodiscard.h:22
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
Definition optional.h:35
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:524
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)
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:1603
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition std_expr.h:1527
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition std_expr.h:277
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:206
bool can_cast_expr< array_exprt >(const exprt &base)
Definition std_expr.h:1592
bool can_cast_type< bool_typet >(const typet &base)
Definition std_types.h:44
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
Definition std_types.h:831
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition std_types.h:731
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.
Symbol table entry.
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.