Function contracts: preliminary support for conditional targets in assigns clause checking #6546

remi-delmas-3000 · 2021-12-23T03:32:06Z

This PR adds support for conditional targets in assigns clauses.

A conditional target specifies a memory location that can be assigned by a function only when a condition holds at the call site.

When a function call is replaced by its contract, conditional targets are havocked only if the condition holds at the call site.

Syntax

comma separated list of targets can now be preceded by condition :, and multiple target lists with or without conditions are separated by ;:

__CPROVER_assigns(
a, b, c; // unconditional targets
condition: x, y, z; // conditional targets
!condition && other_condition: q, r, t; // conditional targets
)

Use cases

These conditional targets allow the user to specify frame conditions for functions that have distinct modes of operation and assign different locations depending on the mode.

They also allow the user to specify validity conditions for the assigned locations, in case they are accessed through chains of struct/union member selections, pointer dereferences, can are not always valid. For instance in the example below, cond would be a condition which guarantees that the target expression corresponds to a valid memory location:

__CPROVER_assigns(cond: p->union.member->array[idx]->member)

Changes

In the ansi-c front-end

In the parser, modify the target rule to accept the new syntax;
Add an new expression class and irep_id for the new construct;
Update the expr2ct expression formatter class to print the new expression type;
Add typechecking rules:
- targets must be lvalues, without ternary operators or side-effects;
- conditions are still allowed to contain side_effect_function_callt but no other side_effect_exprt subtypes.

Remark: In a future PR we will check that any function used in a condition is side-effect-free, i.e. has a contract with an empty assigns clause. For now we trust the user not to use side-effecting functions in conditions.

In the contracts/assigns.{h|c} code:

Add an explicit guard expression to the internal representation of assigns clause targets;
Update the CAR validity condition to guard && all_deref_valid(target) && rw_ok(target, size);
Propagate these changes to the instrumentation of assigns clause checking;
Propagate these changes to the havocking of targets for contract replacement.

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-12-23T04:37:27Z

Codecov Report

Merging #6546 (e3d694d) into develop (bd1401f) will increase coverage by 0.02%.
The diff coverage is 91.53%.

❗ Current head e3d694d differs from pull request most recent head 4a10dd4. Consider uploading reports for the commit 4a10dd4 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6546      +/-   ##
===========================================
+ Coverage    75.99%   76.01%   +0.02%     
===========================================
  Files         1579     1579              
  Lines       181124   181240     +116     
===========================================
+ Hits        137643   137774     +131     
+ Misses       43481    43466      -15

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_base.h	`100.00% <ø> (ø)`
src/ansi-c/c_typecheck_code.cpp	`80.70% <86.84%> (+1.04%)`	⬆️
src/goto-instrument/contracts/assigns.cpp	`95.68% <96.42%> (-0.15%)`	⬇️
src/ansi-c/parser.y	`79.60% <100.00%> (+0.31%)`	⬆️
src/goto-instrument/contracts/assigns.h	`100.00% <100.00%> (ø)`
src/util/std_code.h	`94.06% <0.00%> (+0.01%)`	⬆️
src/solvers/lowering/byte_operators.cpp	`92.25% <0.00%> (+0.09%)`	⬆️
src/pointer-analysis/value_set.cpp	`82.84% <0.00%> (+0.10%)`	⬆️
build/src/ansi-c/ansi_c_y.tab.cpp	`78.37% <0.00%> (+0.22%)`	⬆️
src/goto-programs/rewrite_union.cpp	`100.00% <0.00%> (+5.88%)`	⬆️
... 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 27b02b3...4a10dd4. Read the comment docs.

regression/contracts/aaa-assigns_enforce_guarded_assigns_targets/main.c

src/goto-instrument/contracts/assigns.cpp

tautschnig

I believe the changes to the C front-end require some more work as detailed in my comments.

tautschnig · 2022-01-05T06:18:50Z

regression/contracts/assigns_enforce_conditional_function_call_condition/main.c

+  return true;
+}
+
+int foo(int a, int *x, int *y) __CPROVER_assigns(a && cond() ? *x)


I am not entirely convinced this is the best syntax to use: it seems that ? now has a very difference precedence?

Frama-C has gone that way, with different precedence rules depending on the context of an expression. I would much like to avoid anything the like.

Do you have a suggestion for the operator syntax ?

cond ==> {target, .. } was considered at some point but there would be similar issues in case the condition contains an operator like <==>.

The more verbose if(cond) target or if(cond) {target, .., target } ?

Maybe a completely new digraph or trigraph operator like?? or ?=> ?

What about : (colon)?

Yes that could work !

How about this:

assigns_clause: '__CPROVER_assigns' '(' [ cond_targets (';' cond_targets)* [ ';' ] ] ')' cond_targets: [ logical_equiv_expr ':' ] unary_expr (',' unary_expr)*

This is retro compatible with ,-separated lists of unconditional targets

__CPROVER_assigns(t1, t2, ... )

And we can have ;-separated lists of lists of conditional targets:

__CPROVER_assigns(t1, t2; cond: t3, t4; other_cond: t5, t6, t7)

with an optional ';' at the end you can indent like this:

__CPROVER_assigns( t1, t2; cond: t3, t4; other_cond: t5, t6, t7; )

I'm happy with that if you can come up with a grammar that doesn't require more lookahead!

src/ansi-c/c_typecheck_base.h

src/ansi-c/c_typecheck_code.cpp

src/ansi-c/parser.y

feliperodri · 2022-01-05T18:34:39Z

@remi-delmas-3000 (nitpic) is there any particular reason to add "Function contracts: " as a suffix for every commit (and title) of this PR? I think this pollutes the message more than inform anything. I'd suggest removing it and keep the remaining text.

remi-delmas-3000 · 2022-01-05T22:50:01Z

@remi-delmas-3000 (nitpic) is there any particular reason to add "Function contracts: " as a suffix for every commit (and title) of this PR? I think this pollutes the message more than inform anything. I'd suggest removing it and keep the remaining text.

@feliperodri, it was a request from @tautschnig to make it clear in the log history that a given commit is scoped to function contracts, and make it easier to filter the git history when there are regressions in CBMC-core.

tautschnig

Looks much better! I'm holding off on approving until we've concluded the syntax discussion.

src/ansi-c/c_expr.h

tautschnig · 2022-01-06T10:26:59Z

src/ansi-c/c_typecheck_code.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]

 #include "c_typecheck_base.h"

+#include <ansi-c/c_expr.h>


Move this further down, underneath #include "ansi_c_declaration.h", and use #include "c_expr.h" for consistency.

tautschnig · 2022-01-06T10:30:33Z

src/ansi-c/c_typecheck_code.cpp

+  if(condition.type().id() == ID_empty)
+  {
+    must_throw = true;
+    error().source_location = condition.source_location();
+    error() << "void-typed expressions not allowed as assigns clause conditions"
+            << eom;
+  }


Isn't this caught by implicit_typecast_bool already?

Since neiter implicit_typecast_bool or implicit_typecast have documentation I wasn't sure what to expect.

Fair enough! I was actually hoping for your test cases to confirm whether it is/isn't caught...

src/ansi-c/c_typecheck_code.cpp

src/ansi-c/parser.y

src/goto-instrument/contracts/assigns.cpp

tautschnig

Several comments need addressing, but I'm generally ok with this.

tautschnig · 2022-01-07T09:21:05Z

regression/contracts/assigns_enforce_conditional_unions/test.desc

+^\[update.\d+\] line 90 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
+^\[update.\d+\] line 96 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$
+^\[update.\d+\] line 97 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$
+^\[update.\d+\] line 100 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$


This one is failing in regression tests right now.

The tool is right and the test case is badly specified, fixing it in a new update.

tautschnig · 2022-01-07T09:22:25Z

src/ansi-c/c_expr.h

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


const exprt &expr to fix the Doxygen error

tautschnig · 2022-01-07T09:22:49Z

src/ansi-c/c_typecheck_base.h

+  /// targets of the form `c ? {t1, .. , tn}`, which get expanded to a
+  /// collection `{c ? t1, .. , c ? tn }` by distributing the condition `c`


Syntax needs updating

tautschnig · 2022-01-07T09:23:46Z

src/ansi-c/c_expr.h

+  explicit conditional_target_exprt(exprt _condition, exprt _target_list)
+    : exprt(ID_conditional_target, empty_typet{})
+  {
+    add_to_operands(std::move(_condition));
+    add_to_operands(std::move(_target_list));


Why did you choose to no longer make it a binary_exprt?

I was't really sure what a binary_exprt is supposed to represent, but from reading the code it seemed to be meant for binary operators such as <, +, where both left and right subtrees are homogenous.
This one being asymmetric and only meant to occur at a specify place in the AST seemed like a special case, it did not seem like reusing the binary_exprt interface would bring much.

Ok! (Adding/subtracting pointers is an existing example of binary_exprt with non-matching types.)

tautschnig · 2022-01-07T09:29:26Z

src/ansi-c/c_typecheck_code.cpp

+        exprt ops{ID_expression_list};
+        ops.add_to_operands(actual_target);
+        conditional_target_exprt result{condition, ops};
+        result.add_source_location() = conditional_target.source_location();
+        tmp.push_back(std::move(result));


This appears to be the only place that constructs a conditional_target_exprt. I would, therefore, expect that conditional_target_exprt has a constructor that permit creating the desired expression with just a single statement, like this:

tmp.push_back(conditional_target_exprt{condition, exprt{ID_expression_list, typet{}, {actual_target}}, conditional_target.source_location()});

tautschnig · 2022-01-07T09:31:31Z

src/goto-instrument/contracts/assigns.cpp

@@ -18,8 +18,10 @@ Date: July 2021

 #include <langapi/language_util.h>

+#include <ansi-c/c_expr.h>


I'd appreciate a blank line after this one.

tautschnig · 2022-01-07T09:32:47Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

@@ -15,6 +15,7 @@ Author: Remi Delmas, [email protected]

 #include <langapi/language_util.h>

+#include <ansi-c/c_expr.h>


Blank line after this one, please.

tautschnig · 2022-01-07T09:33:01Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

+#include <iostream>
+


Debugging left-over?

tautschnig · 2022-01-07T09:33:10Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

+
+  std::cout << target.pretty() << std::endl;


Debugging left-over?

tautschnig · 2022-01-07T09:37:18Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

+      const auto &cond_target = to_conditional_target_expr(target);
+
+      // clean the condition if needed
+      null_message_handlert null_handler;


Here and in the other place that introduces a null_message_handlert: should you perhaps use log.get_message_handler() from code_contractst?

feliperodri · 2022-01-07T15:55:09Z

@feliperodri, it was a request from @tautschnig to make it clear in the log history that a given commit is scoped to function contracts, and make it easier to filter the git history when there are regressions in CBMC-core.

@remi-delmas-3000 We should have "labels" to make it easier to filter contributions in the git history, similarly as we see in the linux project. For example, take a look at this commit message:

tracing: Tag trace_percpu_buffer as a percpu pointer

Tag trace_percpu_buffer as a percpu pointer to resolve warnings
reported by sparse:
...

We can adopt the tag CONTRACT to all work related to function and loop contracts (I don't think there is a need to distinct between them) and adopt these guidelines for commit messages. Linux also offers some guidelines about describing changes, but the one from cbea it's clear IMHO. Following these guidelines, your current commit message could be

CONTRACTS: Preliminary support for conditional assigns clauses

Conditional targets specify memory locations that can be assigned if and
only if a condition holds when a function is invoked. It does not yet
work for loops.

- Add a new `conditional_target_exprt` class and associated `irep_ID`;
- Modify ansi-c parser and typechecker to accept the new target syntax
  `cond: t1, ..., tn`;
- Update the CAR class `conditional_address_ranget` with explicit
  condition;
- Change the validity condition of a CAR to `condition &&
  all_deref_valid(target) && rw_ok(target, size)`, for both contract
checking and contract replacement logic;
- Update some tests, add new tests for the feature.

I can add a README file to our src/goto-instrument/contracts module with a reference for these guidelines and start a "contributors guide". (cc. @tautschnig)

feliperodri

Only minor comments. Thanks for implementing this new feature and the improved doc/descriptions!

feliperodri · 2022-01-07T15:56:01Z

regression/contracts/assigns_enforce_conditional_function_call_condition/main.c

+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>


We only need #include <stdbool.h>.

feliperodri · 2022-01-07T15:57:01Z

regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc

+The next step must be to check that the called functions have a contract
+with an empty assigns clause and that they indeed satisfy their contract
+using a CI check.


Is there a issue to track this?

feliperodri · 2022-01-07T15:57:24Z

regression/contracts/assigns_enforce_conditional_lvalue/main.c

+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>


We only need #include <stdbool.h> here.

feliperodri · 2022-01-07T15:57:45Z

regression/contracts/assigns_enforce_conditional_lvalue/test.desc

+^SIGNAL=0$
+--
+--
+Check that conditional assigns clause  `c ? lvalue`


We don't use this pattern anymore.

feliperodri · 2022-01-07T15:58:08Z

regression/contracts/assigns_enforce_conditional_lvalue_list/main.c

@@ -2,12 +2,21 @@
 #include <stdbool.h>
 #include <stdlib.h>


We don't need stdlib.h here.

feliperodri · 2022-01-07T16:11:58Z

src/ansi-c/c_typecheck_code.cpp

 void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
 {
+  exprt::operandst tmp;
+  bool must_throw = false;


Same as above.

Why don't you throw 0 on each if branch instead? You're now evaluating every if condition even if there is a previous error. Is that intentional?

very much intentional, in order to report all errors triggered by the expression instead of reporting them one by one.

feliperodri · 2022-01-07T16:12:55Z

src/ansi-c/c_typecheck_code.cpp

 void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
 {
+  exprt::operandst tmp;


Are those temporary targets? I'd give a more descriptive name for this temporary variable.

feliperodri · 2022-01-07T16:13:35Z

src/ansi-c/c_typecheck_code.cpp

+  // at least one target was not as expected
+  if(must_throw)
+    throw 0;


So why not throw 0 as soon as we find this target?

in order to report all errors found in the target list instead of stopping on the first one.

feliperodri · 2022-01-07T16:15:36Z

src/goto-instrument/contracts/assigns.cpp

+    const auto &conditional_target = to_conditional_target_expr(expr);
+    INVARIANT(
+      conditional_target.targets().size() == 1,
+      "expecting only a single target at this stage");


What stage? Could we be more descriptive?

feliperodri · 2022-01-07T16:17:19Z

src/goto-instrument/contracts/assigns.h

@@ -22,6 +22,27 @@ Date: July 2021

 typedef std::pair<const exprt, const exprt> slicet;

+/// A guarded slice of memory


\brief? Why struct and not a class here?

there are no methods associated with this. Why would it need to be a class ?

…ses. Conditional targets specify memory locations that can be assigned if and only if a condition holds when a function is invoked. *does not yet work for loops*. - Add a new `conditional_target_group_exprt` class and associated irep_id `ID_conditional_target_group` - Update `expr2ct` to print the new expression - Modify `ansi-c/parser.y` to accept the new target syntax - Modify `ansi-c/c_typecheck_code.cpp` for the new expression type - Update `conditional_address_ranget` with explicit condition - Change the validity condition of a CAR to `condition && all_deref_valid(target) && rw_ok(target, size)` for both contract checking and contract replacement logic. - Add new tests for the feature - Update existing tests

remi-delmas-3000 requested review from chrisr-diffblue, feliperodri, martin-cs, peterschrammel, SaswatPadhi and tautschnig as code owners December 23, 2021 03:32

remi-delmas-3000 force-pushed the guarded-assigns-targets branch from 28ae8ce to d80695b Compare December 23, 2021 06:45

tautschnig approved these changes Dec 31, 2021

View reviewed changes

tautschnig assigned remi-delmas-3000 Dec 31, 2021

remi-delmas-3000 force-pushed the guarded-assigns-targets branch from d80695b to 6916359 Compare January 3, 2022 16:15

feliperodri added aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts new feature labels Jan 4, 2022

remi-delmas-3000 requested a review from kroening as a code owner January 4, 2022 23:25

remi-delmas-3000 force-pushed the guarded-assigns-targets branch from e3d694d to cd1ca88 Compare January 4, 2022 23:33

remi-delmas-3000 changed the title ~~Function contracts: preliminary support for guarded assigns clause targets~~ Function contracts: preliminary support for conditional targets in assigns clause checking Jan 4, 2022

remi-delmas-3000 force-pushed the guarded-assigns-targets branch from cd1ca88 to 865b827 Compare January 4, 2022 23:59

tautschnig requested changes Jan 5, 2022

View reviewed changes

remi-delmas-3000 force-pushed the guarded-assigns-targets branch from 865b827 to 3671e58 Compare January 5, 2022 18:31

remi-delmas-3000 force-pushed the guarded-assigns-targets branch from 3671e58 to b01be89 Compare January 5, 2022 23:06

tautschnig reviewed Jan 6, 2022

View reviewed changes

remi-delmas-3000 force-pushed the guarded-assigns-targets branch from b01be89 to a65f3c1 Compare January 7, 2022 00:45

tautschnig approved these changes Jan 7, 2022

View reviewed changes

remi-delmas-3000 force-pushed the guarded-assigns-targets branch 2 times, most recently from d25f258 to 828fc8f Compare January 7, 2022 15:40

feliperodri approved these changes Jan 7, 2022

View reviewed changes

remi-delmas-3000 force-pushed the guarded-assigns-targets branch from 828fc8f to 79b5289 Compare January 7, 2022 21:54

remi-delmas-3000 force-pushed the guarded-assigns-targets branch from 79b5289 to 4a10dd4 Compare January 10, 2022 17:34

remi-delmas-3000 merged commit 169dc18 into diffblue:develop Jan 10, 2022

remi-delmas-3000 deleted the guarded-assigns-targets branch January 10, 2022 20:30

		@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]

		#include "c_typecheck_base.h"

		#include <ansi-c/c_expr.h>

		/// targets of the form `c ? {t1, .. , tn}`, which get expanded to a
		/// collection `{c ? t1, .. , c ? tn }` by distributing the condition `c`

		@@ -18,8 +18,10 @@ Date: July 2021

		#include <langapi/language_util.h>

		#include <ansi-c/c_expr.h>

		@@ -15,6 +15,7 @@ Author: Remi Delmas, [email protected]

		#include <langapi/language_util.h>

		#include <ansi-c/c_expr.h>

		@@ -22,6 +22,27 @@ Date: July 2021

		typedef std::pair<const exprt, const exprt> slicet;

		/// A guarded slice of memory

Function contracts: preliminary support for conditional targets in assigns clause checking #6546

Function contracts: preliminary support for conditional targets in assigns clause checking #6546

Uh oh!

Conversation

remi-delmas-3000 commented Dec 23, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Syntax

Use cases

Changes

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig 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!

remi-delmas-3000 Jan 5, 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!

remi-delmas-3000 Jan 6, 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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri commented Jan 5, 2022

Uh oh!

remi-delmas-3000 commented Jan 5, 2022

Uh oh!

tautschnig left a comment

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!

remi-delmas-3000 Jan 7, 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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 commented Dec 23, 2021 •

edited

Loading

codecov bot commented Dec 23, 2021 •

edited

Loading

remi-delmas-3000 Jan 5, 2022 •

edited

Loading

remi-delmas-3000 Jan 6, 2022 •

edited

Loading

remi-delmas-3000 Jan 7, 2022 •

edited

Loading

remi-delmas-3000 Jan 7, 2022 •

edited

Loading