Merge branch 'main' into users

.github/workflows/proof_ci_resources/config.yaml

@@ -1,8 +1,8 @@
 # Use exact versions (instead of "latest") so we're not broken by surprise upgrades.
-cadical-tag: "rel-2.0.0" # tag of latest release: https://github.com/arminbiere/cadical/releases
-cbmc-version: "6.2.0" # semver of latest release: https://github.com/diffblue/cbmc/releases
-cbmc-viewer-version: "3.9" # semver of latest release: https://github.com/model-checking/cbmc-viewer/releases
-kissat-tag: "rel-4.0.0" # tag of latest release: https://github.com/arminbiere/kissat/releases
+cadical-tag: "rel-2.1.0" # tag of latest release: https://github.com/arminbiere/cadical/releases
+cbmc-version: "6.4.0" # semver of latest release: https://github.com/diffblue/cbmc/releases
+cbmc-viewer-version: "3.10" # semver of latest release: https://github.com/model-checking/cbmc-viewer/releases
+kissat-tag: "rel-4.0.1" # tag of latest release: https://github.com/arminbiere/kissat/releases
 litani-version: "1.29.0" # semver of latest release: https://github.com/awslabs/aws-build-accumulator/releases
 proofs-dir: verification/cbmc/proofs
 run-cbmc-proofs-command: ./run-cbmc-proofs.py

cmake/AwsPrebuildDependency.cmake

@@ -13,11 +13,11 @@ function(aws_prebuild_dependency)
     set(multiValueArgs CMAKE_ARGUMENTS)
     cmake_parse_arguments(AWS_PREBUILD "" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})
 
-    if(NOT AWS_PREBUILD_DEPENDENCY_NAME)
+    if (NOT AWS_PREBUILD_DEPENDENCY_NAME)
         message(FATAL_ERROR "Missing DEPENDENCY_NAME argument in prebuild_dependency function")
     endif()
 
-    if(NOT AWS_PREBUILD_SOURCE_DIR)
+    if (NOT AWS_PREBUILD_SOURCE_DIR)
         message(FATAL_ERROR "Missing SOURCE_DIR argument in prebuild_dependency function")
     endif()
 
@@ -29,18 +29,31 @@ function(aws_prebuild_dependency)
     string(REPLACE ";" "\\\\;" ESCAPED_PREFIX_PATH "${CMAKE_PREFIX_PATH}")
     # For execute_process to accept a dynamically constructed command, it should be passed in a list format.
     set(cmakeCommand "${CMAKE_COMMAND}")
+
+    # Get the list of optional and platform-specific variables that may affect build process.
+    set(cmakeOptionalVariables "")
+    aws_get_variables_for_prebuild_dependency(cmakeOptionalVariables)
+    list(APPEND cmakeCommand ${cmakeOptionalVariables})
+
+    # The following variables should always be used.
     list(APPEND cmakeCommand ${AWS_PREBUILD_SOURCE_DIR})
     list(APPEND cmakeCommand -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE})
     list(APPEND cmakeCommand -DCMAKE_PREFIX_PATH=${ESCAPED_PREFIX_PATH})
     list(APPEND cmakeCommand -DCMAKE_INSTALL_PREFIX=${depInstallDir})
     list(APPEND cmakeCommand -DCMAKE_INSTALL_RPATH=${CMAKE_INSTALL_RPATH})
     list(APPEND cmakeCommand -DBUILD_SHARED_LIBS=${BUILD_SHARED_LIBS})
+    # In case a custom generator was provided via -G option. If we don't propagate it, the default value might
+    # conflict with other cmake options (e.g. CMAKE_MAKE_PROGRAM) or no make program could be found at all.
+    if (CMAKE_GENERATOR)
+        list(APPEND cmakeCommand -G${CMAKE_GENERATOR})
+    endif()
 
     # Append provided arguments to CMake command.
-    if(AWS_PREBUILD_CMAKE_ARGUMENTS)
+    if (AWS_PREBUILD_CMAKE_ARGUMENTS)
         list(APPEND cmakeCommand ${AWS_PREBUILD_CMAKE_ARGUMENTS})
     endif()
 
+    message(STATUS "cmake command for dependency ${AWS_PREBUILD_DEPENDENCY_NAME}: ${cmakeCommand}")
     # Configure dependency project.
     execute_process(
         COMMAND ${cmakeCommand}
@@ -65,6 +78,10 @@ function(aws_prebuild_dependency)
     # Make the installation visible for others.
     list(INSERT CMAKE_PREFIX_PATH 0 ${depInstallDir}/)
     set(CMAKE_PREFIX_PATH ${CMAKE_PREFIX_PATH} PARENT_SCOPE)
+    if (CMAKE_CROSSCOMPILING)
+        list(INSERT CMAKE_FIND_ROOT_PATH 0 ${depInstallDir})
+        set(CMAKE_FIND_ROOT_PATH ${CMAKE_FIND_ROOT_PATH} PARENT_SCOPE)
+    endif()
 
     set(${AWS_PREBUILD_DEPENDENCY_NAME}_PREBUILT TRUE CACHE INTERNAL "Indicate that dependency is built and can be used")
 
@@ -75,3 +92,60 @@ function(aws_prebuild_dependency)
         DESTINATION ${CMAKE_INSTALL_PREFIX}
     )
 endfunction()
+
+# Get list of optional or platform-specific variables that may affect build process.
+function(aws_get_variables_for_prebuild_dependency AWS_CMAKE_PREBUILD_ARGS)
+    set(variables "")
+
+    # The CMake variables below were chosen for Linux, BSD, and Android platforms. If you want to use the prebuild logic
+    # on other platforms, the chances are you have to handle additional variables (like CMAKE_OSX_SYSROOT). Refer to
+    # https://cmake.org/cmake/help/latest/manual/cmake-toolchains.7.html to update the list of handled variables, and
+    # then you can enable a new platform here.
+    if ((NOT UNIX) OR APPLE)
+        message(FATAL_ERROR "aws_get_variables_for_prebuild_dependency is called for unsupported platform")
+    endif()
+
+    get_cmake_property(vars CACHE_VARIABLES)
+    foreach(var ${vars})
+        # Variables in this block make sense only in cross-compiling mode. The variable list is created from the CMake
+        # documentation on toolchains: https://cmake.org/cmake/help/latest/manual/cmake-toolchains.7.html
+        # NOTE: Some variables are missed here (e.g. CMAKE_SYSROOT) because they can be set via toolchain file only.
+        if (CMAKE_CROSSCOMPILING AND (
+                var STREQUAL "CMAKE_TOOLCHAIN_FILE"
+                OR var STREQUAL "CMAKE_SYSTEM_NAME"
+                OR var STREQUAL "CMAKE_SYSTEM_VERSION"
+                OR var STREQUAL "CMAKE_SYSTEM_PROCESSOR"
+                # Android-specific variables.
+                OR var MATCHES "^(CMAKE_)?ANDROID_"))
+            # To store a list within another list, it needs to be escaped first.
+            string(REPLACE ";" "\\\\;" escapedVar "${${var}}")
+            if (escapedVar)
+                list(APPEND variables "-D${var}=${escapedVar}")
+            endif()
+        endif()
+
+        # Other optional variables applicable both in cross-compiling and non-cross-compiling modes.
+        # Refer to https://cmake.org/cmake/help/latest/manual/cmake-variables.7.html for each variable description.
+        if (var STREQUAL "CMAKE_C_COMPILER"
+                OR var MATCHES "^CMAKE_C_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?"
+                OR var STREQUAL "CMAKE_CXX_COMPILER"
+                OR var MATCHES "^CMAKE_CXX_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?"
+                OR var STREQUAL "CMAKE_LINKER_TYPE"
+                OR var MATCHES "^CMAKE_EXE_LINKER_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?"
+                OR var MATCHES "^CMAKE_MODULE_LINKER_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?"
+                OR var MATCHES "^CMAKE_STATIC_LINKER_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?"
+                OR var MATCHES "^CMAKE_SHARED_LINKER_FLAGS(_DEBUG|_RELEASE|_RELWITHDEBINFO|_MINSIZEREL)?"
+                OR var STREQUAL "CMAKE_MAKE_PROGRAM"
+                OR var MATCHES "^CMAKE_RUNTIME_OUTPUT_DIRECTORY"
+                OR var MATCHES "^CMAKE_ARCHIVE_OUTPUT_DIRECTORY"
+                OR var MATCHES "^CMAKE_LIBRARY_OUTPUT_DIRECTORY")
+            # To store a list within another list, it needs to be escaped first.
+            string(REPLACE ";" "\\\\;" escapedVar "${${var}}")
+            if (escapedVar)
+                list(APPEND variables "-D${var}=${escapedVar}")
+            endif()
+        endif()
+    endforeach()
+
+    set(${AWS_CMAKE_PREBUILD_ARGS} ${variables} PARENT_SCOPE)
+endfunction()

tests/hash_table_test.c

@@ -991,6 +991,7 @@ static int s_test_hash_table_eq(struct aws_allocator *allocator, void *ctx) {
 struct churn_entry {
     void *key;
     int original_index;
+    int sorted_index;
     void *value;
     int is_removed;
 };
@@ -1026,7 +1027,7 @@ static int s_test_hash_churn_fn(struct aws_allocator *allocator, void *ctx) {
 
     int i = 0;
     struct aws_hash_table hash_table;
-    int nentries = 2 * 512 * 1024;
+    const int nentries = 2 * 512 * 1024;
     int err_code = aws_hash_table_init(&hash_table, allocator, nentries, aws_hash_ptr, aws_ptr_eq, NULL, NULL);
 
     if (AWS_ERROR_SUCCESS != err_code) {
@@ -1035,21 +1036,19 @@ static int s_test_hash_churn_fn(struct aws_allocator *allocator, void *ctx) {
 
     /* Probability that we deliberately try to overwrite.
        Note that random collisions can occur, and are not explicitly avoided. */
-    double pOverwrite = 0.05;
-    double pDelete = 0.05;
+    const double pOverwrite = 0.05;
+    const double pDelete = 0.05;
 
+    /* Create array of "entries" (actions we'll do to the hash table later) */
     struct churn_entry *entries = calloc(sizeof(*entries), nentries);
-    struct churn_entry **permuted = calloc(sizeof(*permuted), nentries);
-
     for (i = 0; i < nentries; i++) {
         struct churn_entry *e = &entries[i];
-        permuted[i] = e;
         e->original_index = i;
 
         int mode = 0; /* 0 = new entry, 1 = overwrite, 2 = delete */
 
         if (i != 0) {
-            double p = (double)rand();
+            double p = ((double)rand()) / RAND_MAX;
             if (p < pOverwrite) {
                 mode = 1;
             } else if (p < pOverwrite + pDelete) {
@@ -1059,53 +1058,94 @@ static int s_test_hash_churn_fn(struct aws_allocator *allocator, void *ctx) {
 
         e->is_removed = 0;
         if (mode == 0) {
+            /* new entry: random key */
             e->key = (void *)(uintptr_t)rand();
             e->value = (void *)(uintptr_t)rand();
         } else if (mode == 1) {
+            /* overwrite entry: use same key as an earlier entry */
             e->key = entries[(size_t)rand() % i].key; /* not evenly distributed but close enough */
             e->value = (void *)(uintptr_t)rand();
         } else if (mode == 2) {
+            /* delete entry: use same key as an earlier entry */
             e->key = entries[(size_t)rand() % i].key; /* not evenly distributed but close enough */
             e->value = 0;
             e->is_removed = 1;
         }
     }
 
-    qsort(permuted, nentries, sizeof(*permuted), s_qsort_churn_entry);
+    /* Create another array with the entries sorted by key (if tied then sort by original index) */
+    struct churn_entry **sorted_entries = calloc(sizeof(*sorted_entries), nentries);
+    for (i = 0; i < nentries; i++) {
+        sorted_entries[i] = &entries[i];
+    }
+    qsort(sorted_entries, nentries, sizeof(*sorted_entries), s_qsort_churn_entry);
+    for (i = 0; i < nentries; i++) {
+        sorted_entries[i]->sorted_index = i;
+    }
 
     long start = s_timestamp();
 
+    /* Iterate over entries, calling aws_hash_table_remove() or aws_hash_table_create().
+     * Consult sorted_entries to check whether an item with that key should already be in the table or not. */
     for (i = 0; i < nentries; i++) {
         if (!(i % 100000)) {
             printf("Put progress: %d/%d\n", i, nentries);
         }
-        struct churn_entry *e = &entries[i];
+        const struct churn_entry *e = &entries[i];
+        int sorted_i = e->sorted_index;
         if (e->is_removed) {
+            /* call aws_hash_table_remove() with this entry's key... */
             int was_present;
             err_code = aws_hash_table_remove(&hash_table, e->key, NULL, &was_present);
             ASSERT_SUCCESS(err_code, "Unexpected failure removing element");
-            if (i != 0 && entries[i - 1].key == e->key && entries[i - 1].is_removed) {
-                ASSERT_INT_EQUALS(0, was_present, "Expected item to be missing");
+
+            if (sorted_i != 0 && sorted_entries[sorted_i - 1]->key == e->key) {
+                /* if an earlier entry had same key... */
+                if (sorted_entries[sorted_i - 1]->is_removed) {
+                    /* earlier entry was ALSO marked for deletion, so item should be missing now */
+                    ASSERT_INT_EQUALS(0, was_present, "Expected item to be missing");
+                } else {
+                    /* earlier entry was inserted, so item should have been present */
+                    ASSERT_INT_EQUALS(1, was_present, "Expected item to be present");
+                }
             } else {
-                ASSERT_INT_EQUALS(1, was_present, "Expected item to be present");
+                /* no earlier entry with same key, so no chance item was already there */
+                ASSERT_INT_EQUALS(0, was_present, "Expected item to be missing");
             }
         } else {
+            /* call aws_hash_table_create() with this entry's key... */
             struct aws_hash_element *pElem;
             int was_created;
             err_code = aws_hash_table_create(&hash_table, e->key, &pElem, &was_created);
             ASSERT_SUCCESS(err_code, "Unexpected failure adding element");
 
+            if (sorted_i != 0 && sorted_entries[sorted_i - 1]->key == e->key) {
+                /* if an earlier entry had same key... */
+                if (sorted_entries[sorted_i - 1]->is_removed) {
+                    /* earlier entry removed this key, so this entry should create a new one */
+                    ASSERT_INT_EQUALS(1, was_created, "Expected new item to be created");
+                } else {
+                    /* earlier entry already added this key */
+                    ASSERT_INT_EQUALS(0, was_created, "Expected item to already be present");
+                }
+            } else {
+                /* no earlier entry with same key, so no chance item was already there */
+                ASSERT_INT_EQUALS(1, was_created, "Expected new item to be created");
+            }
+
             pElem->value = e->value;
         }
     }
 
+    /* Iterate over sorted_entries. For entries with a given key, the last one
+     * reflects what should be in the hash table */
     for (i = 0; i < nentries; i++) {
         if (!(i % 100000)) {
             printf("Check progress: %d/%d\n", i, nentries);
         }
-        struct churn_entry *e = permuted[i];
+        const struct churn_entry *e = sorted_entries[i];
 
-        if (i < nentries - 1 && permuted[i + 1]->key == e->key) {
+        if (i < nentries - 1 && sorted_entries[i + 1]->key == e->key) {
             // overwritten on subsequent step
             continue;
         }
@@ -1126,7 +1166,7 @@ static int s_test_hash_churn_fn(struct aws_allocator *allocator, void *ctx) {
     long end = s_timestamp();
 
     free(entries);
-    free(permuted);
+    free(sorted_entries);
 
     printf("elapsed=%ld us\n", end - start);
     return 0;