sort bytecode_info table by bytecode #4670

kroening · 2019-05-19T13:12:44Z

The bytecode_info table is now sorted by bytecode, instead of
alphabetically. This is enables direct lookup of bytecodes, and can replace
the table that is currently built at runtime. We do not have any use for
the alphabetic ordering.

Obtained from previous file with

sort -t, -k2 bytecode_info.cpp -b

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a 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).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 5d8125e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112355616

smowton · 2019-05-20T10:30:15Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

-       i_it->statement!="jsr" &&
-       i_it->statement!="jsr_w" &&
-       i_it->statement!="ret")
+    const std::string statement = bytecode_info[i_it->bytecode].mnemonic;


No, this is turning a const char * into a string, for comparison.
Won't fix now, since this will be replaced by bytecode comparisons.

smowton · 2019-05-20T10:32:05Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+    const std::string statement = bytecode_info[i_it->bytecode].mnemonic;
+
+    if(
+      statement != "goto" && statement != "return" &&


Suggested followup -- create symbolic constants for these JAVA_BYTECODE_NOP and so on, and compare those instead of the mnemonics

Yes, that's the plan.

smowton · 2019-05-20T10:33:40Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

-         instruction.statement == "ldc2" ||
-         instruction.statement == "ldc_w" ||
-         instruction.statement == "ldc2_w")
+      const std::string statement =


smowton · 2019-05-20T10:33:48Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -311,8 +311,9 @@ static void infer_opaque_type_fields(
    for(const java_bytecode_parse_treet::instructiont &instruction :
          method.instructions)
    {
-      if(instruction.statement == "getfield" ||
-         instruction.statement == "putfield")
+      const std::string statement =


smowton · 2019-05-20T10:33:58Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -584,8 +586,9 @@ static void create_stub_global_symbols(
    for(const java_bytecode_parse_treet::instructiont &instruction :
          method.instructions)
    {
-      if(instruction.statement == "getstatic" ||
-         instruction.statement == "putstatic")
+      const std::string statement =


smowton · 2019-05-20T10:36:41Z

jbmc/src/java_bytecode/bytecode_info.cpp

@@ -15,86 +15,139 @@ Author: Daniel Kroening, [email protected]
 // clang-format off
 struct bytecode_infot const bytecode_info[]=
 {
-{ "aaload",         0x32, ' ', 2, 1, ' ' }, // arrayref, index → value; load onto the stack a reference from an array  NOLINT(*)
-{ "aastore",        0x53, ' ', 3, 0, ' ' }, // arrayref, index, value →; store into a reference in an array  NOLINT(*)
+{ "nop",            0x00, ' ', 0, 0, ' ' }, // [No change]; perform no operation  NOLINT(*)


Given anyone using this table already has a bytecode, the second field is useless now

Keeping for audit!

smowton · 2019-05-20T10:37:44Z

jbmc/src/java_bytecode/bytecode_info.cpp

 { "impdep1",        0xfe, ' ', 0, 0, ' ' }, // ; reserved for implementation-dependent operations within debuggers; should not appear in any class file  NOLINT(*)
 { "impdep2",        0xff, ' ', 0, 0, ' ' }, // ; reserved for implementation-dependent operations within debuggers; should not appear in any class file  NOLINT(*)
-{ "wide",           0xc4, ' ', 0, 0, ' ' }, // modifier for others  NOLINT(*)
 { nullptr,          0x00, '\0',0, 0, '\0'}, // zero-initialized NOLINT (*)


This looks like a magic terminator, but nothing about it is unique (0x00 is also nop, and a nullptr mnemonic is shared by the missing entries)-- suggest removing it

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: ccab473).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112420225
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 3b70661).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112439621
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 46daf81).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112482347
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: c60a918).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113236477

smowton

Formatting grumbles only, otherwise lgtm

smowton · 2019-05-28T10:00:39Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

-       i_it->statement=="invokeinterface" ||
-       (threading_support && (i_it->statement=="monitorenter" ||
-       i_it->statement=="monitorexit")))
+    if(


Suggest killing clang-format here to keep the nicer one-cndition-per-line format

smowton · 2019-05-28T10:00:46Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

-       i_it->statement=="ifnull" ||
-       i_it->statement=="jsr" ||
-       i_it->statement=="jsr_w")
+    if(


smowton · 2019-05-28T10:01:10Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

+      const std::string statement =
+        bytecode_info[instruction.bytecode].mnemonic;
+      if(
+        statement == "ldc" || statement == "ldc2" || statement == "ldc_w" ||


thk123

🚫 This will need a manual bump - I'll take care of this but please wait before merging
💡 I would add a unit test that verifies the table has the correct structure (e.g. that the position matches the bytecode, that there are no gaps etc)

thk123 · 2019-05-28T11:06:59Z

I will do the bump once rebased - please let me know when

kroening · 2019-05-28T12:02:06Z

@thk123 done!

thk123 · 2019-05-28T12:52:32Z

Sorry could I have one more rebase as I think #4705 is required for TG compatibility and this is just before it.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 7822fac).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113427828

thk123 · 2019-05-29T12:30:49Z

@kroening sorry didn't tag you - can I have one more rebase as #4705 has been merged into TG submodule
#4670 (comment)

tautschnig · 2019-05-30T08:36:02Z

@kroening Please rebase now that #4729 is in to make CI happy.

The bytecode_info table is now sorted by bytecode, instead of alphabetically. This is enables direct lookup of bytecodes, and can replace the table that is currently built at runtime. We do not have any use for the alphabetic ordering. Obtained from previous file with sort -t, -k2 bytecode_info.cpp -b

The run-time generated bytecode table is replaced by bytecode_info. The linear search for the mnemonic is replaced by an array access.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: b149012).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113731628

kroening added the Java Front End label May 19, 2019

kroening requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners May 19, 2019 13:12

allredj reviewed May 19, 2019

View reviewed changes

kroening force-pushed the sort_bytecode_info branch 2 times, most recently from 04c83d3 to ccab473 Compare May 20, 2019 08:23

smowton reviewed May 20, 2019

View reviewed changes

allredj reviewed May 20, 2019

View reviewed changes

kroening force-pushed the sort_bytecode_info branch from ccab473 to 3b70661 Compare May 20, 2019 11:41

allredj reviewed May 20, 2019

View reviewed changes

kroening force-pushed the sort_bytecode_info branch from 3b70661 to 46daf81 Compare May 20, 2019 16:09

allredj reviewed May 20, 2019

View reviewed changes

kroening force-pushed the sort_bytecode_info branch from 46daf81 to c60a918 Compare May 26, 2019 22:05

allredj reviewed May 26, 2019

View reviewed changes

tautschnig assigned smowton, thk123, NathanJPhillips and peterschrammel May 28, 2019

smowton approved these changes May 28, 2019

View reviewed changes

tautschnig added the Needs rebase label May 28, 2019

tautschnig assigned kroening and unassigned smowton, thk123, NathanJPhillips and peterschrammel May 28, 2019

thk123 reviewed May 28, 2019

View reviewed changes

kroening force-pushed the sort_bytecode_info branch from c60a918 to 7822fac Compare May 28, 2019 12:00

allredj reviewed May 28, 2019

View reviewed changes

kroening force-pushed the sort_bytecode_info branch 2 times, most recently from 5023dd0 to 7cca038 Compare May 29, 2019 13:49

kroening removed the Needs rebase label May 30, 2019

tautschnig added the Needs rebase label May 30, 2019

Daniel Kroening added 3 commits May 30, 2019 10:01

fill in missing bytcode table entries

b107258

use bytecode_info instead of bytecode vector

b149012

The run-time generated bytecode table is replaced by bytecode_info. The linear search for the mnemonic is replaced by an array access.

kroening force-pushed the sort_bytecode_info branch from 7cca038 to b149012 Compare May 30, 2019 09:01

kroening removed the Needs rebase label May 30, 2019

kroening merged commit f117f25 into develop May 30, 2019

kroening deleted the sort_bytecode_info branch May 30, 2019 11:57

allredj reviewed May 30, 2019

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

sort bytecode_info table by bytecode #4670

sort bytecode_info table by bytecode #4670

kroening commented May 19, 2019

allredj left a comment

smowton May 20, 2019

kroening May 20, 2019

smowton May 20, 2019

kroening May 20, 2019

smowton May 20, 2019

kroening May 20, 2019

smowton May 20, 2019

smowton May 20, 2019

smowton May 20, 2019

kroening May 20, 2019

smowton May 20, 2019

kroening May 20, 2019

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment

smowton left a comment

smowton May 28, 2019

kroening May 28, 2019

smowton May 28, 2019

smowton May 28, 2019

thk123 left a comment

thk123 commented May 28, 2019

kroening commented May 28, 2019

thk123 commented May 28, 2019

allredj left a comment

thk123 commented May 29, 2019

tautschnig commented May 30, 2019

allredj left a comment

sort bytecode_info table by bytecode #4670

sort bytecode_info table by bytecode #4670

Conversation

kroening commented May 19, 2019

allredj 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

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

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a 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

thk123 left a comment

Choose a reason for hiding this comment

thk123 commented May 28, 2019

kroening commented May 28, 2019

thk123 commented May 28, 2019

allredj left a comment

Choose a reason for hiding this comment

thk123 commented May 29, 2019

tautschnig commented May 30, 2019

allredj left a comment

Choose a reason for hiding this comment