From 454f76daccd835f7e4faffbea02f7b263a07e3f1 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Tue, 1 Oct 2024 21:02:41 +0100 Subject: [PATCH 1/5] jlog: add group and file cat to logs --- proof/Makefile | 8 ++++-- scripts/reporter/jlog | 64 ++++++++++++++++++++++++++++++++++--------- 2 files changed, 56 insertions(+), 16 deletions(-) diff --git a/proof/Makefile b/proof/Makefile index d7dcfa2..56e9be8 100644 --- a/proof/Makefile +++ b/proof/Makefile @@ -25,6 +25,7 @@ ALL_OUT := $(addsuffix .out, $(ALL)) CI ?= 0 CI_REMOVE_OK_LOGS ?= "1" +CI_GITHUB?=0 CI_DIR = CI_CMD = @@ -35,6 +36,7 @@ CI_CMD = 2> $(@D)/$(CI_DIR)/$(@F).log && rm -f $(@D)/$(CI_DIR)/$(@F).error || \ rm $(@D)/$(CI_DIR)/$(@F).log && \ exit 0 \ ) +CI_GITHUB:=1 endif export CI @@ -84,9 +86,9 @@ CI_ALL_FILES := $(shell find $(PROOF) -name '*.log') $(CI_ERROR_FILES) .PHONY: reporter logs $(LOGS) err reporter: - $(JLOG) "Extraction from Jasmin to EasyCrypt status" src/ *_s.ec $(CI_REMOVE_OK_LOGS) - $(JLOG) "Checking EasyCrypt - extracted files status" proof/ *_s.ec.out $(CI_REMOVE_OK_LOGS) - $(JLOG) "Checking EasyCrypt - all files status" proof/ *.ec.out $(CI_REMOVE_OK_LOGS) + $(JLOG) "Extraction from Jasmin to EasyCrypt status" src/ *_s.ec $(CI_REMOVE_OK_LOGS) $(CI_GITHUB) + $(JLOG) "Checking EasyCrypt - extracted files status" proof/ *_s.ec.out $(CI_REMOVE_OK_LOGS) $(CI_GITHUB) + $(JLOG) "Checking EasyCrypt - all files status" proof/ *.ec.out $(CI_REMOVE_OK_LOGS) $(CI_GITHUB) logs: $(LOGS) diff --git a/scripts/reporter/jlog b/scripts/reporter/jlog index 504cc54..1786939 100755 --- a/scripts/reporter/jlog +++ b/scripts/reporter/jlog @@ -5,8 +5,9 @@ top=$(cd "$(dirname "$0")/../../" ; pwd -P) dir=$top/$2 spattern=$3 rempty=$4 +ghci=$5 -NORMAL="\e[0m" +RESET="\e[0m" BOLD="\e[1m" RED="\e[31m" GREEN="\e[32m" @@ -29,16 +30,53 @@ status() sort -t',' -g -k1 | sed -e 's/^[ \t]*//' -e 's/, \.\//, /' > $output } -print() +# cat file in color +cat_c_file() +{ + color=$1 + file=$2 + + echo -e "${color}" + cat $file + echo -e "${RESET}" +} + +# print bold color - some string and a valid file name +print_bc() +{ + prefix=$1 + color=$2 + string=$3 + file_name=$4 + + file_name_relative=$(realpath --relative-to=$top $file_name) + + echo -e "${prefix}${color}${string}${file_name_relative}${RESET}" +} + +print_file() { color=$1; filter=$2; file=$3; label=$4; + begin_group="" + end_group="" + if [[ $ghci -eq 1 ]]; then + begin_group="::group::" + end_group="::endgroup::" + fi + egrep -E "$filter" $file | \ - while read line; do - echo -e "${color}${BOLD}${label}, ${line}${NORMAL}" + while IFS=',' read -r line_count file_name; do + if [[ "$line_count" != "0" ]]; then + print_bc "${begin_group}" "${color}" "${label}, ${line_count}, " "${file_name}" + if [[ $ghci -eq 1 ]]; then cat_c_file "${color}" "${file_name}"; fi + if [[ $ghci -eq 1 ]]; then echo "${end_group}"; fi + else + print_bc "" "${color}" "${label}, 0" "${file_name}" + fi done } @@ -51,22 +89,22 @@ clear_empty() done } -warning=$(mktemp) -error=$(mktemp) +okandwarnings=$(mktemp) +errors=$(mktemp) -status "${spattern}.log" $warning; -status "${spattern}.error" $error; +status "${spattern}.log" $okandwarnings; +status "${spattern}.error" $errors; # print echo -e "${BOLD}$message: ${NORMAL}" -print $GREEN "^0" $warning "OK"; -print $YELLOW "^[^0]" $warning "WARNING"; -print $RED "" $error "ERROR"; +print_file $GREEN "^0" $okandwarnings "OK"; +print_file $YELLOW "^[^0]" $okandwarnings "WARNING"; +print_file $RED "" $errors "ERROR"; if [ "$rempty" == "1" ]; then - clear_empty $warning; + clear_empty $okandwarnings; fi -rm $warning $error +rm $okandwarnings $errors From ada6fa4a28611c068327cc493964fe468bf0e59d Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Tue, 1 Oct 2024 21:21:00 +0100 Subject: [PATCH 2/5] jlog: in src/ test/ bench/ + some refactor --- .github/workflows/amd64-linux.yml | 14 +++++++++----- bench/Makefile | 8 +++++--- proof/Makefile | 7 +++++++ scripts/reporter/jlog | 2 +- src/Makefile | 24 +++++++++++++++++++----- test/Makefile | 10 ++++++---- 6 files changed, 47 insertions(+), 18 deletions(-) diff --git a/.github/workflows/amd64-linux.yml b/.github/workflows/amd64-linux.yml index ced649b..f1b2742 100644 --- a/.github/workflows/amd64-linux.yml +++ b/.github/workflows/amd64-linux.yml @@ -19,7 +19,7 @@ jobs: - name: check safety run: make -j$JOBS -C src/ CI=1 check-safety - name: print report - run: make -C src/ CI=1 reporter + run: make -C src/ CI=1 reporter-check-safety - name: return error run: make -C src/ CI=1 err @@ -32,7 +32,7 @@ jobs: - 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 + run: make -C src/ CI=1 reporter-check-sct - name: return error run: make -C src/ CI=1 err @@ -45,7 +45,7 @@ jobs: - 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 + run: make -C src/ CI=1 reporter-extract-to-easycrypt - name: return error run: make -C src/ CI=1 err @@ -58,7 +58,7 @@ jobs: - 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 + run: make -C src/ CI=1 reporter-compile - name: return error run: make -C src/ CI=1 err @@ -92,6 +92,10 @@ jobs: uses: actions/checkout@v4 - name: run proof - run: make -j$JOBS -C proof/ + run: make -j$JOBS -C proof/ all-no-report + - name: print report + run: make -C proof/ CI=1 reporter + - name: return error + run: make -C proof/ CI=1 err diff --git a/bench/Makefile b/bench/Makefile index ba13a78..d445236 100644 --- a/bench/Makefile +++ b/bench/Makefile @@ -12,6 +12,7 @@ CFLAGS ?= -Wall -Wno-unused-function -Wno-unused-parameter -O3 -march=native \ CI ?= 0 CI_REMOVE_OK_LOGS ?= "1" +CI_GITHUB?=0 CI_DIR = $(@D) CI_CMD = @@ -22,6 +23,7 @@ CI_CMD = 2> $(CI_DIR)/$(@F).log && rm -f $(CI_DIR)/$(@F).error || \ rm -f $(CI_DIR)/$(@F).log && \ exit 127 \ ) +CI_GITHUB:=1 endif export CI @@ -155,9 +157,9 @@ CI_ALL_FILES := $(shell test -d $(BIN) && find $(BIN) -name '*.log') $(CI_ERRO .PHONY: reporter logs $(LOGS) err reporter: - $(JLOG) "Compilation status (*.jazz -> *.s)" src/ *.s $(CI_REMOVE_OK_LOGS) - $(JLOG) "Bench compilation status" bench/$(BIN) bench $(CI_REMOVE_OK_LOGS) - $(JLOG) "Bench execution status" bench/$(BIN) bench.out $(CI_REMOVE_OK_LOGS) + $(JLOG) "Compilation status (*.jazz -> *.s)" src/ *.s $(CI_REMOVE_OK_LOGS) $(CI_GITHUB) + $(JLOG) "Bench compilation status" bench/$(BIN) bench $(CI_REMOVE_OK_LOGS) $(CI_GITHUB) + $(JLOG) "Bench execution status" bench/$(BIN) bench.out $(CI_REMOVE_OK_LOGS) $(CI_GITHUB) logs: $(LOGS) diff --git a/proof/Makefile b/proof/Makefile index 56e9be8..cb82935 100644 --- a/proof/Makefile +++ b/proof/Makefile @@ -120,6 +120,13 @@ all: $(MAKE) reporter $(MAKE) err +all-no-report: CI=1 +all-no-report: + $(MAKE) distclean + $(MAKE) -C $(SRC) extract-to-easycrypt + $(MAKE) check-extracted + $(MAKE) check-all + # ----------------------------------------------------------------------------- # clean rules diff --git a/scripts/reporter/jlog b/scripts/reporter/jlog index 1786939..b5c24bf 100755 --- a/scripts/reporter/jlog +++ b/scripts/reporter/jlog @@ -75,7 +75,7 @@ print_file() if [[ $ghci -eq 1 ]]; then cat_c_file "${color}" "${file_name}"; fi if [[ $ghci -eq 1 ]]; then echo "${end_group}"; fi else - print_bc "" "${color}" "${label}, 0" "${file_name}" + print_bc "" "${color}" "${label}, 0, " "${file_name}" fi done } diff --git a/src/Makefile b/src/Makefile index cdbe2ac..30831c1 100644 --- a/src/Makefile +++ b/src/Makefile @@ -33,6 +33,11 @@ C_HEADER_FILES ?= $(addsuffix include/api.h, $(dir $(ASSEMBLY_FILES))) # of the current status: compilation, safety checking, and sct checking. CI ?= 0 CI_REMOVE_OK_LOGS ?= "1" +CI_GITHUB?=0 + +ifeq ($(CI),1) +CI_GITHUB:=1 +endif export CI @@ -141,12 +146,21 @@ CI_ERROR_FILES := $(shell find $(SRC) -name '*.error') CI_ALL_FILES := $(shell find $(SRC) -name '*.log') $(CI_ERROR_FILES) .PHONY: reporter logs $(LOGS) err +.PHONY: reporter-check-safety reporter-check-sct reporter-extract-to-easycrypt reporter-compile + +reporter: reporter-check-safety reporter-check-sct reporter-extract-to-easycrypt reporter-compile + +reporter-check-safety: + $(JLOG) "Safety checking status" src/ *.safety $(CI_REMOVE_OK_LOGS) $(CI_GITHUB) + +reporter-check-sct: + $(JLOG) "Speculative constant-time status" src/ *.sct $(CI_REMOVE_OK_LOGS) $(CI_GITHUB) + +reporter-extract-to-easycrypt: + $(JLOG) "Extraction to EasyCrypt status" src/ *.ec $(CI_REMOVE_OK_LOGS) $(CI_GITHUB) -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) +reporter-compile: + $(JLOG) "Compilation status (*.jazz -> *.s)" src/ *.s $(CI_REMOVE_OK_LOGS) $(CI_GITHUB) logs: $(LOGS) diff --git a/test/Makefile b/test/Makefile index ab5b533..e9d9752 100644 --- a/test/Makefile +++ b/test/Makefile @@ -10,6 +10,7 @@ CFLAGS ?= -O3 -Wall -Wextra -Wpedantic -Wvla -Werror -std=c99 \ CI ?= 0 CI_REMOVE_OK_LOGS ?= "1" +CI_GITHUB?=0 CI_DIR = $(@D) CI_CMD = @@ -20,6 +21,7 @@ CI_CMD = 2> $(CI_DIR)/$(@F).log && rm -f $(CI_DIR)/$(@F).error || \ rm -f $(CI_DIR)/$(@F).log && \ exit 127 \ ) +CI_GITHUB:=1 endif export CI @@ -125,13 +127,13 @@ CI_ALL_FILES := $(shell test -d $(BIN) && find $(BIN) -name '*.log') $(CI_ERRO .PHONY: reporter logs $(LOGS) err reporter: - $(JLOG) "Compilation status (*.jazz -> *.s)" src/ *.s $(CI_REMOVE_OK_LOGS) + $(JLOG) "Compilation status (*.jazz -> *.s)" src/ *.s $(CI_REMOVE_OK_LOGS) $(CI_GITHUB) @for type in $(TESTS_NAMES); do \ - $(JLOG) "Tests compilation status - $$type" test/$(BIN) $$type $(CI_REMOVE_OK_LOGS); \ - $(JLOG) "Tests execution status - $$type" test/$(BIN) $$type.out $(CI_REMOVE_OK_LOGS); \ + $(JLOG) "Tests compilation status - $$type" test/$(BIN) $$type $(CI_REMOVE_OK_LOGS) $(CI_GITHUB); \ + $(JLOG) "Tests execution status - $$type" test/$(BIN) $$type.out $(CI_REMOVE_OK_LOGS) $(CI_GITHUB); \ done $(JCHK) - $(JLOG) "Checksums status" test/$(BIN) checksum*.ok $(CI_REMOVE_OK_LOGS); + $(JLOG) "Checksums status" test/$(BIN) checksum*.ok $(CI_REMOVE_OK_LOGS) $(CI_GITHUB); logs: $(LOGS) From de9e3e45ff5b9db59f1edfe174957d38bc6de039 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Tue, 1 Oct 2024 21:26:38 +0100 Subject: [PATCH 3/5] jlog, makefile proof, trying script option --- proof/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof/Makefile b/proof/Makefile index cb82935..972ed58 100644 --- a/proof/Makefile +++ b/proof/Makefile @@ -70,7 +70,7 @@ $(ALL_OUT): ifeq ($(CI),1) mkdir -p $(@D)/$(CI_DIR) endif - ($(EASYCRYPT) -R arrays/ -R $(abspath $(@D)/../../) $(ECARGS) $(subst .out,,$@) > $@) $(CI_CMD) || !(($(FAIL_ON_ERROR))) + ($(EASYCRYPT) -script -R arrays/ -R $(abspath $(@D)/../../) $(ECARGS) $(subst .out,,$@) > $@) $(CI_CMD) || !(($(FAIL_ON_ERROR))) # ----------------------------------------------------------------------------- From 8d795f04320a12374560d94c359161182d7fee3c Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Tue, 1 Oct 2024 21:30:59 +0100 Subject: [PATCH 4/5] Revert "jlog, makefile proof, trying script option" This reverts commit de9e3e45ff5b9db59f1edfe174957d38bc6de039. --- proof/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof/Makefile b/proof/Makefile index 972ed58..cb82935 100644 --- a/proof/Makefile +++ b/proof/Makefile @@ -70,7 +70,7 @@ $(ALL_OUT): ifeq ($(CI),1) mkdir -p $(@D)/$(CI_DIR) endif - ($(EASYCRYPT) -script -R arrays/ -R $(abspath $(@D)/../../) $(ECARGS) $(subst .out,,$@) > $@) $(CI_CMD) || !(($(FAIL_ON_ERROR))) + ($(EASYCRYPT) -R arrays/ -R $(abspath $(@D)/../../) $(ECARGS) $(subst .out,,$@) > $@) $(CI_CMD) || !(($(FAIL_ON_ERROR))) # ----------------------------------------------------------------------------- From b8aab929710bc7e62e125427ea183e1fb56793a3 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Tue, 1 Oct 2024 21:48:57 +0100 Subject: [PATCH 5/5] jlog: removing \r --- scripts/reporter/jlog | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/reporter/jlog b/scripts/reporter/jlog index b5c24bf..b30c7ce 100755 --- a/scripts/reporter/jlog +++ b/scripts/reporter/jlog @@ -37,7 +37,7 @@ cat_c_file() file=$2 echo -e "${color}" - cat $file + sed '/\r/d' $file | uniq | cat - echo -e "${RESET}" }