CONTRACTS: Handle all 4 inlining warning types in `inlining_decoratort` #7083

remi-delmas-3000 · 2022-08-25T16:32:11Z

Modifications:

move the class from contracts.cpp to its own file
use regexes to track all 4 types of warnings
add getter methods to inspect functions involved in warnings
add methods to throw errors after warnings

No behaviour or performance impact.

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 · 2022-08-25T17:44:49Z

Codecov Report

Merging #7083 (664a7ac) into develop (f4d92f2) will decrease coverage by 0.00%.
The diff coverage is 55.29%.

@@             Coverage Diff             @@
##           develop    #7083      +/-   ##
===========================================
- Coverage    77.85%   77.85%   -0.01%     
===========================================
  Files         1574     1576       +2     
  Lines       181245   181301      +56     
===========================================
+ Hits        141109   141143      +34     
- Misses       40136    40158      +22

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/inlining_decorator.h	`34.78% <34.78%> (ø)`
...c/goto-instrument/contracts/inlining_decorator.cpp	`62.29% <62.29%> (ø)`
src/goto-instrument/contracts/contracts.cpp	`96.29% <100.00%> (+1.97%)`	⬆️
src/ansi-c/c_expr.h	`100.00% <0.00%> (ø)`

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

regression/contracts/function-calls-03-1/test-enf-f1.desc

feliperodri · 2022-08-29T16:34:10Z

src/goto-instrument/contracts/inlining_decorator.h

+  void print(unsigned level, const std::string &message) override
+  {
+    parse_message(message);
+    wrapped.print(level, message);
+  }
+


Is this only for debugging purposes? Why no coverage in none of the print methods?

This class is used to collect the names of functions that cause inlining warnings and turn them into hard errors.

The inlining_decoratort class is a decorator for the message_handlert class so it both extends message_handlert and wraps a preexistingmessage_handlert object.
The decorator has to implement all message_handlert methods.

This one intercepts messages sent by the inlining class to the message_handlert to extract the names of functions involved in inlining warnings and is essential to how this class works.

All other methods are implemented by redirecting calls to the wrapped object assuming that whatever it does is already the right thing.

feliperodri · 2022-08-29T16:35:07Z

src/goto-instrument/contracts/inlining_decorator.h

+    return wrapped.get_message_count(level);
+  }
+
+  std::string command(unsigned i) const override


Same as before. Why no coverage?

No coverage because the decorator design pattern requires to implement all methods of messaget_handlert, but this decorator only gets used with the GOTO inlining class which does itself not use the whole message_handlert interface. Since all these methods do is to call the same method on the wrapped object code review could be sufficient to validate this class.

feliperodri · 2022-08-29T16:36:08Z

src/goto-instrument/contracts/inlining_decorator.cpp

+    missing_function_set.insert(ss.str());
+  }


Shall we include at least one test to cover these branches?

These methods are used by the new contracts implementation so they will get covered in a later PR

feliperodri · 2022-08-29T16:39:00Z

src/goto-instrument/contracts/inlining_decorator.cpp

+{
+  std::smatch sm;
+  std::regex_match(message, sm, missing_function_regex);
+  if(sm.size() == 2)


Why 2? The size will return "number of capturing groups plus one", so I guess you need at least one(i.e., sm.size() > 1), right?

I think the "plus one" is the whole substring, no? Seems like there should be a better way to check this.

The first match is the whole regex match and the following matches are for the groups within the regex if any. Since my regexes have 1 group this results in two matches for a successful match.

src/goto-instrument/contracts/inlining_decorator.cpp

nwetzler · 2022-08-29T21:22:04Z

src/goto-instrument/contracts/inlining_decorator.cpp

+{
+  std::smatch sm;
+  std::regex_match(message, sm, missing_function_regex);
+  if(sm.size() == 2)


I think the "plus one" is the whole substring, no? Seems like there should be a better way to check this.

remi-delmas-3000 · 2022-08-30T14:45:23Z

Added more documentation and implemented requested changes

remi-delmas-3000 · 2022-08-30T18:47:48Z

The inlining_decoratort class has coverage holes but these methods will get covered in the dynamic frames PR

peterschrammel · 2022-09-01T08:55:48Z

src/goto-instrument/contracts/inlining_decorator.cpp

+  {
+    for(auto it : no_body_set)
+    {
+      log.error() << "inlining_decoratort: no body for '" << it


⛏️ Do you really want to have inlining_decoratort: as part of the output?

Modifications: - move the class from contracts.cpp to its own file - use regexes to track all 4 types of warnings - add getter methods to inspect functions involved in warnings - add methods to throw errors after warnings

remi-delmas-3000 requested review from tautschnig, feliperodri, SaswatPadhi, martin-cs, chris-ryder and peterschrammel as code owners August 25, 2022 16:32

remi-delmas-3000 mentioned this pull request Aug 25, 2022

CONTRACTS: Dynamic frame condition checking #6887

Closed

remi-delmas-3000 force-pushed the inlining-decoratort-improvements branch 2 times, most recently from 14a0433 to 3c0369b Compare August 26, 2022 04:28

feliperodri added aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts labels Aug 29, 2022

feliperodri requested changes Aug 29, 2022

View reviewed changes

feliperodri assigned remi-delmas-3000 Aug 29, 2022

nwetzler approved these changes Aug 29, 2022

View reviewed changes

remi-delmas-3000 force-pushed the inlining-decoratort-improvements branch from 3c0369b to 09bfc72 Compare August 30, 2022 14:41

feliperodri approved these changes Aug 30, 2022

View reviewed changes

feliperodri assigned peterschrammel, martin-cs, chris-ryder and SaswatPadhi and unassigned remi-delmas-3000 Aug 30, 2022

peterschrammel approved these changes Sep 1, 2022

View reviewed changes

remi-delmas-3000 force-pushed the inlining-decoratort-improvements branch from 09bfc72 to 441bee5 Compare September 1, 2022 14:38

remi-delmas-3000 changed the title ~~CONTRACTS: inlining_decoratort improvements~~ CONTRACTS: Handle all 4 inlining warning types in inlining_decoratort Sep 1, 2022

remi-delmas-3000 force-pushed the inlining-decoratort-improvements branch 2 times, most recently from bdd3f95 to 784554f Compare September 1, 2022 15:18

remi-delmas-3000 force-pushed the inlining-decoratort-improvements branch from 784554f to 664a7ac Compare September 1, 2022 15:44

feliperodri approved these changes Sep 1, 2022

View reviewed changes

feliperodri assigned remi-delmas-3000 and unassigned SaswatPadhi, peterschrammel, martin-cs and chris-ryder Sep 1, 2022

remi-delmas-3000 merged commit 312c433 into diffblue:develop Sep 1, 2022

remi-delmas-3000 deleted the inlining-decoratort-improvements branch September 1, 2022 19:18

CONTRACTS: Handle all 4 inlining warning types in inlining_decoratort #7083

CONTRACTS: Handle all 4 inlining warning types in inlining_decoratort #7083

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

Uh oh!

feliperodri Aug 29, 2022

Choose a reason for hiding this comment

Uh oh!

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

feliperodri Aug 29, 2022

Choose a reason for hiding this comment

Uh oh!

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

feliperodri Aug 29, 2022

Choose a reason for hiding this comment

Uh oh!

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

feliperodri Aug 29, 2022

Choose a reason for hiding this comment

Uh oh!

nwetzler Aug 29, 2022

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

nwetzler Aug 29, 2022

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 commented Aug 30, 2022

Uh oh!

remi-delmas-3000 commented Aug 30, 2022

Uh oh!

peterschrammel Sep 1, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

CONTRACTS: Handle all 4 inlining warning types in `inlining_decoratort` #7083

CONTRACTS: Handle all 4 inlining warning types in `inlining_decoratort` #7083

remi-delmas-3000 commented Aug 25, 2022 •

edited

Loading

codecov bot commented Aug 25, 2022 •

edited

Loading

remi-delmas-3000 Aug 30, 2022 •

edited

Loading

remi-delmas-3000 Aug 30, 2022 •

edited

Loading

remi-delmas-3000 Aug 30, 2022 •

edited

Loading

remi-delmas-3000 Aug 30, 2022 •

edited

Loading