Solution: Exercise 02

The following is the solution for Exercise 02.

For this exercise, make sure you run all commands from the directory:

  /path/to/cbat_tools/docs/exercises/02

Task 1

Use wp to find a hex number that represents a correct solution to a 3x3 sudoku cube.

First, run wp on the check function in ./binary/main using --trip-asserts:

    $ bap wp \
          --func=check \
          --trip-asserts \
          binary/main

In response, wp says SAT, which means that wp did find a way to trip the assert.

Next, look at the output to find a sample argument to check. The argument always goes in RDI, so we want to look at RDI. In my case, the output looks like this (yours may not be identical, but it should be close):

SAT!

Model:
	ZF  |->  0x0
	SF  |->  0x0
	RSP |->  0x000000003f800090
	RSI |->  0x0000000000000000
	RDX |->  0x0000000000000000
	RDI |->  0x000000009dee4000  <-- An argument to trip the assert
	RCX |->  0x0000000000000000
	RBP |->  0x0000000000000000
	RAX |->  0x0000000000000000
	R9  |->  0x0000000000000000
	R8  |->  0x0000000000000000
	PF  |->  0x0
	OF  |->  0x0
	CF  |->  0x0
	AF  |->  0x0
	mem_orig |-> [
		else |-> 0x00]
	mem_mod = mem_orig

In this case, it tells me that 0x000000009dee4000 is an argument that I can give to the check function, which will cause it to trip the assert. Try it to confirm it:

    $ ./binary/main 0x000000009dee4000

You will see that it does indeed trip the assert:

+---+---+---+
| 2 | 1 | 3 |
+---+---+---+
| 1 | 3 | 2 |
+---+---+---+
| 3 | 2 | 1 |
+---+---+---+
main: main.c:68: check: Assertion `0' failed.
Aborted

Since the check function only trips the assert for correct solutions, we can conclude that 0x000000009dee4000 is a hex number that represents a correct solution to a 3x3 sudoku cube. If wp suggested to you a different value for RDI, then that number will represent a correct solution too.

Task 2

Convert that hex number to a 3x3 sudoku cube board (draw the board, with the correct 1s, 2s, and 3s in it).

The hex value I received was 0x000000009dee4000. Yours may be different. To convert the hex number to the graphical version of a 3x3 sudoku cube, first convert the number to a binary number (a hex to binary converter is easily found by googling). In my case:

0x000000009dee4000   =>   10011101111011100100000000000000

Every two bits represents a number on the board (the last 12 zeros are just extra padding). We can see this by breaking up the binary number with some spaces:

10 01 11    01 11 10    11 10 01    00000000000000

Put each two-bit chunk onto a 3x3 board, and convert to decimal:

+----+----+----+        +---+---+---+
| 10 | 01 | 11 |        | 2 | 1 | 3 |
+----+----+----+        +---+---+---+
| 01 | 11 | 10 |   =>   | 1 | 3 | 2 |
+----+----+----+        +---+---+---+
| 11 | 10 | 01 |        | 3 | 2 | 1 |
+----+----+----+        +---+---+---+

And with that, you have the graphical version of the board. Of course, the program itself also prints this out for you, which you can use to check your solution. For example, using 0x000000009dee4000:

$ ./binary/main 0x000000009dee4000
+---+---+---+
| 2 | 1 | 3 |
+---+---+---+
| 1 | 3 | 2 |
+---+---+---+
| 3 | 2 | 1 |
+---+---+---+
main: main.c:68: check: Assertion `0' failed.
Aborted

Go back to the list of exercises.