rajamesandClaude Opus 5.5
5d6043e37e
capsules/v4/post79.4th: 537 of v3's POST cases for the FORTH-79 Required Word Set, each carrying what the hosted v3 binary did with the same line (error or not, the stack, the length and checksum of what it printed). Written by v4/tools/mkpost.py. The harness is FORTH-79 plus the two nucleus hooks. docs/v4.0.0/NUCLEUS.md section 6. - NODE-ERROR has a FORTH name: how a definition in FORTH raises an error - the boot passes POST only on seeing its tally line with fail=0 - POST is not in the boot yet (V4_POST_AT_BOOT=0); make -C v4 post runs it Result: tests=537 pass=439 fail=98. The 98 are not yet sorted into v4 defects and differences needing a ruling; v4/README.md has a first reading. Verified: make -C v4 test passes; hosted-check passes on three ISAs; clean qemu with STARFORTH_V4=1 on amd64, aarch64 and riscv64 reaches ok> with the same hashes as hosted (logs/20261005-1601xx..1604xx). Nothing was typed at a bare-metal prompt. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
229 lines
11 KiB
Makefile
229 lines
11 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 post` builds the amd64 system with POST in its boot
|
|
# (V4_POST_AT_BOOT=1, system/boot.c) and boots it: the POST capsule,
|
|
# ../capsules/v4/post79.4th, is loaded after forth79.4th and must end with a
|
|
# clean tally. `make post79` writes that capsule again from v3's cases
|
|
# (tools/mkpost.py); it needs the hosted v3 binary.
|
|
.PHONY: post post79
|
|
$(BINDIR)/starforth4-post: $(HERE)/tools/hosted.c $(BINDIR)/v4_image_64.c $(CAPSULE_DIR_C) $(ENGINE_SRCS) $(SYSTEM_SRCS) $(wildcard $(HERE)/include/v4/*.h) $(HERE)/Makefile
|
|
$(CC_amd64) $(CFLAGS) -D_POSIX_C_SOURCE=200809L -I$(HERE)/include -DV4_CELL_BITS=64 $(HOST_DEFS) -c $(HERE)/tools/hosted.c -o $(BINDIR)/hosted-post.o
|
|
$(CC_amd64) $(SYSTEM_CFLAGS) -DV4_POST_AT_BOOT=1 -static $(BINDIR)/hosted-post.o $(BINDIR)/v4_image_64.c $(CAPSULE_DIR_C) $(ENGINE_SRCS) $(SYSTEM_SRCS) -o $@
|
|
post: $(BINDIR)/starforth4-post
|
|
@$(BINDIR)/starforth4-post < /dev/null
|
|
post79:
|
|
python3 $(HERE)/tools/mkpost.py
|
|
|
|
# `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)
|