Finished applying fixes for jbmc for assignment consistency #3822

thk123 · 2019-01-16T11:17:50Z

Each commit message has a non-empty body, explaining why the change was made.
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). TODO
[na] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig · 2019-01-16T12:28:12Z

src/goto-programs/remove_virtual_functions.cpp

+        "those arguments must be pointer-typed");
+    }
+
+    call_args[i].make_typecast(need_type);


This seems pointless - given the above type_eq the difference could now only be tag/symbol vs non-tag/symbol types.

Not so, that only checked that the types are either type_eq or are pointers

tautschnig · 2019-01-16T12:29:01Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1531,7 +1550,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
    else if(statement=="getfield")
    {
      PRECONDITION(op.size() == 1 && results.size() == 1);
-      results[0]=java_bytecode_promotion(to_member(op[0], arg0));
+      results[0]=java_bytecode_promotion(to_member(op[0], arg0, ns));


This PR will need per-commit clang-format cleanup.

src/goto-programs/remove_virtual_functions.cpp

tautschnig · 2019-01-16T12:32:13Z

Oops, missed the do-not-review label.

romainbrenguier · 2019-01-17T13:06:36Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -642,20 +642,39 @@ static irep_idt get_if_cmp_operator(const irep_idt &stmt)
  throw "unhandled java comparison instruction";
 }

-static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
+static member_exprt to_member(


documentation here would help

romainbrenguier · 2019-01-17T13:07:22Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -642,20 +642,39 @@ static irep_idt get_if_cmp_operator(const irep_idt &stmt)
  throw "unhandled java comparison instruction";
 }

-static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
+static member_exprt to_member(
+  const exprt &pointer, const exprt &fieldref, const namespacet &ns)


⛏️ fieldref is not a good name

romainbrenguier · 2019-01-17T13:15:15Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp


-  dereference_exprt obj_deref=checked_dereference(pointer2, class_type);
+  const irep_idt &component_name = fieldref.get(ID_component_name);


Is fieldref assumed to be a member_exprt? It would be better to make that explicit.

It isn't member_exprt, but rather the nameless expression that describes a getfield or setfield operand produced by the Java bytecode parser

romainbrenguier · 2019-01-17T13:17:14Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+      to_struct_type(ns.follow(accessed_object.type()));
+    auto component = object_type.get_component(component_name);
+
+    if(component.is_not_nil())


⛏️ I would prefer if the loop was expressed as while(component.is_nil()) rather than while(1)

romainbrenguier · 2019-01-17T13:21:59Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+      "infer_opaque_type_fields should guarantee that a member access has a "
+      "corresponding field");
+
+    accessed_object = member_exprt(accessed_object, components.front());


💡 ideally there should be a function giving the parent class from a java class type, that would make this piece of code clearer.

Dumb question: what is it that assures us that we always need to look at the first component? I get that because of Java not permitting multiple inheritance if anything, it must be the first one. Is it because everything inherits at least from java.lang.object that we know that this first component must be a struct type?

Yep, invariant of Java object layout: every class has at least one member, and the first one is either @class_identifier (java.lang.Object, or any stub class whose position in the class hierarchy is unknown) or its single superclass.

thk123 · 2019-01-17T17:32:05Z

So I couldn't reproduce the failure locally, seemingly because ctest does not run the symex-driven-lazy-loading-expected-failure target correctly (finds 0 tests to run). I fixed this by removing -s;symex-driven-loading from the CMakeLists.txt in the relevant regression folder and now get the tests.

I don't understand this change, so if someone does and wants to PR it, that would have my approval. Otherwise, I will PR it after I've got this working.

tautschnig · 2019-01-17T18:09:34Z

@thk123 Are you working off of a branch that has 3313f25?

thk123 · 2019-01-17T18:10:19Z

@tautschnig thanks for the tip @smowton just pointed me towards that - now got the failure locally. It is to do with an invalid pop and only with symex driven lazy loading so will keep digging.

thk123 · 2019-01-18T10:52:25Z

Tracked down the problem with the malformed pop (remove returns had already run on a function, so swapping out the type for the type in the symbol table meant no returns). Just checking locally that passes all the tests, then will push up here to verify on CI and then will create a TG bump since plausible it will break things there too.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 8366f3b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97821114
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

thk123 · 2019-01-18T18:05:17Z

Even when the compile errors are fixed, this fails in TG for non-equal types in symex - this looks to be to do with the custom stubbing - manual bump incoming.

smowton · 2019-01-19T13:13:08Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

 {
  struct_tag_typet class_type(fieldref.get(ID_class));

-  const exprt typed_pointer = typecast_exprt::conditional_cast(
-    pointer, java_reference_type(class_type));
+  const exprt typed_pointer =


This commit contains format fixups that ought to be squashed into a previous commit

smowton

Can't approve my own code of course, but I agree with @thk123 and @kroening's parts

thk123 · 2019-01-21T17:00:59Z

TG bump looks to be passing - will address existing comments and tidy up, then should be ready for a final review from @tautschnig

allredj

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

tautschnig · 2019-01-21T18:32:53Z

@thk123 Just send a ping when you're done with cleanup work.

tautschnig · 2019-01-21T18:34:09Z

@thk123 Actually there isn't anything new that I hadn't looked at in the meantime, so just do the cleanup, merge, and update TG accordingly. Thanks!

thk123 · 2019-01-17T14:01:47Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+
+    // Component not present: check the immediate parent type.
+
+    const auto &components = object_type.components();


⛏️ Looks like resolve_inherited_componentt can be adapted to do this search

That said - this is just moving code from the typecheck so will clean up in a follow up PR/commit

tautschnig · 2019-01-23T09:07:17Z

@thk123 re root_object: there is object_descriptor_exprt, which can be passed an exprt via its build method and then you get a .root_object() - but I need to re-read your code to see whether this does exactly what you need.

tautschnig · 2019-01-23T09:11:56Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+  // may in fact belong to any ancestor type.
+  while(1)
+  {
+    struct_typet object_type =


I'd use const struct_typet &object_type = ... here.

This code is in fact simply moved - I'd prefer to follow this PR up with a clean up PR as this whole block I think can be replaced by resolve_inherited_componentt

Sounds good!

tautschnig · 2019-01-23T09:16:30Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+      "infer_opaque_type_fields should guarantee that a member access has a "
+      "corresponding field");
+
+    accessed_object = member_exprt(accessed_object, components.front());


Dumb question: what is it that assures us that we always need to look at the first component? I get that because of Java not permitting multiple inheritance if anything, it must be the first one. Is it because everything inherits at least from java.lang.object that we know that this first component must be a struct type?

tautschnig · 2019-01-23T09:23:59Z

src/goto-programs/remove_virtual_functions.cpp

+        call_args[i].type().id() == ID_pointer,
+        "where overriding function argument types differ, "
+        "those arguments must be pointer-typed");
+      call_args[i].make_typecast(need_type);


Avoid using make_typecast (it's now deprecated), do call_args[i] = typecast_exprt(call_args[i], need_type); instead.

tautschnig · 2019-01-23T09:27:21Z

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

 #include <goto-programs/goto_functions.h>
+#include <goto-programs/show_goto_functions.h>
+#include <iostream>


Is that a debugging left-over?

tautschnig · 2019-01-23T09:33:33Z

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

+/// by skipping over type casts and removing balanced dereference/address_of
+/// operations
+optionalt<symbol_exprt>
+root_object(const exprt &lhs_expr, const symbol_tablet &symbol_table)


As said in the comment, there is object_descriptor_exprt. I think it may be necessary to extend object_descriptor_exprt::build_object_descriptor_rec with code handling paired dereference_exprt/address_of_exprt, but then it should do the trick for you. I believe all the code that this needs in addition is (some variant of):

else if(expr.id() == ID_dereference) { const dereference_exprt &deref = to_dereference_expr(expr); if(deref.pointer().id() == ID_address_of) { const address_of_exprt &address_of = to_address_of_expr(deref.pointer()); dest.object() = address_of.object(); build_object_descriptor_rec(ns, address_of.object(), dest); } }

Yes I saw the object_descriptor_exprt and saw that it didn't handle the ref/deref. In the interest of not wanting to break anything else that uses this, I will attempt this refactor in a follow up PR too if that is acceptable to you.

I'll post a PR in a few minutes.

tautschnig · 2019-01-23T09:34:37Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

 #include <algorithm>
 #include <functional>
-#include <unordered_set>
+#include <goto-programs/remove_returns.h>


I'd prefer not mixing our headers with STL includes.

thk123 · 2019-01-23T10:02:33Z

what is it that assures us that we always need to look at the first component?

It probably isn't a great assumption - it is true because in java_bytecode_convert_class the base class component is always added first (line 370) and then additional fields (line 458). As with other comment - would prefer to address in follow up PR using resolve_inherited_componentt

Previously we created the expression with the partial type given at the access site (i.e. as part of the get/setfield bytecode), but this lacked any generic type information, which the actual component *did* have. The member expression could therefore be type-inconsistent with the object is addressed. Since it's no longer necessary to make the expression approximately and later fix it up in typecheck_expr, let's just get it right the first time, including giving it the right type.

…le add operations This is generally illegal (but is tricky to trigger, hence no test)

…calls This both ensures that the reference to the callee precisely matches the callee's symbol type, and that parameters match. For example, previously the callee could specifically take a List<Integer>, but the type given at the callsite might just be `callee(List)`, omitting the generic type information, leading to a pointer changing type without a cast.

…ase type This is necessary because a generic qualifier is recorded on the pointer, while the direct member has an unqualified type.

For example, when List<E> extends the Collection<E> interface, its overrides of methods accepting an element, such as add(E), are given in terms of its own E, not that of Collection. Therefore we must cast from Collection::E* to List::E* when using that particular override. Only typecast if the parameter types are distinct

It already tried to do this, but doesn't take account for pointers that encode generic information: in such cases the underlying object type can be equal but the pointers differ, and a cast is necessary.

Once all the cases are fixed, this can be returned to a regular equality

thk123 · 2019-01-23T10:52:54Z

Seem to have done enough rebases to make clang-format go away...

Specifically - be impartial to deref/cast/address of combinations on the lhs. Be impartial to direct assignments without casts Be impartial to casts before assigning to address of another variable

thk123 · 2019-01-23T10:57:38Z

@tautschnig addressed minor comments, larger changes I would like to address in a follow up PR. If that's OK with you, this looks good to merge once CI passes.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 5a9bf1a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98303689
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

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

thk123 requested review from cesaro, cristina-david, kroening, NathanJPhillips, peterschrammel, pkesseli, smowton and tautschnig as code owners January 16, 2019 11:17

thk123 added the do not review label Jan 16, 2019

tautschnig approved these changes Jan 16, 2019

View reviewed changes

romainbrenguier reviewed Jan 17, 2019

View reviewed changes

thk123 force-pushed the assignment-consistency branch from 9adfb23 to c9dea6b Compare January 17, 2019 15:41

thk123 force-pushed the assignment-consistency branch from c9dea6b to 8366f3b Compare January 18, 2019 11:13

allredj reviewed Jan 18, 2019

View reviewed changes

smowton reviewed Jan 19, 2019

View reviewed changes

smowton approved these changes Jan 19, 2019

View reviewed changes

tautschnig assigned thk123 Jan 19, 2019

thk123 force-pushed the assignment-consistency branch from 8366f3b to 050dbec Compare January 21, 2019 15:37

allredj reviewed Jan 21, 2019

View reviewed changes

thk123 force-pushed the assignment-consistency branch from 050dbec to fabeae2 Compare January 22, 2019 09:46

thk123 removed the do not review label Jan 22, 2019

thk123 commented Jan 22, 2019

View reviewed changes

thk123 force-pushed the assignment-consistency branch from fabeae2 to dca461a Compare January 22, 2019 11:58

tautschnig reviewed Jan 23, 2019

View reviewed changes

Daniel Kroening and others added 10 commits January 23, 2019 10:50

expr_initializert: fix type of enum constants

6f38516

symex: check type consistency of assignments

ace71e7

Java method converter: don't hold a symbol table reference across tab…

f490894

…le add operations This is generally illegal (but is tricky to trigger, hence no test)

Java pointer casts: ensure type consistency, even when casting to a b…

0a3b99b

…ase type This is necessary because a generic qualifier is recorded on the pointer, while the direct member has an unqualified type.

Allocate objects: cast when pointer types differ

279c72b

It already tried to do this, but doesn't take account for pointers that encode generic information: in such cases the underlying object type can be equal but the pointers differ, and a cast is necessary.

Reduce type equality check within symex

cc8f05a

Once all the cases are fixed, this can be returned to a regular equality

Increased description in test to make it clear what it is testing

1a583d4

thk123 force-pushed the assignment-consistency branch from dca461a to 5a9bf1a Compare January 23, 2019 10:50

thk123 added 2 commits January 23, 2019 10:56

Fixing unit tests wrt new GOTO format

a1e398d

Specifically - be impartial to deref/cast/address of combinations on the lhs. Be impartial to direct assignments without casts Be impartial to casts before assigning to address of another variable

Resolve issue with return type being erased

f0c520e

thk123 force-pushed the assignment-consistency branch from 5a9bf1a to f0c520e Compare January 23, 2019 10:57

allredj reviewed Jan 23, 2019

View reviewed changes

tautschnig merged commit 02744e6 into diffblue:develop Jan 23, 2019

thk123 mentioned this pull request Jan 23, 2019

Assignment type consistency #3634

Closed

3 tasks

tautschnig mentioned this pull request Jan 23, 2019

Remove unnecessary uses of ns.follow in util/ #3737

Merged

3 tasks

thk123 deleted the assignment-consistency branch January 23, 2019 17:53

This was referenced Feb 15, 2019

Add test checking generic function parameter casts appear when expected #4200

Merged

Add test for casting after a clean or soft cast #4201

Merged

Add test for casting of virtual function parameter types #4202

Merged


		dereference_exprt obj_deref=checked_dereference(pointer2, class_type);
		const irep_idt &component_name = fieldref.get(ID_component_name);


		// Component not present: check the immediate parent type.

		const auto &components = object_type.components();

Finished applying fixes for jbmc for assignment consistency #3822

Finished applying fixes for jbmc for assignment consistency #3822

Uh oh!

Conversation

thk123 commented Jan 16, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig commented Jan 16, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 commented Jan 17, 2019

Uh oh!

tautschnig commented Jan 17, 2019

Uh oh!

thk123 commented Jan 17, 2019

Uh oh!

thk123 commented Jan 18, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 commented Jan 18, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 commented Jan 21, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jan 21, 2019

Uh oh!

tautschnig commented Jan 21, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jan 23, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!