<!-- vim: set ft=markdown: -->
Hacker handle: `0xc3`

# Notes
Initially, all code is simply copied from the `angr_bf` implementation and `s/bf/mbf/g`'ed.

## Execution instructions
To deduce an input, run `solve_5b.py`. Which class of input is deduced is selectable by setting `CHOSEN_ENDING` in the script. Running it under pypy takes about a minute on my system.

## Alterations and additions to the BF platform for `angr`.

### Changes to the loader
The loader is largely kept the same, but the character set in the regex is extended.

### I/O operations
This modification is very small. It is implemented in the "syscalls", where we simply increment `ptr` after executing the syscall.

### Condition flag
We obviously have to store the condition flag somewhere. For this we add a register, CF, which is a single byte and simply contains 1 or 0 based on whether CF is set or unset.
The implementation of `CLEAR` and `SET` are trivial, but the brace instructions `{` and `}` are more complex.

I re-used `BracketInstruction` class that is used for `[` and `]` with slight modifications (the jump addresses that that class generates jump one instruction _past_ the looping instructions, but since `{` does some important work we don't want to skip it when jumping back). Other than that the `{` and `}` instructions are very similar to `[` and `]`, so their implementation is quite self-explanatory.

### Stack
We maintain an 8-byte stack pointer register, which by default points at 0x90000000. The memory for the stack is 0x8000 bytes long, allocated in the SimOS definition. The memory allocated actually spans from 0x8fffffff to 0x90007fff, for implementation reasons.

We have one push instruction and three pop instructions which vary slightly. The push instruction is simple: we get `ptr` and `sp`, load `val`, store it at `sp`, then increment and put `sp`.

The pop instructions are more complicated, because of the "bottomless" aspect of the stack. `Instruction_POP` is used as a base class and contains `pop_from_stack` which does the basic popping.
We use VEX's if-then-else instruction to fetch either zero or the value at `sp - 1` based on whether our stack pointer is at the base (0x90000000). This is also the reason why our stack starts a byte early; The load is not conditional so we may load from `0x8fffffff` (but then discard the value). To keep `angr` from complaining we simply start the stack slightly early.

We similarly compute the new stack pointer using an if-then-else and put it into `sp`.

Using `pop_from_stack`, the three pop instructions `Instruction_POP`, `Instruction_POPADD`, `Instruction_POPSUB` become trivial to implement.

## Deducing the input
I first found the inputs through a manual concolic-esque exploration; by stepping through the program, looking at the generated inputs, and constraining promising input characters in subsequent runs to prevent path explosion, I eventually found the inputs. There is an easy way of finding the input strings in an automated fashion, however.

The solver script can be found as `solve_5b.py`. It can deduce both the "positive" (help Bon Jovi) and the "negative" (sabotage it) input through a straightforward greedy strategy. We prime the search by fixing the first two characters of stdin for each path (which were found through manual exploration) and then explore the program, stashing states that do not improve on the way. Improvement is defined by gaining characters in the combined concretized values of stdin and stdout that correspond to a simple constraint; they need to be `>= 0x20` and `<= 0xf0`. These 'hyperparameters' were found manually, by starting with a restriction to the printable subset and expanding the upper bound due to the randomly generated characters at the end of the input strings. If a state has fewer valid characters than the other states do, it is immediately discarded. Though this is not a complex strategy it works well enough in this case.

Two model inputs, one for each class, are as follows: `'saBotage_it\xf2_and_end_eveRythi\xcf\x92\x93HNg'` and `'help_bon_Jovi\xfa_to_pLay_his_ms\xe2\x9ap\xf7Ic'`.
