In the high assurance computing world Ada SPARK 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.
package Binary_Search
with SPARK_Mode
is
type T is range 0 .. 10;
subtype U is T range 1 .. 10;
type Ar is array (U) of Integer;
function Search (A : Ar; I : Integer) return T with
-- A is sorted
Pre => (for all I1 in A'Range =>
(for all I2 in I1 .. A'Last =>
A (I1) <= A (I2))),
-- If I exists in A, then Search'Result indicates its position
Post => (if Search'Result in A'Range then A (Search'Result) = I
else (for all Index in A'Range => A (Index) /= I));
pragma Export (C, Search, "SPARK_Search");
end 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.
package main
import "fmt"
/*
#cgo LDFLAGS: ${SRCDIR}/searchlib.a -lgnat
#include <string.h>
extern int SPARK_Search(int[], int);
int Search(int a[], int asize, int findme){
int b[asize];
memcpy(b, a, sizeof(b));
return SPARK_Search(b,findme);
}
*/
import "C"
func main() {
test := []C.int{0, 0, 1, 1, 3, 4, 5, 8, 9}
c := C.Search(&test[0], (C.int)(len(test)), C.int(1))
fmt.Printf("%d\\n", c)
}
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:
$ make
gnatprove -P test.gpr
Phase 1 of 3: frame condition computation ...
Phase 2 of 3: analysis and translation to intermediate language ...
Phase 3 of 3: generation and proof of VCs ...
analyzing Binary_Search, 0 checks
analyzing Binary_Search.Search, 12 checks
Summary logged in /home/poptart/src/go/src/github.com/terrorbyte/gspark/gnatprove/gnatprove.out
gnatmake -c binary_search.adb
gcc -c binary_search.adb
ar rc searchlib.a binary_search.o
go build -o spark_test goexample.go
$ ./spark_test
3