Add `--object-bits` option to goto-cc #5440

thomasspriggs · 2020-07-31T19:30:09Z

So that we can support running with non-default settings of --object-bits in goto-cc. This should address the issue seen in #5272

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-08-03T10:46:15Z

Codecov Report

Merging #5440 into develop will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5440   +/-   ##
========================================
  Coverage    68.22%   68.22%           
========================================
  Files         1178     1178           
  Lines        97580    97580           
========================================
  Hits         66573    66573           
  Misses       31007    31007

Flag	Coverage Δ
#cproversmt2	`42.79% <ø> (ø)`
#regression	`65.39% <ø> (ø)`
#unit	`32.26% <ø> (-0.01%)`	⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/goto-cc/gcc_cmdline.cpp	`74.48% <ø> (ø)`
src/goto-cc/goto_cc_mode.cpp	`26.66% <ø> (ø)`

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 b3a6cc4...06c5aa1. Read the comment docs.

hannes-steffenhagen-diffblue · 2020-08-03T13:21:20Z

regression/goto-cc-cbmc-shared-options/object-bits/test.c

+find_first_set(const size_t max_malloc_size, const size_t bits_accumulator)
+{
+  // Implemented using recursion to avoid excessive unwinding or specifying an
+  // unwind limit.


how does recursion stop excessive unwinding?

I discovered this by experimentation. The same algorithm written as a loop spent a long time unwinding if no unwind limit was set. The recursive version only unwinds a sufficient number of times for the value of max_malloc_size which is actually specified.

I am not familiar with the unwinding code. However I would hazard a guess that loop unwinding happens early on, using a only a local analysis. Whereas recursion unwinding happens later as part of symmex. The constant being passed to the function is been propagated in this case, leading to unwinding the exact number of times required.

I haven't been able to reproduce the problem I saw with the iterative version and I never committed that version, so I can't get it back even with git reflog. Therefore I am going to assume there is no problem with unwinding loops / constant propagation. I shall delete this comment in order to avoid being misleading, but leave the recursive version in place because it doesn't seem worth rewriting this.

hannes-steffenhagen-diffblue · 2020-08-03T13:23:32Z

src/goto-cc/gcc_cmdline.cpp

@@ -28,6 +28,7 @@ const char *goto_cc_options_with_separated_argument[]=
  "--native-linker",
  "--print-rejected-preprocessed-source",
  "--mangle-suffix",
+  "--object-bits",


Shouldn't this be added to the other cmdlinets as well?

The original ticket referred to goto-cc only, fixing goto-cc only will get a fix ready for use sooner. Yes, the same problem and fix probably applies to the other entry points as well. The time consuming part of fixing the other entry points would be writing tests for each of them.

There is no standard list of options in the base class. So it would need to be manually added and tested for each cmdlinet in the heirarchy.

hannes-steffenhagen-diffblue

So adding the option to the cmdlinet was all that was needed to make this work? Neat.

hannes-steffenhagen-diffblue · 2020-08-03T13:51:59Z

regression/goto-cc-cbmc-shared-options/object-bits/default_bits.desc

+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion object_bits != 8: FAILURE


can you add the expected results for the other assertions in here as well? Clearly it's supposed to be always 2 successes and one failure but that might be easier to see if its spelt out.

danpoe

I think for now this solution is fine. At some point though, the __CPROVER_max_malloc_size variable will go away anyways (when ADA-576 is implemented) and the conflict will disappear. Then goto-cc should be able to be oblivious to the object bits setting again.

The reason for __CPROVER_max_malloc_size going away is that it is currently used to check that not more memory is allocated than can be addressed by cbmc. However, it turns out that a better way to implement this is to check for pointer overflows instead (see discussion on #5401).

danpoe · 2020-08-03T14:44:54Z

regression/goto-cc-cbmc-shared-options/object-bits/test.c

+  return find_first_set(max_malloc_size >> 1, bits_accumulator + 1);
+}
+
+size_t calculate_object_bits()


IMO it would be unnecessary to reverse engineer the object bits here or even use the value of __CPROVER_max_malloc_size. It's probably sufficient to just run cbmc with a non-default object bits setting after goto-cc and check that it suceeds.

The reason I chose to do it this way is that the previous incorrect behaviour resulted in a warning, but might not actually cause a failure without giving an input program which depends on the implications of the object-bits configuration. I could have used a negative regex to check that the warning message does not appear in the output. However this would not be a robust test because if the text of the message were to be updated then the corresponding test could easily be missed. This may be a little over-engineered but I am happy that this is a robust test and it is clear what the positive regexes are actually checking for.

Yes, that makes sense.

chrisr-diffblue

Have you tested what happens with linking? I'm thinking of the case where you compile one translation unit with one value for object-bits, and another translation unit with a different value for object-bits. How does the linker handle that? (Hopefully with a nice user-friendly error message... :-) )

thomasspriggs · 2020-08-06T11:11:44Z

@chrisr-diffblue If I feed two different goto binaries into cbmc which were generated using different --object-bits configurations then it generates appropriate warning messages -

$ cbmc ./temp_func.gb ./temp_main.gb
CBMC version 5.12 (cbmc-5.12.4-9-gdae95d970-dirty) 64-bit x86_64 linux
Reading GOTO program from file
Reading: ./temp_func.gb
Reading GOTO program from file
Reading: ./temp_main.gb
file <built-in-additions> line 24: warning: conflicting initializers for variable "__CPROVER_max_malloc_size"
using old value in module temp_func file <built-in-additions> line 24
9007199254740992ul
ignoring new value in module temp_main file <built-in-additions> line 24
144115188075855872ul
Generating GOTO Program
Adding CPROVER library (x86_64)
file <built-in-additions> line 24: warning: conflicting initializers for variable "__CPROVER_max_malloc_size"
using old value in module temp_func file <built-in-additions> line 24
9007199254740992ul
ignoring new value in module <built-in-library> file <built-in-additions> line 24
36028797018963968ul
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking

chrisr-diffblue

I'm glad theres a diagnostic, thanks for checking/demonstrating. It's probably an open question whether that should be an error rather than a warning, but that doesn't have to be fixed in this PR, so feel free to raise a Github bug ticket to cover that. It'd be super nice if there was a test case to demonstrate the diagnostic gets triggered (just so we don't end up accidentally losing that at some point :-) ) but again, I won't block the PR just on that.

So that we can support running with non-default settings of `--object-bits` in `goto-cc`.

thomasspriggs requested review from chrisr-diffblue, kroening and tautschnig as code owners July 31, 2020 19:30

thomasspriggs requested review from hannes-steffenhagen-diffblue and NlightNFotis July 31, 2020 19:30

thomasspriggs force-pushed the tas/goto-cc-object-bits-size branch from c53603d to 63fd092 Compare August 3, 2020 09:35

thomasspriggs mentioned this pull request Aug 3, 2020

Refactoring around the goto-cc entry point. #5442

Merged

7 tasks

hannes-steffenhagen-diffblue reviewed Aug 3, 2020

View reviewed changes

NlightNFotis approved these changes Aug 3, 2020

View reviewed changes

danpoe reviewed Aug 3, 2020

View reviewed changes

thomasspriggs requested review from peterschrammel and smowton as code owners August 3, 2020 18:06

thomasspriggs force-pushed the tas/goto-cc-object-bits-size branch 2 times, most recently from 7a0ac50 to 8c8fc97 Compare August 4, 2020 13:38

chrisr-diffblue reviewed Aug 5, 2020

View reviewed changes

danpoe approved these changes Aug 6, 2020

View reviewed changes

chrisr-diffblue approved these changes Aug 6, 2020

View reviewed changes

thomasspriggs mentioned this pull request Aug 6, 2020

Running goto-cc followed by cbmc with different values for --object-bits only causes a warning. #5443

Closed

thomasspriggs added 2 commits August 6, 2020 12:28

Add --object-bits option to goto-cc

e4a50aa

So that we can support running with non-default settings of `--object-bits` in `goto-cc`.

Document new goto-cc --object-bits command line option

06c5aa1

thomasspriggs force-pushed the tas/goto-cc-object-bits-size branch from 8c8fc97 to 06c5aa1 Compare August 6, 2020 11:28

thomasspriggs merged commit 666c2f0 into diffblue:develop Aug 6, 2020

thomasspriggs deleted the tas/goto-cc-object-bits-size branch August 6, 2020 12:57

This was referenced Aug 6, 2020

goto-cc isn't aware of cbmc's --object-bits setting #5272

Closed

Refactoring of the parsing of the --object-bits command line argument #5447

Merged

Add --object-bits option to goto-cc #5440

Add --object-bits option to goto-cc #5440

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Aug 3, 2020 • 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!

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!

hannes-steffenhagen-diffblue 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!

danpoe left a comment • 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!

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!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

thomasspriggs commented Aug 6, 2020

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Add `--object-bits` option to goto-cc #5440

Add `--object-bits` option to goto-cc #5440

thomasspriggs commented Jul 31, 2020 •

edited

Loading

codecov bot commented Aug 3, 2020 •

edited

Loading

thomasspriggs Aug 3, 2020 •

edited

Loading

danpoe left a comment •

edited

Loading