sbv-0.9.17: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

Portability portable experimental erkokl@gmail.com

Data.SBV.Examples.CodeGeneration.GCD

Contents

Description

Computing GCD symbolically, and generating C code for it. This example illustrates symbolic termination related issues when programming with SBV, when the termination of a recursive algorithm crucially depends on the value of a symbolic variable. The technique we use is to statically enforce termination by using a recursion depth counter.

Synopsis

# Computing GCD

sgcd :: (SWord8, SWord8) -> SWord8Source

The symbolic GCD algorithm, over two 8-bit numbers. We define `sgcd (a, 0)` to be `a` for all `a`, which implies `sgcd (0, 0) = 0`. Note that this is essentially Euclid's algorithm, except with a recursion depth counter. We need the depth counter since the algorithm is not symbolically terminating, as we don't have a means of determining that the second argument (`b`) will eventually reach 0 in a symbolic context. Hence we stop after 12 iterations. Why 12? We've empirically determined that this algorithm will recurse at most 12 times for arbitrary 8-bit numbers. Of course, this is a claim that we shall prove below.

# Verification

We prove that `sgcd` does indeed compute the common divisor of the given numbers. Our predicate takes `x`, `y`, and `k`. We show that what `sgcd` returns is indeed a common divisor, and it is at least as large as any given `k`, provided `k` is a common divisor as well.

We have:

````>>> ````prove sgcdIsCorrect
```Q.E.D.
```

# Code generation

Now that we have proof our `sgcd` implementation is correct, we can go ahead and generate C code for it.

This call will generate the required C files. The following is the function body generated for `sgcd`. (We are not showing the generated header, `Makefile`, and the driver programs for brevity.) Note that the generated function is a constant time algorithm for GCD. It is not necessarily fastest, but it will take precisely the same amount of time for all values of `x` and `y`.

```  /* File: "sgcd.c". Automatically generated by SBV. Do not edit! */

#include <inttypes.h>
#include <stdint.h>
#include "sgcd.h"

SWord8 sgcd(const SWord8 x, const SWord8 y)
{
const SWord8 s0 = x;
const SWord8 s1 = y;
const SBool  s3 = s1 == 0x00;
const SWord8 s4 = s0 % s1;
const SWord8 s5 = s3 ? s0 : s4;
const SBool  s6 = 0x00 == s5;
const SWord8 s7 = s1 % s5;
const SWord8 s8 = s6 ? s1 : s7;
const SBool  s9 = 0x00 == s8;
const SWord8 s10 = s5 % s8;
const SWord8 s11 = s9 ? s5 : s10;
const SBool  s12 = 0x00 == s11;
const SWord8 s13 = s8 % s11;
const SWord8 s14 = s12 ? s8 : s13;
const SBool  s15 = 0x00 == s14;
const SWord8 s16 = s11 % s14;
const SWord8 s17 = s15 ? s11 : s16;
const SBool  s18 = 0x00 == s17;
const SWord8 s19 = s14 % s17;
const SWord8 s20 = s18 ? s14 : s19;
const SBool  s21 = 0x00 == s20;
const SWord8 s22 = s17 % s20;
const SWord8 s23 = s21 ? s17 : s22;
const SBool  s24 = 0x00 == s23;
const SWord8 s25 = s20 % s23;
const SWord8 s26 = s24 ? s20 : s25;
const SBool  s27 = 0x00 == s26;
const SWord8 s28 = s23 % s26;
const SWord8 s29 = s27 ? s23 : s28;
const SBool  s30 = 0x00 == s29;
const SWord8 s31 = s26 % s29;
const SWord8 s32 = s30 ? s26 : s31;
const SBool  s33 = 0x00 == s32;
const SWord8 s34 = s29 % s32;
const SWord8 s35 = s33 ? s29 : s34;
const SBool  s36 = 0x00 == s35;
const SWord8 s37 = s36 ? s32 : s35;
const SWord8 s38 = s33 ? s29 : s37;
const SWord8 s39 = s30 ? s26 : s38;
const SWord8 s40 = s27 ? s23 : s39;
const SWord8 s41 = s24 ? s20 : s40;
const SWord8 s42 = s21 ? s17 : s41;
const SWord8 s43 = s18 ? s14 : s42;
const SWord8 s44 = s15 ? s11 : s43;
const SWord8 s45 = s12 ? s8 : s44;
const SWord8 s46 = s9 ? s5 : s45;
const SWord8 s47 = s6 ? s1 : s46;
const SWord8 s48 = s3 ? s0 : s47;

return s48;
}
```