Skip to content

[TG-3657] Always load CProver.nondetInitialize #2267

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jun 5, 2018
Merged

[TG-3657] Always load CProver.nondetInitialize #2267

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
971a34b
Always load cprover-nondet-initialize
Jun 1, 2018
a673e5d
Add test verifying that the cproverNondetInitialize method is always …
Jun 4, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file added jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.class
View file
Open in desktop
Binary file not shown.
11 changes: 11 additions & 0 deletions jbmc/regression/jbmc/cprover-always-load-nondet-initialize/ObjectWithNondetInitialize.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
import org.cprover.CProver;

class ObjectWithNondetInitialize {
private int value_;
public void cproverNondetInitialize() {
CProver.assume(value_ == 13);
}
public int value() {
return value_;
}
}
7 changes: 7 additions & 0 deletions jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Opaque.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
import org.cprover.CProver;

public class Opaque {
public ObjectWithNondetInitialize get() {
return new ObjectWithNondetInitialize();
}
}
Binary file added jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.class
View file
Open in desktop
Binary file not shown.
5 changes: 5 additions & 0 deletions jbmc/regression/jbmc/cprover-always-load-nondet-initialize/Test.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
public class Test {
public int test() {
return (new Opaque()).get().value();
}
}
11 changes: 11 additions & 0 deletions jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
KNOWNBUG
Test.class
--function Test.test --show-goto-functions --lazy-methods
EXIT=0
SIGNAL=0
ObjectWithNondetInitialize\.cproverNondetInitialize\(\)
--
--
Check if cproverNondetInitialize method is loaded in an object
returned from an opaque method
https://github.com/diffblue/cbmc/issues/2273
11 changes: 11 additions & 0 deletions jbmc/src/java_bytecode/ci_lazy_methods.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -248,6 +248,17 @@ bool ci_lazy_methodst::operator()(
}
}

// cproverNondetInitialize has to be force-loaded for mocks to return valid
// objects (objects which satisfy invariants specified in the
// cproverNondetInitialize method)
for(const auto &class_name : instantiated_classes)
{
const irep_idt cprover_validate =
id2string(class_name) + ".cproverNondetInitialize:()V";
if(symbol_table.symbols.count(cprover_validate))
methods_already_populated.insert(cprover_validate);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Surely you should also actually populate them!

Copy link
Contributor Author

@LAJW LAJW Jun 1, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't have to populate anything - all of these variables are local and are used to produce this methods_already_populated set, which is then used to filter out things to not remove (it looks like). Most of them are badly named. For instance this one should be called methods_to_load and probably generated by a separate method.

I initially wanted to refactor this function, but since lazy loading V2 development is in full swing, I decided that would be a wasted effort. If my assumption was wrong, I'll create another PR that cleans this up, and leave this one alone for the sake of merging this fix on time.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I meant, you should ensure the method actually is converted, not just put it in an "already_populated" set. Doing that will stop it being removed from the symbol table; putting it into the worklist will get the symbol's value (the method body) populated.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But the method body is populated. Otherwise it wouldn't fix the test-gen bug, which is what this change was all about. Really, the only problem is with preexisting misleading variable names.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Any idea how it's getting populated without being added to methods_already_populated (whose name is accurate, it is an accumulation of methods that have been populated by the method converting loop above)?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe because there is a special case for it in add_needed_class? https://github.com/diffblue/cbmc/blob/develop/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp#L41

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That would result in its being added to the worklist and converted (and thus retained) in the usual way. Somehow its body is being filled in without going through the ci_lazy_methodst mechanism. Last I heard @LAJW was trying to find out why and submit a fix PR (or justify the status quo)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why it works:
After the typecheck phase in which the ci_lazy_methodst is run, there is a separate lazy_goto_model.load_all_functions(); which ensures all symbols are loaded so actually loads the method.

This fix shouldn't be required because, as @romainbrenguier points out, it is already added to the needed methods by ci_lazy_methods_needed. The problem (I suppose) is that a return type of an opaque method is not sufficient to cause loading that type. This is certainly wrong for test-gen, which will stub that method and try and create the object of that type. @smowton do you have an oppinion on whether that is correct for CBMC? That is:

class Foo {
  public int field;
}
class Opaque {
  static Foo opaqueMethod() { return null; }
}
class EntryClass {
  static int entryFunction() { 
    return Opaque.opaqueMethod().field;
  }
}

Should Foo be loaded?

}

// Remove symbols for methods that were declared but never used:
symbol_tablet keep_symbols;
// Manually keep @inflight_exception, as it is unused at this stage
Expand Down