Skip to content

Commit e9d84d4

Browse files
romainbrenguierromainbrenguier
committed
Move renaming validation functions to renamed.h
This can be useful when the type doesn't tell us directly that an exprt has been renamed, but we would expect it to be.
1 parent 3044640 commit e9d84d4

File tree

3 files changed

+157
-90
lines changed

3 files changed

+157
-90
lines changed

‎src/goto-symex/goto_symex_state.cpp

Lines changed: 6 additions & 90 deletions
Original file line numberDiff line numberDiff line change
@@ -47,90 +47,6 @@ goto_symex_statet::goto_symex_statet(
4747

4848
goto_symex_statet::~goto_symex_statet()=default;
4949

50-
/// Check that \p expr is correctly renamed to level 2 and return true in case
51-
/// an error is detected.
52-
static bool check_renaming(const exprt &expr);
53-
54-
static bool check_renaming(const typet &type)
55-
{
56-
if(type.id()==ID_array)
57-
return check_renaming(to_array_type(type).size());
58-
else if(type.id() == ID_struct || type.id() == ID_union)
59-
{
60-
for(const auto &c : to_struct_union_type(type).components())
61-
if(check_renaming(c.type()))
62-
return true;
63-
}
64-
else if(type.has_subtype())
65-
return check_renaming(to_type_with_subtype(type).subtype());
66-
67-
return false;
68-
}
69-
70-
static bool check_renaming_l1(const exprt &expr)
71-
{
72-
if(check_renaming(expr.type()))
73-
return true;
74-
75-
if(expr.id()==ID_symbol)
76-
{
77-
const auto &type = expr.type();
78-
if(!expr.get_bool(ID_C_SSA_symbol))
79-
return type.id() != ID_code && type.id() != ID_mathematical_function;
80-
if(!to_ssa_expr(expr).get_level_2().empty())
81-
return true;
82-
if(to_ssa_expr(expr).get_original_expr().type() != type)
83-
return true;
84-
}
85-
else
86-
{
87-
forall_operands(it, expr)
88-
if(check_renaming_l1(*it))
89-
return true;
90-
}
91-
92-
return false;
93-
}
94-
95-
static bool check_renaming(const exprt &expr)
96-
{
97-
if(check_renaming(expr.type()))
98-
return true;
99-
100-
if(
101-
expr.id() == ID_address_of &&
102-
to_address_of_expr(expr).object().id() == ID_symbol)
103-
{
104-
return check_renaming_l1(to_address_of_expr(expr).object());
105-
}
106-
else if(
107-
expr.id() == ID_address_of &&
108-
to_address_of_expr(expr).object().id() == ID_index)
109-
{
110-
const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
111-
return check_renaming_l1(index_expr.array()) ||
112-
check_renaming(index_expr.index());
113-
}
114-
else if(expr.id()==ID_symbol)
115-
{
116-
const auto &type = expr.type();
117-
if(!expr.get_bool(ID_C_SSA_symbol))
118-
return type.id() != ID_code && type.id() != ID_mathematical_function;
119-
if(to_ssa_expr(expr).get_level_2().empty())
120-
return true;
121-
if(to_ssa_expr(expr).get_original_expr().type() != type)
122-
return true;
123-
}
124-
else
125-
{
126-
forall_operands(it, expr)
127-
if(check_renaming(*it))
128-
return true;
129-
}
130-
131-
return false;
132-
}
133-
13450
template <>
13551
renamedt<ssa_exprt, L0>
13652
goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)
@@ -170,7 +86,7 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
17086
lhs.update_type();
17187
if(run_validation_checks)
17288
{
173-
DATA_INVARIANT(!check_renaming_l1(lhs), "lhs renaming failed on l1");
89+
DATA_INVARIANT(is_l1_renamed(lhs), "lhs renaming failed on l1");
17490
}
17591
const ssa_exprt l1_lhs = lhs;
17692

@@ -192,8 +108,8 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
192108

193109
if(run_validation_checks)
194110
{
195-
DATA_INVARIANT(!check_renaming(lhs), "lhs renaming failed on l2");
196-
DATA_INVARIANT(!check_renaming(rhs), "rhs renaming failed on l2");
111+
DATA_INVARIANT(is_l2_renamed(lhs), "lhs renaming failed on l2");
112+
DATA_INVARIANT(is_l2_renamed(rhs), "rhs renaming failed on l2");
197113
}
198114

199115
// see #305 on GitHub for a simple example and possible discussion
@@ -224,8 +140,8 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
224140

225141
if(run_validation_checks)
226142
{
227-
DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
228-
DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
143+
DATA_INVARIANT(is_l1_renamed(l1_lhs), "lhs renaming failed on l1");
144+
DATA_INVARIANT(is_l1_renamed(l1_rhs), "rhs renaming failed on l1");
229145
}
230146

231147
value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
@@ -461,7 +377,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
461377
source,
462378
symex_targett::assignment_typet::PHI);
463379

464-
INVARIANT(!check_renaming(ssa_l2), "expr should be renamed to L2");
380+
INVARIANT(is_l2_renamed(ssa_l2), "expr should be renamed to L2");
465381
expr = std::move(ssa_l2);
466382

467383
a_s_read.second.push_back(guard);

‎src/goto-symex/renamed.cpp

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
/*******************************************************************\
2+
3+
Module: Symbolic Execution
4+
5+
Author: Romain Brenguier, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Class for expressions or types renamed up to a given level
11+
12+
#include <util/std_expr.h>
13+
#include <util/ssa_expr.h>
14+
#include "renamed.h"
15+
16+
bool is_l1_renamed(const exprt &expr)
17+
{
18+
if(!is_l2_renamed(expr.type()))
19+
return false;
20+
21+
if(expr.id() == ID_symbol)
22+
{
23+
const auto &type = expr.type();
24+
if(!expr.get_bool(ID_C_SSA_symbol))
25+
return type.id() == ID_code || type.id() == ID_mathematical_function;
26+
if(!to_ssa_expr(expr).get_level_2().empty())
27+
return false;
28+
if(to_ssa_expr(expr).get_original_expr().type() != type)
29+
return false;
30+
}
31+
else
32+
{
33+
forall_operands(it, expr)
34+
if(!is_l1_renamed(*it))
35+
return false;
36+
}
37+
38+
return true;
39+
}
40+
41+
bool is_l2_renamed(const typet &type)
42+
{
43+
if(type.id() == ID_array)
44+
{
45+
if(!is_l2_renamed(to_array_type(type).size()))
46+
return false;
47+
}
48+
else if(type.id() == ID_struct || type.id() == ID_union)
49+
{
50+
for(const auto &c : to_struct_union_type(type).components())
51+
if(!is_l2_renamed(c.type()))
52+
return false;
53+
}
54+
else if(type.has_subtype() &&
55+
!is_l2_renamed(to_type_with_subtype(type).subtype()))
56+
{
57+
return false;
58+
}
59+
return true;
60+
}
61+
62+
bool is_l2_renamed(const exprt &expr)
63+
{
64+
if(!is_l2_renamed(expr.type()))
65+
return false;
66+
67+
if(
68+
expr.id() == ID_address_of &&
69+
to_address_of_expr(expr).object().id() == ID_symbol)
70+
{
71+
return is_l1_renamed(to_address_of_expr(expr).object());
72+
}
73+
else if(
74+
expr.id() == ID_address_of &&
75+
to_address_of_expr(expr).object().id() == ID_index)
76+
{
77+
const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
78+
return is_l1_renamed(index_expr.array()) &&
79+
is_l2_renamed(index_expr.index());
80+
}
81+
else if(expr.id() == ID_symbol)
82+
{
83+
const auto &type = expr.type();
84+
if(!expr.get_bool(ID_C_SSA_symbol))
85+
return (type.id() == ID_code || type.id() == ID_mathematical_function);
86+
if(to_ssa_expr(expr).get_level_2().empty())
87+
return false;
88+
if(to_ssa_expr(expr).get_original_expr().type() != type)
89+
return false;
90+
}
91+
else
92+
{
93+
forall_operands(it, expr)
94+
if(!is_l2_renamed(*it))
95+
return false;
96+
}
97+
return true;
98+
}
99+
100+
optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr)
101+
{
102+
if(is_l1_renamed(expr))
103+
return renamedt<exprt, L1>(std::move(expr));
104+
return {};
105+
}
106+
107+
optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr)
108+
{
109+
if(is_l2_renamed(expr))
110+
return renamedt<exprt, L2>(std::move(expr));
111+
return{};
112+
}
113+
114+
optionalt<renamedt<typet, L2>> check_l2_renaming(typet type)
115+
{
116+
if(is_l2_renamed(type))
117+
return renamedt<typet, L2>(std::move(type));
118+
return {};
119+
}

‎src/goto-symex/renamed.h

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,16 @@ Author: Romain Brenguier, [email protected]
1111
#ifndef CPROVER_GOTO_SYMEX_RENAMED_H
1212
#define CPROVER_GOTO_SYMEX_RENAMED_H
1313

14+
#include <functional>
15+
#include <type_traits>
16+
#include <util/nodiscard.h>
17+
#include <util/optional.h>
18+
#include <util/simplify_expr.h>
19+
20+
class typet;
21+
class exprt;
22+
class ssa_exprt;
23+
1424
/// Symex renaming level names.
1525
enum levelt
1626
{
@@ -65,6 +75,10 @@ class renamedt : private underlyingt
6575
typename renamedt<exprt, selectively_mutate_level>::mutator_functiont
6676
get_mutated_expr);
6777

78+
friend optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr);
79+
friend optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr);
80+
friend optionalt<renamedt<typet, L2>> check_l2_renaming(typet type);
81+
6882
/// Only the friend classes can create renamedt objects
6983
explicit renamedt(underlyingt value) : underlyingt(std::move(value))
7084
{
@@ -100,4 +114,22 @@ void selectively_mutate(
100114
}
101115
}
102116

117+
/// \return true if \p expr has been renamed to level 2
118+
bool is_l2_renamed(const exprt &expr);
119+
120+
/// \return true if \p type has been renamed to level 2
121+
bool is_l2_renamed(const typet &type);
122+
123+
/// \return true if \p expr has been renamed to level 1
124+
bool is_l1_renamed(const exprt &expr);
125+
126+
/// \return a renamed object if \p expr has been renamed to level 1
127+
NODISCARD optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr);
128+
129+
/// \return a renamed object if \p expr has been renamed to level 2
130+
NODISCARD optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr);
131+
132+
/// \return a renamed object if \p type has been renamed to level 2
133+
NODISCARD optionalt<renamedt<typet, L2>> check_l2_renaming(typet type);
134+
103135
#endif // CPROVER_GOTO_SYMEX_RENAMED_H

0 commit comments

Comments
 (0)