A senario where symbolic execution may be improved ?

[moliam]

In the architecture of Driller, AFL component is augmented by angr. And generally only one path is investigated by the angr component at a time, contrary to purely utilizing angr for testing where all the possible paths can be explored.
Recently I encountered the following scenario where symbolic execution is not very efficient and intelligent:

void foo(char* str)
{
    int n = 0;
    for(int i = 0;i < 10;i++)
    {
        if('A' == str[i])    // symbolic comparison
        {
              n++;
        }
    }
    if(8 == n)   // key point
    {
         /*bug code*/
    }
}

Assume str is a symbolic input. Driller actually cannot calculate the key point comparison because the value of n is constant and key point condition is unsolvable, although it is dependent on the symbolic variable str. Of course the bug code can still be explored after many rounds of interactions between angr and AFL because the condition at the symbolic comparison will be negated many times. But are there any algorithms with which the key point condition can become sovable and be solved at one time ? I think this may greatly improve the efficiency of the symbolic execution engine.

[zardus]

I think what you're describing is essentially the motivating problem for Veritesting (https://users.ece.cmu.edu/~dbrumley/pdf/Avgerinos%20et%20al._2014_Enhancing%20Symbolic%20Execution%20with%20Veritesting.pdf), which is implemented in angr as well (testcases here: https://github.com/angr/angr/blob/master/tests/test_veritesting.py).

Note that our implementation may not create optimal ASTs, and will eventually overwhelm the constraint solver. There is definitely room for implementation improvements there...

[moliam]

Thank you very much. But I cannot find the binary file corresponding to https://github.com/angr/angr/blob/master/tests/test_veritesting.py. Any thing wrong here?

[rhelmot]

(question was answered in a different issue - the binaries are in the angr/binaries repo)