104 lines
3.5 KiB
Makefile
104 lines
3.5 KiB
Makefile
.PHONY: check fmt clippy test kani build all image run ci kernel-fmt kernel-clippy kernel-test test-qemu
|
|
|
|
RISCV_TARGET = riscv64gc-unknown-none-elf
|
|
KERNEL_BIN = target/$(RISCV_TARGET)/release/adapter-riscv
|
|
# Harts QEMU boots; `make run-gui SMP=1` for a single core.
|
|
SMP ?= 4
|
|
|
|
KERNEL_CRATES = -p types -p domain -p kernel -p platform
|
|
|
|
all: check fmt clippy test
|
|
|
|
# Gate for kernel work: formatting, lints, unit tests, Kani proofs, RISC-V build.
|
|
ci: kernel-fmt kernel-clippy kernel-test kani build
|
|
|
|
kernel-fmt:
|
|
cargo fmt $(KERNEL_CRATES) -p adapter-riscv -- --check
|
|
|
|
kernel-clippy:
|
|
cargo clippy $(KERNEL_CRATES) --all-targets -- -D warnings
|
|
cargo clippy -p adapter-riscv --target $(RISCV_TARGET) --no-deps -- -D warnings
|
|
|
|
kernel-test:
|
|
cargo test $(KERNEL_CRATES)
|
|
|
|
check:
|
|
cargo check --workspace
|
|
|
|
fmt:
|
|
cargo fmt --all -- --check
|
|
|
|
# Libraries on the host; programs (no_std, they link only for RISC-V) for
|
|
# their target, as `build` builds them. The adapter is `kernel-clippy`'s.
|
|
clippy:
|
|
cargo clippy --workspace --exclude adapter-riscv --lib -- -D warnings
|
|
cargo clippy --target $(RISCV_TARGET) --release $(PROGRAMS) -- -D warnings
|
|
|
|
test:
|
|
cargo test --workspace
|
|
|
|
# CBMC can eat all RAM and take the desktop down with it; cap each run.
|
|
KANI = systemd-run --user --scope -q -p MemoryMax=12G -p MemorySwapMax=0 cargo kani
|
|
|
|
kani-types:
|
|
$(KANI) -p types
|
|
|
|
kani-domain:
|
|
$(KANI) -p domain
|
|
|
|
kani-kernel:
|
|
$(KANI) -p kernel
|
|
|
|
kani: kani-types kani-domain kani-kernel
|
|
|
|
PROGRAMS = -p init -p echo -p sleep -p snake \
|
|
-p display-qemu -p input-qemu -p storage-qemu \
|
|
-p log-server -p permission-manager -p session-server -p smptest -p spawntest -p hello \
|
|
-p terminal-server -p shell -p cat -p ls -p counter -p gatekeeper -p flaky -p tally -p settings -p home
|
|
|
|
# Programs first: the kernel image packs init and storage (see the
|
|
# adapter's build.rs).
|
|
build:
|
|
cargo build --target $(RISCV_TARGET) --release $(PROGRAMS)
|
|
cargo build --target $(RISCV_TARGET) --release -p adapter-riscv
|
|
@# The kernel's tables are one static: if every empty entry is zero it
|
|
@# lives in .bss and costs nothing in the image (see domain::slot).
|
|
@data=$$(llvm-size -A $(KERNEL_BIN) | awk '$$1 == ".data" { print $$2 }'); \
|
|
if [ "$${data:-0}" -gt 16384 ]; then \
|
|
echo "kernel .data is $$data bytes: some table's empty value is not all zero bytes (use domain::slot::Slot)"; exit 1; \
|
|
fi
|
|
|
|
# The keystore holds the owner's sealed keys: made once, never rebuilt.
|
|
KEYS_IMG ?= keys.img
|
|
QEMU_KEYS = -drive file=$(KEYS_IMG),if=none,format=raw,id=ks -device virtio-blk-device,drive=ks \
|
|
-device virtio-rng-device
|
|
|
|
image: build
|
|
scripts/make-disk-image.sh
|
|
[ -f $(KEYS_IMG) ] || truncate -s 64K $(KEYS_IMG)
|
|
|
|
# Boots a test image (normal image + bin/smptest) on $(SMP) harts; init runs
|
|
# the SMP self-test and halts. Passes only on "SMPTEST PASS".
|
|
test-qemu: build
|
|
IMG=test.img SMPTEST=1 scripts/make-disk-image.sh > /dev/null
|
|
SMP=$(SMP) scripts/test-qemu.sh test.img
|
|
|
|
run: build
|
|
qemu-system-riscv64 -machine virt -m 512M -smp $(SMP) -nographic -bios default \
|
|
-kernel $(KERNEL_BIN)
|
|
|
|
run-disk: image
|
|
qemu-system-riscv64 -machine virt -m 512M -smp $(SMP) -nographic -bios default \
|
|
-kernel $(KERNEL_BIN) \
|
|
-drive file=boot.img,if=none,format=raw,id=hd0 \
|
|
-device virtio-blk-device,drive=hd0 $(QEMU_KEYS)
|
|
|
|
run-gui: image
|
|
qemu-system-riscv64 -machine virt -m 512M -smp $(SMP) -bios default \
|
|
-kernel $(KERNEL_BIN) \
|
|
-drive file=boot.img,if=none,format=raw,id=hd0 \
|
|
-device virtio-blk-device,drive=hd0 $(QEMU_KEYS) \
|
|
-device virtio-gpu-device \
|
|
-device virtio-keyboard-device \
|
|
-serial stdio
|