Change `code_typet` to `java_method_typet` in JBMC #2661

jeannielynnmoulton · 2018-08-01T17:27:23Z

In a previous PR, a class java_method_typet was created to store exceptions. This changes all code_typets to java_method_typets so there are no clashes or conversion problems.

...

test-gen bump: https://github.com/diffblue/test-gen/pull/2120

mgudemann · 2018-08-02T05:54:44Z

@jeannielynnmoulton there's an odd compilation failure https://travis-ci.org/diffblue/cbmc/jobs/410917905#L8158

mgudemann

I think the change looks good. My question is whether we can be sure that all casts actually return a java_method_typet. Is there a check that the ID_C_java_method_type comment is set? Is this required?

jeannielynnmoulton · 2018-08-02T11:30:48Z

@mgu I've address the compile issue - it was an incorrect import in the unit tests. I seem to only be able to set the ID in the non const cast, which I guess it expected. I've added a unit test as well. If this is not what you meant, let's chat on slack.

allredj

Passed Diffblue compatibility checks (cbmc commit: 6b85d77).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80743015

mgudemann

LGTM

allredj

Passed Diffblue compatibility checks (cbmc commit: b45fe75).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80756580

thk123

It is a improvement, but would love to be able to get rid of the add_exception method and instead construct it perfectly up front. Blocking changes marked with 🚫

thk123 · 2018-08-02T15:10:23Z

jbmc/src/java_bytecode/java_types.h

+  }
+
+  /// \deprecated
+  DEPRECATED("Use the two argument constructor instead")


Why add a deprecated method?

Adding improvements to constructors. Having a no-constructor can be handy it seems, and it is used in at least one place, so I'm modifying it to use one of the two argument constructors with empty values so it does not use the deprecated code_typet constructor.

Honestly this feels worse - as it hides the fact we've created an invalid java_method_typet without even the compiler warning. When you've got a min lets discuss where this is being used and whether we can do any better.

Removed and replaced where empty constructor would have been used with java_method_typet({}, empty_typet())

thk123 · 2018-08-02T16:00:28Z

jbmc/src/java_bytecode/java_types.h

@@ -268,6 +298,7 @@ inline const java_method_typet &to_java_method_type(const typet &type)
 inline java_method_typet &to_java_method_type(typet &type)
 {
  PRECONDITION(type.id() == ID_code);
+  type.set(ID_C_java_method_type, true);


🚫 Do this in the constructor only and check it here. That will catch any cases where something is expecting a java_method_typet but actually got a regular old code_typet

Best: introduce:

template <> inline bool can_cast_type<java_method_typet>(const typet &type) { return type.id() == ID_code && type.get_bool(ID_C_java_method_type); }

Above the two to_java_method_type and use it in the pre-condition of both.

thk123 · 2018-08-02T16:01:39Z

jbmc/unit/java-testing-utils/require_type.cpp

-/// \return The cast version of the type code_type
-code_typet require_type::require_code(const typet &type)
+/// \return The cast version of the type method_type
+java_method_typet require_type::require_code(const typet &type)


🚫 I think it would be best to keep this and have another (require_java_method), or update the name of the method to be require_java_method

thk123 · 2018-08-02T16:02:02Z

jbmc/unit/java-testing-utils/require_type.cpp

-/// \return The type cast to a code_typet
-code_typet
+/// \return The type cast to a java_method_typet
+java_method_typet


🚫 I think it would be best to keep this and have another (require_java_method), or update the name of the method to be require_java_method

thk123 · 2018-08-02T16:02:44Z

jbmc/unit/java-testing-utils/require_type.cpp

 }

 /// Verify that a function has a parameter of a specific name.
 /// \param function_type: The type of the function
 /// \param param_name: The name of the parameter
 /// \return: A reference to the parameter structure corresponding to this
 /// parameter name.
-code_typet::parametert require_type::require_parameter(
-  const code_typet &function_type,
+java_method_typet::parametert require_type::require_parameter(


I probably wouldn't change this at all - it isn't specific to java methods to have parameters.

thk123 · 2018-08-02T16:04:54Z

jbmc/unit/java-testing-utils/require_type.cpp

-/// \return The cast version of the type code_type
-code_typet require_type::require_code(const typet &type)
+/// \return The cast version of the type method_type
+java_method_typet require_type::require_code(const typet &type)
 {
  REQUIRE(type.id() == ID_code);


If you introduce the following in java_types:

template <> inline bool can_cast_type<java_method_typet>(const typet &type) { return type.id() == ID_code && type.get_bool(ID_C_java_method_type); }

Then you can use that here instead of checking the id directly (and will allow you to also check the bool. This only applies if you end up with a require_java_type method.

thk123 · 2018-08-02T16:07:35Z

jbmc/unit/java_bytecode/java_types/java_method_type.cpp

+    {
+      THEN("It should have id code_typet and java_method_typet")
+      {
+        java_method_typet method_type = to_java_method_type(code_type);


This test will fail when you introduce the change to not change this on to_method_type. I don't think you need this test at all. A more useful test might be in one of the java_bytecode unit tests to check that you get a java_method_typet for the method symbols.

thk123 · 2018-08-02T16:09:07Z

jbmc/src/java_bytecode/java_types.h

+  /// Constructs a new code type, i.e. method type
+  /// \param _parameters: the vector of method parameters
+  /// \param _return_type: the return type
+  java_method_typet(parameterst &&_parameters, const typet &_return_type)


💡 One thing that would make this really swell is if the constructor also took the exceptions it might throw (and then ditch add_throws_exceptions). Not sure if feasible, but if you did this you would be able to guarantee that all java methods are in the correct state of having their exceptions list.

This does sound swell, but is not immediately obvious to me how to do this, not even sure that it is possible, so I've not done it here.

martin-cs · 2018-08-02T18:46:41Z

[ Caveat : I don't follow the JVM front-end / JBMC ]

This could be quite a large change. That doesn't mean it is wrong or right; just, you know, be careful out there ;-)

jeannielynnmoulton · 2018-08-06T15:46:15Z

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -36,7 +36,7 @@ static void create_initialize(symbol_table_baset &symbol_table)
  initialize.base_name=INITIALIZE_FUNCTION;
  initialize.mode=ID_java;

-  initialize.type = code_typet({}, empty_typet());
+  initialize.type = java_method_typet({}, empty_typet());


Empty constructor here.

jeannielynnmoulton · 2018-08-06T15:46:30Z

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -715,7 +715,7 @@ bool generate_java_start_function(
  symbolt new_symbol;

  new_symbol.name=goto_functionst::entry_point();
-  new_symbol.type = code_typet({}, empty_typet());
+  new_symbol.type = java_method_typet({}, empty_typet());


Empty constructor here

Oh OK, my mistake. These are all OK since they relate to a parameters void returning method (so makes sense they have no parameters and no return).

I guess I would do as you've done here and explicitly call with those two arguments rather than providing the default constructor shortcut. (i.e. get rid of this I think unused constructor https://github.com/diffblue/cbmc/pull/2661/files#diff-2d3ac05ff88eab2a38135f7ff4ef5ad1R251)

That sounds like a plan. (BTW, it wasn't my intention to passive aggressively tag these, I was doing it for myself so that we could discuss tomorrow :) )

jeannielynnmoulton · 2018-08-06T15:48:30Z

jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp

@@ -64,7 +64,10 @@ SCENARIO("string_identifiers_resolution_from_equations",

    WHEN("There is a function call")
    {
-      symbol_exprt fun_sym("f", code_typet());
+      java_method_typet::parameterst parameters;


Empty constructor was used here

allredj

This PR failed Diffblue compatibility checks (cbmc commit: f4636ee).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/81047197
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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).

allredj

Passed Diffblue compatibility checks (cbmc commit: df47bd6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/81048598

allredj

Passed Diffblue compatibility checks (cbmc commit: 030c3cd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/81119605

thk123

Constructors all look good - just one missed blocking comment from last review I think

thk123 · 2018-08-08T09:06:04Z

jbmc/unit/java-testing-utils/require_type.cpp

 /// Verify that a function has a parameter of a specific name.
 /// \param function_type: The type of the function
 /// \param param_name: The name of the parameter
 /// \return: A reference to the parameter structure corresponding to this
 /// parameter name.
 code_typet::parametert require_type::require_parameter(
-  const code_typet &function_type,
+  const java_method_typet &function_type,


I thought we'd agreed to leave this taking a code_typet? #2661 (comment)

Missed it, sorry. Fixed.

thk123 · 2018-08-08T13:58:54Z

jbmc/unit/java-testing-utils/require_type.h


-code_typet::parametert
+java_method_typet::parametert


Sorry to be a pain - this wants to be left as code_typet - but I trust you to apply this!

This is for variables that have been changed to java_method_typet from code_typet

Also removes an irrelevant unit test due to this change.

4f5e148 Merge pull request diffblue#2713 from thk123/dump/expr2c-configuration 01b7418 Merge pull request diffblue#2710 from thomasspriggs/tas/struct_component b763877 Merge pull request diffblue#2737 from diffblue/remove-appveyor 9c3fd45 Add AWS CodeBuild badges 4261fd8 Remove appveyor badge fe23db7 Remove appveyor.yml 21857a7 Add support for getting components by name to `struct_exprt` 05993f4 Merge pull request diffblue#2727 from tautschnig/fptr-debug 0ecd008 Merge pull request diffblue#2701 from antlechner/antonia/enum-constants 159bf15 Merge pull request diffblue#2205 from diffblue/rename_symbol_type 5ca6cd2 Restrict new clinit_wrapper calls to enum types 6e04213 Reformatting the structs to aid readability 0cfacb8 Add type2c conversion for specifying a type name c3fef70 Add a clean configuration for expr2c 3a40db1 Make expr2ct configurable in a number of ways 097cf71 Merge pull request diffblue#2731 from diffblue/increase-version 170c1ea Merge pull request diffblue#2730 from diffblue/parent-child-invariant c9e46ae Temporarily remove new UNREACHABLE statements 03e3877 Add tests for nondet initialization of enums 3e32140 CI lazy methods: load clinit for all param types 5542c54 Move nondet enum initialization to new function 6ecf4f9 Nondet-init enums by assigning them to a constant 6c84caa Refactor logic for generating a nondet int 07d1e44 Always run clinit_wrapper before nondet object init 3be826f Add some documentation to java_object_factory 5e80310 add invariant on parent-child class relationship 2cf1931 Merge pull request diffblue#2661 from jeannielynnmoulton/jeannie/JavaMethodType c6acc9c increased version number in preparation for release 5.10 0ee4178 Merge pull request diffblue#2729 from tautschnig/add-sub-conflict f5aff56 Merge pull request diffblue#2705 from danpoe/feature/replace-function-calls 89048e6 Function-pointer remvoval: print human-friendly debug messages 1fc3118 Use pointer difference type when adding to pointer 072b592 Merge pull request diffblue#2726 from tautschnig/java-loc 4dca215 Goto program should not use java_method_typet 273fff4 Add can_cast_type and precondition. 6cb7e5d Reinstate require_code and add require_java_method 78f7cb7 Refactor constructors for java_method_typet 6cefc61 Unit tests conversion from code_typet to java_method_typet c3b8b5a Update tag in to_java_method_type 972315a Update docs on java_method_typet constructor 211931c Add tag for java_method_type 551df9c Update unit tests to use java_method_typet da18c9f Change variables named code_type to method_type f1bd41e Change code_typet to java_method_typet in jbmc be3c4c6 Merge pull request diffblue#2430 from tautschnig/vs-function-id 03fa885 Replace function calls c4d79ab Java string preprocessing: use provided source location fb0c552 Java string preprocessing: use and document parameter function_id c31edca Merge pull request diffblue#2725 from tautschnig/replace-symbolt-code-type 2c1fc06 Merge pull request diffblue#2721 from tautschnig/replace_symbol-cleanup2 8211a78 Merge pull request diffblue#2722 from tautschnig/cleanup-valuest 30bc071 Add "// empty last line" to options list in goto_instrument_parse_options.h 8c8801c List source files in goto-programs/Makefile in lexicographic order 40d28ae replace_symbolt: report replacements in code_typet::return_type 4b9df3b Revert "Ignore return value" e39ea2e Merge pull request diffblue#2683 from karkhaz/kk-continue-unsafe 424ab4f --stop-on-fail now stops on failed path 545bff8 Add clear() to path exploration worklist 95d8d0f Generalise option setting from strategy unit tests e85fb77 Cleanup constant_propagator_domaint::valuest 18d08bf Merge pull request diffblue#2719 from tautschnig/quiet-unit-tests 30d557a Constant propagation: Check type consistency before adding to replacement map a5ce621 Make unit tests quiet 61b3086 Merge pull request diffblue#2468 from tautschnig/vs-names 7bfd36b Merge pull request diffblue#2714 from diffblue/msvc-asm 3785941 Remove names of unused parameters af79cb9 add support for Visual Studio style inline assembler 254b4d4 Merge pull request diffblue#2642 from diffblue/remove_asm_fix 26009a3 remove_asm now guarantees that functions called exist 9c10f38 Merge pull request diffblue#2716 from tautschnig/fix-buildspec c3b2beb Merge pull request diffblue#2635 from qaphla/move_is_lvalue e247a29 CodeBuild: Remove empty artifact stanza 756018d Merge pull request diffblue#2709 from owen-jones-diffblue/doc/how-to-run-tests bba5dea Merge pull request diffblue#2699 from diffblue/goto-cc-clang 355fbd2 avoid assert() 6178908 bump goto binary version f93deec type symbols now use ID_symbol_type 22b755a Merge pull request diffblue#2711 from diffblue/mode-gcc-asm-functions cf75535 Merge pull request diffblue#2702 from owen-jones-diffblue/doc/minor-fixes-to-cprover-developer-documentation 5c06786 set mode for functions added by remove_asm ef53b65 Update description of regression test framework 312ca1d Add section to documentation about running tests d7ddf59 Merge pull request diffblue#2700 from romainbrenguier/clean-up/side-effect-location 119e88b Pass location around for nondet initialization 50660db Specify source location for nondet expressions d1f2ad9 Replace -> with → e448db6 Merge pull request diffblue#2708 from owen-jones-diffblue/coding-standard-class-comments 519370d State that identifiers should be good 30d29b9 Replace unicode arrows → with ascii ones -> 611374f Document classes and member variables unless obvious adb7ef0 Minor fixes to documentation outline fd4f563 Add side_effect_exprt constructor with location 98657d8 Merge pull request diffblue#2668 from diffblue/expose_remove_preconditions 6a36fa4 Merge pull request diffblue#2615 from owen-jones-diffblue/doc/cbmc-developer-guide 61a8c30 Merge pull request diffblue#2666 from NlightNFotis/invariant_changes c0bcce7 use clang as native compiler for goto-clang 1f19e23 goto-cc: use result of our native compiler detection d9d9e2a Merge pull request diffblue#2692 from diffblue/follow-tags f94d5e2 follow union, struct and enum tags 99e33bd fix typo in comments for struct_tag_typet 1f53246 expose remove_preconditions f212505 Avoids using expr.op0 when type is known 7b36ca2 Moves is_lvalue to expr_util.c 4782b48 Fix invariant regression tests efb1c40 Refactor invariant_failedt definition. 515f050 Pass the condition to the invariant_failedt constructor. bf6dd9e Added extra use-case hints to the already present invariant definitions. 612b4f8 Address review comments 7233f92 Rearrange everything into separate pages 1cb3cdd Move other tools into a separate file 82eefb7 Fix links between files d9e690b Move folder walkthrough to a separate file 2939db4 Address review comments 8d5cbcb Create CBMC developer guide documentation git-subtree-dir: cbmc git-subtree-split: 4f5e148

jeannielynnmoulton requested review from cesaro, cristina-david, mgudemann, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners August 1, 2018 17:27

mgudemann reviewed Aug 2, 2018

View reviewed changes

jeannielynnmoulton force-pushed the jeannie/JavaMethodType branch from e304e68 to 6b85d77 Compare August 2, 2018 11:29

allredj reviewed Aug 2, 2018

View reviewed changes

mgudemann approved these changes Aug 2, 2018

View reviewed changes

jeannielynnmoulton mentioned this pull request Aug 2, 2018

[TG-4345] Parse thrown exceptions in java #2607

Merged

jeannielynnmoulton force-pushed the jeannie/JavaMethodType branch from 6b85d77 to b45fe75 Compare August 2, 2018 13:27

allredj reviewed Aug 2, 2018

View reviewed changes

thk123 suggested changes Aug 2, 2018

View reviewed changes

jeannielynnmoulton force-pushed the jeannie/JavaMethodType branch 2 times, most recently from f4636ee to df47bd6 Compare August 6, 2018 15:26

jeannielynnmoulton requested a review from thk123 August 6, 2018 15:27

jeannielynnmoulton commented Aug 6, 2018

View reviewed changes

allredj reviewed Aug 6, 2018

View reviewed changes

jeannielynnmoulton force-pushed the jeannie/JavaMethodType branch from df47bd6 to 030c3cd Compare August 7, 2018 08:45

allredj reviewed Aug 7, 2018

View reviewed changes

jeannielynnmoulton force-pushed the jeannie/JavaMethodType branch from 030c3cd to 22d200f Compare August 7, 2018 16:14

jeannielynnmoulton force-pushed the jeannie/JavaMethodType branch from 22d200f to ac38580 Compare August 7, 2018 16:29

jeannielynnmoulton requested review from thk123 and removed request for thk123 August 7, 2018 16:31

thk123 reviewed Aug 8, 2018

View reviewed changes

jeannielynnmoulton force-pushed the jeannie/JavaMethodType branch 3 times, most recently from a088d3b to 26ef690 Compare August 8, 2018 10:58

jeannielynnmoulton requested a review from thk123 August 8, 2018 12:51

thk123 approved these changes Aug 8, 2018

View reviewed changes

jeannielynnmoulton added the work in progress label Aug 13, 2018

jeannielynnmoulton force-pushed the jeannie/JavaMethodType branch from 26ef690 to 3349d5e Compare August 13, 2018 10:05

jeannielynnmoulton removed the work in progress label Aug 13, 2018

jeannielynnmoulton force-pushed the jeannie/JavaMethodType branch from 3349d5e to 468b6ce Compare August 13, 2018 11:06

jeannielynnmoulton added 11 commits August 13, 2018 16:08

Change code_typet to java_method_typet in jbmc

f1bd41e

Change variables named code_type to method_type

da18c9f

This is for variables that have been changed to java_method_typet from code_typet

Update unit tests to use java_method_typet

551df9c

Add tag for java_method_type

211931c

Update docs on java_method_typet constructor

972315a

Update tag in to_java_method_type

c3b8b5a

Unit tests conversion from code_typet to java_method_typet

6cefc61

Refactor constructors for java_method_typet

78f7cb7

Reinstate require_code and add require_java_method

6cb7e5d

Add can_cast_type and precondition.

273fff4

Also removes an irrelevant unit test due to this change.

Goto program should not use java_method_typet

4dca215

jeannielynnmoulton force-pushed the jeannie/JavaMethodType branch from 468b6ce to 4dca215 Compare August 13, 2018 15:08

jeannielynnmoulton merged commit 2cf1931 into diffblue:develop Aug 13, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Change `code_typet` to `java_method_typet` in JBMC #2661

Change `code_typet` to `java_method_typet` in JBMC #2661

jeannielynnmoulton commented Aug 1, 2018 •

edited

Loading

mgudemann commented Aug 2, 2018

mgudemann left a comment

jeannielynnmoulton commented Aug 2, 2018

allredj left a comment

mgudemann left a comment

allredj left a comment

thk123 left a comment

thk123 Aug 2, 2018

jeannielynnmoulton Aug 6, 2018

thk123 Aug 6, 2018

jeannielynnmoulton Aug 8, 2018

thk123 Aug 2, 2018

thk123 Aug 2, 2018

thk123 Aug 2, 2018

thk123 Aug 2, 2018

thk123 Aug 2, 2018

thk123 Aug 2, 2018

thk123 Aug 2, 2018

thk123 Aug 2, 2018

jeannielynnmoulton Aug 6, 2018 •

edited

Loading

martin-cs commented Aug 2, 2018

jeannielynnmoulton Aug 6, 2018

jeannielynnmoulton Aug 6, 2018

thk123 Aug 6, 2018

jeannielynnmoulton Aug 6, 2018

jeannielynnmoulton Aug 6, 2018

allredj left a comment

allredj left a comment

allredj left a comment

thk123 left a comment

thk123 Aug 8, 2018

jeannielynnmoulton Aug 8, 2018

thk123 Aug 8, 2018


		code_typet::parametert
		java_method_typet::parametert

Change code_typet to java_method_typet in JBMC #2661

Change code_typet to java_method_typet in JBMC #2661

Conversation

jeannielynnmoulton commented Aug 1, 2018 • edited Loading

mgudemann commented Aug 2, 2018

mgudemann left a comment

Choose a reason for hiding this comment

jeannielynnmoulton commented Aug 2, 2018

allredj left a comment

Choose a reason for hiding this comment

mgudemann left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

thk123 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

jeannielynnmoulton Aug 6, 2018 • edited Loading

Choose a reason for hiding this comment

martin-cs commented Aug 2, 2018

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

thk123 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

Change `code_typet` to `java_method_typet` in JBMC #2661

Change `code_typet` to `java_method_typet` in JBMC #2661

jeannielynnmoulton commented Aug 1, 2018 •

edited

Loading

jeannielynnmoulton Aug 6, 2018 •

edited

Loading