search

project-oak / rust-verification-tools

RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.
https://project-oak.github.io/rust-verification-tools/
Apache License 2.0
273 stars 37 forks source link

AArch64 Docker build error #141

Open chadbrewbaker opened 3 years ago

chadbrewbaker commented 3 years ago

Docker version 20.10.6, build 370c289 macOS 11.4 aarch64 on commit e58c6a54f2.

=> ERROR importing cache manifest from rvt_base:latest

I had to delete this line from docker/mkimage:

--cache-from="${DOCKER_IMAGE_NAME}:${DOCKER_VERSION}" \

This cache doesn't exist on the first build?

chadbrewbaker commented 3 years ago

Another error on commit 46fd9f1ab883b.

macOS 11.4, aarch64, Docker version 20.10.6, build 370c289


docker/build
To build LLVM11 version, use env LLVM11=yes docker/build
Making docker image rvt_base:latest using Dockerfile
../mkimage: line 20: [: -v: unary operator expected
[+] Building 0.6s (3/3) FINISHED                                                                                                                 
 => [internal] load build definition from Dockerfile                                                                                        0.0s
 => => transferring dockerfile: 1.88kB                                                                                                      0.0s
 => [internal] load .dockerignore                                                                                                           0.0s
 => => transferring context: 2B                                                                                                             0.0s
 => ERROR [internal] load metadata for docker.io/library/ubuntu:20.04                                                                       0.5s
------
 > [internal] load metadata for docker.io/library/ubuntu:20.04:
------
failed to solve with frontend dockerfile.v0: failed to create LLB definition: rpc error: code = Unknown desc = open /Users/USERNAME/.docker/.token_seed: permission denied
chadbrewbaker commented 3 years ago

Ran sudo docker/build, now getting this error that it is unable to find many packages.


 => ERROR [2/3] RUN apt-get --yes update   && apt-get install --no-install-recommends --yes   bison   build-essential   clang-10   clang-format-10   c  8.7s
------                                                                                                                                                       
 > importing cache manifest from rvt_base:latest:                                                                                                            
------                                                                                                                                                       
------                                                                                                                                                       
 > [2/3] RUN apt-get --yes update   && apt-get install --no-install-recommends --yes   bison   build-essential   clang-10   clang-format-10   clang-tools-10   clang-11   clang-format-11   clang-tools-11   gcc-multilib   g++-7-multilib   cmake   curl   doxygen   expect   flex   git   libboost-all-dev   libcap-dev   libffi-dev   libgoogle-perftools-dev   libncurses5-dev   libsqlite3-dev   libssl-dev   libtcmalloc-minimal4   lib32stdc++-7-dev   libgmp-dev   libgmpxx4ldbl   lld-10   lld-11   llvm-10   llvm-10-dev   llvm-11   llvm-11-dev   ncurses-doc   ninja-build   perl   pkg-config   python   python3   python3-minimal   python3-pip   subversion   sudo   unzip   wget   && apt-get clean   && pip3 install --no-cache-dir setuptools   && pip3 install --no-cache-dir     argparse     colored     lit     pyyaml     tabulate     termcolor     toml     wllvm:
#6 0.419 Get:1 http://ports.ubuntu.com/ubuntu-ports focal InRelease [265 kB]
#6 1.035 Get:2 http://ports.ubuntu.com/ubuntu-ports focal-updates InRelease [114 kB]
#6 1.135 Get:3 http://ports.ubuntu.com/ubuntu-ports focal-backports InRelease [101 kB]
#6 1.260 Get:4 http://ports.ubuntu.com/ubuntu-ports focal-security InRelease [114 kB]
#6 1.465 Get:5 http://ports.ubuntu.com/ubuntu-ports focal/restricted arm64 Packages [1317 B]
#6 1.473 Get:6 http://ports.ubuntu.com/ubuntu-ports focal/multiverse arm64 Packages [139 kB]
#6 1.480 Get:7 http://ports.ubuntu.com/ubuntu-ports focal/main arm64 Packages [1234 kB]
#6 2.020 Get:8 http://ports.ubuntu.com/ubuntu-ports focal/universe arm64 Packages [11.1 MB]
#6 6.737 Get:9 http://ports.ubuntu.com/ubuntu-ports focal-updates/main arm64 Packages [988 kB]
#6 7.171 Get:10 http://ports.ubuntu.com/ubuntu-ports focal-updates/restricted arm64 Packages [2893 B]
#6 7.171 Get:11 http://ports.ubuntu.com/ubuntu-ports focal-updates/universe arm64 Packages [912 kB]
#6 7.501 Get:12 http://ports.ubuntu.com/ubuntu-ports focal-updates/multiverse arm64 Packages [5147 B]
#6 7.502 Get:13 http://ports.ubuntu.com/ubuntu-ports focal-backports/universe arm64 Packages [4304 B]
#6 7.503 Get:14 http://ports.ubuntu.com/ubuntu-ports focal-security/restricted arm64 Packages [2649 B]
#6 7.505 Get:15 http://ports.ubuntu.com/ubuntu-ports focal-security/universe arm64 Packages [666 kB]
#6 7.656 Get:16 http://ports.ubuntu.com/ubuntu-ports focal-security/multiverse arm64 Packages [2378 B]
#6 7.657 Get:17 http://ports.ubuntu.com/ubuntu-ports focal-security/main arm64 Packages [586 kB]
#6 7.879 Fetched 16.3 MB in 8s (2114 kB/s)
#6 7.879 Reading package lists...
#6 8.245 Reading package lists...
#6 8.580 Building dependency tree...
#6 8.648 Reading state information...
#6 8.679 Package gcc-multilib is not available, but is referred to by another package.
#6 8.679 This may mean that the package is missing, has been obsoleted, or
#6 8.679 is only available from another source
#6 8.679 
#6 8.715 E: Package 'gcc-multilib' has no installation candidate
#6 8.715 E: Unable to locate package g++-7-multilib
#6 8.715 E: Couldn't find any package by regex 'g++-7-multilib'
#6 8.715 E: Unable to locate package lib32stdc++-7-dev
#6 8.715 E: Couldn't find any package by regex 'lib32stdc++-7-dev'
------
executor failed running [/bin/sh -c apt-get --yes update   && apt-get install --no-install-recommends --yes   bison   build-essential   clang-10   clang-format-10   clang-tools-10   clang-11   clang-format-11   clang-tools-11   gcc-multilib   g++-7-multilib   cmake   curl   doxygen   expect   flex   git   libboost-all-dev   libcap-dev   libffi-dev   libgoogle-perftools-dev   libncurses5-dev   libsqlite3-dev   libssl-dev   libtcmalloc-minimal4   lib32stdc++-7-dev   libgmp-dev   libgmpxx4ldbl   lld-10   lld-11   llvm-10   llvm-10-dev   llvm-11   llvm-11-dev   ncurses-doc   ninja-build   perl   pkg-config   python   python3   python3-minimal   python3-pip   subversion   sudo   unzip   wget   && apt-get clean   && pip3 install --no-cache-dir setuptools   && pip3 install --no-cache-dir     argparse     colored     lit     pyyaml     tabulate     termcolor     toml     wllvm]: exit code: 100'''
chadbrewbaker commented 3 years ago

z3 isn't releasing an aarch64 Ubuntu build. This will have to be built from source pinned to whatever commit hash is recommended.

Next error, there is no prebuilt config for aarch64 on klee-uclibc:


 => ERROR [8/8] RUN sh build_klee                                                                                                                      12.3s
------                                                                                                                                                       
 > importing cache manifest from rvt_klee:latest:                                                                                                            
------                                                                                                                                                       
------                                                                                                                                                       
 > [8/8] RUN sh build_klee:                                                                                                                                  
#13 0.164 Cloning into 'klee-uclibc'...                                                                                                                      
#13 12.12 Note: switching to 'klee_uclibc_v1.2'.
#13 12.12 
#13 12.12 You are in 'detached HEAD' state. You can look around, make experimental
#13 12.12 changes and commit them, and you can discard any commits you make in this
#13 12.12 state without impacting any branches by switching back to a branch.
#13 12.12 
#13 12.12 If you want to create a new branch to retain commits you create, you may
#13 12.12 do so (now or later) by using -c with the switch command. Example:
#13 12.12 
#13 12.12   git switch -c <new-branch-name>
#13 12.12 
#13 12.12 Or undo this operation with:
#13 12.12 
#13 12.12   git switch -
#13 12.12 
#13 12.12 Turn off this advice by setting config variable advice.detachedHead to false
#13 12.12 
#13 12.12 HEAD is now at 8ccd74cf6 Merge pull request #25 from MartinNowack/fix_32bit_detection
#13 12.15 INFO:Forcing C compiler to be.../usr/bin/clang-10
#13 12.15 INFO:Absolute path to compiler.../usr/bin/clang-10
#13 12.15 INFO:Disabling assertions
#13 12.15 INFO:Configuring for Debug build
#13 12.15 INFO:Configuring for LLVM bitcode archive
#13 12.15 INFO:Using llvm-config at.../usr/bin/llvm-config-10
#13 12.18 INFO:Using llvm tool dir.../usr/lib/llvm-10/bin
#13 12.18 INFO:Found "/usr/lib/llvm-10/bin/llvm-objdump".
#13 12.18 INFO:Found "/usr/lib/llvm-10/bin/llvm-link".
#13 12.18 INFO:Found "/usr/lib/llvm-10/bin/llvm-ar".
#13 12.18 INFO:Found "/usr/lib/llvm-10/bin/llvm-nm".
#13 12.18 INFO:Testing LLVM Bitcode compiler.../usr/bin/clang-10
#13 12.24 INFO:Compiler /usr/bin/clang-10 works
#13 12.24 INFO:Using LLVM Bitcode Compiler.../usr/bin/clang-10
#13 12.24 INFO:Checking for ncurses...
#13 12.29 INFO:Writing templated file to "/home/root/klee-uclibc/Makefile.klee"
#13 12.29 INFO:Setting up pre-made configure for...aarch64
#13 12.29 ERROR:"/home/root/klee-uclibc/klee-premade-configs/aarch64" does not exist. Cannot install pre-made .config file
------
executor failed running [/bin/sh -c sh build_klee]: exit code: 1
alastairreid commented 3 years ago

Thanks for the report.

It looks like the first issue is due to Ubuntu having a slightly different set of packages (or names for packages??) on Arm than on x86. Probably not too hard to fix.

The second issue seems to be about KLEE and KLEE-uclibc supporting Arm. A quick search on their github page suggests that there have been no discussions of AArch64 or Arm so it doesn't seem to be on their radar. You could perhaps try the KLEE project's own docker images https://klee.github.io/docker/ and https://hub.docker.com/r/klee/klee/ in case they work. (If those do work, then I can try to figure out what they do different; if not, probably best reporting on the KLEE issue tracker)

[Incidentally... In case you are wondering why don't just use KLEE's docker images directly? When we first started using KLEE, this was not possible. After the recent simplification of our own docker images, I think that we are very close to being able to use the KLEE docker images. I suspect that we will switch to using their images sometime in the future.]