Fix static symbols referencing in harness file #5412

NlightNFotis · 2020-07-07T15:13:31Z

This is fixing an issue we came across when trying to run goto-harness against the batch jobs in the https://github.com/awslabs/aws-c-common/tree/master/.cbmc-batch/jobs files, where the tool would generate harnesses that referenced static symbols in different files.

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.

codecov · 2020-07-07T15:47:39Z

Codecov Report

Merging #5412 into develop will decrease coverage by 0.00%.
The diff coverage is 60.00%.

@@             Coverage Diff             @@
##           develop    #5412      +/-   ##
===========================================
- Coverage    68.21%   68.21%   -0.01%     
===========================================
  Files         1178     1178              
  Lines        97542    97550       +8     
===========================================
+ Hits         66537    66542       +5     
- Misses       31005    31008       +3

Flag	Coverage Δ
#cproversmt2	`42.76% <ø> (ø)`
#regression	`65.38% <60.00%> (-0.01%)`	⬇️
#unit	`32.26% <ø> (ø)`

Impacted Files	Coverage Δ
src/goto-programs/name_mangler.h	`100.00% <ø> (ø)`
src/goto-programs/name_mangler.cpp	`64.70% <50.00%> (ø)`
src/goto-harness/recursive_initialization.cpp	`89.95% <62.50%> (-0.50%)`	⬇️

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 069db73...d8ad34f. Read the comment docs.

src/goto-harness/recursive_initialization.cpp

regression/goto-harness-gb-input/chain.sh

thk123

Even when relying on magic strings, it is important to not duplicate them, as this makes them even more fragile and prone to error.

regression/goto-harness-gb-input/static-symbol-referencing/test.desc

src/goto-harness/recursive_initialization.cpp

regression/goto-harness-gb-input/Makefile

NlightNFotis · 2020-07-09T10:56:49Z

@thk123 @hannes-steffenhagen-diffblue All of your comments have now been addressed. Can I get another review please?

thk123

Blocking comment addressed - but feel quite strongly that a test without much positive regexes is not a great test.

thk123 · 2020-07-09T11:41:56Z

Done - looks like you've got a formatting problem btw

hannes-steffenhagen-diffblue

I don’t particularly like that this includes a binary, but I suppose it’s better than not having a test at all.

Need to have instructions for how to recreate the goto bianry file

martin-cs

Code change looks fine. Agree with @thk123 about the issue of binary tests. The binary format is not intended to be stable or portable.

regression/goto-harness-gb-input/Makefile

regression/goto-harness-gb-input/static-symbol-referencing/test.desc

NlightNFotis · 2020-07-16T14:18:27Z

Hi @martin-cs @thk123 @hannes-steffenhagen-diffblue I have re-requested approvals on this - The PR was rewritten (at least the last commit that contains the test), to now address your concerns and contains a c source file as a test, and with some other shortcomings addressed.

hannes-steffenhagen-diffblue

I think this is probably addressing @martin-cs and @thk123 comments now

hannes-steffenhagen-diffblue · 2020-07-16T14:19:44Z

src/goto-harness/recursive_initialization.cpp

@@ -1008,6 +1009,27 @@ code_blockt recursive_initializationt::build_function_pointer_constructor(
  for(const auto &target : targets)
  {
    auto const assign = code_assignt{dereference_exprt{result}, target};
+    auto const sym_to_lookup =


Aside comment:

FWIW I think we should probably do something cleverer for function pointers, this is very similar to function pointer removal.

hannes-steffenhagen-diffblue · 2020-07-16T14:21:24Z

src/goto-harness/recursive_initialization.cpp

+        : "";
+    // skip referencing globals because the corresponding symbols in the symbol
+    // table are no longer marked as file local.
+    if(has_prefix(id2string(sym_to_lookup), FILE_LOCAL_PREFIX))


The thinking here is that symbols prefixed this way might actually be referenceable, but we decided to push off potential different handling for this case off as a different feature. This is coming from --export-file-local-symbols apparently.

regression/goto-harness-multi-file-project/static_symbols_referencing/first_one.c

thk123

Blocking problems addressed

NlightNFotis · 2020-07-17T10:07:11Z

Hi @martin-cs, can we get another review on this one? Thanks :)

martin-cs

@NlightNFotis Looks much better -- thank you!

danpoe

LGTM

NlightNFotis requested review from cesaro, chrisr-diffblue, cristina-david, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli, romainbrenguier, smowton, tautschnig and thk123 as code owners July 7, 2020 15:13

NlightNFotis force-pushed the fix_static_symbols_referencing branch from 61e3242 to 2200d36 Compare July 8, 2020 10:54

hannes-steffenhagen-diffblue reviewed Jul 8, 2020

View reviewed changes

src/goto-harness/recursive_initialization.cpp Outdated Show resolved Hide resolved

src/goto-harness/recursive_initialization.cpp Outdated Show resolved Hide resolved

regression/goto-harness-gb-input/chain.sh Outdated Show resolved Hide resolved

NlightNFotis force-pushed the fix_static_symbols_referencing branch 3 times, most recently from fabce15 to f40631e Compare July 8, 2020 16:36

NlightNFotis requested a review from hannes-steffenhagen-diffblue July 8, 2020 18:40

thk123 reviewed Jul 9, 2020

View reviewed changes

NlightNFotis force-pushed the fix_static_symbols_referencing branch from f40631e to 5bf11c8 Compare July 9, 2020 10:55

thk123 previously approved these changes Jul 9, 2020

View reviewed changes

NlightNFotis force-pushed the fix_static_symbols_referencing branch from 5bf11c8 to 15d47ca Compare July 9, 2020 13:41

hannes-steffenhagen-diffblue approved these changes Jul 9, 2020

View reviewed changes

martin-cs requested changes Jul 13, 2020

View reviewed changes

regression/goto-harness-gb-input/Makefile Outdated Show resolved Hide resolved

regression/goto-harness-gb-input/static-symbol-referencing/test.desc Outdated Show resolved Hide resolved

regression/goto-harness-gb-input/static-symbol-referencing/test.desc Outdated Show resolved Hide resolved

Introduce global constant for file local prefix in the mangler

a19f027

Add fix for file local symbols referencing

3b2494f

NlightNFotis force-pushed the fix_static_symbols_referencing branch from 15d47ca to 3b16eb9 Compare July 16, 2020 14:15

NlightNFotis requested review from thk123, hannes-steffenhagen-diffblue and martin-cs July 16, 2020 14:16

hannes-steffenhagen-diffblue approved these changes Jul 16, 2020

View reviewed changes

hannes-steffenhagen-diffblue reviewed Jul 16, 2020

View reviewed changes

regression/goto-harness-multi-file-project/static_symbols_referencing/first_one.c Show resolved Hide resolved

Add test for fixing of referencing of static symbols in harness file.

d8ad34f

NlightNFotis force-pushed the fix_static_symbols_referencing branch from 3b16eb9 to d8ad34f Compare July 16, 2020 14:39

thk123 approved these changes Jul 16, 2020

View reviewed changes

martin-cs approved these changes Jul 19, 2020

View reviewed changes

danpoe approved these changes Jul 20, 2020

View reviewed changes

NlightNFotis mentioned this pull request Jul 20, 2020

Changes to goto-harness documentation #5428

Merged

7 tasks

peterschrammel approved these changes Jul 20, 2020

View reviewed changes

NlightNFotis merged commit febb5cf into diffblue:develop Jul 20, 2020

NlightNFotis deleted the fix_static_symbols_referencing branch February 19, 2021 11:22

Fix static symbols referencing in harness file #5412

Fix static symbols referencing in harness file #5412

Uh oh!

Conversation

NlightNFotis commented Jul 7, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Jul 7, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

NlightNFotis commented Jul 9, 2020

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 commented Jul 9, 2020

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

NlightNFotis commented Jul 16, 2020

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Jul 16, 2020

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Jul 16, 2020

Choose a reason for hiding this comment

Uh oh!

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

NlightNFotis commented Jul 17, 2020

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

danpoe left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

NlightNFotis commented Jul 7, 2020 •

edited

Loading

codecov bot commented Jul 7, 2020 •

edited

Loading