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