From a0cfcf0e86124f1baac9f65bcf107632ab0b4bdc Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Thu, 8 Aug 2024 20:27:06 +0100 Subject: [PATCH] wip: src/ Makefiles cleanup + workflow to check src/ with Dockerfile in scripts/Docker --- ...proof.yml => amd64-linux-main-proof.yml.0} | 0 ...-linux-main.yml => amd64-linux-main.yml.0} | 0 .github/workflows/amd64-linux.yml | 81 +++++ build-common/Makefile | 277 ++++++++++++----- build-common/Makefile.checksafety | 46 +-- build-common/Makefile.checksct | 35 ++- build-common/Makefile.common | 286 +++++++++++++----- proof/.gitignore | 1 + scripts/extract-all.sh | 2 + scripts/reporter/jlog | 72 +++++ 10 files changed, 598 insertions(+), 202 deletions(-) rename .github/workflows/{amd64-linux-main-proof.yml => amd64-linux-main-proof.yml.0} (100%) rename .github/workflows/{amd64-linux-main.yml => amd64-linux-main.yml.0} (100%) create mode 100644 .github/workflows/amd64-linux.yml create mode 100755 scripts/reporter/jlog diff --git a/.github/workflows/amd64-linux-main-proof.yml b/.github/workflows/amd64-linux-main-proof.yml.0 similarity index 100% rename from .github/workflows/amd64-linux-main-proof.yml rename to .github/workflows/amd64-linux-main-proof.yml.0 diff --git a/.github/workflows/amd64-linux-main.yml b/.github/workflows/amd64-linux-main.yml.0 similarity index 100% rename from .github/workflows/amd64-linux-main.yml rename to .github/workflows/amd64-linux-main.yml.0 diff --git a/.github/workflows/amd64-linux.yml b/.github/workflows/amd64-linux.yml new file mode 100644 index 00000000..657cfadd --- /dev/null +++ b/.github/workflows/amd64-linux.yml @@ -0,0 +1,81 @@ +name: amd64-linux + +on: + workflow_dispatch: + push: + branches: + - main + pull_request: + +jobs: + + # extract src + extract-src: + runs-on: [self-hosted, linux, X64, amd64-main] + steps: + - name: checkout + uses: actions/checkout@v4 + with: + submodules: 'true' + + - name: extract src from submodules + run: ./scripts/extract-all.sh + + # src + check-safety: + needs: extract-src + runs-on: [self-hosted, linux, X64, amd64-main] + steps: + - name: checkout + uses: actions/checkout@v4 + + - name: check safety + run: make -j$JOBS -C src/ CI=1 check-safety + - name: print report + run: make -C src/ CI=1 reporter + - name: return error + run: make -C src/ CI=1 err + + check-sct: + needs: extract-src + runs-on: [self-hosted, linux, X64, amd64-main] + steps: + - name: checkout + uses: actions/checkout@v4 + + - name: check speculative constant-time (v1) + run: make -j$JOBS -C src/ CI=1 check-sct + - name: print report + run: make -C src/ CI=1 reporter + - name: return error + run: make -C src/ CI=1 err + + extract-to-easycrypt: + needs: extract-src + runs-on: [self-hosted, linux, X64, amd64-main] + steps: + - name: checkout + uses: actions/checkout@v4 + + - name: check extraction from Jasmin to EasyCrypt + run: make -j$JOBS -C src/ CI=1 extract-to-easycrypt + - name: print report + run: make -C src/ CI=1 reporter + - name: return error + run: make -C src/ CI=1 err + + compile-src: + needs: extract-src + runs-on: [self-hosted, linux, X64, amd64-main] + steps: + - name: checkout + uses: actions/checkout@v4 + + - name: check compilation of libformosa25519.a + run: make -j$JOBS -C src/ CI=1 libformosa25519.a + - name: print report + run: make -C src/ CI=1 reporter + - name: return error + run: make -C src/ CI=1 err + + diff --git a/build-common/Makefile b/build-common/Makefile index 27d7314d..fca928f1 100644 --- a/build-common/Makefile +++ b/build-common/Makefile @@ -1,127 +1,242 @@ -# -*- Makefile -*- +# ----------------------------------------------------------------------------- + +JASMIN ?= jasminc + +# ----------------------------------------------------------------------------- -# -------------------------------------------------------------------- -AS ?= as CC ?= clang CFLAGS ?= -O3 -Wall -Wextra -Wpedantic -Wvla -Werror -std=c99 \ -Wundef -Wshadow -Wcast-align -Wpointer-arith -Wmissing-prototypes \ -fstrict-aliasing -fno-common -pipe +AR ?= ar +RANLIB ?= ranlib + + +# ----------------------------------------------------------------------------- + +SRC := . +PROOF := $(abspath ../proof) +SCRIPTS := $(abspath ../scripts) +FILTER ?= $(SRC)/crypto_% +EXCLUDE ?= -JASMIN ?= jasminc -JASMIN_CT ?= jasmin-ct +IMPLEMENTATIONS_FILES ?= $(filter $(FILTER), $(filter-out $(EXCLUDE), $(sort $(shell find $(SRC)/ -name '*.jazz')))) +IMPLEMENTATIONS_DIRECTORIES := $(dir $(IMPLEMENTATIONS_FILES)) + +ASSEMBLY_FILES ?= $(IMPLEMENTATIONS_FILES:%.jazz=%.s) +OBJECT_FILES := $(ASSEMBLY_FILES:%.s=%.o) +C_HEADER_FILES ?= $(addsuffix include/api.h, $(dir $(ASSEMBLY_FILES))) + + +# ----------------------------------------------------------------------------- +# when CI=1, information about compilation/checking properties of the files +# will be stored under .ci/ folders in the implementations directories. Then +# the user of this Makefile can run 'make CI=1 report' to get a simple report +# of the current status: compilation, safety checking, and sct checking. +CI ?= 0 +CI_REMOVE_OK_LOGS ?= "1" -# -------------------------------------------------------------------- -CI ?= 0 export CI -CICL ?= "1" -# -------------------------------------------------------------------- -LOGS := libjade-logs-src.tar.gz -EXCLUDE ?= -SRC := . +# ----------------------------------------------------------------------------- +# setting the default rule as 'all': compiles, and checks safety and sct for +# all implementations -FILTER ?= $(SRC)/crypto_% -JAZZ ?= $(filter $(FILTER), $(filter-out $(addprefix ./,$(EXCLUDE)), $(sort $(dir $(shell find $(SRC) -name '*.jazz'))))) -SAFETY ?= $(addsuffix safety, $(JAZZ)) -SCT ?= $(addsuffix check_sct, $(JAZZ)) - -SOURCES ?= $(filter-out ./, $(sort $(dir $(shell find $(SRC) -name 'Makefile')))) -ASM := $(shell find $(SRC) -name '*.s') -API := $(addsuffix include/api.h, $(dir $(ASM))) -OBJ := $(ASM:%.s=%.o) - -FAIL_ON_ERROR ?= 0 - -# -------------------------------------------------------------------- -ifeq ($(CI),1) -.PHONY: backward_compatibility -backward_compatibility: - $(MAKE) default - $(MAKE) reporter - mv $(LOGS) check.tar.gz - $(MAKE) err -endif +default: all + + +# ----------------------------------------------------------------------------- +# compile Jasmin implementations to assembly and create libjade.a -# -------------------------------------------------------------------- -.PHONY: libjade.a libjade.h $(JAZZ) clean distclean $(LOGS) -.INTERMEDIATE: $(OBJ) +.PHONY: libjade.a libjade.h $(ASSEMBLY_FILES) -default: libjade.a libjade.h +.INTERMEDIATE: $(OBJECT_FILES) -all: $(JAZZ) +just_compile: $(ASSEMBLY_FILES) -libjade.a: $(JAZZ) +libjade.a: $(ASSEMBLY_FILES) $(MAKE) __libjade -__libjade: $(OBJ) - ar -rc libjade.a $(OBJ) - ranlib libjade.a - echo "" | cat - $(API) > libjade.h +__libjade: $(OBJECT_FILES) + $(AR) -rc libjade.a $(OBJECT_FILES) + $(RANLIB) libjade.a + echo "" | cat - $(C_HEADER_FILES) > libjade.h -$(JAZZ): - $(MAKE) -C $@ || !(($(FAIL_ON_ERROR))) +$(ASSEMBLY_FILES): + $(MAKE) -C $(@D) $(@F) -# -------------------------------------------------------------------- -SAFETY_TIMEOUT ?= 1440m -export SAFETY_TIMEOUT +# ----------------------------------------------------------------------------- +# safety checking -.PHONY: safety -safety: $(SAFETY) +CHECK_SAFETY ?= $(addsuffix check-safety, $(IMPLEMENTATIONS_DIRECTORIES)) -$(SAFETY): - $(MAKE) -C $(@D) $(@F) || true +CHECK_SAFETY_TIMEOUT ?= 10m +export CHECK_SAFETY_TIMEOUT -# -------------------------------------------------------------------- -.PHONY: check_sct -check_sct: $(SCT) +.PHONY: check-safety $(CHECK_SAFETY) -$(SCT): - $(MAKE) -C $(@D) $(@F) || true +check-safety: $(CHECK_SAFETY) -# -------------------------------------------------------------------- -ifeq ($(CI),1) +$(CHECK_SAFETY): + $(MAKE) -C $(@D) $(@F) -reporter: - $(MAKE) reporter_s - $(MAKE) $(LOGS) -reporter_s: - ./../scripts/ci/reporter/jlog "Compilation status" src/ *.s $(CICL) - $(MAKE) $(LOGS) +# ----------------------------------------------------------------------------- +# speculative "constant-time" checking / "secret-independence" checking + +CHECK_SCT ?= $(addsuffix check-sct, $(IMPLEMENTATIONS_DIRECTORIES)) + +.PHONY: check-sct $(CHECK_SCT) + +check-sct: $(CHECK_SCT) + +$(CHECK_SCT): + $(MAKE) -C $(@D) $(@F) + + +# ----------------------------------------------------------------------------- +# extraction to easycrypt (updates proof/ directory) + +EXTRACT_TO_EASYCRYPT ?= $(addsuffix extract-to-easycrypt, $(IMPLEMENTATIONS_DIRECTORIES)) + +.PHONY: extract-to-easycrypt $(EXTRACT_TO_EASYCRYPT) + +extract-to-easycrypt: $(EXTRACT_TO_EASYCRYPT) + +$(EXTRACT_TO_EASYCRYPT): + $(MAKE) -C $(@D) $(@F) -reporter_safety: - ./../scripts/ci/reporter/jlog "Safety status" src/ *.safety $(CICL) - $(MAKE) $(LOGS) -reporter_sct: - ./../scripts/ci/reporter/jlog "Speculative constant-time status" src/ *.sct $(CICL) +# ----------------------------------------------------------------------------- +# preprocess-inplace and revert-preprocess-inplace -ERR := $(shell find $(BIN) -name '*.error') -CIR := $(shell find $(BIN) -name '*.log') $(ERR) +PREPROCESS_INPLACE ?= $(addsuffix preprocess-inplace, $(IMPLEMENTATIONS_DIRECTORIES)) + +.PHONY: preprocess-inplace $(PREPROCESS_INPLACE) + +preprocess-inplace: $(PREPROCESS_INPLACE) + +$(PREPROCESS_INPLACE): + $(MAKE) -C $(@D) $(@F) + + +REVERT_PREPROCESS_INPLACE ?= $(addsuffix revert-preprocess-inplace, $(IMPLEMENTATIONS_DIRECTORIES)) + +.PHONY: preprocess-inplace $(REVERT_PREPROCESS_INPLACE) + +revert-preprocess-inplace: $(REVERT_PREPROCESS_INPLACE) + +$(REVERT_PREPROCESS_INPLACE): + $(MAKE) -C $(@D) $(@F) + + +# ----------------------------------------------------------------------------- +# reporter: this section defines rules for reporting the current implementation +# status + +LOGS ?= libjade-logs-src.tar.gz +JLOG := $(SCRIPTS)/reporter/jlog + +CI_ERROR_FILES := $(shell find $(SRC) -name '*.error') +CI_ALL_FILES := $(shell find $(SRC) -name '*.log') $(CI_ERROR_FILES) + +.PHONY: reporter logs $(LOGS) err + +reporter: + $(JLOG) "Safety checking status" src/ *.safety $(CI_REMOVE_OK_LOGS) + $(JLOG) "Speculative constant-time status" src/ *.sct $(CI_REMOVE_OK_LOGS) + $(JLOG) "Extraction to EasyCrypt status" src/ *.ec $(CI_REMOVE_OK_LOGS) + $(JLOG) "Compilation status (*.jazz -> *.s)" src/ *.s $(CI_REMOVE_OK_LOGS) + +logs: $(LOGS) $(LOGS): @$(JASMIN) -version > notes -ifeq ($(words $(CIR)),0) - @echo "good job." >> notes +ifeq ($(words $(CI_ALL_FILES)),0) + @echo "There are no logs with warnings or errors. Good job." >> notes @tar -zcvf $@ notes else - @tar -zcvf $@ notes $(CIR) + @tar -zcvf $@ notes $(CI_ALL_FILES) endif @rm notes err: -ifneq ($(words $(ERR)),0) - $(error $(ERR)) +ifneq ($(words $(CI_ERROR_FILES)),0) + $(error $(CI_ERROR_FILES)) endif -endif -# -------------------------------------------------------------------- +# ----------------------------------------------------------------------------- +# to run 'everything': $ make -j$(nproc) all +.PHONY: all + +all: CI=1 +all: + $(MAKE) distclean + $(MAKE) check-safety + $(MAKE) check-sct + $(MAKE) extract-to-easycrypt + $(MAKE) libjade.a + $(MAKE) libjade.h + $(MAKE) reporter + $(MAKE) err + +all-with-preprocess-inplace: CI=1 +all-with-preprocess-inplace: + $(MAKE) distclean + $(MAKE) preprocess-inplace + $(MAKE) check-safety + $(MAKE) check-sct + $(MAKE) extract-to-easycrypt + $(MAKE) libjade.a + $(MAKE) libjade.h + $(MAKE) reporter + $(MAKE) err + + +# ----------------------------------------------------------------------------- +# clean rules + +.PHONY: clean distclean + clean: - rm -f libjade.a libjade.h $(LOGS) check.tar.gz + rm -f libjade.a libjade.h + rm -f $(LOGS) + for i in $(IMPLEMENTATIONS_DIRECTORIES); do $(MAKE) -C $$i clean; done + rm -f $(PROOF)/arrays/*Array*.ec distclean: clean - for i in $(SOURCES); do $(MAKE) -C $$i clean; done + + +# ----------------------------------------------------------------------------- +# printing section +.PHONY: print-available-implementations + +print-available-implementations: + @for i in $(IMPLEMENTATIONS_DIRECTORIES:./%=%); do echo $$i; done + + +# ----------------------------------------------------------------------------- +# debug/print rules: helps to check the effects of FILTER or EXCLUDE + +debug-print-variables: + @echo "" + @echo " SRC: $(SRC)\n" + @echo " PROOF: $(PROOF)\n" + @echo " FILTER: $(FILTER)\n" + @echo " EXCLUDE: $(EXCLUDE)\n" + @echo " IMPLEMENTATIONS_DIRECTORIES: $(IMPLEMENTATIONS_DIRECTORIES)\n" + @echo " IMPLEMENTATIONS_FILES: $(IMPLEMENTATIONS_FILES)\n" + + @echo " ASSEMBLY_FILES: $(ASSEMBLY_FILES)\n" + @echo " OBJECT_FILES: $(OBJECT_FILES)\n" + @echo " C_HEADER_FILES: $(C_HEADER_FILES)\n" + + @echo " CHECK_SAFETY: $(CHECK_SAFETY)\n" + @echo " CHECK_SCT: $(CHECK_SCT)\n" + @echo " EXTRACT_TO_EASYCRYPT: $(EXTRACT_TO_EASYCRYPT)\n" + + @echo " LOGS: $(LOGS)\n" diff --git a/build-common/Makefile.checksafety b/build-common/Makefile.checksafety index 27814f33..9f9ac143 100644 --- a/build-common/Makefile.checksafety +++ b/build-common/Makefile.checksafety @@ -1,38 +1,44 @@ -# Notes: -# - this file defines fine-grained targets that allow checking the safety of individual exported -# functions -# - it is meant to be included by Makefile.common, right before the 'generic' safety targets +# ----------------------------------------------------------------------------- ifneq ($(OP),) SAFETY_FLAGS ?= -SAFETY_TIMEOUT ?= 4320m -SAFETY_DIR := .safety -CHECK_SAFETY_S = (time timeout -v $(SAFETY_TIMEOUT) $(JASMINC) -slice $* -checksafety $(SAFETY_FLAGS) $(shell cat $(SAFETY_DIR)/$*.safetyparam) $< 2> $@) $(CIT) -CHECK_SAFETY = (time timeout -v $(SAFETY_TIMEOUT) $(JASMINC) -checksafety $(SAFETY_FLAGS) $(shell cat $(SAFETY_DIR)/$(OP).safetyparam) $< 2> $@) $(CIT) +SAFETY_TIMEOUT ?= 10m -SAFETY_TARGETS = $(addsuffix .safety, $(FUNCTIONS)) +CHECK_SAFETY_SLICE = (time timeout -v $(SAFETY_TIMEOUT) $(JASMIN) $(JINCLUDE) -slice $* -checksafety $(SAFETY_FLAGS) $< 2> $@) $(CI_CMD) +CHECK_SAFETY_SLICE_STDOUT = (time timeout -v $(SAFETY_TIMEOUT) $(JASMIN) $(JINCLUDE) -slice $* -checksafety $(SAFETY_FLAGS) $< ) $(CI_CMD) -checksafety-all: $(SAFETY_TARGETS) +CHECK_SAFETY = (time timeout -v $(SAFETY_TIMEOUT) $(JASMIN) $(JINCLUDE) -checksafety $(SAFETY_FLAGS) $< 2> $@) $(CI_CMD) +CHECK_SAFETY_STDOUT = (time timeout -v $(SAFETY_TIMEOUT) $(JASMIN) $(JINCLUDE) -checksafety $(SAFETY_FLAGS) $< ) $(CI_CMD) -$(OP).safety : $(OP).jazz $(SAFETY_DIR)/$(OP).safetyparam $(DEPS_DIR)/$(OP).safety.d | $(SAFETY_DIR) $(DEPS_DIR) $(CI_DIR) +SAFETY_TARGETS = $(addsuffix .safety, $(FUNCTIONS)) +SAFETY_TARGETS_STDOUT = $(addsuffix .stdout, $(SAFETY_TARGETS)) + +# ----------------------------------------------------------------------------- + +check-safety: $(SAFETY_TARGETS) + +$(OP).safety: $(OP).jazz $(DEPS_DIR)/$(OP).safety.d | $(DEPS_DIR) $(CI_DIR) $(DEPS) $(CHECK_SAFETY) +$(OP).safety.stdout: $(OP).jazz $(DEPS_DIR)/$(OP).safety.d | $(CI_DIR) + $(DEPS) + $(CHECK_SAFETY_STDOUT) + +# -- + $(SAFETY_TARGETS): -%.safety : $(OP).jazz $(SAFETY_DIR)/$(OP).safetyparam $(DEPS_DIR)/%.safety.d | $(SAFETY_DIR) $(DEPS_DIR) $(CI_DIR) +%.safety: $(OP).jazz $(DEPS_DIR)/%.safety.d | $(DEPS_DIR) $(CI_DIR) $(DEPS) - $(CHECK_SAFETY_S) + $(CHECK_SAFETY_SLICE) + +%.safety.stdout: $(OP).jazz | $(DEPS_DIR) $(CI_DIR) + $(DEPS) + $(CHECK_SAFETY_SLICE_STDOUT) DEPFILES := \ $(DEPFILES) \ $(addprefix $(DEPS_DIR)/, $(addsuffix .safety.d, $(FUNCTIONS) $(OP))) -$(SAFETY_DIR)/$(OP).safetyparam: $(SAFETY_DIR) - $(MAKE) -C $(TEST) bin/$(RDIR)/safetyparams - (cd $(SAFETY_DIR) && $(TDIR)/safetyparams) - -$(SAFETY_DIR): ; @mkdir -p $@ - endif - diff --git a/build-common/Makefile.checksct b/build-common/Makefile.checksct index 2168ccfb..ecb7a377 100644 --- a/build-common/Makefile.checksct +++ b/build-common/Makefile.checksct @@ -1,47 +1,46 @@ -# Notes: -# - this file defines fine-grained targets that allow checking the speculative constant-time of individual exported -# functions -# - it is meant to be included by Makefile.common +# ----------------------------------------------------------------------------- -# JASMIN_CT belongs here (and not Makefile.common): some options differ from jasminc JASMIN_CT ?= jasmin-ct +# ----------------------------------------------------------------------------- + ifneq ($(OP),) -# TODO: remove --infer and annotate exported functions -SCT_FLAGS ?= --infer +SCT_FLAGS ?= --infer -CHECK_SCT_SLICE = (JASMINPATH="Jade=$(SRC)" $(JASMIN_CT) --slice $* --sct $(SCT_FLAGS) $< > $@ 2>&1) $(CIT) -CHECK_SCT_SLICE_STDOUT = (JASMINPATH="Jade=$(SRC)" $(JASMIN_CT) --slice $* --sct $(SCT_FLAGS) $< ) $(CIT) +CHECK_SCT_SLICE = (JASMINPATH="formosa25519=$(SRC)" $(JASMIN_CT) --slice $* --sct $(SCT_FLAGS) $< > $@ 2>&1) $(CI_CMD) +CHECK_SCT_SLICE_STDOUT = (JASMINPATH="formosa25519=$(SRC)" $(JASMIN_CT) --slice $* --sct $(SCT_FLAGS) $< ) $(CI_CMD) -CHECK_SCT = (JASMINPATH="Jade=$(SRC)" $(JASMIN_CT) --sct $(SCT_FLAGS) $< > $@ 2>&1) $(CIT) -CHECK_SCT_STDOUT = (JASMINPATH="Jade=$(SRC)" $(JASMIN_CT) --sct $(SCT_FLAGS) $< ) $(CIT) +CHECK_SCT = (JASMINPATH="formosa25519=$(SRC)" $(JASMIN_CT) --sct $(SCT_FLAGS) $< > $@ 2>&1) $(CI_CMD) +CHECK_SCT_STDOUT = (JASMINPATH="formosa25519=$(SRC)" $(JASMIN_CT) --sct $(SCT_FLAGS) $< ) $(CI_CMD) SCT_TARGETS = $(addsuffix .sct, $(FUNCTIONS)) SCT_TARGETS_STDOUT = $(addsuffix .stdout, $(SCT_TARGETS)) -check_sct: $(SCT_TARGETS) -$(OP).sct : $(OP).jazz $(DEPS_DIR)/$(OP).sct.d | $(DEPS_DIR) $(CI_DIR) +# ----------------------------------------------------------------------------- +check-sct: $(SCT_TARGETS) + +$(OP).sct: $(OP).jazz $(DEPS_DIR)/$(OP).sct.d | $(DEPS_DIR) $(CI_DIR) $(DEPS) $(CHECK_SCT) -$(OP).sct.stdout : $(OP).jazz | $(CI_DIR) +$(OP).sct.stdout: $(OP).jazz | $(CI_DIR) $(CHECK_SCT_STDOUT) +# -- + $(SCT_TARGETS): -%.sct : $(OP).jazz $(DEPS_DIR)/%.sct.d | $(DEPS_DIR) $(CI_DIR) +%.sct: $(OP).jazz $(DEPS_DIR)/%.sct.d | $(DEPS_DIR) $(CI_DIR) $(DEPS) $(CHECK_SCT_SLICE) $(SCT_TARGETS_STDOUT): -%.sct.stdout : $(OP).jazz | $(CI_DIR) +%.sct.stdout: $(OP).jazz | $(CI_DIR) $(CHECK_SCT_SLICE_STDOUT) DEPFILES := \ $(DEPFILES) \ $(addprefix $(DEPS_DIR)/, $(addsuffix .sct.d, $(FUNCTIONS) $(OP))) -$(SCT_DIR): ; @mkdir -p $@ - endif diff --git a/build-common/Makefile.common b/build-common/Makefile.common index c27a291c..0d621b8e 100644 --- a/build-common/Makefile.common +++ b/build-common/Makefile.common @@ -1,107 +1,183 @@ +# ----------------------------------------------------------------------------- +# paths vars -# -------------------------------------------------------------------- -TOP = $(abspath $(dir $(filter %Makefile.common,$(MAKEFILE_LIST)))../) -SRC = $(TOP)/src/ -BC = $(TOP)/build-common/ -TEST = $(TOP)/test/ -PROOF = $(TOP)/proof/ - -CDIR = $(abspath $(dir $(abspath $(firstword $(MAKEFILE_LIST))))) -RDIR = $(subst $(SRC),,$(CDIR)) -TDIR = $(TEST)bin/$(RDIR) -PDIR = $(PROOF)$(RDIR) - -# OPERATION: crypto_kem, crypto_hash, ..., common; OP is a shorthand for OPERATION -OPERATION = $(word 1, $(subst /, ,$(RDIR))) -OP = $(word 2, $(subst _, , $(OPERATION)_)) -NAMESPACE = $(subst crypto_,jade_, $(subst -,_,$(subst /,_,$(RDIR)))) +PROJECT_DIR = $(abspath $(dir $(filter %Makefile.common,$(MAKEFILE_LIST)))../) +PROJECT_PARENT_DIR = $(abspath $(PROJECT_DIR)/../) -# -------------------------------------------------------------------- +BUILD_COMMON = $(PROJECT_DIR)/build-common +SRC = $(PROJECT_DIR)/src +TEST = $(PROJECT_DIR)/test +PROOF = $(PROJECT_DIR)/proof -include $(BC)/Makefile.functions +ABS_IMPLEMENTATION_DIR = $(abspath $(dir $(abspath $(firstword $(MAKEFILE_LIST))))) +REL_IMPLEMENTATION_DIR = $(subst $(SRC)/,,$(ABS_IMPLEMENTATION_DIR)) + + +# ----------------------------------------------------------------------------- +# implementation vars + +OP = $(word 2, $(subst _, , $(word 1, $(subst /, ,$(REL_IMPLEMENTATION_DIR))))) +NAMESPACE = $(subst crypto_,jade_, $(subst -,_,$(subst /,_,$(REL_IMPLEMENTATION_DIR)))) + +ifeq ($(OP),kem) +ifeq ($(SRCS),kem.jazz) +FUNCTIONS = $(addprefix $(NAMESPACE)_, keypair_derand keypair enc_derand enc dec) +endif +endif + +ifeq ($(OP),hash) +ifeq ($(SRCS),hash.jazz) +FUNCTIONS = $(NAMESPACE) +endif +endif + +ifeq ($(OP),onetimeauth) +ifeq ($(SRCS),onetimeauth.jazz) +FUNCTIONS = $(NAMESPACE) $(NAMESPACE)_verify +endif +endif + +ifeq ($(OP),scalarmult) +ifeq ($(SRCS),scalarmult.jazz) +FUNCTIONS = $(NAMESPACE) $(NAMESPACE)_base +endif +endif + +ifeq ($(OP),secretbox) +ifeq ($(SRCS),secretbox.jazz) +FUNCTIONS = $(NAMESPACE) $(NAMESPACE)_open +endif +endif + +ifeq ($(OP),sign) +ifeq ($(SRCS),sign.jazz) +FUNCTIONS = $(NAMESPACE)_keypair $(NAMESPACE) $(NAMESPACE)_open +endif +endif + +ifeq ($(OP),xof) +ifeq ($(SRCS),xof.jazz) +FUNCTIONS = $(NAMESPACE) +endif +endif + + +# ----------------------------------------------------------------------------- +# ci vars -# -------------------------------------------------------------------- CI_DIR = -CIT = +CI_CMD = ifeq ($(CI),1) CI_DIR := .ci -CIT = 2> $(CI_DIR)/$(@F).log && rm -f $(CI_DIR)/$(@F).error || \ - (echo $$? > $(CI_DIR)/$(@F).error && \ - cat $(CI_DIR)/$(@F).log >> $(CI_DIR)/$(@F).error && \ - rm $(CI_DIR)/$(@F).log && \ - exit 127) +CI_CMD = 2> $(CI_DIR)/$(@F).log && rm -f $(CI_DIR)/$(@F).error || \ + (echo $$? | cat - $(CI_DIR)/$(@F).log > $(CI_DIR)/$(@F).error && \ + rm $(CI_DIR)/$(@F).log && \ + exit 127 \ + ) endif -# -------------------------------------------------------------------- -JEXT ?= jazz -override JFLAGS += -noinsertarraycopy $(addprefix -slice ,$(FUNCTIONS)) -JINCLUDE = -I Jade:$(SRC) -JASMIN ?= jasminc -JASMINC := $(JASMIN) $(JFLAGS) $(JINCLUDE) -COMPILE = ($(JASMINC) -o $@ $<) $(CIT) +# ----------------------------------------------------------------------------- +# compile vars -# -------------------------------------------------------------------- -CHECKS_DIR := checks +JASMIN ?= jasminc -# -------------------------------------------------------------------- -DEPS_DIR := .deps -DEPS = ((printf "$@: "; printf "$< "; $(JASMINC) -print-dependencies $<) > $(DEPS_DIR)/$(@F).d) $(CIT) -DEPFILES := +JEXT ?= jazz +override JFLAGS += -stack-zero loopSCT -noinsertarraycopy +JINCLUDE ?= -I formosa25519:$(SRC) -# -------------------------------------------------------------------- -compile: $(SRCS:%.$(JEXT)=%.s) - @true +JASMIN_COMPILE = ($(JASMIN) $(JFLAGS) $(JINCLUDE) -o $@ $<) $(CI_CMD) -# -------------------------------------------------------------------- -# Note: by using a single-file extraction, only one Jasmin file can be processed (the first from SRCS) +ASSEMBLY_FILES = $(SRCS:%.$(JEXT)=%.s) -extract: $(EC_DIR)/extracted_s.ec $(EC_DIR)/extracted_ct.ec - @true -$(EC_DIR)/extracted_s.ec : $(SRCS) $(DEPS_DIR)/extracted_s.ec.d | $(DEPS_DIR) $(EC_DIR) $(CI_DIR) - $(DEPS) - $(EXTRACT_S) +# preprocessing vars -$(EC_DIR)/extracted_ct.ec : $(SRCS) $(DEPS_DIR)/extracted_ct.ec.d | $(DEPS_DIR) $(EC_DIR) $(CI_DIR) - $(DEPS) - $(EXTRACT_CT) +JPP ?= $(PROJECT_DIR)/scripts/releaser/jpp +PREPROCESSED_FILES := $(SRCS:%.$(JEXT)=%.jpp) +JASMIN_PREPROCESS = ($(JPP) $(JINCLUDE) -b $(PROJECT_PARENT_DIR)/ -out $@ -in $<) $(CI_CMD) -# -------------------------------------------------------------------- -extract0: extract_s extract_ct - @true +# ----------------------------------------------------------------------------- +# extraction vars -extract_s: $(SRCS:%.$(JEXT)=$(EC_DIR)/%_s.ec) - @true +EXTRACT_DIR = $(PROOF)/$(REL_IMPLEMENTATION_DIR) +EXTRACT_ARRAY_DIR = $(PROOF)/arrays +EFLAGS ?= $(addprefix -ec , $(FUNCTIONS)) + +JASMIN_EXTRACT = (cd $(EXTRACT_DIR) && $(JASMIN) $(JINCLUDE) $(EFLAGS) -oecarray $(EXTRACT_ARRAY_DIR) -oec $(notdir $@) $(ABS_IMPLEMENTATION_DIR)/$<) $(CI_CMD) + +EASYCRYPT_FILES = $(SRCS:%.$(JEXT)=$(EXTRACT_DIR)/%_s.ec) + + +# ----------------------------------------------------------------------------- +# dependencies vars + +DEPS_DIR ?= .deps +DEPS = ((printf "$@: "; printf "$< "; $(JASMIN) $(JINCLUDE) -print-dependencies $<) > $(DEPS_DIR)/$(@F).d) $(CI_CMD) +DEPFILES ?= -extract_ct: $(SRCS:%.$(JEXT)=$(EC_DIR)/%_ct.ec) + +# ----------------------------------------------------------------------------- +# default rule + +default: compile + + +# ----------------------------------------------------------------------------- +# preprocess rules + +preprocess: $(PREPROCESSED_FILES) @true -%.s : %.$(JEXT) $(DEPS_DIR)/%.s.d | $(DEPS_DIR) $(CI_DIR) +$(PREPROCESSED_FILES): +%.jpp: %.$(JEXT) $(DEPS_DIR)/%.s.d | $(DEPS_DIR) $(CI_DIR) $(DEPS) - $(COMPILE) + $(JASMIN_PREPROCESS) + +preprocess-inplace: preprocess + for file in $(SRCS); do mv $${file%.$(JEXT)}.jpp $$file; done + +revert-preprocess-inplace: + for file in $(SRCS); do git checkout $$file; done + +# ----------------------------------------------------------------------------- +# compilation rules + +compile: $(ASSEMBLY_FILES) + @true -$(EC_DIR)/%_s.ec : %.$(JEXT) $(DEPS_DIR)/%_s.ec.d | $(DEPS_DIR) $(EC_DIR) $(CI_DIR) +$(ASSEMBLY_FILES): +%.s: %.$(JEXT) $(DEPS_DIR)/%.s.d | $(DEPS_DIR) $(CI_DIR) $(DEPS) - $(EXTRACT_S) + $(JASMIN_COMPILE) + + +# ----------------------------------------------------------------------------- +# extraction rules + +extract-to-easycrypt: $(EASYCRYPT_FILES) + @true -$(EC_DIR)/%_ct.ec : %.$(JEXT) $(DEPS_DIR)/%_ct.ec.d | $(DEPS_DIR) $(EC_DIR) $(CI_DIR) +$(EASYCRYPT_FILES): +$(EXTRACT_DIR)/%_s.ec : %.$(JEXT) $(DEPS_DIR)/%_s.ec.d | $(DEPS_DIR) $(EXTRACT_DIR) $(EXTRACT_ARRAY_DIR) $(CI_DIR) $(DEPS) - $(EXTRACT_CT) + $(JASMIN_EXTRACT) -# -------------------------------------------------------------------- -include $(BC)/Makefile.checksafety +# ----------------------------------------------------------------------------- +# include Makefiles for checking implementations' properties -# -------------------------------------------------------------------- +include $(BUILD_COMMON)/Makefile.checksafety +include $(BUILD_COMMON)/Makefile.checksct -include $(BC)/Makefile.checksct -# -------------------------------------------------------------------- -$(CHECKSDIR): ; @mkdir -p $@ +# ----------------------------------------------------------------------------- +# directories + $(DEPS_DIR): ; @mkdir -p $@ -$(EC_DIR): ; @mkdir -p $@; touch $@/.gitkeep +$(EXTRACT_DIR): ; @mkdir -p $@; touch $@/.gitkeep +$(EXTRACT_ARRAY_DIR): ; @mkdir -p $@; touch $@/.gitkeep ifeq ($(CI),1) $(CI_DIR): ; @mkdir -p $@ endif @@ -109,26 +185,70 @@ endif DEPFILES := \ $(DEPFILES) \ $(SRCS:%.$(JEXT)=$(DEPS_DIR)/%.s.d) \ - $(SRCS:%.$(JEXT)=$(DEPS_DIR)/%_s.ec.d) \ - $(SRCS:%.$(JEXT)=$(DEPS_DIR)/%_ct.ec.d) \ - $(DEPS_DIR)/extracted_s.ec.d \ - $(DEPS_DIR)/extracted_ct.ec.d + $(SRCS:%.$(JEXT)=$(DEPS_DIR)/%_s.ec.d) $(DEPFILES): include $(wildcard $(DEPFILES)) -# -------------------------------------------------------------------- -.PHONY: .jflags -.jflags: - @echo -n "$(JFLAGS)" > .jflags + +# ----------------------------------------------------------------------------- +# the following rule records the flags used to compile the implementation +# these are used by the release script + +.PHONY: .JFLAGS +.JFLAGS: + @echo -n "$(JFLAGS)" > .JFLAGS + # -------------------------------------------------------------------- -.PHONY: clean +.PHONY: clean distclean clean: - @rm -fr $(DEPS_DIR) $(CHECKS_DIR) $(SAFETY_DIR) *.s *.safety* *.sct* *.o *.a .jflags *.out -ifeq ($(CI),1) - @rm -fr $(CI_DIR) -endif + rm -fr $(CI_DIR) $(DEPS_DIR) *.jpp *.s *.safety* *.sct* *.o .JFLAGS + +distclean: clean + rm -fr $(EASYCRYPT_FILES) + +# -------------------------------------------------------------------- +debug-print-variables: + @echo "" + @echo "Path variables:" + @echo " PROJECT_DIR: $(PROJECT_DIR)" + @echo " SRC: $(SRC)" + @echo " TEST: $(TEST)" + @echo " PROOF: $(PROOF)" + @echo " ABS_IMPLEMENTATION_DIR: $(ABS_IMPLEMENTATION_DIR)" + @echo " REL_IMPLEMENTATION_DIR: $(REL_IMPLEMENTATION_DIR)" + @echo "" + @echo "Implementation variables:" + @echo " OP: $(OP)" + @echo " NAMESPACE: $(NAMESPACE)" + @echo " FUNCTIONS: $(FUNCTIONS)" + @echo "" + @echo "CI variables:" + @echo " CI_DIR: $(CI_DIR)" + @echo " CI_CMD: not printed, it is rule dependent." + @echo "" + @echo "Compilation variables:" + @echo " JASMIN: $(JASMIN)" + @echo " JEXT: $(JEXT)" + @echo " JFLAGS: $(JFLAGS)" + @echo " JINCLUDE: $(JINCLUDE)" + @echo " SRCS: $(SRCS)" + @echo " ASSEMBLY_FILES: $(ASSEMBLY_FILES)" + @echo " JASMIN_COMPILE: not printed, it is rule dependent." + @echo "" + @echo "Preprocess variables:" + @echo " JPP: $(JPP)" + @echo " PREPROCESSED_FILES: $(PREPROCESSED_FILES)" + @echo " JASMIN_PREPROCESS: not printed, it is rule dependent." + @echo "" + @echo "Extraction variables:" + @echo " EXTRACT_DIR: $(EXTRACT_DIR)" + @echo " EXTRACT_ARRAY_DIR: $(EXTRACT_ARRAY_DIR)" + @echo " EFLAGS: $(EFLAGS)" + @echo " EASYCRYPT_FILES: $(EASYCRYPT_FILES)" + @echo " JASMIN_EXTRACT: not printed, it is rule dependent." + @echo "" diff --git a/proof/.gitignore b/proof/.gitignore index 837893af..582c0c2c 100644 --- a/proof/.gitignore +++ b/proof/.gitignore @@ -3,3 +3,4 @@ *_ct.ec *.ec.out *Array*.ec +arrays/ diff --git a/scripts/extract-all.sh b/scripts/extract-all.sh index 3b997727..160d49aa 100755 --- a/scripts/extract-all.sh +++ b/scripts/extract-all.sh @@ -30,3 +30,5 @@ for SUBMODULE in "$LIBJADE_ROOT"/submodules/formosa-*;do fi done done + +echo "include ../build-common/Makefile" > "$LIBJADE_SRC/Makefile" diff --git a/scripts/reporter/jlog b/scripts/reporter/jlog new file mode 100755 index 00000000..504cc54c --- /dev/null +++ b/scripts/reporter/jlog @@ -0,0 +1,72 @@ +#!/usr/bin/env bash + +message=$1 +top=$(cd "$(dirname "$0")/../../" ; pwd -P) +dir=$top/$2 +spattern=$3 +rempty=$4 + +NORMAL="\e[0m" +BOLD="\e[1m" +RED="\e[31m" +GREEN="\e[32m" +YELLOW='\e[33m' + +# given a pattern (for instance, *.TAG.log or *.TAG.error) and an output file +# - prints to $output the line counts for each *.TAG.log, sorted by the number of lines +status() +{ + pattern=$1; + output=$2; + + find $dir -name $pattern | \ + while read file; do + d=$(dirname $file); + b=$(basename $file); + c=$(wc -l <$file); + echo "$c, $d/$b"; + done | \ + sort -t',' -g -k1 | sed -e 's/^[ \t]*//' -e 's/, \.\//, /' > $output +} + +print() +{ + color=$1; + filter=$2; + file=$3; + label=$4; + + egrep -E "$filter" $file | \ + while read line; do + echo -e "${color}${BOLD}${label}, ${line}${NORMAL}" + done +} + +clear_empty() +{ + file=$1; + egrep -E "^0" $file | cut -d',' -f2 | \ + while read log; do + rm -f "$log"; + done +} + +warning=$(mktemp) +error=$(mktemp) + +status "${spattern}.log" $warning; +status "${spattern}.error" $error; + +# print +echo -e "${BOLD}$message: ${NORMAL}" + +print $GREEN "^0" $warning "OK"; +print $YELLOW "^[^0]" $warning "WARNING"; +print $RED "" $error "ERROR"; + +if [ "$rempty" == "1" ]; then + clear_empty $warning; +fi + +rm $warning $error +