# Assignment: SMT

Due: Mon, 04 Apr 2016 23:00:00 -0700

Finish the Z3Py guide and/or the Rosette guide. You may use either tool to finish this assignment.

## Division by constants

The Jitk paper from OSDI’14 (Figure 11; Section 3.2.2) describes an incorrect optimization in the Linux kernel. Consider unsigned integer division `n / k`, where `n` is a 32-bit unsigned integer and `k` is a 32-bit unsigned constant. The incorrect optimization tries to avoid division on the critical path using two steps:
1. precompute a 32-bit unsigned integer `R`; and
2. compute the result using `reciprocal_divide(n, R)`, which uses multiplication and shift only.

In particular, `R` is precomputed as:

and `reciprocal_divide` is implemented as extracting the high 32 bits of the 64-bit product of `n` and `R`:

Take `42 / 3` as an example: precomputing `R` gives `((1ULL << 32) + (3 - 1)) / 3 = 1431655766` and `reciprocal_divide(42, 1431655766)` gives `14`. Unfortunately, this optimization is buggy on some `n` and `k`, as described by commit aee636c4.

#### Question

Is this optimization correct for `k = 3`? If so, prove it. If not, find a counter example.

Figure 10-45 of Hacker’s Delight describes the following optimization that computes `n / k` for the `k = 3` case:

#### Question

Is this optimization correct? If so, prove it. If not, find a counter example.

#### Challenge

The paper Division by Invariant Integers Using Multiplication from PLDI’94 describes a correct optimization that computes `n / k` for a general `k`. This is implemented by Linux kernel’s commit 809fa972 to fix the earlier bug. In this commit correct? Verify its correctness or find a counter example.

As a reference, see similar optimizations and proofs in CompCert.

Write up your answers to the questions, along with any code or proof, in a plain text file named `answers.txt`.

## Network diagnosis

#### Challenge

Design and implement a network diagnosis tool that resembles Anteater from SIGCOMM’11 using SMT. Your tool should work for a network as shown in Figure 3 of the paper, for example, to find loops in a network. You may design an input file format or hard-code the input in code.

## Hash collision generation

#### Challenge

Use SMT to generate MD4 hash collisions. You may find the following references useful.