1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
SDK ?= $(HOME)/.cache/split/microkit-sdk-2.3.1
TOOL ?= $(HOME)/.cache/split/microkit-2.3.1/target/release/microkit
BOARD := $(SDK)/board/qemu_virt_aarch64/debug
CC := aarch64-linux-gnu-gcc
LD := aarch64-linux-gnu-ld
CFLAGS := -std=gnu11 -O2 -g -Wall -Wextra -Werror -Wno-unused-function -ffreestanding -nostdlib -mstrict-align -I$(BOARD)/include
QEMU := qemu-system-aarch64 -machine virt,virtualization=on -cpu cortex-a53 -m 2G -nographic -monitor none -serial stdio
.PHONY: all proof model work demo check run clean
all: build/loader.img
build:
mkdir -p build
build/pager.o: guest/pager.c guest/split.h | build
$(CC) $(CFLAGS) -c $< -o $@
build/alpha.o: guest/client.c guest/split.h | build
$(CC) $(CFLAGS) -DCLIENT=0 -c $< -o $@
build/beta.o: guest/client.c guest/split.h | build
$(CC) $(CFLAGS) -DCLIENT=1 -c $< -o $@
build/unsafe.o: guest/pager.c guest/split.h | build
$(CC) $(CFLAGS) -DSHARED_WRITE=1 -c $< -o $@
build/%.elf: build/%.o
$(LD) -L$(BOARD)/lib $< -lmicrokit -Tmicrokit.ld -o $@
build/loader.img: build/pager.elf build/alpha.elf build/beta.elf guest/split.system
MICROKIT_SDK=$(SDK) $(TOOL) --board qemu_virt_aarch64 --config debug --search-path build -o $@ -r build/report.txt guest/split.system
build/unsafe.img: build/unsafe.elf build/alpha.elf build/beta.elf guest/split.system
sed 's/pager.elf/unsafe.elf/' guest/split.system > build/unsafe.system
MICROKIT_SDK=$(SDK) $(TOOL) --board qemu_virt_aarch64 --config debug --search-path build -o $@ -r build/unsafe.txt build/unsafe.system
proof:
isabelle build -D proof
build/split.ml: proof/Export.thy proof/Reuse.thy proof/Snapshot.thy proof/Execution.thy proof/Protocol.thy proof/Isolation.thy proof/Model.thy proof/ROOT | build
isabelle build -D proof
isabelle export -n -d proof -O build/generated -x 'Split.Export:code/**' Split
cp build/generated/Split.Export/code/split.ocaml $@
build/check: build/split.ml host/check.ml Makefile
ocamlopt -w -a -I build -c build/split.ml
ocamlopt -w +a-4-42-70 -I +unix -I build -c -o build/check.cmx host/check.ml
ocamlopt -I +unix -I build unix.cmxa build/split.cmx build/check.cmx -o $@
model: build/check
build/check --model
work: all build/check
build/check work example/document
demo run: work
check: all build/unsafe.img model
build/check --test
clean:
rm -rf build