⊕ 2017-06-14
In the high assurance computing world [Ada SPARK](http://www.spark-2014.org/about) is fairly important due to it's formal verification toolkits. Unfortunately it is also not the most friendly language to use in many cases. In order to deal with SPARK's weaknesses and pair in Go's strengths, I decided to use both languages C bindings to integrate SPARK functions into Go to get the best of both worlds.Setting up requires Ada, Go, and the SPARK toolset. In order to test the viability of this I decided to use the Binary_Search example that ships with SPARK. This example searches a set of 0-9 numbers for the first instance and returns it's location in the set. The only change that needs to be made to these examples is to add a pragma Export to the specification file (.ads) before ending a function. The implementation file (.adb) and project file (.gpr) do not need to be modified at all.
1package Binary_Search
2 with SPARK_Mode
3is
4 type T is range 0 .. 10;
5 subtype U is T range 1 .. 10;
6
7 type Ar is array (U) of Integer;
8
9 function Search (A : Ar; I : Integer) return T with
10 -- A is sorted
11 Pre => (for all I1 in A'Range =>
12 (for all I2 in I1 .. A'Last =>
13 A (I1) <= A (I2))),
14 -- If I exists in A, then Search'Result indicates its position
15 Post => (if Search'Result in A'Range then A (Search'Result) = I
16 else (for all Index in A'Range => A (Index) /= I));
17 pragma Export (C, Search, "SPARK_Search");
18
19end Binary_Search;
Proving the code can be done by pointing to the project file with the proof tools: gnatprove -P test.gpr. Read the output and the output file in ./gnatprove/gnatprove.out
When this code is compiled with gnatmake -c binary_search.adb the compiler creates the exported function into binary_search.o. I decided to follow the GNAT User's Guide to create a static archive: ar rc searchlib.a binary_search.o. This could also just as easily turned into a shared object or whatever fits your needs.
Now that there is a static archive created we just need to point cgo to the correct archive and to include the gnat libraries (at the time of writing I didn't try to statically compile the library in): #cgo LDFLAGS: ${SRCDIR}/searchlib.a -lgnat
Finally we make create the calls to the external function that is included: extern int SPARK_Search(int[], int);
This should now be accessible through the C.SPARK_Search call. In the working example I also added a C function to deal with some cgo idiosyncracies that I ran into. A simpe go run should complete successfully.
1package main
2
3import "fmt"
4
5/*
6#cgo LDFLAGS: ${SRCDIR}/searchlib.a -lgnat
7#include <string.h>
8extern int SPARK_Search(int[], int);
9
10int Search(int a[], int asize, int findme){
11 int b[asize];
12 memcpy(b, a, sizeof(b));
13 return SPARK_Search(b,findme);
14}
15*/
16import "C"
17
18func main() {
19 test := []C.int{0, 0, 1, 1, 3, 4, 5, 8, 9}
20 c := C.Search(&test[0], (C.int)(len(test)), C.int(1))
21 fmt.Printf("%d\\n", c)
22}
The fully working example can be viewed here at the git repo. A full run of the program searching for the position of 1 in the set 0, 0, 1, 1, 3, 4, 5, 8, 9 looks like the following:
1$ make
2gnatprove -P test.gpr
3Phase 1 of 3: frame condition computation ...
4Phase 2 of 3: analysis and translation to intermediate language ...
5Phase 3 of 3: generation and proof of VCs ...
6analyzing Binary_Search, 0 checks
7analyzing Binary_Search.Search, 12 checks
8Summary logged in /home/poptart/src/go/src/github.com/terrorbyte/gspark/gnatprove/gnatprove.out
9gnatmake -c binary_search.adb
10gcc -c binary_search.adb
11ar rc searchlib.a binary_search.o
12go build -o spark_test goexample.go
13$ ./spark_test
143