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>
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);
38 if(response.cast<smt_success_responset>())
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 }
54 if(response.cast<smt_unsupported_responset>())
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(
85 can_cast_expr<symbol_exprt>(expr_node) ||
86 can_cast_expr<array_exprt>(expr_node) ||
90 {
91 dependent_expressions.push_back(expr_node);
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.
98 const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr_node);
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 }
104 return dependent_expressions;
105}
106
108 const array_exprt &array,
109 const smt_identifier_termt &array_identifier)
110{
111 identifier_table.emplace(array_identifier.identifier(), array_identifier);
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));
117 const smt_assert_commandt element_definition{smt_core_theoryt::equal(
118 smt_array_theoryt::select(array_identifier, index),
119 convert_expr_to_smt(elements.at(i)))};
120 solver_process->send(element_definition);
121 }
122}
123
125 const array_of_exprt &array,
126 const smt_identifier_termt &array_identifier)
127{
128 const smt_sortt index_type =
130 const smt_identifier_termt array_index_identifier{
131 id2string(array_identifier.identifier()) + "_index", index_type};
132 const smt_termt element_value = convert_expr_to_smt(array.what());
133
134 const smt_assert_commandt elements_definition{smt_forall_termt{
135 {array_index_identifier},
137 smt_array_theoryt::select(array_identifier, array_index_identifier),
138 element_value)}};
139 solver_process->send(elements_definition);
140}
141
143 const string_constantt &string,
144 const smt_identifier_termt &array_identifier)
145{
146 initialize_array_elements(string.to_array_expr(), array_identifier);
147}
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(
155 array_sort.cast<smt_array_sortt>(),
156 "Converting array typed expression to SMT should result in a term of array "
157 "sort.");
158 const smt_identifier_termt array_identifier{
159 "array_" + std::to_string(array_sequence()), array_sort};
160 solver_process->send(smt_declare_function_commandt{array_identifier, {}});
161 initialize_array_elements(array, array_identifier);
162 expression_identifiers.emplace(array, array_identifier);
163}
164
166 const exprt &expr,
167 const irep_idt &symbol_identifier,
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{
175 symbol_identifier, convert_type_to_smt_sort(expr.type())),
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;
200 to_be_defined.push(dependency);
201 }
202 return result;
203 };
204 push_dependencies_needed(expr);
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))
220 define_array_function(*array_expr);
221 else if(
222 const auto array_of_expr = expr_try_dynamic_cast<array_of_exprt>(current))
223 {
224 define_array_function(*array_of_expr);
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 {
236 *nondet_symbol,
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{
276 solver_process->send(smt_set_logic_commandt{smt_logic_allt{}});
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(
291 auto prophecy_pointer_in_range =
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(
315 expression_handle_identifiers.find(in_expr) !=
317 {
318 return;
319 }
320
321 const exprt lowered_expr = lower(in_expr);
322
323 define_dependent_functions(lowered_expr);
325 "B" + std::to_string(handle_sequence()),
326 {},
327 convert_expr_to_smt(lowered_expr)};
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_pre([&](const exprt &expr_node) {
338 if(!can_cast_type<array_typet>(expr_node.type()))
339 return;
340 if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
341 {
342 for(auto operand_ite = ++with_expr->operands().begin();
343 operand_ite != with_expr->operands().end();
344 operand_ite += 2)
345 {
346 const auto index_expr = *operand_ite;
347 const auto index_term = convert_expr_to_smt(index_expr);
348 const auto index_identifier =
349 "index_" + std::to_string(index_sequence());
350 const auto index_definition =
351 smt_define_function_commandt{index_identifier, {}, index_term};
353 index_expr, index_definition.identifier());
354 identifier_table.emplace(
355 index_identifier, index_definition.identifier());
357 smt_define_function_commandt{index_identifier, {}, index_term});
358 }
359 }
360 });
361}
362
364 exprt root_expr)
365{
366 root_expr.visit_pre([&](exprt &node) {
368 {
369 const auto instance = "padding_" + std::to_string(padding_sequence());
370 const auto term =
373 node = symbol_exprt{instance, node.type()};
374 }
375 });
376 return root_expr;
377}
378
400
402{
404 debug << "`handle` -\n " << expr.pretty(2, 0) << messaget::eom;
405 });
407 return expr;
408}
409
410std::optional<smt_termt>
412{
413 // Lookup the non-lowered form first.
414 const auto handle_find_result = expression_handle_identifiers.find(expr);
415 if(handle_find_result != expression_handle_identifiers.cend())
416 return handle_find_result->second;
417 const auto expr_find_result = expression_identifiers.find(expr);
418 if(expr_find_result != expression_identifiers.cend())
419 return expr_find_result->second;
420
421 // If that didn't yield any results, then try the lowered form.
422 const exprt lowered_expr = lower(expr);
423 const auto lowered_handle_find_result =
424 expression_handle_identifiers.find(lowered_expr);
425 if(lowered_handle_find_result != expression_handle_identifiers.cend())
426 return lowered_handle_find_result->second;
427 const auto lowered_expr_find_result =
428 expression_identifiers.find(lowered_expr);
429 if(lowered_expr_find_result != expression_identifiers.cend())
430 return lowered_expr_find_result->second;
431 return {};
432}
433
435 const smt_termt &array,
436 const array_typet &type) const
437{
438 INVARIANT(
439 type.is_complete(), "Array size is required for getting array values.");
440 const auto size = numeric_cast<std::size_t>(get(type.size()));
441 INVARIANT(
442 size,
443 "Size of array must be convertible to std::size_t for getting array value");
444 std::vector<exprt> elements;
445 const auto index_type = type.index_type();
446 elements.reserve(*size);
447 for(std::size_t index = 0; index < size; ++index)
448 {
449 const auto index_term = ::convert_expr_to_smt(
450 from_integer(index, index_type),
455 auto element = get_expr(
456 smt_array_theoryt::select(array, index_term), type.element_type());
457 if(!element)
458 return {};
459 elements.push_back(std::move(*element));
460 }
461 return array_exprt{elements, type};
462}
463
465 const smt_termt &struct_term,
466 const struct_tag_typet &type) const
467{
468 const auto encoded_result =
469 get_expr(struct_term, struct_encoding.encode(type));
470 if(!encoded_result)
471 return {};
472 return {struct_encoding.decode(*encoded_result, type)};
473}
474
476 const smt_termt &union_term,
477 const union_tag_typet &type) const
478{
479 const auto encoded_result =
480 get_expr(union_term, struct_encoding.encode(type));
481 if(!encoded_result)
482 return {};
483 return {struct_encoding.decode(*encoded_result, type)};
484}
485
487 const smt_termt &descriptor,
488 const typet &type) const
489{
490 if(const auto array_type = type_try_dynamic_cast<array_typet>(type))
491 {
492 if(array_type->is_incomplete())
493 return {};
494 return get_expr(descriptor, *array_type);
495 }
496 if(const auto struct_type = type_try_dynamic_cast<struct_tag_typet>(type))
497 {
498 return get_expr(descriptor, *struct_type);
499 }
500 if(const auto union_type = type_try_dynamic_cast<union_tag_typet>(type))
501 {
502 return get_expr(descriptor, *union_type);
503 }
504 const smt_get_value_commandt get_value_command{descriptor};
505 const smt_responset response = get_response_to_command(
506 *solver_process, get_value_command, identifier_table);
507 const auto get_value_response = response.cast<smt_get_value_responset>();
508 if(!get_value_response)
509 {
511 "Expected get-value response from solver, but received - " +
512 response.pretty()};
513 }
514 if(get_value_response->pairs().size() > 1)
515 {
517 "Expected single valuation pair in get-value response from solver, but "
518 "received multiple pairs - " +
519 response.pretty()};
520 }
522 get_value_response->pairs()[0].get().value(), type, ns);
523}
524
525// This is a fall back which builds resulting expression based on getting the
526// values of its operands. It is used during trace building in the case where
527// certain kinds of expression appear on the left hand side of an
528// assignment. For example in the following trace assignment -
529// `byte_extract_little_endian(x, offset) = 1`
530// `::get` will be called on `byte_extract_little_endian(x, offset)` and
531// we build a resulting expression where `x` and `offset` are substituted
532// with their values.
534 const exprt &expr,
535 const stack_decision_proceduret &decision_procedure)
536{
537 exprt copy = expr;
538 for(auto &op : copy.operands())
539 {
540 exprt eval_op = decision_procedure.get(op);
541 if(eval_op.is_nil())
542 return nil_exprt{};
543 op = std::move(eval_op);
544 }
545 return copy;
546}
547
549{
551 debug << "`get` - \n " + expr.pretty(2, 0) << messaget::eom;
552 });
553 auto descriptor = [&]() -> std::optional<smt_termt> {
554 if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
555 {
556 const auto array = get_identifier(index_expr->array());
557 const auto index = get_identifier(index_expr->index());
558 if(!array || !index)
559 return {};
560 return smt_array_theoryt::select(*array, *index);
561 }
562 if(auto identifier_descriptor = get_identifier(expr))
563 {
564 return identifier_descriptor;
565 }
566 const exprt lowered = lower(expr);
567 if(gather_dependent_expressions(lowered).empty())
568 {
569 INVARIANT(
571 "Objects in expressions being read should already be tracked from "
572 "point of being set/handled.");
573 return ::convert_expr_to_smt(
574 lowered,
579 }
580 return {};
581 }();
582 if(!descriptor)
583 {
586 "symbol expressions must have a known value",
588 return build_expr_based_on_getting_operands(expr, *this);
589 }
590 if(auto result = get_expr(*descriptor, expr.type()))
591 return std::move(*result);
592 return expr;
593}
594
596 std::ostream &out) const
597{
598 UNIMPLEMENTED_FEATURE("printing of assignments.");
599}
600
601std::string
603{
604 return "incremental SMT2 solving via " + solver_process->description();
605}
606
607std::size_t
612
614 const exprt &in_expr,
615 bool value)
616{
618 debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n "
619 << in_expr.pretty(2, 0) << messaget::eom;
620 });
621 const exprt lowered_expr = lower(in_expr);
623
624 define_dependent_functions(lowered_expr);
625 auto converted_term = [&]() -> smt_termt {
626 const auto expression_handle_identifier =
627 expression_handle_identifiers.find(lowered_expr);
628 if(expression_handle_identifier != expression_handle_identifiers.cend())
629 return expression_handle_identifier->second;
630 else
631 return convert_expr_to_smt(lowered_expr);
632 }();
633 if(!value)
634 converted_term = smt_core_theoryt::make_not(converted_term);
635 solver_process->send(smt_assert_commandt{converted_term});
636}
637
639 const std::vector<exprt> &assumptions)
640{
641 for(const auto &assumption : assumptions)
642 {
644 "pushing of assumption:\n " + assumption.pretty(2, 0));
645 }
646 UNIMPLEMENTED_FEATURE("`push` of empty assumptions.");
647}
648
653
658
659[[nodiscard]] static decision_proceduret::resultt
671
673{
675 for(const auto &key_value : object_map)
676 {
677 const decision_procedure_objectt &object = key_value.second;
678 if(object_properties_defined[object.unique_id])
679 continue;
680 else
681 object_properties_defined[object.unique_id] = true;
682 define_dependent_functions(object.size);
684 object.unique_id, convert_expr_to_smt(object.size)));
686 object.unique_id, object.is_dynamic));
687 }
688}
689
691{
695 ns),
696 ns));
698 if(lowered != expression)
699 debug << "lowered to -\n " << lowered.pretty(2, 0) << messaget::eom;
700 });
701 return lowered;
702}
703
706{
711 if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
712 {
713 if(check_sat_response->kind().cast<smt_unknown_responset>())
714 log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
715 return lookup_decision_procedure_result(check_sat_response->kind());
716 }
717 if(const auto problem = get_problem_messages(result))
718 throw analysis_exceptiont{*problem};
719 throw analysis_exceptiont{"Unexpected kind of response from SMT solver."};
720}
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.
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...
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
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:3086
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...
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
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition std_expr.h:1587
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:1654
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.