Enforce __CPROVER_loop_invariant contracts in goto-instrument #5884

SaswatPadhi · 2021-03-04T18:32:47Z

This PR resolves #5882.

It enforces __CPROVER_loop_invariant contract (in addition to function contracts) when --enforce-all-contracts or --enforce-contract <fun> flag is used with goto-instrument.

NOTE: The code_contracts.h and code_contracts.cpp files need a thorough clean up -- the return types seem inconsistent (void vs bool) for many functions that have similar behavior, and several functions don't use the C++11 range-based for loops etc. I would make a separate PR later for refactoring and cleanup. This PR only adds the invariant checking back into the contracts flags and enables related regression tests.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour. I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2021-03-04T19:32:13Z

Codecov Report

Merging #5884 (45b6d72) into develop (6779f39) will increase coverage by 0.04%.
The diff coverage is 82.60%.

@@             Coverage Diff             @@
##           develop    #5884      +/-   ##
===========================================
+ Coverage    72.90%   72.95%   +0.04%     
===========================================
  Files         1425     1425              
  Lines       154282   154281       -1     
===========================================
+ Hits        112485   112561      +76     
+ Misses       41797    41720      -77

Impacted Files	Coverage Δ
src/goto-instrument/code_contracts.h	`100.00% <ø> (ø)`
src/goto-instrument/code_contracts.cpp	`91.01% <82.60%> (+10.12%)`	⬆️
src/ansi-c/parser.y	`78.10% <0.00%> (+0.20%)`	⬆️
src/goto-programs/goto_convert.cpp	`90.86% <0.00%> (+0.59%)`	⬆️
src/analyses/cfg_dominators.h	`100.00% <0.00%> (+1.44%)`	⬆️
src/analyses/local_may_alias.cpp	`60.27% <0.00%> (+2.73%)`	⬆️
src/analyses/natural_loops.h	`100.00% <0.00%> (+5.40%)`	⬆️
src/goto-instrument/loop_utils.cpp	`63.63% <0.00%> (+38.63%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 7f998c4...45b6d72. Read the comment docs.

tautschnig · 2021-03-04T21:18:08Z

[...]

I would make a separate PR later for refactoring and cleanup. This PR only adds the invariant checking back into the contracts flags and enables related regression tests.

@SaswatPadhi Please make sure you sync with @feliperodri on this to avoid duplicate work.

feliperodri

I'd aslo recommend you to break down the PR into at least two commits: one for the changes in code_contracts.* files and another for the updates in the regression tests.

regression/contracts/invar_check_01/test.desc

regression/contracts/invar_loop_constant/test.desc

martin-cs

Seems good. Comments are only minor improvements. Thanks for the contribution.

regression/contracts/invar_check_break_pass/test.desc

regression/contracts/invar_check_continue/test.desc

regression/contracts/invar_check_large/test.desc

src/goto-instrument/code_contracts.cpp

hannes-steffenhagen-diffblue · 2021-03-05T11:12:59Z

src/goto-instrument/code_contracts.cpp

-  // look at all function calls
-  Forall_goto_program_instructions(ins, goto_function.body)
-    if(ins->is_function_call())
-      apply_contract(goto_function.body, ins);


Still d20bbe1

Case in point: In this case it's a bit hard for me to see why this loop was removed. It's combined with a fairly straightforward refactoring of the preceding loop so it's difficult for me see if this was an intentional change or a mistake that snuck in during refactoring.

This particular function was perhaps the old entry point for the old contracts flag. It was used to replace loops with invariant contracts and function calls with function contracts. I removed this loop intentionally because the replacement of calls with contracts now happens in replace_calls. You can see a very similar loop in replace_calls:

cbmc/src/goto-instrument/code_contracts.cpp

Lines 894 to 916 in 947fb8f

for(auto &goto_function : goto_functions.function_map)

{

Forall_goto_program_instructions(ins, goto_function.second.body)

{

if(ins->is_function_call())

{

const code_function_callt &call = ins->get_function_call();

// TODO we don't handle function pointers

if(call.function().id() != ID_symbol)

continue;

const irep_idt &fun_name =

to_symbol_expr(call.function()).get_identifier();

auto found = std::find(

funs_to_replace.begin(), funs_to_replace.end(), id2string(fun_name));

if(found == funs_to_replace.end())

continue;

fail |= apply_contract(goto_function.second.body, ins);

}

}

}

hannes-steffenhagen-diffblue

I'm ok with the actual changes, clang-format weirdness can be resolved (see my reply to your slack message), would prefer if the first commit was split up further before merging but not a blocker.

The `code_contracts` function was unused and the function contract application part of it was improved in `replace_calls`. This commit: - removes this old unused functionality, - renames `code_contracts` to `apply_loop_contract`, and - renames `apply_contract` to `apply_function_contract`.

Loop invariant annotations were being silently ignored when goto-instrument was invoked with `--enforce-contracts` or `--enforce-contract`. These flags now enforce both function and loop invariant contracts.

- Moved comments from .c files to descriptions in .desc files - Added new tests to check multiple loops, nested loops, loop-local variables - Enabled and clarified a regression test that was flagged as a buggy one

SaswatPadhi · 2021-03-05T18:18:42Z

Thanks for the review, @martin-cs and @hannes-steffenhagen-diffblue. I think I have addressed all your comments now. Please take another look and let me know if I should make any more changes.

martin-cs

Yep; looks good.

martin-cs · 2021-03-05T20:10:56Z

I realise this isn't really the right place to ask this but... if you are considering a reworking / rewrite of the code contracts stuff:

Is there any chance you could look at / incorporate / test / obsolete the k-induction code in goto-instrument? There were tests for this somewhere but I don't know if these are enabled.
Could it get added to the manual? I think we are close to having one of the best deductive verification tools for C ( and with @danielsn and @tautschnig 's work on s2n, one of the best used ) but no-one outside would know (I am aware that goto-analyze also needs documentation).

SaswatPadhi · 2021-03-05T20:45:39Z

Hi @martin-cs,

Yes sure, that sounds very related to what I am working on, so I should look at the k-induction code as well. I will take a look at the code and tests next week.
Good idea! @feliperodri is maintaining an internal Wiki page documenting the contracts stuff, but we should add these to the public manuals too. Could you please point us to where we should be adding them?

martin-cs · 2021-03-05T23:19:22Z

@SaswatPadhi

src/goto-instrument/k-induction.{h,cpp} and regression/k-induction but it is not routinely run so who knows if it still works!
doc/cprover-manual would be good.

SaswatPadhi requested review from chrisr-diffblue, hannes-steffenhagen-diffblue, martin-cs, peterschrammel and smowton as code owners March 4, 2021 18:32

chrisr-diffblue requested review from tautschnig, karkhaz and feliperodri March 4, 2021 18:36

tautschnig approved these changes Mar 4, 2021

View reviewed changes

feliperodri requested changes Mar 4, 2021

View reviewed changes

regression/contracts/invar_check_01/test.desc Outdated Show resolved Hide resolved

regression/contracts/invar_loop_constant/test.desc Outdated Show resolved Hide resolved

SaswatPadhi force-pushed the loop_invariant_contract_fix branch from a0a7304 to eae9473 Compare March 4, 2021 23:06

SaswatPadhi requested a review from feliperodri March 4, 2021 23:10

feliperodri approved these changes Mar 4, 2021

View reviewed changes

SaswatPadhi force-pushed the loop_invariant_contract_fix branch 2 times, most recently from 4c4c2cd to 5564547 Compare March 5, 2021 00:28

feliperodri added aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Mar 5, 2021

martin-cs approved these changes Mar 5, 2021

View reviewed changes

regression/contracts/invar_check_break_pass/test.desc Show resolved Hide resolved

regression/contracts/invar_check_continue/test.desc Show resolved Hide resolved

regression/contracts/invar_check_large/test.desc Outdated Show resolved Hide resolved

hannes-steffenhagen-diffblue reviewed Mar 5, 2021

View reviewed changes

hannes-steffenhagen-diffblue approved these changes Mar 5, 2021

View reviewed changes

SaswatPadhi added 3 commits March 5, 2021 11:09

Minor refactoring and documentation changes

1b2cdc6

Enforce __CPROVER_loop_invariant contracts

aede6f9

Loop invariant annotations were being silently ignored when goto-instrument was invoked with `--enforce-contracts` or `--enforce-contract`. These flags now enforce both function and loop invariant contracts.

SaswatPadhi force-pushed the loop_invariant_contract_fix branch from 5564547 to 142ff6a Compare March 5, 2021 18:15

Improved regression tests for invariant contract

45b6d72

- Moved comments from .c files to descriptions in .desc files - Added new tests to check multiple loops, nested loops, loop-local variables - Enabled and clarified a regression test that was flagged as a buggy one

SaswatPadhi force-pushed the loop_invariant_contract_fix branch from 142ff6a to 45b6d72 Compare March 5, 2021 18:17

SaswatPadhi changed the title ~~Loop invariant contracts are now enforced~~ Enforce __CPROVER_loop_invariant contracts in goto-instrument Mar 5, 2021

martin-cs approved these changes Mar 5, 2021

View reviewed changes

feliperodri merged commit 6ad479d into diffblue:develop Mar 5, 2021

SaswatPadhi deleted the loop_invariant_contract_fix branch March 5, 2021 20:42

feliperodri assigned SaswatPadhi Apr 1, 2021

feliperodri added the bugfix label Apr 1, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Enforce __CPROVER_loop_invariant contracts in goto-instrument #5884

Enforce __CPROVER_loop_invariant contracts in goto-instrument #5884

Uh oh!

SaswatPadhi commented Mar 4, 2021

Uh oh!

codecov bot commented Mar 4, 2021 •

edited

Loading

Uh oh!

tautschnig commented Mar 4, 2021

Uh oh!

feliperodri left a comment

Uh oh!

Uh oh!

Uh oh!

martin-cs left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue Mar 5, 2021

Uh oh!

SaswatPadhi Mar 5, 2021 •

edited

Loading

Uh oh!

hannes-steffenhagen-diffblue left a comment

Uh oh!

SaswatPadhi commented Mar 5, 2021

Uh oh!

martin-cs left a comment

Uh oh!

martin-cs commented Mar 5, 2021

Uh oh!

SaswatPadhi commented Mar 5, 2021

Uh oh!

martin-cs commented Mar 5, 2021

Uh oh!

Uh oh!

	for(auto &goto_function : goto_functions.function_map)
	{
	Forall_goto_program_instructions(ins, goto_function.second.body)
	{
	if(ins->is_function_call())
	{
	const code_function_callt &call = ins->get_function_call();

	// TODO we don't handle function pointers
	if(call.function().id() != ID_symbol)
	continue;

	const irep_idt &fun_name =
	to_symbol_expr(call.function()).get_identifier();
	auto found = std::find(
	funs_to_replace.begin(), funs_to_replace.end(), id2string(fun_name));
	if(found == funs_to_replace.end())
	continue;

	fail \|= apply_contract(goto_function.second.body, ins);
	}
	}
	}

Enforce __CPROVER_loop_invariant contracts in goto-instrument #5884

Enforce __CPROVER_loop_invariant contracts in goto-instrument #5884

Uh oh!

Conversation

SaswatPadhi commented Mar 4, 2021

Uh oh!

codecov bot commented Mar 4, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

tautschnig commented Mar 4, 2021

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue Mar 5, 2021

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi Mar 5, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi commented Mar 5, 2021

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Mar 5, 2021

Uh oh!

SaswatPadhi commented Mar 5, 2021

Uh oh!

martin-cs commented Mar 5, 2021

Uh oh!

Uh oh!

codecov bot commented Mar 4, 2021 •

edited

Loading

SaswatPadhi Mar 5, 2021 •

edited

Loading