angr / angr

A powerful and user-friendly binary analysis platform!
http://angr.io
BSD 2-Clause "Simplified" License
7.48k stars 1.07k forks source link

loop-bound does not work for nested while loop #3516

Open Muqi-Zou opened 2 years ago

Muqi-Zou commented 2 years ago

looks like "bound=1" does not work on following code:

int test6(int input,int input2){
    int temp3;
    temp3 = 1;
    while(input < 120){
        temp3 = temp3+ 1;
        input = input - 1;

        while(input2 < 120){
            temp3 = temp3+ 1;
            input2 = input2 - 1;

        }
    }
    return temp3;
}

You may run pypy3 angr_running.py ./test_whileloop 0 test6 to check it. bug_loop_bound.zip

Muqi-Zou commented 2 years ago

Btw, a few issues here: 1. It looks like the order of successors from the loop_seer is reversed, I mean not the same as what it is without "bound=1"

  1. For the nested forloop (function test4 in the test_whileloop.c), though angr terminates, I do not think it terminates at the correct position, i.e., when bound=1, angr terminates the explored state after executing the same branch instruction third times, which should be twice.
Muqi-Zou commented 2 years ago

I may find the issue there, we may need a handler to handle exits is null.