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:

	uint64_t k64 = (uint64_t)k;
	return (uint32_t)(((UINT64_C(1) << 32) + (k64 - 1)) / k64);

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

uint32_t reciprocal_divide(uint32_t n, uint32_t R)
	return (uint32_t)(((uint64_t)n * (uint64_t)R) >> 32);

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.


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:

uint32_t divu3(uint32_t n)
	uint32_t r = (0x55555555 * n + (n >> 1) - (n >> 3)) >> 30;
	return (n - r) * 0xaaaaaaab;


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


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


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


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