rajamesandClaude Opus 5.5
2bf958ce3a
v4/system/post.c: for each case it empties the node's data stack, sends DECIMAL FORTH DEFINITIONS, sends the case's lines keeping what the node prints, reads the stack, and judges: an error exactly if one is expected, and otherwise the stack and every character printed. A failing case is named with what it printed and left. Nothing of it is on the node. Its tests are in test_host_quit.c, on that test's node: 29 checks of cases that must pass and cases that must fail -- a wrong value, depth, order or output, an error wanted or unwanted, a case of two lines, depth-only cases, the starting state, more printing than is kept, and a line that never comes back. Both widths and the sanitizers. The boot still runs the capsule; that is the next commit. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
271 lines
14 KiB
Makefile
271 lines
14 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))
|
|
|
|
# BLOCKS (docs/v4.0.0/MESH.md section 8). A node asks its kernel for a
|
|
# block, and system/blocks.c serves it from the kernel's block subsystem,
|
|
# which is v3's and is built as v3 builds it. Tests named
|
|
# test_host_*.c link them. V3_BLOCK_SRCS is all of v3 that the block
|
|
# subsystem needs: its two device back ends, the log and the clock.
|
|
ROOT_DIR := $(abspath $(HERE)/..)
|
|
V3_BLOCK_SRCS := $(addprefix $(ROOT_DIR)/v3/src/,block_subsystem.c blkio_ram.c blkio_file.c log.c platform/platform_init.c platform/linux/time.c)
|
|
V3_CFLAGS := -std=gnu99 -Wall $(OPT) -I$(ROOT_DIR)/v3/include -I$(ROOT_DIR)/kernel/include
|
|
BLOCKS_SRC := $(HERE)/system/blocks.c
|
|
V3_INC := -isystem $(ROOT_DIR)/v3/include -isystem $(ROOT_DIR)/kernel/include
|
|
uses_blocks = $(findstring /test_host_,$(1))
|
|
blocks_inc = $(if $(call uses_blocks,$(1)),$(V3_INC))
|
|
|
|
$(BINDIR)/v3blocks.o: $(V3_BLOCK_SRCS) $(wildcard $(ROOT_DIR)/v3/include/*.h) $(HERE)/Makefile
|
|
@rm -rf $(BINDIR)/v3o && mkdir -p $(BINDIR)/v3o
|
|
cd $(BINDIR)/v3o && $(CC) $(V3_CFLAGS) -c $(V3_BLOCK_SRCS)
|
|
$(LD) -r $(BINDIR)/v3o/*.o -o $@
|
|
$(BINDIR)/san-v3blocks.o: $(V3_BLOCK_SRCS) $(wildcard $(ROOT_DIR)/v3/include/*.h) $(HERE)/Makefile
|
|
@rm -rf $(BINDIR)/san-v3o && mkdir -p $(BINDIR)/san-v3o
|
|
cd $(BINDIR)/san-v3o && $(CC) $(V3_CFLAGS) -O1 -g -fno-omit-frame-pointer -fsanitize=address,undefined -fno-sanitize-recover=all -c $(V3_BLOCK_SRCS)
|
|
$(LD) -r $(BINDIR)/san-v3o/*.o -o $@
|
|
# blocks.c is compiled with each test that uses it, under that test's own
|
|
# flags: its warnings, its sanitizers, its cell width and node size.
|
|
# So are POST's runner and its cases (system/post.c, system/post_cases.c;
|
|
# docs/v4.0.0/NUCLEUS.md 6.3), which are the kernel's too.
|
|
blocks_src = $(if $(call uses_blocks,$(1)),$(BLOCKS_SRC) $(HERE)/system/post.c $(HERE)/system/post_cases.c)
|
|
blocks_objs = $(if $(call uses_blocks,$(1)),$(BINDIR)/v3blocks.o)
|
|
san_blocks_objs = $(if $(call uses_blocks,$(1)),$(BINDIR)/san-v3blocks.o)
|
|
|
|
# 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.
|
|
# The nucleus as a capsule of F18 code (include/v4/capsule.h). The 64-bit one
|
|
# is a product's: it goes into the capsule directory, ../capsules/v4, where
|
|
# the repository's mkcapsule finds it, hashes it and signs it with every
|
|
# other capsule. It is a built file kept in the tree, as
|
|
# ../capsules/BLOCK_MAP.md is, and is to be committed when it changes.
|
|
ROOT := $(abspath $(HERE)/..)
|
|
NUCLEUS_64 := $(ROOT)/capsules/v4/nucleus-64.f18
|
|
NUCLEUS_32 := $(BINDIR)/nucleus-32.f18
|
|
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 fabric.c capsule.c message.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) $$@ $$(NUCLEUS_$(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.
|
|
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)/v4_image_64.c
|
|
$(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) $(BLOCKS_SRC) $(V3_BLOCK_SRCS) $$(wildcard $(HERE)/include/v4/*.h) $(HERE)/Makefile
|
|
$$(CC_$(1)) $$(CFLAGS) -D_POSIX_C_SOURCE=200809L -I$(HERE)/include $(V3_INC) -DV4_CELL_BITS=64 $(HOST_DEFS) -c $(HERE)/tools/hosted.c -o $(BINDIR)/hosted-$(1).o
|
|
@rm -rf $(BINDIR)/v3o-$(1) && mkdir -p $(BINDIR)/v3o-$(1)
|
|
cd $(BINDIR)/v3o-$(1) && $$(CC_$(1)) $(V3_CFLAGS) -I$(HERE)/include -DV4_CELL_BITS=64 $(HOST_DEFS) -c $(V3_BLOCK_SRCS) $(BLOCKS_SRC)
|
|
$$(CC_$(1)) $$(SYSTEM_CFLAGS) -static $(BINDIR)/hosted-$(1).o $(BINDIR)/v4_image_64.c $(CAPSULE_DIR_C) $$(ENGINE_SRCS) $$(SYSTEM_SRCS) $(BINDIR)/v3o-$(1)/*.o -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` boots the amd64 system alone, which is the quick check after a
|
|
# change to the vocabulary: nucleus, forth79.4th, POST, prompt. `make
|
|
# post79` writes the POST capsule, ../capsules/v4/post79.4th, again from
|
|
# v3's cases and tools/post79_rules.py (tools/mkpost.py); it needs the
|
|
# hosted v3 binary.
|
|
.PHONY: post post79
|
|
post: $(BINDIR)/starforth4-amd64
|
|
@$(BINDIR)/starforth4-amd64 < /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, POST: PASSED and the prompt: the same hashes on every ISA. It
|
|
# also checks that what the boot loaded is part of the system: after COLD
|
|
# the capsule's words and the kernel's are still there, and FORGET refuses
|
|
# them.
|
|
.PHONY: hosted hosted-check
|
|
hosted: $(foreach i,$(HOSTED_ISAS),$(BINDIR)/starforth4-$(i))
|
|
hosted-check: $(foreach i,$(HOSTED_ISAS),$(BINDIR)/boot-$(i).txt)
|
|
@grep -q '^POST: PASSED$$' $(BINDIR)/boot-amd64.txt || { echo "hosted-check: no POST: PASSED"; exit 1; }
|
|
@cmp $(BINDIR)/boot-amd64.txt $(BINDIR)/boot-aarch64.txt
|
|
@cmp $(BINDIR)/boot-amd64.txt $(BINDIR)/boot-riscv64.txt
|
|
@printf 'COLD\n3 4 U* . .\nFORGET U*\nBYE\n' | $(BINDIR)/starforth4-amd64 > $(BINDIR)/cold-amd64.txt
|
|
@grep -q '^ok> 0 12 ok$$' $(BINDIR)/cold-amd64.txt || { echo "hosted-check: COLD lost the capsule's words"; cat $(BINDIR)/cold-amd64.txt; exit 1; }
|
|
@grep -q '^ok> Protected word$$' $(BINDIR)/cold-amd64.txt || { echo "hosted-check: a capsule word could be forgotten"; exit 1; }
|
|
@grep -q '^ok> Goodbye!$$' $(BINDIR)/cold-amd64.txt || { echo "hosted-check: COLD lost BYE"; exit 1; }
|
|
@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) $(call blocks_src,$(2)) $(call blocks_objs,$(2)) $$(wildcard $(HERE)/include/v4/*.h) $$(wildcard $(HERE)/tests/*.h) $(HERE)/Makefile
|
|
@mkdir -p $(BINDIR)
|
|
$$(CC) $$(CFLAGS) -I$(HERE)/include $(call blocks_inc,$(2)) -DV4_CELL_BITS=$(1) $(call node_size,$(2)) $(capsule_dir) \
|
|
$(2) $$(SRCS) $(call blocks_src,$(2)) $(call blocks_objs,$(2)) -o $$@
|
|
|
|
$(BINDIR)/san-$(1)-$(notdir $(2)): $(2) $$(SRCS) $(call blocks_src,$(2)) $(call san_blocks_objs,$(2)) $$(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 $(call blocks_inc,$(2)) -DV4_CELL_BITS=$(1) $(call node_size,$(2)) $(capsule_dir) \
|
|
$(2) $$(SRCS) $(call blocks_src,$(2)) $(call san_blocks_objs,$(2)) -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)
|