Swapped find and avoid on sim_mgr.explore when using argv claripy

I'll start off by saying this feels like it's got to be something I'm missing, but I don't get it.

I've got this test.c:

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

int main(int argc, char ** argv){
    if (strcmp(argv[1], "asdf")) {
        puts("Great job\n");
    } else {
        puts("Bad job\n");
    }

    return 0;
}

I'm trying to use angr to discover the valid argv[1]. As you can imagine, this is from a CTF challenge, but I've reduced it down to a minimal-seeming test case.

Here's my minimal angr program:

#!/usr/bin/env python3
import angr
import claripy

base_address = 0x100000

win = base_address + 0x1179 
fail = base_address + 0x1187

FLAG_LEN=4

project = angr.Project("./test", main_opts = {'base_addr': base_address})

flag_chars = [claripy.BVS(f'flag_{i}', 8) for i in range(FLAG_LEN)]
flag = claripy.Concat(*flag_chars)

state = project.factory.full_init_state(
    args=["./test", flag]
)

for c in flag_chars: 
    state.solver.add(c >= ord('a')) 
    state.solver.add(c <= ord('z'))

sim_mgr = project.factory.simulation_manager(state)
sim_mgr.explore(find=win, avoid=fail)     

if len(sim_mgr.found) > 0:
    for found in sim_mgr.found:
        print(found.posix.dumps(1))  
        print("[>>] {!r}".format(found.solver.eval(flag,cast_to=bytes)))

I'm running this using the docker image angr/angr at latest, currently 3aee76c1cd7a. Running that gives me varied outputs, but this run it was [>>] b'phah'. Clearly not asdf, right?

I tried swapping out the win/fail addresses for a lambda that detects the right output:

def is_good(state):
    output = state.posix.dumps(1)
    if b'Great' in output:
        return True

sim_mgr = project.factory.simulation_manager(state)
sim_mgr.explore(find=is_good)

Only to get similarly weird output: [>>] b'appb'.

I also tried leaving avoid=fail out entirely, same result.

Then, in despair, I tried swapping the find and avoid parameters (sim_mgr.explore(find=fail, avoid=win)) and it works correctly. Baffling! If I print out state.posix.dumps(1) I see that the find states get "Bad job" and the avoid states get "Great job". I double checked my offsets in Ghidra and Cloud Binja, they look the same. Here's the gdb output on the binary I'm working with, which I compiled as gcc -Wall -O0 -o test test.c:

(gdb) disas main
Dump of assembler code for function main:
   0x0000000000001145 <+0>: push   %rbp
   0x0000000000001146 <+1>: mov    %rsp,%rbp
   0x0000000000001149 <+4>: sub    $0x10,%rsp
   0x000000000000114d <+8>: mov    %edi,-0x4(%rbp)
   0x0000000000001150 <+11>:    mov    %rsi,-0x10(%rbp)
   0x0000000000001154 <+15>:    mov    -0x10(%rbp),%rax
   0x0000000000001158 <+19>:    add    $0x8,%rax
   0x000000000000115c <+23>:    mov    (%rax),%rax
   0x000000000000115f <+26>:    lea    0xe9e(%rip),%rsi        # 0x2004
   0x0000000000001166 <+33>:    mov    %rax,%rdi
   0x0000000000001169 <+36>:    call   0x1040 <strcmp@plt>
   0x000000000000116e <+41>:    test   %eax,%eax
   0x0000000000001170 <+43>:    je     0x1180 <main+59>
   0x0000000000001172 <+45>:    lea    0xe90(%rip),%rdi        # 0x2009
   0x0000000000001179 <+52>:    call   0x1030 <puts@plt>
   0x000000000000117e <+57>:    jmp    0x118c <main+71>
   0x0000000000001180 <+59>:    lea    0xe8d(%rip),%rdi        # 0x2014
   0x0000000000001187 <+66>:    call   0x1030 <puts@plt>
   0x000000000000118c <+71>:    mov    $0x0,%eax
   0x0000000000001191 <+76>:    leave  
   0x0000000000001192 <+77>:    ret    
End of assembler dump.
(gdb) x/s 0x2009
0x2009: "Great job\n"
(gdb) x/s 0x2014
0x2014: "Bad job\n"

I'm seeing the same behavior with a CTF binary (a lot more complicated so it's harder to post here). Other things I tried:

add_options=angr.options.unicorn
remove_options={angr.options.LAZY_SOLVES}
state = project.factory.entry_state( instead of state = project.factory.full_init_state(
Constructing flag as claripy.BVS('whatever', 8*4) instead of a list of single-byte BVSes
Instead of state.solver.add on each flag_char, do state.add_constraints(flag.get_byte(i) >= ord('a')) for each byte of the flag

As you can tell, I'm not a very savvy angr user! I'm definitely cribbing from https://gist.github.com/k3170makan/e01ee70ec1b99b22be36e5fc53d218fa a good bit, as well as the angr CHEATSHEET.md and a bunch of CTF writeups. Working off of argv instead of stdin seems pretty rare in written up challenges, so I feel like I'm probably missing some core thing.

angr / angr-doc

Swapped find and avoid on sim_mgr.explore when using argv claripy #374