cprover
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
12
13#include <util/expr_util.h>
14#include <util/simplify_expr.h>
16#include <util/simplify_utils.h>
17#include <util/symbol_table.h>
18
19#include <algorithm>
20#include <map>
21#include <ostream>
22#include <stack>
23
24#ifdef DEBUG
25# include <iostream>
26#endif
27
28typedef exprt (
30
31static exprt
32assume_not(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
33static exprt
34assume_or(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
35static exprt
36assume_and(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
37static exprt
38assume_eq(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
39static exprt assume_noteq(
41 const exprt &expr,
42 const namespacet &ns);
45 const exprt &expr,
46 const namespacet &ns);
49 const exprt &expr,
50 const namespacet &ns);
51
53static bool is_value(const abstract_object_pointert &obj);
54
55std::vector<abstract_object_pointert> eval_operands(
56 const exprt &expr,
58 const namespacet &ns);
59
60bool is_ptr_diff(const exprt &expr)
61{
62 return (expr.id() == ID_minus) &&
63 (expr.operands()[0].type().id() == ID_pointer) &&
64 (expr.operands()[1].type().id() == ID_pointer);
65}
66
67bool is_ptr_comparison(const exprt &expr)
68{
69 auto const &id = expr.id();
70 bool is_comparison = id == ID_equal || id == ID_notequal || id == ID_lt ||
71 id == ID_le || id == ID_gt || id == ID_ge;
72
73 return is_comparison && (expr.operands()[0].type().id() == ID_pointer) &&
74 (expr.operands()[1].type().id() == ID_pointer);
75}
76
77static bool is_access_expr(const irep_idt &id)
78{
79 return id == ID_member || id == ID_index || id == ID_dereference;
80}
81
82static bool is_object_creation(const irep_idt &id)
83{
84 return id == ID_array || id == ID_struct || id == ID_constant ||
85 id == ID_address_of;
86}
87
88static bool is_dynamic_allocation(const exprt &expr)
89{
90 return expr.id() == ID_side_effect && expr.get(ID_statement) == ID_allocate;
91}
92
94abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
95{
96 if(bottom)
97 return abstract_object_factory(expr.type(), ns, false, true);
98
99 // first try to canonicalise, including constant folding
100 const exprt &simplified_expr = simplify_expr(expr, ns);
101
102 const irep_idt simplified_id = simplified_expr.id();
104 return resolve_symbol(simplified_expr, ns);
105
106 if(
107 is_access_expr(simplified_id) || is_ptr_diff(simplified_expr) ||
108 is_ptr_comparison(simplified_expr))
109 {
110 auto const operands = eval_operands(simplified_expr, *this, ns);
111 auto const &target = operands.front();
112
113 return target->expression_transform(simplified_expr, operands, *this, ns);
114 }
115
117 return abstract_object_factory(simplified_expr.type(), simplified_expr, ns);
118
119 if(is_dynamic_allocation(simplified_expr))
122 exprt(ID_dynamic_object, simplified_expr.type()),
123 ns);
124
125 // No special handling required by the abstract environment
126 // delegate to the abstract object
127 if(!simplified_expr.operands().empty())
128 return eval_expression(simplified_expr, ns);
129
130 // It is important that this is top as the abstract object may not know
131 // how to handle the expression
132 return abstract_object_factory(simplified_expr.type(), ns, true, false);
133}
134
136 const exprt &expr,
137 const namespacet &ns) const
138{
139 const symbol_exprt &symbol(to_symbol_expr(expr));
140 const auto symbol_entry = map.find(symbol.get_identifier());
141
142 if(symbol_entry.has_value())
143 return symbol_entry.value();
144 return abstract_object_factory(expr.type(), ns, true, false);
145}
146
148 const exprt &expr,
149 const abstract_object_pointert &value,
150 const namespacet &ns)
151{
152 PRECONDITION(value);
153
154 if(value->is_bottom())
155 {
156 bool bottom_at_start = this->is_bottom();
157 this->make_bottom();
158 return !bottom_at_start;
159 }
160
162 // Build a stack of index, member and dereference accesses which
163 // we will work through the relevant abstract objects
164 exprt s = expr;
165 std::stack<exprt> stactions; // I'm not a continuation, honest guv'
166 while(s.id() != ID_symbol)
167 {
168 if(s.id() == ID_index || s.id() == ID_member || s.id() == ID_dereference)
169 {
170 stactions.push(s);
171 s = s.operands()[0];
172 }
173 else
174 {
175 lhs_value = eval(s, ns);
176 break;
177 }
178 }
179
180 if(!lhs_value)
181 {
182 INVARIANT(s.id() == ID_symbol, "Have a symbol or a stack");
183 lhs_value = resolve_symbol(s, ns);
184 }
185
187
188 // This is the root abstract object that is in the map of abstract objects
189 // It might not have the same type as value if the above stack isn't empty
190
191 if(!stactions.empty())
192 {
193 // The symbol is not in the map - it is therefore top
194 final_value = write(lhs_value, value, stactions, ns, false);
195 }
196 else
197 {
198 // If we don't have a symbol on the LHS, then we must have some expression
199 // that we can write to (i.e. a pointer, an array, a struct) This appears
200 // to be none of that.
201 if(s.id() != ID_symbol)
202 {
203 throw std::runtime_error("invalid l-value");
204 }
205 // We can assign the AO directly to the symbol
206 final_value = value;
207 }
208
209 const typet &lhs_type = ns.follow(lhs_value->type());
210 const typet &rhs_type = ns.follow(final_value->type());
211
212 // Write the value for the root symbol back into the map
213 INVARIANT(
215 "Assignment types must match"
216 "\n"
217 "lhs_type :" +
218 lhs_type.pretty() +
219 "\n"
220 "rhs_type :" +
221 rhs_type.pretty());
222
223 // If LHS was directly the symbol
224 if(s.id() == ID_symbol)
225 {
226 symbol_exprt symbol_expr = to_symbol_expr(s);
227
229 {
230 CHECK_RETURN(!symbol_expr.get_identifier().empty());
231 map.insert_or_replace(symbol_expr.get_identifier(), final_value);
232 }
233 }
234 return true;
235}
236
238 const abstract_object_pointert &lhs,
239 const abstract_object_pointert &rhs,
240 std::stack<exprt> remaining_stack,
241 const namespacet &ns,
242 bool merge_write)
243{
245 const exprt &next_expr = remaining_stack.top();
246 remaining_stack.pop();
247
248 const irep_idt &stack_head_id = next_expr.id();
249 INVARIANT(
252 "Write stack expressions must be index, member, or dereference");
253
254 return lhs->write(*this, ns, remaining_stack, next_expr, rhs, merge_write);
255}
256
258{
259 // We should only attempt to assume Boolean things
260 // This should be enforced by the well-structured-ness of the
261 // goto-program and the way assume is used.
262 PRECONDITION(expr.type().id() == ID_bool);
263
264 auto simplified = simplify_expr(expr, ns);
265 auto assumption = do_assume(simplified, ns);
266
267 if(assumption.id() != ID_nil) // I.E. actually a value
268 {
269 // Should be of the right type
270 INVARIANT(
271 assumption.type().id() == ID_bool, "simplification preserves type");
272
273 if(assumption.is_false())
274 {
276 make_bottom();
277 return !currently_bottom;
278 }
279 }
280
281 return false;
282}
283
284static auto assume_functions =
285 std::map<irep_idt, assume_function>{{ID_not, assume_not},
287 {ID_or, assume_or},
294
295// do_assume attempts to reduce the expression
296// returns
297// true_exprt when the assumption does not hold
298// false_exprt if the assumption does not hold & the domain should go bottom
299// nil_exprt if the assumption can't be evaluated & we should give up
301{
302 auto expr_id = expr.id();
303
305
306 if(fn)
307 return fn(*this, expr, ns);
308
309 return eval(expr, ns)->to_constant();
310}
311
313 const typet &type,
314 const namespacet &ns,
315 bool top,
316 bool bttm) const
317{
320 type, top, bttm, empty_constant_expr, *this, ns);
321}
322
324 const typet &type,
325 const exprt &e,
326 const namespacet &ns) const
327{
328 return abstract_object_factory(type, false, false, e, *this, ns);
329}
330
332 const typet &type,
333 bool top,
334 bool bttm,
335 const exprt &e,
336 const abstract_environmentt &environment,
337 const namespacet &ns) const
338{
339 return object_factory->get_abstract_object(
340 type, top, bttm, e, environment, ns);
341}
342
344{
345 return object_factory->config();
346}
347
352{
353 // for each entry in the incoming environment we need to either add it
354 // if it is new, or merge with the existing key if it is not present
355 if(bottom)
356 {
357 *this = env;
358 return !env.bottom;
359 }
360
361 if(env.bottom)
362 return false;
363
364 // For each element in the intersection of map and env.map merge
365 // If the result of the merge is top, remove from the map
366 bool modified = false;
367 for(const auto &entry : env.map.get_delta_view(map))
368 {
370 entry.get_other_map_value(), entry.m, merge_location, widen_mode);
371
372 modified |= merge_result.modified;
373 map.replace(entry.k, merge_result.object);
374 }
375
376 return modified;
377}
378
380{
381 // TODO(tkiley): error reporting
382 make_top();
383}
384
386{
387 // since we assume anything is not in the map is top this is sufficient
388 map.clear();
389 bottom = false;
390}
391
393{
394 map.clear();
395 bottom = true;
396}
397
399{
400 return map.empty() && bottom;
401}
402
404{
405 return map.empty() && !bottom;
406}
407
409 std::ostream &out,
410 const ai_baset &ai,
411 const namespacet &ns) const
412{
413 out << "{\n";
414
415 for(const auto &entry : map.get_view())
416 {
417 out << entry.first << " () -> ";
418 entry.second->output(out, ai, ns);
419 out << "\n";
420 }
421
422 out << "}\n";
423}
424
426{
427 if(is_bottom())
428 return false_exprt();
429 if(is_top())
430 return true_exprt();
431
433 for(const auto &entry : map.get_view())
434 {
435 auto sym = entry.first;
436 auto val = entry.second;
437 auto pred = val->to_predicate(symbol_exprt(sym, val->type()));
438
439 predicates.push_back(pred);
440 }
441
442 if(predicates.size() == 1)
443 return predicates.front();
444
446 return and_exprt(predicates);
447}
448
450{
451 for(const auto &entry : map.get_view())
452 {
453 if(entry.second == nullptr)
454 {
455 return false;
456 }
457 }
458 return true;
459}
460
462 const exprt &e,
463 const namespacet &ns) const
464{
465 // We create a temporary top abstract object (according to the
466 // type of the expression), and call expression transform on it.
467 // The value of the temporary abstract object is ignored, its
468 // purpose is just to dispatch the expression transform call to
469 // a concrete subtype of abstract_objectt.
470 auto eval_obj = abstract_object_factory(e.type(), ns, true, false);
471 auto operands = eval_operands(e, *this, ns);
472
473 return eval_obj->expression_transform(e, operands, *this, ns);
474}
475
477{
478 map.erase_if_exists(expr.get_identifier());
479}
480
481std::vector<abstract_environmentt::map_keyt>
483 const abstract_environmentt &first,
484 const abstract_environmentt &second)
485{
486 // Find all symbols who have different write locations in each map
487 std::vector<abstract_environmentt::map_keyt> symbols_diff;
488 for(const auto &entry : first.map.get_view())
489 {
490 const auto &second_entry = second.map.find(entry.first);
491 if(second_entry.has_value())
492 {
493 if(second_entry.value().get()->has_been_modified(entry.second))
494 {
495 CHECK_RETURN(!entry.first.empty());
496 symbols_diff.push_back(entry.first);
497 }
498 }
499 }
500
501 // Add any symbols that are only in the second map
502 for(const auto &entry : second.map.get_view())
503 {
504 const auto &second_entry = first.map.find(entry.first);
505 if(!second_entry.has_value())
506 {
507 CHECK_RETURN(!entry.first.empty());
508 symbols_diff.push_back(entry.first);
509 }
510 }
511 return symbols_diff;
512}
513
514static std::size_t count_globals(const namespacet &ns)
515{
516 auto const &symtab = ns.get_symbol_table();
517 auto val = std::count_if(
518 symtab.begin(),
519 symtab.end(),
520 [](const symbol_tablet::const_iteratort::value_type &sym) {
521 return sym.second.is_lvalue && sym.second.is_static_lifetime;
522 });
523 return val;
524}
525
528{
529 abstract_object_statisticst statistics = {};
530 statistics.number_of_globals = count_globals(ns);
532 for(auto const &object : map.get_view())
533 {
534 if(visited.find(object.second) == visited.end())
535 {
536 object.second->get_statistics(statistics, visited, *this, ns);
537 }
538 }
539 return statistics;
540}
541
542std::vector<abstract_object_pointert> eval_operands(
543 const exprt &expr,
545 const namespacet &ns)
546{
547 std::vector<abstract_object_pointert> operands;
548
549 for(const auto &op : expr.operands())
550 operands.push_back(env.eval(op, ns));
551
552 return operands;
553}
554
557{
558 return std::dynamic_pointer_cast<const abstract_value_objectt>(
559 obj->unwrap_context());
560}
561
563{
564 return as_value(obj) != nullptr;
565}
566
568 std::map<irep_idt, irep_idt>{{ID_equal, ID_notequal},
570 {ID_le, ID_gt},
571 {ID_lt, ID_ge},
572 {ID_ge, ID_lt},
573 {ID_gt, ID_le}};
574
575static exprt invert_result(const exprt &result)
576{
577 if(!result.is_boolean())
578 return result;
579
580 if(result.is_true())
581 return false_exprt();
582 return true_exprt();
583}
584
585static exprt invert_expr(const exprt &expr)
586{
587 auto expr_id = expr.id();
588
591 return nil_exprt();
592
594 auto inverse_op = inverse_operation->second;
597}
598
601 const abstract_object_pointert &previous,
602 const exprt &destination,
604 const namespacet &ns)
605{
606 auto context =
607 std::dynamic_pointer_cast<const context_abstract_objectt>(previous);
608 if(context != nullptr)
609 obj = context->envelop(obj);
610 env.assign(destination, obj, ns);
611}
612
615 const exprt &expr,
616 const namespacet &ns)
617{
618 auto const &not_expr = to_not_expr(expr);
619
621 if(inverse_expression.is_not_nil())
622 return env.do_assume(inverse_expression, ns);
623
624 auto result = env.do_assume(not_expr.op(), ns);
625 return invert_result(result);
626}
627
630 const exprt &expr,
631 const namespacet &ns)
632{
633 auto and_expr = to_and_expr(expr);
634 bool nil = false;
635 for(auto const &operand : and_expr.operands())
636 {
637 auto result = env.do_assume(operand, ns);
638 if(result.is_false())
639 return result;
640 nil |= result.is_nil();
641 }
642 if(nil)
643 return nil_exprt();
644 return true_exprt();
645}
646
649 const exprt &expr,
650 const namespacet &ns)
651{
652 auto or_expr = to_or_expr(expr);
653
655 for(auto const &operand : or_expr.operands())
657
658 auto result = assume_and(env, and_exprt(negated_operands), ns);
659 return invert_result(result);
660}
661
663{
668
670 {
671 return as_value(left)->to_interval();
672 }
674 {
675 return as_value(right)->to_interval();
676 }
677
678 bool are_bad() const
679 {
680 return left == nullptr || right == nullptr ||
681 (left->is_top() && right->is_top()) || !is_value(left) ||
682 !is_value(right);
683 }
684
685 bool has_top() const
686 {
687 return left->is_top() || right->is_top();
688 }
689};
690
693 const exprt &expr,
694 const namespacet &ns)
695{
696 auto const &relationship_expr = to_binary_expr(expr);
697
698 auto lhs = relationship_expr.lhs();
699 auto rhs = relationship_expr.rhs();
700 auto left = env.eval(lhs, ns);
701 auto right = env.eval(rhs, ns);
702
703 if(left->is_top() && right->is_top())
704 return {};
705
706 return {lhs, rhs, left, right};
707}
708
711 const left_and_right_valuest &operands,
712 const namespacet &ns)
713{
714 if(operands.left->is_top() && is_assignable(operands.lhs))
715 {
716 // TOP == x
717 auto constrained = std::make_shared<interval_abstract_valuet>(
718 operands.right_interval(), env, ns);
719 prune_assign(env, operands.left, operands.lhs, constrained, ns);
720 }
721 if(operands.right->is_top() && is_assignable(operands.rhs))
722 {
723 // x == TOP
724 auto constrained = std::make_shared<interval_abstract_valuet>(
725 operands.left_interval(), env, ns);
726 prune_assign(env, operands.right, operands.rhs, constrained, ns);
727 }
728 return true_exprt();
729}
730
733 const exprt &expr,
734 const namespacet &ns)
735{
736 auto operands = eval_operands_as_values(env, expr, ns);
737
738 if(operands.are_bad())
739 return nil_exprt();
740
741 if(operands.has_top())
742 return assume_eq_unbounded(env, operands, ns);
743
744 auto meet = operands.left->meet(operands.right);
745
746 if(meet->is_bottom())
747 return false_exprt();
748
749 if(is_assignable(operands.lhs))
750 prune_assign(env, operands.left, operands.lhs, meet, ns);
751 if(is_assignable(operands.rhs))
752 prune_assign(env, operands.right, operands.rhs, meet, ns);
753 return true_exprt();
754}
755
758 const exprt &expr,
759 const namespacet &ns)
760{
761 auto const &notequal_expr = to_binary_expr(expr);
762
763 auto left = env.eval(notequal_expr.lhs(), ns);
764 auto right = env.eval(notequal_expr.rhs(), ns);
765
766 if(left->is_top() || right->is_top())
767 return nil_exprt();
768 if(!is_value(left) || !is_value(right))
769 return nil_exprt();
770
771 auto meet = left->meet(right);
772
773 if(meet->is_bottom())
774 return true_exprt();
775
776 return false_exprt();
777}
778
781 const left_and_right_valuest &operands,
782 const namespacet &ns)
783{
784 if(operands.left->is_top() && is_assignable(operands.lhs))
785 {
786 // TOP < x, so prune range is min->right.upper
788 min_exprt(operands.left->type()),
789 operands.right_interval().get_upper(),
790 operands.left->type());
791 auto constrained =
792 std::make_shared<interval_abstract_valuet>(pruned_expr, env, ns);
793 prune_assign(env, operands.left, operands.lhs, constrained, ns);
794 }
795 if(operands.right->is_top() && is_assignable(operands.rhs))
796 {
797 // x < TOP, so prune range is left.lower->max
799 operands.left_interval().get_lower(),
800 max_exprt(operands.right->type()),
801 operands.right->type());
802 auto constrained =
803 std::make_shared<interval_abstract_valuet>(pruned_expr, env, ns);
804 prune_assign(env, operands.right, operands.rhs, constrained, ns);
805 }
806
807 return true_exprt();
808}
809
812 const exprt &expr,
813 const namespacet &ns)
814{
815 auto operands = eval_operands_as_values(env, expr, ns);
816 if(operands.are_bad())
817 return nil_exprt();
818
819 if(operands.has_top())
820 return assume_less_than_unbounded(env, operands, ns);
821
822 auto left_interval = operands.left_interval();
823 auto right_interval = operands.right_interval();
824
825 const auto &left_lower = left_interval.get_lower();
826 const auto &right_upper = right_interval.get_upper();
827
828 auto reduced_le_expr =
830 auto result = env.eval(reduced_le_expr, ns)->to_constant();
831 if(result.is_true())
832 {
833 if(is_assignable(operands.lhs))
834 {
836 left_interval.get_upper(), right_upper);
837 auto constrained =
838 as_value(operands.left)->constrain(left_lower, pruned_upper);
839 prune_assign(env, operands.left, operands.lhs, constrained, ns);
840 }
841 if(is_assignable(operands.rhs))
842 {
844 left_lower, right_interval.get_lower());
845 auto constrained =
846 as_value(operands.right)->constrain(pruned_lower, right_upper);
847 prune_assign(env, operands.right, operands.rhs, constrained, ns);
848 }
849 }
850 return result;
851}
852
854 std::map<irep_idt, irep_idt>{{ID_ge, ID_le}, {ID_gt, ID_lt}};
855
858 const exprt &expr,
859 const namespacet &ns)
860{
861 auto const &gt_expr = to_binary_expr(expr);
862
864 auto symmetric_expr =
866
868}
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
static bool is_access_expr(const irep_idt &id)
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)
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:119
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:40
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Boolean AND.
Definition std_expr.h:1974
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
Represents an interval of values.
Definition interval.h:48
static exprt get_max(const exprt &a, const exprt &b)
Definition interval.cpp:959
static exprt get_min(const exprt &a, const exprt &b)
Definition interval.cpp:964
const exprt & get_lower() const
Definition interval.cpp:29
const exprt & get_upper() const
Definition interval.cpp:34
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:33
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.cpp:51
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
The Boolean constant false.
Definition std_expr.h:2865
instructionst::const_iterator const_targett
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
const irep_idt & id() const
Definition irep.h:396
+∞ upper bound for intervals
Definition interval.h:18
-∞ upper bound for intervals
Definition interval.h:31
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
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:2874
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
The Boolean constant true.
Definition std_expr.h:2856
The type of an expression, extends irept.
Definition type.h:29
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition expr_util.cpp:21
Deprecated expression utility functions.
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:807
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition std_expr.h:2021
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition std_expr.h:2129
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:627
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
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...