search

rgrig / topl

TOPL Runtime Verifier
5 stars 1 forks source link

Provide aliasing hints for infer. #55

Closed rgrig closed 6 years ago

rgrig commented 6 years ago

When calling a monitored method, we need to tell Infer that the receiver object (and perhaps the arguments?) could be aliased to one of the TOPL monitor registers. Otherwise, in some situations, Infer uses a heuristic that the receiver object is not aliased to anything else known to be on the heap, which includes TOPL registers.

It is easy to give such hints, using if statements. For example:

if (x == topl.Property.r0) {} else {}
x.monitored_methos()
rgrig commented 6 years ago

See also https://github.com/facebook/infer/issues/823

rgrig commented 6 years ago

A call x.foo(a,b,c) should be given a hint iff the property has a pattern of the form r.foo(...); that is, (i) the method name matches and (ii) there is a guard on argument 0 (i.e. the receiver object).

rgrig commented 6 years ago

Partially addressed by https://github.com/rgrig/topl/commit/ffcccc2abd96b2e76d924a07dee145a45266b028 JVM seems happy with the new bytecode (not thoroughly tested, though). Infer, however, stops printing Postconditions (in the PrePost pairs). We need to figure out why.

rgrig commented 6 years ago

The pre/post problem was unrelated: https://github.com/facebook/infer/issues/831