Enable harnesses that were fixed by the unreleased version of CBMC

library/core/src/slice/iter.rs

@@ -3604,18 +3604,24 @@ mod verify {
                 }
 
                 check_unsafe_contracts!(check_next_back_unchecked, $ty, next_back_unchecked());
-                //check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any()));
-                //check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any()));
+                check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any()));
+                check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any()));
 
                 // FIXME: The functions that are commented out are currently failing verification.
                 // Debugging the issue is currently blocked by:
                 // https://github.com/model-checking/kani/issues/3670
                 //
                 // Public functions that call safe abstraction `make_slice`.
-                // check_safe_abstraction!(check_as_slice, $ty, as_slice);
-                // check_safe_abstraction!(check_as_ref, $ty, as_ref);
+                check_safe_abstraction!(check_as_slice, $ty, |iter: &mut Iter<'_, $ty>| {
+                    iter.as_slice();
+                });
+                check_safe_abstraction!(check_as_ref, $ty, |iter: &mut Iter<'_, $ty>| {
+                    iter.as_ref();
+                });
 
-                // check_safe_abstraction!(check_advance_back_by, $ty, advance_back_by, kani::any());
+                check_safe_abstraction!(check_advance_back_by, $ty, |iter: &mut Iter<'_, $ty>| {
+                    iter.advance_back_by(kani::any());
+                });
 
                 check_safe_abstraction!(check_is_empty, $ty, |iter: &mut Iter<'_, $ty>| {
                     let _ = iter.is_empty();
@@ -3626,12 +3632,12 @@ mod verify {
                 check_safe_abstraction!(check_size_hint, $ty, |iter: &mut Iter<'_, $ty>| {
                     let _ = iter.size_hint();
                 });
-                //check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); });
-                //check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); });
+                check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); });
+                check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); });
                 check_safe_abstraction!(check_next_back, $ty, |iter: &mut Iter<'_, $ty>| {
                     let _ = iter.next_back();
                 });
-                //check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); });
+                check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); });
                 check_safe_abstraction!(check_next, $ty, |iter: &mut Iter<'_, $ty>| {
                     let _ = iter.next();
                 });

library/core/src/str/pattern.rs

@@ -2000,10 +2000,6 @@ pub mod verify {
         }
     }
 
-    /* This harness check `small_slice_eq` with dangling pointer to slice
-       with zero size. Kani finds safety issue of `small_slice_eq` in this
-       harness and hence the proof will fail.
-
     #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86
     #[kani::proof]
     #[kani::unwind(4)]
@@ -2022,5 +2018,4 @@ pub mod verify {
             true
         );
     }
-    */
 }

scripts/run-kani.sh

@@ -65,29 +65,30 @@ TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE}
 REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
 BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
 
-# Function to read commit ID from TOML file
+# Function to read kani_commit ID from TOML file
 read_commit_from_toml() {
     local file="$1"
+    local table="$2"
     if [[ ! -f "$file" ]]; then
         echo "Error: TOML file not found: $file" >&2
         exit 1
     fi
-    local commit=$(grep '^commit *=' "$file" | sed 's/^commit *= *"\(.*\)"/\1/')
-    if [[ -z "$commit" ]]; then
-        echo "Error: 'commit' field not found in TOML file" >&2
+    local kani_commit=$(grep -A1 "\[${table}\]" "${file}" | grep 'commit' | cut -d'"' -f2)
+    if [[ -z "$kani_commit" ]]; then
+        echo "Error: 'kani_commit' field in table '${table}' not found in TOML file" >&2
         exit 1
     fi
-    echo "$commit"
+    echo "$kani_commit"
 }
 
 clone_kani_repo() {
     local repo_url="$1"
     local directory="$2"
     local branch="$3"
-    local commit="$4"
+    local kani_commit="$4"
     git clone "$repo_url" "$directory"
     pushd "$directory"
-    git checkout "$commit"
+    git checkout "$kani_commit"
     popd
 }
 
@@ -100,6 +101,39 @@ get_current_commit() {
     fi
 }
 
+# Build the specified CBMC commit and push installation PATH
+#
+# If the directory does not exist, we initialize an empty repository
+# and add the remote so we can do a shallow clone of a specific commit.
+build_cbmc() {
+    local directory="$1"
+    local cbmc_commit="$2"
+    if [ ! -d "${directory}" ]; then
+      mkdir -p "${directory}"
+      pushd "${directory}" > /dev/null
+      git init .
+      git remote add origin https://github.com/diffblue/cbmc
+    else
+      pushd "${directory}" > /dev/null
+    fi
+    git fetch --depth 1 origin "$cbmc_commit"
+    git checkout "$cbmc_commit"
+    if [ ! -d "${directory}/build" ]; then
+      cmake -S . -Bbuild \
+        -DWITH_JBMC=OFF \
+        -Dsat_impl="minisat2;cadical"\
+        -DCMAKE_CXX_STANDARD_LIBRARIES=-lstdc++fs \
+        -DCMAKE_CXX_FLAGS=-Wno-error=register \
+        -DCMAKE_INSTALL_PREFIX=./install
+    fi
+    cmake --build build -- -j$(nproc)
+    make -C build install
+    export PATH="${directory}/install/bin:${PATH}"
+    version=$(cbmc --version)
+    echo "Finished building CBMC ${version}"
+    popd > /dev/null
+}
+
 build_kani() {
     local directory="$1"
     pushd "$directory"
@@ -152,28 +186,31 @@ main() {
     echo "Using TOML file: $TOML_FILE"
     echo "Using repository URL: $REPO_URL"
 
-    # Read commit ID from TOML file
-    commit=$(read_commit_from_toml "$TOML_FILE")
+    # Read kani_commit ID from TOML file
+    kani_commit=$(read_commit_from_toml "$TOML_FILE" "kani")
+    cbmc_commit=$(read_commit_from_toml "$TOML_FILE" "cbmc")
 
     # Check if binary already exists and is up to date
-    if check_binary_exists "$build_dir" "$commit"; then
+    if check_binary_exists "$build_dir" "$kani_commit"; then
         echo "Kani binary is up to date. Skipping build."
     else
-        echo "Building Kani from commit: $commit"
+        echo "Building Kani from kani_commit: $kani_commit"
 
         # Remove old build directory if it exists
         rm -rf "$build_dir"
         mkdir -p "$build_dir"
 
-        # Clone repository and checkout specific commit
-        clone_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
+        # Clone repository and checkout specific kani_commit
+        clone_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$kani_commit"
 
         # Build project
         build_kani "$build_dir"
 
         echo "Kani build completed successfully!"
     fi
 
+    build_cbmc "${build_dir}/cbmc" "$cbmc_commit"
+
     # Get the path to the Kani executable
     kani_path=$(get_kani_path "$build_dir")
     echo "Kani executable path: $kani_path"

tool_config/kani-version.toml

@@ -3,3 +3,7 @@
 
 [kani]
 commit = "8400296f5280be4f99820129bc66447e8dff63f4"
+
+# Temporarily track CBMC version with spurious CEX fix
+[cbmc]
+commit = "83f61a4127f9b2f8fcd45993dfe9a9fbecc362e1"