Skip to content

Dump c var overlap #6257

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 13 commits into from
Aug 3, 2021
Merged

Dump c var overlap #6257

merged 13 commits into from
Aug 3, 2021

Conversation

TGWDB
Copy link
Contributor

@TGWDB TGWDB commented Jul 28, 2021

This PR adds checking for variable scope collision between function local variables and function arguments. These were previously allowed to clash as shown in PR #6242 . This PR fixes #6242

  • 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.

TGWDB added 10 commits July 26, 2021 09:39
This adds variable name collision checking for collision between
function arguments and local function variables.

Fixes diffblue#6242
This fixes unit test checking when scope collision causes
variable renaming.
This adds regression tests for rol/ror using symtba2gb and
goto-instrument.
Adds unit test for expr2c of rol and ror operators, testing both
signed and unisgned conversions.
Tidies up the style and addresses reviewer comments:
- use to_shift_exprt before call to convert_rox
- remove "kind" path to try and guess bit width
This adds variable name collision checking for collision between
function arguments and local function variables.

Fixes diffblue#6242
This fixes unit test checking when scope collision causes
variable renaming.
This adds regression tests for when names collide in dump-c
output when converting from json.
@TGWDB TGWDB added aws Bugs or features of importance to AWS CBMC users bugfix labels Jul 28, 2021
@codecov
Copy link

codecov bot commented Jul 28, 2021

Codecov Report

Merging #6257 (8a224be) into develop (3493061) will increase coverage by 0.01%.
The diff coverage is 94.49%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6257      +/-   ##
===========================================
+ Coverage    76.16%   76.18%   +0.01%     
===========================================
  Files         1484     1485       +1     
  Lines       162173   162231      +58     
===========================================
+ Hits        123525   123594      +69     
+ Misses       38648    38637      -11     
Impacted Files Coverage Δ
src/ansi-c/expr2c_class.h 100.00% <ø> (ø)
src/goto-instrument/contracts/assigns.cpp 92.36% <ø> (ø)
src/goto-instrument/contracts/contracts.h 100.00% <ø> (ø)
...rc/goto-instrument/contracts/memory_predicates.cpp 83.81% <ø> (-0.19%) ⬇️
src/goto-instrument/contracts/contracts.cpp 91.83% <90.24%> (-0.10%) ⬇️
src/ansi-c/expr2c.cpp 65.60% <94.87%> (+0.65%) ⬆️
src/solvers/smt2/smt2_parser.cpp 77.90% <100.00%> (ø)
unit/ansi-c/expr2c.cpp 100.00% <100.00%> (ø)
... and 3 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 b0b71d0...8a224be. Read the comment docs.

@TGWDB TGWDB force-pushed the dump-c-var-overlap branch from ac74654 to 51d28bd Compare July 28, 2021 18:41
martin and others added 3 commits July 29, 2021 15:44
Resolve an ambiguous resolution of an overloaded function in G++ 6
This adds conversion for the rol and ror operators from CBMC
internals into C code. This is done by bit-twiddling the values
to achieve the outcome.

Fixes diffblue#6241
// We could also conflict with a function argument, the code below
// finds the function we're in, and checks we don't conflict with
// any argument to the function
const std::string symbol_str = id2string(symbol_id);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there a reasons this symbol name/symboilt lookup code is not the same as the code in lines 168-173 above? In fact, can the checks in this block not just be folded into that existing check block?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The check in lines 168-173 is seeing whether the symbol we're looking at now has a conflict with a function symbol name, e.g.

void f();

void main(int argc)
{
  int f;
  int g;

where here f is both a local variable in main and also the function f.

The new code is finding the current function we're in (e.g. inside main above) to check for collisions between local symbols and argument symbols (i.e. above f and g symbols in the main function do not collide with argc.

Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would it be possible to add a dump-c regression test as well? It would seem rather simple to construct this case. Thank you!

@TGWDB
Copy link
Contributor Author

TGWDB commented Aug 3, 2021

Would it be possible to add a dump-c regression test as well? It would seem rather simple to construct this case. Thank you!

I can do this, but will wait and do it after #6253 since this includes infrastructure for regression tests of this form.

@TGWDB TGWDB merged commit b65fee1 into diffblue:develop Aug 3, 2021
@tautschnig
Copy link
Collaborator

Would it be possible to add a dump-c regression test as well? It would seem rather simple to construct this case. Thank you!

I can do this, but will wait and do it after #6253 since this includes infrastructure for regression tests of this form.

@TGWDB Did this actually happen? #6253 got merged, and now the diff in this PR looks almost as big, so I'm struggling to tell.

@TGWDB
Copy link
Contributor Author

TGWDB commented Aug 4, 2021

@tautschnig Yes, two tests added for detecting different variable name collisions in this commit:
aa0a5dc

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
aws Bugs or features of importance to AWS CBMC users bugfix
Projects
None yet
Development

Successfully merging this pull request may close these issues.

goto-instrument --dump-c produces invalid code when parameter name overlaps with local variable name
4 participants