Skip to content

Commit

Permalink
feat: add a warning when using unsafe blocks without safety comments (#…
Browse files Browse the repository at this point in the history
  • Loading branch information
guipublic authored Dec 20, 2024
1 parent fd816cf commit 5c00a79
Show file tree
Hide file tree
Showing 71 changed files with 294 additions and 63 deletions.
21 changes: 16 additions & 5 deletions compiler/noirc_frontend/src/debug/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -523,7 +523,9 @@ pub fn build_debug_crate_file() -> String {
__debug_var_assign_oracle(var_id, value);
}
pub fn __debug_var_assign<T>(var_id: u32, value: T) {
unsafe {{
unsafe {
//@safety: debug context
{
__debug_var_assign_inner(var_id, value);
}}
}
Expand All @@ -534,7 +536,9 @@ pub fn build_debug_crate_file() -> String {
__debug_var_drop_oracle(var_id);
}
pub fn __debug_var_drop(var_id: u32) {
unsafe {{
unsafe {
//@safety: debug context
{
__debug_var_drop_inner(var_id);
}}
}
Expand All @@ -545,7 +549,9 @@ pub fn build_debug_crate_file() -> String {
__debug_fn_enter_oracle(fn_id);
}
pub fn __debug_fn_enter(fn_id: u32) {
unsafe {{
unsafe {
//@safety: debug context
{
__debug_fn_enter_inner(fn_id);
}}
}
Expand All @@ -556,7 +562,9 @@ pub fn build_debug_crate_file() -> String {
__debug_fn_exit_oracle(fn_id);
}
pub fn __debug_fn_exit(fn_id: u32) {
unsafe {{
unsafe {
//@safety: debug context
{
__debug_fn_exit_inner(fn_id);
}}
}
Expand All @@ -567,7 +575,9 @@ pub fn build_debug_crate_file() -> String {
__debug_dereference_assign_oracle(var_id, value);
}
pub fn __debug_dereference_assign<T>(var_id: u32, value: T) {
unsafe {{
unsafe {
//@safety: debug context
{
__debug_dereference_assign_inner(var_id, value);
}}
}
Expand All @@ -594,6 +604,7 @@ pub fn build_debug_crate_file() -> String {
}}
pub fn __debug_member_assign_{n}<T, Index>(var_id: u32, value: T, {var_sig}) {{
unsafe {{
//@safety: debug context
__debug_inner_member_assign_{n}(var_id, value, {vars});
}}
}}
Expand Down
23 changes: 19 additions & 4 deletions compiler/noirc_frontend/src/lexer/lexer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -726,7 +726,7 @@ impl<'a> Lexer<'a> {
}

fn parse_comment(&mut self, start: u32) -> SpannedTokenResult {
let doc_style = match self.peek_char() {
let mut doc_style = match self.peek_char() {
Some('!') => {
self.next_char();
Some(DocStyle::Inner)
Expand All @@ -735,9 +735,17 @@ impl<'a> Lexer<'a> {
self.next_char();
Some(DocStyle::Outer)
}
Some('@') => Some(DocStyle::Safety),
_ => None,
};
let comment = self.eat_while(None, |ch| ch != '\n');
let mut comment = self.eat_while(None, |ch| ch != '\n');
if doc_style == Some(DocStyle::Safety) {
if comment.starts_with("@safety") {
comment = comment["@safety".len()..].to_string();
} else {
doc_style = None;
}
}

if !comment.is_ascii() {
let span = Span::from(start..self.position);
Expand All @@ -752,7 +760,7 @@ impl<'a> Lexer<'a> {
}

fn parse_block_comment(&mut self, start: u32) -> SpannedTokenResult {
let doc_style = match self.peek_char() {
let mut doc_style = match self.peek_char() {
Some('!') => {
self.next_char();
Some(DocStyle::Inner)
Expand All @@ -761,6 +769,7 @@ impl<'a> Lexer<'a> {
self.next_char();
Some(DocStyle::Outer)
}
Some('@') => Some(DocStyle::Safety),
_ => None,
};

Expand All @@ -787,7 +796,13 @@ impl<'a> Lexer<'a> {
ch => content.push(ch),
}
}

if doc_style == Some(DocStyle::Safety) {
if content.starts_with("@safety") {
content = content["@safety".len()..].to_string();
} else {
doc_style = None;
}
}
if depth == 0 {
if !content.is_ascii() {
let span = Span::from(start..self.position);
Expand Down
3 changes: 3 additions & 0 deletions compiler/noirc_frontend/src/lexer/token.rs
Original file line number Diff line number Diff line change
Expand Up @@ -345,6 +345,7 @@ impl Display for FmtStrFragment {
pub enum DocStyle {
Outer,
Inner,
Safety,
}

#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
Expand Down Expand Up @@ -424,11 +425,13 @@ impl fmt::Display for Token {
Token::LineComment(ref s, style) => match style {
Some(DocStyle::Inner) => write!(f, "//!{s}"),
Some(DocStyle::Outer) => write!(f, "///{s}"),
Some(DocStyle::Safety) => write!(f, "//@safety{s}"),
None => write!(f, "//{s}"),
},
Token::BlockComment(ref s, style) => match style {
Some(DocStyle::Inner) => write!(f, "/*!{s}*/"),
Some(DocStyle::Outer) => write!(f, "/**{s}*/"),
Some(DocStyle::Safety) => write!(f, "/*@safety{s}*/"),
None => write!(f, "/*{s}*/"),
},
Token::Quote(ref stream) => {
Expand Down
13 changes: 12 additions & 1 deletion compiler/noirc_frontend/src/parser/errors.rs
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,8 @@ pub enum ParserErrorReason {
WrongNumberOfAttributeArguments { name: String, min: usize, max: usize, found: usize },
#[error("The `deprecated` attribute expects a string argument")]
DeprecatedAttributeExpectsAStringArgument,
#[error("Unsafe block must start with a safety comment")]
MissingSafetyComment,
}

/// Represents a parsing error, or a parsing error in the making.
Expand Down Expand Up @@ -181,7 +183,11 @@ impl ParserError {
}

pub fn is_warning(&self) -> bool {
matches!(self.reason(), Some(ParserErrorReason::ExperimentalFeature(_)))
matches!(
self.reason(),
Some(ParserErrorReason::ExperimentalFeature(_))
| Some(ParserErrorReason::MissingSafetyComment)
)
}
}

Expand Down Expand Up @@ -272,6 +278,11 @@ impl<'a> From<&'a ParserError> for Diagnostic {
"Noir doesn't have immutable references, only mutable references".to_string(),
error.span,
),
ParserErrorReason::MissingSafetyComment => Diagnostic::simple_warning(
"Missing Safety Comment".into(),
"Unsafe block must start with a safety comment: //@safety".into(),
error.span,
),
other => Diagnostic::simple_error(format!("{other}"), String::new(), error.span),
},
None => {
Expand Down
19 changes: 17 additions & 2 deletions compiler/noirc_frontend/src/parser/parser/expression.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ use crate::{
MemberAccessExpression, MethodCallExpression, Statement, TypePath, UnaryOp, UnresolvedType,
},
parser::{labels::ParsingRuleLabel, parser::parse_many::separated_by_comma, ParserErrorReason},
token::{Keyword, Token, TokenKind},
token::{DocStyle, Keyword, SpannedToken, Token, TokenKind},
};

use super::{
Expand Down Expand Up @@ -375,6 +375,20 @@ impl<'a> Parser<'a> {
return None;
}

let next_token = self.next_token.token();
if matches!(
next_token,
Token::LineComment(_, Some(DocStyle::Safety))
| Token::BlockComment(_, Some(DocStyle::Safety))
) {
//Checks the safety comment is there, and skip it
let span = self.current_token_span;
self.eat_left_brace();
self.token = SpannedToken::new(Token::LeftBrace, span);
} else {
self.push_error(ParserErrorReason::MissingSafetyComment, self.current_token_span);
}

let start_span = self.current_token_span;
if let Some(block) = self.parse_block() {
Some(ExpressionKind::Unsafe(block, self.span_since(start_span)))
Expand Down Expand Up @@ -957,7 +971,8 @@ mod tests {

#[test]
fn parses_unsafe_expression() {
let src = "unsafe { 1 }";
let src = "unsafe { //@safety: test
1 }";
let expr = parse_expression_no_errors(src);
let ExpressionKind::Unsafe(block, _) = expr.kind else {
panic!("Expected unsafe expression");
Expand Down
5 changes: 4 additions & 1 deletion compiler/noirc_frontend/src/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3880,7 +3880,8 @@ fn errors_on_cyclic_globals() {
fn warns_on_unneeded_unsafe() {
let src = r#"
fn main() {
unsafe {
unsafe {
//@safety: test
foo()
}
}
Expand All @@ -3900,7 +3901,9 @@ fn warns_on_nested_unsafe() {
let src = r#"
fn main() {
unsafe {
//@safety: test
unsafe {
//@safety: test
foo()
}
}
Expand Down
1 change: 1 addition & 0 deletions compiler/noirc_frontend/src/tests/references.rs
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@ fn constrained_reference_to_unconstrained() {
let x_ref = &mut x;
if x == 5 {
unsafe {
//@safety: test context
mut_ref_input(x_ref, y);
}
}
Expand Down
2 changes: 2 additions & 0 deletions docs/docs/noir/concepts/unconstrained.md
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,7 @@ We can then run `u72_to_u8` as unconstrained brillig code in order to calculate
```rust
fn main(num: u72) -> pub [u8; 8] {
let out = unsafe {
//@safety: 'out' is properly constrained below in 'assert(num == reconstructed_num);'
u72_to_u8(num)
};

Expand Down Expand Up @@ -96,6 +97,7 @@ This ends up taking off another ~250 gates from our circuit! We've ended up with

Note that in order to invoke unconstrained functions we need to wrap them in an `unsafe` block,
to make it clear that the call is unconstrained.
Furthermore, a warning is emitted unless the `unsafe` block starts with a `//@safety: ...` comment explaining why it is fine to call the unconstrained function.

Generally we want to use brillig whenever there's something that's easy to verify but hard to compute within the circuit. For example, if you wanted to calculate a square root of a number it'll be a much better idea to calculate this in brillig and then assert that if you square the result you get back your number.

Expand Down
3 changes: 3 additions & 0 deletions noir_stdlib/src/array/check_shuffle.nr
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,9 @@ where
T: Eq,
{
unsafe {
/*@safety : shuffle_indices is ensured to be a permutation of 0..N, and then
shuffle_indices is ensured to map lhs to rhs: assert(lhs[i] == rhs[shuffle_indices[i]]), for all i in 0..N
*/
let shuffle_indices = __get_shuffle_indices(lhs, rhs);

for i in 0..N {
Expand Down
7 changes: 4 additions & 3 deletions noir_stdlib/src/array/mod.nr
Original file line number Diff line number Diff line change
Expand Up @@ -185,9 +185,10 @@ where
/// ```
pub fn sort_via<Env>(self, ordering: fn[Env](T, T) -> bool) -> Self {
unsafe {
// Safety: `sorted` array is checked to be:
// a. a permutation of `input`'s elements
// b. satisfying the predicate `ordering`
/*@safety: `sorted` array is checked to be:
a. a permutation of `input`'s elements
b. satisfying the predicate `ordering`
*/
let sorted = quicksort::quicksort(self, ordering);

if !is_unconstrained() {
Expand Down
11 changes: 9 additions & 2 deletions noir_stdlib/src/collections/umap.nr
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,11 @@ impl<K, V, B> UHashMap<K, V, B> {
H: Hasher,
{
// docs:end:contains_key
unsafe { self.get(key) }.is_some()
unsafe {
//@safety : unconstrained context
self.get(key)
}
.is_some()
}

// Returns true if the map contains no elements.
Expand Down Expand Up @@ -432,7 +436,10 @@ where
// Not marked as deleted and has key-value.
if equal & slot.is_valid() {
let (key, value) = slot.key_value_unchecked();
let other_value = unsafe { other.get(key) };
let other_value = unsafe {
//@safety : unconstrained context
other.get(key)
};

if other_value.is_none() {
equal = false;
Expand Down
15 changes: 13 additions & 2 deletions noir_stdlib/src/field/bn254.nr
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,10 @@ fn assert_gt_limbs(a: (Field, Field), b: (Field, Field)) {
let (alo, ahi) = a;
let (blo, bhi) = b;
unsafe {
/*@safety: borrow is enforced to be boolean due to its type.
if borrow is 0, it asserts that (alo > blo && ahi >= bhi)
if borrow is 1, it asserts that (alo <= blo && ahi > bhi)
*/
let borrow = lte_hint(alo, blo);

let rlo = alo - blo - 1 + (borrow as Field) * TWO_POW_128;
Expand All @@ -55,6 +59,7 @@ pub fn decompose(x: Field) -> (Field, Field) {
compute_decomposition(x)
} else {
unsafe {
/*@safety: decomposition is properly checked below*/
// Take hints of the decomposition
let (xlo, xhi) = decompose_hint(x);

Expand All @@ -74,7 +79,12 @@ pub fn decompose(x: Field) -> (Field, Field) {

pub fn assert_gt(a: Field, b: Field) {
if is_unconstrained() {
assert(unsafe { field_less_than(b, a) });
assert(
unsafe {
//@safety: already unconstrained
field_less_than(b, a)
},
);
} else {
// Decompose a and b
let a_limbs = decompose(a);
Expand All @@ -92,13 +102,14 @@ pub fn assert_lt(a: Field, b: Field) {
pub fn gt(a: Field, b: Field) -> bool {
if is_unconstrained() {
unsafe {
//@safety: unsafe in unconstrained
field_less_than(b, a)
}
} else if a == b {
false
} else {
// Take a hint of the comparison and verify it
unsafe {
//@safety: Take a hint of the comparison and verify it
if field_less_than(a, b) {
assert_gt(b, a);
false
Expand Down
1 change: 1 addition & 0 deletions noir_stdlib/src/field/mod.nr
Original file line number Diff line number Diff line change
Expand Up @@ -238,6 +238,7 @@ pub fn bytes32_to_field(bytes32: [u8; 32]) -> Field {
fn lt_fallback(x: Field, y: Field) -> bool {
if is_unconstrained() {
unsafe {
//@safety : unconstrained context
field_less_than(x, y)
}
} else {
Expand Down
5 changes: 4 additions & 1 deletion noir_stdlib/src/hash/mod.nr
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,10 @@ fn __derive_generators<let N: u32, let M: u32>(
// does not assert the limbs are 128 bits
// does not assert the decomposition does not overflow the EmbeddedCurveScalar
fn from_field_unsafe(scalar: Field) -> EmbeddedCurveScalar {
let (xlo, xhi) = unsafe { crate::field::bn254::decompose_hint(scalar) };
let (xlo, xhi) = unsafe {
//@safety : xlo and xhi decomposition is checked below
crate::field::bn254::decompose_hint(scalar)
};
// Check that the decomposition is correct
assert_eq(scalar, xlo + crate::field::bn254::TWO_POW_128 * xhi);
EmbeddedCurveScalar { lo: xlo, hi: xhi }
Expand Down
Loading

0 comments on commit 5c00a79

Please sign in to comment.