JR and maps

[GAJaloyan]

Hi,

It seems that JR (or SPF) fails on the following small piece of code:

import java.util.Map;
import java.util.TreeMap;
import gov.nasa.jpf.symbc.Debug;

public class Test {
    protected Test() {
        // prevents calls from subclass
        throw new UnsupportedOperationException();
    }

    public static void main(String[] args) {
        Map<String, Object> map1 = new TreeMap<>(String.CASE_INSENSITIVE_ORDER);
        map1.put("key", Debug.makeSymbolicBoolean("test1"));

        Map<String, Object> map2 = new TreeMap<>(String.CASE_INSENSITIVE_ORDER);
        map2.put("key", Debug.makeSymbolicBoolean("test2"));
        System.out.println(map2.get("key"));
    }
}

When trying to debug, I see that the fieldAttr of the value associated to the key is an ObjectList of Boolean, containing both symbolic booleans that I created (while it should be a sole Boolean).

This results in the following crash:

gov.nasa.jpf.util.ObjectList$Node cannot be cast to gov.nasa.jpf.symbc.numeric.Expression
java.lang.ClassCastException: gov.nasa.jpf.util.ObjectList$Node cannot be cast to gov.nasa.jpf.symbc.numeric.Expression
    at gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil.isSymCond(SpfUtil.java:83)
    at gov.nasa.jpf.symbc.VeritestingListener.executeInstruction(VeritestingListener.java:319)
    at gov.nasa.jpf.vm.VM.notifyExecuteInstruction(VM.java:793)                                      
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1904)

Given that symbolic values seem to work pretty well with everything else (except maps), I assume that there is a wrong interaction between both that makes everything crash. The same bug happens if I replace TreeMaps by HashMaps.

Regards, Georges-Axel.

PS: this is the jpf file that I use:

classpath=/private/tmp/test/reproducer/build/test.jar
symbolic.debug=false
symbolic.lazy=false
veritestingMode = 5
performanceMode = true
search.multiple_errors=true
symbolic.dp=z3bitvectorinc
listener = .symbc.VeritestingListener,gov.nasa.jpf.symbc.numeric.solvers.IncrementalListener
symbolic.optimizechoices=false
jitAnalysis = true

[sohah]

Hi,

I am unable to reproduce the exception. It seems that you had a problem and tried to strip away some code to maybe take some private code out or to try to simplify the problem. However, while trying to do so, it looks like some important code is missing. For instance, I do not see a symbolic if-statement for which JR is going to try to do path merging on. I also see the throw statement at the constructor, which is going to be executed the first thing and thus terminating before execution is allowed to go to "main". Finally, I do not see in the jpf configuration the setup for the specific symbolic method that you would want to symbolically execute.

I tried however to write some code that uses maps in the way you described above, thinking that this is what is causing you the problem, but I couldn't reproduce the error there either. It seems that JR is terminating successfully with no exception.

The code I tried is below, along with the jpf file. If you can manipulate these to expose the problem, then I can see it too and I would be able to help.

P.S. Can you pass your email or include it with your profile? It might be useful to talk directly to speed up the process of solving of issues. Mine is "husseinsoh [at] gmail [dot] com" or "soha [at] umn [dot] edu".

import java.util.Map;
 import java.util.TreeMap;

 import gov.nasa.jpf.symbc.Debug;

 public class Issue1 {
    protected Issue1() {
        // prevents calls from subclass
//        throw new UnsupportedOperationException();
    }

    public static void main(String[] args) {
        (new Issue1()).invokeMap(1);
    }

    public int invokeMap(int x) {
        if (x > 100) {
            Map<String, Object> map1 = new TreeMap<>(String.CASE_INSENSITIVE_ORDER);
            map1.put("key", Debug.makeSymbolicBoolean("test1"));

            Map<String, Object> map2 = new TreeMap<>(String.CASE_INSENSITIVE_ORDER);
            map2.put("key", Debug.makeSymbolicBoolean("test2"));
            System.out.println(map2.get("key"));

            x = x + 3;
        }
        return x;
    }
}

The jpf configuration file is:

target=Issue1
classpath=${jpf-symbc}/build/examples
symbolic.debug=false
symbolic.lazy=false
veritestingMode = 5
performanceMode = true
search.multiple_errors=true
symbolic.dp=z3bitvectorinc

symbolic.method=Issue1.invokeMap(sym)

#listener = .symbc.SymbolicListener,gov.nasa.jpf.symbc.numeric.solvers.IncrementalListener

listener = .symbc.VeritestingListener,gov.nasa.jpf.symbc.numeric.solvers.IncrementalListener
symbolic.optimizechoices=false
jitAnalysis = true

[GAJaloyan]

Hi Sohah,

I pulled the latest version from jpf-core, and it seems to have solved the issue.

Regards, Georges-Axel.