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,
44 const goto_symex_statet &previous_state,
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())
53 apply_condition(op, previous_state, ns);
54 }
55 else if(auto not_expr = expr_try_dynamic_cast<not_exprt>(condition))
56 {
57 const exprt &operand = not_expr->op();
58 if(auto notequal_expr = expr_try_dynamic_cast<notequal_exprt>(operand))
59 {
60 // !(A != B)
61 // -->
62 // A == B
64 equal_exprt{notequal_expr->lhs(), notequal_expr->rhs()},
65 previous_state,
66 ns);
67 }
68 else if(auto equal_expr = expr_try_dynamic_cast<equal_exprt>(operand))
69 {
70 // !(A == B)
71 // -->
72 // A != B
74 notequal_exprt{equal_expr->lhs(), equal_expr->rhs()},
75 previous_state,
76 ns);
77 }
78 else
79 {
80 // !A
81 // -->
82 // A == false
83 apply_condition(equal_exprt{operand, false_exprt{}}, previous_state, ns);
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
112 const auto propagation_entry = propagation.find(l1_identifier);
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
128 apply_condition(equal_exprt{condition, true_exprt()}, previous_state, ns);
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)
137 const notequal_exprt &notequal_expr =
138 expr_dynamic_cast<notequal_exprt>(condition);
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())
148 apply_condition(equal_exprt{lhs, false_exprt{}}, previous_state, ns);
149 else if(rhs.is_false())
150 apply_condition(equal_exprt{lhs, true_exprt{}}, previous_state, ns);
151 else
153 }
154}
exprt & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
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.
Definition: goto_state.cpp:42
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.
Definition: goto_state.cpp:18
Central data structure: state.
std::function< std::size_t(const irep_idt &)> get_l2_name_provider() const
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
std::vector< threadt > threads
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.
Definition: sharing_map.h:388
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
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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.
Definition: value_set.cpp:1233
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
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1292
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:173
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...