Problem H
R3: Symbolic Execution

This is the $4$th of $4$ steps in the SRE problem. The complete problem specification is on the NSA Cyber Challenge website.

Encoding

The input lines are binary data encoded as a string using the “hexlify” method (named for the way Python implements it in the binascii module). The binary $16$-bit unsigned integer represented in hexadecimal as 0xBEEF would simply be converted into an ASCII string “beef” (always use lower-case letters). The most significant bytes come first.

Input

The input is a binary MARIE program image represented as a series of hexadecimal strings. Each line will contain one string (a 16-bit word) for each memory location. There will be less than or equal to $4\, 096$ lines.

Output

See the Sample Output for proper formatting. For generating variable names, use “x” plus an Integer starting at 1. So the first variable generated would be “x1”, second variable generated would be “x2”, and so on. For every output instruction encountered (while simulating execution), output a simplified expression. The standard rules for order of operations should affect the ordering of your expression but where it doesn’t affect order of operations, variable names should be output in lexicographic order and constants should be last.

a000
5000
2009
5000
3009
300a
200a
6000
7000
0000
000a

Generated input symbol x1
Generated input symbol x2
Output: x1 + x2 + 10