Skip to content

Fix handling of DEAD instructions and function call inlining #6473

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Nov 30, 2021
Merged

Fix handling of DEAD instructions and function call inlining #6473

Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
26760d3
fix writeset inclusion checks on DEAD instructions
SaswatPadhi Nov 24, 2021
911db55
refactor function call inling for code contracts
SaswatPadhi Nov 24, 2021
abd36cf
instrument loop head for inclusion checks as well
SaswatPadhi Nov 24, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 15 additions & 4 deletions src/goto-instrument/contracts/contracts.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -256,10 +256,13 @@ void code_contractst::check_apply_loop_contracts(
// Forward the loop_head iterator until the start of the body.
// This is necessary because complex C loop_head conditions could be
// converted to multiple GOTO instructions (e.g. temporaries are introduced).
// If the loop_head location shifts to a different function,
// assume that it's an inlined function and keep skipping.
// FIXME: This simple approach wouldn't work when
// the loop guard in the source file is split across multiple lines.
const auto head_loc = loop_head->source_location();
while(loop_head->source_location() == head_loc)
while(loop_head->source_location() == head_loc ||
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems fragile. An alternative solution could be to have the C front end inject LOCATION markers to precisely delimit loop entry, loop guard evaluation, loop condition test, loop body, loop step instructions, jump back to head instructions.

Copy link
Contributor Author

@SaswatPadhi SaswatPadhi Nov 24, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, @martin-cs suggested something similar (keeping some markers around), in my other PR.

I would suggest not to fix this this in the same PR especially because it would touch the C front end (parsing functions etc.) This PR is tiny and it only fixes the assigns clause issues (with DEAD) and makes it play well with function call inlining (modulo the existing issue with loop body finding).

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I agree with both. I have already had Opinions at @SaswatPadhi about loop structure detection (@remi-delmas-3000 did I CC you? If not I can resend. ); this is fragile and is asking for trouble and inconsistency with the rest of CPROVER. I think this functionality should be factored out and used in all appropriate places.

But I also agree with @SaswatPadhi ; that is outside of the scope of this PR.

loop_head->source_location().get_function() != head_loc.get_function())
loop_head++;

// At this point, we are just past the loop head,
Expand Down Expand Up @@ -678,6 +681,12 @@ void code_contractst::apply_loop_contract(
local_may_aliast local_may_alias(goto_function);
natural_loops_mutablet natural_loops(goto_function.body);

if(!natural_loops.loop_map.size())
return;

goto_function_inline(
goto_functions, function_name, ns, log.get_message_handler());
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As discussed offline: calls to goto_function_inline will require goto_functions.update() to be called afterwards.


Comment on lines +688 to +693
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

inlining after loop detection will miss loops that are hidden behind function calls that do not have contracts

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

which is okay? because they don't have contracts anyway?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't object but do note that this kind of inlining can get expensive.

// A graph node type that stores information about a loop.
// We create a DAG representing nesting of various loops in goto_function,
// sort them topologically, and instrument them in the top-sorted order.
Expand Down Expand Up @@ -992,7 +1001,11 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
function_obj->second.body, instruction_it, snapshot_instructions);
};

// Insert aliasing assertions
// Inline all function calls.
goto_function_inline(
goto_functions, function_obj->first, ns, log.get_message_handler());
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As above: call goto_functions.update()


// Insert write set inclusion checks.
check_frame_conditions(
function_obj->first,
function_obj->second.body,
Expand All @@ -1010,8 +1023,6 @@ void code_contractst::check_frame_conditions(
const goto_programt::targett &instruction_end,
assigns_clauset &assigns)
{
goto_function_inline(goto_functions, function, ns, log.get_message_handler());

for(; instruction_it != instruction_end; ++instruction_it)
{
const auto &pragmas = instruction_it->source_location().get_pragmas();
Expand Down