rajamesandClaude Opus 5.5
294e69463a
One boot, v4/system/boot.c, for both products: it starts the nucleus image, finds each capsule in the baked capsule directory, recomputes its hash, checks its signature, gives its blocks to the node a line at a time, and prints PARITY:V4_NUCLEUS, PARITY:V4_CAPSULE and PARITY:OK before the prompt. A line the node does not accept ends the boot with the capsule, block and line named. docs/v4.0.0/NUCLEUS.md. - hosted Linux product for amd64, aarch64 and riscv64 (make -C v4 hosted); make -C v4 hosted-check boots all three and requires identical output - the kernel's v4 entry (STARFORTH_V4=1) calls the same boot - capsules/v4/forth79.4th, block 6000: no definitions yet - mkimage builds the nucleus only; no FORTH source is compiled at build time - capsule_blocks.c: the Block-header parse, free of any VM, for every loader Verified: make -C v4 test passes; hosted-check passes on the three ISAs with the same hashes; the kernel compiles with STARFORTH_V4=1 on the three. Not verified: no bare-metal boot of v4 has been run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
215 lines
10 KiB
Makefile
215 lines
10 KiB
Makefile
# v4/Makefile -- host golden model build.
|
|
#
|
|
# JUSTIFICATION.md section 5: the host node runs the same mesh-defined
|
|
# instruction set as the hardware, so the C99 model is the reference the
|
|
# hardware is compared against -- not a host-specific reimplementation.
|
|
# There is consequently nothing v4-specific in the architecture here; the
|
|
# build is plain hosted C99 and the ISA is defined in DECOMPOSITION.md.
|
|
#
|
|
# The two builds that matter are the two cell widths. v4/Makefile builds and
|
|
# runs the tests at both, because a width-dependent bug that only appears at
|
|
# 32 bits is exactly the failure mode the F18's 32-bit cells invite and
|
|
# exactly the one a 64-bit-only test run would miss.
|
|
#
|
|
# C99, warnings fatal. A warning here is a defect in a model whose only job
|
|
# is to be trusted.
|
|
|
|
CC ?= cc
|
|
CSTD := -std=c99
|
|
WARN := -Wall -Wextra -Wpedantic -Werror
|
|
OPT ?= -O2 -g
|
|
CFLAGS ?= $(CSTD) $(WARN) $(OPT)
|
|
|
|
# Anchor everything to this Makefile's directory so the build behaves the same
|
|
# whether it is invoked as `make -C v4 test` or `make -f v4/Makefile test`
|
|
# from the repository root. Without this the wildcards below silently expand
|
|
# to nothing from the root and the build "succeeds" having compiled no tests.
|
|
HERE := $(patsubst %/,%,$(dir $(abspath $(lastword $(MAKEFILE_LIST)))))
|
|
|
|
SRCS := $(wildcard $(HERE)/src/*.c)
|
|
TESTS := $(wildcard $(HERE)/tests/*.c)
|
|
|
|
# Cell widths to build and verify. 32 is the F18/Zynq case, 64 the aarch64
|
|
# host case; see DECOMPOSITION.md D-5.
|
|
WIDTHS := 32 64
|
|
|
|
BINDIR := $(HERE)/build
|
|
|
|
# Node memory is a build parameter (V4_NODE_WORDS, node.h; 1024 words unless
|
|
# set). A mesh node is small, but the host node holds the compiler, the
|
|
# dictionary and the text being compiled (JUSTIFICATION.md section 9), which
|
|
# do not fit 1024 words. Tests named test_host_*.c are therefore built with a
|
|
# host node of HOST_WORDS words; every other test keeps the mesh-node size.
|
|
#
|
|
# The host node's stacks are deeper too (DECOMPOSITION.md D-17): 32 values and
|
|
# 32 return entries, where a mesh node has the F18's 10 and 9. The stack is
|
|
# its top registers and a ring; the ring sizes are what is set here.
|
|
HOST_WORDS := 16384
|
|
HOST_DATA_RING := 30
|
|
HOST_RET_RING := 31
|
|
node_size = $(if $(findstring /test_host_,$(1)),-DV4_NODE_WORDS=$(HOST_WORDS) -DV4_DATA_RING=$(HOST_DATA_RING) -DV4_RET_RING=$(HOST_RET_RING))
|
|
|
|
# The capsule sources: definitions as text (include/v4/text.h), which tests
|
|
# assemble onto a node. The directory is passed to the tests so that they
|
|
# find the files whatever directory make was run from.
|
|
CAPSULES := $(wildcard $(HERE)/capsule/*.v4)
|
|
capsule_dir := -DV4_CAPSULE_DIR='"$(HERE)/capsule"'
|
|
|
|
# THE NUCLEUS IMAGE. tools/mkimage.c, built for the host node (HOST_WORDS
|
|
# and the host stack sizes) at one cell width, assembles the nucleus --
|
|
# capsule/*.v4 -- and writes it as a C file, $(BINDIR)/v4_image_<width>.c.
|
|
# The hosted system below and the bare-metal kernel (kernel/Makefile,
|
|
# STARFORTH_V4=1) link the 64-bit one. docs/v4.0.0/NUCLEUS.md.
|
|
HOST_DEFS := -DV4_NODE_WORDS=$(HOST_WORDS) -DV4_DATA_RING=$(HOST_DATA_RING) -DV4_RET_RING=$(HOST_RET_RING)
|
|
ENGINE_SRCS := $(addprefix $(HERE)/src/,node.c exec.c stack.c iword.c heat.c guard.c image.c)
|
|
|
|
define IMAGE_RULE
|
|
$(BINDIR)/mkimage-$(1): $(HERE)/tools/mkimage.c $$(SRCS) $$(wildcard $(HERE)/include/v4/*.h) $(HERE)/tests/host_map.h $(HERE)/Makefile
|
|
@mkdir -p $(BINDIR)
|
|
$$(CC) $$(CFLAGS) -I$(HERE)/include -DV4_CELL_BITS=$(1) $(HOST_DEFS) $(capsule_dir) $(HERE)/tools/mkimage.c $$(SRCS) -o $$@
|
|
|
|
$(BINDIR)/v4_image_$(1).c: $(BINDIR)/mkimage-$(1) $$(CAPSULES)
|
|
$(BINDIR)/mkimage-$(1) $$@
|
|
endef
|
|
$(foreach w,$(WIDTHS),$(eval $(call IMAGE_RULE,$(w))))
|
|
|
|
.PHONY: image
|
|
image: $(foreach w,$(WIDTHS),$(BINDIR)/v4_image_$(w).c)
|
|
|
|
# THE HOSTED SYSTEM: StarForth v4 as a Linux program, a product, for amd64,
|
|
# aarch64 and riscv64 -- $(BINDIR)/starforth4-<isa>. It is the engine, the
|
|
# 64-bit nucleus image, the capsule directory and the boot (system/boot.c)
|
|
# that loads the capsules from it: the same four the kernel links. The
|
|
# directory is made by the repository's own tools/mkcapsule.c from
|
|
# ../capsules, signed if the key is on this machine (kernel/Makefile,
|
|
# SIGN_KEY), and the code that reads it is the kernel's, compiled here as it
|
|
# is there. The binaries are static, so the two foreign ones run under
|
|
# user-mode QEMU with nothing else installed.
|
|
ROOT := $(abspath $(HERE)/..)
|
|
HOSTED_ISAS := amd64 aarch64 riscv64
|
|
CC_amd64 ?= cc
|
|
CC_aarch64 ?= aarch64-linux-gnu-gcc
|
|
CC_riscv64 ?= riscv64-linux-gnu-gcc
|
|
RUN_amd64 ?=
|
|
RUN_aarch64 ?= qemu-aarch64
|
|
RUN_riscv64 ?= qemu-riscv64
|
|
|
|
SIGN_KEY ?= /home/rajames/CLionProjects/lithosananke-ca/intermediate/snakeoil-intermediate.key
|
|
SIGN_KEY_ARGS = $(if $(wildcard $(SIGN_KEY)),--sign-key $(SIGN_KEY),)
|
|
CRYPTO_SRCS := $(addprefix $(ROOT)/kernel/src/crypto/,ed25519.c fe25519.c scalar25519.c sha512.c)
|
|
MKCAPSULE_SRCS := $(ROOT)/tools/mkcapsule.c $(ROOT)/tools/pkcs8_ed25519.c $(CRYPTO_SRCS)
|
|
CAPSULE_FILES := $(shell find $(ROOT)/capsules -type f ! -name '.*' 2>/dev/null)
|
|
CAPSULE_DIR_C := $(BINDIR)/capsule_generated.c
|
|
|
|
# the kernel's capsule code: find, check the hash, verify the signature,
|
|
# split a payload into blocks
|
|
SYSTEM_SRCS := $(HERE)/system/boot.c \
|
|
$(addprefix $(ROOT)/kernel/src/capsule/,capsule_find.c capsule_validate.c capsule_sig.c capsule_blocks.c) \
|
|
$(ROOT)/kernel/src/hash/xxhash64.c $(ROOT)/kernel/src/crypto/x509_ed25519.c $(CRYPTO_SRCS)
|
|
# The kernel's sources are held to the kernel's warnings, not this model's.
|
|
SYSTEM_CFLAGS := $(CSTD) -Wall -Wextra $(OPT) -I$(HERE)/include -I$(ROOT)/kernel/include -I$(ROOT)/v3/include \
|
|
-DV4_CELL_BITS=64 $(HOST_DEFS)
|
|
|
|
$(BINDIR)/mkcapsule: $(MKCAPSULE_SRCS)
|
|
@mkdir -p $(BINDIR)
|
|
cc -std=c99 -Wall -Wextra -O2 -I$(ROOT)/v3/include -I$(ROOT)/kernel/include -I$(ROOT)/tools -o $@ $(MKCAPSULE_SRCS)
|
|
|
|
$(CAPSULE_DIR_C): $(BINDIR)/mkcapsule $(CAPSULE_FILES)
|
|
$(BINDIR)/mkcapsule $(SIGN_KEY_ARGS) $(ROOT)/capsules $@
|
|
|
|
define HOSTED_RULE
|
|
$(BINDIR)/starforth4-$(1): $(HERE)/tools/hosted.c $(BINDIR)/v4_image_64.c $(CAPSULE_DIR_C) $$(ENGINE_SRCS) $$(SYSTEM_SRCS) $$(wildcard $(HERE)/include/v4/*.h) $(HERE)/Makefile
|
|
$$(CC_$(1)) $$(CFLAGS) -D_POSIX_C_SOURCE=200809L -I$(HERE)/include -DV4_CELL_BITS=64 $(HOST_DEFS) -c $(HERE)/tools/hosted.c -o $(BINDIR)/hosted-$(1).o
|
|
$$(CC_$(1)) $$(SYSTEM_CFLAGS) -static $(BINDIR)/hosted-$(1).o $(BINDIR)/v4_image_64.c $(CAPSULE_DIR_C) $$(ENGINE_SRCS) $$(SYSTEM_SRCS) -o $$@
|
|
|
|
$(BINDIR)/boot-$(1).txt: $(BINDIR)/starforth4-$(1)
|
|
@echo " [hosted $(1)]"
|
|
@$$(RUN_$(1)) $(BINDIR)/starforth4-$(1) < /dev/null > $$@ || { cat $$@; rm -f $$@; exit 1; }
|
|
@cat $$@
|
|
endef
|
|
$(foreach i,$(HOSTED_ISAS),$(eval $(call HOSTED_RULE,$(i))))
|
|
|
|
# `make hosted` builds the three. `make hosted-check` boots each with no
|
|
# input and requires that all three print the same lines, ending in
|
|
# PARITY:OK and the prompt: the same hashes on every ISA.
|
|
.PHONY: hosted hosted-check
|
|
hosted: $(foreach i,$(HOSTED_ISAS),$(BINDIR)/starforth4-$(i))
|
|
hosted-check: $(foreach i,$(HOSTED_ISAS),$(BINDIR)/boot-$(i).txt)
|
|
@grep -q '^PARITY:OK$$' $(BINDIR)/boot-amd64.txt || { echo "hosted-check: no PARITY:OK"; exit 1; }
|
|
@cmp $(BINDIR)/boot-amd64.txt $(BINDIR)/boot-aarch64.txt
|
|
@cmp $(BINDIR)/boot-amd64.txt $(BINDIR)/boot-riscv64.txt
|
|
@echo "hosted-check: amd64, aarch64 and riscv64 boot identically"
|
|
|
|
.PHONY: all test sanitize clean $(addprefix test-,$(WIDTHS))
|
|
|
|
all: test
|
|
|
|
# A build that finds no tests must fail loudly, not report a vacuous pass. A
|
|
# loop over an empty list exits 0 having run nothing, which in CI is
|
|
# indistinguishable from a green run -- the worst possible failure mode for a
|
|
# test harness, and one this Makefile has already produced once.
|
|
ifeq ($(strip $(TESTS)),)
|
|
$(error No test sources under $(HERE)/tests -- refusing to report success)
|
|
endif
|
|
|
|
# One test binary per (width, test source) pair. The cell width is a
|
|
# preprocessor parameter rather than a runtime one, so the two widths are
|
|
# separate compilations -- which is the point: there is no single code path
|
|
# that could paper over a width assumption.
|
|
#
|
|
# `make test` builds optimised; `make sanitize` builds the same sources under
|
|
# AddressSanitizer and UndefinedBehaviorSanitizer at both widths and runs them.
|
|
# The optimized run catches logic errors, this one catches the out-of-bounds
|
|
# ring index and the width-dependent shift that a logic-only test cannot see.
|
|
# -fno-sanitize-recover=all makes every UBSan report fatal: without it UBSan
|
|
# prints the report and carries on, and the run still says "passed".
|
|
#
|
|
# Both binaries depend on this Makefile, so a flag change rebuilds them.
|
|
define TEST_RULE
|
|
$(BINDIR)/$(1)-$(notdir $(2)): $(2) $$(SRCS) $$(wildcard $(HERE)/include/v4/*.h) $$(wildcard $(HERE)/tests/*.h) $(HERE)/Makefile
|
|
@mkdir -p $(BINDIR)
|
|
$$(CC) $$(CFLAGS) -I$(HERE)/include -DV4_CELL_BITS=$(1) $(call node_size,$(2)) $(capsule_dir) \
|
|
$(2) $$(SRCS) -o $$@
|
|
|
|
$(BINDIR)/san-$(1)-$(notdir $(2)): $(2) $$(SRCS) $$(wildcard $(HERE)/include/v4/*.h) $$(wildcard $(HERE)/tests/*.h) $(HERE)/Makefile
|
|
@mkdir -p $(BINDIR)
|
|
$$(CC) $$(CSTD) $$(WARN) -O1 -g -fno-omit-frame-pointer \
|
|
-fsanitize=address,undefined -fno-sanitize-recover=all -I$(HERE)/include -DV4_CELL_BITS=$(1) $(call node_size,$(2)) $(capsule_dir) \
|
|
$(2) $$(SRCS) -o $$@
|
|
endef
|
|
|
|
# One run target per (width, test) and one prerequisite line per width, so
|
|
# adding a test file cannot redefine a recipe and the run cannot skip the
|
|
# build. A shell loop over `$^` is avoided deliberately: `$^` is make syntax
|
|
# that does not survive the define/eval expansion, and a silently-empty loop
|
|
# list is exactly the vacuous-pass failure this file already made once.
|
|
define RUN_RULE
|
|
run-$(1)-$(notdir $(2)): $(BINDIR)/$(1)-$(notdir $(2)) $$(CAPSULES)
|
|
@echo " [V4_CELL_BITS=$(1) $$@]"
|
|
@$(BINDIR)/$(1)-$(notdir $(2))
|
|
|
|
test-$(1): run-$(1)-$(notdir $(2))
|
|
endef
|
|
|
|
# The same sources and the same assertions, under ASan+UBSan.
|
|
define SAN_RULE
|
|
san-$(1)-$(notdir $(2)): $(BINDIR)/san-$(1)-$(notdir $(2))
|
|
@echo " [ASan+UBSan V4_CELL_BITS=$(1) $$@]"
|
|
@$(BINDIR)/san-$(1)-$(notdir $(2))
|
|
endef
|
|
|
|
$(foreach w,$(WIDTHS),$(foreach t,$(TESTS),$(eval $(call TEST_RULE,$(w),$(t)))))
|
|
$(foreach w,$(WIDTHS),$(foreach t,$(TESTS),$(eval $(call RUN_RULE,$(w),$(t)))))
|
|
$(foreach w,$(WIDTHS),$(foreach t,$(TESTS),$(eval $(call SAN_RULE,$(w),$(t)))))
|
|
|
|
sanitize: $(foreach w,$(WIDTHS),$(foreach t,$(TESTS),san-$(w)-$(notdir $(t))))
|
|
@echo "all v4 tests passed under ASan+UBSan"
|
|
|
|
.PHONY: $(foreach w,$(WIDTHS),$(foreach t,$(TESTS),run-$(w)-$(notdir $(t)) san-$(w)-$(notdir $(t))))
|
|
|
|
test: $(addprefix test-,$(WIDTHS))
|
|
@echo "all v4 tests passed"
|
|
|
|
clean:
|
|
rm -rf $(BINDIR)
|