cprover
Loading...
Searching...
No Matches
goto_state.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Romain Brenguier, romain.brenguier@diffblue.com
6
7\*******************************************************************/
8
9#include "goto_state.h"
11#include "goto_symex_state.h"
12
13#include <util/format_expr.h>
14
19{
21 propagation.get_view(view);
22
23 for(const auto &name_value : view)
24 {
25 out << name_value.first << " <- " << format(name_value.second) << "\n";
26 }
27}
28
43 const exprt &condition,
45 const namespacet &ns)
46{
47 if(auto and_expr = expr_try_dynamic_cast<and_exprt>(condition))
48 {
49 // A == B && C == D && E == F ...
50 // -->
51 // Apply each condition individually
52 for(const auto &op : and_expr->operands())
54 }
55 else if(auto not_expr = expr_try_dynamic_cast<not_exprt>(condition))
56 {
57 const exprt &operand = not_expr->op();
59 {
60 // !(A != B)
61 // -->
62 // A == B
66 ns);
67 }
69 {
70 // !(A == B)
71 // -->
72 // A != B
74 notequal_exprt{equal_expr->lhs(), equal_expr->rhs()},
76 ns);
77 }
78 else
79 {
80 // !A
81 // -->
82 // A == false
84 }
85 }
86 else if(auto equal_expr = expr_try_dynamic_cast<equal_exprt>(condition))
87 {
88 // Base case: try to apply a single equality constraint
89 exprt lhs = equal_expr->lhs();
90 exprt rhs = equal_expr->rhs();
91 if(is_ssa_expr(rhs))
92 std::swap(lhs, rhs);
93
94 if(is_ssa_expr(lhs) && goto_symex_is_constantt()(rhs))
95 {
96 const ssa_exprt &ssa_lhs = to_ssa_expr(lhs);
98 !ssa_lhs.get_level_2().empty(),
99 "apply_condition operand should be L2 renamed");
100
101 if(
102 previous_state.threads.size() == 1 ||
103 previous_state.write_is_shared(ssa_lhs, ns) !=
105 {
106 const ssa_exprt l1_lhs = remove_level_2(ssa_lhs);
107 const irep_idt &l1_identifier = l1_lhs.get_identifier();
108
110 l1_identifier, l1_lhs, previous_state.get_l2_name_provider());
111
113 if(!propagation_entry.has_value())
114 propagation.insert(l1_identifier, rhs);
115 else if(propagation_entry->get() != rhs)
116 propagation.replace(l1_identifier, rhs);
117
118 value_set.assign(l1_lhs, rhs, ns, true, false);
119 }
120 }
121 }
122 else if(
123 can_cast_expr<symbol_exprt>(condition) && condition.type() == bool_typet())
124 {
125 // A
126 // -->
127 // A == true
129 }
130 else if(
132 expr_checked_cast<notequal_exprt>(condition).lhs().type() == bool_typet{})
133 {
134 // A != (true|false)
135 // -->
136 // A == (false|true)
139 exprt lhs = notequal_expr.lhs();
140 exprt rhs = notequal_expr.rhs();
141 if(is_ssa_expr(rhs))
142 std::swap(lhs, rhs);
143
144 if(!is_ssa_expr(lhs) || !goto_symex_is_constantt()(rhs))
145 return;
146
147 if(rhs.is_true())
149 else if(rhs.is_false())
151 else
153 }
154}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
The Boolean type.
Definition std_types.h:36
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
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:42
typet & type()
Return the type of the expression.
Definition expr.h:82
The Boolean constant false.
Definition std_expr.h:2865
symex_level2t level2
Definition goto_state.h:38
void apply_condition(const exprt &condition, const goto_symex_statet &previous_state, const namespacet &ns)
Given a condition that must hold on this path, propagate as much knowledge as possible.
sharing_mapt< irep_idt, exprt > propagation
Definition goto_state.h:71
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition goto_state.h:51
void output_propagation_map(std::ostream &)
Print the constant propagation map in a human-friendly format.
Central data structure: state.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Disequality.
Definition std_expr.h:1283
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
const irep_idt get_level_2() const
Definition ssa_expr.h:73
The Boolean constant true.
Definition std_expr.h:2856
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Transforms this value-set by executing executing the assignment lhs := rhs against it.
static format_containert< T > format(const T &o)
Definition format.h:37
goto_statet class definition
GOTO Symex constant propagation.
Symbolic Execution.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
ssa_exprt remove_level_2(ssa_exprt ssa)
Definition ssa_expr.cpp:218
bool is_ssa_expr(const exprt &expr)
Definition ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
std::size_t increase_generation(const irep_idt &l1_identifier, const ssa_exprt &lhs, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
Allocates a fresh L2 name for the given L1 identifier, and makes it the latest generation on this pat...