63 lines
2.3 KiB
Makefile
63 lines
2.3 KiB
Makefile
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
|