Merge pull request #110 from os-checker/data-hash-split-json

Feat: Generate `hash.json` and `split` json folder; bump toolchain to nightly-2025-08-19

Author: zjp-CN

.github/gen_core.json.sh

@@ -4,7 +4,7 @@ set -o pipefail
 
 export WORKSPACE="${WORKSPACE:-$(pwd)}"
 
-export RUST_LOG=off
+export DV_LOG=off
 export OUTPUT_DIR=$WORKSPACE/assets
 export KANI_DIR=$WORKSPACE/kani/target/kani
 export VERIFY_RUST_STD_LIBRARY=$WORKSPACE/verify-rust-std/library
@@ -13,7 +13,7 @@ export VERIFY_RUST_STD_LIBRARY=$WORKSPACE/verify-rust-std/library
 # * update runid after verify-rust-std submodule syncs
 # * update snapshots after runid changes
 rm tmp -rf
-gh run download -D tmp -R model-checking/verify-rust-std 16777123952
+gh run download -D tmp -R model-checking/verify-rust-std 17086909032
 
 ls -alh $VERIFY_RUST_STD_LIBRARY
 

.github/install-kani.sh

@@ -1,20 +1,27 @@
-set -ex
+#!/usr/bin/bash
+set -exo pipefail
 
 # NOTE: verify-rust-std pins its kani commit, and
 # distributed-verification pins another.
 # So this means for verify-rust-std jobs,
 # distributed-verification may be broken to compile.
 git submodule update --init kani
 
+# Temporary patch to https://github.com/model-checking/kani/pull/4312
+cp .github/kani_contract_mode.patch kani
+
 # Install kani
 pushd kani
 git submodule update --init charon
 
+# Apply the patch
+git apply kani_contract_mode.patch
+
 ./scripts/setup/ubuntu/install_deps.sh
 cargo build-dev -- --release
 
 export PATH=$(pwd)/scripts:$PATH
-echo PATH=$PATH >>$GITHUB_ENV
+echo PATH="$PATH" >>"$GITHUB_ENV"
 kani --version
 
 popd

.github/kani_contract_mode.patch

@@ -0,0 +1,13 @@
+diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+index ed8bde7f8..d8f2eae87 100644
+--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
++++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+@@ -71,7 +71,7 @@ const fn kani_register_contract<T, F: FnOnce() -> T>(f: F) -> T {
+                 }
+                 // Dummy function that we replace to pick the contract mode.
+                 // By default, return ORIGINAL
+-                #[inline(never)]
++                #[inline]
+                 #[kanitool::fn_marker = "kani_contract_mode"]
+                 const fn kani_contract_mode() -> kani::internal::Mode {
+                     kani::internal::ORIGINAL

.github/workflows/test.yml

@@ -54,7 +54,7 @@ jobs:
         autoharness: ["", "-autoharness"]
     if: true
     env:
-      UNSTABLE_ARGS: -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts
+      UNSTABLE_ARGS: -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z stubbing
       AUTO: ${{ matrix.autoharness }}
     steps:
       - name: Remove unnecessary software to free up disk space

.gitignore

@@ -13,5 +13,6 @@ core.json
 *.sqlite3
 *.db
 *.diff
+*.log
 
 tmp/

Cargo.lock

@@ -17,13 +17,13 @@ eyre = "0.6"
 color-eyre = "0.6"
 
 # logger
+log = "0.4.27"
 tracing = "0.1"
 tracing-subscriber = { version = "0.3", features = ["env-filter"] }
 tracing-error = "0.2"
 
 # db
 rusqlite = { version = "0.36.0", features = ["bundled", "jiff"] }
-serde_rusqlite = "0.39.1"
 jiff = { version = "0.2", features = ["serde"] }
 
 [dev-dependencies]

Cargo.toml

@@ -0,0 +1,30 @@
+-- sqlite3 ../artifacts/artifact-libcore/core.sqlite3 <hash.sql | jq -s '.' >../ui/verify-rust-std_data/hash.json
+WITH
+  df AS (
+    SELECT
+      file,
+      name,
+      proof_kind,
+      hash
+    FROM
+      db
+    ORDER BY
+      file,
+      name
+  )
+SELECT
+  JSON_PATCH (
+    '{}',
+    JSON_OBJECT (
+      'file',
+      file,
+      'name',
+      name,
+      'proof_kind',
+      proof_kind,
+      'hash',
+      hash
+    )
+  )
+FROM
+  df;

assets/hash.sql

@@ -0,0 +1,35 @@
+#!/usr/bin/bash
+
+set -eou pipefail
+
+# Usage: sqlite.sh db-path sql-path
+# e.g. ./split.sh ../artifacts/artifact-libcore/core.sqlite3 split.sql ../tmp/json
+db=$1
+sql=$2
+base=$3
+
+echo "db=$db, sql=$sql, base=$base"
+
+# Let parallel use bash.
+export PARALLEL_SHELL=$(type -p bash)
+
+run() {
+  PREFIX=/home/runner/work/verify-rust-std/verify-rust-std/library/
+
+  # Read all arguments and JSON from stdin through parallel pipe.
+  while IFS=$'\t' read -r filename hash json; do
+    # $base is unavaible in parallel run, so pass it as env var.
+    json_folder="$BASE/${filename#"$PREFIX"}"
+    json_file="$json_folder/$hash.json"
+    echo "$json_file"
+    mkdir -p "$json_folder"
+    jq 'del(.[] | select(. == []))' <<<"$json" >"$json_file"
+  done
+}
+
+# Let parallel call the function.
+export -f run
+
+sqlite3 -batch "$db" -separator $'\t' <"$sql" |
+  parallel --colsep '\t' --pipe --progress --tagstring '[Job {#}]' \
+    "BASE=$base run"

assets/split.sh

@@ -0,0 +1,33 @@
+SELECT
+  file,
+  hash,
+  JSON_PATCH (
+    '{}',
+    JSON_OBJECT (
+      'file',
+      file,
+      'name',
+      name,
+      'hash',
+      hash,
+      'hash_direct',
+      hash_direct,
+      'inst_kind',
+      inst_kind,
+      'proof_kind',
+      proof_kind,
+      'attrs',
+      JSON (attrs),
+      'src',
+      src,
+      'macro_backtrace',
+      JSON (macro_backtrace),
+      'callees',
+      JSON (callees)
+    )
+  ) AS data
+FROM
+  db
+ORDER BY
+  file,
+  hash;