CBMC: /home/runner/work/cbmc/cbmc/src/util/symbol_table.cpp Source File

17 std::pair<symbolt &, bool> symbol_tablet::insert(symbolt symbol)

18{

19 // Add the symbol to the table or retrieve existing symbol with the same name

20 std::pair<symbolst::iterator, bool> result=

21 internal_symbols.emplace(symbol.name, std::move(symbol));

22 symbolt &new_symbol=result.first->second;

23 if(result.second)

24 {

25 try

26 {

27 symbol_base_mapt::iterator base_result=

28 internal_symbol_base_map.emplace(new_symbol.base_name, new_symbol.name);

29 if(!new_symbol.module.empty())

30 {

31 try

32 {

33 internal_symbol_module_map.emplace(

34 new_symbol.module, new_symbol.name);

35 }

36 catch(...)

37 {

38 internal_symbol_base_map.erase(base_result);

39 throw;

40 }

41 }

42 }

43 catch(...)

44 {

45 internal_symbols.erase(result.first);

46 throw;

47 }

48 }

49 return std::make_pair(std::ref(new_symbol), result.second);

50}

67 bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol)

68{

69 // Add an empty symbol to the table or retrieve existing symbol with same name

70 symbolt temp_symbol;

71 // This is not copying the symbol, this is passing the three required

72 // parameters to insert (just in the symbol)

73 temp_symbol.name=symbol.name;

74 temp_symbol.base_name=symbol.base_name;

75 temp_symbol.module=symbol.module;

76 std::pair<symbolt &, bool> result=insert(std::move(temp_symbol));

77 if(result.second)

78 {

79 // Move the provided symbol into the symbol table, this can't be done

80 // earlier

81 result.first.swap(symbol);

82 }

83 // Return the address of the symbol in the table

84 new_symbol=&result.first;

85 return !result.second;

86}

90 void symbol_tablet::erase(const symbolst::const_iterator &entry)

91{

92 const symbolt &symbol=entry->second;

93

94 auto base_it = symbol_base_map.lower_bound(symbol.base_name);

95 const auto base_it_end = symbol_base_map.upper_bound(symbol.base_name);

96 while(base_it!=base_it_end && base_it->second!=symbol.name)

97 ++base_it;

98 INVARIANT(

99 base_it!=base_it_end,

100 "symbolt::base_name should not be changed "

101 "after it is added to the symbol_table "

102 "(name: "+id2string(symbol.name)+", "

103 "current base_name: "+id2string(symbol.base_name)+")");

104 internal_symbol_base_map.erase(base_it);

105

106 if(!symbol.module.empty())

107 {

108 auto module_it = symbol_module_map.lower_bound(symbol.module);

109 auto module_it_end = symbol_module_map.upper_bound(symbol.module);

110 while(module_it != module_it_end && module_it->second != symbol.name)

111 ++module_it;

112 INVARIANT(

113 module_it != module_it_end,

114 "symbolt::module should not be changed "

115 "after it is added to the symbol_table "

116 "(name: " +

117 id2string(symbol.name) +

118 ", "

119 "current module: " +

120 id2string(symbol.module) + ")");

121 internal_symbol_module_map.erase(module_it);

122 }

123

124 internal_symbols.erase(entry);

125}

130 void symbol_tablet::validate(const validation_modet vm) const

131{

132 // Check that identifiers are mapped to the correct symbol

133 for(const auto &elem : symbols)

134 {

135 const auto symbol_key = elem.first;

136 const auto &symbol = elem.second;

137

138 // First of all, ensure symbol well-formedness

139 DATA_CHECK_WITH_DIAGNOSTICS(

140 vm, symbol.is_well_formed(), "Symbol is malformed: ", symbol_key);

141

142 // Check that symbols[id].name == id

143 DATA_CHECK_WITH_DIAGNOSTICS(

144 vm,

145 symbol.name == symbol_key,

146 "Symbol table entry must map to a symbol with the correct identifier",

147 "Symbol table key '",

148 symbol_key,

149 "' maps to symbol '",

150 symbol.name,

151 "'");

152

153 // Check that the symbol basename is mapped to its full name

154 if(!symbol.base_name.empty())

155 {

156 const auto base_map_search =

157 symbol_base_map.equal_range(symbol.base_name);

158 const bool base_map_matches_symbol =

159 std::find_if(

160 base_map_search.first,

161 base_map_search.second,

162 [&symbol_key](const symbol_base_mapt::value_type &match) {

163 return match.second == symbol_key;

164 }) != symbol_base_map.end();

165

166 DATA_CHECK_WITH_DIAGNOSTICS(

167 vm,

168 base_map_matches_symbol,

169 "The base_name of a symbol should map to itself",

170 "Symbol table key '",

171 symbol_key,

172 "' has a base_name '",

173 symbol.base_name,

174 "' which does not map to itself");

175 }

176

177 // Check that the module name of the symbol is mapped to the full name

178 if(!symbol.module.empty())

179 {

180 auto module_map_search = symbol_module_map.equal_range(symbol.module);

181 bool module_map_matches_symbol =

182 std::find_if(

183 module_map_search.first,

184 module_map_search.second,

185 [&symbol_key](const symbol_module_mapt::value_type &match) {

186 return match.second == symbol_key;

187 }) != symbol_module_map.end();

188

189 DATA_CHECK_WITH_DIAGNOSTICS(

190 vm,

191 module_map_matches_symbol,

192 "Symbol table module map should map to symbol",

193 "Symbol table key '",

194 symbol_key,

195 "' has a module name of '",

196 symbol.module,

197 "' which does not map to itself");

198 }

199 }

200

201 // Check that all base name map entries point to a symbol entry

202 for(auto base_map_entry : symbol_base_map)

203 {

204 DATA_CHECK_WITH_DIAGNOSTICS(

205 vm,

206 has_symbol(base_map_entry.second),

207 "Symbol table base_name map entries must map to a symbol name",

208 "base_name map entry '",

209 base_map_entry.first,

210 "' maps to non-existant symbol name '",

211 base_map_entry.second,

212 "'");

213 }

214

215 // Check that all module map entries point to a symbol entry

216 for(auto module_map_entry : symbol_module_map)

217 {

218 DATA_CHECK_WITH_DIAGNOSTICS(

219 vm,

220 has_symbol(module_map_entry.second),

221 "Symbol table module map entries must map to a symbol name",

222 "base_name map entry '",

223 module_map_entry.first,

224 "' maps to non-existant symbol name '",

225 module_map_entry.second,

226 "'");

227 }

228}

230 bool symbol_tablet::operator==(const symbol_tablet &other) const

231{

232 // we cannot use == for comparing the multimaps as it compares the items

233 // sequentially, but the order of items with equal keys depends on the

234 // insertion order

235

236 {

237 std::vector<std::pair<irep_idt, irep_idt>> v1(

238 internal_symbol_base_map.begin(), internal_symbol_base_map.end());

239

240 std::vector<std::pair<irep_idt, irep_idt>> v2(

241 other.internal_symbol_base_map.begin(),

242 other.internal_symbol_base_map.end());

243

244 std::sort(v1.begin(), v1.end());

245 std::sort(v2.begin(), v2.end());

246

247 if(v1 != v2)

248 return false;

249 }

250

251 {

252 std::vector<std::pair<irep_idt, irep_idt>> v1(

253 internal_symbol_module_map.begin(), internal_symbol_module_map.end());

254

255 std::vector<std::pair<irep_idt, irep_idt>> v2(

256 other.internal_symbol_module_map.begin(),

257 other.internal_symbol_module_map.end());

258

259 std::sort(v1.begin(), v1.end());

260 std::sort(v2.begin(), v2.end());

261

262 if(v1 != v2)

263 return false;

264 }

265

266 return internal_symbols == other.internal_symbols;

267}

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

symbol_table_baset::symbol_base_map

const symbol_base_mapt & symbol_base_map

Read-only field, used to look up symbol names given their base names.

Definition symbol_table_base.h:34

symbol_table_baset::symbol_module_map

const symbol_module_mapt & symbol_module_map

Read-only field, used to look up symbol names given their modules.

Definition symbol_table_base.h:39

symbol_table_baset::symbols

const symbolst & symbols

Read-only field, used to look up symbols given their names.

Definition symbol_table_base.h:31

symbol_table_baset::has_symbol

bool has_symbol(const irep_idt &name) const

Check whether a symbol exists in the symbol table.

Definition symbol_table_base.h:88

symbol_tablet

The symbol table.

Definition symbol_table.h:14

symbol_tablet::operator==

bool operator==(const symbol_tablet &other) const

Definition symbol_table.cpp:230

symbol_tablet::internal_symbols

symbolst internal_symbols

Value referenced by symbol_table_baset::symbols.

Definition symbol_table.h:17

symbol_tablet::erase

virtual void erase(const symbolst::const_iterator &entry) override

Remove a symbol from the symbol table.

Definition symbol_table.cpp:90

symbol_tablet::internal_symbol_module_map

symbol_module_mapt internal_symbol_module_map

Value referenced by symbol_table_baset::symbol_module_map.

Definition symbol_table.h:21

symbol_tablet::move

virtual bool move(symbolt &symbol, symbolt *&new_symbol) override

Move a symbol into the symbol table.

Definition symbol_table.cpp:67

symbol_tablet::internal_symbol_base_map

symbol_base_mapt internal_symbol_base_map

Value referenced by symbol_table_baset::symbol_base_map.

Definition symbol_table.h:19

symbol_tablet::insert

virtual std::pair< symbolt &, bool > insert(symbolt symbol) override

Author: Diffblue Ltd.

Definition symbol_table.cpp:17

symbol_tablet::validate

void validate(const validation_modet vm=validation_modet::INVARIANT) const override

Check that the symbol table is well-formed.

Definition symbol_table.cpp:130

symbolt

Symbol table entry.

Definition symbol.h:28

symbolt::name

irep_idt name

The unique identifier.

Definition symbol.h:40

symbolt::base_name

irep_idt irep_idt base_name

Name of module the symbol belongs to.

Definition symbol.h:46

id2string

const std::string & id2string(const irep_idt &d)

Definition irep.h:44

invariant.h

INVARIANT

#define INVARIANT(CONDITION, REASON)

This macro uses the wrapper function 'invariant_violated_string'.

Definition invariant.h:423

symbol_table.h

Author: Diffblue Ltd.

validate.h

DATA_CHECK_WITH_DIAGNOSTICS

#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)

Definition validate.h:37

validation_modet

validation_modet

Definition validation_mode.h:13