CONTRACTS: adding requires and ensures clauses for function pointers #6821

remi-delmas-3000 · 2022-04-22T21:53:21Z

Adding syntax extensions and typechecking for two new contract clauses:

__CPROVER_requires_contract(function_pointer, contract_symbol)
__CPROVER_ensures_contract(function_pointer, contract_symbol)

These clauses allow to specify pre and post conditions about function pointers. The first parameter must be a function-pointer-typed lvalue expression, without side effects of disjunctions. The second parameter must be a contract symbol (ie a function symbol that carries a contract). A simple enforcement/replacement : assign said contract to the pointer for assumptions (replace ensures, enforce requires) or check that the pointer is equal to said contract symbol (replace requires, enforce ensures).

Used in combination with --restrict-function-pointer and --replace-call-with-contract they allow to model and use proof assumptions about function pointers.

see code example here and command line switches here

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.
[NOT YET] 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 · 2022-04-25T19:11:17Z

Codecov Report

Merging #6821 (6d37049) into develop (09cc397) will increase coverage by 0.00%.
The diff coverage is 83.05%.

❗ Current head 6d37049 differs from pull request most recent head 63cd722. Consider uploading reports for the commit 63cd722 to get more accurate results

@@            Coverage Diff            @@
##           develop    #6821    +/-   ##
=========================================
  Coverage    77.03%   77.03%            
=========================================
  Files         1594     1594            
  Lines       185016   185174   +158     
=========================================
+ Hits        142520   142647   +127     
- Misses       42496    42527    +31

Impacted Files	Coverage Δ
src/ansi-c/ansi_c_convert_type.h	`100.00% <ø> (ø)`
src/ansi-c/c_typecheck_base.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/ansi-c/c_typecheck_code.cpp	`77.15% <43.75%> (-2.89%)`	⬇️
src/goto-instrument/contracts/contracts.cpp	`94.42% <93.47%> (-0.07%)`	⬇️
src/ansi-c/ansi_c_convert_type.cpp	`80.69% <100.00%> (+0.55%)`	⬆️
src/ansi-c/c_expr.h	`100.00% <100.00%> (ø)`
src/ansi-c/c_typecheck_base.cpp	`78.88% <100.00%> (+0.55%)`	⬆️
src/ansi-c/parser.y	`80.22% <100.00%> (+0.18%)`	⬆️
src/ansi-c/scanner.l	`63.37% <100.00%> (+0.06%)`	⬆️
... and 6 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 e3dd810...63cd722. Read the comment docs.

tautschnig · 2022-04-26T21:29:06Z

src/ansi-c/c_expr.h

+  return ret;
+}
+
+/// \copydoc to_function_pointer_obeys_contract_expr_expr(const exprt &expr)


Duplicate _expr in copydoc.

tautschnig · 2022-04-26T21:30:24Z

src/ansi-c/c_typecheck_code.cpp

+    error().source_location = expr.source_location();
+    error() << "expected ID_function_pointer_obeys_contract expression in "
+               "requires_contract/ensures_contract clause, found "
+            << id2string(expr.id()) << eom;


Nit pick: id2string is not needed here, operator<< will take care.

tautschnig · 2022-04-26T21:31:15Z

src/ansi-c/c_typecheck_code.cpp

+  {
+    error().source_location = function_pointer.source_location();
+    error() << "first parameter of the clause must have no ternary operator"
+            << eom;
+  }


Missing throw 0;

tautschnig · 2022-04-26T21:34:15Z

src/ansi-c/parser.y

+        {
+          $$=$1;
+          set($$, ID_C_spec_ensures_contract);
+          exprt tmp = exprt(ID_function_pointer_obeys_contract);


exprt tmp(ID_function_pointer_obeys_contract);

tautschnig · 2022-04-26T21:34:32Z

src/ansi-c/parser.y

+        {
+          $$=$1;
+          set($$, ID_C_spec_requires_contract);
+          exprt tmp = exprt(ID_function_pointer_obeys_contract);


exprt tmp(ID_function_pointer_obeys_contract);

src/ansi-c/scanner.l

tautschnig · 2022-04-26T21:36:12Z

src/goto-instrument/contracts/contracts.cpp

+  for(auto &expr : requires_contract)
+  {
+    auto &obeys_expr = to_function_pointer_obeys_contract_expr(expr);
+    replace_symbolt replace(common_replace);


I don't think you need to take a copy here, just use common_replace directly two lines later.

tautschnig · 2022-04-26T21:36:31Z

src/goto-instrument/contracts/contracts.cpp

+  for(auto &expr : ensures_contract)
+  {
+    auto &obeys_expr = to_function_pointer_obeys_contract_expr(expr);
+    replace_symbolt replace(common_replace);


As above, no need for a copy.

tautschnig · 2022-04-26T21:36:46Z

src/goto-instrument/contracts/contracts.cpp

+  for(auto &expr : requires_contract)
+  {
+    auto &obeys_expr = to_function_pointer_obeys_contract_expr(expr);
+    replace_symbolt replace(common_replace);


No need for a copy.

tautschnig · 2022-04-26T21:37:25Z

src/goto-instrument/contracts/contracts.cpp

+  for(auto &expr : ensures_contract)
+  {
+    auto &obeys_expr = to_function_pointer_obeys_contract_expr(expr);
+    replace_symbolt replace(common_replace);


No need for a copy. (And now I'm starting to wonder why a very similar (the same?) code exists multiple times.

(And now I'm starting to wonder why a very similar (the same?) code exists multiple times

This is mostly because I'm lazy :). The code is now factored into two separate methods.

remi-delmas-3000 · 2022-04-27T19:02:17Z

Thank you @tautschnig I took into account all your comments.

tautschnig · 2022-04-27T19:23:27Z

src/goto-instrument/contracts/contracts.cpp

+  for(auto &expr : requires_contract)
+    assert_function_pointer_obeys_contract(
+      to_function_pointer_obeys_contract_expr(expr),
+      ID_precondition,
+      common_replace,
+      mode,
+      new_program);


Braces around the body, please.

tautschnig · 2022-04-27T19:24:05Z

src/goto-instrument/contracts/contracts.cpp

+  for(auto &expr : ensures_contract)
+    assume_function_pointer_obeys_contract(
+      to_function_pointer_obeys_contract_expr(expr),
+      ID_postcondition,
+      common_replace,
+      new_program);


Braces around the body, please.

tautschnig · 2022-04-27T19:27:25Z

src/goto-instrument/contracts/contracts.cpp

+  for(auto &expr : requires_contract)
+    assume_function_pointer_obeys_contract(
+      to_function_pointer_obeys_contract_expr(expr),
+      ID_precondition,
+      common_replace,
+      check);


Braces around body, please.

tautschnig · 2022-04-27T19:27:33Z

src/goto-instrument/contracts/contracts.cpp

+  for(auto &expr : ensures_contract)
+    assert_function_pointer_obeys_contract(
+      to_function_pointer_obeys_contract_expr(expr),
+      ID_postcondition,
+      common_replace,
+      function_symbol.mode,
+      check);


Braces around body, please.

src/goto-instrument/contracts/contracts.cpp

Syntax extensions and typechecking, and simple contract enforcement and replacement logic.

remi-delmas-3000 · 2022-04-27T20:38:22Z

src/langapi/language_util.cpp


-#include <memory>
-
-#include <util/symbol_table.h>
+#include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
+#include <util/symbol_table.h>

 #include "language.h"
 #include "mode.h"

+#include <memory>


I had to reorder the includes section to match the current clang-format rules, but it makes me feel like the priority is listed in inverse order in the rules (usually we want standard lib includes first then local headers and then other deps).

IncludeBlocks: Regroup IncludeCategories: - Regex: '_class.h(>|")$' Priority: 0 - Regex: '<util/' Priority: 1 - Regex: '<goto-programs/' Priority: 2 - Regex: '<.+/.+>' Priority: 3 - Regex: '^"[^/]+"$' Priority: 4 - Regex: '<[^/]+>' Priority: 5

It's in that order on purpose (I can say so as this piece of code is my fault). My rationale for placing STL headers last is that it will help surface missing includes that would suddenly bite when a header file is newly used in another place. But maybe that's a bad idea?

I have no objections to this new ordering and it's actually good to know if any other include file is inadvertently missing an stl include.

I was just surprised by global reordering effect of adding a single new line in the existing block of #include <utils/*.h>. Let's keep using the new ordering policy.

Yes, it does result in some short-term churn, but should lead to eventual consistency. Previously, there were unwritten rules for how includes are to be ordered, but no automated enforcement.

remi-delmas-3000 requested review from tautschnig, feliperodri, SaswatPadhi, kroening, peterschrammel and chris-ryder as code owners April 22, 2022 21:53

remi-delmas-3000 self-assigned this Apr 22, 2022

remi-delmas-3000 added aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts labels Apr 22, 2022

remi-delmas-3000 force-pushed the contracts-obeys-clause branch 3 times, most recently from 10ab523 to ef03bb1 Compare April 25, 2022 18:18

tautschnig reviewed Apr 26, 2022

View reviewed changes

remi-delmas-3000 force-pushed the contracts-obeys-clause branch from ef03bb1 to 136855e Compare April 27, 2022 19:21

tautschnig approved these changes Apr 27, 2022

View reviewed changes

remi-delmas-3000 force-pushed the contracts-obeys-clause branch from 136855e to ebe7c4d Compare April 27, 2022 20:21

CONTRACTS: adding requires and ensures clauses for function pointers

63cd722

Syntax extensions and typechecking, and simple contract enforcement and replacement logic.

remi-delmas-3000 force-pushed the contracts-obeys-clause branch from 6d37049 to 63cd722 Compare April 27, 2022 20:36

remi-delmas-3000 commented Apr 27, 2022

View reviewed changes

remi-delmas-3000 merged commit 142db0b into diffblue:develop Apr 27, 2022

CONTRACTS: adding requires and ensures clauses for function pointers #6821

CONTRACTS: adding requires and ensures clauses for function pointers #6821

Uh oh!

Conversation

remi-delmas-3000 commented Apr 22, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Apr 25, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

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!

Choose a reason for hiding this comment

Uh oh!

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!

remi-delmas-3000 commented Apr 27, 2022

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!

remi-delmas-3000 Apr 27, 2022 • 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!

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!

remi-delmas-3000 commented Apr 22, 2022 •

edited

Loading

codecov bot commented Apr 25, 2022 •

edited

Loading

remi-delmas-3000 Apr 27, 2022 •

edited

Loading