Set addr_bits via command line and per language #1161

peterschrammel · 2017-07-21T07:18:38Z

In Java we often need more than 256 objects (which is a bottleneck), whereas some other people work with very large objects. Setting the number of address bits via the command line allows everyone who really needs it to adjust the encoding. Additionally language defaults are set so that for normal usage the option is not required.

1c4191a adds a test that should fail if we checked that offset arithmetic didn't overflow (which is not detected at the moment).

Tested with with --addr-bits n for n in [-1,65] on cbmc and cbmc-java regression tests. Found one bug in getting models from the solver 50a56a1.

Improved error messages (which looks ugly as it is now and shows the need for properly typed exceptions throughout the codebase).

tautschnig · 2017-07-21T07:25:18Z

As much as I hope to get #1086 done (and fully working) some time soon, this seems to be a very reasonable workaround. The bits I'd ask to improve are the user-facing messages, as the majority of users will have no idea about the encoding.

tautschnig · 2017-07-24T10:54:31Z

src/cbmc/cbmc_parse_options.cpp

@@ -1060,6 +1062,7 @@ void cbmc_parse_optionst::help()
    " --graphml-witness filename   write the witness in GraphML format to filename\n" // NOLINT(*)
    "\n"
    "Backend options:\n"
+    " --addr-bits n                number of bits used for object addresses\n"


I'd say "object-bits", but more important is the message, which we need to get as clear as possible. How about "number of bits to distinguish objects that have their address taken (default: 8)". Comments welcome!

tautschnig · 2017-07-24T10:57:56Z

src/solvers/flattening/bv_pointers.cpp

-    throw "too many variables";
+  const std::size_t max_objects=std::size_t(1)<<object_bits;
+  if(a==max_objects)
+    throw "too many dynamic objects: maximum number of objects is set to 2^n="+


"too many addressed objects" maybe? Taking the address of a local or static variable also counts...

tautschnig · 2017-07-24T11:00:50Z

src/util/config.cpp

+  }
+
+  // set addr_bits according to entry point language
+  if(symbol_table.has_symbol(CPROVER_PREFIX "_start"))


Use else if and avoid duplicate error messages by just using the "DATA_INVARIANT" below?

tautschnig · 2017-07-24T11:05:10Z

src/cbmc/cbmc_parse_options.cpp

@@ -662,6 +662,8 @@ int cbmc_parse_optionst::get_goto_program(
    if(!binaries.empty())
      config.set_from_symbol_table(symbol_table);

+    config.set_addr_bits(cmdline, symbol_table);


I believe this should be done by configt automatically, as doing this only in "cbmc_parse_options.cpp" may not be sufficient.

What do you mean by 'automatically'?

config.set(cmdline) (line 103) should just take care of this, I'd say.

You can't set language defaults at this point because the language isn't known yet.

Well, we can always set defaults for all languages, can't we? If we have a design that requires calling the config 1) multiple times and 2) in a certain sequence then this is bound to break.

Setting the config has already been a multistage process before, in particular there are side conditions that the symbol table has been populated. Ie. You don't get the final config before having processed all input files. I see two options: 1) update the config after loading input files (means hooking into language_Ui.final and read Goto binary), 2) introduce a config.finalise call that must be invoked after having read the last input file.
The first option wouldn't require any collaboration of *_parse_optionst, but scatters initialisation of config over several functions, which might become hard to understand. The second one does require collaboration but makes it a bit more uniform wrt how it is currently done in master.

My apologies, yes, it is a two-step process in case goto binaries are being read. But then shouldn't those two same steps suffice to adjust the address bits?

Your suggestions go further to eliminate even that second step, or rather avoid the redundancy across tools. Indeed read_object_and_link could be a good place to invoke config.set_from_symbol_table.

It's only called from within configt.

smowton

Looks good, a few minor notes

smowton · 2017-07-25T20:45:27Z

regression/cbmc/address_space_size_limit3/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--32 --little-endian --object-bits 25 --pointer-check


Please comment either in this test,desc or in the test body what this assembly is testing

smowton · 2017-07-25T20:48:22Z

src/solvers/smt1/smt1_conv.cpp


    p.offset=
-      binary2integer(value.substr(BV_ADDR_BITS, std::string::npos), true);
+      binary2integer(
+        value.substr(config.bv_encoding.object_bits, std::string::npos), true);


Style: break line before true);

This is legal if it fits into the line.

smowton · 2017-07-25T20:53:52Z

src/util/config.cpp

+      bv_encoding.object_bits=cpp.default_object_bits;
+    DATA_INVARIANT(
+      0<bv_encoding.object_bits && bv_encoding.object_bits<ansi_c.pointer_width,
+      "object_bits should fit into pointer width");


Suggest reporting the outcome (and why) so that user reports show the decision process. For example
Running with 8 object bits, 24 offset bits (user-specified) or
Running with 16 object bits, 48 offset bits (default for java language)

Good idea. Added output to status stream.

peterschrammel · 2017-07-26T12:54:56Z

@tautschnig, @smowton, I have taken into account your comments.

tautschnig

Looks good to me, thank you for all the refactoring!

One is detected with --pointer-check enabled, the other one is currently not detected.

Bug exhibited by cbmc-java/iterator2 when run with --object-bits 35

peterschrammel · 2018-06-09T14:09:17Z

@tautschnig, do we need still need these old develop->master PRs?

tautschnig · 2018-06-09T14:11:12Z

I don't really think we need those anymore, unless they have resulted in useful discussion and should thus yield fixes in develop.

peterschrammel · 2018-06-09T14:12:05Z

I'll check before closing.

tautschnig · 2019-03-02T09:32:18Z

Closing as merged in develop with "master" no longer being updated.

peterschrammel added the do not merge label Jul 21, 2017

peterschrammel force-pushed the object-encoding branch 3 times, most recently from 823b7e8 to 50a56a1 Compare July 22, 2017 20:26

peterschrammel removed the do not merge label Jul 22, 2017

peterschrammel force-pushed the object-encoding branch from 50a56a1 to 9d9080f Compare July 22, 2017 20:34

peterschrammel requested a review from tautschnig July 22, 2017 20:34

tautschnig requested changes Jul 24, 2017

View reviewed changes

peterschrammel added 3 commits July 25, 2017 15:29

Make configt::set_classpath private

b5d4187

It's only called from within configt.

Factorize setting config from symbol table when reading goto binaries

549443b

Replace BV_ADDR_BITS by config setting

c624d24

peterschrammel force-pushed the object-encoding branch 2 times, most recently from 0bf0ba7 to ba6e04d Compare July 25, 2017 14:02

Better error message when too many dynamic objects

c29bf8c

peterschrammel force-pushed the object-encoding branch from ba6e04d to d1c7938 Compare July 25, 2017 14:05

peterschrammel requested a review from smowton July 25, 2017 20:37

smowton approved these changes Jul 25, 2017

View reviewed changes

peterschrammel force-pushed the object-encoding branch from d1c7938 to 5c6134a Compare July 26, 2017 09:27

tautschnig approved these changes Jul 26, 2017

View reviewed changes

smowton approved these changes Jul 26, 2017

View reviewed changes

peterschrammel assigned kroening Aug 1, 2017

peterschrammel added the enhancement label Aug 1, 2017

peterschrammel mentioned this pull request Aug 1, 2017

Set addr_bits via command line and per language (test-gen-support) #1189

Merged

peterschrammel added 5 commits August 2, 2017 16:06

Allow specifying object-bits via command line and language defaults

18f30a6

Catch command line parsing exceptions

d7715c7

Add java address space limits tests

f4a6dd1

Tests for overflows in pointer arithmetic

12e280f

One is detected with --pointer-check enabled, the other one is currently not detected.

Fix getting model for object address (unsigned -> size_t)

e9b9dd8

Bug exhibited by cbmc-java/iterator2 when run with --object-bits 35

Output message about used object bits settings

ded2d1c

peterschrammel force-pushed the object-encoding branch from 5c6134a to ded2d1c Compare August 2, 2017 15:07

tautschnig changed the base branch from master to develop August 22, 2017 12:20

tautschnig changed the base branch from develop to master August 22, 2017 15:18

tautschnig changed the title ~~Set addr_bits via command line and per language~~ [develop->master] Set addr_bits via command line and per language Aug 22, 2017

tautschnig changed the title ~~[develop->master] Set addr_bits via command line and per language~~ Set addr_bits via command line and per language Sep 2, 2017

tautschnig added the develop->master label Sep 2, 2017

tautschnig closed this Mar 2, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Set addr_bits via command line and per language #1161

Set addr_bits via command line and per language #1161

peterschrammel commented Jul 21, 2017 •

edited

Loading

tautschnig commented Jul 21, 2017

tautschnig Jul 24, 2017

tautschnig Jul 24, 2017

tautschnig Jul 24, 2017

tautschnig Jul 24, 2017

peterschrammel Jul 25, 2017

tautschnig Jul 25, 2017

peterschrammel Jul 25, 2017

tautschnig Jul 25, 2017

peterschrammel Jul 25, 2017 •

edited

Loading

tautschnig Jul 25, 2017

smowton left a comment

smowton Jul 25, 2017

smowton Jul 25, 2017

peterschrammel Jul 26, 2017

smowton Jul 25, 2017

peterschrammel Jul 26, 2017

peterschrammel commented Jul 26, 2017

tautschnig left a comment

peterschrammel commented Jun 9, 2018

tautschnig commented Jun 9, 2018

peterschrammel commented Jun 9, 2018

tautschnig commented Mar 2, 2019

Set addr_bits via command line and per language #1161

Set addr_bits via command line and per language #1161

Conversation

peterschrammel commented Jul 21, 2017 • edited Loading

tautschnig commented Jul 21, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel Jul 25, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented Jul 26, 2017

tautschnig left a comment

Choose a reason for hiding this comment

peterschrammel commented Jun 9, 2018

tautschnig commented Jun 9, 2018

peterschrammel commented Jun 9, 2018

tautschnig commented Mar 2, 2019

peterschrammel commented Jul 21, 2017 •

edited

Loading

peterschrammel Jul 25, 2017 •

edited

Loading