linting: add shellcheck for shell script lint

META.sh

@@ -17,17 +17,17 @@ META=META.yml
 # Manual extraction of metadata with basic cmd line tools
 VAL=$(cat $META |
   grep "name\|$2" |
-  grep $1 -A 1 |
-  grep $2 |
+  grep "$1" -A 1 |
+  grep "$2" |
   cut -d ":" -f 2 | tr -d ' ')
 
 # More robust extraction using yq
-if (which yq 2>&1 >/dev/null); then
+if (which yq >/dev/null 2>&1); then
   QUERY=".implementations | .[] | select(.name==\"$1\") | .\"$2\""
-  echo "cat $META | yq "$QUERY" -r"
+  echo "cat $META | yq \"$QUERY\" -r"
   VAL_JQ=$(cat $META | yq "$QUERY" -r)
 
-  if [[ $VAL_JQ != $VAL ]]; then
+  if [[ $VAL_JQ != "$VAL" ]]; then
     echo "ERROR parsing metadata file $META"
     exit 1
   fi
@@ -43,5 +43,5 @@ if [[ $INPUT != "" ]]; then
     exit 0
   fi
 else
-  echo $VAL
+  echo "$VAL"
 fi

nix/util.nix

@@ -88,7 +88,8 @@ rec {
 
       inherit (pkgs)
         nixpkgs-fmt
-        shfmt;
+        shfmt
+        shellcheck;
 
       inherit (pkgs.python3Packages)
         mpmath sympy black pyparsing pyyaml;

proofs/cbmc/list_proofs.sh

@@ -6,5 +6,5 @@
 # which are those containing a *harness.c file.
 
 ROOT=$(git rev-parse --show-toplevel)
-cd $ROOT
+cd "$ROOT" || exit
 ls -1 proofs/cbmc/**/*harness.c | cut -d '/' -f 3

proofs/hol_light/x86_64/list_proofs.sh

@@ -6,5 +6,5 @@
 # we have a spec and proof in HOL-Light.
 
 ROOT=$(git rev-parse --show-toplevel)
-cd $ROOT
+cd "$ROOT" || exit
 ls -1 proofs/hol_light/x86_64/mldsa/*.S | cut -d '/' -f 5 | sed 's/\.S//'

proofs/hol_light/x86_64/proofs/build-proof.sh

@@ -34,7 +34,8 @@ output_path=$3
 output_dir=$(dirname "$output_path")
 [ -d "$output_dir" ] || mkdir -p "$output_dir"
 
-export HOLLIGHT_DIR="$(dirname ${hol_sh_cmd})"
+HOLLIGHT_DIR="$(dirname "${hol_sh_cmd}")"
+export HOLLIGHT_DIR
 if [ ! -f "${HOLLIGHT_DIR}/hol_lib.cmxa" ]; then
   echo "hol_lib.cmxa does not exist in HOLLIGHT_DIR('${HOLLIGHT_DIR}')."
   echo "Did you compile HOL Light with HOLLIGHT_USE_MODULE set to 1?"
@@ -50,20 +51,20 @@ echo "Generating a template .ml that loads the file...: ${template_ml}"
   echo "check_axioms ();;"
   echo 'let proof_end_time = Unix.time();;'
   echo 'Printf.printf "Running time: %f sec, Start unixtime: %f, End unixtime: %f\n" (proof_end_time -. proof_start_time) proof_start_time proof_end_time;;'
-) >>${template_ml}
+) >>"${template_ml}"
 
 inlined_prefix="$(mktemp)"
 inlined_ml="${inlined_prefix}.ml"
 inlined_cmx="${inlined_prefix}.cmx"
-(cd "${S2N_BIGNUM_DIR}" && HOLLIGHT_LOAD_PATH=${ROOT} ocaml ${HOLLIGHT_DIR}/inline_load.ml "${template_ml}" "${inlined_ml}")
+(cd "${S2N_BIGNUM_DIR}" && HOLLIGHT_LOAD_PATH=${ROOT} ocaml "${HOLLIGHT_DIR}"/inline_load.ml "${template_ml}" "${inlined_ml}")
 
 # Give a large stack size.
 OCAMLRUNPARAM=l=2000000000 \
   ocamlopt.byte -pp "$(${hol_sh_cmd} -pp)" -I "${HOLLIGHT_DIR}" -I +unix -c \
-  hol_lib.cmxa ${inlined_ml} -o ${inlined_cmx} -w -a
+  hol_lib.cmxa "${inlined_ml}" -o "${inlined_cmx}" -w -a
 ocamlfind ocamlopt -package zarith,unix -linkpkg hol_lib.cmxa \
-  -I "${HOLLIGHT_DIR}" ${inlined_cmx} \
+  -I "${HOLLIGHT_DIR}" "${inlined_cmx}" \
   -o "${output_path}"
 
 # Remove the intermediate files to save disk space
-rm -f ${inlined_cmx} ${template_ml} ${inlined_ml}
+rm -f "${inlined_cmx}" "${template_ml}" "${inlined_ml}"

scripts/format

@@ -13,8 +13,6 @@ ROOT="$(realpath "$(dirname "$0")"/../)"
 # Standard color definitions
 GREEN="\033[32m"
 RED="\033[31m"
-BLUE="\033[94m"
-BOLD="\033[1m"
 NORMAL="\033[0m"
 
 # utility
@@ -29,36 +27,40 @@ error()
 }
 
 info "Formatting nix files"
-if ! command -v nixpkgs-fmt 2>&1 >/dev/null; then
+if ! command -v nixpkgs-fmt >/dev/null 2>&1; then
   error "nixpkgs-fmt not found. Are you running in a nix shell? See BUILDING.md."
   exit 1
 fi
 
 nixpkgs-fmt "$ROOT"
 
 info "Formatting shell scripts"
-if ! command -v shfmt 2>&1 >/dev/null; then
+if ! command -v shfmt >/dev/null 2>&1; then
   error "shfmt not found. Are you running in a nix shell? See BUILDING.md."
   exit 1
 fi
-shfmt -s -w -l -i 2 -ci -fn $(shfmt -f $(git grep -l '' :/))
+
+# Find all scripts in the repo
+ALL_FILES=$(git grep -l '' :/)
+SHELL_SCRIPTS=$(echo "$ALL_FILES" | xargs shfmt -f)
+echo $SHELL_SCRIPTS | xargs shfmt -s -w -l -i 2 -ci -fn
 
 info "Formatting python scripts"
-if ! command -v black 2>&1 >/dev/null; then
+if ! command -v black >/dev/null 2>&1; then
   error "black not found. Are you running in a nix shell? See BUILDING.md."
   exit 1
 fi
 black --include "(scripts/tests|scripts/simpasm|scripts/cfify|scripts/autogen|scripts/check-namespace|\.py$)" "$ROOT"
 
 info "Formatting c files"
-if ! command -v clang-format 2>&1 >/dev/null; then
+if ! command -v clang-format >/dev/null 2>&1; then
   error "clang-format not found. Are you running in a nix shell? See BUILDING.md."
   exit 1
 fi
 
 nproc=$(getconf _NPROCESSORS_ONLN || echo 1)
 
-git ls-files -- ":/*.c" ":/*.h" | xargs -P $nproc -I {} sh -c '
+git ls-files -- ":/*.c" ":/*.h" | xargs -P "$nproc" -I {} sh -c '
   # Ignore symlinks
   if [[ ! -L {} ]]; then
     clang-format -i {}
@@ -67,7 +69,7 @@ git ls-files -- ":/*.c" ":/*.h" | xargs -P $nproc -I {} sh -c '
 info "Checking for eol"
 check-eol()
 {
-  git ls-files -- ":/" ":/!:*.png" | xargs -P $nproc -I {} sh -c '
+  git ls-files -- ":/" ":/!:*.png" | xargs -P "$nproc" -I {} sh -c '
     # Ignore symlinks
     if [[ ! -L {} && $(tail -c1 "{}" | wc -l) == 0 ]]; then
       echo "" >>"{}"

scripts/lint

@@ -20,8 +20,6 @@ fi
 # Standard color definitions
 GREEN="\033[32m"
 RED="\033[31m"
-BLUE="\033[94m"
-BOLD="\033[1m"
 NORMAL="\033[0m"
 
 info()
@@ -106,15 +104,37 @@ gh_error_simple()
   fi
 }
 
+run-shellcheck()
+{
+  if ! command -v shellcheck >/dev/null; then
+    gh_error_simple "Shellcheck missing" "shellcheck is not installed"
+    error "Lint shellcheck"
+    SUCCESS=false
+    gh_summary_failure "Lint shellcheck"
+    return 0
+  fi
+
+  checkerr "Lint shellcheck" "$(shellcheck --severity=warning $SHELL_SCRIPTS)"
+}
+
 # Formatting
 SUCCESS=true
 
+# Get list of shell scripts and .c/.h files for linting
+ALL_FILES=$(git grep -l '' :/)
+ALL_C_FILES=$(git ls-files ":/*.c" ":/*.h")
+SHELL_SCRIPTS=$(echo "$ALL_FILES" | xargs shfmt -f)
+
 gh_group_start "Linting nix files with nixpkgs-fmt"
 checkerr "Lint nix" "$(nixpkgs-fmt --check "$ROOT")"
 gh_group_end
 
 gh_group_start "Linting shell scripts with shfmt"
-checkerr "Lint shell" "$(shfmt -s -l -i 2 -ci -fn $(shfmt -f $(git grep -l '' :/)))"
+checkerr "Lint shell" "$(echo $SHELL_SCRIPTS | xargs shfmt -s -l -i 2 -ci -fn)"
+gh_group_end
+
+gh_group_start "Linting shell scripts with shellcheck"
+run-shellcheck
 gh_group_end
 
 gh_group_start "Linting python scripts with black"
@@ -130,7 +150,7 @@ fi
 gh_group_end
 
 gh_group_start "Linting c files with clang-format"
-checkerr "Lint C" "$(clang-format $(git ls-files ":/*.c" ":/*.h") --Werror --dry-run 2>&1 | grep "error:" | cut -d ':' -f 1,2 | tr ':' ' ')"
+checkerr "Lint C" "$(echo $ALL_C_FILES | xargs clang-format --Werror --dry-run 2>&1 | grep "error:" | cut -d ':' -f 1,2 | tr ':' ' ')"
 gh_group_end
 
 check-eol-dry-run()
@@ -152,22 +172,22 @@ check-spdx()
   local success=true
   for file in $(git ls-files -- ":/" ":/!:*.json" ":/!:*.png" ":/!:*LICENSE*" ":/!:.git*" ":/!:flake.lock"); do
     # Ignore symlinks
-    if [[ ! -L $file && $(grep "SPDX-License-Identifier:" $file | wc -l) == 0 ]]; then
+    if [[ ! -L $file && $(grep "SPDX-License-Identifier:" "$file" | wc -l) == 0 ]]; then
       gh_error "$file" "${line:-1}" "Missing license header error" "$file is missing SPDX License header"
       success=false
     fi
   done
   for file in $(git ls-files -- "*.[chsS]" "*.py" "*.mk" "*.yml" "**/Makefile*" ":/!proofs/cbmc/*.py" ":/!examples/bring_your_own_fips202/custom_fips202/tiny_sha3/*" ":/!examples/custom_backend/mldsa_native/src/fips202/native/custom/src/*"); do
     # Ignore symlinks
-    if [[ ! -L $file && $(grep "Copyright (c) The mldsa-native project authors" $file | wc -l) == 0 ]]; then
+    if [[ ! -L $file && $(grep "Copyright (c) The mldsa-native project authors" "$file" | wc -l) == 0 ]]; then
       gh_error "$file" "${line:-1}" "Missing copyright header error" "$file is missing copyright header"
       success=false
     fi
   done
   # For source files in dev/* and mldsa/*, we enforce `Apache-2.0 OR ISC OR MIT`
   for file in $(git ls-files -- "*.[chsSi]" | grep "^dev/\|^mldsa/"); do
     # Ignore symlinks
-    if [[ ! -L $file && $(grep "SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT" $file | wc -l) == 0 ]]; then
+    if [[ ! -L $file && $(grep "SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT" "$file" | wc -l) == 0 ]]; then
       gh_error "$file" "${line:-1}" "Missing license header error" "$file is not licensed under 'Apache-2.0 OR ISC OR MIT'"
       success=false
     fi
@@ -188,7 +208,7 @@ gh_group_end
 
 check-autogenerated-files()
 {
-  if python3 $ROOT/scripts/autogen --dry-run; then
+  if python3 "$ROOT"/scripts/autogen --dry-run; then
     info "Check native auto-generated files"
     gh_summary_success "Check native auto-generated files"
   else
@@ -204,7 +224,7 @@ gh_group_end
 
 check-magic()
 {
-  if python3 $ROOT/scripts/check-magic >/dev/null; then
+  if python3 "$ROOT"/scripts/check-magic >/dev/null; then
     info "Check magic constants"
     gh_summary_success "Check magic constants"
   else
@@ -224,7 +244,7 @@ fi
 
 check-contracts()
 {
-  if python3 $ROOT/scripts/check-contracts >/dev/null; then
+  if python3 "$ROOT"/scripts/check-contracts >/dev/null; then
     info "Check contracts"
     gh_summary_success "Check contracts"
   else