Feat: add tag-std and cargo-tag-std demo by driving rustc #1

zjp-CN · 2025-05-08T14:03:13Z

********* "demo" [Rlib] has reached 10 instances *********
(stable mir) "test" ("src/lib.rs:8:1: 8:21") => "#[tag_std::unreachable]\n"

(stable mir) "MyStruct::get" ("src/lib.rs:27:5: 27:42") => "#[tag_std::contract(!Null(self.ptr) && Align(self.ptr, u8) &&\nAllocated(self.ptr, u8, self.len, *) && Init(self.ptr, u8, self.len, *) &&\nValidInt(self.len*sizeof(u8), [0,isize::MAX]) && Alias(self.ptr, *))]\n"

********* "demo" [Executable] has reached 18 instances *********
(internal api) "demo::MyStruct::get" ("/home/zjp/rust/tag-std/demo/rustc_driver/tests/basic/src/lib.rs:27:5: 27:42") => "#[tag_std::contract(!Null(self.ptr) && Align(self.ptr, u8) &&\nAllocated(self.ptr, u8, self.len, *) && Init(self.ptr, u8, self.len, *) &&\nValidInt(self.len*sizeof(u8), [0,isize::MAX]) && Alias(self.ptr, *))]\n"

+ tag_std=/home/zjp/rust/tag-std/demo/rustc_driver/target/debug/tag-std + cd ./tests/basic + /home/zjp/rust/tag-std/demo/rustc_driver/target/debug/tag-std src/lib.rs --crate-type=lib ["test"] "#[tag_std::unreachable]\n" ["MyStruct::get"] "#[tag_std::contract(!Null(self.ptr) && Align(self.ptr, u8) &&\nAllocated(self.ptr, u8, self.len, *) && Init(sel f.ptr, u8, self.len, *) &&\nValidInt(self.len*sizeof(u8), [0,isize::MAX]) && Alias(self.ptr, *))]\n"

rustc_driver/tests/basic $ tag-std src/main.rs --extern demo -L target/debug/ (body) "main" (body) "std::vec::Vec::<u8>::new" (body) "std::vec::Vec::<u8>::into_raw_parts" (body) "core::fmt::rt::Argument::<'_>::new_debug::<&mut [u8]>" (body) "<&mut [u8] as std::fmt::Debug>::fmt" (body) "<[u8] as std::fmt::Debug>::fmt" (body) "std::fmt::DebugList::<'_, '_>::entries::<&u8, std::slice::Iter<'_, u8>>" (body) "<std::slice::Iter<'_, u8> as std::iter::IntoIterator>::into_iter" (body) "<std::slice::Iter<'_, u8> as std::iter::Iterator>::next" (body) "core::num::<impl usize>::unchecked_sub::precondition_check" (body) "core::fmt::rt::<impl std::fmt::Arguments<'_>>::new_v1::<2, 1>" [src/main.rs:47:5] reachability.instances.len() = 18 [src/main.rs:47:5] reachability.cross_crates = false (error) demo::MyStruct::from not converted to be an item: Error("Item kind `Item` cannot be converted") (error) core::panicking::panic_nounwind not converted to be an item: Error("Item kind `Item` cannot be converted") (error) std::io::_print not converted to be an item: Error("Item kind `Item` cannot be converted") (error) std::fmt::DebugList::<'_, '_>::finish not converted to be an item: Error("Item kind `Item` cannot be converted") (error) demo::MyStruct::get not converted to be an item: Error("Item kind `Item` cannot be converted") (error) std::fmt::DebugList::<'_, '_>::entry not converted to be an item: Error("Item kind `Item` cannot be converted") (error) std::fmt::Formatter::<'_>::debug_list not converted to be an item: Error("Item kind `Item` cannot be converted")

…port + /home/zjp/rust/tag-std/demo/rustc_driver/target/debug/cargo_tag_std Compiling demo v0.1.0 (/home/zjp/rust/tag-std/demo/rustc_driver/tests/basic) [src/main.rs:53:5] reachability.instances.len() = 10 (stable mir) "test" ("src/lib.rs:8:1: 8:21") => "#[tag_std::unreachable]\n" (stable mir) "MyStruct::get" ("src/lib.rs:27:5: 27:42") => "#[tag_std::contract(!Null(self.ptr) && Align(self.ptr, u8) &&\nAllocated(self.ptr, u8, self.len, *) && Init(self.ptr, u8, self.len, *) &&\nValidInt(self.len*sizeof(u8), [0,isize::MAX]) && Alias(self.ptr, *))]\n" [src/main.rs:53:5] reachability.instances.len() = 18 (internal api) "demo::MyStruct::get" ("/home/zjp/rust/tag-std/demo/rustc_driver/tests/basic/src/lib.rs:27:5: 27:42") => "#[tag_std::contract(! Null(self.ptr) && Align(self.ptr, u8) &&\nAllocated(self.ptr, u8, self.len, *) && Init(self.ptr, u8, self.len, *) &&\nValidInt(self.len*sizeof (u8), [0,isize::MAX]) && Alias(self.ptr, *))]\n" Finished `dev` profile [unoptimized + debuginfo] target(s) in 1.75s

zjp-CN added 4 commits May 8, 2025 17:26

rename cargo_tag_std to cargo-tag-std; fix wrapper detection

a7d1aa1

zjp-CN force-pushed the rustc_driver branch 3 times, most recently from 18deb0f to f8e51a7 Compare May 8, 2025 14:10

print local crate name and type; and minor cleanups

9be540e

zjp-CN force-pushed the rustc_driver branch from f8e51a7 to 9be540e Compare May 8, 2025 14:11

zjp-CN mentioned this pull request May 8, 2025

Instances from dependency crates are unable to be converted to CrateItem rust-lang/project-stable-mir#99

Open

hxuhack merged commit 3e72745 into Artisan-Lab:main May 9, 2025

This was referenced May 17, 2025

Attribute syntax #2

Open

Support safety attributes in Rust for Linux #3

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Feat: add tag-std and cargo-tag-std demo by driving rustc #1

Feat: add tag-std and cargo-tag-std demo by driving rustc #1

Uh oh!

zjp-CN commented May 8, 2025

Uh oh!

Uh oh!

Feat: add tag-std and cargo-tag-std demo by driving rustc #1

Feat: add tag-std and cargo-tag-std demo by driving rustc #1

Uh oh!

Conversation

zjp-CN commented May 8, 2025

Uh oh!

Uh oh!