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