Skip to content

Commit d67621f

Browse files
smowtonOwen Jones
authored and
Owen Jones
committed
CSVSA: tolerate unreachable function calls
If a function call instruction exists but can't be reached (for example, because according to CSVSA's analysis we must throw a null-pointer exception before reaching the target callsite) then it will not exist in CSVSA's callee map. In this case simply rewrite the callsite to an ASSUME FALSE.
1 parent f7beab7 commit d67621f

File tree

1 file changed

+11
-1
lines changed

1 file changed

+11
-1
lines changed

src/driver/csvsa_specializer.cpp

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -438,6 +438,17 @@ goto_programt::targett csvsa_specializert::specialize_instruction(
438438
const auto &callee_map = context.get_callee_map();
439439

440440
// Replace virtual function calls with specific dispatch tables:
441+
auto child_nodes_it = callee_map.find(it->location_number);
442+
if(child_nodes_it == callee_map.end())
443+
{
444+
// This instruction was never examined by CSVSA -- it must be
445+
// unreachable.
446+
it->make_assumption(false_exprt());
447+
return it;
448+
}
449+
450+
const auto &child_nodes = child_nodes_it->second;
451+
441452
auto &function = to_code_function_call(instruction.code).function();
442453
if(function.id() == ID_virtual_function)
443454
{
@@ -487,7 +498,6 @@ goto_programt::targett csvsa_specializert::specialize_instruction(
487498
{
488499
// Static function call -- simply replace by the target specialization.
489500
auto &function_symbol = expr_dynamic_cast<symbol_exprt>(function);
490-
const auto &child_nodes = callee_map.at(it->location_number);
491501
INVARIANT(
492502
child_nodes.size() <= 1, "Non-virtual calls should have a single target");
493503
// If there are no children, this is a stub -- leave the call alone.

0 commit comments

Comments
 (0)