Symbc crash reading input - "can't find caller stackframe for invokevirtual java.io.InputStream.read([BII)I"

[Pedro Louro]

Hi all,

I have the goal to symbolic execute a whole program ( even if it work
just with small programs), so I´ve tried to apply symbc to a main
method, assuming as symbolic the values that come from input.
For this I added to the example "TestPaths.java" the following code:

InputStreamReader isr = new InputStreamReader(System.in);
BufferedReader br = new BufferedReader(isr);
try {
String test = br.readLine();
} catch (IOException e) {
e.printStackTrace();
}

When I run symbc here I get an error :

[SEVERE] JPF exception, terminating: exception during
instructionExecuted() notification
java.lang.AssertionError: can't find caller stackframe for:
invokevirtual java.io.InputStream.read([BII)I
at
gov.nasa.jpf.jvm.bytecode.InvokeInstruction.getArgumentValues(InvokeInstruction.java:
159)
at
gov.nasa.jpf.symbc.SymbolicListener.instructionExecuted(SymbolicListener.java:
336)
at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:692)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:
1989)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:
1941)
at
gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:
656)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1716)
at gov.nasa.jpf.search.Search.forward(Search.java:500)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:80)
at gov.nasa.jpf.JPF.run(JPF.java:535)
at gov.nasa.jpf.JPF.start(JPF.java:166)
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:86)
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during
instructionExecuted() notification
at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:703)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:
1989)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:
1941)
at
gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:
656)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1716)
at gov.nasa.jpf.search.Search.forward(Search.java:500)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:80)
at gov.nasa.jpf.JPF.run(JPF.java:535)
at gov.nasa.jpf.JPF.start(JPF.java:166)
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:86)
Caused by: java.lang.AssertionError: can't find caller stackframe for:
invokevirtual java.io.InputStream.read([BII)I
at
gov.nasa.jpf.jvm.bytecode.InvokeInstruction.getArgumentValues(InvokeInstruction.java:
159)
at
gov.nasa.jpf.symbc.SymbolicListener.instructionExecuted(SymbolicListener.java:
336)
at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:692)
... 14 more

What could be the problem here? It would be possible to achieve my
goal with jpf-symbc?
Thanks in advance!

[Corina Pasareanu]

hey:
It should work for medium sized programs?
Currently it can handle inputs of primitive types, user defined data structures and strings.
You'll need to abstract away the buffered reader, etc.
If you send my your app I can take a look.
thanks,
Corina

[Pedro Louro]

Thank you for your response Corina!
For the program I was just wondering, I don´t have a specific target
yet.
I´ve modified the TestPaths.java example for the folowing code ( just
added the readLine from the bufferedReader) and I get the error that I
´ve posted before.
How can it handle inputs of primitive types if I can´t read them ?

public static void main (String[] args){
System.out.println("!!!!!!!!!!!!!!! Start Testing! ");

InputStreamReader isr = new InputStreamReader(System.in);
BufferedReader br = new BufferedReader(isr);
try {
String test = br.readLine();
} catch (IOException e) {
e.printStackTrace();
}

(new TestPaths()).testMe2(0,false);
}

public void testMe2 (int x, boolean b) {
System.out.println("!!!!!!!!!!!!!!! First step! ");
//System.out.println("x = " + x);
if (b) {
if (x <= 1200){
System.out.println(" <= 1200");
}
if(x >= 1200){
System.out.println(" >= 1200");
testMe(x,true);

[Pedro Louro]

Well, I have a new update here ( I still have the same problem above).
I erased the readLine part and added an int random generator as I show
below. When I run symbc for this method "TestPaths.testMe2(sym#sym)",
it doesn´t generate the conditions associated with the
nondeterministic random int as I expected.
So, if I got this right, symbc just tracks the symbolic arguments from
the method call, but it doesn´t bothers with the sources of non-
determinism inside the method, like input reads and random numbers. Is
this right?
It is possible to generate conditions for these cases to?

Thanks for your help!

public void testMe2 (int x, boolean b) {
System.out.println("!!!!!!!!!!!!!!! First step! ");

Random random = new Random();
int temp = random.nextInt();

if (temp > 50)
System.out.println("random > 50");
else
System.out.println("random <= 50");

if (b) {
if (x <= 1200){
System.out.println(" <= 1200");
}
if(x >= 1200){
System.out.println(" >= 1200");
}
}
}

result:
====================================================== Method
Summaries
Symbolic values: x_1_SYMINT,b_2_SYMINT

testMe2(1200,true)
testMe2(-1000000,true)
testMe2(1201,true)
testMe2(don't care,false)

[Corina Pasareanu]

yes, the symbolic execution will transform the parameters in symbolic values.
instead of the random bit you can make "temp" another parameter, and symbolic execution will consider both possibilities ("then" and "else" branches) in "if(temp>50)"

corina

[Pedro Louro]

ok, so I have two specific questions:

1) When I call the readLine from the BufferedReader I get the

"java.lang.AssertionError: can't find caller stackframe for:

invokevirtual java.io.InputStream.read([BII)I" . Do you have some
ideia why I get this error?

2) Is it hard to modify symbc in order to also consider as a symbolic
value, assignments from random generators and readline() ?

[Jiangfan Shi]

I think you are encountering a hard part of JPF, which is related to
calling native methods. Usually these native methods will just use
default values for their parameters, and these default values are
generated by JPF during its' symbolic execution over previous methods.
So this gives you the first trouble.

For the second, one idea maybe extract the variable to a class field,
then use @Symbolic("true") to make it symbolic variable explicitly,
and finally you just use this variable without really assigning random
value to it ( that is, you just delete the readline() statement).

Maybe I am wrong somewhere, but in general you are facing a limitation
of JPF world.

Best,

Jiangfan

[Corina Pasareanu]

Thank you Jiangfan:
Yes you are right, you need to model the native methods in the "JPF world (look for example in src/peers that provides models for Math library functions). We have a recent result that will appear at ISSTA that treats native methods as uninterpreted functions. We'll robustify that code, document it and then people should be using it.
For the particular exaple at hand, Willem Visser and his student are working on handling strings symbolically. So they might address modeling some of the read functions.
Regards,
Corina

[Pedro Louro]

Thank you both!

If I undestood well, I can do what I want just by picking in the
"executeInstruction" from the SymbolicListener, all the assignments of
the readln(), make the variable explicity symbolic and then skip the
instruction (to avoid the crash).

The thing is, how can I:

1) skip an instruction to execute (I read in the wiki that is possible
to do that in the "executeInstruction" but don´t know how.
2) get to the variable to explicitly put it to symbolic?

I´m sorry to bother so much , but this is really important for my
thesis and just by analyzing the code I´m not getting there.

Best Regards
Pedro Louro

On 16 Maio, 19:30, Corina Pasareanu <corina.ani...@gmail.com> wrote:
> Thank you Jiangfan:
> Yes you are right, you need to model the native methods in the "JPF world
> (look for example in src/peers that provides models for Math library
> functions). We have a recent result that will appear at ISSTA that treats
> native methods as uninterpreted functions. We'll robustify that code,
> document it and then people should be using it.
> For the particular exaple at hand, Willem Visser and his student are working
> on handling strings symbolically. So they might address modeling some of the
> read functions.
> Regards,
> Corina
>

> ...
>
> mais informações »

[Corina Pasareanu]

To see an example on how to skip instructions look in the jpf-symbc project in:

concolic/ConcreteExeceutionListener method instructionExecuted

[Pedro Louro]

Hello all!

Ok, the symbc doesn´t crash anymore with readLine because I´m skipping
it´s execution.
Now I need to catch the "ASTORE" next to the readLine, and to know in
which Local it´s going to store the value in order to mark it has
symbolic.
First, how can I find what is the local that is manipulated with the
ASTORE, and second, how can I mark it as symbolic?

Hopefully, with this 2 points I´m done with modfying jpf and I can
produce some results :)

Best Regards
Pedro Louro

> ...
>
> mais informações »

[Corina Pasareanu]

hey

you can mark it symbolic by setting the attribute a symbolic expression
look at the bytecode instructions already under symbc, you can do similar with ASTORE

corina