Unify havocing codegen within code contracts #6292

SaswatPadhi · 2021-08-12T00:16:52Z

Resolves #6235.

In this PR, we unify the havocing code generation for both loop & function contracts.

This fixes multiple known issues:

(function contracts) entire arrays were not being havoced
(loop contracts) pointers not checked for nullness before havocing

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.
n/a ~~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).
n/a ~~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-08-12T01:27:30Z

Codecov Report

Merging #6292 (55cbcb7) into develop (a0a1329) will decrease coverage by 0.00%.
The diff coverage is 97.87%.

@@             Coverage Diff             @@
##           develop    #6292      +/-   ##
===========================================
- Coverage    75.98%   75.98%   -0.01%     
===========================================
  Files         1510     1512       +2     
  Lines       163467   163471       +4     
===========================================
- Hits        124213   124209       -4     
- Misses       39254    39262       +8

Impacted Files	Coverage Δ
src/goto-instrument/contracts/assigns.h	`100.00% <ø> (ø)`
src/goto-instrument/havoc_loops.cpp	`0.00% <0.00%> (ø)`
src/goto-instrument/loop_utils.cpp	`90.62% <ø> (-3.93%)`	⬇️
src/goto-instrument/contracts/assigns.cpp	`98.29% <100.00%> (-0.25%)`	⬇️
src/goto-instrument/contracts/contracts.cpp	`92.59% <100.00%> (ø)`
src/goto-instrument/havoc_utils.cpp	`100.00% <100.00%> (ø)`
src/goto-instrument/havoc_utils.h	`100.00% <100.00%> (ø)`
src/goto-instrument/k_induction.cpp	`96.22% <100.00%> (ø)`
src/solvers/smt2/smt2_conv.cpp	`66.50% <0.00%> (-0.20%)`	⬇️
... and 1 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 3092e7b...55cbcb7. Read the comment docs.

feliperodri

Thanks for implementing this fix!! Just a few comments.

feliperodri · 2021-08-12T03:06:42Z

src/goto-instrument/havoc_utils.h

+void append_havoc_code(
+  const source_locationt source_location,
+  const modifiest &modifies,
+  goto_programt &dest);
+
+void append_object_havoc_code_for_expr(
+  const source_locationt source_location,
+  const exprt &expr,
+  goto_programt &dest);
+
+void append_scalar_havoc_code_for_expr(
+  const source_locationt source_location,
+  const exprt &expr,
+  goto_programt &dest);


Why the suffix "append"? Perhaps we can come up with more intuitive names. What do you think about havoc_code, havoc_object, and havoc_scalar?

The original prefix was build and it was inserting goto statements at the end of the dest goto program. I was always confused about whether it adds the statements at the beginning or at the end, so I just changed build -> append. What part of the name is unintuitive?

The names havoc_code, havoc_object, and havoc_scalar seem okay but lead to the same confusion as build. Also notice that append_havoc_code takes an entire modifies set, but the append_*_havoc_code_for_expr functions take exprt.

The editor autocompletes anyway, so I just use longer function names that are more explicit about their effect.

This is not a blocker, since it is probably just a style matter. For me, clear and concise method names yields clear code.

I was always confused about whether it adds the statements at the beginning or at the end, so I just changed build -> append.

I'd add this information to a header comment in each method. This will also help us to build document for this file using Doxygen. Some editors also pick up this information. For instance, take a look at this method:

cbmc/src/goto-instrument/contracts/contracts.h

Lines 74 to 87 in 0bbbe19

/// \brief Replace all calls to each function in the list with that function's

/// contract

///

/// Use this function when proving code that calls into an expensive function,

/// `F`. You can write a contract for F using __CPROVER_requires and

/// __CPROVER_ensures, and then use this function to replace all calls to `F`

/// with an assertion that the `requires` clause holds followed by an

/// assumption that the `ensures` clause holds. In order to ensure that `F`

/// actually abides by its `ensures` and `requires` clauses, you should

/// separately call `code_constractst::enforce_contracts()` on `F` and verify

/// it using `cbmc --function F`.

///

/// \return `true` on failure, `false` otherwise

bool replace_calls(const std::set<std::string> &functions);

Also notice that append_havoc_code takes an entire modifies set, but the append_*_havoc_code_for_expr functions take exprt.

This is the type of information that could easily go to a comment header or inferred just by looking at the parameters.

Thanks, I agree I should add some comments here regardless, but for now I think I will leave append_*_havoc_code_for_expr and append_havoc_code, unless there is something specific that's incorrect / confusing about these names.

What do you think about havoc_code, havoc_object, and havoc_scalar?

I thought a bit more about these names, but havoc_code seems incorrect -- it doesn't havoc a codet but a set<exprt>.

I guess we can revisit this later when we add comments & documentation for our functions.

Personally, I like the append_*_ naming :-)

feliperodri · 2021-08-12T03:08:49Z

src/goto-instrument/contracts/assigns.cpp

+  modifiest modifies;
+  std::for_each(
+    targets.begin(),
+    targets.end(),
+    [&modifies](const assigns_clause_targett *t) {
+      modifies.insert(to_address_of_expr(t->get_direct_pointer()).object());
+    });


Very clean 👏 nice!

😄 Thanks!

While writing this transformation, I noticed that targets is a vector, unlike modifies, which is a set. If we write the same expression twice in the __CPROVER_assigns clause, would we end up havocing / enforcing it twice? Or, does the parser / typechecker somehow guard against this?

If we write the same expression twice in the __CPROVER_assigns clause, would we end up havocing / enforcing it twice? Or, does the parser / typechecker somehow guard against this?

We don't have any regression tests that cover this behavior. Could you write a regression test that cover this scenario for both loop contracts and function contracts?

While writing this transformation, I noticed that targets is a vector, unlike modifies, which is a set.

Could you turn targets into a set too? Regardless of our type-checking procedure, set would be a more appropriate data structure here.

These modifications might be part of a separate PR. I'm happy to implement it too if that's the case.

Currently this is not a concern for loops because we don't allow manual assigns clause annotation yet.

I would separate this refactor (vector -> set) into another PR though. I'll open an internal ticket to track it.

src/goto-instrument/havoc_utils.cpp

feliperodri

I don't have any more blocking comments. 🚀

This change fixes multiple known issues: - (function contracts) entire arrays were not being havoced - (loop contracts) pointers not checked for nullness before havocing

SaswatPadhi added bugfix aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Aug 12, 2021

SaswatPadhi self-assigned this Aug 12, 2021

SaswatPadhi requested review from chrisr-diffblue, feliperodri, martin-cs, peterschrammel and tautschnig as code owners August 12, 2021 00:16

SaswatPadhi force-pushed the havoc_fix branch 5 times, most recently from 0cbf501 to d84d2b4 Compare August 12, 2021 00:56

SaswatPadhi changed the title ~~Unify havocing within code contracts~~ Unify havocing codegen within code contracts Aug 12, 2021

feliperodri requested changes Aug 12, 2021

View reviewed changes

SaswatPadhi force-pushed the havoc_fix branch 2 times, most recently from 209f403 to 64fe788 Compare August 12, 2021 04:09

Refactor out havoc utility functions

d0d2522

SaswatPadhi force-pushed the havoc_fix branch from 64fe788 to cdb760e Compare August 12, 2021 04:13

SaswatPadhi requested a review from feliperodri August 12, 2021 04:17

feliperodri approved these changes Aug 13, 2021

View reviewed changes

Unify havocing code for all contracts

55cbcb7

This change fixes multiple known issues: - (function contracts) entire arrays were not being havoced - (loop contracts) pointers not checked for nullness before havocing

SaswatPadhi force-pushed the havoc_fix branch from cdb760e to 55cbcb7 Compare August 17, 2021 16:45

chrisr-diffblue approved these changes Aug 18, 2021

View reviewed changes

SaswatPadhi merged commit 1268cc1 into diffblue:develop Aug 18, 2021

SaswatPadhi deleted the havoc_fix branch August 18, 2021 14:12

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Unify havocing codegen within code contracts #6292

Unify havocing codegen within code contracts #6292

Uh oh!

SaswatPadhi commented Aug 12, 2021 •

edited

Loading

Uh oh!

codecov bot commented Aug 12, 2021 •

edited

Loading

Uh oh!

feliperodri left a comment

Uh oh!

feliperodri Aug 12, 2021

Uh oh!

SaswatPadhi Aug 12, 2021

Uh oh!

feliperodri Aug 13, 2021

Uh oh!

SaswatPadhi Aug 17, 2021

Uh oh!

chrisr-diffblue Aug 18, 2021

Uh oh!

feliperodri Aug 12, 2021

Uh oh!

SaswatPadhi Aug 12, 2021

Uh oh!

feliperodri Aug 13, 2021

Uh oh!

SaswatPadhi Aug 17, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri left a comment

Uh oh!

Uh oh!

	/// \brief Replace all calls to each function in the list with that function's
	/// contract
	///
	/// Use this function when proving code that calls into an expensive function,
	/// `F`. You can write a contract for F using __CPROVER_requires and
	/// __CPROVER_ensures, and then use this function to replace all calls to `F`
	/// with an assertion that the `requires` clause holds followed by an
	/// assumption that the `ensures` clause holds. In order to ensure that `F`
	/// actually abides by its `ensures` and `requires` clauses, you should
	/// separately call `code_constractst::enforce_contracts()` on `F` and verify
	/// it using `cbmc --function F`.
	///
	/// \return `true` on failure, `false` otherwise
	bool replace_calls(const std::set<std::string> &functions);

Unify havocing codegen within code contracts #6292

Unify havocing codegen within code contracts #6292

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

SaswatPadhi commented Aug 12, 2021 •

edited

Loading

codecov bot commented Aug 12, 2021 •

edited

Loading