Skip to content

Commit 283bdbc

Browse files
tautschnigtautschnig
authored
Merge pull request #3187 from chrisr-diffblue/check-symbol-table-mappings
Check symbol table mappings
2 parents 89be4c9 + 0f18b68 commit 283bdbc

File tree

4 files changed

+169
-4
lines changed

4 files changed

+169
-4
lines changed

‎src/goto-programs/goto_model.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ class goto_modelt : public abstract_goto_modelt
9696
/// reported via DATA_INVARIANT violations or exceptions.
9797
void validate(const validation_modet vm) const
9898
{
99-
symbol_table.validate();
99+
symbol_table.validate(vm);
100100

101101
const namespacet ns(symbol_table);
102102
goto_functions.validate(ns, vm);

‎src/util/symbol_table.cpp

+96
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,9 @@
22

33
#include "symbol_table.h"
44

5+
#include <algorithm>
56
#include <util/invariant.h>
7+
#include <util/validate.h>
68

79
/// Move or copy a new symbol to the symbol table
810
/// \remark: This is a nicer interface than move and achieves the same
@@ -114,3 +116,97 @@ void symbol_tablet::erase(const symbolst::const_iterator &entry)
114116

115117
internal_symbols.erase(entry);
116118
}
119+
120+
/// Check whether the symbol table is in a valid state
121+
/// \param vm Determine whether to throw exceptions or trigger INVARIANT
122+
/// when validation fails
123+
void symbol_tablet::validate(const validation_modet vm) const
124+
{
125+
// Check that identifiers are mapped to the correct symbol
126+
for(const auto &elem : symbols)
127+
{
128+
const auto symbol_key = elem.first;
129+
const auto &symbol = elem.second;
130+
131+
// Check that symbols[id].name == id
132+
DATA_CHECK_WITH_DIAGNOSTICS(
133+
symbol.name == symbol_key,
134+
"Symbol table entry must map to a symbol with the correct identifier",
135+
"Symbol table key '",
136+
symbol_key,
137+
"' maps to symbol '",
138+
symbol.name,
139+
"'");
140+
141+
// Check that the symbol basename is mapped to its full name
142+
if(!symbol.base_name.empty())
143+
{
144+
const auto base_map_search =
145+
symbol_base_map.equal_range(symbol.base_name);
146+
const bool base_map_matches_symbol =
147+
std::find_if(
148+
base_map_search.first,
149+
base_map_search.second,
150+
[&symbol_key](const typename symbol_base_mapt::value_type &match) {
151+
return match.second == symbol_key;
152+
}) != symbol_base_map.end();
153+
154+
DATA_CHECK_WITH_DIAGNOSTICS(
155+
base_map_matches_symbol,
156+
"The base_name of a symbol should map to itself",
157+
"Symbol table key '",
158+
symbol_key,
159+
"' has a base_name '",
160+
symbol.base_name,
161+
"' which does not map to itself");
162+
}
163+
164+
// Check that the module name of the symbol is mapped to the full name
165+
if(!symbol.module.empty())
166+
{
167+
auto module_map_search = symbol_module_map.equal_range(symbol.module);
168+
bool module_map_matches_symbol =
169+
std::find_if(
170+
module_map_search.first,
171+
module_map_search.second,
172+
[&symbol_key](const typename symbol_module_mapt::value_type &match) {
173+
return match.second == symbol_key;
174+
}) != symbol_module_map.end();
175+
176+
DATA_CHECK_WITH_DIAGNOSTICS(
177+
module_map_matches_symbol,
178+
"Symbol table module map should map to symbol",
179+
"Symbol table key '",
180+
symbol_key,
181+
"' has a module name of '",
182+
symbol.module,
183+
"' which does not map to itself");
184+
}
185+
}
186+
187+
// Check that all base name map entries point to a symbol entry
188+
for(auto base_map_entry : symbol_base_map)
189+
{
190+
DATA_CHECK_WITH_DIAGNOSTICS(
191+
has_symbol(base_map_entry.second),
192+
"Symbol table base_name map entries must map to a symbol name",
193+
"base_name map entry '",
194+
base_map_entry.first,
195+
"' maps to non-existant symbol name '",
196+
base_map_entry.second,
197+
"'");
198+
}
199+
200+
// Check that all module map entries point to a symbol entry
201+
for(auto module_map_entry : symbol_module_map)
202+
{
203+
DATA_CHECK_WITH_DIAGNOSTICS(
204+
has_symbol(module_map_entry.second),
205+
"Symbol table module map entries must map to a symbol name",
206+
"base_name map entry '",
207+
module_map_entry.first,
208+
"' maps to non-existant symbol name '",
209+
module_map_entry.second,
210+
"'");
211+
}
212+
}

‎src/util/symbol_table.h

+1-3
Original file line numberDiff line numberDiff line change
@@ -111,9 +111,7 @@ class symbol_tablet : public symbol_table_baset
111111
}
112112

113113
/// Check that the symbol table is well-formed
114-
void validate() const
115-
{
116-
}
114+
void validate(const validation_modet vm = validation_modet::INVARIANT) const;
117115
};
118116

119117
#endif // CPROVER_UTIL_SYMBOL_TABLE_H

‎unit/util/symbol_table.cpp

+71
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
/// \file Tests for symbol_tablet
44

55
#include <testing-utils/catch.hpp>
6+
#include <util/exception_utils.h>
67
#include <util/journalling_symbol_table.h>
78

89
TEST_CASE("Iterating through a symbol table", "[core][utils][symbol_tablet]")
@@ -25,6 +26,76 @@ TEST_CASE("Iterating through a symbol table", "[core][utils][symbol_tablet]")
2526
REQUIRE(counter == 1);
2627
}
2728

29+
SCENARIO(
30+
"symbol_table_validity_checks",
31+
"[core][utils][symbol_table_validity_checks]")
32+
{
33+
GIVEN("A valid symbol table")
34+
{
35+
symbol_tablet symbol_table;
36+
37+
symbolt symbol;
38+
irep_idt symbol_name = "Test";
39+
symbol.name = symbol_name;
40+
symbol.base_name = "TestBase";
41+
symbol.module = "TestModule";
42+
43+
symbol_table.insert(symbol);
44+
45+
THEN("validate() should return")
46+
{
47+
symbol_table.validate(validation_modet::EXCEPTION);
48+
}
49+
WHEN("A symbol name is transformed without updating the symbol table")
50+
{
51+
symbolt &transformed_symbol = symbol_table.get_writeable_ref(symbol_name);
52+
transformed_symbol.name = "TransformTest";
53+
54+
THEN("validate() should throw an exception")
55+
{
56+
REQUIRE_THROWS_AS(
57+
symbol_table.validate(validation_modet::EXCEPTION),
58+
incorrect_goto_program_exceptiont);
59+
}
60+
// Reset symbol to a valid name after the previous test
61+
transformed_symbol.name = symbol_name;
62+
}
63+
WHEN(
64+
"A symbol base_name is transformed without updating the base_name "
65+
"mapping")
66+
{
67+
symbolt &transformed_symbol = symbol_table.get_writeable_ref(symbol_name);
68+
// Transform the symbol
69+
transformed_symbol.base_name = "TransformTestBase";
70+
71+
THEN("validate() should throw an exception")
72+
{
73+
REQUIRE_THROWS_AS(
74+
symbol_table.validate(validation_modet::EXCEPTION),
75+
incorrect_goto_program_exceptiont);
76+
}
77+
// Reset symbol to a valid base_name after the previous test
78+
transformed_symbol.base_name = "TestBase";
79+
}
80+
WHEN(
81+
"A symbol module identifier is transformed without updating the module "
82+
"mapping")
83+
{
84+
symbolt &transformed_symbol = symbol_table.get_writeable_ref(symbol_name);
85+
transformed_symbol.module = "TransformTestModule";
86+
87+
THEN("validate() should throw an exception")
88+
{
89+
REQUIRE_THROWS_AS(
90+
symbol_table.validate(validation_modet::EXCEPTION),
91+
incorrect_goto_program_exceptiont);
92+
}
93+
// Reset symbol to a valid module name
94+
transformed_symbol.module = "TestModule";
95+
}
96+
}
97+
}
98+
2899
SCENARIO("journalling_symbol_table_writer",
29100
"[core][utils][journalling_symbol_table_writer]")
30101
{

0 commit comments

Comments
 (0)