AOP with JPF

[Mark Tanti]

Hi,

I wrote two identical projects, both of them having the same jpf file. The only difference between these two is that one of them is set as an Aspect Oriented Project. The problem I am currently facing is that when I verify the normal Java project, the result would be as predicted and obviously it makes sense. On the other hand, when trying to verify the AOP project, JPF will produce 1 path and will stuck forever trying to verify until a no memory exception will pop up. 

Can it be the case where JPF is not capable of handling cross checking, which is involved in AOP?

Thanks

Mark Tanti

[Alexander von Rhein]

Hi Mark,

i did use JPF to verify AspectJ projects and it worked as expected.
However my aspects were very basic.
I only used them to check specifications when certain methods are executed.

privileged public aspect Specifications1 {
    before(Client client, Email msg) :
         call(static void EmailSystem.Client.autoRespond(Client, Email))
         && args(client, msg) {
        // autoResponder
         if (!specification_statisfied(msg)) {
                // throw exception
            }
    }
}

Perhaps you can try a simpler aspect and find out which part causes problems.

--Alex

--

---
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.

[Mark Tanti]

Hi Rhein,

My aspects are very basic as well but when trying to execute, the below is returned..

Executing command: java -jar C:\Users\Mark\SkyDrive\ICT\Degree\Year5\FYP\EclipseCode\jpf-core\build\RunJPF.jar +shell.port=4242 C:\Users\Mark\SkyDrive\ICT\Degree\Year5\FYP\EclipseCode\JPF Example\src\jpfexample\SymbolicExecutor.jpf 

Running Symbolic PathFinder ...

symbolic.dp=choco

symbolic.string_dp_timeout_ms=0

symbolic.string_dp=none

symbolic.choco_time_bound=30000

symbolic.min_int=0

symbolic.max_int=100

symbolic.min_double=-8.0

symbolic.max_double=7.0

JavaPathfinder v7.0 (rev 1155) - (C) RIACS/NASA Ames Research Center

====================================================== system under test

jpfexample.JPFExample.main()

====================================================== search started: 31/03/14 21:29

*************Summary***************

PC is:constraint # = 1

x_1_SYMINT[1] > y_2_SYMINT[0]

Return is:  CONST_1

***********************************

sym v null

sym v null

1

[SEVERE] JPF out of memory

====================================================== search constraint

JPF out of memory

====================================================== snapshot 

thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,lockCount:0,suspendCount:0}

  call stack:

thread java.lang.Thread:{id:1,name:Thread-1,status:RUNNING,priority:10,lockCount:0,suspendCount:0}

  call stack:

[SEVERE] JPF exception, terminating: exception during out-of-memory termination

java.lang.NullPointerException

at gov.nasa.jpf.search.Search.error(Search.java:400)

at gov.nasa.jpf.search.Search.error(Search.java:391)

at gov.nasa.jpf.JPF.run(JPF.java:645)

at gov.nasa.jpf.JPF.start(JPF.java:190)

at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)

at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)

at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)

at java.lang.reflect.Method.invoke(Unknown Source)

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 out-of-memory termination

at gov.nasa.jpf.JPF.run(JPF.java:648)

at gov.nasa.jpf.JPF.start(JPF.java:190)

at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)

at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)

at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)

at java.lang.reflect.Method.invoke(Unknown Source)

at gov.nasa.jpf.tool.Run.call(Run.java:76)

at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:117)

Caused by: java.lang.NullPointerException

at gov.nasa.jpf.search.Search.error(Search.java:400)

at gov.nasa.jpf.search.Search.error(Search.java:391)

at gov.nasa.jpf.JPF.run(JPF.java:645)

... 7 more

Thanks Mark

[Alexander von Rhein]

Hi Mark,

I have used AspectJ only with normal JPF (and my extension JPF-BDD).
It seems you are using Symbolic PathFinder.

I can imagine that AspectJ generates some unusual constructs that trick Symbolic PathFinder into an endless loop.
I guess the only way to find out where the problem lies exactly is to reduce your application until you have a minimal example which triggers the exception.
(Or start with a very small example.)

--Alex

[Corina Pasareanu]

Hi

yes if you are using Symbolic Pathfinder this problem is for me :)

i can try to debug if you send me a succinct description of an example+config file.
But first: did you run it with JPF (i.e. non-symbolic)?

Do you still get a bug?

Thanks,

 Corina

[Mark Tanti]

Hi

attached please find my simple example..

it consists of a simple java application which compares two integer numbers. A monitor is included in AOP which checks that the two integers are not the same. in any case, the monitor will output into a separate file. a .jpf file is also included which I used to verify the application.

In this case, the path finder will just stop processing while verifying.

Thanks

Mark

[Mark Tanti]

Hi, 

Yes I tried non symbolic path finder and it did exactly the same thing. 

Now I also managed to use SPF with AOP, but very simple AOP. As soon as I start to include some more complex methods, the same error will start being returned again (ie. out of memory)

Thanks Mark

[Corina Pasareanu]

is this an out-of-memory problem?

then this is not an error.

corina

[Mark Tanti]

Hi,

Yes, the error is an out-of-memory exception. I think that the cause of all this is when trying to use Object instead of a primitive variable. I think JPF is trying to keep digging in until there isn't any more memory left, and then it throws this out-of-memory exception.

Does this make any sense?

Regards,

Mark

[Corina Pasareanu]

you can try to run it by putting a limit on the search depth, e.g.

search.depth_limit = 10