Run remove-virtual-functions on a per-function basis #1717

smowton · 2018-01-09T17:04:13Z

This introduces a mechanism to re-number a single GOTO program, since various parts of the CBMC codebase will assume the globally-unique-location-numbers invariant holds and it's safest to ensure it holds as much of the time as possible, then uses it to move remove-virtual-functions to run as each function is elaborated, rather than all in one go at the end.

tautschnig · 2018-01-09T17:19:29Z

src/goto-programs/goto_functions_template.h

@@ -102,16 +102,23 @@ class goto_functions_templatet
  typedef goto_function_templatet<bodyT> goto_functiont;
  typedef std::map<irep_idt, goto_functiont> function_mapt;
  function_mapt function_map;
+  /// A location number such that unused_location_number - MAX_UINT are all


Is that - a minus (subtraction) or (more likely) indicating a range? Would you mind being clinical here and use a notation that unambiguously states whether that's a (half) open interval?

tautschnig · 2018-01-09T17:25:15Z

src/goto-programs/goto_functions_template.h

+  /// unused. There might still be unused numbers below this.
+  /// If numbering a new function or renumbering a function, starting from this
+  /// number is safe.
+  unsigned unused_location_number;


I don't think this should be public?

tautschnig · 2018-01-09T17:26:26Z

src/goto-programs/goto_model.h

@@ -67,4 +67,28 @@ class goto_modelt
  void unload(const irep_idt &name) { goto_functions.unload(name); }
 };

+/// Interface for renumbering the locations in a goto_programt
+class goto_program_location_numberingt


What exactly is the value of this?

tautschnig · 2018-01-09T17:27:16Z

src/goto-programs/goto_model.h

@@ -77,7 +77,7 @@ class goto_program_location_numberingt
  /// \param goto_model: will be used to ensure unique numbering of
  ///   goto programs, specifically incrementing its unused_location_number
  ///   member each time a program is re-numbered.
-  goto_program_location_numberingt(goto_modelt &goto_model):
+  explicit goto_program_location_numberingt(goto_modelt &goto_model):


Wrong commit. (Though in my earlier comment it doubted the overall value of this interface as well.)

tautschnig · 2018-01-09T17:57:40Z

src/goto-programs/lazy_goto_model.cpp

@@ -23,14 +23,18 @@ lazy_goto_modelt::lazy_goto_modelt(
  post_process_functionst post_process_functions,
  message_handlert &message_handler)
  : goto_model(new goto_modelt()),
+    goto_model_numbering_interface(*goto_model),


Isn't this just a container for goto_modelt? I find this pretty weird.

smowton · 2018-01-10T15:12:48Z

@tautschnig all comments addressed, except for the interface, whose purpose is to permit GOTO program renumbering (a non-const operation on goto_functionst) without providing a non-const reference to the entire function map, which should explicitly not be perturbed while post-processing a single function in isolation.

Alternatively solutions:

Rewrite location_number as union { struct { uint32_t function_number; uint32_t instruction_number; }; uint64_t location_number; }, thus permitting GOTO program re-numbering without coordinating via goto_functionst again (good thing to do, more churny)
Make unused_location_number mutable, so a const ref to goto_functionst suffices (don't like it; mutable is rather a blunt instrument compared to supplying a specific interface that exposes the required feature)
Maintain a back-pointer from goto_programt to the function map it is in (error-prone; can a particular program (perhaps briefly) be in more than one map, for example?)

smowton · 2018-01-10T16:25:11Z

@NathanJPhillips: please review (can't tag you due to your lack of write access to cbmc)

tautschnig · 2018-01-10T17:13:28Z

[...] purpose is to permit GOTO program renumbering (a non-const operation on goto_functionst) without providing a non-const reference to the entire function map, which should explicitly not be perturbed while post-processing a single function in isolation.

This sounds good to me, and certainly I wouldn't have complained at all had I read this comment in the source code. Would you mind adding it? ("Interface for renumbering the locations in a goto_programt" lacks the "why" that the above explanation does provide.)

tautschnig

Approving with the assumption that comments will be clarified (well, indeed they might just need to be shifted from the point-of-use to the definition).

smowton · 2018-01-10T18:12:39Z

Added a comment as requested.

peterschrammel · 2018-01-10T20:35:33Z

src/goto-programs/goto_model.h

+/// not be altered.
+class goto_program_location_numberingt
+{
+  goto_modelt &goto_model;


Nit pick: prefer protected members at bottom (as typical in the codebase).

peterschrammel · 2018-01-10T20:36:37Z

src/goto-programs/goto_program_template.h

@@ -512,7 +514,10 @@ class goto_program_templatet
  void compute_location_numbers(unsigned &nr)
  {
    for(auto &i : instructions)
+    {
+      INVARIANT(nr != UINT_MAX, "Too many location numbers assigned");


use std::numeric_limits::max

peterschrammel · 2018-01-10T20:49:37Z

unit/testing-utils/load_java_class.cpp

-    [] (goto_functionst::goto_functiont &function, symbol_tablet &symbol_table)
+    [] (goto_functionst::goto_functiont &function,
+        symbol_tablet &symbol_table,
+        goto_program_location_numberingt &location_numbering)


It feels quite odd nonetheless that we introduced goto_modelt as a container for goto_functions and symbol_table to simplify our interfaces and now here we are creating interfaces that require even more parameters. What about wrapping a goto_function and its goto_model into a goto_function_modelt? Then you can call renumber() on the goto_function_model without exposing the underlying goto_model.

smowton · 2018-01-11T11:35:23Z

@peterschrammel you're quite right, I created goto_model_functiont which provides similar functionality but is much nicer. @tautschnig might want to look again since this has changed a bit.

tautschnig · 2018-01-11T11:41:49Z

src/goto-programs/goto_model.h

+
+  /// Re-number our goto_function. After this method returns all instructions'
+  /// location numbers may have changed, but will be globally unique and in
+  /// program order within the program.


Nit pick: "program order" may be ambiguous (or possibly wrong) here; the numbers are strictly increasing as they are laid out in the underlying storage (source text or a list of statements), which need not coincide with the order of execution.

This is the wording used elsewhere in goto-programs/goto_program_template.h so I'll keep this as-is

smowton · 2018-01-11T12:11:35Z

Test-gen bump here: https://github.com/diffblue/test-gen/pull/1361

goto_programt::compute_location_numbers numbers it from zero, but of course these numbers may clash with other programs; this adds the ability to renumber a program, at the cost of wasting some "address" space.

This means lazy loading drivers do not need to understand virtual function calls, as they have already been converted into explicit dispatch tables.

peterschrammel

This looks more elegant now.

d190fd8 Merge remote-tracking branch 'upstream/develop' into pull-support-20180112 5bd5962 Merge pull request diffblue#1667 from romainbrenguier/feature/type_cast 8ecb55a Merge pull request diffblue#1717 from smowton/smowton/feature/remove_virtual_functions_per_function 0d7310a Merge pull request diffblue#1691 from romainbrenguier/bugfix/getClass#TG-1245 2064849 Use type_checked_cast in boolbv_width c5fc351 Validate data in pointer_typet in to_pointer_typet 35905c6 Add can_cast_type, validate_type for pointer_typet b72bacf Define type_try_dynamic_cast and type_checked_cast 23c3561 Unit test for string symbol resolution c13e602 Adding only needed equations in symbol resolution ae4deff Debug information for string equations 912828d JBMC: Run remove-virtual-functions as each function is converted a711c64 Introduce mechanism for renumbering an individual GOTO program e308a32 Merge pull request diffblue#1679 from NlightNFotis/nondet_extra_test e6ceb91 Merge pull request diffblue#1724 from tautschnig/fix-visitor ea74bed Add extra test for nondet-static flag and arrays 4f74896 Use irept API, not implementation-level API c55b4a5 Merge pull request diffblue#1682 from martin-cs/fix/dependence-graph-namespace-lifespan 1a2c14b Merge pull request diffblue#1722 from diffblue/unsafe_type_constructors 957a568 Merge pull request diffblue#1677 from NlightNFotis/pb4_develop 9c5add4 remove deprecated constructors for three bitvector types c96e02a no longer use deprecated constructors for some bitvector types 954060e Add unit test for has_subtype 3dd3877 Refactor has_char_pointer_subtype with has_subtype 4699c13 Extend symbol resolution to string_typet 74144fc Handle if_exprt in add_axioms_for_string_literal c6c1b3f Add an optional guard to add_axioms_for_constant 933d635 Merge pull request diffblue#1716 from mgudemann/fix/null_check_for_java_instanceof 1659314 Merge pull request diffblue#1715 from smowton/smowton/cleanup/jbmc_unused_passes 9c457b7 Add regression test for null instanceof. 2080cd3 Complete instanceof for Java. d4300d0 Merge pull request diffblue#1697 from diffblue/nondet_symbol_exprt 1c68dd4 Merge pull request diffblue#1714 from tautschnig/c-library-strcat 44b5bae Merge pull request diffblue#1698 from thomasspriggs/tg1633 c4304ba JBMC: Remove C-only passes bb8cfaa C library: Check upper bounds in memset, memcpy, memmove 7d4984f C library: Implement strcat, strncat 2a5cea2 This introduces nondet_symbol_exprt, which is generated by symbolic execution in response to side_effect_expr_nondett 85193a0 Merge pull request diffblue#1694 from NathanJPhillips/feature/add-raw-lhs-to-trace d9122dc Merge pull request diffblue#1710 from NathanJPhillips/feature/remove_instanceof_per_function 092df69 Switch from custom file / path routines to Boost-filesystem c8821b2 Allow to remove instanceof when remove exceptions 94b7658 Don't pass iterators into function calls a9c4e4f Added regression tests 76318ce Protect extended trace behind a command line option 69b0ff1 Added base_name in comments for all symbols e86080a Add raw LHS irep field to trace output ddd1b7a Add remove_instanceof overload to remove from a particular instruction 1c227b7 Merge pull request diffblue#1660 from smowton/smowton/fix/lazy_methods_array_parameters ae89c94 Lazy loading: assume concrete generic parameter types are needed 80eb6a6 TG-1877: Include array pointer types in needed classes 1053e5f Fix for [TG-1633] Inner generic types have incorrect type identifier e2cda1a Merge pull request diffblue#1704 from tautschnig/fix-copy-paste ef4a65e Fix op1/op0 copy&paste typo 21ea31f Merge pull request diffblue#1702 from peterschrammel/goto-diff-java c4bc953 Merge pull request diffblue#1701 from peterschrammel/allow-instrument-jdk 2811363 Java regression test for goto-diff 43d2e09 Also reset fresh temporary symbol counter 9ef28f4 Compare relative goto target offsets eaf3a7d Get source location from symbol table ab59659 Allow instrumentation of java.* and org.cprover.* 6fbd59c Merge pull request diffblue#1631 from tautschnig/fix-pointer-minus 7c04b5c Merge pull request diffblue#1699 from NathanJPhillips/feature/reset-main-in-tests 5e0f186 Pointer difference over void* is difference over char* faf8f00 Merge commit 'a83b52cddbed22304372c276512c63701eb3aedb' into pull-support-20180104 8236db4 Merge pull request diffblue#1419 from peterschrammel/refactor/cover-instrument a580e27 Merge pull request diffblue#1689 from smowton/smowton/feature/get_this 591511a Allow callers of load_java_class to pass the name of the main function 1b86b27 Merge pull request diffblue#1687 from smowton/smowton/feature/class-hierarchy-dot fd2bf6a Merge pull request diffblue#1688 from smowton/smowton/feature/parameter_indices f570ce5 Merge pull request diffblue#1696 from smowton/smowton/fix/identical_struct_equality 61b0d6d Merge pull request diffblue#1666 from mgudemann/bugfix/removed_required_virtual_calls 3365054 Add regression test 2b6dc8b Resolve concrete function call if no implementation is found 3f1fd64 Add code_typet::get_parameter_indices 42cf61a Fix testing for empty line in test desc file 2090000 Fix missing newline at end of desc file e448d5f Fix unsatisfiable test line f7f033d String smoke tests: ensure no type mismatches are seen b627c3d Replace unsound struct-cast simplification 8fa42b3 Class hierarchy: add DOT output, unit tests 04f2faf Mark GOTO instructions with unresolved virtual calls aac181f Pass command line options via optionst b6fa3e8 Factorize source location initialization 8da5395 Document cover functions a7f0c3d Introduce cover instrumenter 873627a Split cover into several files 0fc08f3 Replace cover-function-only by cover-include-pattern 1f2102c Add code_typet::get_this 2801f0f Avoid crashing when --dependence-graph is used by correcting namespace scoping. acac776 Add a test for the same-named static functions crashing dependence graph in the goto-analyser 05f46a9 Fix the problem where two static functions with the same name would cause the dependency graph to fail. git-subtree-dir: cbmc git-subtree-split: d190fd8

smowton requested review from cesaro, kroening, mgudemann, peterschrammel and tautschnig as code owners January 9, 2018 17:04

smowton force-pushed the smowton/feature/remove_virtual_functions_per_function branch from 3797122 to 8c5968c Compare January 9, 2018 17:14

tautschnig reviewed Jan 9, 2018

View reviewed changes

smowton force-pushed the smowton/feature/remove_virtual_functions_per_function branch 2 times, most recently from bd3b228 to ae9602e Compare January 10, 2018 14:45

smowton force-pushed the smowton/feature/remove_virtual_functions_per_function branch from ae9602e to 71021f2 Compare January 10, 2018 15:19

tautschnig approved these changes Jan 10, 2018

View reviewed changes

tautschnig assigned cesaro, mgudemann, peterschrammel and smowton Jan 10, 2018

smowton force-pushed the smowton/feature/remove_virtual_functions_per_function branch from 71021f2 to 68a8453 Compare January 10, 2018 18:08

smowton requested a review from Degiorgio January 10, 2018 18:13

peterschrammel reviewed Jan 10, 2018

View reviewed changes

smowton force-pushed the smowton/feature/remove_virtual_functions_per_function branch 2 times, most recently from 4cf4752 to a37bfdd Compare January 11, 2018 11:32

tautschnig reviewed Jan 11, 2018

View reviewed changes

smowton force-pushed the smowton/feature/remove_virtual_functions_per_function branch from a37bfdd to 74d0a5a Compare January 11, 2018 16:03

smowton added 2 commits January 11, 2018 16:05

Introduce mechanism for renumbering an individual GOTO program

a711c64

goto_programt::compute_location_numbers numbers it from zero, but of course these numbers may clash with other programs; this adds the ability to renumber a program, at the cost of wasting some "address" space.

JBMC: Run remove-virtual-functions as each function is converted

912828d

This means lazy loading drivers do not need to understand virtual function calls, as they have already been converted into explicit dispatch tables.

smowton force-pushed the smowton/feature/remove_virtual_functions_per_function branch from 74d0a5a to 912828d Compare January 11, 2018 16:05

peterschrammel approved these changes Jan 12, 2018

View reviewed changes

smowton merged commit 8ecb55a into diffblue:develop Jan 12, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Run remove-virtual-functions on a per-function basis #1717

Run remove-virtual-functions on a per-function basis #1717

smowton commented Jan 9, 2018 •

edited

Loading

tautschnig Jan 9, 2018

tautschnig Jan 9, 2018

tautschnig Jan 9, 2018

tautschnig Jan 9, 2018

tautschnig Jan 9, 2018

smowton commented Jan 10, 2018

smowton commented Jan 10, 2018

tautschnig commented Jan 10, 2018

tautschnig left a comment

smowton commented Jan 10, 2018

peterschrammel Jan 10, 2018

peterschrammel Jan 10, 2018

peterschrammel Jan 10, 2018

smowton commented Jan 11, 2018

tautschnig Jan 11, 2018

smowton Jan 11, 2018 •

edited

Loading

smowton commented Jan 11, 2018

peterschrammel left a comment

Run remove-virtual-functions on a per-function basis #1717

Run remove-virtual-functions on a per-function basis #1717

Conversation

smowton commented Jan 9, 2018 • edited Loading

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 10, 2018

smowton commented Jan 10, 2018

tautschnig commented Jan 10, 2018

tautschnig left a comment

Choose a reason for hiding this comment

smowton commented Jan 10, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton commented Jan 11, 2018

Choose a reason for hiding this comment

smowton Jan 11, 2018 • edited Loading

Choose a reason for hiding this comment

smowton commented Jan 11, 2018

peterschrammel left a comment

Choose a reason for hiding this comment

smowton commented Jan 9, 2018 •

edited

Loading

smowton Jan 11, 2018 •

edited

Loading