From bec5fd1a2298f7f455c559ddfc938fd7a24e9b4d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 9 Aug 2024 16:37:57 +0200
Subject: [PATCH] Update CBMC build instructions for Amazon Linux 2 (#3431)

The default compiler on Amazon Linux 2 is GCC 7, which is not
sufficiently recent for building CBMC v6+. Install and use GCC 10,
adjust warnings to cope with the flex version provided by Amazon Linux
2, and handle the non-default std::filesystem support. Furthermore,
apply a workaround until https://github.com/diffblue/cbmc/issues/8357
has been fixed on the CBMC side.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 scripts/setup/al2/install_cbmc.sh | 79 +++++++++++++++++++++++++++++--
 scripts/setup/al2/install_deps.sh |  1 +
 2 files changed, 77 insertions(+), 3 deletions(-)

diff --git a/scripts/setup/al2/install_cbmc.sh b/scripts/setup/al2/install_cbmc.sh
index 34abcc52db93..de4b5215e083 100755
--- a/scripts/setup/al2/install_cbmc.sh
+++ b/scripts/setup/al2/install_cbmc.sh
@@ -21,10 +21,83 @@ git clone \
 
 pushd "${WORK_DIR}"
 
-mkdir build
-git submodule update --init
+# apply workaround for https://github.com/diffblue/cbmc/issues/8357 until it is
+# properly fixed in CBMC
+cat > varargs.patch << "EOF"
+--- a/src/ansi-c/library/stdio.c
++++ b/src/ansi-c/library/stdio.c
+@@ -1135,7 +1135,7 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
 
-cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
+-        __CPROVER_OBJECT_SIZE(arg))
++        __CPROVER_OBJECT_SIZE(*(void **)&arg))
+   {
+     void *a = va_arg(arg, void *);
+     __CPROVER_havoc_object(a);
+@@ -1233,7 +1233,7 @@ int __stdio_common_vfscanf(
+
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
+-        __CPROVER_OBJECT_SIZE(args))
++        __CPROVER_OBJECT_SIZE(*(void **)&args))
+   {
+     void *a = va_arg(args, void *);
+     __CPROVER_havoc_object(a);
+@@ -1312,7 +1312,7 @@ __CPROVER_HIDE:;
+   (void)*s;
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
+-        __CPROVER_OBJECT_SIZE(arg))
++        __CPROVER_OBJECT_SIZE(*(void **)&arg))
+   {
+     void *a = va_arg(arg, void *);
+     __CPROVER_havoc_object(a);
+@@ -1388,7 +1388,7 @@ int __stdio_common_vsscanf(
+   (void)*s;
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
+-        __CPROVER_OBJECT_SIZE(args))
++        __CPROVER_OBJECT_SIZE(*(void **)&args))
+   {
+     void *a = va_arg(args, void *);
+     __CPROVER_havoc_object(a);
+@@ -1774,12 +1774,12 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
+   (void)*fmt;
+
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
+-        __CPROVER_OBJECT_SIZE(ap))
++        __CPROVER_OBJECT_SIZE(*(void **)&ap))
+
+   {
+     (void)va_arg(ap, int);
+     __CPROVER_precondition(
+-      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
++      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap),
+       "vsnprintf object overlap");
+   }
+
+@@ -1822,12 +1822,12 @@ int __builtin___vsnprintf_chk(
+   (void)*fmt;
+
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
+-        __CPROVER_OBJECT_SIZE(ap))
++        __CPROVER_OBJECT_SIZE(*(void **)&ap))
+
+   {
+     (void)va_arg(ap, int);
+     __CPROVER_precondition(
+-      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
++      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap),
+       "vsnprintf object overlap");
+   }
+
+EOF
+
+cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" \
+  -DCMAKE_C_COMPILER=gcc10-cc -DCMAKE_CXX_COMPILER=gcc10-c++ \
+  -DCMAKE_CXX_STANDARD_LIBRARIES=-lstdc++fs \
+  -DCMAKE_CXX_FLAGS=-Wno-error=register
 cmake3 --build build -- -j$(nproc)
 sudo make -C build install
 
diff --git a/scripts/setup/al2/install_deps.sh b/scripts/setup/al2/install_deps.sh
index 0010aa58bab4..ce901ab8afa5 100755
--- a/scripts/setup/al2/install_deps.sh
+++ b/scripts/setup/al2/install_deps.sh
@@ -11,6 +11,7 @@ set -eu
 DEPS=(
   cmake
   cmake3
+  gcc10-c++
   git
   openssl-devel
   python3-pip