wip

Dockerfile.nsym

@@ -9,15 +9,25 @@ ARG GO_VERSION=1.20.1
 ARG GO_ARCHIVE="go${GO_VERSION}.linux-amd64.tar.gz"
 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections
 RUN apt-get update
-RUN apt-get install -y wget unzip git cmake clang llvm python3-pip libncurses5 opam libgmp-dev cabal-install
-RUN apt-get install -y g++-aarch64-linux-gnu lld
+RUN apt-get install -y curl wget unzip git cmake clang llvm g++-aarch64-linux-gnu lld python3-pip file
 
 RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \
    mkdir $GOROOT &&  mv go/* $GOROOT && rm $GO_ARCHIVE
-RUN pip3 install wllvm
-RUN pip3 install psutil
 
-ADD ./SAW/scripts /lc/scripts
+# Dependencies for Cryptol-Air-Interface
+# ghcup, ghc-8.10.7
+# libgmp-dev
+# zlib: libghc-bzlib-dev zlib1g-dev
+
+# Dependencies for Ocaml tools
+# apt-get install opam
+# opam init
+# eval $(opam env)
+# opam switch create 4.14.0
+# eval $(opam env)
+# opam install dune ppxlib ppx_deriving zarith odoc
+
+ADD ./NSym/scripts /lc/scripts
 RUN /lc/scripts/docker_install.sh
 ENV CRYPTOLPATH="../../../cryptol-specs:../../spec"
 

Dockerfile.saw

@@ -20,7 +20,7 @@ ADD ./SAW/scripts /lc/scripts
 RUN /lc/scripts/docker_install.sh
 ENV CRYPTOLPATH="../../../cryptol-specs:../../spec"
 
-# This container expects all files in the directory to be mounted or copied. 
+# This container expects all files in the directory to be mounted or copied.
 # The GitHub action will mount the workspace and set the working directory of the container.
 # Another way to mount the files is: docker run -v `pwd`:`pwd` -w `pwd` <name>
 

NSym/scripts/build_llvm.sh

@@ -14,8 +14,6 @@ export LDFLAGS="-fuse-ld=lld"
 
 export LLVM_COMPILER=clang
 export BINUTILS_TARGET_PREFIX=aarch64-linux-gnu
-export LLVM_COMPILER_PATH=/usr/lib/llvm-14/bin
-wllvm-sanity-checker
 
 cmake -DCMAKE_BUILD_TYPE=$BUILD_TYPE \
       -DKEEP_ASM_LOCAL_SYMBOLS=1 \

NSym/scripts/docker_entrypoint.sh

@@ -3,4 +3,4 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0
 
-(cd NSym && ./scripts/entrypoint_check.sh)
+(cd NSym && ./scripts/install.sh && ./scripts/entrypoint_check.sh)

NSym/scripts/docker_install.sh

@@ -0,0 +1,36 @@
+#!/bin/sh
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+set -ex
+
+Z3_URL='https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip'
+YICES_URL='https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz'
+
+mkdir -p /bin /deps
+
+# fetch Z3
+if [ ! -f /bin/z3 ]
+then
+    mkdir -p /deps/z3
+    wget $Z3_URL -O /deps/z3.zip
+    unzip /deps/z3.zip -d /deps/z3
+    cp /deps/z3/*/bin/z3 /bin/z3
+fi
+
+# install wllvm
+git clone https://github.com/travitch/whole-program-llvm /deps/whole-program-llvm
+cd /deps/whole-program-llvm
+git checkout cd8774483917f4de15da5a535179136bb55d5ae3
+pip3 install -e .
+
+# # fetch Yices
+# if [ ! -f /bin/yices ]
+# then
+#     mkdir -p /deps/yices
+#     wget $YICES_URL -O /deps/yices.tar.gz
+#     tar -x -f /deps/yices.tar.gz --one-top-level=/deps/yices
+#     cp /deps/yices/*/bin/yices /bin/yices
+#     cp /deps/yices/*/bin/yices-smt2 /bin/yices-smt2
+# fi

NSym/scripts/entrypoint_check.sh

@@ -8,3 +8,14 @@ set -ex
 ./scripts/build_aarch64.sh "Release" "neoverse-n1"
 ./scripts/build_llvm.sh "Release"
 ./scripts/post_build.sh
+
+# TODO: run proofs for graviton2
+
+rm -rf build/
+rm -rf build_src/
+
+./scripts/build_aarch64.sh "Release" "neoverse-512tvb"
+./scripts/build_llvm.sh "Release"
+./scripts/post_build.sh
+
+# TODO: run proofs for graviton3

NSym/scripts/install.sh

@@ -0,0 +1,41 @@
+#!/bin/sh
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+set -ex
+
+C2A_URL='https://cryptol-air-interface.s3.us-west-2.amazonaws.com/cryptol-air-interface-2023-11-06-9180412-Linux-x86_64.tar.gz'
+ELF_URL='https://ocaml-elf-loader.s3.us-west-2.amazonaws.com/elf_loader-2023-11-07-a1fcf84-Linux_x86_64.tar.gz'
+OSI_URL='https://ocaml-smt-interface.s3.us-west-2.amazonaws.com/ocaml_smt_interface-2023-11-07-9654c87-Linux_x86_64.tar.gz'
+NSYM_URL='https://native-code-symbolic-simulator.s3.us-west-2.amazonaws.com/nsym-2023-11-07-146e349-Linux_x86_64.tar.gz'
+
+mkdir -p /bin /.opam /deps
+
+# fetch Cryptol-Air-Interface
+rm -rf /deps/cryptol-air-interface
+mkdir -p /deps/cryptol-air-interface
+wget $C2A_URL -O /deps/cryptol-air-interface.tar.gz
+tar -x -f /deps/cryptol-air-interface.tar.gz --one-top-level=/deps/cryptol-air-interface
+cp /deps/cryptol-air-interface/*/bin/cryptol-to-air /bin/cryptol-to-air
+
+# fetch OCaml-SMT-Interface
+rm -rf /deps/ocaml-smt-interface
+mkdir -p /deps/ocaml-smt-interface
+wget $OSI_URL -O /deps/ocaml-smt-interface.tar.gz
+tar -x -f /deps/ocaml-smt-interface.tar.gz --one-top-level=/deps/ocaml-smt-interface
+cp -r /deps/ocaml-smt-interface/*/lib/. /.opam/lib/
+
+# fetch OCamlElfLoader
+rm -rf /deps/ocaml-elf-loader
+mkdir -p /deps/ocaml-elf-loader
+wget $ELF_URL -O /deps/ocaml-elf-loader.tar.gz
+tar -x -f /deps/ocaml-elf-loader.tar.gz --one-top-level=/deps/ocaml-elf-loader
+cp -r /deps/ocaml-elf-loader/*/lib/. /.opam/lib/
+
+# fetch NSym
+rm -rf /deps/nsym
+mkdir -p /deps/nsym
+wget $NSYM_URL -O /deps/nsym.tar.gz
+tar -x -f /deps/nsym.tar.gz --one-top-level=/deps/nsym
+cp -r /deps/nsym/*/lib/. /.opam/lib/

NSym/scripts/stage_nsym.sh

@@ -0,0 +1,48 @@
+#!/bin/bash
+
+PKG=NSym
+PKG_NAME=nsym
+ARCH=Linux_x86_64
+
+DATE=`date +%F`
+LIB_PATH=/root/.opam/4.14.0/lib
+
+CUR_PATH=`pwd`
+SRC_PATH=/root/${PKG}
+cd ${SRC_PATH}
+git config --global --add safe.directory ${SRC_PATH}
+COMMIT_HASH=`git rev-parse --short HEAD`
+dune build -p nsym_config @install
+dune install nsym_config
+dune build -p air @install
+dune install air
+dune build -p arm @install
+dune install arm
+dune build -p specs @install
+dune install specs
+dune build -p cosim @install
+dune install cosim
+
+echo $DATE
+echo $COMMIT_HASH
+
+RELEASE=${PKG_NAME}-${DATE}-${COMMIT_HASH}-${ARCH}
+TARGET=tmp/${RELEASE}
+
+echo ${RELEASE}
+
+cd ${CUR_PATH}
+rm -rf ./tmp
+mkdir -p ${TARGET}/lib
+cp -r ${LIB_PATH}/nsym_config ${TARGET}/lib/
+cp -r ${LIB_PATH}/air ${TARGET}/lib/
+cp -r ${LIB_PATH}/arm ${TARGET}/lib/
+cp -r ${LIB_PATH}/specs ${TARGET}/lib/
+cp -r ${LIB_PATH}/cosim ${TARGET}/lib/
+
+cd tmp
+find ${RELEASE}/lib -type f -name '*.ml' -delete
+tar cvfz ${RELEASE}.tar.gz ${RELEASE}
+
+echo
+echo "RELEASED PACKAGE to `pwd`/${RELEASE}.tar.gz"

NSym/scripts/stage_ocaml_elf_loader.sh

@@ -0,0 +1,36 @@
+#!/bin/bash
+
+PKG=OCamlElfLoader
+PKG_NAME=elf_loader
+ARCH=Linux_x86_64
+
+DATE=`date +%F`
+LIB_PATH=/root/.opam/4.14.0/lib
+
+CUR_PATH=`pwd`
+SRC_PATH=/root/${PKG}
+cd ${SRC_PATH}
+git config --global --add safe.directory ${SRC_PATH}
+COMMIT_HASH=`git rev-parse --short HEAD`
+dune build -p ${PKG_NAME} @install
+dune install ${PKG_NAME}
+
+echo $DATE
+echo $COMMIT_HASH
+
+RELEASE=${PKG_NAME}-${DATE}-${COMMIT_HASH}-${ARCH}
+TARGET=tmp/${RELEASE}
+
+echo ${RELEASE}
+
+cd ${CUR_PATH}
+rm -rf ./tmp
+mkdir -p ${TARGET}/lib
+cp -r ${LIB_PATH}/${PKG_NAME} ${TARGET}/lib/
+
+cd tmp
+find ${RELEASE}/lib -type f -name '*.ml' -delete
+tar cvfz ${RELEASE}.tar.gz ${RELEASE}
+
+echo
+echo "RELEASED PACKAGE to `pwd`/${RELEASE}.tar.gz"

NSym/scripts/stage_ocaml_smt_interface.sh

@@ -0,0 +1,36 @@
+#!/bin/bash
+
+PKG=OCaml-SMT-Interface
+PKG_NAME=ocaml_smt_interface
+ARCH=Linux_x86_64
+
+DATE=`date +%F`
+LIB_PATH=/root/.opam/4.14.0/lib
+
+CUR_PATH=`pwd`
+SRC_PATH=/root/${PKG}
+cd ${SRC_PATH}
+git config --global --add safe.directory ${SRC_PATH}
+COMMIT_HASH=`git rev-parse --short HEAD`
+dune build -p ${PKG_NAME} @install
+dune install ${PKG_NAME}
+
+echo $DATE
+echo $COMMIT_HASH
+
+RELEASE=${PKG_NAME}-${DATE}-${COMMIT_HASH}-${ARCH}
+TARGET=tmp/${RELEASE}
+
+echo ${RELEASE}
+
+cd ${CUR_PATH}
+rm -rf ./tmp
+mkdir -p ${TARGET}/lib
+cp -r ${LIB_PATH}/${PKG_NAME} ${TARGET}/lib/
+
+cd tmp
+find ${RELEASE}/lib -type f -name '*.ml' -delete
+tar cvfz ${RELEASE}.tar.gz ${RELEASE}
+
+echo
+echo "RELEASED PACKAGE to `pwd`/${RELEASE}.tar.gz"