Experiments in using VeriFast verification tool.
These are mostly just explorations of the tool but I am making them available in case they are useful to others. (You will be better served by running through the excellent VeriFast tutorial if you have not already done so.)
I mostly explore this code using the VeriFast the IDE but I am including a Makefile so that I can run regression tests on them.
Similar (possibly better) worked examples of OS kernel-like code:
- verifast/examples/helloproc (all files in the same directory as that file)
Download and install a recent VeriFast release
wget https://github.com/verifast/verifast/releases/download/19.12/verifast-19.12-macos.tar.gz
tar xf verifast-19.12-macos.tar.gz
ln -s verifast-19.12 verifast
# make binaries in release executable on recent MacOS versions
xattr -r -d com.apple.quarantine verifast
All the examples can be checked with this command
make check
[Warning: I am likely to forget to update this – you might want to explore the source directly.]
Current examples (all in the src directory)
-
list.c – singly linked list.
The standard list definition. Included so that it can be reused in other examples.
-
list_generic.c - generic (aka polymorphic) list.
Implementation of a list where the spine of the list contains pointers to the contents of the list. This is not very idiomatic C but it is helpful for exploring polymorphism.
-
alist.c - atomic linked list using a mutex.
The challenge here is that I wanted the mutex to be part of the object it protects.
-
mylock.h and locktest.c - locks that can be stack/statically-allocated.
The challenge here is tweaking the standard mutex definition to allow locks that are not allocated on the heap.
-
wrap.h and wraptest.c - wrapping arithmetic library.
The challenge here is that VeriFast doesn't seem to be very good at reasoning about wrapping integer operations so, to help it out, I carefully implemented 'wrap_add64' and 'wrap_sub64' that perform wrapping addition and subtraction without any intermediate overflow.
-
padding.c - casting between types of different sizes.
The challenge here is that the objects have to be padded with extra space and, when we cast from one to the other, we have to use 'open_struct' and 'chars_join' to convert the object plus its padding back to raw memory and then use 'chars_split' and 'close_struct' to convert raw memory back to an object plus some padding.
-
align.c - reasoning about alignment of objects
The challenge here is saying that a pointer has to be aligned. By itself, this seems to be easy but what is hard is that VeriFast does not support "alignas" or "alignof" so, instead of saying that a global variable has some alignment at the place where it is declared, every use of that global has to add an assumption that it is aligned.
-
malloc0.c - a simplistic memory allocator.
The challenge here is slicing an object off the front of a contiguous block of memory and converting it to a struct.
-
malloc1.c and malloctest.c - a memory allocator that supports free
The challenge here is that entries on the freelist have been padded out to some larger size and we have to use the techniques in padding.c to convert between the two views.
A secondary challenge is that we want all allocations to satisfy some minimum alignment requirement.
These are examples where (as far as I can tell) VeriFast is able to cope with some feature of the C language. (For these examples, I would welcome suggestions for how to change the example so that it is accepted by VeriFast. Especially if the change would not be too large.)
-
struct.c - using structs with a single field to define new types
The challenge here is that VeriFast does not accept passing structs by value; only passing copies of structs by value.