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/c_types.h>
8#include <util/range.h>
10#include <util/std_expr.h>
12
24
25#include <stack>
26#include <unordered_set>
27
31 smt_base_solver_processt &solver_process,
32 const smt_commandt &command,
33 const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
34{
35 solver_process.send(command);
36 auto response = solver_process.receive_response(identifier_table);
37 if(response.cast<smt_success_responset>())
38 return solver_process.receive_response(identifier_table);
39 else
40 return response;
41}
42
45static std::optional<std::string>
47{
48 if(const auto error = response.cast<smt_error_responset>())
49 {
50 return "SMT solver returned an error message - " +
51 id2string(error->message());
52 }
53 if(response.cast<smt_unsupported_responset>())
54 {
55 return {"SMT solver does not support given command."};
56 }
57 return {};
58}
59
72static std::vector<exprt> gather_dependent_expressions(const exprt &root_expr)
73{
74 std::vector<exprt> dependent_expressions;
75
76 std::stack<const exprt *> stack;
77 stack.push(&root_expr);
78
79 while(!stack.empty())
80 {
81 const exprt &expr_node = *stack.top();
82 stack.pop();
83 if(
84 can_cast_expr<symbol_exprt>(expr_node) ||
85 can_cast_expr<array_exprt>(expr_node) ||
89 {
90 dependent_expressions.push_back(expr_node);
91 }
92 // The decision procedure does not depend on the values inside address of
93 // code typed expressions. We can build the address without knowing the
94 // value at that memory location. In this case the hypothetical compiled
95 // machine instructions at the address are not relevant to solving, only
96 // representing *which* function a pointer points to is needed.
97 const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr_node);
98 if(address_of && can_cast_type<code_typet>(address_of->object().type()))
99 continue;
100 for(auto &operand : expr_node.operands())
101 stack.push(&operand);
102 }
103 return dependent_expressions;
104}
105
107 const array_exprt &array,
108 const smt_identifier_termt &array_identifier)
109{
110 identifier_table.emplace(array_identifier.identifier(), array_identifier);
111 const std::vector<exprt> &elements = array.operands();
112 const typet &index_type = array.type().index_type();
113 for(std::size_t i = 0; i < elements.size(); ++i)
114 {
115 const smt_termt index = convert_expr_to_smt(from_integer(i, index_type));
116 const smt_assert_commandt element_definition{smt_core_theoryt::equal(
117 smt_array_theoryt::select(array_identifier, index),
118 convert_expr_to_smt(elements.at(i)))};
119 solver_process->send(element_definition);
120 }
121}
122
124 const array_of_exprt &array,
125 const smt_identifier_termt &array_identifier)
126{
127 const smt_sortt index_type =
129 const smt_identifier_termt array_index_identifier{
130 id2string(array_identifier.identifier()) + "_index", index_type};
131 const smt_termt element_value = convert_expr_to_smt(array.what());
132
133 const smt_assert_commandt elements_definition{smt_forall_termt{
134 {array_index_identifier},
136 smt_array_theoryt::select(array_identifier, array_index_identifier),
137 element_value)}};
138 solver_process->send(elements_definition);
139}
140
142 const string_constantt &string,
143 const smt_identifier_termt &array_identifier)
144{
145 initialize_array_elements(string.to_array_expr(), array_identifier);
146}
147
148template <typename t_exprt>
150 const t_exprt &array)
151{
152 const smt_sortt array_sort = convert_type_to_smt_sort(array.type());
153 INVARIANT(
154 array_sort.cast<smt_array_sortt>(),
155 "Converting array typed expression to SMT should result in a term of array "
156 "sort.");
157 const smt_identifier_termt array_identifier{
158 "array_" + std::to_string(array_sequence()), array_sort};
159 solver_process->send(smt_declare_function_commandt{array_identifier, {}});
160 initialize_array_elements(array, array_identifier);
161 expression_identifiers.emplace(array, array_identifier);
162}
163
165 const exprt &expr,
166 const irep_idt &symbol_identifier,
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)
171{
172 const smt_declare_function_commandt function{
174 symbol_identifier, convert_type_to_smt_sort(expr.type())),
175 {}};
176 expression_identifiers.emplace(expr, function.identifier());
177 identifier_table.emplace(symbol_identifier, function.identifier());
178 solver_process->send(function);
179}
180
184 const exprt &expr)
185{
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;
190 });
191 std::stack<exprt> to_be_defined;
192 const auto push_dependencies_needed = [&](const exprt &expr) {
193 bool result = false;
194 for(const auto &dependency : gather_dependent_expressions(expr))
195 {
196 if(!seen_expressions.insert(dependency).second)
197 continue;
198 result = true;
199 to_be_defined.push(dependency);
200 }
201 return result;
202 };
203 push_dependencies_needed(expr);
204 while(!to_be_defined.empty())
205 {
206 const exprt current = to_be_defined.top();
207 if(push_dependencies_needed(current))
208 continue;
209 if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
210 {
212 *symbol_expr,
213 symbol_expr->get_identifier(),
217 }
218 else if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
219 define_array_function(*array_expr);
220 else if(
221 const auto array_of_expr = expr_try_dynamic_cast<array_of_exprt>(current))
222 {
223 define_array_function(*array_of_expr);
224 }
225 else if(
226 const auto string = expr_try_dynamic_cast<string_constantt>(current))
227 {
228 define_array_function(*string);
229 }
230 else if(
231 const auto nondet_symbol =
233 {
235 *nondet_symbol,
236 nondet_symbol->get_identifier(),
240 }
241 to_be_defined.pop();
242 }
243}
244
248 exprt expr,
249 const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
250 &expression_identifiers)
251{
252 expr.visit_pre([&](exprt &node) -> void {
253 auto find_result = expression_identifiers.find(node);
254 if(find_result == expression_identifiers.cend())
255 return;
256 const auto type = find_result->first.type();
257 node = symbol_exprt{find_result->second.identifier(), type};
258 });
259 return expr;
260}
261
263 const namespacet &_ns,
264 std::unique_ptr<smt_base_solver_processt> _solver_process,
265 message_handlert &message_handler)
266 : ns{_ns},
267 number_of_solver_calls{0},
268 solver_process(std::move(_solver_process)),
269 log{message_handler},
270 object_map{initial_smt_object_map()},
271 struct_encoding{_ns}
272{
275 solver_process->send(smt_set_logic_commandt{smt_logic_allt{}});
278}
279
281{
282 expr.visit_pre([&ns](exprt &expr) {
283 if(
284 auto prophecy_r_or_w_ok =
286 {
287 expr = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns);
288 }
289 else if(
290 auto prophecy_pointer_in_range =
292 {
293 expr = simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
294 }
295 });
296 return expr;
297}
298
300 const exprt &in_expr)
301{
302 if(
303 expression_handle_identifiers.find(in_expr) !=
305 {
306 return;
307 }
308
309 const exprt lowered_expr = lower(in_expr);
310
311 define_dependent_functions(lowered_expr);
313 "B" + std::to_string(handle_sequence()),
314 {},
315 convert_expr_to_smt(lowered_expr)};
316 expression_handle_identifiers.emplace(in_expr, function.identifier());
317 identifier_table.emplace(
318 function.identifier().identifier(), function.identifier());
319 solver_process->send(function);
320}
321
323 const exprt &expr)
324{
325 expr.visit_pre([&](const exprt &expr_node) {
326 if(!can_cast_type<array_typet>(expr_node.type()))
327 return;
328 if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
329 {
330 for(auto operand_ite = ++with_expr->operands().begin();
331 operand_ite != with_expr->operands().end();
332 operand_ite += 2)
333 {
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};
341 index_expr, index_definition.identifier());
342 identifier_table.emplace(
343 index_identifier, index_definition.identifier());
345 smt_define_function_commandt{index_identifier, {}, index_term});
346 }
347 }
348 });
349}
350
352 exprt root_expr)
353{
354 root_expr.visit_pre([&](exprt &node) {
356 {
357 const auto instance = "padding_" + std::to_string(padding_sequence());
358 const auto term =
361 node = symbol_exprt{instance, node.type()};
362 }
363 });
364 return root_expr;
365}
366
388
390{
392 debug << "`handle` -\n " << expr.pretty(2, 0) << messaget::eom;
393 });
395 return expr;
396}
397
398std::optional<smt_termt>
400{
401 // Lookup the non-lowered form first.
402 const auto handle_find_result = expression_handle_identifiers.find(expr);
403 if(handle_find_result != expression_handle_identifiers.cend())
404 return handle_find_result->second;
405 const auto expr_find_result = expression_identifiers.find(expr);
406 if(expr_find_result != expression_identifiers.cend())
407 return expr_find_result->second;
408
409 // If that didn't yield any results, then try the lowered form.
410 const exprt lowered_expr = lower(expr);
411 const auto lowered_handle_find_result =
412 expression_handle_identifiers.find(lowered_expr);
413 if(lowered_handle_find_result != expression_handle_identifiers.cend())
414 return lowered_handle_find_result->second;
415 const auto lowered_expr_find_result =
416 expression_identifiers.find(lowered_expr);
417 if(lowered_expr_find_result != expression_identifiers.cend())
418 return lowered_expr_find_result->second;
419 return {};
420}
421
423 const smt_termt &array,
424 const array_typet &type) const
425{
426 INVARIANT(
427 type.is_complete(), "Array size is required for getting array values.");
428 const auto size = numeric_cast<std::size_t>(get(type.size()));
429 INVARIANT(
430 size,
431 "Size of array must be convertible to std::size_t for getting array value");
432 std::vector<exprt> elements;
433 const auto index_type = type.index_type();
434 elements.reserve(*size);
435 for(std::size_t index = 0; index < size; ++index)
436 {
437 const auto index_term = ::convert_expr_to_smt(
438 from_integer(index, index_type),
443 auto element = get_expr(
444 smt_array_theoryt::select(array, index_term), type.element_type());
445 if(!element)
446 return {};
447 elements.push_back(std::move(*element));
448 }
449 return array_exprt{elements, type};
450}
451
453 const smt_termt &struct_term,
454 const struct_tag_typet &type) const
455{
456 const auto encoded_result =
457 get_expr(struct_term, struct_encoding.encode(type));
458 if(!encoded_result)
459 return {};
460 return {struct_encoding.decode(*encoded_result, type)};
461}
462
464 const smt_termt &union_term,
465 const union_tag_typet &type) const
466{
467 const auto encoded_result =
468 get_expr(union_term, struct_encoding.encode(type));
469 if(!encoded_result)
470 return {};
471 return {struct_encoding.decode(*encoded_result, type)};
472}
473
475 const smt_termt &descriptor,
476 const typet &type) const
477{
478 if(const auto array_type = type_try_dynamic_cast<array_typet>(type))
479 {
480 if(array_type->is_incomplete())
481 return {};
482 return get_expr(descriptor, *array_type);
483 }
484 if(const auto struct_type = type_try_dynamic_cast<struct_tag_typet>(type))
485 {
486 return get_expr(descriptor, *struct_type);
487 }
488 if(const auto union_type = type_try_dynamic_cast<union_tag_typet>(type))
489 {
490 return get_expr(descriptor, *union_type);
491 }
492 const smt_get_value_commandt get_value_command{descriptor};
493 const smt_responset response = get_response_to_command(
494 *solver_process, get_value_command, identifier_table);
495 const auto get_value_response = response.cast<smt_get_value_responset>();
496 if(!get_value_response)
497 {
499 "Expected get-value response from solver, but received - " +
500 response.pretty()};
501 }
502 if(get_value_response->pairs().size() > 1)
503 {
505 "Expected single valuation pair in get-value response from solver, but "
506 "received multiple pairs - " +
507 response.pretty()};
508 }
510 get_value_response->pairs()[0].get().value(), type, ns);
511}
512
513// This is a fall back which builds resulting expression based on getting the
514// values of its operands. It is used during trace building in the case where
515// certain kinds of expression appear on the left hand side of an
516// assignment. For example in the following trace assignment -
517// `byte_extract_little_endian(x, offset) = 1`
518// `::get` will be called on `byte_extract_little_endian(x, offset)` and
519// we build a resulting expression where `x` and `offset` are substituted
520// with their values.
522 const exprt &expr,
523 const stack_decision_proceduret &decision_procedure)
524{
525 exprt copy = expr;
526 for(auto &op : copy.operands())
527 {
528 exprt eval_op = decision_procedure.get(op);
529 if(eval_op.is_nil())
530 return nil_exprt{};
531 op = std::move(eval_op);
532 }
533 return copy;
534}
535
537{
539 debug << "`get` - \n " + expr.pretty(2, 0) << messaget::eom;
540 });
541 auto descriptor = [&]() -> std::optional<smt_termt> {
542 if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
543 {
544 const auto array = get_identifier(index_expr->array());
545 const auto index = get_identifier(index_expr->index());
546 if(!array || !index)
547 return {};
548 return smt_array_theoryt::select(*array, *index);
549 }
550 if(auto identifier_descriptor = get_identifier(expr))
551 {
552 return identifier_descriptor;
553 }
554 const exprt lowered = lower(expr);
555 if(gather_dependent_expressions(lowered).empty())
556 {
557 INVARIANT(
559 "Objects in expressions being read should already be tracked from "
560 "point of being set/handled.");
561 return ::convert_expr_to_smt(
562 lowered,
567 }
568 return {};
569 }();
570 if(!descriptor)
571 {
574 "symbol expressions must have a known value",
576 return build_expr_based_on_getting_operands(expr, *this);
577 }
578 if(auto result = get_expr(*descriptor, expr.type()))
579 return std::move(*result);
580 return expr;
581}
582
584 std::ostream &out) const
585{
586 UNIMPLEMENTED_FEATURE("printing of assignments.");
587}
588
589std::string
591{
592 return "incremental SMT2 solving via " + solver_process->description();
593}
594
595std::size_t
600
602 const exprt &in_expr,
603 bool value)
604{
606 debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n "
607 << in_expr.pretty(2, 0) << messaget::eom;
608 });
609 const exprt lowered_expr = lower(in_expr);
611
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;
618 else
619 return convert_expr_to_smt(lowered_expr);
620 }();
621 if(!value)
622 converted_term = smt_core_theoryt::make_not(converted_term);
623 solver_process->send(smt_assert_commandt{converted_term});
624}
625
627 const std::vector<exprt> &assumptions)
628{
629 for(const auto &assumption : assumptions)
630 {
632 "pushing of assumption:\n " + assumption.pretty(2, 0));
633 }
634 UNIMPLEMENTED_FEATURE("`push` of empty assumptions.");
635}
636
641
646
647[[nodiscard]] static decision_proceduret::resultt
659
661{
663 for(const auto &key_value : object_map)
664 {
665 const decision_procedure_objectt &object = key_value.second;
666 if(object_properties_defined[object.unique_id])
667 continue;
668 else
669 object_properties_defined[object.unique_id] = true;
670 define_dependent_functions(object.size);
672 object.unique_id, convert_expr_to_smt(object.size)));
674 object.unique_id, object.is_dynamic));
675 }
676}
677
679{
680 const exprt lowered = struct_encoding.encode(lower_enum(
682 ns));
684 if(lowered != expression)
685 debug << "lowered to -\n " << lowered.pretty(2, 0) << messaget::eom;
686 });
687 return lowered;
688}
689
692{
697 if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
698 {
699 if(check_sat_response->kind().cast<smt_unknown_responset>())
700 log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
701 return lookup_decision_procedure_result(check_sat_response->kind());
702 }
703 if(const auto problem = get_problem_messages(result))
704 throw analysis_exceptiont{*problem};
705 throw analysis_exceptiont{"Unexpected kind of response from SMT solver."};
706}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::optional< 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...
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:1616
const array_typet & type() const
Definition std_expr.h:1623
Array constructor from single element.
Definition std_expr.h:1553
const array_typet & type() const
Definition std_expr.h:1560
exprt & what()
Definition std_expr.h:1570
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:33
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
operandst & operands()
Definition expr.h:94
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
bool is_nil() const
Definition irep.h:368
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:94
The NIL expression.
Definition std_expr.h:3073
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.
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.
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:93
irep_idt identifier() const
Definition smt_terms.cpp:81
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
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: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.
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:44
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...
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:1660
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition std_expr.h:1582
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition std_expr.h:327
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:256
bool can_cast_expr< array_exprt >(const exprt &base)
Definition std_expr.h:1649
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:875
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition std_types.h:775
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.