Understand the output of JBSE

[danglotb]

Hi,

I am facing an issue on analyzing the output of JBSE.

In fact, I have this method:

public void method(int lit0, int lit1, int lit2) {
    Seller seller = new Seller(lit0, new Item("Potion", lit1));
    Player player = new fPlayer("Timoleon", lit2);
    player.buyItem(potion, seller);
}

The output of the exeuction of JBSE is:

Path condition: 
    {R0} == Object[0] (fresh) &&
    pre_init(fr/inria/stamp/MainTest) &&
    pre_init(fr/inria/stamp/tavern/Seller) &&
    pre_init(fr/inria/stamp/tavern/Item) &&
    pre_init(java/util/ArrayList) &&
    pre_init(java/util/AbstractList) &&
    pre_init(java/util/AbstractCollection) &&
    pre_init(fr/inria/stamp/tavern/Player) &&
    pre_init(java/lang/StringBuilder) &&
    pre_init(java/lang/AbstractStringBuilder) &&
    pre_init(java/lang/System) &&
    {V3} != -2147483648 &&
    {V3} < 0 &&
    {R1} == Object[18] (fresh) &&
    {V16} >= 0 &&
    0 < {V16} &&
     ~ {V3} <= {V18}
    where:
    {R0} == {ROOT}:this &&
    {V3} == {ROOT}:__PARAM[3] &&
    {R1} == [java/lang/AbstractStringBuilder].sizeTable &&
    {V16} == [java/lang/AbstractStringBuilder].sizeTable.length &&
    {V18} == [java/lang/AbstractStringBuilder].sizeTable.[0]

{V3} is the parameter lit3, and has some condition. The most important is: ~ {V3} <= {V18} where {V18} is [java/lang/AbstractStringBuilder].sizeTable.[0].

However, in my code, I don't understand the link between the value of lit3 and the value of the first cell of a table inside java.lang.AbstractStringBuilder.

For more information, please find the code of the both classes Player and Seller:

public class Seller {

    private int gold;

    private List<Item> items;

    public Seller(int gold, Item itemToSell) {
        this.gold = gold;
        this.items = new ArrayList<>();
        this.items.add(itemToSell);
    }

    public Seller(int gold, List<Item> itemsToSell) {
        this.gold = gold;
        this.items = itemsToSell;
    }

    public Item sellItem(String s, Player p) {
        Item i = null;
        for (int i2 = 0; i2 < this.items.size(); i2++) {
            final Item i3 = this.items.get(i2);
            if (i3.name.equals(s)) {
                i = i3;
            }
        }
        if (i != null) {
            final Integer g_p = p.getGold();
            final int value = g_p.compareTo(i.price);
            if (value == 0) {
                this.gold = this.gold + i.price;
                p.giveGold(i.price);
                return i;
            }
            if (value > 0) {
                this.gold = this.gold + i.price;
                p.giveGold(i.price);
                return i;
            }
        }
        return null;
    }
}

public class Player {

    private int gold;
    private List<Item> items;
    private String name;

    public Player(String name, int gold) {
        this.name = name;
        this.gold = gold;
        this.items = new ArrayList<>();
    }

    public String getName() {
        return this.name;
    }

    public int getGold() {
        return gold;
    }

    public void giveGold(int amount) {
        this.gold = this.getGold() - amount;
    }

    public void buyItem(String name, Seller seller) {
        final Item item = seller.sellItem(name, this);
        if (item != null) {
            this.items.add(item);
        }
    }
}

and the whole traces for the given state: trace.txt

Could please explain what I misundertood?

Thank you!

-- Benjamin.

[danglotb]

Hi, I just found where this comparison is done.

My method:

public void method(int lit0, int lit1, int lit2) {
    Seller seller = new Seller(lit0, new Item("Potion", lit1));
    Player player = new fPlayer("Timoleon", lit2);
    player.buyItem(potion, seller);
}

is actually a test, that assert the value of the toString() of both objects Seller and Player. But, before running JBSE, I remove the assertions, but keeps the call to toString() which results with:

public void method(int lit0, int lit1, int lit2) {
    Seller seller = new Seller(lit0, new Item("Potion", lit1));
    Player player = new fPlayer("Timoleon", lit2);
    player.toString();
    seller.toString();
    player.buyItem(potion, seller);
    player.toString();
    seller.toString();
}

I think that JBSE is a little stuck in the exploration on those calls, and with the limit of Depth/Count that I setted, It can't reach another condition.

However, I still do not understand how JBSE builds these predicates.

Cheers,

-- Benjamin.

[pietrobraione]

Hi Benjamin, sorry for my late answer. Analyzing number-to-string conversion code in standard libraries is a quite hard thing for JBSE (and, in my opinion, for any symbolic analysis tool) because of low-level bit twiddling and for the presence of code that manages boundary cases (note, e.g., the clause {V3} != -2147483648, that signifies that there is another path in the code where the case {V3} == -2147483648 is analyzed). Currently I am alone on this project and busy enhancing JBSE so it can analyze Java 8 bytecode, but as soon as I will complete the porting task I will work on models for strings and maps. This said, I have some advices for you. 1- Do not use the master branch of JBSE: this is the Java 8 branch on which I am working, that has some severe regressions. Until it will be ready please use the pre-java8 branch. 2- When you compile your code add the switch to put debug information in the classfiles: JBSE will exploit it to emit more meaningful reports, e.g., it will print {V3} == {ROOT}:lit2 instead of {V3} == {ROOT}:__PARAM[3]. 3- The {R1} == [java/lang/AbstractStringBuilder].sizeTable means that JBSE is assuming that the class java.lang.AbstractStringBuilder was already loaded before the start of symbolic execution. Thus, it will not initialize the static fields of the class (including sizeTable) and will populate them with symbols ({R1} in this case). This is not what you want to do with some standard classes as AbstractStringBuilder. To avoid this you must instruct JBSE to run the static constructor of the class and initialize its static fields. At this purpose create a file, say, /home/braione/mygame.jbse and put in it the following lines:

init begin
java/lang/AbstractStringBuilder
end

then, in the driver code that sets up the parameters and launches JBSE add the line

new SettingsReader("/home/braione/mygame.jbse").fillRunParameters(p);

where p is the RunParameters object you are using to configure JBSE. (note that fillRunParameters throws some checked exceptions, so you should either enclose the above line in a try-catch block or add the exceptions to the signature of the method that contains the line). Best, Pietro