Skip to content
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.

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

When Java method doesn't exist, the list of existing methods reported by crucible_jvm_verify is wrong #911

Closed
atomb opened this issue Nov 18, 2020 · 2 comments · Fixed by #922
Assignees
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm

Comments

@atomb
Copy link
Contributor

atomb commented Nov 18, 2020

When running crucible_jvm_verify on, for example, the method key add(Ljava/math/BigInteger;Ljava/math/BigInteger;)Ljava/math/BigInteger; from java.math.BigInteger, I get the following:

ExecException unknown Could not find method
add(Ljava/math/BigInteger;Ljava/math/BigInteger;)Ljava/math/BigInteger;
in class java.math.BigInteger.
Available methods: "<clinit>"
"<init>" "clone" "equals"
"finalize" "getClass" "hashCode"
"notify" "notifyAll"
"registerNatives" "toString"
"wait" "wait" "wait" "Please check that the class and method are correct."

It looks like it's perhaps jumping one level too high in the class hierarchy and listing the methods of the parent class (java.lang.Object in this case)?

@atomb atomb added the subsystem: crucible-jvm Issues related to Java verification with crucible-jvm label Nov 18, 2020
@brianhuffman
Copy link
Contributor

Yes, I know exactly what's wrong here. Obviously I didn't test this code thoroughly enough. If no matching methods are found in a class, and the class has a superclass, then the search forgets about the original class and calls itself again on the superclass. But if it runs out of superclasses and never finds anything, it only lists the methods for the last class in the chain (java.lang.Object in your case). Instead, it should backtrack to the beginning and list all the available methods for all classes in the chain.

@brianhuffman brianhuffman self-assigned this Nov 18, 2020
@brianhuffman
Copy link
Contributor

Probably the easiest way to get the behavior we want is for the inner function of findMethod to take an extra accumulating parameter that remembers the set of method names that it has passed over so far. Then if we get to the end and find no matching methods, we will have the entire list on hand to print out.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants