Enforce purity on missing assigns clause

[feliperodri]

CBMC currently doesn't enforce assigns clauses if there isn't one.
However, whenever enforcing a function contract, the absence of an
assigns clause should be interpreted as an empty write set
(i.e., no inputs will be modified by this function).
CBMC now properly checks for empty assigns clause behavior.

Signed-off-by: Felipe R. Monteiro [email protected]

• 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.

[SaswatPadhi]

I just realized that the PR doesn't actually add support for __CPROVER_assigns(). It only checks for purity of functions when assigns clause is missing. So may be we can rename the PR (and update the commit message) to: "Enforce purity on missing assigns clause"?

[codecov]

Codecov Report

Merging #6074 (c29b69a) into develop (1f0d7b3) will increase coverage by 0.26%.
The diff coverage is 95.45%.

@@             Coverage Diff             @@
##           develop    #6074      +/-   ##
===========================================
+ Coverage    74.17%   74.44%   +0.26%     
===========================================
  Files         1446     1446              
  Lines       157784   157778       -6     
===========================================
+ Hits        117036   117456     +420     
+ Misses       40748    40322     -426     

Impacted Files	Coverage Δ
src/goto-instrument/code_contracts.cpp	84.74% <95.45%> (-0.01%)	⬇️
src/ansi-c/ansi_c_entry_point.cpp	65.88% <0.00%> (-21.50%)	⬇️
src/util/ieee_float.cpp	78.79% <0.00%> (-9.52%)	⬇️
src/util/file_util.cpp	71.42% <0.00%> (-5.36%)	⬇️
src/util/validate_code.cpp	80.00% <0.00%> (-5.00%)	⬇️
src/util/std_types.cpp	83.95% <0.00%> (-4.94%)	⬇️
src/ansi-c/preprocessor_line.cpp	91.66% <0.00%> (-4.17%)	⬇️
src/util/validate_types.cpp	92.30% <0.00%> (-3.85%)	⬇️
src/langapi/mode.cpp	90.47% <0.00%> (-2.39%)	⬇️
src/ansi-c/c_preprocess.cpp	31.19% <0.00%> (-1.75%)	⬇️
... and 10 more

---

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 749074b...c29b69a. Read the comment docs.

[kroening]

I just realized that the PR doesn't actually add support for __CPROVER_assigns(). It only checks for purity of functions when assigns clause is missing. So may be we can rename the PR (and update the commit message) to: "Enforce purity on missing assigns clause"?

Yes, renaming the PR would help!

[TGWDB]

I think this looks ok. There are some small tidying bits I noted, and I think it will fail regression tests (but this should just be fixing the test regexs). The only bit that is unclear to me is whether removing the old code that used to enforce failure is safe and won't break expected functionality. (Why was it written if this is fairly clearly failing when there is no assignment if this should instead be pure and not evaluated as a failure?)

[SaswatPadhi]

Approving since I don't have any additional comments, but let's fix all of the comments from @TGWDB.

[feliperodri]

The only bit that is unclear to me is whether removing the old code that used to enforce failure is safe and won't break expected functionality. (Why was it written if this is fairly clearly failing when there is no assignment if this should instead be pure and not evaluated as a failure?)

@TGWDB Before, when enforcing a contract for function foo, CBMC would fail if any of its inner functions don't have an assigns clause, even if the inner function preserve all inputs. This behavior is too restrict. If a function doesn't change any of the inputs, its assigns clause should be empty. On this PR, we do one step further and instead of adding a false assertion for functions without assigns clause, we check for purity of the inner functions (i.e., they don't change any of the inputs).

[chrisr-diffblue]

Looks good to me, thanks - with just one small sanity check on my part :-)

[chrisr-diffblue]

Just a check - is there a test case that will fail if this code ever gets inserted again? :-) It superficially looks like an "obvious" optimisation, so I can imaging someone in the future re-adding it with good intent.

[feliperodri]

If somebody add this back, assigns_enforce_15 will fail. For this case, we have assignments, but because there is no assigns clause, we wouldn't even complain about them. we should report an error in this case, because we want to enforce contracts across all functions using --enforce-all-contracts flag.