1#!/usr/bin/env bash 2# 3# Use this script to update the HACL generated hash algorithm implementation 4# code from a local checkout of the upstream hacl-star repository. 5# 6 7set -e 8set -o pipefail 9 10if [[ "${BASH_VERSINFO[0]}" -lt 4 ]]; then 11 echo "A bash version >= 4 required. Got: $BASH_VERSION" >&2 12 exit 1 13fi 14 15if [[ $1 == "" ]]; then 16 echo "Usage: $0 path-to-hacl-directory" 17 echo "" 18 echo " path-to-hacl-directory should be a local git checkout of a" 19 echo " https://github.com/hacl-star/hacl-star/ repo." 20 exit 1 21fi 22 23# Update this when updating to a new version after verifying that the changes 24# the update brings in are good. 25expected_hacl_star_rev=bb3d0dc8d9d15a5cd51094d5b69e70aa09005ff0 26 27hacl_dir="$(realpath "$1")" 28cd "$(dirname "$0")" 29actual_rev=$(cd "$hacl_dir" && git rev-parse HEAD) 30 31if [[ "$actual_rev" != "$expected_hacl_star_rev" ]]; then 32 echo "WARNING: HACL* in '$hacl_dir' is at revision:" >&2 33 echo " $actual_rev" >&2 34 echo "but expected revision:" >&2 35 echo " $expected_hacl_star_rev" >&2 36 echo "Edit the expected rev if the changes pulled in are what you want." 37fi 38 39# Step 1: copy files 40 41declare -a dist_files 42dist_files=( 43 Hacl_Hash_SHA2.h 44 Hacl_Streaming_Types.h 45 Hacl_Hash_SHA1.h 46 internal/Hacl_Hash_SHA1.h 47 Hacl_Hash_MD5.h 48 Hacl_Hash_SHA3.h 49 internal/Hacl_Hash_MD5.h 50 internal/Hacl_Hash_SHA3.h 51 Hacl_Hash_SHA2.c 52 internal/Hacl_Hash_SHA2.h 53 Hacl_Hash_SHA1.c 54 Hacl_Hash_MD5.c 55 Hacl_Hash_SHA3.c 56) 57 58declare -a include_files 59include_files=( 60 include/krml/lowstar_endianness.h 61 include/krml/internal/target.h 62) 63 64declare -a lib_files 65lib_files=( 66 krmllib/dist/minimal/FStar_UInt_8_16_32_64.h 67 krmllib/dist/minimal/fstar_uint128_struct_endianness.h 68 krmllib/dist/minimal/FStar_UInt128_Verified.h 69) 70 71# C files for the algorithms themselves: current directory 72(cd "$hacl_dir/dist/gcc-compatible" && tar cf - "${dist_files[@]}") | tar xf - 73 74# Support header files (e.g. endianness macros): stays in include/ 75(cd "$hacl_dir/dist/karamel" && tar cf - "${include_files[@]}") | tar xf - 76 77# Special treatment: we don't bother with an extra directory and move krmllib 78# files to the same include directory 79for f in "${lib_files[@]}"; do 80 cp "$hacl_dir/dist/karamel/$f" include/krml/ 81done 82 83# Step 2: some in-place modifications to keep things simple and minimal 84 85# This is basic, but refreshes of the vendored HACL code are infrequent, so 86# let's not over-engineer this. 87if [[ $(uname) == "Darwin" ]]; then 88 # You're already running with homebrew or macports to satisfy the 89 # bash>=4 requirement, so requiring GNU sed is entirely reasonable. 90 sed=gsed 91else 92 sed=sed 93fi 94 95readarray -t all_files < <(find . -name '*.h' -or -name '*.c') 96 97# types.h originally contains a complex series of if-defs and auxiliary type 98# definitions; here, we just need a proper uint128 type in scope 99# is a simple wrapper that defines the uint128 type 100cat > include/krml/types.h <<EOF 101#pragma once 102 103#include <inttypes.h> 104 105typedef struct FStar_UInt128_uint128_s { 106 uint64_t low; 107 uint64_t high; 108} FStar_UInt128_uint128, uint128_t; 109 110#define KRML_VERIFIED_UINT128 111 112#include "krml/lowstar_endianness.h" 113#include "krml/fstar_uint128_struct_endianness.h" 114#include "krml/FStar_UInt128_Verified.h" 115EOF 116# Adjust the include path to reflect the local directory structure 117$sed -i 's!#include.*types.h"!#include "krml/types.h"!g' "${all_files[@]}" 118$sed -i 's!#include.*compat.h"!!g' "${all_files[@]}" 119 120# FStar_UInt_8_16_32_64 contains definitions useful in the general case, but not 121# for us; trim! 122$sed -i -z 's!\(extern\|typedef\)[^;]*;\n\n!!g' include/krml/FStar_UInt_8_16_32_64.h 123 124# This contains static inline prototypes that are defined in 125# FStar_UInt_8_16_32_64; they are by default repeated for safety of separate 126# compilation, but this is not necessary. 127$sed -i 's!#include.*Hacl_Krmllib.h"!!g' "${all_files[@]}" 128 129# Use globally unique names for the Hacl_ C APIs to avoid linkage conflicts. 130$sed -i -z 's!#include <string.h>\n!#include <string.h>\n#include "python_hacl_namespaces.h"\n!' Hacl_Hash_*.h 131 132# Finally, we remove a bunch of ifdefs from target.h that are, again, useful in 133# the general case, but not exercised by the subset of HACL* that we vendor. 134$sed -z -i 's!#ifndef KRML_\(PRE_ALIGN\|POST_ALIGN\|ALIGNED_MALLOC\|ALIGNED_FREE\|HOST_TIME\)\n\(\n\|# [^\n]*\n\|[^#][^\n]*\n\)*#endif\n\n!!g' include/krml/internal/target.h 135$sed -z -i 's!\n\n\([^#][^\n]*\n\)*#define KRML_\(EABORT\|EXIT\)[^\n]*\(\n [^\n]*\)*!!g' include/krml/internal/target.h 136$sed -z -i 's!\n\n\([^#][^\n]*\n\)*#if [^\n]*\n\( [^\n]*\n\)*#define KRML_\(EABORT\|EXIT\|CHECK_SIZE\)[^\n]*\(\n [^\n]*\)*!!g' include/krml/internal/target.h 137$sed -z -i 's!\n\n\([^#][^\n]*\n\)*#if [^\n]*\n\( [^\n]*\n\)*# define _\?KRML_\(DEPRECATED\|HOST_SNPRINTF\)[^\n]*\n\([^#][^\n]*\n\|#el[^\n]*\n\|# [^\n]*\n\)*#endif!!g' include/krml/internal/target.h 138 139echo "Updated; verify all is okay using git diff and git status." 140