Skip to content

Instantly share code, notes, and snippets.

@cwgreene

cwgreene/gist:ff6dc78942d9dfd612dcc73ae4d19bf2

Last active February 8, 2021 07:56
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save cwgreene/ff6dc78942d9dfd612dcc73ae4d19bf2 to your computer and use it in GitHub Desktop.
Save cwgreene/ff6dc78942d9dfd612dcc73ae4d19bf2 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
The correct code should match 'no\n'. Memory should be 'no\n\x00'.
This is the memory expression at the initial stack offset (it should be 'n')
mem:
memory 0x7fffffffffeff20 8
If
| __eq__
| | __add__
| | | <BV64 0x7fffffffffeff20>
| | | <BV64 packetsize_0_stdin_40_64>
| | <BV64 0x7fffffffffeff20>
| <BV8 0>
| Extract
| | 31
| | 24
| | If
| | | __eq__
| | | | <BV64 packetsize_0_stdin_40_64>
| | | | <BV64 0x4>
| | | <BV32 packet_0_stdin_41_32>
| | | Concat
| | | | Extract
| | | | | 31
| | | | | 8
| | | | | If
| | | | | | __eq__
| | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | <BV64 0x3>
| | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | Concat
| | | | | | | Extract
| | | | | | | | 31
| | | | | | | | 16
| | | | | | | | If
| | | | | | | | | __eq__
| | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | <BV64 0x2>
| | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | Concat
| | | | | | | | | | Extract
| | | | | | | | | | | 31
| | | | | | | | | | | 24
| | | | | | | | | | | If
| | | | | | | | | | | | __eq__
| | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | <BV64 0x1>
| | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | <BV32 0x1000000>
| | | | | | | | | | <BV24 0x0>
| | | | | | | <BV16 0x0>
| | | | <BV8 0>
And here is the global constraint (only the first And clause is relevant, as it's the one that is true when strcmp returns 0).
<Bool strlen_42_64 == 0x3 && (if 0x7fffffffffeff20 + packetsize_0_stdin_40_64 == 0x7fffffffffeff20 then 0 else (if packetsize_0_stdin_40_64 == 0x4 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x3 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x2 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x1 then packet_0_stdin_41_32 else 0x1000000)[31:24] .. 0x0))[31:16] .. 0x0))[31:8] .. 0))[31:24]) == 110 && (if 0x7fffffffffeff20 + packetsize_0_stdin_40_64 == 0x7fffffffffeff21 then 0 else (if packetsize_0_stdin_40_64 == 0x4 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x3 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x2 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x1 then packet_0_stdin_41_32 else 0x1000000)[31:24] .. 0x0))[31:16] .. 0x0))[31:8] .. 0))[23:16]) == 111 && (if 0x7fffffffffeff20 + packetsize_0_stdin_40_64 == 0x7fffffffffeff22 then 0 else (if packetsize_0_stdin_40_64 == 0x4 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x3 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x2 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x1 then packet_0_stdin_41_32 else 0x1000000)[31:24] .. 0x0))[31:16] .. 0x0))[31:8] .. 0))[15:8]) == 10 && strncmp_ret_43_64{UNINITIALIZED} == 0x0 || !(strlen_42_64 == 0x3 && (if 0x7fffffffffeff20 + packetsize_0_stdin_40_64 == 0x7fffffffffeff20 then 0 else (if packetsize_0_stdin_40_64 == 0x4 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x3 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x2 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x1 then packet_0_stdin_41_32 else 0x1000000)[31:24] .. 0x0))[31:16] .. 0x0))[31:8] .. 0))[31:24]) == 110 && (if 0x7fffffffffeff20 + packetsize_0_stdin_40_64 == 0x7fffffffffeff21 then 0 else (if packetsize_0_stdin_40_64 == 0x4 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x3 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x2 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x1 then packet_0_stdin_41_32 else 0x1000000)[31:24] .. 0x0))[31:16] .. 0x0))[31:8] .. 0))[23:16]) == 111 && (if 0x7fffffffffeff20 + packetsize_0_stdin_40_64 == 0x7fffffffffeff22 then 0 else (if packetsize_0_stdin_40_64 == 0x4 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x3 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x2 then packet_0_stdin_41_32 else ((if packetsize_0_stdin_40_64 == 0x1 then packet_0_stdin_41_32 else 0x1000000)[31:24] .. 0x0))[31:16] .. 0x0))[31:8] .. 0))[15:8]) == 10) && strncmp_ret_43_64{UNINITIALIZED} == 0x1>
Or
| And
| | __eq__
| | | <BV64 strlen_42_64>
| | | <BV64 0x3>
| | __eq__
| | | If
| | | | __eq__
| | | | | __add__
| | | | | | <BV64 0x7fffffffffeff20>
| | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | <BV64 0x7fffffffffeff20>
| | | | <BV8 0>
| | | | Extract
| | | | | 31
| | | | | 24
| | | | | If
| | | | | | __eq__
| | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | <BV64 0x4>
| | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | Concat
| | | | | | | Extract
| | | | | | | | 31
| | | | | | | | 8
| | | | | | | | If
| | | | | | | | | __eq__
| | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | <BV64 0x3>
| | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | Concat
| | | | | | | | | | Extract
| | | | | | | | | | | 31
| | | | | | | | | | | 16
| | | | | | | | | | | If
| | | | | | | | | | | | __eq__
| | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | <BV64 0x2>
| | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | Concat
| | | | | | | | | | | | | Extract
| | | | | | | | | | | | | | 31
| | | | | | | | | | | | | | 24
| | | | | | | | | | | | | | If
| | | | | | | | | | | | | | | __eq__
| | | | | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | | | | <BV64 0x1>
| | | | | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | | | | <BV32 0x1000000>
| | | | | | | | | | | | | <BV24 0x0>
| | | | | | | | | | <BV16 0x0>
| | | | | | | <BV8 0>
| | | <BV8 110>
| | __eq__
| | | If
| | | | __eq__
| | | | | __add__
| | | | | | <BV64 0x7fffffffffeff20>
| | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | <BV64 0x7fffffffffeff21>
| | | | <BV8 0>
| | | | Extract
| | | | | 23
| | | | | 16
| | | | | If
| | | | | | __eq__
| | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | <BV64 0x4>
| | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | Concat
| | | | | | | Extract
| | | | | | | | 31
| | | | | | | | 8
| | | | | | | | If
| | | | | | | | | __eq__
| | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | <BV64 0x3>
| | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | Concat
| | | | | | | | | | Extract
| | | | | | | | | | | 31
| | | | | | | | | | | 16
| | | | | | | | | | | If
| | | | | | | | | | | | __eq__
| | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | <BV64 0x2>
| | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | Concat
| | | | | | | | | | | | | Extract
| | | | | | | | | | | | | | 31
| | | | | | | | | | | | | | 24
| | | | | | | | | | | | | | If
| | | | | | | | | | | | | | | __eq__
| | | | | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | | | | <BV64 0x1>
| | | | | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | | | | <BV32 0x1000000>
| | | | | | | | | | | | | <BV24 0x0>
| | | | | | | | | | <BV16 0x0>
| | | | | | | <BV8 0>
| | | <BV8 111>
| | __eq__
| | | If
| | | | __eq__
| | | | | __add__
| | | | | | <BV64 0x7fffffffffeff20>
| | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | <BV64 0x7fffffffffeff22>
| | | | <BV8 0>
| | | | Extract
| | | | | 15
| | | | | 8
| | | | | If
| | | | | | __eq__
| | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | <BV64 0x4>
| | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | Concat
| | | | | | | Extract
| | | | | | | | 31
| | | | | | | | 8
| | | | | | | | If
| | | | | | | | | __eq__
| | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | <BV64 0x3>
| | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | Concat
| | | | | | | | | | Extract
| | | | | | | | | | | 31
| | | | | | | | | | | 16
| | | | | | | | | | | If
| | | | | | | | | | | | __eq__
| | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | <BV64 0x2>
| | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | Concat
| | | | | | | | | | | | | Extract
| | | | | | | | | | | | | | 31
| | | | | | | | | | | | | | 24
| | | | | | | | | | | | | | If
| | | | | | | | | | | | | | | __eq__
| | | | | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | | | | <BV64 0x1>
| | | | | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | | | | <BV32 0x1000000>
| | | | | | | | | | | | | <BV24 0x0>
| | | | | | | | | | <BV16 0x0>
| | | | | | | <BV8 0>
| | | <BV8 10>
| | __eq__
| | | <BV64 strncmp_ret_43_64{UNINITIALIZED}>
| | | <BV64 0x0>
| And
| | Not
| | | And
| | | | __eq__
| | | | | <BV64 strlen_42_64>
| | | | | <BV64 0x3>
| | | | __eq__
| | | | | If
| | | | | | __eq__
| | | | | | | __add__
| | | | | | | | <BV64 0x7fffffffffeff20>
| | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | <BV64 0x7fffffffffeff20>
| | | | | | <BV8 0>
| | | | | | Extract
| | | | | | | 31
| | | | | | | 24
| | | | | | | If
| | | | | | | | __eq__
| | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | <BV64 0x4>
| | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | Concat
| | | | | | | | | Extract
| | | | | | | | | | 31
| | | | | | | | | | 8
| | | | | | | | | | If
| | | | | | | | | | | __eq__
| | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | <BV64 0x3>
| | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | Concat
| | | | | | | | | | | | Extract
| | | | | | | | | | | | | 31
| | | | | | | | | | | | | 16
| | | | | | | | | | | | | If
| | | | | | | | | | | | | | __eq__
| | | | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | | | <BV64 0x2>
| | | | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | | | Concat
| | | | | | | | | | | | | | | Extract
| | | | | | | | | | | | | | | | 31
| | | | | | | | | | | | | | | | 24
| | | | | | | | | | | | | | | | If
| | | | | | | | | | | | | | | | | __eq__
| | | | | | | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | | | | | | <BV64 0x1>
| | | | | | | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | | | | | | <BV32 0x1000000>
| | | | | | | | | | | | | | | <BV24 0x0>
| | | | | | | | | | | | <BV16 0x0>
| | | | | | | | | <BV8 0>
| | | | | <BV8 110>
| | | | __eq__
| | | | | If
| | | | | | __eq__
| | | | | | | __add__
| | | | | | | | <BV64 0x7fffffffffeff20>
| | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | <BV64 0x7fffffffffeff21>
| | | | | | <BV8 0>
| | | | | | Extract
| | | | | | | 23
| | | | | | | 16
| | | | | | | If
| | | | | | | | __eq__
| | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | <BV64 0x4>
| | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | Concat
| | | | | | | | | Extract
| | | | | | | | | | 31
| | | | | | | | | | 8
| | | | | | | | | | If
| | | | | | | | | | | __eq__
| | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | <BV64 0x3>
| | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | Concat
| | | | | | | | | | | | Extract
| | | | | | | | | | | | | 31
| | | | | | | | | | | | | 16
| | | | | | | | | | | | | If
| | | | | | | | | | | | | | __eq__
| | | | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | | | <BV64 0x2>
| | | | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | | | Concat
| | | | | | | | | | | | | | | Extract
| | | | | | | | | | | | | | | | 31
| | | | | | | | | | | | | | | | 24
| | | | | | | | | | | | | | | | If
| | | | | | | | | | | | | | | | | __eq__
| | | | | | | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | | | | | | <BV64 0x1>
| | | | | | | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | | | | | | <BV32 0x1000000>
| | | | | | | | | | | | | | | <BV24 0x0>
| | | | | | | | | | | | <BV16 0x0>
| | | | | | | | | <BV8 0>
| | | | | <BV8 111>
| | | | __eq__
| | | | | If
| | | | | | __eq__
| | | | | | | __add__
| | | | | | | | <BV64 0x7fffffffffeff20>
| | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | <BV64 0x7fffffffffeff22>
| | | | | | <BV8 0>
| | | | | | Extract
| | | | | | | 15
| | | | | | | 8
| | | | | | | If
| | | | | | | | __eq__
| | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | <BV64 0x4>
| | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | Concat
| | | | | | | | | Extract
| | | | | | | | | | 31
| | | | | | | | | | 8
| | | | | | | | | | If
| | | | | | | | | | | __eq__
| | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | <BV64 0x3>
| | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | Concat
| | | | | | | | | | | | Extract
| | | | | | | | | | | | | 31
| | | | | | | | | | | | | 16
| | | | | | | | | | | | | If
| | | | | | | | | | | | | | __eq__
| | | | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | | | <BV64 0x2>
| | | | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | | | Concat
| | | | | | | | | | | | | | | Extract
| | | | | | | | | | | | | | | | 31
| | | | | | | | | | | | | | | | 24
| | | | | | | | | | | | | | | | If
| | | | | | | | | | | | | | | | | __eq__
| | | | | | | | | | | | | | | | | | <BV64 packetsize_0_stdin_40_64>
| | | | | | | | | | | | | | | | | | <BV64 0x1>
| | | | | | | | | | | | | | | | | <BV32 packet_0_stdin_41_32>
| | | | | | | | | | | | | | | | | <BV32 0x1000000>
| | | | | | | | | | | | | | | <BV24 0x0>
| | | | | | | | | | | | <BV16 0x0>
| | | | | | | | | <BV8 0>
| | | | | <BV8 10>
| | __eq__
| | | <BV64 strncmp_ret_43_64{UNINITIALIZED}>
| | | <BV64 0x1>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment