Hello,
When I try to run JPF as shown in the "Using JDart" section, I get a JPF configuration error:

Exception in thread "main" ---------------------- JPF error stack trace ---------------------
JPF configuration error: class not found gov.nasa.jpf.jdart.JDart by classloader: gov.nasa.jpf.JPFClassLoader@5c647e05
at gov.nasa.jpf.Config.asClass(Config.java:1667)
at gov.nasa.jpf.Config.getClass(Config.java:1691)
at gov.nasa.jpf.Config.getInstance(Config.java:1885)
at gov.nasa.jpf.Config.getInstance(Config.java:1880)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:106)

I followed all the required steps in the README.md.
However, if I add ${jpf-jdart} in the extensions property in site.properties file, I pass beyond this error and the shell is loaded (Another error class not found error related to opt4j is generated).

I'm confuzed about this issue, did I do wrong the configuration part ? is it ok if I add jDart to extensions property ?

Best regards,

It would be nice if JDART could poking into the the symbolic execution tree at runtime like SPF, and shows path conditions in a human friendly format :)

Hello,
I think there is a bug in the method gov.nasa.jpf.jdart.ConcolicMethodExplorer.advanceValuation() at line 218, file gov.nasa.jpf.jdart.ConcolicMethodExplorer.java

The original code is:
`for (Variable v : currValuation.getVariables()) {

    if (!nextValuation.containsValueFor(v)) {

      nextValuation.addEntry(new ValuationEntry(v, 
              nextValuation.getValue(v))); // returns the default value for this type
    }
  }

`

I guest that the correct code should be:
` for (Variable v : currValuation.getVariables()) {

    if (!nextValuation.containsValueFor(v)) {

      nextValuation.addEntry(new ValuationEntry(v, 
              currValuation.getValue(v))); //Suggested fix: change nextValuation to currValuation
    }
  }`

Hello,
I noticed an ArrayIndexOutOfBoundsException that occurred on some "switch" statement, here is one of the buggy scripts:

        byte[] buffer = {(byte) 0x97, (byte) 0x10, (byte) 0xDE, (byte) 0x1E, (byte) 0xA0, (byte) 0x40, (byte) 0x31};
        byte cmptr = 0;

        switch(buffer[1]){
        case (byte) 0x00:
            cmptr++;
            break;
        case (byte) 0x01:
            cmptr--;
            break;
        case (byte) 0x02:
            buffer[0]=cmptr;
            break;  

        case (byte) 0x03:
            cmptr=buffer[5];
            break;
        default:
            System.err.println("We have a problem here");
        }

The exception:

Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: -1
at gov.nasa.jpf.jdart.bytecode.TABLESWITCH.getTargetPC(TABLESWITCH.java:54)
at gov.nasa.jpf.jdart.bytecode.SwitchHelper.execute(SwitchHelper.java:60)
at gov.nasa.jpf.jdart.bytecode.TABLESWITCH.execute(TABLESWITCH.java:64)
at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
at gov.nasa.jpf.search.Search.forward(Search.java:579)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
at gov.nasa.jpf.JPF.run(JPF.java:613)
at gov.nasa.jpf.jdart.JDart.run(JDart.java:207)
at gov.nasa.jpf.jdart.JDart.start(JDart.java:131)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:108)

After trying to debug it I found out that the field "targetIdx gets value -1, so when it's passed to getTargetPC(int targetIdx) it raises the exception.
TABLESWITCH.lastIdx also equals -1.

The babelfish.arc.nasa.gov server is not accessible publicly while the Dockerfile still tries to retrieve code from it. Which causes the failure in container initialization. See below extract from Dockerfile:

# Install jpf-core
WORKDIR ${JDART_DIR}
RUN hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core 
# We know that rev 29 works with jdart
WORKDIR ${JDART_DIR}/jpf-core
RUN hg update -r 29
RUN ant 

Hello,

Is it possible to generate an xml version of report ?
trying to add report.publisher+=,xml to a jpf file doesn't seem to include JDart output along with JPF output.

Thanks

Although JDart is able to make an array symbolic element-wise, the size of the array cannot be treated. I understand the difficulty (or even impossibility) for this. But is it possible to assign a constant for such fields in advance? Therefore the field that cannot be treated directly could be assigned a value manually and the test will not crash.

I find that, if a data structure contains enum field, such field won't be made symbolic although I tried to make all fields symbolic.

I totally understand enums are (immutable) objects and cannot be handled directly. And currently I have several makeshifts for this:

1. Add a wrapper for the target function.
   Such wrapper has an integer parameter, which allows the SUT to assign different enum types accordingly. If we change the target function to this wrapper and make the integer parameter symbolic, the enum can be "symbolic" as well.
2. Add an integer field in the data structure to control the enum type accordingly.
   This may require a deep modification for the SUT. I myself don't prefer it.
3. Call getTypeValue() to convert enum to its integer value.
   Then it seems to work for me - the underlying integer value could be symbolic.

Please let me know whether I'm on the right way for this issue or if you have any more suggestions.

Perhaps the documentation can contain such guidance as well? (Please let me know if it already talks about such issue.)

Thanks!

Hi,
Let's say a java project uses some external frameworks or depends on some external jar files. These jar files are set in the classpath of the project. When I run the .jpf file, Jdart and Jpf-core doesn't recognize these jar files. So jdart throws 'ClassNotFound' exception.

How can I add these external jar files to the classpath of jpf-core or jdart ?
Will it solve the issue just by adding these jar files to the classpath ?

Hello,

I encountered a problem when trying to install jdart, could you please help me? I guess the problem should be configuration for z3.

In more detail, I fetched new repositories for jdart (https://github.com/psycopaths/jdart), z3(https://github.com/Z3Prover/z3) and jconstraints-z3 (https://github.com/psycopaths/jConstraints-z3) by git. I already have a compiled jpf-core version 8. My java version is 8 as well.

The ant command at folder jdart/ works well. So do the commands to build z3 (including make install and mvn install:install-file -Dfile=com.microsoft.z3.jar -DgroupId=com.microsoft -DartifactId=z3 -Dversion=0.9 -Dpackaging=jar). But for jconstraints-z3, I get the following error msg for mvn install:
[INFO] Building jConstraints-z3 1.0-SNAPSHOT
[INFO] ------------------------------------------------------------------------
[WARNING] The POM for gov.nasa:jconstraints:jar:0.9.1-SNAPSHOT is missing, no dependency information available
[INFO] ------------------------------------------------------------------------
[INFO] BUILD FAILURE

Therefore, I have to put jconstraints-0.9.1-SNAPSHOT.jar from jdart/lib/ and com.microsoft.z3.jar from z3/build into ~/.jconstraints/extensions as makeshift. After that, I add these two .jar into jpf-jdart.native_classpath inside jpf.properties of jdart/:
jpf-jdart.native_classpath=
....................................
${jpf-jdart}/build/jpf-jdart-annotations.jar;
/home/zzy/.jconstraints/extensions/com.microsoft.z3.jar;
/home/zzy/.jconstraints/extensions/jconstraints-0.9.1-SNAPSHOT.jar

and add jdart into ~/.jpf/site.properties:
jpf.home=/home/zzy/jpf
jpf-core=${jpf.home}/jpf-core
extensions=${jpf-core}
jpf-jdart=${jpf.home}/jdart
extensions+=,${jpf-jdart}

However, when I tried to run ../jpf-core/bin/jpf src/examples/features/simple/test_foo.jpf (the file path is slightly different from README because the one in README does not exist) inside the folder jdart/, I got the following error:
JPF configuration error: error instantiating class gov.nasa.jpf.jdart.JDart for entry "shell":

exception in gov.nasa.jpf.jdart.JDart(gov.nasa.jpf.Config):

java.lang.IllegalArgumentException: 'z3' does not denote a valid constraint solver (provider)

Do I miss anything here? I'm a little confused where jdart looks for z3 so that I seems to not put it at proper places.

One thing I noticed here is that I didn't set JVM_ARGS (but how?....). Because I have no access to jConstraints (https://bitbucket.org/psycopaths/jconstraints) and have no idea what happens there. I'm sorry that I still couldn't understand the relationship between z3, jconstraints-z3 and jconstraints well so far.

My folder structure is like:
~/jpf$ pwd
/home/zzy/jpf
~/jpf$ ls
jconstraints-z3 jpf-core z3 jdart

Thanks in advance!

Hello,
I want to know if it's possible to work with JDart on JavaCard ?
Is it possible to add javacard framework to JPF virtual machine ?

Hi,

I tried to run jdart on Apollo (rjc.zip) that is widely used in the SPF community.

With the same setting to the coral solver, jdart only explored one single path of Apollo because of the UNSAT return when calling coral, while SPF successfully explored Apollo.

Any clue or experience on why jdart fails in this case?

I have an Object named 'md' in the field of my test class, I want to make it and its fields both symbolic. The Object 'md' has two fields which are named 'id' and 'jd' respectively. 'id' and 'jd' are both of primitive type int.
However, when I config as follows:

jdart.configs.cm1analysis.symbolic.include=this.md

I found 'md' is symbolic, but the fields of 'md' are not symbolic.
Here is information shown in the command line:

[FINEST] processing primitive field this.md.id, force: false, makeSymbolic: false

Is there any way to make the field of the field of an Object be forced to be symbolic?
The two fields 'id' and 'jd' are public in Object 'md'.

What is more, when I refer to the field of 'md' by method, for example: using 'md.getId() > 10' instead of 'md.id > 10', JDart seems not working properly?

my test class is shown below:
`
public class MArrayTest {

int[] arr = {1, 2, 3, 4};
MData md = new MData();

public void TestArrayIndex(int i) throws Exception
{
	if (arr[i] > 3)
	{
		System.err.println("errors happen.");
		throw new Exception("some strange errors happen.");
	}
	if (md.getId() > 10)
	{
		System.err.println("Ha Ha!");
	}
	System.err.println("i");
}

public static void main(String[] args) {
	MArrayTest mat = new MArrayTest();
	try {
		mat.TestArrayIndex(0);
	} catch (Exception e) {
		e.printStackTrace();
	}
}

}
`

The type of 'md' which is of name 'MData' is shown below:

`
import java.util.HashMap;

public class MData {

public int id=0;
public int jd=0;
// HashMap<String, String> hm = new HashMap<String, String>();

public MData() {
}

public int getId() {
	return id;
}

public void setId(int id) {
	this.id = id;
}

public int getJd() {
	return jd;
}

public void setJd(int jd) {
	this.jd = jd;
}

}
`

The configuration file is shown below:

`
@using = jpf-jdart
shell=gov.nasa.jpf.jdart.JDart
symbolic.dp=z3
symbolic.dp.z3.bitvectors=true
log.finest=jdart
log.info=constraints

classpath=target/classes

target=MArrayTest
concolic.method.cm1=MArrayTest.TestArrayIndex(i:int)
concolic.method.cm1.config=cm1analysis
jdart.configs.cm1analysis.symbolic.include=this.md
concolic.method=cm1
`

Besides, I want to ask another question: "Does the jpf configuration 'classpath' still hold the same meaning in jdart?"

I tried to use the method mentioned in the README file by
$ docker build -t jdart .
Command to try to install Jdart, unfortunately there was a problem and the installation failed.

The exact reason for the error is shown above. I'm not sure if it's the configuration of my machine that's preventing me from successfully installing the Java8 installer or if it's something else that's causing this result.

JDart currently does not add constraints for array access with a symbolic index.

A solution would be to add the decisions to the constraints tree in all the *ALOAD instructions. The decisions to be added should correspond to accessing all the elements of the array (which has a fixed length), plus two additional decisions corresponding to the two cases where access is out of bounds.

At the moment, there is no regression test suite. The current ant test target does nothing - it refers to JUnit testing and non-existing class files.

It would be nice to have a regression test suite. There are several existing tests, but not utilized by the ant target.

As already decribed in the JPF google group (https://groups.google.com/forum/#!topic/java-pathfinder/lABLeGYc4pw) the vagrant file stopped working due to authorization issues while cloning the jpf-core dependency.

Hi there, I'm new here and I have just investigated JDart about half a month. My requirement now is to extract the path condition of a pair of specific test input, and I just do not know how solve it. I have read paper about JDart and I found similar problem at issue#27. I followed the discussion there and implement a function to parse Node root in InternalConstraintTree but I doesn't work for me (maybe my implementation is not right).

I think I'm now still very confused about how JDart works. I looks like JDart will maintain a symbolic tree during execution and will dynamically update this tree when solved. Thus I want to know is there possible to extract the symbolic tree or maybe there are some more simplistic way to extract path condition for a specific test input? Such as instrument some codes and then execute to obtain path constraints? Anything relevant is welcome, I would very appreciate it if you could help me! Thx!

Dear JDart community,

I'm using JDart these days and I just come up with a problem , that is, how to deal a method with no parameters which could be affected by other methods with symbolic inputs? Just like the following example. IncValue is the class under test. IncValue has two public methods: incVal and examVal. Method incVal requires a integer as input and examVal needs no param.

package simple.noparams;

/**
 *
 * Should we take method without parameters into account?
 * It depends on whether and how a method without parameters
 * are affected by symbolic values that passed in through
 * other methods with parameters.
 *
 * @author Adian
 */
public class IncValue {
    private int val = 1;
    public void incVal(int x) {
        this.val += x;
        if(x > 0)
            System.out.println("Larger val");
        else
            System.out.println("Smaller val");
    }
    public void examVal() {
        System.out.println("(val == x + 1)");
        if(this.val > 0)
            if(this.val < 10)
                System.out.println("(val > 0) && (val < 10)");
            else
                System.out.println("(val >= 10)");
        else
            if(this.val > -5)
                System.out.println("(val < 0) && (val > -5)");
            else
                System.out.println("(val <= -5");
    }
}

Now I want to use the test driver IncValueDriver1 together with the jpf configurations below to executing IncValue. I have noticed that JDart can only execute one method concolically (by set concolic.method=<target_method>), thus I consider the method as the target method under test. Just as the examples shows, the execution of examVal cannot be effected directly from the test driver since it requires no parameter to run, though its execution can be indirectly affected by the value passed in through invoking incVal. The x passed into incVal which will add the field val by x and turns out to effect the result of invoking examVal. I'd like to get the path conditions of executing examVal when a symbolic value x is passed in by invoking incVal. The path conditions I expected looks like ((x+1) > 0) && ((x+1) < 10).

Is there any possible way to implement this? I have noticed that there are some available settings for symbolic fields, (e.g. <prefix>.symbolic), but I not sure how it works. It seems the this in example configurations refers to the instance of test driver, rather than the object (e.g. incValue in my example) created during the execution of test driver. I would appreciate it someone could help, please reply me at your convenience, thanks a lot 😄 !

public class IncValueDriver1 {
    public static void main(String[] args) {
        IncValue incValue = new IncValue();
        incValue.incVal(5);
        incValue.examVal();
    }
}

Here is my configurations:

###############################################################################
#
# default jdart tools
#
# Some how like listeners for SPF and JPF
shell=gov.nasa.jpf.jdart.JDart
symbolic.dp=z3
symbolic.dp.z3.bitvectors=true

###############################################################################
#
# logging and jpf output
#
log.finest=jdart
log.info=constraints

### Common configs for IncValue
concolic.method.incVal=simple.noparams.IncValue.incVal(x:int)
concolic.method.incVal.config=incVal

concolic.method.examVal=simple.noparams.IncValue.examVal()
concolic.method.examVal.config=examVal

### Configs for IncValueDriver1

target=simple.noparams.IncValueDriver1
concolic.method=examVal

## Symbolize object fields
jdart.configs.all_fields_symbolic.symbolic.include=this.*

Hi,
I have a java project (say 'MyProj') with few classes and methods. The JDart project is configured separately.
I want to test a method from MyProj. I can add/include MyProj into JDart in 'Build Path' setting of Eclipse.
The corresponding .jpf file is created inside JDart project. When run, it throws a message cannot load application class .....

It is not always possible to create classes inside JDart project. I may have some existing projects which might not be easy to copy inside JDart project. How can I test such projects ?

Hi,
The paper "The Dart, the Psyco, and the Doop" said that it is allowed to set the return value of a method and instance fields as symbolic variables.

Are there some documents for setting return values of a method as symbolic variables, or some documents for introducing the configuration options of JDart?
Thank you.
Zhen

when I test test_foo.jpf in " C:\Users\asus\jdart\src\examples\features\simple" test work right ,but when I add a method call myMethod and I test it with test_myMethod.jpf nothing happen, I also try to make an other class java in the other repository "C:\Users\asus\jdart\src\examples\features\test" called Testm.java the problem is :

[SEVERE] cannot load application class features.test.Testm

I tried everything without finding any solution [.](url

)

this is my site.properties

jpf-core=C:/Users/asus/git/jpf-core
jpf-jdart=C:/Users/asus/jdart
extensions=${jpf-core},${jpf-symbc}

this is test_myMethod.jpf

@include=./example.jpf

concolic.method=myMethod

this is example.jpf :

@include=../../config/jdart.jpf

target=features.test.Testm

concolic.method.myMethod=features.test.Testm.myMethod(i:int)
concolic.method.myMethod.config=all_fields_symbolic

this using.jpf :

@using = jpf-jdart

target=features.test.Testm

method config jdart

concolic.method.myMethod=features.test.Test.myMethod(i:int)
concolic.method=myMethod

jpf config

jvm.insn_factory.class=gov.nasa.jpf.jdart.ConcolicInstructionFactory
peer_packages=gov.nasa.jpf.jdart.peers;
listener=gov.nasa.jpf.jdart.ConcolicListener
perturb.class=gov.nasa.jpf.jdart.ConcolicPerturbator
search.multiple_errors=true
jdart.concolic_explorer_instance=gov.nasa.jpf.jdart.ConcolicExplorer@jdart-explorer

jdart config

symbolic.dp=z3
symbolic.dp.z3.bitvectors=true

logging

log.finest=jdart
log.info=constraints

Hi,
From the wiki what I understand is:
1- JDart doesn't support string as symbolic. It means I cannot get test case values for a string.
2- JDart supports List and Map but the configuration needs to be different in the jpf file.

Could you please tell me how can I get test case values of List and Map and what what kind of condition I have to write for List and Map in the method, so that Jdart will solve it and will generate some test case values.
If in case it supports string, how can I get the test case value of a string. what configuration I have to write in the jpf file ?

Regards,
S R Giri

Hello,

I felt confused about the configuration option max_depth.

According to WiKi, the resulting constraints tree will in no case be deeper than max_depth. In the implementation, however, it seems max_depth is just ignored during the construction of constraints tree.

if(anaConf.maxDepthExceeded(current.depth)) {
      //System.err.println("DEPTH EXCEEDED");
      return BranchEffect.NORMAL; // just ignore it
 }

Alternatively, max_depth is used when finding the next valuation, i.e., skipping the node that is deeper than the max_depth.

if(anaConf.maxAltDepthExceeded(ad) || anaConf.maxDepthExceeded(currentTarget.depth)) {
      currentTarget.dontKnow();
      continue;
}

As a result, the construction of constraints tree can be get stuck for programs that have deep loops. For example, the iteration of a loop may depend on an input that could be 100,000,000.

for (int i = 0; i < n; i++) {
      ...
}

Am I understanding the implementation correctly?
Any ideas of avoiding the "stuck" in such cases?

Thank you.
Bihuan

I always test a java method in the JDart's Directory , I want to test from a file placed in desktop without moving the file it is possible with JDart ??
if it is possible can someone give me instruction how to do that

How can I get/print the concrete value returned by the function that is executed concolically?

I am not looking to get the post-condition but the value that the function returns when it is normally executed with the current seed used by JDart.

Hello,

I would like to know how could I collect the constraints of the (single) path that is executed when a function is executed with a specific input. Like what is mentioned in this paper in Section 3.3, Termination.

I have downloaded and configured JPF + JDart, went through the JDart github Wiki and experimented with some of the provided examples (mostly in /examples/features/simple).
For example, I have added the following lines at the end of the test_foo.jpf file:
concolic.method.foo.config=foo
jdart.configs.foo.constraints=(i==0)
And it looks like indeed, JDart is only exploring one path as the output says:

. . .
[INFO] ----Constraints Tree Statistics---
[INFO] # paths (total): 1
[INFO] # OK paths: 1
[INFO] # ERROR paths: 0
[INFO] # DONT_KNOW paths: 0

My question is, how can I get the constraints (and in what form) of that single path in the same run?
Additionally, are there any other JDart configurations I can do to optimize the process (like tell it to stop when that path is done and not try to go along another path as it will be impossible anyway given my additional constraint)?

I am new to JDart so any additional information/pointer is very welcome.

Thank you,
Jason

Hi,
I am able to get the test cases printed on the console. But I don't know what configuration I should make in jpf file so that I can get the JUnit test cases and the coverage report.
Please guide me.

Regards,
S R Giri

In the directory jdart/src/examples/features/simple, if run test_ctor.jpf, errors happen. The rest of files are of no problems. The test_ctor.jpf file is about to test the constructor of a class.
Here is the error:
Exception in thread "main" ---------------------- JPF error stack trace ---------------------
JPF configuration error: error instantiating class gov.nasa.jpf.jdart.JDart for entry "shell":

exception in gov.nasa.jpf.jdart.JDart(gov.nasa.jpf.Config):

java.lang.NullPointerException
at gov.nasa.jpf.Config.getInstance(Config.java:2015)
at gov.nasa.jpf.Config.getInstance(Config.java:1889)
at gov.nasa.jpf.Config.getInstance(Config.java:1880)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:106)
Caused by: java.lang.NullPointerException
at gov.nasa.jpf.jdart.config.MethodSpec.parse(MethodSpec.java:33)
at gov.nasa.jpf.jdart.config.MethodSpec.parse(MethodSpec.java:28)
at gov.nasa.jpf.jdart.config.ConcolicMethodConfig.read(ConcolicMethodConfig.java:30)
at gov.nasa.jpf.jdart.config.ConcolicConfig.initialize(ConcolicConfig.java:217)
at gov.nasa.jpf.jdart.config.ConcolicConfig.(ConcolicConfig.java:76)
at gov.nasa.jpf.jdart.JDart.(JDart.java:72)
at sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
at sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
at java.lang.reflect.Constructor.newInstance(Constructor.java:423)
at gov.nasa.jpf.Config.getInstance(Config.java:1985)
... 3 more

Hi,
I have a question on method stubbing. Let's say I want to generate test cases for a method 'testMe(int x, int y)'. And 'testMe()' calls another method 'halfValue(int x)'. I do not want JDart to go inside 'halfValue()' method. Is there anything in JDart which can stub 'halfValue()' ?

public void testMe(int x, int y){
  //do something
  int z = halfValue(y);
  if(z > 10  /* && few more conditions */){
    //do something
  }else{
    //do something
  }
  //do something
}

public int halfValue(int x){
  return x/2;
}

Please note: the halfValue() method works on the input 'y' and the condition in testMe() is based on the returned value from halfValue() method.

Thanks,
S. R. Giri

Does jdart support complex data structure?