feat: embed and check githash in .olean

.github/workflows/ci.yml

@@ -248,7 +248,7 @@ jobs:
           mkdir build
           cd build
           ulimit -c unlimited # coredumps
-          OPTIONS=()
+          OPTIONS=(-DUSE_GITHASH=ON)  # this also enables githash embedding into .olean headers
           if [[ -n '${{ matrix.prepare-llvm }}' ]]; then
             wget -q ${{ matrix.llvm-url }}
             PREPARE="$(${{ matrix.prepare-llvm }})"

CMakeLists.txt

@@ -11,7 +11,7 @@ foreach(var ${vars})
     list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
   elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
-    if("${var}" STREQUAL "USE_GMP")
+    if("${var}" MATCHES "USE_GMP|USE_GITHASH")
       # must forward options that generate incompatible .olean format
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
@@ -34,8 +34,7 @@ ExternalProject_add(stage0
   SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
   SOURCE_SUBDIR src
   BINARY_DIR stage0
-  # do not rebuild stage0 when git hash changes; it's not from this commit anyway
-  CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
+  CMAKE_ARGS -DSTAGE=0 ${PLATFORM_ARGS} ${STAGE0_ARGS}
   BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
   INSTALL_COMMAND ""  # skip install
   DEPENDS ${EXTRA_DEPENDS}

src/CMakeLists.txt

@@ -37,7 +37,7 @@ option(SPLIT_STACK        "SPLIT_STACK"        OFF)
 option(LLVM               "LLVM"               OFF)
 
 # When ON we include githash in the version string
-option(USE_GITHASH        "GIT_HASH"           ON)
+option(USE_GITHASH        "GIT_HASH"           OFF)
 # When ON we install LICENSE files to CMAKE_INSTALL_PREFIX
 option(INSTALL_LICENSE "INSTALL_LICENSE" ON)
 # When ON thread storage is automatically finalized, it assumes platform support pthreads.

src/library/module.cpp

@@ -3,6 +3,15 @@ Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
+
+.olean serialization and deserialization.
+
+File format:
+
+16 bytes: the string "oleanfile!!!!!!!"
+32 bytes: `LEAN_GITHASH` (empty for non-releases), padded with '0' to the right
+1 word: the base address
+remainder: binary data
 */
 #include <unordered_map>
 #include <vector>
@@ -25,6 +34,7 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
 #include "library/constants.h"
 #include "library/time_task.h"
 #include "library/util.h"
+#include "githash.h"
 
 #ifdef LEAN_WINDOWS
 #include <windows.h>
@@ -43,6 +53,8 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
 namespace lean {
 // manually padded to multiple of word size, see `initialize_module`
 static char const * g_olean_header   = "oleanfile!!!!!!!";
+static size_t const g_githash_header_size = 32;
+
 
 extern "C" LEAN_EXPORT object * lean_save_module_data(b_obj_arg fname, b_obj_arg mod, b_obj_arg mdata, object *) {
     std::string olean_fn(string_cstr(fname));
@@ -73,9 +85,13 @@ extern "C" LEAN_EXPORT object * lean_save_module_data(b_obj_arg fname, b_obj_arg
         // `MapViewOfFileEx` addresses must be aligned to the "memory allocation granularity", which is 64KB.
         base_addr = base_addr & ~((1LL<<16) - 1);
 
-        object_compactor compactor(reinterpret_cast<void *>(base_addr + strlen(g_olean_header) + sizeof(base_addr)));
+        object_compactor compactor(reinterpret_cast<void *>(base_addr + strlen(g_olean_header) + g_githash_header_size + sizeof(base_addr)));
         compactor(mdata);
         out.write(g_olean_header, strlen(g_olean_header));
+        out.write(LEAN_GITHASH, std::min(g_githash_header_size, strlen(LEAN_GITHASH)));
+        if (g_githash_header_size > strlen(LEAN_GITHASH)) {
+            out << std::string(g_githash_header_size - strlen(LEAN_GITHASH), '0');
+        }
         out.write(reinterpret_cast<char *>(&base_addr), sizeof(base_addr));
         out.write(static_cast<char const *>(compactor.data()), compactor.size());
         out.close();
@@ -116,13 +132,14 @@ extern "C" LEAN_EXPORT object * lean_read_module_data(object * fname, object *)
         in.seekg(0, in.end);
         size_t size = in.tellg();
         in.seekg(0);
-        size_t header_size = strlen(g_olean_header);
+        size_t header_size = strlen(g_olean_header) + g_githash_header_size;
         if (size < header_size) {
             return io_result_mk_error((sstream() << "failed to read file '" << olean_fn << "', invalid header").str());
         }
         char * header = new char[header_size];
         in.read(header, header_size);
-        if (strncmp(header, g_olean_header, header_size) != 0) {
+        if (memcmp(header, g_olean_header, strlen(g_olean_header)) != 0 ||
+            memcmp(header + strlen(g_olean_header), LEAN_GITHASH, std::min(g_githash_header_size, strlen(LEAN_GITHASH))) != 0) {
             return io_result_mk_error((sstream() << "failed to read file '" << olean_fn << "', invalid header").str());
         }
         delete[] header;