CONTRACTS: Populate function name in source locations #7037

nwetzler · 2022-07-27T22:40:27Z

During parsing of function parameters, the function name should be set
in the source location, but only for top-level function declarations
and definitions. In addition, function contracts should be only
allowed for top-level function declarations and definitions.

CBMC Viewer reports a failure when analyzing the incomplete coverage
report, causing the CMBC Starter Kit to fail during a standard build.

Also removed source location from "end function" command during
contract checking and added proper source location to function
contract instrumentation.

Resolves issues #7032, #7070

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.

tautschnig · 2022-07-28T12:56:27Z

@nwetzler The failing tests still need looking at.

kroening · 2022-07-28T20:20:52Z

src/ansi-c/c_typecheck_base.cpp

@@ -674,6 +674,28 @@ void c_typecheck_baset::apply_asm_label(
  }
 }

+/// Recursively set function name in source locations of expression


Would it not be better to set the function name when parsing the contract?

Remi and I were under the impression that the function name doesn't exist or isn't readily available at parsing time. This is because the function doesn't fully exist until the body has been parsed. If it is possible during parsing, that would be a better solution, but I didn't see a way to make it happen.

You've got the function name once the declarator has been seen; this is well before the contract.

@kroening I've now changed this in the parser and have removed changes from type-checking. The parser will now set the function in source location, but only for top-level functions. I think this change results in the correct behavior and excludes problems introduced by function pointers.

nwetzler · 2022-07-28T23:52:29Z

@nwetzler The failing tests still need looking at.

I've updated the contract tests to include the function name in regular expressions.

codecov · 2022-08-01T13:44:58Z

Codecov Report

Merging #7037 (83abf73) into develop (948994a) will increase coverage by 0.00%.
The diff coverage is 87.28%.

@@           Coverage Diff            @@
##           develop    #7037   +/-   ##
========================================
  Coverage    77.87%   77.87%           
========================================
  Files         1574     1574           
  Lines       181163   181180   +17     
========================================
+ Hits        141072   141089   +17     
  Misses       40091    40091

Impacted Files	Coverage Δ
jbmc/src/jbmc/jbmc_parse_options.cpp	`75.88% <0.00%> (ø)`
...variable-sensitivity/variable_sensitivity_domain.h	`100.00% <ø> (ø)`
.../analyses/variable-sensitivity/write_stack_entry.h	`100.00% <ø> (ø)`
src/ansi-c/ansi_c_typecheck.cpp	`67.85% <0.00%> (ø)`
src/ansi-c/expr2c_class.h	`100.00% <ø> (ø)`
src/cpp/cpp_typecheck.cpp	`77.70% <0.00%> (ø)`
src/goto-analyzer/goto_analyzer_parse_options.cpp	`72.27% <ø> (ø)`
src/goto-cc/armcc_cmdline.cpp	`22.22% <ø> (ø)`
src/goto-cc/gcc_cmdline.cpp	`79.23% <ø> (ø)`
src/goto-cc/ms_cl_cmdline.cpp	`0.00% <ø> (ø)`
... and 127 more

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

src/ansi-c/parser.y

During parsing of function parameters, the function name should be set in the source location, but only for top-level function declarations and definitions. In addition, function contracts should be only allowed for top-level function declarations and definitions. CBMC Viewer reports a failure when analyzing the incomplete coverage report, causing the CMBC Starter Kit to fail during a standard build. Also removed source location from "end function" command during contract checking and added proper source location to function contract instrumentation. Resolves issues diffblue#7032, diffblue#7070

jimgrundy

Thanks for those changes. I like it.

feliperodri

LGTM, only minor comments.

feliperodri · 2022-08-16T17:32:48Z

regression/contracts/embedded_contract_fail_01/test.desc

+--
+Checks if function contracts can be attached to function pointers
+(with non-empty parameter lists) in function parameters.  This should
+fail.  Exit code 64 for Windows servers.


You don't need to include "Exit code 64 for Windows servers." in the description, the error code itself is self-explanatory.

I felt better reminding myself why there are two acceptable exit codes. I'd like to keep the comment unless the 1 and 64 pattern is super common.

The pattern is quite common as it appears in 118 test description, but there is no harm in leaving this reminder here as well.

feliperodri · 2022-08-16T18:47:31Z

src/ansi-c/parser.y

+          int contract_in_global_scope = (PARSER.scopes.size() == 1);
+          int contract_in_top_level_function_scope = (PARSER.scopes.size() == 2);


Could you explain the magic numbers 1 and 2 in the comment?

I was hoping the long variable names, combined with the comment above, would be self-documenting. When we initialize the parser, we start by pushing a global scope onto the stack. (There's an invariant that we never have an empty scopes stack.) So a size of 1 means the stack only contains the global scope. A size of two means we must be in some top-level event like a function declaration or definition because we've pushed something else on the stack.

feliperodri · 2022-08-16T18:48:23Z

src/ansi-c/parser.y

+            // Set function name (last declarator) in source location
+            // before parsing function contracts.  Only do this if we
+            // are at a global scope.
+            if (PARSER.current_scope().prefix.empty()) {


@kroening is there a better way to check if we are at a global scope?

I borrowed this methodology from the add_declarator function in ansi_c_parser.cpp:

// global? if(current_scope().prefix.empty()) ansi_c_declaration.set_is_global(true);

I had originally written something like:
if (PARSER.current_scope() == PARSER.root_scope())
But there's no equality comparator defined for the scope class.

SaswatPadhi

Thanks! LGTM

nwetzler requested review from tautschnig, feliperodri, SaswatPadhi, remi-delmas-3000, kroening and chris-ryder as code owners July 27, 2022 22:40

tautschnig approved these changes Jul 28, 2022

View reviewed changes

tautschnig assigned nwetzler Jul 28, 2022

kroening reviewed Jul 28, 2022

View reviewed changes

nwetzler force-pushed the contract-coverage branch from f5cadb0 to 3880b98 Compare July 28, 2022 23:51

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

nwetzler force-pushed the contract-coverage branch from 3880b98 to 9f92553 Compare August 12, 2022 21:50

nwetzler requested review from kroening and tautschnig August 12, 2022 21:54

nwetzler force-pushed the contract-coverage branch 2 times, most recently from 43be30c to 6a8c9a6 Compare August 15, 2022 19:47

nwetzler changed the title ~~Populate function name in source locations for function contracts~~ CONTRACTS: Populate function name in source locations Aug 15, 2022

jimgrundy reviewed Aug 15, 2022

View reviewed changes

src/ansi-c/parser.y Outdated Show resolved Hide resolved

nwetzler force-pushed the contract-coverage branch 2 times, most recently from ca619bf to 1b168d1 Compare August 16, 2022 01:14

nwetzler requested a review from jimgrundy August 16, 2022 01:17

nwetzler force-pushed the contract-coverage branch from 1b168d1 to 83abf73 Compare August 16, 2022 16:26

jimgrundy approved these changes Aug 16, 2022

View reviewed changes

feliperodri approved these changes Aug 16, 2022

View reviewed changes

SaswatPadhi approved these changes Aug 17, 2022

View reviewed changes

jimgrundy merged commit 8756346 into diffblue:develop Aug 17, 2022

This was referenced Aug 24, 2022

Function contract source locations incomplete #7032

Closed

Function contracts can be attached to function pointers as parameters #7070

Closed

nwetzler mentioned this pull request Aug 29, 2022

CONTRACTS: Dynamic frame condition checking #6887

Closed

nwetzler mentioned this pull request Sep 28, 2022

An error(UserWarning(f'Unexpected coverage goal xml data: "{basic_block_lines}"') from error) is reported from cbmc-viewer when I use more than one structure parameters in __CPROVER_ensures. model-checking/cbmc-viewer#131

Closed

		int contract_in_global_scope = (PARSER.scopes.size() == 1);
		int contract_in_top_level_function_scope = (PARSER.scopes.size() == 2);

CONTRACTS: Populate function name in source locations #7037

CONTRACTS: Populate function name in source locations #7037

Uh oh!

Conversation

nwetzler commented Jul 27, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig commented Jul 28, 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!

nwetzler commented Jul 28, 2022

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

Uh oh!

jimgrundy left a comment

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!

SaswatPadhi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

nwetzler commented Jul 27, 2022 •

edited

Loading

codecov bot commented Aug 1, 2022 •

edited

Loading