Feat: Generate hash.json and split json folder; bump toolchain to nightly-2025-08-19
#110
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
$ verify_rust_std split --db artifacts/artifact-libcore/core.sqlite3 --base tmp/json Error: 0: Invalid column type Null at index: 5, name: proof_kind Location: src/db/split_to_json.rs:38
$ ./split.sh ../artifacts/artifact-libcore/core.sqlite3 split.sql ../tmp/json distributed-verification/tmp/json $ dust -b -r 477M └─┬ . 452M ├─┬ core 452M │ └─┬ src 312M │ ├─┬ num 132M │ │ ├─┬ int_macros.rs 132M │ │ │ └── DbFunctions.json 122M │ │ ├─┬ uint_macros.rs 122M │ │ │ └── DbFunctions.json 35M │ │ └─┬ nonzero.rs 35M │ │ └── DbFunctions.json 19M │ ├─┬ internal_macros.rs 19M │ │ └── DbFunctions.json 18M │ ├─┬ sync 18M │ │ └─┬ atomic.rs 18M │ │ └── DbFunctions.json 16M │ ├── slice 15M │ ├── fmt 13M │ ├─┬ ub_checks.rs 13M │ │ └── DbFunctions.json 11M │ ├─┬ intrinsics 10M │ │ └─┬ mod.rs 10M │ │ └── DbFunctions.json 8.3M │ ├── ptr 7.8M │ └─┬ array 7.4M │ └── mod.rs 17M └─┬ stdarch 17M └─┬ crates 17M └─┬ core_arch 17M └─┬ src 7.9M └─┬ simd.rs 7.9M └── DbFunctions.json
assets $ ./split.sh ../artifacts/artifact-libcore/core.sqlite3 split.sql ../tmp/split distributed-verification/tmp/split $ dust -b -r 559M └─┬ . 511M ├─┬ core 511M │ └─┬ src 323M │ ├─┬ num 134M │ │ ├── int_macros.rs 124M │ │ ├── uint_macros.rs 36M │ │ └── nonzero.rs 27M │ ├── internal_macros.rs 21M │ ├── slice 20M │ ├─┬ sync 20M │ │ └── atomic.rs 19M │ ├── ptr 16M │ ├── fmt 13M │ ├── ub_checks.rs 13M │ ├─┬ intrinsics 13M │ │ └── mod.rs 9.1M │ └── array 32M ├─┬ stdarch 32M │ └─┬ crates 32M │ └─┬ core_arch 32M │ └─┬ src 11M │ ├─┬ arm_shared 11M │ │ └── neon 10M │ └── simd.rs 8.3M └─┬ home 8.3M └─┬ runner 8.3M └─┬ work 8.3M └─┬ distributed-verification 8.3M └─┬ distributed-verification 8.3M └─┬ kani 8.2M └── library
…953) This fixes upstream CI failure. cc model-checking/verify-rust-std#465 cc model-checking/kani#4303
cc model-checking/kani#4295 cc model-checking/verify-rust-std@c090506#diff-8348895dea8741e872b7dd41b86e35d72e0f497c56ff6ed5c42bf5958ba2fe45 error: Using the stub_verified attribute requires activating the unstable `stubbing` feature --> /home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/intrinsics/mod.rs:3583:13 | 3583 | #[kani::stub_verified(transmute_unchecked_wrapper)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ... 3605 | should_succeed_no_validity_reqs!(should_succeed_char_to_i32, char, i32); | ----------------------------------------------------------------------- in this macro invocation | = note: this error originates in the attribute macro `kani::stub_verified` which comes from the expansion of the macro `should_succeed_no_validity_reqs` (in Nightly builds, run with -Z macro-backtrace for more info)
Compiling core v0.0.0 (/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core) error: multiple input filenames provided (first two filenames are `core` and `/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/lib.rs`)
add log file support
zjp-CN
force-pushed
the
data-hash-split-json
branch
from
7845f8f to
2d76f05
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR
hash.jsonandsplitjson folder in verify-rust-std_datasplitJSONs are DbFunction info under split folder; each JSON file is stored asbase_folder/src_file_path/function_hash.jsonhash.jsonhelps to locate it via function namecompiler_builtinscannot call functions through upstream monomorphizations #111kani::modifiescauses an error that compiler_builtins cannot call functions through upstream monomorphizations model-checking/verify-rust-std#477