Skip to content
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

Jump to bottom

Contracts/DFCC: split conjunctions in loop invariants #8458

Merged
merged 1 commit into from
Sep 17, 2024
Merged

Contracts/DFCC: split conjunctions in loop invariants #8458

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
44 changes: 36 additions & 8 deletions src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -425,10 +425,24 @@
const irep_idt &language_mode =
dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
{
// Assume the loop invariant after havocing the state.
code_assumet assumption{invariant};
assumption.add_source_location() = loop_head_location;
converter.goto_convert(assumption, step_instrs, language_mode);
// Assume the loop invariant after havocing the state; produce one
// assumption per conjunct to ease analysis of counterexamples, and possibly

Check warning on line 429 in src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp#L429 

Added line #L429 was not covered by tests
// also improve solver performance (observed with Bitwuzla)
if(invariant.id() == ID_and)
{
for(const auto &op : invariant.operands())
{
code_assumet assumption{op};
assumption.add_source_location() = loop_head_location;
converter.goto_convert(assumption, step_instrs, language_mode);
}
tautschnig marked this conversation as resolved.
Show resolved Hide resolved
}
else

Check warning on line 440 in src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp#L440 

Added line #L440 was not covered by tests
{
code_assumet assumption{invariant};
assumption.add_source_location() = loop_head_location;
converter.goto_convert(assumption, step_instrs, language_mode);
}
}

{
Expand Down Expand Up @@ -506,10 +520,24 @@
"Check invariant after step for loop " +
id2string(check_location.get_function()) + "." +
std::to_string(cbmc_loop_id));
// Assume the loop invariant after havocing the state.
code_assertt assertion{invariant};
assertion.add_source_location() = check_location;
converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
// Assert the loop invariant after havocing the state; produce one assertion
// per conjunct to ease analysis of counterexamples, and possibly also

Check warning on line 524 in src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp#L524 

Added line #L524 was not covered by tests
// improve solver performance (observed with Bitwuzla)
if(invariant.id() == ID_and)
{
for(const auto &op : invariant.operands())
{
code_assertt assertion{op};
assertion.add_source_location() = check_location;
converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
}
}
else

Check warning on line 535 in src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp#L535 

Added line #L535 was not covered by tests
{
code_assertt assertion{invariant};
assertion.add_source_location() = check_location;
converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
}
}

{
Expand Down
Loading