# 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.
# 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) $$(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` 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) $$(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)