CBMC
Loading...
Searching...
No Matches
abstract_environment.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6
7\*******************************************************************/
8
9#include <util/expr_util.h>
10#include <util/namespace.h>
11#include <util/simplify_expr.h>
12#include <util/simplify_utils.h>
13#include <util/symbol_table.h>
14
17
18#include <algorithm>
19#include <map>
20#include <ostream>
21#include <stack>
22
23#ifdef DEBUG
24# include <iostream>
25#endif
26
30
31typedef exprt (
33
34static exprt
35assume_not(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
36static exprt
37assume_or(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
38static exprt
39assume_and(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
40static exprt
41assume_eq(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
42static exprt assume_noteq(
44 const exprt &expr,
45 const namespacet &ns);
48 const exprt &expr,
49 const namespacet &ns);
52 const exprt &expr,
53 const namespacet &ns);
54
56static bool is_value(const abstract_object_pointert &obj);
57
58std::vector<abstract_object_pointert> eval_operands(
59 const exprt &expr,
61 const namespacet &ns);
62
63bool is_ptr_diff(const exprt &expr)
64{
65 return (expr.id() == ID_minus) &&
66 (expr.operands()[0].type().id() == ID_pointer) &&
67 (expr.operands()[1].type().id() == ID_pointer);
68}
69
70bool is_ptr_comparison(const exprt &expr)
71{
72 auto const &id = expr.id();
73 bool is_comparison = id == ID_equal || id == ID_notequal || id == ID_lt ||
74 id == ID_le || id == ID_gt || id == ID_ge;
75
76 return is_comparison && (expr.operands()[0].type().id() == ID_pointer) &&
77 (expr.operands()[1].type().id() == ID_pointer);
78}
79
80static bool is_access_expr(const exprt &expr)
81{
83 return is_access_expr(tc->op());
84
85 return expr.id() == ID_member || expr.id() == ID_index ||
86 expr.id() == ID_dereference;
87}
88
89static bool is_object_creation(const irep_idt &id)
90{
91 return id == ID_array || id == ID_struct || id == ID_constant ||
92 id == ID_address_of;
93}
94
95static bool is_dynamic_allocation(const exprt &expr)
96{
97 return expr.id() == ID_side_effect && expr.get(ID_statement) == ID_allocate;
98}
99
101abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
102{
103 if(bottom)
104 return abstract_object_factory(expr.type(), ns, false, true);
105
106 // first try to canonicalise, including constant folding
107 const exprt &simplified_expr = simplify_expr(expr, ns);
108
109 const irep_idt simplified_id = simplified_expr.id();
111 return resolve_symbol(simplified_expr, ns);
112
113 if(
114 is_access_expr(simplified_expr) || is_ptr_diff(simplified_expr) ||
115 is_ptr_comparison(simplified_expr))
116 {
117 auto const operands = eval_operands(simplified_expr, *this, ns);
118 auto const &target = operands.front();
119
120 return target->expression_transform(simplified_expr, operands, *this, ns);
121 }
122
124 return abstract_object_factory(simplified_expr.type(), simplified_expr, ns);
125
126 if(is_dynamic_allocation(simplified_expr))
129 exprt(ID_dynamic_object, simplified_expr.type()),
130 ns);
131
132 // No special handling required by the abstract environment
133 // delegate to the abstract object
134 if(!simplified_expr.operands().empty())
135 return eval_expression(simplified_expr, ns);
136
137 // It is important that this is top as the abstract object may not know
138 // how to handle the expression
139 return abstract_object_factory(simplified_expr.type(), ns, true, false);
140}
141
143 const exprt &expr,
144 const namespacet &ns) const
145{
146 const symbol_exprt &symbol(to_symbol_expr(expr));
147 const auto symbol_entry = map.find(symbol.get_identifier());
148
149 if(symbol_entry.has_value())
150 return symbol_entry.value();
151 return abstract_object_factory(expr.type(), ns, true, false);
152}
153
155 const exprt &expr,
156 const abstract_object_pointert &value,
157 const namespacet &ns)
158{
159 PRECONDITION(value);
160
161 if(value->is_bottom())
162 {
163 bool bottom_at_start = this->is_bottom();
164 this->make_bottom();
165 return !bottom_at_start;
166 }
167
169 // Build a stack of index, member and dereference accesses which
170 // we will work through the relevant abstract objects
171 exprt s = expr;
172 std::stack<exprt> stactions; // I'm not a continuation, honest guv'
173 while(s.id() != ID_symbol)
174 {
175 if(
176 s.id() == ID_index || s.id() == ID_member || s.id() == ID_dereference ||
177 s.id() == ID_typecast)
178 {
179 stactions.push(s);
180 s = s.operands()[0];
181 }
182 else
183 {
184 lhs_value = eval(s, ns);
185 break;
186 }
187 }
188
189 if(!lhs_value)
190 {
191 INVARIANT(s.id() == ID_symbol, "Have a symbol or a stack");
192 lhs_value = resolve_symbol(s, ns);
193 }
194
196
197 // This is the root abstract object that is in the map of abstract objects
198 // It might not have the same type as value if the above stack isn't empty
199
200 if(!stactions.empty())
201 {
202 // The symbol is not in the map - it is therefore top
203 final_value = write(lhs_value, value, stactions, ns, false);
204 }
205 else
206 {
207 // If we don't have a symbol on the LHS, then we must have some expression
208 // that we can write to (i.e. a pointer, an array, a struct) This appears
209 // to be none of that.
210 if(s.id() != ID_symbol)
211 {
212 throw std::runtime_error("invalid l-value");
213 }
214 // We can assign the AO directly to the symbol
215 final_value = value;
216 }
217
218 // Write the value for the root symbol back into the map
219 INVARIANT(
220 lhs_value->type() == final_value->type(),
221 "Assignment types must match"
222 "\n"
223 "lhs_type :" +
224 lhs_value->type().pretty() +
225 "\n"
226 "rhs_type :" +
227 final_value->type().pretty());
228
229 // If LHS was directly the symbol
230 if(s.id() == ID_symbol)
231 {
232 symbol_exprt symbol_expr = to_symbol_expr(s);
233
235 {
236 CHECK_RETURN(!symbol_expr.get_identifier().empty());
237 map.insert_or_replace(symbol_expr.get_identifier(), final_value);
238 }
239 }
240 return true;
241}
242
244 const abstract_object_pointert &lhs,
245 const abstract_object_pointert &rhs,
246 std::stack<exprt> remaining_stack,
247 const namespacet &ns,
248 bool merge_write)
249{
251 const exprt &next_expr = remaining_stack.top();
252 remaining_stack.pop();
253
254 const irep_idt &stack_head_id = next_expr.id();
255 INVARIANT(
258 "Write stack expressions must be index, member, dereference, or typecast");
259
260 return lhs->write(*this, ns, remaining_stack, next_expr, rhs, merge_write);
261}
262
264{
265 // We should only attempt to assume Boolean things
266 // This should be enforced by the well-structured-ness of the
267 // goto-program and the way assume is used.
268 PRECONDITION(expr.is_boolean());
269
270 auto simplified = simplify_expr(expr, ns);
271 auto assumption = do_assume(simplified, ns);
272
273 if(assumption.id() != ID_nil) // I.E. actually a value
274 {
275 // Should be of the right type
276 INVARIANT(assumption.is_boolean(), "simplification preserves type");
277
278 if(assumption.is_false())
279 {
281 make_bottom();
282 return !currently_bottom;
283 }
284 }
285
286 return false;
287}
288
289static auto assume_functions =
290 std::map<irep_idt, assume_function>{{ID_not, assume_not},
292 {ID_or, assume_or},
299
300// do_assume attempts to reduce the expression
301// returns
302// true_exprt when the assumption does not hold
303// false_exprt if the assumption does not hold & the domain should go bottom
304// nil_exprt if the assumption can't be evaluated & we should give up
306{
307 auto expr_id = expr.id();
308
310
311 if(fn)
312 return fn(*this, expr, ns);
313
314 return eval(expr, ns)->to_constant();
315}
316
318 const typet &type,
319 const namespacet &ns,
320 bool top,
321 bool bttm) const
322{
325 type, top, bttm, empty_constant_expr, *this, ns);
326}
327
329 const typet &type,
330 const exprt &e,
331 const namespacet &ns) const
332{
333 return abstract_object_factory(type, false, false, e, *this, ns);
334}
335
337 const typet &type,
338 bool top,
339 bool bttm,
340 const exprt &e,
341 const abstract_environmentt &environment,
342 const namespacet &ns) const
343{
344 return object_factory->get_abstract_object(
345 type, top, bttm, e, environment, ns);
346}
347
349{
350 return object_factory->config();
351}
352
357{
358 // for each entry in the incoming environment we need to either add it
359 // if it is new, or merge with the existing key if it is not present
360 if(bottom)
361 {
362 *this = env;
363 return !env.bottom;
364 }
365
366 if(env.bottom)
367 return false;
368
369 // For each element in the intersection of map and env.map merge
370 // If the result of the merge is top, remove from the map
371 bool modified = false;
372 for(const auto &entry : env.map.get_delta_view(map))
373 {
375 entry.get_other_map_value(), entry.m, merge_location, widen_mode);
376
377 modified |= merge_result.modified;
378 map.replace(entry.k, merge_result.object);
379 }
380
381 return modified;
382}
383
385{
386 // TODO(tkiley): error reporting
387 make_top();
388}
389
391{
392 // since we assume anything is not in the map is top this is sufficient
393 map.clear();
394 bottom = false;
395}
396
398{
399 map.clear();
400 bottom = true;
401}
402
404{
405 return map.empty() && bottom;
406}
407
409{
410 return map.empty() && !bottom;
411}
412
414 std::ostream &out,
415 const ai_baset &ai,
416 const namespacet &ns) const
417{
418 out << "{\n";
419
420 for(const auto &entry : map.get_view())
421 {
422 out << entry.first << " () -> ";
423 entry.second->output(out, ai, ns);
424 out << "\n";
425 }
426
427 out << "}\n";
428}
429
431{
432 if(is_bottom())
433 return false_exprt();
434 if(is_top())
435 return true_exprt();
436
438 for(const auto &entry : map.get_view())
439 {
440 auto sym = entry.first;
441 auto val = entry.second;
442 auto pred = val->to_predicate(symbol_exprt(sym, val->type()));
443
444 predicates.push_back(pred);
445 }
446
447 if(predicates.size() == 1)
448 return predicates.front();
449
451 return and_exprt(predicates);
452}
453
455{
456 for(const auto &entry : map.get_view())
457 {
458 if(entry.second == nullptr)
459 {
460 return false;
461 }
462 }
463 return true;
464}
465
467 const exprt &e,
468 const namespacet &ns) const
469{
470 // We create a temporary top abstract object (according to the
471 // type of the expression), and call expression transform on it.
472 // The value of the temporary abstract object is ignored, its
473 // purpose is just to dispatch the expression transform call to
474 // a concrete subtype of abstract_objectt.
475 auto eval_obj = abstract_object_factory(e.type(), ns, true, false);
476 auto operands = eval_operands(e, *this, ns);
477
478 return eval_obj->expression_transform(e, operands, *this, ns);
479}
480
482{
483 map.erase_if_exists(expr.get_identifier());
484}
485
486std::vector<abstract_environmentt::map_keyt>
488 const abstract_environmentt &first,
489 const abstract_environmentt &second)
490{
491 // Find all symbols who have different write locations in each map
492 std::vector<abstract_environmentt::map_keyt> symbols_diff;
493 for(const auto &entry : first.map.get_view())
494 {
495 const auto &second_entry = second.map.find(entry.first);
496 if(second_entry.has_value())
497 {
498 if(second_entry.value().get()->has_been_modified(entry.second))
499 {
500 CHECK_RETURN(!entry.first.empty());
501 symbols_diff.push_back(entry.first);
502 }
503 }
504 }
505
506 // Add any symbols that are only in the second map
507 for(const auto &entry : second.map.get_view())
508 {
509 const auto &second_entry = first.map.find(entry.first);
510 if(!second_entry.has_value())
511 {
512 CHECK_RETURN(!entry.first.empty());
513 symbols_diff.push_back(entry.first);
514 }
515 }
516 return symbols_diff;
517}
518
519static std::size_t count_globals(const namespacet &ns)
520{
521 auto const &symtab = ns.get_symbol_table();
522 auto val = std::count_if(
523 symtab.begin(),
524 symtab.end(),
525 [](const symbol_tablet::const_iteratort::value_type &sym) {
526 return sym.second.is_lvalue && sym.second.is_static_lifetime;
527 });
528 return val;
529}
530
533{
534 abstract_object_statisticst statistics = {};
535 statistics.number_of_globals = count_globals(ns);
537 for(auto const &object : map.get_view())
538 {
539 if(visited.find(object.second) == visited.end())
540 {
541 object.second->get_statistics(statistics, visited, *this, ns);
542 }
543 }
544 return statistics;
545}
546
547std::vector<abstract_object_pointert> eval_operands(
548 const exprt &expr,
550 const namespacet &ns)
551{
552 std::vector<abstract_object_pointert> operands;
553
554 for(const auto &op : expr.operands())
555 operands.push_back(env.eval(op, ns));
556
557 return operands;
558}
559
562{
563 return std::dynamic_pointer_cast<const abstract_value_objectt>(
564 obj->unwrap_context());
565}
566
568{
569 return as_value(obj) != nullptr;
570}
571
573 std::map<irep_idt, irep_idt>{{ID_equal, ID_notequal},
575 {ID_le, ID_gt},
576 {ID_lt, ID_ge},
577 {ID_ge, ID_lt},
578 {ID_gt, ID_le}};
579
580static exprt invert_result(const exprt &result)
581{
582 if(!result.is_boolean())
583 return result;
584
585 if(result.is_true())
586 return false_exprt();
587 return true_exprt();
588}
589
590static exprt invert_expr(const exprt &expr)
591{
592 auto expr_id = expr.id();
593
596 return nil_exprt();
597
599 auto inverse_op = inverse_operation->second;
602}
603
606 const abstract_object_pointert &previous,
607 const exprt &destination,
609 const namespacet &ns)
610{
611 auto context =
612 std::dynamic_pointer_cast<const context_abstract_objectt>(previous);
613 if(context != nullptr)
614 obj = context->envelop(obj);
615 env.assign(destination, obj, ns);
616}
617
620 const exprt &expr,
621 const namespacet &ns)
622{
623 auto const &not_expr = to_not_expr(expr);
624
626 if(inverse_expression.is_not_nil())
627 return env.do_assume(inverse_expression, ns);
628
629 auto result = env.do_assume(not_expr.op(), ns);
630 return invert_result(result);
631}
632
635 const exprt &expr,
636 const namespacet &ns)
637{
638 auto and_expr = to_and_expr(expr);
639 bool nil = false;
640 for(auto const &operand : and_expr.operands())
641 {
642 auto result = env.do_assume(operand, ns);
643 if(result.is_false())
644 return result;
645 nil |= result.is_nil();
646 }
647 if(nil)
648 return nil_exprt();
649 return true_exprt();
650}
651
654 const exprt &expr,
655 const namespacet &ns)
656{
657 auto or_expr = to_or_expr(expr);
658
660 for(auto const &operand : or_expr.operands())
662
663 auto result = assume_and(env, and_exprt(negated_operands), ns);
664 return invert_result(result);
665}
666
668{
673
675 {
676 return as_value(left)->to_interval();
677 }
679 {
680 return as_value(right)->to_interval();
681 }
682
683 bool are_bad() const
684 {
685 return left == nullptr || right == nullptr ||
686 (left->is_top() && right->is_top()) || !is_value(left) ||
687 !is_value(right);
688 }
689
690 bool has_top() const
691 {
692 return left->is_top() || right->is_top();
693 }
694};
695
698 const exprt &expr,
699 const namespacet &ns)
700{
701 auto const &relationship_expr = to_binary_expr(expr);
702
703 auto lhs = relationship_expr.lhs();
704 auto rhs = relationship_expr.rhs();
705 auto left = env.eval(lhs, ns);
706 auto right = env.eval(rhs, ns);
707
708 if(left->is_top() && right->is_top())
709 return {};
710
711 return {lhs, rhs, left, right};
712}
713
716 const left_and_right_valuest &operands,
717 const namespacet &ns)
718{
719 if(operands.left->is_top() && is_assignable(operands.lhs))
720 {
721 // TOP == x
722 auto constrained = std::make_shared<interval_abstract_valuet>(
723 operands.right_interval(), env, ns);
724 prune_assign(env, operands.left, operands.lhs, constrained, ns);
725 }
726 if(operands.right->is_top() && is_assignable(operands.rhs))
727 {
728 // x == TOP
729 auto constrained = std::make_shared<interval_abstract_valuet>(
730 operands.left_interval(), env, ns);
731 prune_assign(env, operands.right, operands.rhs, constrained, ns);
732 }
733 return true_exprt();
734}
735
738 const exprt &expr,
739 const namespacet &ns)
740{
741 auto operands = eval_operands_as_values(env, expr, ns);
742
743 if(operands.are_bad())
744 return nil_exprt();
745
746 if(operands.has_top())
747 return assume_eq_unbounded(env, operands, ns);
748
749 auto meet = operands.left->meet(operands.right);
750
751 if(meet->is_bottom())
752 return false_exprt();
753
754 if(is_assignable(operands.lhs))
755 prune_assign(env, operands.left, operands.lhs, meet, ns);
756 if(is_assignable(operands.rhs))
757 prune_assign(env, operands.right, operands.rhs, meet, ns);
758 return true_exprt();
759}
760
763 const exprt &expr,
764 const namespacet &ns)
765{
766 auto const &notequal_expr = to_binary_expr(expr);
767
768 auto left = env.eval(notequal_expr.lhs(), ns);
769 auto right = env.eval(notequal_expr.rhs(), ns);
770
771 if(left->is_top() || right->is_top())
772 return nil_exprt();
773 if(!is_value(left) || !is_value(right))
774 return nil_exprt();
775
776 auto meet = left->meet(right);
777
778 if(meet->is_bottom())
779 return true_exprt();
780
781 return false_exprt();
782}
783
786 const left_and_right_valuest &operands,
787 const namespacet &ns)
788{
789 if(operands.left->is_top() && is_assignable(operands.lhs))
790 {
791 // TOP < x, so prune range is min->right.upper
793 min_value_exprt(operands.left->type()),
794 operands.right_interval().get_upper(),
795 operands.left->type());
796 auto constrained =
797 std::make_shared<interval_abstract_valuet>(pruned_expr, env, ns);
798 prune_assign(env, operands.left, operands.lhs, constrained, ns);
799 }
800 if(operands.right->is_top() && is_assignable(operands.rhs))
801 {
802 // x < TOP, so prune range is left.lower->max
804 operands.left_interval().get_lower(),
805 max_value_exprt(operands.right->type()),
806 operands.right->type());
807 auto constrained =
808 std::make_shared<interval_abstract_valuet>(pruned_expr, env, ns);
809 prune_assign(env, operands.right, operands.rhs, constrained, ns);
810 }
811
812 return true_exprt();
813}
814
817 const exprt &expr,
818 const namespacet &ns)
819{
820 auto operands = eval_operands_as_values(env, expr, ns);
821 if(operands.are_bad())
822 return nil_exprt();
823
824 if(operands.has_top())
825 return assume_less_than_unbounded(env, operands, ns);
826
827 auto left_interval = operands.left_interval();
828 auto right_interval = operands.right_interval();
829
830 const auto &left_lower = left_interval.get_lower();
831 const auto &right_upper = right_interval.get_upper();
832
833 auto reduced_le_expr =
835 auto result = env.eval(reduced_le_expr, ns)->to_constant();
836 if(result.is_true())
837 {
838 if(is_assignable(operands.lhs))
839 {
841 left_interval.get_upper(), right_upper);
842 auto constrained =
843 as_value(operands.left)->constrain(left_lower, pruned_upper);
844 prune_assign(env, operands.left, operands.lhs, constrained, ns);
845 }
846 if(is_assignable(operands.rhs))
847 {
849 left_lower, right_interval.get_lower());
850 auto constrained =
851 as_value(operands.right)->constrain(pruned_lower, right_upper);
852 prune_assign(env, operands.right, operands.rhs, constrained, ns);
853 }
854 }
855 return result;
856}
857
859 std::map<irep_idt, irep_idt>{{ID_ge, ID_le}, {ID_gt, ID_lt}};
860
863 const exprt &expr,
864 const namespacet &ns)
865{
866 auto const &gt_expr = to_binary_expr(expr);
867
869 auto symmetric_expr =
871
873}
std::vector< abstract_object_pointert > eval_operands(const exprt &expr, const abstract_environmentt &env, const namespacet &ns)
static auto assume_functions
static bool is_value(const abstract_object_pointert &obj)
static exprt assume_not(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static auto inverse_operations
static exprt invert_expr(const exprt &expr)
static abstract_value_pointert as_value(const abstract_object_pointert &obj)
static bool is_object_creation(const irep_idt &id)
static auto symmetric_operations
left_and_right_valuest eval_operands_as_values(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt assume_eq(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt assume_noteq(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static std::size_t count_globals(const namespacet &ns)
static exprt assume_or(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
exprt(* assume_function)(abstract_environmentt &, const exprt &, const namespacet &)
static exprt assume_less_than(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
static exprt invert_result(const exprt &result)
exprt assume_less_than_unbounded(abstract_environmentt &env, const left_and_right_valuest &operands, const namespacet &ns)
static exprt assume_and(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
bool is_ptr_comparison(const exprt &expr)
void prune_assign(abstract_environmentt &env, const abstract_object_pointert &previous, const exprt &destination, abstract_object_pointert obj, const namespacet &ns)
static bool is_dynamic_allocation(const exprt &expr)
exprt assume_eq_unbounded(abstract_environmentt &env, const left_and_right_valuest &operands, const namespacet &ns)
static exprt assume_greater_than(abstract_environmentt &env, const exprt &expr, const namespacet &ns)
bool is_ptr_diff(const exprt &expr)
static bool is_access_expr(const exprt &expr)
An abstract version of a program environment.
bool is_ptr_comparison(const exprt &expr)
bool is_ptr_diff(const exprt &expr)
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Statistics gathering for the variable senstivity domain.
virtual bool assume(const exprt &expr, const namespacet &ns)
Reduces the domain based on a condition.
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print out all the values in the abstract object map.
bool is_bottom() const
Gets whether the domain is bottom.
abstract_object_pointert resolve_symbol(const exprt &e, const namespacet &ns) const
exprt to_predicate() const
Gives a boolean condition that is true for all values represented by the environment.
void make_top()
Set the domain to top (i.e. everything)
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
void erase(const symbol_exprt &expr)
Delete a symbol from the map.
static std::vector< abstract_environmentt::map_keyt > modified_symbols(const abstract_environmentt &first, const abstract_environmentt &second)
For our implementation of variable sensitivity domains, we need to be able to efficiently find symbol...
bool verify() const
Check the structural invariants are maintained.
virtual void havoc(const std::string &havoc_string)
This should be used as a default case / everything else has failed The string is so that I can easily...
exprt do_assume(const exprt &e, const namespacet &ns)
const vsd_configt & configuration() const
Exposes the environment configuration.
variable_sensitivity_object_factory_ptrt object_factory
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
abstract_object_statisticst gather_statistics(const namespacet &ns) const
virtual bool merge(const abstract_environmentt &env, const goto_programt::const_targett &merge_location, widen_modet widen_mode)
Computes the join between "this" and "b".
void make_bottom()
Set the domain to top (i.e. no possible states / unreachable)
bool is_top() const
Gets whether the domain is top.
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
virtual abstract_object_pointert eval_expression(const exprt &e, const namespacet &ns) const
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
sharing_mapt< map_keyt, abstract_object_pointert > map
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Boolean AND.
Definition std_expr.h:2125
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Represents an interval of values.
Definition interval.h:52
static exprt get_max(const exprt &a, const exprt &b)
Definition interval.cpp:960
static exprt get_min(const exprt &a, const exprt &b)
Definition interval.cpp:965
const exprt & get_lower() const
Definition interval.cpp:27
const exprt & get_upper() const
Definition interval.cpp:32
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
std::vector< exprt > operandst
Definition expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The Boolean constant false.
Definition std_expr.h:3200
instructionst::const_iterator const_targett
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
+∞ upper bound for intervals
Definition interval.h:18
-∞ upper bound for intervals
Definition interval.h:33
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition namespace.h:123
The NIL expression.
Definition std_expr.h:3209
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
The Boolean constant true.
Definition std_expr.h:3191
The type of an expression, extends irept.
Definition type.h:29
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition expr_util.cpp:24
Deprecated expression utility functions.
An interval to represent a set of possible values.
exprt simplify_expr(exprt src, const namespacet &ns)
bool sort_operands(exprt::operandst &operands)
sort operands of an expression according to ordering defined by operator<
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:895
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition std_expr.h:2177
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition std_expr.h:2322
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2484
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
abstract_object_pointert right
constant_interval_exprt right_interval() const
constant_interval_exprt left_interval() const
abstract_object_pointert left
Author: Diffblue Ltd.
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...