run_hacl.sh (4419B)
1 #!/usr/bin/env bash 2 3 if [[ $(id -u) -eq 0 ]]; then 4 # Drop privileges by re-running this script. 5 # Note: this mangles arguments, better to avoid running scripts as root. 6 exec su worker -c "$0 $*" 7 fi 8 9 set -e -x -v 10 11 export HACL_STAR=~/hacl-star 12 export KARAMEL=~/karamel 13 export LIBCRUX=~/libcrux 14 15 # HACL* 16 git clone -q "https://github.com/hacl-star/hacl-star" ${HACL_STAR} 17 git -C ${HACL_STAR} checkout -q 0f136f28935822579c244f287e1d2a1908a7e552 18 19 # Format the C snapshot. 20 cd ${HACL_STAR}/dist/mozilla 21 cp ${VCS_PATH}/nss/.clang-format . 22 find . -type f -name '*.[ch]' -exec clang-format -i {} \+ 23 cd ${HACL_STAR}/dist/karamel 24 cp ${VCS_PATH}/nss/.clang-format . 25 find . -type f -name '*.[ch]' -exec clang-format -i {} \+ 26 cd ${HACL_STAR}/dist/gcc-compatible 27 cp ${VCS_PATH}/nss/.clang-format . 28 find . -type f -name '*.[ch]' -exec clang-format -i {} \+ 29 30 cd ${HACL_STAR} 31 patches=(${VCS_PATH}/nss/automation/taskcluster/scripts/patches/*.patch) 32 for f in "${patches[@]}"; do 33 git apply "$f" 34 done 35 36 # Libcrux 37 38 git clone -q "https://github.com/cryspen/libcrux" ${LIBCRUX} 39 git -C ${LIBCRUX} checkout -q 5a1d172a1bcff83bb401bfa718d08a2dc8c77e4e 40 41 cd ${LIBCRUX} 42 cp ${VCS_PATH}/nss/.clang-format . 43 find libcrux-ml-kem/extracts/c/generated -type f -name '*.[ch]' -exec clang-format -i {} \+ 44 45 # Karamel 46 git clone -q "https://github.com/FStarLang/karamel" ${KARAMEL} 47 git -C ${KARAMEL} checkout -q 80f5435f2fc505973c469a4afcc8d875cddd0d8b 48 49 cd ${KARAMEL} 50 cp ${VCS_PATH}/nss/.clang-format . 51 find include krmllib -type f -name '*.[ch]' -exec clang-format -i {} \+ 52 53 # These diff commands will return 1 if there are differences and stop the script. 54 55 # We have two checks in the script. 56 # The first one only checks the files in the verified/internal folder; the second one does for all the rest 57 # It was implemented like this due to not uniqueness of the names in the verified folders 58 # For instance, the files Hacl_Chacha20.h are present in both directories, but the content differs. 59 60 # TODO(Bug 1899443): remove these exceptions 61 files=($(find ${VCS_PATH}/nss/lib/freebl/verified/internal -type f -name '*.[ch]')) 62 for f in "${files[@]}"; do 63 file_name=$(basename "$f") 64 hacl_file=($(find ${HACL_STAR}/dist/mozilla/internal/ ${LIBCRUX}/libcrux-ml-kem/extracts/c/generated/internal -type f -name $file_name)) 65 if [ $file_name == "Hacl_Ed25519.h" \ 66 -o $file_name == "Hacl_Ed25519_PrecompTable.h" ] 67 then 68 continue 69 fi 70 diff -u $hacl_file $f 71 done 72 73 files=($(find ${VCS_PATH}/nss/lib/freebl/verified/ -type f -name '*.[ch]' -not -path "*/freebl/verified/internal/*" -not -path "*/freebl/verified/config.h" -not -path "*/freebl/verified/libcrux*")) 74 for f in "${files[@]}"; do 75 file_name=$(basename "$f") 76 hacl_file=($(find ${HACL_STAR}/dist/mozilla/ ${KARAMEL}/include/ ${KARAMEL}/krmllib/dist/minimal/ ${LIBCRUX}/libcrux-ml-kem/extracts/c/generated/ -type f -name $file_name -not -path "*/hacl-star/dist/mozilla/internal/*" -not -path "*/libcrux-ml-kem/extracts/c/generated/internal/*")) 77 if [ $file_name == "Hacl_P384.c" \ 78 -o $file_name == "Hacl_P384.h" \ 79 -o $file_name == "Hacl_P521.c" \ 80 -o $file_name == "Hacl_P521.h" \ 81 -o $file_name == "eurydice_glue.h" \ 82 -o $file_name == "target.h" ] 83 then 84 continue 85 fi 86 87 if [ $file_name == "Hacl_Ed25519.h" \ 88 -o $file_name == "Hacl_Ed25519.c" ] 89 then 90 continue 91 fi 92 diff -u $hacl_file $f 93 done 94 95 # Here we process the code that's not located in /hacl-star/dist/mozilla/ but 96 # /hacl-star/dist/gcc-compatible. 97 98 files=($(find ${VCS_PATH}/nss/lib/freebl/verified/internal -type f -name '*.[ch]')) 99 for f in "${files[@]}"; do 100 file_name=$(basename "$f") 101 hacl_file=($(find ${HACL_STAR}/dist/gcc-compatible/internal/ -type f -name $file_name)) 102 if [ $file_name != "Hacl_Ed25519.h" \ 103 -a $file_name != "Hacl_Ed25519_PrecompTable.h" ] 104 then 105 continue 106 fi 107 diff -u $hacl_file $f 108 done 109 110 files=($(find ${VCS_PATH}/nss/lib/freebl/verified/ -type f -name '*.[ch]' -not -path "*/freebl/verified/internal/*")) 111 for f in "${files[@]}"; do 112 file_name=$(basename "$f") 113 hacl_file=($(find ${HACL_STAR}/dist/gcc-compatible/ -type f -name $file_name -not -path "*/hacl-star/dist/gcc-compatible/internal/*")) 114 if [ $file_name != "Hacl_Ed25519.h" \ 115 -a $file_name != "Hacl_Ed25519.c" ] 116 then 117 continue 118 fi 119 diff -u $hacl_file $f 120 done