Adding `#pragma CPROVER enable "named-check"` #6450

remi-delmas-3000 · 2021-11-10T00:59:19Z

This PR adds the possibility to selectively activate checks :

on blocks of C code using #pragma CPROVER enable "named-check"
to individual GOTO instructions and expressions using source_location.add_pragma("enable:named-check")

It is possible to enable/disable a check, to push a level on the stack and override the check status using another pragma enable/disable pragma.
Attempts to enable and disable a same check at the same stack level are detected and cause a PARSING_ERROR in the C front end and a INVARIANT violation in goto_check.

Modifications:

the collection of allocations on the whole goto program using goto_checkt::collect_allocation is now always on
a messaget log attribute is added to goto_checkt to be able to log warnings in case a same check is enabled/disabled more than once on a given GOTO instruction
the flag_resett class is extended to detect multiple 'set_flag' operations on a same flag
the ansi-c lexer/parser is modified to accept #pragma CPROVER enable "named check" and flag shadowing
tests are added in regression/cbmc/pragma_cprover_enable* to test the feature

This feature is needed as part of the function and loop contracts verification, to be able to selectively activate checks on instructions used for assigns-clause checking, in order to guarantee the soundness of the analysis, even if these checks are not globally activated in the current or ulterior goto-instrument or cbmc passes

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

Nice :) Mostly minor comments below.

Can we add at least one regression test to check nesting of both disable and enable pragmas, something like:

  int n;

#pragma CPROVER check push
#pragma CPROVER check enable "signed-overflow"
   // generate overflow checks for the following addition
  int x = n + n;
#pragma CPROVER check push
#pragma CPROVER check disable "signed-overflow"
   // do not generate overflow checks for the following increment operations
  ++n;
  n++;
#pragma CPROVER check pop
   // generate overflow checks for the following addition
  int b = n + n;
#pragma CPROVER check pop

SaswatPadhi · 2021-11-10T05:00:41Z

src/analyses/goto_check.cpp

+
+  /// when true causes a forced collection of all allocations
+  /// (needed to allow selectively enabling checks per instruction)
+  bool do_collect_allocations;


It seems like we are setting this to true in the constructor and no other method sets it to false, so wouldn't this be always true? And if that's the case, can we completely remove this and also remove the if(!... & !...) return; check in collect_allocations?

Or did I miss a code path where it won't be true?

this variable was removed and collection is now always on

SaswatPadhi · 2021-11-10T05:04:34Z

src/analyses/goto_check.cpp

+    {
+      log.warning() << "Found more than one CPROVER enable/disable check "
+                       "pragma on a same goto instruction"
+                    << messaget::eom;


I think the error message could be improved a bit. Having "more than one CPROVER enable/disable check" is fine as long as they are different checks.
I think we want to say that we the same check being enabled/disabled multiple times times at a goto instruction.

message updated to include the name of the check

SaswatPadhi · 2021-11-10T05:05:24Z

regression/cbmc/pragma_cprover_enable3/test.desc

+^SIGNAL=0$
+--
+^\[main.pointer_primitives.\d+\] line 17 
+--


[nit] missing newline. Also in a few other files.

SaswatPadhi · 2021-11-10T05:07:47Z

regression/cbmc/pragma_cprover_enable1/main.c

+#pragma CPROVER check enable "signed-overflow"
+  // generate assertions for the following statement
+  x = x + y[1];
+  // pop all annotations


Suggested change

// pop all annotations

// pop all checks added since the last push

[nit] also in other test files

comment removed

feliperodri

Only minor comments (modulo Saswat's comments).

feliperodri · 2021-11-10T19:52:49Z

doc/cprover-manual/properties.md

 use `#pragma CPROVER check disable "<name_of_check>"`, which remains in effect
 until a `#pragma CPROVER check pop` (to re-enable all properties
-disabled before or since the last `#pragma CPROVER check push`) is provided.
+disabled or enabled before or since the last `#pragma CPROVER check push`) is provided. 


(to re-enable all properties disabled or enabled before or since the last `#pragma CPROVER check push`)

This wording seems confusing. Could you re-write it?

documentation updated

feliperodri · 2021-11-10T19:53:18Z

doc/cprover-manual/properties.md

+until a `#pragma CPROVER check pop` (to re-enable all properties
+disabled or enabled before or since the last `#pragma CPROVER check push`) is provided.


Same as above.

documentation updated

feliperodri · 2021-11-10T19:54:14Z

regression/cbmc/pragma_cprover_enable1/main.c

+#pragma CPROVER check enable "signed-overflow"
+  // generate assertions for the following statement
+  x = x + y[1];
+  // pop all annotations


feliperodri · 2021-11-10T19:54:29Z

regression/cbmc/pragma_cprover_enable1/test.desc

+^SIGNAL=0$
+--
+--
+Checks that we can selectively activate checks using pragmas.


Add newline.

feliperodri · 2021-11-10T19:57:08Z

src/analyses/goto_check.cpp

+
+  /// when true causes a forced collection of all allocations
+  /// (needed to allow selectively enabling checks per instruction)
+  bool do_collect_allocations;


codecov · 2021-11-12T02:45:26Z

Codecov Report

Merging #6450 (f245b3a) into develop (bfa4c2c) will increase coverage by 0.05%.
The diff coverage is 95.69%.

@@             Coverage Diff             @@
##           develop    #6450      +/-   ##
===========================================
+ Coverage    76.01%   76.06%   +0.05%     
===========================================
  Files         1527     1546      +19     
  Lines       164465   165584    +1119     
===========================================
+ Hits        125013   125951     +938     
- Misses       39452    39633     +181

Impacted Files	Coverage Δ
jbmc/src/janalyzer/janalyzer_parse_options.cpp	`48.25% <ø> (ø)`
jbmc/src/jbmc/jbmc_parse_options.cpp	`72.32% <ø> (ø)`
.../goto-instrument/goto_instrument_parse_options.cpp	`68.29% <ø> (ø)`
src/ansi-c/scanner.l	`61.94% <92.30%> (+0.18%)`	⬆️
src/ansi-c/ansi_c_parser.cpp	`88.78% <96.00%> (+2.19%)`	⬆️
src/analyses/goto_check.cpp	`90.03% <96.15%> (+1.25%)`	⬆️
jbmc/src/jdiff/jdiff_parse_options.cpp	`68.11% <100.00%> (ø)`
src/ansi-c/ansi_c_parser.h	`100.00% <100.00%> (ø)`
src/goto-programs/process_goto_program.cpp	`100.00% <100.00%> (ø)`
src/util/format_type.cpp	`49.23% <0.00%> (-15.39%)`	⬇️
... and 87 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 e27dba6...f245b3a. Read the comment docs.

chrisr-diffblue · 2021-11-12T14:48:38Z

Just a general git housekeeping comment - it's generally better to use git pull --rebase origin develop (replace origin with whatever you've called your remote - origin being the default if you didn't specify/change the remote name) to update your branch with the latest develop branch, rather than doing a merge of develop - it will lead to cleaner commits and cleaner git history.

tautschnig

Functionality looks ok, but I think this PR needs some cleanup to remove as much noise as possible.

src/goto-instrument/goto_instrument_parse_options.cpp

src/ansi-c/scanner.l

src/ansi-c/ansi_c_parser.h

jbmc/src/jdiff/jdiff_parse_options.cpp

src/analyses/goto_check.cpp

src/ansi-c/ansi_c_parser.cpp

SaswatPadhi

A few more comments; nothing major

src/ansi-c/ansi_c_parser.h

src/ansi-c/ansi_c_parser.cpp

SaswatPadhi · 2021-11-16T15:57:55Z

src/analyses/goto_check.cpp

      if(d.first == "disable:bounds-check")
-        flag_resetter.set_flag(enable_bounds_check, false);
+        flag_resetter.set_flag(enable_bounds_check, false, err_msg);


I am not sure if I understand why err_msg needs to be a lambda function. It seems like it's called immediately (at the INVARIANT check) within the set_flag call. Can we not just pass a string here instead?

this lambda is used to defer the creation of the error string until it is actually needed (if ever).

SaswatPadhi · 2021-11-16T15:58:19Z

src/analyses/goto_check.cpp

+          return "no_enum_check flag disabled and enabled at \n" +
+                 i.source_location().pretty();
+        };
+        no_enum_check_flag_resetter.set_flag(no_enum_check, true, err_msg);


Same comment as above.
Can we not just pass a string here instead?

now passing flag name and instructions to set_flag

src/analyses/goto_check.cpp

SaswatPadhi · 2021-11-16T16:01:34Z

src/analyses/goto_check.cpp

+  /// \brief True iff flag has already been seen by \ref set_flag
+  bool seen(bool &flag)
+  {
+    return seen_flags.find(&flag) != seen_flags.end();


Hmm, we seem to be taking the address of flag here. So if we have two flags with the same content but different addresses then this would break?

Do we have some mechanism to guard against it? Or if there's some other reason as to why this is a non-issue, we should mention that in the comments above this function.

the class flag_resett is file-local so as long as the discipline is respected in this file it should be ok.

tautschnig · 2021-11-17T15:25:17Z

src/analyses/goto_check.cpp

    if(flag != new_value)
    {
-      flags_to_reset.emplace_back(&flag, flag);
+      flags_to_reset.insert(std::pair<bool *, bool>(&flag, flag));


I might be wrong, but I believe you can shorten this to flags_to_reset.insert({&flag, flag}); with C++11.

Or just flags_to_reset.emplace(&flag, flag); to avoid creating a temporary pair.

src/analyses/goto_check.cpp

tautschnig · 2021-11-17T15:27:16Z

src/analyses/goto_check.cpp

  ~flag_resett()
  {
    for(const auto &flag_pair : flags_to_reset)
      *flag_pair.first = flag_pair.second;
  }

 private:
-  std::list<std::pair<bool *, bool>> flags_to_reset;
+  /// \brief True iff flag has already been seen by \ref set_flag
+  bool seen(bool *flag)


Not that it matters a whole lot, but the parameter type should be const bool * to make clear that no modification will occur. Also, the method should be marked const.

method removed

src/analyses/goto_check.cpp

src/ansi-c/ansi_c_parser.cpp

SaswatPadhi

Approving modulo Michael's remaining comments and one minor suggestion:

SaswatPadhi · 2021-11-19T15:30:25Z

src/ansi-c/ansi_c_parser.cpp

+    std::string check_name = id2string(pragma.first);
+    std::string full_name =
+      (pragma.second ? "enable:" : "disable:") + check_name;


Suggested change

std::string check_name = id2string(pragma.first);

std::string full_name =

(pragma.second ? "enable:" : "disable:") + check_name;

auto check_name = id2string(pragma.first);

auto full_name =

(pragma.second ? "enable:" : "disable:") + check_name;

scanner.l uses std::string everywhere so I'll keep this as is for consistency

Yes, but not sure why it has to be kept this way here though ... Using auto is not only more succinct but also makes it future proof (disconnects this from the underlying type, which is base std::string today)

this would only be patching two lines out of several dozen that could use auto the whole lexer would need refactoring to be effectively future proof.

Up to you 🙂

feliperodri · 2021-11-22T22:38:10Z

@peterschrammel @martin-cs could you take a look at this PR? It's missing code owner approval.

martin-cs · 2021-11-30T18:06:45Z

@feliperodri Apologies for the lag; I missed this one.

martin-cs · 2021-11-30T18:08:12Z

This would be easier to review if it were split up into multiple commits. Parsing, implementation, testing would seem a reasonable start.

Adding enable and disable pragmas for a same check at a same pragma stack level triggers an error. Enable and disable pragmas for a same check in different stack levels is allowed, and shadowing is managed when flattening the stack.

No change in behaviour expected. No need for specific tests.

Needed so that the data required to express pointer checks is always available to process a enable pragmas.

…ble updates with opposite values.

remi-delmas-3000 · 2021-12-01T01:40:13Z

@martin-cs @feliperodri @tautschnig I reworked the commit history it should be good for the final review now

martin-cs · 2021-12-01T16:00:01Z

Thank you @remi-delmas-3000 it makes reviewing so much easier!

remi-delmas-3000 added aws Bugs or features of importance to AWS CBMC users aws-high labels Nov 10, 2021

remi-delmas-3000 requested review from tautschnig, SaswatPadhi, kroening and feliperodri November 10, 2021 00:59

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

remi-delmas-3000 requested review from chrisr-diffblue, martin-cs and peterschrammel as code owners November 10, 2021 00:59

SaswatPadhi reviewed Nov 10, 2021

View reviewed changes

feliperodri approved these changes Nov 10, 2021

View reviewed changes

remi-delmas-3000 requested a review from romainbrenguier as a code owner November 12, 2021 01:14

remi-delmas-3000 mentioned this pull request Nov 12, 2021

Disable redundant automatic checks on assigns clause checking instrumentation [depends-on: #6450] #6455

Closed

7 tasks

tautschnig requested changes Nov 15, 2021

View reviewed changes

remi-delmas-3000 force-pushed the pragma-cprover-enable branch from 843b48e to 9686089 Compare November 15, 2021 23:39

feliperodri requested review from tautschnig and SaswatPadhi November 16, 2021 15:15

remi-delmas-3000 force-pushed the pragma-cprover-enable branch from 4e8f4e2 to 702bbd9 Compare November 16, 2021 15:17

SaswatPadhi suggested changes Nov 16, 2021

View reviewed changes

remi-delmas-3000 force-pushed the pragma-cprover-enable branch from 702bbd9 to 1018f34 Compare November 16, 2021 19:48

remi-delmas-3000 mentioned this pull request Nov 16, 2021

Disable unnecessary pointer checks, enable necessary pointer checks i… #6459

Merged

7 tasks

remi-delmas-3000 force-pushed the pragma-cprover-enable branch 4 times, most recently from 565af96 to c8cd39e Compare November 17, 2021 15:06

tautschnig assigned SaswatPadhi Nov 17, 2021

tautschnig approved these changes Nov 17, 2021

View reviewed changes

SaswatPadhi approved these changes Nov 19, 2021

View reviewed changes

tautschnig assigned peterschrammel and martin-cs and unassigned SaswatPadhi and remi-delmas-3000 Nov 19, 2021

remi-delmas-3000 force-pushed the pragma-cprover-enable branch 3 times, most recently from 0f77949 to b48db7c Compare November 22, 2021 22:31

feliperodri changed the title ~~adding #pragma CPROVER enable "named-check"~~ Adding #pragma CPROVER enable "named-check" Nov 22, 2021

remi-delmas-3000 force-pushed the pragma-cprover-enable branch 2 times, most recently from d5c6659 to 0008223 Compare November 23, 2021 14:53

remi-delmas-3000 mentioned this pull request Nov 23, 2021

Prevent multiple instrumentation of a same check and instrumentation of instrumentation assertions #6471

Merged

5 tasks

remi-delmas-3000 force-pushed the pragma-cprover-enable branch from 0008223 to 21897d5 Compare November 23, 2021 16:53

Remi Delmas added 8 commits December 1, 2021 00:52

Adds a message_handlert to goto_check functions and goto_checkt.

4337f38

No change in behaviour expected. No need for specific tests.

collect_allocations is now always on.

dc6daa8

Needed so that the data required to express pointer checks is always available to process a enable pragmas.

Adding extra logic to flat_resett to detect and trigger errors on dou…

d59448d

…ble updates with opposite values.

Adds processing of enable pragmas with flag_resett

4c33a24

Regression tests for enable pragmas

a219cf7

Remove unused import

cebf6d5

Updated documentation for CPROVER check enable and disable pragmas.

68e8888

remi-delmas-3000 force-pushed the pragma-cprover-enable branch from 21897d5 to 68e8888 Compare December 1, 2021 01:35

Removing unused import

f245b3a

peterschrammel approved these changes Dec 1, 2021

View reviewed changes

tautschnig merged commit fe79da1 into diffblue:develop Dec 1, 2021

	// pop all annotations
	// pop all checks added since the last push

		until a `#pragma CPROVER check pop` (to re-enable all properties
		disabled or enabled before or since the last `#pragma CPROVER check push`) is provided.

Adding #pragma CPROVER enable "named-check" #6450

Adding #pragma CPROVER enable "named-check" #6450

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

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!

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

Uh oh!

Codecov Report

Uh oh!

chrisr-diffblue commented Nov 12, 2021

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

SaswatPadhi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Adding `#pragma CPROVER enable "named-check"` #6450

Adding `#pragma CPROVER enable "named-check"` #6450

remi-delmas-3000 commented Nov 10, 2021 •

edited

Loading

codecov bot commented Nov 12, 2021 •

edited

Loading

SaswatPadhi Nov 16, 2021 •

edited

Loading

remi-delmas-3000 Nov 16, 2021 •

edited

Loading

SaswatPadhi Nov 22, 2021 •

edited

Loading