Prevent multiple instrumentation of a same check and instrumentation of instrumentation assertions by remi-delmas-3000 · Pull Request #6471 · diffblue/cbmc

remi-delmas-3000 · 2021-11-23T16:50:01Z

This PR addresses the following issues:

Running goto-instrument multiple times with a same named-check switch creates redundant assertions:

goto-cc test.c -o test.o
goto-instrument --pointer-check test.o test1.o
goto-instrument --pointer-check test1.o test2.o
goto-instrument --pointer-check test2.o test3.o
// 3x pointer-check assertions generated  in test3.o

Applying --pointer-overflow-check followed by --unsigned-overflow-check in different goto-instrument invocations results in the pointer-overflow-check assertions to be instrumented for unsigned-overflow-check, and causes systematic errors.

// overflow.c
#include <stdlib.h>
const int N = 100;
int main()
{
  int *buf = malloc(N * sizeof(*buf));
  char *lb = (((char *)buf) - __CPROVER_POINTER_OFFSET(buf));
  char *ub = (((char *)buf) - __CPROVER_POINTER_OFFSET(buf)) + __CPROVER_OBJECT_SIZE(buf) - 1;
}

Running these passes

goto-cc overflow.c o overflow.goto
goto-instrument --pointer-overflow-check overflow.goto check1.goto
goto-instrument --unsigned-overflow-check check1.goto check2.goto
cbmc check2.goto

results in this systematic error

[main.overflow.2] line 12 arithmetic overflow on unsigned + in (unsigned long int)(signed long int)OBJECT_SIZE(buf) + 18446744073709551615ul: FAILURE

The PR adds the following in goto_check:

for 1): when an instruction is processed for a given named-check, either because the command line switch was used or because an "enable" pragma was added by the user in the source program, we add a pragma "checked:named-check" to the instruction. These pragmas get saved to goto binary files and persist across tool invocations. We check for the presence of "checked:named-check" pragmas to ensure check assertions are only generated once.
for 2): we add "disable:named-check" pragmas for all named checks to all assertions generated by goto_checkt::add_guarded_assertion. This will prevent these check assertions to be instrumented by other checks in future invocations of goto-instrument or cbmc.

The "checked" pragmas are reserved for internal use and are not exposed to the user in the front-end.

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/
[x ] 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).
[x ] 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-11-23T18:03:15Z

Codecov Report

Merging #6471 (7897cac) into develop (e286cd2) will increase coverage by 0.19%.
The diff coverage is 98.24%.

❗ Current head 7897cac differs from pull request most recent head 0aaf191. Consider uploading reports for the commit 0aaf191 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6471      +/-   ##
===========================================
+ Coverage    76.07%   76.27%   +0.19%     
===========================================
  Files         1548     1546       -2     
  Lines       166359   165627     -732     
===========================================
- Hits        126563   126329     -234     
+ Misses       39796    39298     -498

Impacted Files	Coverage Δ
src/analyses/goto_check.cpp	`90.16% <98.24%> (+23.49%)`	⬆️
...rc/goto-instrument/goto_instrument_parse_options.h	`100.00% <0.00%> (ø)`
src/analyses/goto_check_java.cpp
src/analyses/goto_check_c.cpp

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 7b40362...0aaf191. Read the comment docs.

tautschnig

Apart from comments as below: can this change please be turned into multiple commits as follows:

Introduce a message handler to goto_check. [no change in behaviour expected, no tests required]
Changes to the ansi_c_parsert API. [no change in behaviour expected, no tests required]
Adding support for pragma CPROVER enable [new feature, includes documentation updates and tests]
Changes to flag (re)setting [no change in behaviour expected, no tests required, could perhaps be done before the above commit.]
Support for "checked:..." [tests expected as this avoids redundant instrumentation]
Adding "disable:..." [tests expected]

tautschnig · 2021-11-24T14:41:58Z

regression/cbmc/pragma_cprover_enable_all/test.desc

@@ -0,0 +1,27 @@
+CORE broken-smt-backend


Just curious: any idea why this is failing with the SMT back-end?

I honestly have no idea. Seems related to some constructs being rejected by the SMT parser

tautschnig · 2021-11-24T14:42:10Z

regression/cbmc/pragma_cprover_enable_all/test.desc

+^\[main\.overflow\.\d+\] line 49 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
+^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed \+ in j \+ 1: FAILURE
+--
+This test uses all possible named-checks to maximize coverage.


Nit pick: newline at end of file.

tautschnig · 2021-11-24T14:45:55Z

src/analyses/goto_check.cpp

+  /// if the flag was already seen before.
+  void disable(bool &flag)
+  {
+    if(flag != false)


if(!flag) would seem more idiomatic.

tautschnig · 2021-11-24T14:52:18Z

src/analyses/goto_check.cpp

+        resetter.set_flag(enable_pointer_primitive_check, false, d.first);
+      else if(d.first == "enable:bounds-check")
+        resetter.set_flag(enable_bounds_check, true, d.first);
+      else if(d.first == "enable:pointer-check")
+        resetter.set_flag(enable_pointer_check, true, d.first);
+      else if(d.first == "enable:memory_leak-check")
+        resetter.set_flag(enable_memory_leak_check, true, d.first);


Randomly placing my comment in this block of code: I think we should now look at refactoring this piece of code, perhaps as follows:

string-split id2string(d.first) on :

parse the first component into an enum { DISABLE, ENABLED, CHECKED }

lookup the second component in a map that is initialised in the constructor (the map will map strings or irep_idtto bool* or bool&)

perform a set_flag operation on the result of that lookup, directed by the enum value.

As is, this will become a maintenance nightmare.

Yes, agreed.

martin-cs

I agree with @tautschnig that this would be better / easier to review as several commits.

Also, not wanting to be "that guy" but can we briefly discuss the motivation for this PR? You give two interesting and relevant use cases. In the first one, if you run the instrumentation multiple times, you get multiple copies of the assertion -- I am kind of OK with this? Is avoiding this a major problem for your workflow(s)? In the second case, should goto-check be looking at code in assertions by default, or really at all? CPROVER assertions are "execution neutral" in that they are just checks, they can't affect the values of variables or alter execution[1], so why are the checks for undefined behaviour looking in them? At least shouldn't the checks on expressions within assertions do things like convert e to !undefined_cases_of_e => e?

[1] But what about...

int g = 0;
int f00() { __CPROVER_assert(f00() != 0) ; return ++g; }

tautschnig · 2021-12-02T14:07:08Z

src/analyses/goto_check.cpp


+  /// Maps a named-check name to the corresponding boolean flag.
+  std::map<irep_idt, bool *> name_to_flag{
+    {"no-enum-check", &no_enum_check},


Can you please insert a commit at the beginning of your commit series that entirely removes no_enum_check from goto_check.cpp? It is always false. Seems like an unnecessary piece of code introduced in 85b90f3, probably had a meaning at some point while developing that change back then.

This flag is an override to the user-controlled enable_enum_check that is set to true before checking LHS in assignments:

// Reset the no_enum_check with the flag reset for exception // safety { flag_resett resetter(i); resetter.set_flag(no_enum_check, true, "no_enum_check"); check(assign_lhs); }

If we remove this flag CBMC will start checking LHS expressions, I think the problem could be that these assertions will trigger when the LHS is uninitialised and can take any integer value.

tautschnig · 2021-12-02T14:08:17Z

src/analyses/goto_check.cpp

+  } check_statust;
+
+  /// optional (named-check, status) pair
+  typedef optionalt<std::pair<irep_idt, check_statust>> named_check_statust;


CODING_STANDARD.md says that we nowadays prefer using over typedef.

should I also change all other typedef in this file into using ?

tautschnig · 2021-12-02T14:09:12Z

src/analyses/goto_check.cpp

+  ///
+  /// \returns a pair (name, status) if the match succeeds
+  /// and the name is known, nothing otherwise.
+  named_check_statust match_named_check(irep_idt named_check);


const irep_idt &named_check; also, should this method be const?

tautschnig · 2021-12-02T14:11:03Z

src/analyses/goto_check.cpp

+
+  /// \brief Adds "checked" pragmas for all currently active named checks
+  /// on the given source location.
+  void add_active_named_check_pragmas(source_locationt &source_location);


Should be marked const

tautschnig · 2021-12-02T14:12:33Z

src/analyses/goto_check.cpp

+
+  /// \brief Adds "disable" pragmas for all named checks
+  /// on the given source location.
+  void add_all_disable_named_check_pragmas(source_locationt &source_location);


tautschnig · 2021-12-02T14:15:44Z

src/analyses/goto_check.cpp

+    // inhibit already checked checks
+    for(auto flag : already_checked)
+      resetter.disable(*flag);


Do you really need this already_checked list? Can't you invoke resetter.disable(...) directly earlier on?

The check pragmas have priority over enable so they must be applied last.

I have moved the priority logic inside flag_resett

tautschnig · 2021-12-02T14:17:09Z

src/analyses/goto_check.cpp

+void goto_checkt::add_active_named_check_pragmas(
+  source_locationt &source_location)
+{
+  for(auto it : name_to_flag)


I'd avoid "it" as a name for this isn't an iterator. Also, I'm never quite sure what the exact type here is, so I tend to use const auto &entry : name_to_flag to make sure it's a const reference and not a copy.

tautschnig · 2021-12-02T14:17:25Z

src/analyses/goto_check.cpp

+void goto_checkt::add_all_disable_named_check_pragmas(
+  source_locationt &source_location)
+{
+  for(auto it : name_to_flag)


As above: const reference.

tautschnig · 2021-12-02T14:18:41Z

src/analyses/goto_check.cpp

+  if(s.find("enable:") == 0)
+  {
+    status = check_statust::ENABLE;
+  }
+  else if(s.find("disable:") == 0)
+  {
+    status = check_statust::DISABLE;
+  }
+  else if(s.find("checked:") == 0)


Use has_prefix(s, "...") instead of s.find(...) == 0.

tautschnig · 2021-12-02T14:21:31Z

src/analyses/goto_check.cpp

+    return {};
+  }
+
+  auto sep = s.find(":");


Each of the above branches would actually have a constant known value for this. Perhaps avoid the duplicate find? Alternatively, do the find early on and then just compare the substrings up to that known position of the colon.

remi-delmas-3000 · 2021-12-02T16:08:54Z

Also, not wanting to be "that guy" but can we briefly discuss the motivation for this PR? You give two interesting and relevant use cases. In the first one, if you run the instrumentation multiple times, you get multiple copies of the assertion --

Hi @martin-cs , the motivation for this PR is that the function contract and loop contract workflows involve several distinct goto-instrument passes that introduce new instrumentation variables, assertions and assumptions in a goto program which then get analysed using CBMC once all transformations are applied.

This ultimate analysis pass uses any automatic checks the user decides to activate (pointer-checks, overflow-checks, enum-checks, etc.).

Some of this contract instrumentation is execution neutral and some of it requires extra checks:

we add instrumentation that performs pointer validity checks (to guard snapshots of history variables, to guard write set inclusion checks, etc.) and are expected to manipulate invalid pointers, and we need to disable the built-in CBMC pointer checks
we add instrumentation that performs pointer arithmetic for write set inclusion checking, which needs to get checked for overflow, regardless of what checks the user decides to use for the last analysis step.

I am kind of OK with this? Is avoiding this a major problem for your workflow(s)?

Our contract instrumentation happens early on and in later passes, with the current goto-instrument and cbmc behaviour, it gets picked up and instrumented if it were user code. This results in an explosion of the number of VCCs (x10, from 8k to 80k on our larger benchmarks) when all checks are activated in the last stage. Most of them being useless and hurting performance badly, some of them causing systematic errors. Most importantly we cannot guarantee that any of the checks we need for the soundness of our instrumentation will eventually be performed (eventhough our template Makefile for contracts proofs has all checks activated, the user can always decide to not activate pointer overflow checks and we have no control over this).

So this PR, combined with this other PR #6450 which introduces "enable" pragmas, gives us the level of control we need to ensure required checks will be instrumented exactly once, and that unnecessary checks or redundant checks will not be instrumented, while letting the user freely decide on what checks to instantiate on his own code.

One thing to be noticed is that these "checked" pragmas are not exposed to the user so the possibilities for abuse are limited.

In the second case, should goto-check be looking at code in assertions by default, or really at all? CPROVER assertions are "execution neutral" in that they are just checks, they can't affect the values of variables or alter execution[1], so why are the checks for undefined behaviour looking in them?

This is precisely what this PR is trying to fix. My take is that checks should be instantiated on user-provided assertions that are part of the original program, but not necessarily on all instrumentation code and assertions (though in some cases checks might be required to ensure soundness, as is the case with write set inclusion checking).

A question to you : is there any fundamental difference of intent in uses of assert vs uses of __CPROVER_assert ?

I was under the impression that assert would persist in the user program and be executed at runtime, and that __CPROVER_assert were a kind of "proof only" assertions that were not meant to persist in the program at runtime. But I don't know for sure.

At least shouldn't the checks on expressions within assertions do things like convert e to !undefined_cases_of_e => e?

Assuming we're talking about goto_check generated assertions, this would not solve the problem that the whole ASSERT !undefined_cases_of_e => e would be instrumented again at the next invocation of goto-check or cbmc if CLI flags are set.

[1] But what about...

int g = 0;
int f00() { __CPROVER_assert(f00() != 0) ; return ++g; }

Can goto_check generate this kind of assertions ? I hope not.
On the other hand, if this were a user-provided assertion, I would expect it to get instrumented with any check the user decides to activate on the CLI.

…rumentation. When several invocations to goto-instrument/cmbc are performed with named-check flags, the same assertions were generated several times, and assertions generated by a check A in some pass would be instrumented by a check B in some ulterior pass. "checked" pragmas allow to keep track of which checks have been performed on which instructions and are saved in the goto binaries, hence surviving across invocations of the tools. The presente of a "checked" pragma for a given check on an instruction prevents future invocations of the tools to generate again the assertions of that check. We also tag all assertions generated by goto_check with "disable" pragmas to avoid instrumenting instrumentation assertions in ulterior invocations of the tool.

martin-cs · 2021-12-02T20:28:01Z

@remi-delmas-3000 thank you for the detailed and thoughtful exploration of the context. I feel like I understand your workflow a bit better now. I can see that it is a problem and none of the work-flows changes I proposed will easily fix it. I am not 100% convinced there isn't an over-all better way but I think that would be a bit "global optimum" and I can see this is an improvement, even if to a local optimum.

A question to you : is there any fundamental difference of intent in uses of assert vs uses of __CPROVER_assert ?

I think they should do different things. I think assert should terminate the program if it fails (or assume(0)) while __CPROVER_assert is a pure check that should directly map to an ASSERT instruction.

tautschnig · 2021-12-03T09:34:25Z

A question to you : is there any fundamental difference of intent in uses of assert vs uses of __CPROVER_assert ?

I think they should do different things. I think assert should terminate the program if it fails (or assume(0)) while __CPROVER_assert is a pure check that should directly map to an ASSERT instruction.

I suppose I should try to find some time for #5866 to enshrine this.

kroening · 2021-12-03T10:56:13Z

A question to you : is there any fundamental difference of intent in uses of assert vs uses of __CPROVER_assert ?

I think they should do different things. I think assert should terminate the program if it fails (or assume(0)) while __CPROVER_assert is a pure check that should directly map to an ASSERT instruction.

I suppose I should try to find some time for #5866 to enshrine this.

I would be very careful with this. Note that assert(0) does not abort when NDEBUG is set, which is often the case in production binaries. The failing assertion may then hide a genuine security vulnerability.

remi-delmas-3000 added dependent - do not merge aws Bugs or features of importance to AWS CBMC users aws-high labels Nov 23, 2021

remi-delmas-3000 requested a review from tautschnig November 23, 2021 16:50

remi-delmas-3000 requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel and romainbrenguier as code owners November 23, 2021 16:50

remi-delmas-3000 self-assigned this Nov 23, 2021

remi-delmas-3000 force-pushed the pragma-checked branch from b3ad1d3 to 1655871 Compare November 23, 2021 17:46

remi-delmas-3000 force-pushed the pragma-checked branch 2 times, most recently from 404748e to 1c232cb Compare November 23, 2021 18:24

tautschnig reviewed Nov 24, 2021

View reviewed changes

martin-cs reviewed Nov 25, 2021

View reviewed changes

remi-delmas-3000 force-pushed the pragma-checked branch from 1c232cb to 70aada0 Compare December 1, 2021 22:40

tautschnig approved these changes Dec 2, 2021

View reviewed changes

tautschnig removed the dependent - do not merge label Dec 2, 2021

tautschnig assigned peterschrammel, martin-cs and chrisr-diffblue Dec 2, 2021

peterschrammel approved these changes Dec 2, 2021

View reviewed changes

kroening mentioned this pull request Dec 2, 2021

Split goto_check #6497

Merged

4 tasks

remi-delmas-3000 force-pushed the pragma-checked branch 2 times, most recently from f37fc08 to 057a147 Compare December 2, 2021 19:14

Remi Delmas added 2 commits December 2, 2021 19:36

Adding a test that demonstrates the non-duplication.

0aaf191

tautschnig force-pushed the pragma-checked branch from 057a147 to 0aaf191 Compare December 2, 2021 19:36

remi-delmas-3000 force-pushed the pragma-checked branch from 0aaf191 to 4125dbe Compare December 2, 2021 19:56

tautschnig force-pushed the pragma-checked branch from 4125dbe to 0aaf191 Compare December 2, 2021 20:08

martin-cs approved these changes Dec 2, 2021

View reviewed changes

tautschnig merged commit 8ab933b into diffblue:develop Dec 3, 2021

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

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!

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!

martin-cs 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!

Choose a reason for hiding this comment

Uh oh!

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

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 Dec 2, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

martin-cs commented Dec 2, 2021

Uh oh!

tautschnig commented Dec 3, 2021

Uh oh!

kroening commented Dec 3, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

remi-delmas-3000 commented Nov 23, 2021 •

edited

Loading

codecov bot commented Nov 23, 2021 •

edited

Loading

remi-delmas-3000 Dec 2, 2021 •

edited

Loading

remi-delmas-3000 commented Dec 2, 2021 •

edited

Loading