Unsound path condition

[m-carrasco]

Hi,

First of all, thanks for sharing this great project. I really appreciate the work you’ve put into it.

I just wanted to report an issue I came across that seems to lead to an unsound path condition. Specifically, multiple inputs that satisfy the condition end up taking different paths in the code.

In this example, it looks like the addition is being concretized unexpectedly, even though the intermediate values remain symbolic.

I'd love to ask for some help if possible, as I cannot find the root cause of the problem yet.

Input code:

// spout -Dconcolic.bytes=64,53 -cp VERIFIER_JAR:example/ -Dconcolic.execution=true -Dtaint.flow=OFF Main

import tools.aqua.concolic.Verifier;
import java.util.LinkedList;

public class Main {
    public static void main(String[] args)
    {
        LinkedList<Integer> xx = new LinkedList<>();
        xx.add(new Integer(Verifier.nondetByte()));
        
        LinkedList<Integer> yy = new LinkedList<>();
        yy.add(new Integer(Verifier.nondetByte()));

        int xDigit = xx.get(0);

        //if (xDigit == 64){
        //    The symbolic state is correct for this variable (no concretization)
        //    [DECISION] (assert (= #x00000040 ((_ sign_extend 24) __byte_0))) // branchCount=2, branchId=0 
        //    System.out.println("64");
        //}

        int yDigit = yy.get(0);
        //if (yDigit == 53){
        //    The symbolic state is correct for this variable (no concretization)
        //    [DECISION] (assert (= #x00000035 ((_ sign_extend 24) __byte_1))) // branchCount=2, branchId=0
        //    System.out.println("53");
        //}

        long sum = xDigit + yDigit;
        if (sum == 117){ // The operands are symbolic, but the result is concretised
            System.out.println("117");
        }

        System.exit(0);
    }
}

The output path conditions are:

======================== END PATH [BEGIN].
[DECLARE] (declare-fun __byte_0 () (_ BitVec 8))
[WITNESS] Main.java : LMain;.main([Ljava/lang/String;)V : 13 : 64
[DECLARE] (declare-fun __byte_1 () (_ BitVec 8))
[WITNESS] Main.java : LMain;.main([Ljava/lang/String;)V : 16 : 53
======================== END PATH [END].

I have tried a few modifications to the above example and, strangely, fixed/hidden the issue. The next code example works without issues and generates the correct path conditions.

public class Main {
    public static void main(String[] args)
    {
        int xDigit = new Integer(Verifier.nondetByte());
        int yDigit = new Integer(Verifier.nondetByte());

        long sum = xDigit + yDigit;
        if (sum == 117){
            System.out.println("117");
        }

        System.exit(0);
    }
}

The output is:

======================== END PATH [BEGIN].
[DECLARE] (declare-fun __byte_0 () (_ BitVec 8))
[WITNESS] Main.java : LMain;.main([Ljava/lang/String;)V : 12 : 64
[DECLARE] (declare-fun __byte_1 () (_ BitVec 8))
[WITNESS] Main.java : LMain;.main([Ljava/lang/String;)V : 20 : 53
[DECISION] (assert (= ((_ sign_extend 32) (bvadd ((_ sign_extend 24) __byte_1) ((_ sign_extend 24) __byte_0))) #x0000000000000075)) // branchCount=2, branchId=0
======================== END PATH [END].

I think there might be a chance that the internal stack that maintains the annotations could be invalid, which could lead to this error. Otherwise, it is difficult to understand why the first example is buggy, whereas the second one works correctly.

If I could help investigate this further, please let me know!

Best,
Manuel

[m-carrasco]

Hi,

I was able to identify the root cause of the above issue. It is fixed in this PR.

This one is a minimized test case which also reproduces the error:

    public static void main(String[] args)
    {
        int v = Verifier.nondetByte();
        int xDigit = v;
        int p = xDigit;
        long sum = p;
        if (sum == 117) {
            System.out.println("117");
        }
        System.exit(0);
    }

I've noticed that if this test case was simplified further, the generated bytecode would use LLOAD_3 rather than LLOAD <index> and the concretization issue is gone. I inspected the implementation of both handlers and found a likely typo, which if fixed solves the reported issue.

Best,
Manuel

[fhowar]

Thanks for reporting the issue! I will be able to look into this and the other issues after April 5.