Constraints not behaving correctly

[bannsec]

It appears that the constraints are not being added when passed to the SimProcedures or something. I have the following C code:

#include <stdio.h>
#include <stdlib.h>

int main() {

    int x;
    char s[8];

    fgets(s,sizeof(s),stdin);

    x = atoi(s);

    if (x == 1337)
        printf("You win!\n");
    else
        printf("You lose!\n");

    return 0;
}

The idea here is to test that tracer will notice the missed branch if I give it, say an input of "2". It does notice the missed branch, but the constraints are messed up. Here's a quick python example:

In [85]: t = tracer.Tracer("./a.out","1")

In [86]: pg = t.next_branch()

In [87]: while pg.missed[0].state.se.any_int(pg.missed[0].state.ip) != 0x4006ad:
    ...:     pg = t.next_branch()
    ...:     
In [88]: pg.missed # Found the branch I want
Out[88]: [<Path with 53 runs (at 0x4006ad)>]

In [89]: pg.missed[0].state.se.constraints
Out[89]: 
[<Bool file_/dev/stdin_252_0_20521_8 == 10>,
 <Bool (0x7fffffffffeff58 + (if (0x1 < (if ((if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) == 0x0) then (if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) else ((if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) + 0x1))) then 0x1 else (if ((if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) == 0x0) then (if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) else ((if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) + 0x1)))) <= 0x7fffffffffeff58>,
 <Bool (0x7fffffffffeff58 + (if (0x1 < (if ((if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) == 0x0) then (if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) else ((if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) + 0x1))) then 0x1 else (if ((if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) == 0x0) then (if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) else ((if (file_/dev/stdin_252_0_20521_8 == 10) then 0x0 else 0x0) + 0x1)))) == 0x7fffffffffeff58>,
 <Bool num_bytes_20531_64 == 0x0>,
 <Bool num_bytes_20532_64 == 0x0>,
 <Bool num_bytes_20533_64 == 0x0>,
 <Bool (if ((if (num_bytes_20533_64 == 0x0) then 0x0 else (if (num_bytes_20533_64 == 0x1) then 0xd0 else (if (num_bytes_20533_64 == 0x2) then 0x8f0 else (if (num_bytes_20533_64 == 0x3) then 0x5a30 else (if (num_bytes_20533_64 == 0x4) then 0x386b0 else (if (num_bytes_20533_64 == 0x5) then 0x2343b0 else (if (num_bytes_20533_64 == 0x6) then 0x160a5b0 else (if (num_bytes_20533_64 == 0x7) then 0xdc679b0 else (if (num_bytes_20533_64 == 0x8) then 0x89c0c1b0 else (if (num_bytes_20533_64 == 0x9) then 0x56187910f else 0x0)))))))))) < 0x7fffffffffffffff) then (if (num_bytes_20533_64 == 0x0) then 0x0 else (if (num_bytes_20533_64 == 0x1) then 0xd0 else (if (num_bytes_20533_64 == 0x2) then 0x8f0 else (if (num_bytes_20533_64 == 0x3) then 0x5a30 else (if (num_bytes_20533_64 == 0x4) then 0x386b0 else (if (num_bytes_20533_64 == 0x5) then 0x2343b0 else (if (num_bytes_20533_64 == 0x6) then 0x160a5b0 else (if (num_bytes_20533_64 == 0x7) then 0xdc679b0 else (if (num_bytes_20533_64 == 0x8) then 0x89c0c1b0 else (if (num_bytes_20533_64 == 0x9) then 0x56187910f else 0x0))))))))))[63:0] else 0x7fffffffffffffff)[31:0] == 0x539>]

In [90]: pg.missed[0].state.satisfiable()
Out[90]: False

Notice that the constraints on this state stdin needs to be "\n", which will obviously never pass the integer check.

Attached is the binary itself:

a.zip

[salls]

Some notes here from our discussion in irc. You will need to call remove_preconstraints() on the missed path, since we preconstrain the input to be what was given initially.

There was a bug on the linux side where we didn't add preconstraints correctly. This is fixed by https://github.com/angr/tracer/commit/58f2dfd9e50a29f0813802529f8411c6eaa91722

Tracer currently limits the size of the input to what was given with this line size=len(self.input))} It might make sense to allow it to be optional

[bannsec]

Awesome. Gonna close this. Two follow-ups I see, one would be adding an example of using tracer (i could submit something, just not sure where to yet), 2 would be agree that size should be optional. I'll open up an issue to track this. Likely should be a strait forward change once all my angr bits start working again!

Thanks!