Attribute syntax

[zjp-CN]

In tool attributes demo:

tag-std/demo/rustc_driver/tests/basic/src/lib.rs

Lines 19 to 24 in 3e72745

	///contract(!Null(self.ptr); Align(self.ptr, u8); Allocated(self.ptr, u8, self.len, *); Init(self.ptr, u8, self.len, *); ValidInt(self.len*sizeof(u8), [0,isize::MAX]); Alias(self.ptr, *);
	#[tag_std::contract(
	!Null(self.ptr) && Align(self.ptr, u8) &&
	Allocated(self.ptr, u8, self.len, *) && Init(self.ptr, u8, self.len, *) &&
	ValidInt(self.len*sizeof(u8), [0,isize::MAX]) && Alias(self.ptr, *)
	)]

the syntax is #[tag_std::contract( a bunch of properities )].

But a possibly nicer syntax is #[safety::requires::property( ... )]:

#![register_tool(safety)]

#[safety::requires::NotNull(self.ptr)]
#[safety::requires::Align(self.ptr, u8)]
#[safety::requires::Allocated(self.ptr, u8, self.len, *)]
#[safety::requires::Init(self.ptr, u8, self.len, *)]
#[safety::requires::ValidInt(self.len*sizeof(u8), 0..=isize::MAX)]
#[safety::hazard::Alias(self.ptr, *)]
unsafe fn foo(&self) { ... }

cc #1

[hxuhack]

Thanks. @zjp-CN. How about the following way?

#[safe::require(InBound(src, T, len))]
#[safe::require(Init(src, T, count))]
#[safe::require(!Overlap(dst, src, T, 1))]
#[safe::require(Align(src, T))]
#[safe::require(Align(dst, T))]
#[safe::hazard(Alias(dst, src))]

Each safety property is started with a safe keyword, followed by a require, hazard, or option property. Since the project does not consider safe APIs, we do not need ensure. See primitive-sp.md for more details.

[hxuhack]

We have specified the attribute syntax in usage.md.

Syntax for annotating unsafe APIs:

#[safety::precond::Align(p, T)]
#[safety::option::Trait(T, Copy)]
#[safety::hazard::Alias(p, 0)]

Syntax for annotating callsites:

#[safety::discharges::Align(p, T)::memo(...)]
#[safety::discharges::Alias(p, 0)::memo(...)]

[hxuhack]

Due to the limitation of the parser, we change the syntax of discharges to the following way:

#[safety::discharges(Align(p, T), memo = "...")]
#[safety::discharges(Alias(p, 0), "..."]