Running Symbolic PathFinder

[Quoc-Sang Phan]

Dear all,

I have some questions about running Symbolic PathFinder (SPF). I need
to use SPF in a shell script, but I find most instructions is for
eclipse. I build jpf-core successfully, and tried with some examples
in jpf-core/src/examples.
When I try jpf-symbc

1) I confuse because there are two shell script jpf in jpf-core/bin
and jpf-symbc/bin. The former calls jpf-core/build/RunJPF.jar, and the
latter calls jpf-symbc/tools/RunJPF.jar. So I don't know which script
or jar file should I use for SPF?

2) I tried with both scripts above with :~/Programs/jpf/jpf-symbc$ jpf
src/examples/TestPaths.jpf
For the one in jpf-core/bin, I got the following error:
-------------------
[SEVERE] JPF configuration error: class not found
gov.nasa.jpf.symbc.SymbolicInstructionFactory by classloader:
gov.nasa.jpf.JPFClassLoader@10b30a7
> used within "vm.class" instantiation of class gov.nasa.jpf.jvm.JVM
[SEVERE] JPF terminated
-------------------

For the one in jpf-symbc/bin, I got the error:
error: cannot find gov.nasa.jpf.JPF
So I guess, there is something wrong with my configuration, this is my
site.properties file:
------------------------------
user.home = /home/d2b
jpf.home = ${user.home}/Programs/jpf
jpf-core = ${jpf.home}/jpf-core
jpf-symbc = ${jpf.home}/jpf-symbc
extensions=${jpf-core},${jpf-symbc}
------------------------------
Could you tell me how to fix it?

3) Do I need to build jpf-symbc ? I tried bin/ant test and have the
following error:
ERROR: no ant.jar found in known tools dirs (check your
site.properties)
My site.properties file is as above.

Thank you very much.
Best wishes,
Sang

[Corina Pasareanu]

this is what works for me:
java -Djava.library.path=/home/me/workspace/jpf-symbc/lib -jar /home/me/workspace/jpf-core/build/RunJPF.jar /home/me/workspace/jpf-symbc/ExSymExe.jpf

here are the site.properties in my .jpf dir:
jpf-core = ${user.home}/workspace/jpf-core
jpf-symbc = ${user.home}/workspace/jpf-symbc
extensions+=,${jpf-core}
extensions+=,${jpf-symbc}

corina

[Quoc-Sang Phan]

Dear Corina,

I made my site.properties exactly the same as yours:
------------------
user.home = /home/d2b
jpf-core = ${user.home}/Programs/jpf/jpf-core
jpf-symbc = ${user.home}/Programs/jpf/jpf-symbc
extensions+=,${jpf-core}
extensions+=,${jpf-symbc}
------------------
. However, when I run
...:~/Programs/jpf/jpf-symbc$ bin/ant test

I got the following error:

ERROR: no ant.jar found in known tools dirs (check your
site.properties)

Could you please tell me how to fix it?

Best wishes,
Sang

[Quoc-Sang Phan]

I searched past discussions for information

http://groups.google.com/group/java-pathfinder/browse_thread/thread/c98df28c46973c4d/

http://groups.google.com/group/java-pathfinder/browse_thread/thread/4391e7d05f0325e9

There were some people having the same error as mine, but I didn't
find any clue of solution for it.

Sang

[Corina Pasareanu]

can you send the command that you are executing?
no ant.jat is expected
there is an ant in e.g. workspace/jpf-symbc/bin

[Quoc-Sang Phan]

Dear Corina,

I'm executing the shell script "ant" in symbc/bin
d2b@d2b:~/Programs/jpf/jpf-symbc$ bin/ant test

The structure of JPF folder in my environment is as bellow:
/home/d2b/Programs/jpf
/home/d2b/Programs/jpf/jpf-core
/home/d2b/Programs/jpf/jpf-symbc

The content of /home/d2b/Programs/jpf/site.properties

------------------
user.home = /home/d2b
jpf-core = ${user.home}/Programs/jpf/jpf-core
jpf-symbc = ${user.home}/Programs/jpf/jpf-symbc
extensions+=,${jpf-core}
extensions+=,${jpf-symbc}
------------------

My jpf-core and jpf-symbc are latest from Mecurial.

Best wishes,
Sang

On Feb 14, 9:57 pm, Corina Pasareanu <corina.ani...@gmail.com> wrote:
> can you send the command that you are executing?
> no ant.jat is expected
> there is an ant in e.g. workspace/jpf-symbc/bin
>

> On Tue, Feb 14, 2012 at 5:59 AM, Quoc-Sang Phan <dark2bri...@gmail.com>wrote:
>
>
>
>
>
>
>
> > I searched past discussions for information
>

> >http://groups.google.com/group/java-pathfinder/browse_thread/thread/c...
>
> >http://groups.google.com/group/java-pathfinder/browse_thread/thread/4...

[Corina Pasareanu]

did you try running directly:
java -jar tools/RunAnt.jar test

[Quoc-Sang Phan]

Dear Corina,

I already tried, but the result is still the same as running "bin/ant
test"

ERROR: no ant.jar found in known tools dirs (check your
site.properties)

Best wishes,
Sang

[Anwesha Das]

Hi,

   I am using the jpf-core along with jpf-symbc. I need to modify the source code of jpf-symbc. I am unable to compile jpf-symbc because of missing packages certain import statements do not work. I have used the mercurial links available for download for both jpf-core and jpf-symbc(http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc). Can anyone please help me fix the issue of jpf-symbc compilation? If jpf-core and jpf-symbc are incompatible, how do I know the compatible version of jpf-core for the available jpf-symbc?

Thanks and Regards,
Anwesha

[Corina Pasareanu]

hi
the issues should be fixed
are you running java v7?
thanks
corina

--
 
---
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/groups/opt_out.

[Anwesha Das]

yes its open jdk 7, this is what I get when I type "java -version"

java version "1.7.0_25"
OpenJDK Runtime Environment (IcedTea 2.3.10) (7u25-2.3.10-1ubuntu0.12.04.2)
OpenJDK Server VM (build 23.7-b01, mixed mode)

But m unable to compile it says "cannot find gov.nasa.jpf.JPF" when I try to compile .jpf file and

error of imports and missing classes while building jpf-symbc.

Pl let me know.

--
 
---
You received this message because you are subscribed to a topic in the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/java-pathfinder/H4M3Cb0rpOk/unsubscribe.
To unsubscribe from this group and all its topics, send an email to java-pathfind...@googlegroups.com.

[Anwesha Das]

   Could compile it now. There is an issue with the repository, sometimes there are missing files may be, redoing things worked. Yes, both jpf-core and jpf-symbc latest/default ones work may be.

Thanks and Regards,
Anwesha

[Quoc-Sang Phan]

Hi Corina,

I compile SPF v7 successfully. 

But when I run ant/test, there is a test failure:

build.xml:235: Test gov.nasa.jpf.symbc.TestBooleanSpecial1 failed

Attached you will find the full output.

Best wishes,

Sang

[Corina Pasareanu]

ok

thanks for the feedback
well look into it
corina

[Corina Pasareanu]

yes

On Thu, Sep 5, 2013 at 9:50 PM, Anwesha Das <ad...@ncsu.edu> wrote:

Hi,

Can anyone plz confirm whether spf (jpf-symbc) and jpf-core can run .class files? In other words if I donot have the source code (.java file) can I use .class file(bytecode) as input to the JPF to get the result? I have seen the document, I need to test and verify. Could you please tell me the command line argument to (NOT bin/jpf and path to the .jpf file) run a bytecode file, I mean .class file?

Any help is welcome. There are commands given where we are asked to give the application classpath, does that mean the path to .class file generated inside the build folder? Tried that, its not working !!

Thanks and Regards,

Anwesha

--
 
---
You received this message because you are subscribed to a topic in the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/java-pathfinder/H4M3Cb0rpOk/unsubscribe.
To unsubscribe from this group and all its topics, send an email to java-pathfind...@googlegroups.com.

For more options, visit https://groups.google.com/groups/opt_out.

[Quoc-Sang Phan]

Hi Das,

JPF works on bytecode, it doesn't need the source code.

Suppose you are in the "build" folder of your main application. If you don't like the script jpf and the config file, just run:

java -jar /path-to-jpf-folder/jpf-core/build/RunJPF.jar your.package.YourApplication

Sang

[Anwesha Das]

Thanks Phan. Yes, verified that.

Now I want to make jpf-symbc take the annotations like (@symbolic (true) node n) from an external file rather than the .java source code assuming I do not have access to the source code. Basically I want to make JPF follow one path (whatver I give it in terms of true/false or 1/0) instead of it going over all the paths. Any idea where in (file) I need to make changes? Will it be annotationType.java ?

Any suggestions/directions will be helpful !!

Thanks and Regards,
Anwesha

--

 
---
You received this message because you are subscribed to a topic in the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/java-pathfinder/H4M3Cb0rpOk/unsubscribe.
To unsubscribe from this group and all its topics, send an email to java-pathfind...@googlegroups.com.

[Quoc-Sang Phan]

Hi Das,

I think you need to implement it yourself.

If you want to annotate the byte code program in an external file, this file must be a model of the program, e.g. it models the control flow graph.

(the java source code is also a model of the byte code program).

Suppose you only have the bytecode, you need to parse it, build the model, and annotate this model.

It is not difficult, but it will take much effort.

Best wishes,

Sang

[Corina Pasareanu]

you can use a listener for that and force spf take the path you want

corina

--
 
---

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.

[Anwesha Das]

I went through both SymbolicListener.java and SymbolicSequenceListener.java, I need to change the latter SymbolicSequenceListener.java. So it procures the sequence of methods in getmethodsequence() by exploring the chain of choice generators for a given path. But the no. of nodes in the path is defined by control flow graph and the path(nodes in it) is in the form of CG interface, not true/false?

Some idea about changing the listener to follow a path, so that I can still figure out later the feasibility of the entered path based on errors found or not? Any help will be really appreciated.

Thanks and Regards,

Anwesha

On Sat, Sep 7, 2013 at 1:03 PM, Anwesha Das <ad...@ncsu.edu> wrote:

could you please elaborate and explain, where do I feed in the path? All I want is to make SPF follow 1 path. Do I need to write a new listener?

[Kasper Søe Luckow]

Hi Anwesha,

You do not necessarily need to write a new listener for this to work correctly. If you want to force SPF to take a single path (possibly defined by some specification you provide from a file etc.), I would suggest to look at the choiceGeneratorAdvanced method in the PropertyListenerAdapter interface; using this, you can intercept the choice which JPF is advancing to, and force a selection. For inspiration have a look at ASymbolicExecutionTreeListener in the *.symbc.symexectree package which, to some extent, does what you are looking for, but on thread choices instead of path condition choices.

- Kasper

On Saturday, 7 September 2013 19:03:38 UTC+2, Anwesha Das wrote:

could you please elaborate and explain, where do I feed in the path? All I want is to make SPF follow 1 path. Do I need to write a new listener?

On Sat, Sep 7, 2013 at 12:58 PM, Corina Pasareanu <corina...@gmail.com> wrote:

[Anwesha Das]

Seems there is some problem with jpf-symbc. Also changes are pushed often I guess. I am unable to run .jpf file using command line,

inside the jpf-symbc directory, I give bin/jpf <Anyname>.jpf

But it throws error. It works with jpf-core/bin/jpf or runJPF.jar, but not from jpf-symbc. Can someone please explain?

[Corina Pasareanu]

yes we are updating jpf-symbc as we transitioned to v7 recently.

we can not help you unless you give a (small) example, tell us what the error is, ...

thanks

corina

[Anwesha Das]

1. First problem is ant test doesn't work, as earlier mentioned in the thread:

But when I run ant/test, there is a test failure:

build.xml:235: Test gov.nasa.jpf.symbc.TestBooleanSpecial1 failed

2. Second problem is bin/jpf from jpf-symbc doesn't work for compiling .jpf files in symbc:   (as I said runJPF.jar from jpf-core if used, works)

command bin/jpf path/to/jpf/file/TestPaths.jpf  (from within 'jpf-symbc' folder)

The error it gives while compiling is:

[SEVERE] JPF configuration error: error instantiating class.nasa.jpf.symbc.SymbolicInstructionFactory for entry "vm.insn.factory.class":..... [SEVERE] JPF terminated.

3. And finally the third problem is with visualizer (gov/nasa/jpf/symbc/symexectree), it doesn't seem to contain some imported files/packages in SETPrettyPrinter.java, which are att.grappa.* ones

    Specially with the current default mercurial link.

Although the last one may not pose much problem, the others are a problem at times. Please have a look at them.

Thanks and Regards,
Anwesha

[Anwesha Das]

@Corina, @ Kasper and everyone else

In the files of bytecode (symbc.bytecode) say IFEQ.java, if its the first bytecode instruction, conditionvalue is set to false or true and accordingly enters pc_addDet comparator. If I set conditionValue = true or false (whatever I want to) and make the enter one of the branches, and I do that in all the files, I can make SPF follow one path?

I mean for symbolic variables as well, I want it follow a specific path I give, forcing the conditionvalues to be true or false (irrespective of whether the instruction is the first or not)  can make SPF take one of the branches, am I on the right direction?

Please let me know. :-)

Thanks,

Anwesha

[Kasper Søe Luckow]

See below:

On Sunday, 8 September 2013 20:04:18 UTC+2, Anwesha Das wrote:

1. First problem is ant test doesn't work, as earlier mentioned in the thread:

But when I run ant/test, there is a test failure:

build.xml:235: Test gov.nasa.jpf.symbc.TestBooleanSpecial1 failed

I am not getting that error - not even with a fresh clone. Can you maybe be more specific; what is the error result? Are you sure you have the latest revision of SPF?

 

2. Second problem is bin/jpf from jpf-symbc doesn't work for compiling .jpf files in symbc:   (as I said runJPF.jar from jpf-core if used, works)

command bin/jpf path/to/jpf/file/TestPaths.jpf  (from within 'jpf-symbc' folder)

The error it gives while compiling is:

[SEVERE] JPF configuration error: error instantiating class.nasa.jpf.symbc.SymbolicInstructionFactory for entry "vm.insn.factory.class":..... [SEVERE] JPF terminated.

I have fixed this problem now. Apparently RunJPF.jar was an old copy from jpf-core v6 that obviously does not work now :)

 

3. And finally the third problem is with visualizer (gov/nasa/jpf/symbc/symexectree), it doesn't seem to contain some imported files/packages in SETPrettyPrinter.java, which are att.grappa.* ones

    Specially with the current default mercurial link.

Similar to you first issue, I do not experience this. Which revision of SPF are you currently using? I just pushed rev 512, which includes the fixed RunJPF.jar.

 

Although the last one may not pose much problem, the others are a problem at times. Please have a look at them.

Thanks and Regards,
Anwesha

Thanks for you comments. Let me know if you are still experiencing problems.

- Kasper 

[Kasper Søe Luckow]

What you are describing will only apply for if-instructions for which the decision predicate is symbolic. It is not clear to me from your description if that is what you want to achieve; do you want to control branch selection regardless of whether the decision predicate is symbolic or not?

While you probably could do what you are suggesting if you are interested in controlling the selection of branches for if-instructions with symbolic decision predicates, that would require you to modify *all* if-instructions and change their semantics. I think it would be much easier to implement this as a listener thus conceptually being an extension to SPF; whenever JPF is advancing to a new choice (see choiceGeneratorAdvanced in PropertyListener), you can check whether that choice is a path condition choice (formally a PCChoiceGenerator). If it is, you can enforce which branch to follow using the instance method select(i) where i denotes whether to take the true or the false branch.

Let me know if you have further questions :)

[Anwesha Das]

@Kasper,

Thanks a lot for your response. :-)

I downloaded both jpf-core and jpf-symbc after checking the thread,

1. ant test from jpf-symbc still gives errors:

" Caused by: gov.nasa.jpf.symbc.symexectree.visualizer.PrettyPrinterException: java.io.FileNotFoundException: /home/anwesha/projects/jpf/jpf-symbc/prettyprint/gov.nasa.jpf.symbc.symexectree.visualizer.TestCGOptimization$TestSystem.testIF_ICMPEQ.dot (No such file
or directory)"

Its related to the 3rd bullet point I had mentioned.

2nd problem seems to have solved.

Regarding making SPF follow one path, yes I feel that way I mentioned was a crude/inconvenient way.

My aim is to make SPF follow one path for symbolic variables only. So if a variable is symbolic, then all branch statements related to that should follow a path I specify.(sequence of true/false values)

So Is it the symbolicListener or the SymbolicSequenceListener, I should change, advancechoicegenerator can help in controlling the next path, but what about the initial path? How do I specify that?

Thanks and Regards,
Anwesha

[Kasper Søe Luckow]

The first problem seems to be caused by a missing folder, "prettyprint", in the root of jpf-symbc. It is only used as an output folder for the test cases in relation to the symbolic visualizer, but I will add it asap. Thanks for pointing that out.

Regarding your second question; yes, you could use either symbolicListener or SymbolicSequenceListener and enforce choice selection by implementing choiceGeneratorAdvanced - it depends on the purpose of your analysis. E.g. the former will print out a summary of the symbolic information while the latter can be used for JUnit test case generation. In general, a listener is used for monitoring and controlling the operations of JPF according to your needs, and can be used for presenting the results of the analysis e.g. as HTML as is the case with symbolicListener. Maybe it would be better writing a new listener that fits your analysis(?)

Can you elaborate on what you mean by "initial path"? Do you mean the path before reaching the specified symbolic method?

[Anwesha Das]

@Kasper:

What I mean is: say my path is {1 0 1  0}

I want my first branch instruction(switches can also be converted to if else branches, wherever there are 2 possibilities, I tell what to take true or false) to fall to 1, now, advancechoicegenerator can help me from what I understand to go from 1 to 0(1st to 2nd), then 0 to 1(2nd to 3rd). Since that method will be called after the first instruction is executed.

 (No, I am not concerned with the path before reaching symbolic method, since thats deterministic, m concerned with symbolic methods only)

Its like, I have pc.solve's value. I feed in that, accordingly it should fork necessary processes/methods based on what I feed in.

In symbolicListener()  what will be my getTotalNumberOfChoices(), if I want SPF to follow a path?

Thanks,
Anwesha

[Anwesha Das]

Making the IfInstrSymbHelper.java-> getNextInstructionAndSetPCChoice() take the conditionvalue I give, instead of getnextchoice() value can make SPF follow 1 path ( for all ifs) right? Can switch be made to work similarly?

[Kasper Søe Luckow]

Yes, I think you could do that. IfInstrSymbHelper.java is not completely refactored, however - it is in a kind of intermediate (somewhat ugly) state right now. You need to make the changes multiple places in that file for enforcing your functionality for if-instructions regardless of type (long, double, etc.).

[Anwesha Das]

@Kasper,

1. Why do you use 3 comparators for long, double and float?  We need 2 comparators for the rest of ifs with integers? Whats the reason for 3 in the rest?

2. Also, if I over-write a variable defined as symbolic, does that become concrete from symbolic during run-time? Say at one statement in the code I assign a value to a symbolic variable? Does that become concrete after the execution of that line? Please explain.

In that case, I have to look into concrete branching as well, I felt once a variable is declared as symbolic, even if I over-write it remains symbolic, jpf-symbc.

Basically, if I make SPF follow an infeasible path, it should tell me the constraints it violated or errors encountered, its not telling me that.

Thanks and Regards,
Anwesha

[Kasper Søe Luckow]

Hi Anwesha,

1. I suggest you have a look at the semantics of those bytecodes (see e.g. http://docs.oracle.com/javase/specs/jvms/se7/html/jvms-6.html); for example, fcmpl does a floating point *comparison* between two floating point values. The result pushed onto the operand stack subsequently is not a boolean value, but an integer value corresponding to the comparator (>, ==, <) that evaluates to true for the expression.

2: Suppose you wrote something (a bit contrived) like this:

public int driver(int var) {

var = 2;

if(var == 2) {

//do stuff

}

} 

and you run SPF with driver as a symbolic method (i.e. var is symbolic), var you will always enter the body of the if-stmt regardless of whether var was symbolic initially. I suggest you read e.g. Symbolic Execution and Program Testing by King et al. and Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis by Pasareanu et al. Maybe that will help understanding what is going on.

- Kasper

[Corina Pasareanu]

hi

yes once a variable is assigned a concrete value it will be concrete.

why would you expect otherwise?

what errors would you expect on infeasible paths? program errors?

there should be no errors, since the path is infeasible.
perhaps you want to say that you want to write your own code such that to detect if the path is infeasible.

corina

[Anwesha Das]

Consider the following code:

int test(int x,int y)
{

     If (x==1)
     {

         print ("x is one");

         y = 2;

     }

     if (y<2)

        print "y less than two")

    else

       print ("y not less than two")
}

void main(args)

{ 
    int x = 1;

    int y = 1;

    test (x,y)

}

       

in jpf I give symbolic.method = test(sym#sym)

So, I make it follow (true, true), which means both 'if's are made true. (This is an infeasible path, since second if cannot be true, as 'y' is made true after the first 'if' is satisfied).

I never expect program errors, I expect constraint violation errors. In other words, corresponding to an infeasible path, there exists no possible constraints.

In this case the output I get is "x is one" which is correct, as the second 'if' cannot be true, even if I force SPF to follow that path. But the output doesn't say anything about constraint violation, I cannot distinguish the output from the case where, I make it follow path (true,false).

This situation doesn't arise, if I donot make y = 2 inside the first if condition. In that case each of (true,true), (true,false),(false,false) everything works since all these specific paths are feasible. I can make SPF follow one specific path. So does over-writing the 'y' variable as 2 declared as symbolic, make it concrete? OR is it that it remains symbolic, but doesn't show explicitly the constraint violation(or no constraints generated) !!

Please clarify if you are aware.

Thanks and Regards,
Anwesha

[Anwesha Das]

Re-writing one line which had minor spelling error:

"So, I make it follow (true, true), which means both 'if's are made true. (This is an infeasible path, since second if cannot be true, as 'y' is made two after the first 'if' is satisfied)."

[Corina Pasareanu]

SPF performs a symbolic execution of the program. Whenever a path condition becomes unsat, SPF backtracks.

Corina

[Anwesha Das]

Hi

   Is there any way by which I can make the long,float,double variables follow a path based on boolean values(true or false) similar to Integer type? Because of the opcode issue they use 3 comparators, in IFInstrSymbHelper.java file, I am facing some problems, the worst option will be to provide 3 options as input (for each > == <, it can be true or false), but that's not the way. Any help will be really helpful. I want it similar to integer.

And how is "while" condition handled? Same as "if" and "for" ? There are 2 conditions in all kinds of getNextInstructionAndSetPCChoice(), if there is a choice and if there is no choice(first time around), certain times it doesn't go into the second condition(if there is a choice) even though it should. Clarify/give some inputs if you can.

Thanks and Regards,
Anwesha

[Corina Pasareanu]

hi
spf works at bytecode level
you should study a bit how they work

corina

[Anwesha Das]

Hi,

   Could you plz tell me how you handle multi-threading in symbc? I mean for a multi-threaded application, do you make a new thread for a thread in the user code or donot actually make a thread ? How do u exactly handle it?

Thanks and Regards,
Anwesha

[Corina Pasareanu]

you just run your multi threaded appluication inside the tool

corina

[Anwesha Das]

1. I think my question was whether symbc creates a new thread for each thread in the user code, i mean if the user code creates a new thread when running without symbc then when running with symbc, does it still create a new thread?

2. Also, do u handle String in symbolic execution? I saw long,double,float,integer etc. Tested with String in the user source code. Doesn't seem to work. Could you please confirm.

Thanks,
Anwesha

[Willem Visser]

1. Yes every user thread is also a thread in SE

2. There is a facility to handle strings, but it is not that great (and it might have been purged in one of the revisions, so not even sure it is still there). A new one is in the works.

[Corina Pasareanu]

The string handling should be there. we did not remove it from v7 but we did not test it extensively ...

corina

[Anwesha Das]

But I tried testing, it did not work. I used "String" variable for the 'if' branch. Can you point me to the code chunk which handles "String" datatype for symbolic execution?

Thanks and Regrads,
Anwesha

[Anwesha Das]

Hi, please let me know where u handle strings in the code? It would be helpful, since I tested it dint work !!

Also could you please guide as to how you handle multiple threads in symbc?

[Corina Pasareanu]

Hi:

Please write to me directly so that not to inundate the mailing list.

Dod you try to run a multithreaded Java application?

Dd you get an error? It is not clear from your message. There is nothing specific to SPF that you need to do wrt threads.

If you want to report an error please send a small Java program and the jpf config file together with a description of the error.

What exactly did you test wrt strings? It is not clear. Please send your test Java program with jpf config.

Thanks,

Corina

[Anwesha Das]

this is code for string testing:

public static void main(String[] args) {
        String month1 = "June";
        teststring(month1);
    }

public static void teststring(String month1) {
        if (month1 == "July")
                System.out.println("String works");
        else
                System.out.println("String Does not work");
}

In .jpf I have the following:

target=SwitchDemo

classpath=${jpf-symbc}/build/examples
sourcepath=${jpf-symbc}/src/examples

symbolic.method = SwitchDemo.teststring(sym)

#symbolic.debug=true

listener = gov.nasa.jpf.symbc.SymbolicListener

symbolic.min_int=-100
symbolic.max_int=100

symbolic.min_double=-100.0
symbolic.max_double=100.0

I expect it to print both "String works" and "String doesn't work" since month1 is symbolic. But I donot get that, also in the output there is no specification of constraints etc.

Please let me know about it.

Thanks and Regards,

Anwesha

[Anwesha Das]

I figured out the strings execution code in symbc, strings are handled, also I included "package Strings" in the example code. But somehow this example given above doesn't give me the required output. As I wrote earlier I do not get what i expect to get as the output.

Thanks and Regards,
Anwesha

[Quoc-Sang Phan]

SPF failed in Anwesha's example because it doesn't catch IF_ACMPNE.

So the core handles it, the choice generator is ThreadChoiceFromSet of core, not PCChoiceGenerator of SPF.

Sang

[Corina Pasareanu]

what does it mean it "does not catch" IF_ACMPNE.

you would need to turn lazy intyi on if you want to treat reference types symbolically.

regards
corina

--

[Quoc-Sang Phan]

Hi Corina,

In bytecode of SPF, "IF_ACMPNE" is not overridden, so it is handle by bytecode of core.

I will check lazy init.

Sang

[Anwesha Das]

@Corina,

  I am getting confused, could you please direct me to the file where you parse bytecode Strings and call SymbolicStringhandler class?

I mean like IfInstSymHelper and TableSwitch( the respective files in bytecode call them), where do u handle SymbolicStrings?

Who calls SymbolicStringhandler class in bytecode?

Is it inside the translator? Tried with lazy initialization "on", didn't work. Could you tell me why it didn't work?

--
 
---
You received this message because you are subscribed to a topic in the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/java-pathfinder/H4M3Cb0rpOk/unsubscribe.
To unsubscribe from this group and all its topics, send an email to java-pathfind...@googlegroups.com.

[Quoc-Sang Phan]

@Anwesha
SPF does not handle string1 = string2 as in your example.

However, it does handle string1.equals(string2), which is a more common way to compare strings.

A simple search, e.g. by eclipse, will tell you SymbolicStringhandler is only called in 1 place in BytecodeUtils.

[Anwesha Das]

Saw that, "Hampi" library handles that I believe( string1== string2), but couldn't find the SymbolicStringHandler call by bytecodeUtils. Also, couldn't use hampi to execute that.

Could u help me locate the usage in bytecodeutils? I wonder I have it in my version.

--

[Quoc-Sang Phan]

The problem is not hampi.

As I've said in my previous mail, SPF doesn't handle IF_ACMPNE, so there is no PC, hampi or any solver is not called.

In the case of string1.equals(string2), it is translated to Invoke..., and SPF handles it.

Sang

[Anwesha Das]

Could u help me locate SymbolicStringHandler call by bytecodeUtils?

[Quoc-Sang Phan]

I"m using v6 (stable version). I can locate it with Ctrl+F. Can you check?

[Anwesha Das]

Ok it is there in version 6 but not in version 7. Already made changes to version 7 code. Don't know if I revert back to version 6 certain things may stop working !!

[Anwesha Das]

Version 6 doesn't compile correctly like version 7. I needed String and multi-threading to work in version 7, since I already made changes to the code. Let me know of any suggestions. Also the code structure is different, I don't think I can revert back to version 6.

Thanks and Regards,
Anwesha

[Corina Pasareanu]

version 6 should compile correctly. you should use v6 of jpf-core.

please report any compilation errors that you have.

thank you

corina

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.

[Anwesha Das]

Hi Corina,

  What is the status of strings and multi-threading? Earlier you were updating it while moving to version 7. There were missing code patches in string. Is it completed now? Also, is the multi-threading part completely working now?  It would be great if you could let me know.

Thanks and Regards,
Anwesha

[Corina Pasareanu]

Hi:

Yes the multi-threading should be handled. We have also worked on the string part in the past month or two so please try it and let me know about the results (we believe it still needs debugging).

Thank you

Corina

[Anwesha Das]

Hi,

  I am having problem again with running a jpf file from jpf-symbc folder. Last time, the problem was Kasper resolved to fix this was
"Apparently RunJPF.jar was an old copy from jpf-core v6 that obviously does not work now :)"

I downloaded the latest core and symbc on 5th Jan. Can you please check and let me know, how to run jpf from symbc, and if everything is fine?

This is what I get:

[WARNING] unknown classpath element: /home/anwesha/projects/jpf/jpf-shell/build/examples
[SEVERE] JPF configuration error: error instantiating class gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo for entry "vm.classloader.class":
> exception in gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo(gov.nasa.jpf.vm.VM,int):
>> java.lang.NoSuchMethodError: gov.nasa.jpf.Config.getIndexableKey(Ljava/lang/String;I)Ljava/lang/String;
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
[SEVERE] JPF terminated

Thanks and Regards,
Anwesha

[Anwesha]

Hi,

  I needed some help, suggestion regarding using symbc for Tomcat Java application or hadoop. I mean changing the "classpath" parameter in properties file of jpf-symbc does not seem to work. I wish use symbc to do exploration on Tomcat Java code of a hadoop application.

Could I get any viable suggestions please?  :-)

Thanks and Regards,
Anwesha

On Wed, Jan 22, 2014 at 4:48 PM, Kasper Søe Luckow <kslu...@gmail.com> wrote:

Good. I am not using jpf-shell (nor am I maintaining it), so you should probably ask that question on the mailing list. Also be sure to attach the specific build errors you are experiencing.

On Wed, Jan 22, 2014 at 1:24 PM, Anwesha <anwesha....@gmail.com> wrote:

Thanks Kasper, I got it working now. But there is some issue with the jpf shell build. Please check that.

On Tue, Jan 21, 2014 at 4:29 PM, Kasper Søe Luckow <kslu...@gmail.com> wrote:

There must be something wrong with your build or your site.properties file. I cannot reproduce it. Please take a look at why you get the NoSuchMethodError for the getIndexableKey method of Config. That exception is thrown in jpf-core and not in jpf-symbc. Briefly, a NoSuchMethodError means that your compiled classes (in this case Config), does not contain the particular method with that signature. Such errors are typical when you have compiled a class against a different version (that does not have that method) than the one you are actually using when running the application. This makes me almost certain that you have not build your projects properly. Have you by any chance modified getIndexableKey? You could try cleaning jpf-core (and all projects you are depending on) using "ant clean", and then build from scratch all the projects using "ant build".

On Tue, Jan 21, 2014 at 12:46 PM, Anwesha <anwesha....@gmail.com> wrote:

Even without jpf-shell, the error I am getting is :

[SEVERE] JPF configuration error: error instantiating class gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo for entry "vm.classloader.class":
> exception in gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo(gov.nasa.jpf.vm.VM,int):
>> java.lang.NoSuchMethodError: gov.nasa.jpf.Config.getIndexableKey(Ljava/lang/String;I)Ljava/lang/String;
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM

I used bin/ant build to compile both jpf-core and jpf-symbc

I use bin/jpf src/examples/TestPaths.jpf to run but unable to do so. Please help.

Thanks and Regards,
Anwesha

On Tue, Jan 21, 2014 at 3:39 PM, Anwesha <anwesha....@gmail.com> wrote:

I checked, I am using the correct versions. Could you please check why I am unable to compile .jpf file from symbc.

I downloaded the latest build of jpf-shell, and
tried compiling. It gives build errors.

On Wed, Jan 15, 2014 at 4:52 PM, Kasper Søe Luckow <kslu...@gmail.com> wrote:

Looking a bit closer at this issue, it seems to me that something is wrong with your build. How come you get the warning: "[WARNING] unknown classpath element: /home/anwesha/projects/jpf/jpf-shell/build/examples"? That seems to me that you didn't build jpf-shell properly. Otherwise build/examples would be present. Are you sure you have build (using "ant build") jpf-core, jpf-symbc, and jpf-shell (and other projects you might be depending on). Also, please verify that your site.properties are correct. I just did a fresh clone of the repository, and Run*.jar works fine.

On Wed, Jan 15, 2014 at 12:09 PM, Anwesha Das <ad...@ncsu.edu> wrote:

Hi,

 Could you please check back.

On Tue, Jan 14, 2014 at 3:39 PM, Anwesha Das <ad...@ncsu.edu> wrote:

Hi,

  I am having problem again with running a jpf file from jpf-symbc folder. Last time, the problem was Kasper resolved to fix this was

"Apparently RunJPF.jar was an old copy from jpf-core v6 that obviously does not work now :)"

I downloaded the latest core and symbc on 5th Jan. Can you please check and let me know, how to run jpf from symbc, and if everything is fine?

This is what I get:

[WARNING] unknown classpath element: /home/anwesha/projects/jpf/jpf-shell/build/examples
[SEVERE] JPF configuration error: error instantiating class gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo for entry "vm.classloader.class":
> exception in gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo(gov.nasa.jpf.vm.VM,int):
>> java.lang.NoSuchMethodError: gov.nasa.jpf.Config.getIndexableKey(Ljava/lang/String;I)Ljava/lang/String;
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
[SEVERE] JPF terminated

Could you please check back, I really need to work on it.

Thanks and Regards,
Anwesha

--
Anwesha

--
Anwesha

--
Anwesha

--
Anwesha

[Anwesha]

Hi, Can any one suggest me with this? Any pointers would be helpful.

Thanks and Regards,

Anwesha

--
Anwesha

[Anwesha]

Hi,

   If want to make main the symbolic method, assume I have no other functions or even if other functions are there, I want to test main() as symbolic, what needs to be done? I am unable to see symbolic execution in a method, unless the method to be made symbolic is invoked from main with at least once symbolic variable.

Questions are:

1. Can I make main method symbolic, (and hence every functionality within it)

2. Can I make a function (other than main) symbolic, which has no parameter list to be passed? like Test()

but inside the method Test(), I want to do symbolic execution with all the defined variables. is it possible?

3. Can I explicitly prevent symbc from backtracking, once violation happens? If yes, where? I prefer not to touch the jpf core code in search section. Preferably in symbc, anyway to stop backtracking?

If yes, how? Any clarification and suggestion would be really helpful. Please let me know.

Thanks and Regards,
Anwesha

--
Anwesha

[Anwesha]

Can anyone help me please?

Thanks and Regards,
Anwesha

--
Anwesha

[Quoc-Sang Phan]

Hi,

Regarding your questions in the previous post:

1) I don't know. It's possible to declare a static method as symbolic in SPF, but I'm not sure for main.

But is it really necessary? you can always create a fake main, and then pass everything from main to that fake main.

2) Yes. In the body of test(), use, e.g., Debug.makeSymbolicInteger to make symbolic variables.

3) I'm not clear what you want by "prevent SPF from backtracking", since SPF backtracks to find other errors. If you need only one error, you can set multi_error to false.

Sang

[marsand...@gmail.com]

Dear Phan，

I encountered the same problem of yours：

[SEVERE] JPF configuration error: class not found 
gov.nasa.jpf.symbc.SymbolicInstructionFactory by classloader: 
gov.nasa.jpf.JPFClassLoader@10b30a7 
> used within "vm.class" instantiation of class gov.nasa.jpf.jvm.JVM 
[SEVERE] JPF terminated 

could you tell me how did you deal with this error?

thanks!

Jack 

On Monday, February 13, 2012 at 9:15:54 PM UTC+8, Quoc-Sang Phan wrote:

Dear all,

I have some questions about running Symbolic PathFinder (SPF). I need
to use SPF in a shell script, but I find most instructions is for
eclipse. I build jpf-core successfully, and tried with some examples
in jpf-core/src/examples.
When I try jpf-symbc

1) I confuse because there are two shell script jpf in jpf-core/bin
and jpf-symbc/bin. The former calls jpf-core/build/RunJPF.jar, and the
latter calls jpf-symbc/tools/RunJPF.jar. So I don't know which script
or jar file should I use for SPF?

2) I tried with both scripts above with :~/Programs/jpf/jpf-symbc$ jpf
src/examples/TestPaths.jpf
For the one in jpf-core/bin, I got the following error:
-------------------
[SEVERE] JPF configuration error: class not found
gov.nasa.jpf.symbc.SymbolicInstructionFactory by classloader:
gov.nasa.jpf.JPFClassLoader@10b30a7
> used within "vm.class" instantiation of class gov.nasa.jpf.jvm.JVM
[SEVERE] JPF terminated
-------------------

For the one in jpf-symbc/bin, I got the error:
error: cannot find gov.nasa.jpf.JPF
So I guess, there is something wrong with my configuration, this is my
site.properties file:
------------------------------
user.home = /home/d2b
jpf.home = ${user.home}/Programs/jpf
jpf-core = ${jpf.home}/jpf-core
jpf-symbc = ${jpf.home}/jpf-symbc
extensions=${jpf-core},${jpf-symbc}
------------------------------
Could you tell me how to fix it?

3) Do I need to build jpf-symbc ? I tried bin/ant test and have the
following error:
ERROR: no ant.jar found in known tools dirs (check your
site.properties)
My site.properties file is as above.

Thank you very much.
Best wishes,
Sang

[Quoc-Sang Phan]

Hi Jack,

I ran into this error because I made a mistake, but I couldn't remember exactly what it was.

(it has been 3 years). Could you give me some information how you run SPF?

--Sang