Skip to content

Commit b25d6e5

Browse files
author
Remi Delmas
committed
CONTRACTS: avoid double map lookup
1 parent fe2ddda commit b25d6e5

File tree

1 file changed

+25
-21
lines changed

1 file changed

+25
-21
lines changed

src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp

Lines changed: 25 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -67,31 +67,35 @@ void dfcc_swap_and_wrapt::swap_and_wrap(
6767
std::set<irep_idt> &function_pointer_contracts,
6868
bool allow_recursive_calls)
6969
{
70-
auto found = cache.find(function_id);
71-
if(found != cache.end())
72-
{
73-
auto &pair = found->second;
70+
auto pair = cache.insert({function_id, {contract_id, contract_mode}});
71+
auto inserted = pair.second;
7472

73+
if(!inserted)
74+
{
75+
auto old_contract_id = pair.first->second.first;
76+
auto old_contract_mode = pair.first->second.second;
77+
78+
// different swapp already performed, abort
79+
if(old_contract_id != contract_id || old_contract_mode != contract_mode)
80+
{
81+
auto mode1 = (old_contract_mode == dfcc_contract_modet::REPLACE)
82+
? "REPLACE"
83+
: "CHECK";
84+
auto mode2 =
85+
(contract_mode == dfcc_contract_modet::REPLACE) ? "REPLACE" : "CHECK)";
86+
87+
std::ostringstream err_msg;
88+
err_msg << "DFCC: multiple attempts to swap and wrap function '"
89+
<< function_id << "':\n";
90+
err_msg << "- with '" << old_contract_id << "' in mode " << mode1 << "\n";
91+
err_msg << "- with '" << contract_id << "' in mode " << mode2 << "\n";
92+
throw invalid_input_exceptiont(err_msg.str());
93+
}
7594
// same swap already performed
76-
if(pair.first == contract_id && pair.second == contract_mode)
77-
return;
78-
79-
// already swapped with something else, abort
80-
auto mode1 =
81-
(pair.second == dfcc_contract_modet::REPLACE) ? "REPLACE" : "CHECK";
82-
auto mode2 =
83-
(contract_mode == dfcc_contract_modet::REPLACE) ? "REPLACE" : "CHECK)";
84-
85-
std::ostringstream err_msg;
86-
err_msg << "DFCC: multiple attempts to swap and wrap function '"
87-
<< function_id << "':\n";
88-
err_msg << "- with '" << pair.first << "' in mode " << mode1 << "\n";
89-
err_msg << "- with '" << contract_id << "' in mode " << mode2 << "\n";
90-
throw invalid_input_exceptiont(err_msg.str());
95+
return;
9196
}
9297

93-
cache.insert({function_id, {contract_id, contract_mode}});
94-
98+
// actually perform the translation
9599
switch(contract_mode)
96100
{
97101
case dfcc_contract_modet::CHECK:

0 commit comments

Comments
 (0)