rgrig / topl

TOPL Runtime Verifier
5 stars 1 forks source link

value initialized by constructors #25

Closed rgrig closed 12 years ago

rgrig commented 12 years ago

I want x = new A(y) to be treated by topl essentially the same as x = A.make(y). To offer this illusion some trickery is needed while instrumenting the bytecode, because static methods and constructors are compiled to different things. In this example the static method takes y as an argument and returns x. But, the constructor takes two arguments x and y and returns nothing. Right now the instrumentation emits an event call with the value of y and an event return with no value, so the returned value is not accessible. (In fact, it leads to a crash of the checker.)

Note: The call event does not send x on purpose. One reason is that I want to emulate the static method behavior. Another reason, more serious, is that x can't be put in an array of objects before it is initialized. (Well, some JVM versions are forgiving, but others do conform to the spec.)

How to simulate a return that carries x? (Note: At the point were return is reached x must be initialized, if the input bytecode is valid.) Initially x is in register 0, but there is no guarantee that it still is (although for code generated by normal compilers it probably is). One idea is to push it on the stack in the beginning and then take it of the stack just before return to build up the event. Alas, there is no guarantee that in the original bytecode the stack is empty when return is reached.

Is there a simple solution to send a return event with value x?

rgrig commented 12 years ago

@yoff: Any idea? I'd like something that correctly handles any valid bytecode, not just bytecode that looks generated by a compiler. The option we have now is to use the infrastructure in Barista to track how the stack looks at the return point. But, I'd like a simple solution.

yoff commented 12 years ago

@yoff: Any idea? I'd like something that correctly handles any valid bytecode, not just bytecode that looks generated by a compiler. The option we have now is to use the infrastructure in Barista to track how the stack looks at the return point. But, I'd like a simple solution. Does storing the value in a local variable work? i.e. using astore in the beginning and aload just before return?

rgrig commented 12 years ago

That should be easier. Thanks!

rgrig commented 12 years ago

This is now waiting on https://github.com/rgrig/barista/issues/14

rgrig commented 12 years ago

This is now not waiting anymore. :)

yoff commented 12 years ago

Indeed, I saw you got the high level locals in, that is really nice! :-)