Call destructors on goto out of scope #395

smowton · 2017-01-05T13:30:30Z

CBMC already generates dead instructions when an automatic variable leaves scope due to exiting a lexical scope ({} block). However a dead op is not generated when the block is left by a goto instruction. This PR adds support for that, first adding destructors whenever a block is exited, and then restoring simple guarded gotos when possible.

This also adds dead instructions in appropriate places if lexical scope inference is done for Java (for which, see #392), as due to the translation from Java bytecode, goto statements are a normal way to leave a lexical scope in this case.

mgudemann

please also run cpplint

mgudemann · 2017-01-16T17:16:34Z

src/goto-programs/goto_convert.cpp

+{
+  std::map<goto_programt::targett, int> itertoint;
+
+  int i=0;


reduce scope, change to size_t

mgudemann · 2017-01-16T17:23:51Z

src/goto-programs/goto_convert.cpp

+
+\*******************************************************************/
+
+static inline bool is_size_one(const goto_programt &g)


is this optimization necessary? Could this be moved to a class or a util file?

No idea, inherited it from the original code -- suggest asking @kroening about this as he was the original author

mgudemann · 2017-01-16T17:25:20Z

src/goto-programs/goto_convert.cpp

+  if(is_guarded_goto)
+    guarded_gotos.push_back({tmp_v.instructions.begin(),
+                             tmp_w.instructions.begin(),
+                             guard});


mgudemann · 2017-01-16T17:25:50Z

src/goto-programs/goto_convert_exceptions.cpp

@@ -375,22 +375,32 @@ void goto_convertt::unwind_destructor_stack(
  std::size_t final_stack_size,
  goto_programt &dest)
 {
+  unwind_destructor_stack(source_location,final_stack_size,
+                          dest,targets.destructor_stack);


kroening · 2017-01-17T16:17:58Z

May I suggest adding the obvious test?

smowton · 2017-01-17T16:29:45Z

Addressed Matthias' comments

The case where it enters a scope is not handled at present, as I don't know how to phrase that in terms of goto-program decl statements. It's also illegal in C++ if a nontrivial constructor would be needed, and can't be constructed in Java source AFAIK.

Instead of building it in the first pass, make a pessimistic multi-instruction branch and then promote it in the post-pass if no destructors got added.

This checks that (a) the loop iterator 'i' gets killed before function exit and (b) there aren't too may basic blocks (indicated by 'GOTO 10' appearing, which would indicate the second loop's guarded goto statements are being unnecessarily disrupted. (For example, producing 'if(j==5) goto 2; goto end; 2: ...' instead of the simpler 'if(j==5) goto end; ...', which is necessary for the i-loop to accomodate the 'dead i;' statement, but not for the j-loop)

smowton · 2017-01-18T10:25:29Z

Added test (see commit message for details) and rebased. Note the test won't pass until #392 lands as at the moment there are no blocks in Java programs for this code to act upon.

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

Add verbosity level to cmdline.

smowton force-pushed the call_destructors_on_goto_out_of_scope branch 2 times, most recently from c80b1ee to 379b7bc Compare January 5, 2017 16:36

peterschrammel requested a review from mgudemann January 12, 2017 16:13

mgudemann suggested changes Jan 16, 2017

View reviewed changes

smowton force-pushed the call_destructors_on_goto_out_of_scope branch from 379b7bc to f710046 Compare January 17, 2017 15:52

smowton added 3 commits January 18, 2017 10:19

Restore the guarded-goto construct

ea16fd4

Instead of building it in the first pass, make a pessimistic multi-instruction branch and then promote it in the post-pass if no destructors got added.

smowton force-pushed the call_destructors_on_goto_out_of_scope branch from 4970203 to cfbe2ac Compare January 18, 2017 10:25

kroening merged commit eb19783 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#395 from diffblue/add_verbosity_to_cmdline

edf9898

Add verbosity level to cmdline.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Call destructors on goto out of scope #395

Call destructors on goto out of scope #395

smowton commented Jan 5, 2017

mgudemann left a comment

mgudemann Jan 16, 2017

mgudemann Jan 16, 2017

smowton Jan 17, 2017

mgudemann Jan 16, 2017

mgudemann Jan 16, 2017

kroening commented Jan 17, 2017

smowton commented Jan 17, 2017

smowton commented Jan 18, 2017 •

edited

Loading


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

		static inline bool is_size_one(const goto_programt &g)

Call destructors on goto out of scope #395

Call destructors on goto out of scope #395

Conversation

smowton commented Jan 5, 2017

mgudemann left a comment

Choose a reason for hiding this comment

mgudemann Jan 16, 2017

Choose a reason for hiding this comment

mgudemann Jan 16, 2017

Choose a reason for hiding this comment

smowton Jan 17, 2017

Choose a reason for hiding this comment

mgudemann Jan 16, 2017

Choose a reason for hiding this comment

mgudemann Jan 16, 2017

Choose a reason for hiding this comment

kroening commented Jan 17, 2017

smowton commented Jan 17, 2017

smowton commented Jan 18, 2017 • edited Loading

smowton commented Jan 18, 2017 •

edited

Loading