Java local variable block scoping #392

smowton · 2017-01-04T15:26:26Z

See PR https://github.com/diffblue/cbmc-testgen/pull/35 for full description.

This is the first substantial piece of the local variable scoping work, now that its pre-requisites are all merged. Note that the companion PR against cbmc-testgen is still awaiting review; making this now so this can be reviewed in parallel.

Recommend reviewing commit by commit; the first two are necessary admin, the next two make the substantial changes, and the final one cleans up code style issues.

peterschrammel

Looks good. Do you have tests for this?
Please run cpplint.

peterschrammel · 2017-01-06T17:53:54Z

src/java_bytecode/java_bytecode_convert_method.cpp

+    bool leaf;
+    std::vector<unsigned> branch_addresses;
+    std::vector<block_tree_nodet> branch;
+    block_tree_nodet() : leaf(false) {}


no spaces around ":"

peterschrammel · 2017-01-06T17:56:15Z

src/java_bytecode/java_bytecode_convert_method.cpp

+      if(p<(*findstart) || p>=findlim_block_start_address)
+      {
+        debug() << "Warning: refusing to create lexical block spanning " <<
+          (*findstart) << "-" << findlim_block_start_address <<


align << (more instances)

peterschrammel · 2017-01-06T17:59:02Z

src/java_bytecode/java_bytecode_convert_method.cpp

+  std::advance(branchaddriter, child_offset);
+  auto branchaddrlim=branchaddriter;
+  std::advance(branchaddrlim, nblocks);
+  newnode.branch_addresses.insert(newnode.branch_addresses.begin(),


put params on next line

peterschrammel · 2017-01-06T17:59:46Z

src/java_bytecode/java_bytecode_convert_method.cpp

  {
+    const auto& it=*ait;


const auto &it (more instances)

peterschrammel · 2017-01-06T18:01:12Z

src/java_bytecode/java_bytecode_convert_method.cpp

-      code.add(code_labelt(label(std::to_string(address)), c));
-    else if(c.get_statement()!=ID_skip)
-      code.add(c);
+    if(!start_new_block)


Add a comment to explain what these two cases mean

This will be needed by forthcoming changes that use these types outside convert_instructions.

Previously these were added post-hoc like anonymous locals, but this will be tidier when the forthcoming variable scoping work is added.

These maintain a tree that describes the java bytecode addresses corresponding to different code_blockt instances in the Java program's translated representation. They will be used to create a nested tree of code_blockt instances allowing named program variables to be declared as close to their true live ranges as possible.

smowton · 2017-01-09T10:59:23Z

Pushed further style fixes and rebased. Tests to come shortly...

The block tree maintenance functions introduced in the previous commit are used to add a `code_declt` for each named variable as close to its true scope as possible.

smowton · 2017-01-09T12:30:01Z

Pushed a basic test -- also fixed an unrelated test failure due to mishandling class files without a variable table.

peterschrammel · 2017-01-16T14:00:54Z

src/java_bytecode/java_bytecode_convert_method.cpp

+  code_blockt root_block;
+
+  bool start_new_block=true;
+  for(auto ait=address_map.begin(), aend=address_map.end(); ait!=aend; ++ait)


What is the reason for not using a ranged for here?

peterschrammel · 2017-01-16T14:10:38Z

src/java_bytecode/java_bytecode_convert_method.cpp

+
+\*******************************************************************/
+
+void replace_goto_target(


Please add this utility function as a static method to the class.

peterschrammel · 2017-01-16T14:11:52Z

src/java_bytecode/java_bytecode_convert_method.cpp

+        address_map);
+    }
+  }
+  for(const auto &vlist : variables)


Why do you need two passes here?

See comment in first pass (elaborated slightly in amendment)

peterschrammel · 2017-01-16T14:19:07Z

src/java_bytecode/java_bytecode_convert_method.cpp

+    new_symbol.name=identifier;
+    new_symbol.type=t;
+    new_symbol.base_name=v.name;
+    new_symbol.pretty_name=id2string(identifier).substr(6, std::string::npos);


Maybe add a comment that this removes the java:: prefix

peterschrammel · 2017-01-16T21:35:30Z

Also see comments by @mgudemann in https://github.com/diffblue/cbmc-testgen/pull/35

This simply checks that a scoped block got created at PC index 7 (which will enclose a variable scope, but this is harder to spot with a regex) where previously the variable would have been global.

smowton · 2017-01-17T15:40:37Z

All comments addressed (including Matthias') except where noted

67c80fc Merge pull request diffblue#394 from diffblue/jeannie/LinkedHashMapIterators 6667484 Tests that the iteration order is correct. 38301ea Tests other methods and constructor in LinkedHashMap f795b3d Models other methods in LinkedHashMap. 25773a6 Tests entrySet(), keySet() and values() in LinkedHashMap ee8cfad Models keySet(), entrySet() and values() in LinkedHashMap. 02c8271 Merge pull request diffblue#393 from diffblue/jeannie/UpdateReadMeForSpec 81460d3 Update readme.md to include new style for specs 9efcce3 Merge pull request diffblue#396 from diffblue/antonia/clean-up-for-TG-1081 c902c03 Merge pull request diffblue#397 from diffblue/jeannie/ForgotAppendObjectDocs 772a977 Merge pull request diffblue#390 from diffblue/antonia/enable-fixed-tests 5bef2ff Merge pull request diffblue#398 from diffblue/antonia/ticket-references-bugfix ed1dca2 Merge pull request diffblue#395 from diffblue/allredj/disable-tests-failing-on-tg2717 c07841d Add more tests for String.getBytes(Charset) d568e47 Fix array index bug in String.getBytesUTF_16 2218407 Model String.getBytes(Charset) 9c3a8bc Clarify difference of String.getBytes from JDK cf1c23b Merge the two active scenarios in String.spec dd5d2d9 Remove support_v1 tag from String specs 5f9a7e1 Split String tests into Level 0 and Level 1+ f2877b9 Enable Class test that was blocked by TG-1081 034f3e0 Remove reference to TG-1081 from File model 43afde7 Force static initialiser for File model d95ff9e Remove reference to fixed bug from Date model 0807806 Remove references to fixed bugs from Arrays model cde4085 Remove references to fixed bugs from HashMap model d85fe5b Update RaceTimes references to TG-1404 and TG-1523 0e925e5 Update ticket number in HashMap.spec 03a5186 Enable TG-1404 tests fa051dd Delete ArrayList CustomType test file b0e853b Enable HashMap test previously blocked by TG-1877 44bfe0a Merge pull request diffblue#392 from diffblue/lajw/TG-2389-enable-tests 595dd5d Changes CProver helped methods in HashMap to protected. c52771c Merge pull request diffblue#385 from diffblue/jeannie/UpdateTestRunner de0abdc Enable tests fixed by recent test-gen fixes b64357a Remove ticket numbers from resolved bugfix tests 53eca00 Documents StringBuilder and StringBuffer append(Object) baec23f Merge pull request diffblue#389 from diffblue/antonia/enable-TG-2666-test b2f0258 Enable LinkedList test that was blocked by TG-2666 57e79e5 Add knownbug tests for TG-2717 80fa433 Merge pull request diffblue#387 from diffblue/forejtv/unsupportedcharsetexception 990129c Merge pull request diffblue#391 from diffblue/allredj/disable-html-report 97f32f6 Don't write to the Html report 4cb5996 Merge pull request diffblue#382 from diffblue/antonia/address-ArrayList-todos 6749702 Merge pull request diffblue#386 from diffblue/antonia/gauge-telemetry-off 546dfdc Move legacy style tests into main Gauge step 5be886f Mark UnsupportedCharsetException as untested 1c17838 Add regression test for side effects 8c836ab Add tests for ArrayLists w. (non-default) capacity 34a141d Address bugfix TODOs in ArrayList 563b631 Correct bug description in comment 3e7603d Merge pull request diffblue#383 from diffblue/antonia/reformat-HashSet-tests 5d4e013 [TG-2751] Added UnsupportedCharsetException 11b28fb Reformat HashSet.spec f77c3c4 Rename HashSet_L2.spec to HashSet_L0.spec a16a1e7 Move all HashSet Maven tests into HashSet.spec f21a2da Merge pull request diffblue#376 from diffblue/jeannie/LinkedHashMap 820c5f7 Merge pull request diffblue#380 from diffblue/jeannie/AppendObject af65f4d Tests java.lang.StringBuffer append(Object) a554517 Reformat tests in java.util.StringBuilder dd6d3f6 Models append(Object) for StringBuilder and StringBuffer. 8920399 Tests toString() methods on existing models where possible 647f4fe Tests toString() methods on existing models where possible 978273b Documents and implements toString() methods in existing models. 78020ee Documents java.util.LinkedHashMap fb0cf92 Tests java.util.LinkedHashMap 7a9df4e Models java.util.LinkedHashMap 5a8af60 Marks all methods as notModelled() for java.util.LinkedHashMap 8d6b149 Initial commit for java.util.LinkedHashMap 34b7c54 Merge pull request diffblue#359 from diffblue/forejtv/throwable-no-static e2230de Cleanup of unused (mostly static) variables 255013e Merge pull request diffblue#384 from diffblue/jeannie/DisableBoundedGenericHashMap f374d5f Merge pull request diffblue#381 from diffblue/justin/TG2600-Correction ce6328b Turn off Gauge telemetry on Travis 6ab2864 Updates TestRunner.java to mimic platform parameters. 8ee75a4 Disables a HashMap test that depends on bounded generic type. 3677c3a [TG-2600] correct a mistake in the L1RemoveLast test 4511813 Merge pull request diffblue#378 from diffblue/antonia/LinkedList-first-model 6bda7ea Add tests for LinkedList b5d4cbe Model LinkedList methods specified in TG-2600 aa6e90a Empty models for new classes 3c25555 Copy LinkedList and related classes from jdk 5e4d410 Merge pull request diffblue#373 from diffblue/romain/tests/activate-arrays-hashset-test#TG-1404 a0d9289 Activate some Arrays test 27d06b4 Activate tests for Hashset fixed by TG-1404 224962a Merge pull request diffblue#371 from diffblue/romain/tests/activate-after-fix-1404 ed26b28 Activate level 2 tests fixed by TG-1404 b59c1e9 Relabel known-bug for Level2 HashMap test 5c0041b Activate tests for HashMap.values fixed by TG-1404 2777872 Activate tests for HashMap.entrySet 50d3f2c Activate tests for HashMap.keySet fixed by TG-1404 6146215 Activate ArrayList test fixed by TG-1404 bc09fd7 Merge pull request diffblue#365 from diffblue/jeannie/getTimeZone 29cf7e0 Merge pull request diffblue#372 from diffblue/forejtv/bump-up-gauge-v bdd500a Change Gauge Java Maven Plugin to 0.6.6 190aa18 Tests java.util.TimeZone 170a992 Documents java.util.TimeZone in javadocs 9e52664 Models java.util.TimeZone constructor, getID, setID and getTimeZone. eac578e Tests sun.util.calendar.ZoneInfo b4be728 Documents sun.util.calendar.ZoneInfo in javadocs e5ffa98 Models the sun.util.calendar.ZoneInfo constructor and getTimeZone() 6d704ad Marks methods as notModelled() for sun.util.calendar.ZoneInfo d249adb Marks methods as notModelled() for java.util.TimeZone 7f71d8d Initial commit for sun.util.calendar.ZoneInfo. b53d9c1 Initial commit for java.util.TimeZone 056aad2 Merge pull request diffblue#368 from diffblue/allredj/fix-hashtable-spec 8848414 Merge pull request diffblue#370 from diffblue/allredj/stringbuffer-spec-small-correction 1d947e5 Small correction to StringBuffer spec file 42f1a93 Fix typo in hashtable spec file git-subtree-dir: benchmarks/LIBRARIES/models git-subtree-split: 67c80fcdcf82418b5e7099ae63dec3360b153f90

…-macros-for-exit-codes Use existing macros for exit codes

kroening requested a review from peterschrammel January 5, 2017 10:02

kroening added the Java Front End label Jan 5, 2017

smowton mentioned this pull request Jan 5, 2017

Call destructors on goto out of scope #395

Merged

peterschrammel requested changes Jan 6, 2017

View reviewed changes

smowton force-pushed the local_variable_block_scoping_master branch from eb15505 to 88b3563 Compare January 9, 2017 10:47

smowton added 3 commits January 9, 2017 10:49

Move converted_instructiont and address_mapt to class scope

f72679d

This will be needed by forthcoming changes that use these types outside convert_instructions.

Add named variables to the symtab upon registration

7c201a2

Previously these were added post-hoc like anonymous locals, but this will be tidier when the forthcoming variable scoping work is added.

smowton force-pushed the local_variable_block_scoping_master branch from 88b3563 to 263a5a0 Compare January 9, 2017 10:58

Add scoped mamed variable declarations

49688fa

The block tree maintenance functions introduced in the previous commit are used to add a `code_declt` for each named variable as close to its true scope as possible.

smowton force-pushed the local_variable_block_scoping_master branch from 263a5a0 to 1339dd5 Compare January 9, 2017 12:21

peterschrammel requested changes Jan 16, 2017

View reviewed changes

smowton added 2 commits January 17, 2017 15:39

Style fixes for java_bytecode_convert_method

5e2f632

Add basic test for lexical scope inference

6cc846a

This simply checks that a scoped block got created at PC index 7 (which will enclose a variable scope, but this is harder to spot with a regex) where previously the variable would have been global.

smowton force-pushed the local_variable_block_scoping_master branch from 192dadf to 6cc846a Compare January 17, 2017 15:40

kroening merged commit 0353de5 into diffblue:master Jan 18, 2017

smowton pushed a commit to smowton/cbmc that referenced this pull request May 9, 2018

Merge pull request diffblue#392 from diffblue/owen-jones-diffblue/use…

6171f06

…-macros-for-exit-codes Use existing macros for exit codes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Java local variable block scoping #392

Java local variable block scoping #392

smowton commented Jan 4, 2017

peterschrammel left a comment

peterschrammel Jan 6, 2017

peterschrammel Jan 6, 2017

peterschrammel Jan 6, 2017

peterschrammel Jan 6, 2017

peterschrammel Jan 6, 2017

smowton commented Jan 9, 2017

smowton commented Jan 9, 2017

peterschrammel Jan 16, 2017

peterschrammel Jan 16, 2017

peterschrammel Jan 16, 2017

smowton Jan 17, 2017

peterschrammel Jan 16, 2017

peterschrammel commented Jan 16, 2017

smowton commented Jan 17, 2017


		\*******************************************************************/

		void replace_goto_target(

Java local variable block scoping #392

Java local variable block scoping #392

Conversation

smowton commented Jan 4, 2017

peterschrammel 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

smowton commented Jan 9, 2017

smowton commented Jan 9, 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

peterschrammel commented Jan 16, 2017

smowton commented Jan 17, 2017