Calling member functions in annotations (jpf-aprop)

105 views
Skip to first unread message

Florian Biermann

unread,
Mar 31, 2014, 9:13:43 AM3/31/14
to java-pa...@googlegroups.com
Hey everyone,

For my master's thesis, I am trying to model-check a concurrent image filtering algorithms using a shared union-find data structure. The state space is huge, and I want to rely on annotations to reduce it, as well as to use those to verify that my code is correct, of course.

In order to do so, I need to access some fields of the object for which I want to verify member functions. Simple example:

class Algorithm {
    final int MAX_VALUES = 256;

    @Requires("0 <= p")
    @Ensures("0 <= Result && Result < MAX_VALUES")
    public int value(int p) {
  
      // Returns the value of the pixel p.
    }

    @Requires("value(p) <= value(n)")
    public void unite(int p, int n) {
        // Filters a pixel from the image.
    }
}

Here, the @Requires annotation on unite needs to make a member function call. However, jpf-aprop does not allow me to do this, giving the following error message:

Running Symbolic PathFinder ...
symbolic.dp=coral
symbolic.string_dp_timeout_ms=0
symbolic.string_dp=none
symbolic.min_int=0
symbolic.max_int=3
symbolic.min_double=-8.0
symbolic.max_double=7.0
JavaPathfinder v7.0 - (C) RIACS/NASA Ames Research Center


====================================================== system under test
dk.itu.parallel.morphology.verify.FilterDriver.main()

====================================================== search started: 3/31/14 3:10 PM
Making new image...
[SEVERE] JPF exception, terminating: exception during instructionExecuted() notification
gov.nasa.jpf.aprop.ContractException: numeric comparison for non numbers: 0,null
    at gov.nasa.jpf.aprop.Contract.compareNumericValues(Contract.java:128)
    at gov.nasa.jpf.aprop.Contract$LE.holds(Contract.java:282)
    at gov.nasa.jpf.aprop.ContractAnd.holds(ContractAnd.java:36)
    at gov.nasa.jpf.aprop.ContractAnd.holds(ContractAnd.java:36)
    at gov.nasa.jpf.aprop.ContractAnd.holds(ContractAnd.java:36)
    at gov.nasa.jpf.aprop.ContractAnd.holds(ContractAnd.java:36)
    at gov.nasa.jpf.aprop.Contract.holdsAny(Contract.java:56)
    at gov.nasa.jpf.aprop.listener.ContractVerifier.instructionExecuted(ContractVerifier.java:196)
    at gov.nasa.jpf.vm.VM.notifyInstructionExecuted(VM.java:789)
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1913)
    at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1853)
    at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:738)
    at gov.nasa.jpf.vm.VM.forward(VM.java:1672)
    at gov.nasa.jpf.search.Search.forward(Search.java:580)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)
    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:190)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:606)
    at gov.nasa.jpf.tool.Run.call(Run.java:76)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:117)
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during instructionExecuted() notification
    at gov.nasa.jpf.vm.VM.notifyInstructionExecuted(VM.java:796)
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1913)
    at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1853)
    at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:738)
    at gov.nasa.jpf.vm.VM.forward(VM.java:1672)
    at gov.nasa.jpf.search.Search.forward(Search.java:580)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)
    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:190)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:606)
    at gov.nasa.jpf.tool.Run.call(Run.java:76)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:117)
Caused by: gov.nasa.jpf.aprop.ContractException: numeric comparison for non numbers: 0,null
    at gov.nasa.jpf.aprop.Contract.compareNumericValues(Contract.java:128)
    at gov.nasa.jpf.aprop.Contract$LE.holds(Contract.java:282)
    at gov.nasa.jpf.aprop.ContractAnd.holds(ContractAnd.java:36)
    at gov.nasa.jpf.aprop.ContractAnd.holds(ContractAnd.java:36)
    at gov.nasa.jpf.aprop.ContractAnd.holds(ContractAnd.java:36)
    at gov.nasa.jpf.aprop.ContractAnd.holds(ContractAnd.java:36)
    at gov.nasa.jpf.aprop.Contract.holdsAny(Contract.java:56)
    at gov.nasa.jpf.aprop.listener.ContractVerifier.instructionExecuted(ContractVerifier.java:196)
    at gov.nasa.jpf.vm.VM.notifyInstructionExecuted(VM.java:789)
    ... 14 more

How else can I access runtime member variables in annotations? Do I need to write my own predicate for this? I'd be really grateful for some help on this.

Thanks in advance,
Florian

PETER C MEHLITZ

unread,
Mar 31, 2014, 1:08:26 PM3/31/14
to java-pa...@googlegroups.com
jpf-aprop had this philosophy that there should be a clear boundary between SUT and contract, and the latter should not be able to (easily) change SUT behavior, hence directly calling SUT methods wasn't supported. The exceptions are Predicates ("..satisfies <Predicate>.." clauses), which can be both at the SUT and native level, but have to adhere to the Predicate interface (evaluate()). That means, you have to wrap your whole "value(p) <= value(n)" into a Predicate class. I recall there was a reg test that shows both native and SUT level Predicate implementation.

-- Peter
> --
>
> ---
> You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Florian Biermann

unread,
Apr 1, 2014, 6:26:08 AM4/1/14
to java-pa...@googlegroups.com
Hi Peter,

Thanks for clarifying this. I now implemented my predicate using the
Predicate interface. Cursiously enough, it only gets executed when used
as a post- or precondition, not as an invariant. Is this a conscious
design decision?

Also, I need to model similar behavior as the IsMonotonicDecreasing
predicate (storing information), just that I want to use my member
function value(int) for evaluation. When I try implementing that using a
simple Predicate, I get a null-pointer exception:

[SEVERE] JPF exception, terminating: exception during
instructionExecuted() notification
java.lang.NullPointerException
at
gov.nasa.jpf.symbc.bytecode.INVOKEVIRTUAL.execute(INVOKEVIRTUAL.java:45)
at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1899)
at gov.nasa.jpf.vm.ThreadInfo.executeMethodAtomic(ThreadInfo.java:2061)
at
gov.nasa.jpf.aprop.Satisfies$ForwardingPredicate.evaluate(Satisfies.java:173)
at gov.nasa.jpf.aprop.Satisfies.holds(Satisfies.java:297)
[...]

Anything I can do to make this work and behave like the
IsMonotonicDecreasing example? If I try using the NativePredicate
interface, I cannot pass my Algorithm class directly, but instead I get
an instance of gov.nasa.jpf.vm.DynamicElementInfo. How can I get my
Algorithm object out of that again?

Thanks,
Florian
>> You received this message because you are subscribed to the Google Groups "Java(tm) Pathfinder" group.

Florian Biermann

unread,
Apr 2, 2014, 8:26:35 AM4/2/14
to java-pa...@googlegroups.com
Short update:

I found the cause of my NullPointerException. Turns out that
MJIEnv.getClassInfo() returns null sometimes, which is not handled
properly. Actually, INVOKEVIRTUAL.execute() wants to notify me that some
method could not be found (INVOKEVIRTUAL.getInvokedMethod() returns
null). The method in question is evaluate() on the predicate I wrote.

This happens after JPF verified the first couple of states of my
program. Before, it is able to execute evaluate(). I guess I am missing
out on something essential here. If I remove the ContractVerifier from
my listeners, everything works find (obviously).

Here is my configuration, maybe I messed up here?


@using=jpf-symbc
@using=jpf-aprop

# Taken directly from jpf-aprop examples
listener.autoload=\
javax.annotation.Nonnull,\
javax.annotation.concurrent.GuardedBy,\
gov.nasa.jpf.annotation.Const,\
gov.nasa.jpf.annotation.NonShared,\
gov.nasa.jpf.annotation.Invariant,\
gov.nasa.jpf.annotation.Ensures,\
gov.nasa.jpf.annotation.Requires

listener.javax.annotation.Nonnull=gov.nasa.jpf.aprop.listener.NonnullChecker
listener.javax.annotation.concurrent.GuardedBy=gov.nasa.jpf.aprop.listener.LockChecker
listener.gov.nasa.jpf.annotation.Const=gov.nasa.jpf.aprop.listener.ConstChecker
listener.gov.nasa.jpf.annotation.NonShared=gov.nasa.jpf.aprop.listener.NonSharedChecker
listener.gov.nasa.jpf.annotation.Invariant=gov.nasa.jpf.aprop.listener.ContractVerifier@pbc
listener.gov.nasa.jpf.annotation.Ensures=gov.nasa.jpf.aprop.listener.ContractVerifier@pbc
listener.gov.nasa.jpf.annotation.Requires=gov.nasa.jpf.aprop.listener.ContractVerifier@pbc

# Link to binaries and libraries
classpath =
${config_path}/../bin:${config_path}/../lib/multiverse-core-0.7.0.jar
sourcepath = ${config_path}/src:${config_path}/verify
native_classpath+=:${config_path}/../bin:${config_path}/verify
type_classpath+=:${config_path}/../bin:${config_path}/verify

# Specify driver
target = dk.itu.parallel.morphology.verify.FilterDriver

vm.insn_factory.class = gov.nasa.jpf.symbc.SymbolicInstructionFactory
vm.storage.class = nil
vm.por = true

# Configure symbolic execution
symbolic.min_int = 0
symbolic.max_int = 9

symbolic.debug = true

# Constraint solvers
symbolic.dp = omega.native
#symbolic.dp = coral

symbolic.lazy = true
symbolic.lazy.subtypes = true

#search.class = gov.nasa.jpf.search.heuristic.BFSHeuristic
#search.class = gov.nasa.jpf.search.heuristic.Interleaving
search.class = gov.nasa.jpf.search.heuristic.DFSHeuristic
search.depth_limit = 9

#listener = gov.nasa.jpf.aprop.listener.ContractVerifier
listener+=,gov.nasa.jpf.symbc.SymbolicListener
listener+=,gov.nasa.jpf.symbc.heap.HeapSymbolicListener
listener+=,gov.nasa.jpf.listener.PreciseRaceDetector
search.multiple_errors = true

log.info = gov.nasa.jpf.vm.ClassInfo
log.info+=,gov.nasa.jpf.aprop

cg.max_processors = 3


Any help is much appreciated!
Florian
Reply all
Reply to author
Forward
0 new messages