|
| 1 | +############################################################################# |
| 2 | +# Copyright (c) The mlkem-native project authors |
| 3 | +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. |
| 4 | +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0 |
| 5 | +############################################################################# |
| 6 | + |
| 7 | +# |
| 8 | +# This Makefile is derived from the Makefile x86/Makefile in s2n-bignum. |
| 9 | +# - Remove all s2n-bignum proofs and tutorial, add mlkem-native proofs |
| 10 | +# - Minor path modifications to support base theories from s2n-bignum |
| 11 | +# to reside in a separate read-only directory |
| 12 | +# |
| 13 | + |
| 14 | +.DEFAULT_GOAL := run_proofs |
| 15 | + |
| 16 | +OSTYPE_RESULT=$(shell uname -s) |
| 17 | +ARCHTYPE_RESULT=$(shell uname -m) |
| 18 | + |
| 19 | +SRC ?= $(S2N_BIGNUM_DIR) |
| 20 | +SRC_X86 ?= $(SRC)/x86 |
| 21 | + |
| 22 | +# Add explicit language input parameter to cpp, otherwise the use of #n for |
| 23 | +# numeric literals in x86 code is a problem when used inside #define macros |
| 24 | +# since normally that means stringization. |
| 25 | +# |
| 26 | +# Some clang-based preprocessors seem to behave differently, and get confused |
| 27 | +# by single-quote characters in comments, so we eliminate // comments first. |
| 28 | + |
| 29 | +ifeq ($(OSTYPE_RESULT),Darwin) |
| 30 | +PREPROCESS=sed -e 's/\/\/.*//' | $(CC) -E -xassembler-with-cpp - |
| 31 | +else |
| 32 | +PREPROCESS=$(CC) -E -xassembler-with-cpp - |
| 33 | +endif |
| 34 | + |
| 35 | +# Generally GNU-type assemblers are happy with multiple instructions on |
| 36 | +# a line, but we split them up anyway just in case. |
| 37 | + |
| 38 | +SPLIT=tr ';' '\n' |
| 39 | + |
| 40 | +# If actually on an x86_64 machine, just use the assembler (as). Otherwise |
| 41 | +# use a cross-assembling version so that the code can still be assembled |
| 42 | +# and the proofs checked against the object files (though you won't be able |
| 43 | +# to run code without additional emulation infrastructure). For the clang |
| 44 | +# version on OS X we just add the "-arch x86_64" option. For the Linux/gcc |
| 45 | +# toolchain we assume the presence of the special cross-assembler. This |
| 46 | +# can be installed via something like: |
| 47 | +# |
| 48 | +# sudo apt-get install binutils-x86-64-linux-gnu |
| 49 | + |
| 50 | +ifeq ($(ARCHTYPE_RESULT),x86_64) |
| 51 | +ASSEMBLE=as |
| 52 | +OBJDUMP=objdump -d |
| 53 | +else |
| 54 | +ifeq ($(OSTYPE_RESULT),Darwin) |
| 55 | +ASSEMBLE=as -arch x86_64 |
| 56 | +OBJDUMP=otool -tvV |
| 57 | +else |
| 58 | +ASSEMBLE=x86_64-linux-gnu-as |
| 59 | +OBJDUMP=x86_64-linux-gnu-objdump -d |
| 60 | +endif |
| 61 | +endif |
| 62 | + |
| 63 | +OBJ = mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o \ |
| 64 | + mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o \ |
| 65 | + mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o |
| 66 | + |
| 67 | +# Build object files from assembly sources |
| 68 | +$(OBJ): %.o : %.S |
| 69 | + @echo "Preparing $@ ..." |
| 70 | + @echo "AS: `$(ASSEMBLE) --version`" |
| 71 | + @echo "OBJDUMP: `$(OBJDUMP) --version`" |
| 72 | + $(Q)[ -d $(@D) ] || mkdir -p $(@D) |
| 73 | + cat $< | $(PREPROCESS) | $(SPLIT) | $(ASSEMBLE) -o $@ - |
| 74 | + # MacOS may generate relocations in non-text sections that break |
| 75 | + # the object file parser in HOL-Light |
| 76 | + strip $@ |
| 77 | + |
| 78 | +clean:; rm -f */*.o */*/*.o */*.correct */*.native |
| 79 | + |
| 80 | +# Proof-related parts |
| 81 | +# |
| 82 | +# The proof files are all independent, though each one loads the |
| 83 | +# same common infrastructure "base.ml". So you can potentially |
| 84 | +# run the proofs in parallel for more speed, e.g. |
| 85 | +# |
| 86 | +# nohup make -j 16 proofs & |
| 87 | +# |
| 88 | +# If you build hol-light yourself (see https://github.com/jrh13/hol-light) |
| 89 | +# in your home directory, and do "make" inside the subdirectory hol-light, |
| 90 | +# then the following HOLDIR setting should be right: |
| 91 | + |
| 92 | +HOLDIR?=$(HOLLIGHTDIR) |
| 93 | +HOLLIGHT:=$(HOLDIR)/hol.sh |
| 94 | + |
| 95 | +BASE?=$(shell dirname $(realpath $(firstword $(MAKEFILE_LIST)))) |
| 96 | + |
| 97 | +PROOF_BINS = $(OBJ:.o=.native) |
| 98 | +PROOF_LOGS = $(OBJ:.o=.correct) |
| 99 | + |
| 100 | +# Build precompiled binary for dumping bytecodes |
| 101 | +proofs/dump_bytecode.native: proofs/dump_bytecode.ml $(OBJ) |
| 102 | + ./proofs/build-proof.sh $(BASE)/$< "$(HOLLIGHT)" "$@" |
| 103 | + |
| 104 | +# Build precompiled native binaries of HOL Light proofs |
| 105 | + |
| 106 | +.SECONDEXPANSION: |
| 107 | +%.native: proofs/$$(*F).ml %.o ; ./proofs/build-proof.sh $(BASE)/$< "$(HOLLIGHT)" "$@" |
| 108 | + |
| 109 | +# Run them and print the standard output+error at *.correct |
| 110 | +%.correct: %.native |
| 111 | + $< 2>&1 | tee $@ |
| 112 | + @if (grep -i "error:\|exception:" "$@" >/dev/null); then \ |
| 113 | + echo "$< had errors!"; \ |
| 114 | + exit 1; \ |
| 115 | + else \ |
| 116 | + echo "$< OK"; \ |
| 117 | + fi |
| 118 | + |
| 119 | +build_proofs: $(PROOF_BINS); |
| 120 | +run_proofs: build_proofs $(PROOF_LOGS); |
| 121 | + |
| 122 | +proofs: run_proofs ; $(SRC)/tools/count-proofs.sh . |
| 123 | + |
| 124 | +dump_bytecode: proofs/dump_bytecode.native |
| 125 | + ./$< |
| 126 | + |
| 127 | +.PHONY: proofs build_proofs run_proofs sematest clean dump_bytecode |
| 128 | + |
| 129 | +# Always run sematest regardless of dependency check |
| 130 | +FORCE: ; |
| 131 | +# Always use max. # of cores because in Makefile one cannot get the passed number of -j. |
| 132 | +# A portable way of getting the number of max. cores: |
| 133 | +# https://stackoverflow.com/a/23569003/1488216 |
| 134 | +NUM_CORES_FOR_SEMATEST = $(shell getconf _NPROCESSORS_ONLN) |
| 135 | +sematest: FORCE $(OBJ) $(SRC_X86)/proofs/simulator_iclasses.ml $(SRC_X86)/proofs/simulator.native |
| 136 | + $(SRC)/tools/run-sematest.sh x86 $(NUM_CORES_FOR_SEMATEST) |
0 commit comments