Skip to content

Commit f5fee09

Browse files
committed
Reject invalid pure effect contracts
1 parent e062459 commit f5fee09

5 files changed

Lines changed: 103 additions & 1 deletion

File tree

src/analyzer.rs

Lines changed: 62 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use crate::checks;
44
use crate::diagnostic::{Diagnostic, code};
55
use crate::hir::{DuplicateSymbolKind, Hir, HirTypeKind};
66
use crate::lexer::{Token, lex};
7-
use crate::syntax::ast::{Callee, EffectDecl, Expr, Item, Stmt, TypeRef};
7+
use crate::syntax::ast::{Callee, DataEffect, EffectDecl, Expr, Item, Stmt, TypeRef};
88
use crate::syntax::parse_source;
99

1010
pub fn analyze_source(file: &str, source: &str) -> Vec<Diagnostic> {
@@ -187,6 +187,60 @@ impl Analyzer<'_> {
187187
);
188188
}
189189
}
190+
191+
if function
192+
.effects
193+
.iter()
194+
.any(|effect| matches!(effect, EffectDecl::Name(name) if name == "pure"))
195+
{
196+
for param in function
197+
.params
198+
.iter()
199+
.filter(|param| param.effect == Some(DataEffect::Mut))
200+
{
201+
self.diagnostics.push(
202+
Diagnostic::error(
203+
code::INVALID_PURE_EFFECT,
204+
format!(
205+
"`{}` is declared pure but parameter `{}` is mutable.",
206+
function.name, param.name
207+
),
208+
param.span.clone(),
209+
"mutable parameter in pure function",
210+
)
211+
.with_cause("A `pure` function must not mutate reachable managed state.")
212+
.with_fix(
213+
"remove_pure_or_mut",
214+
"Remove `pure`, or change the parameter to `read` if the function does not mutate it.",
215+
"manual",
216+
),
217+
);
218+
}
219+
220+
for effect in function
221+
.effects
222+
.iter()
223+
.filter(|effect| matches!(effect, EffectDecl::Retains(_)))
224+
{
225+
self.diagnostics.push(
226+
Diagnostic::error(
227+
code::INVALID_PURE_EFFECT,
228+
format!(
229+
"`{}` is declared pure but also retains a parameter.",
230+
function.name
231+
),
232+
function.span.clone(),
233+
"retention in pure function",
234+
)
235+
.with_cause("A `pure` function must not retain parameters after returning.")
236+
.with_fix(
237+
"remove_pure_or_retains",
238+
format!("Remove `pure` or remove `{}`.", effect_display(effect)),
239+
"manual",
240+
),
241+
);
242+
}
243+
}
190244
}
191245
}
192246

@@ -553,6 +607,13 @@ fn effect_name(effect: &EffectDecl) -> &str {
553607
}
554608
}
555609

610+
fn effect_display(effect: &EffectDecl) -> String {
611+
match effect {
612+
EffectDecl::Name(name) => name.clone(),
613+
EffectDecl::Retains(param) => format!("retains({param})"),
614+
}
615+
}
616+
556617
fn duplicate_symbol_label(kind: DuplicateSymbolKind) -> &'static str {
557618
match kind {
558619
DuplicateSymbolKind::Function => "function",

src/diagnostic.rs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ pub mod code {
99
pub const DUPLICATE_FILE_MODE: &str = "RS0006";
1010
pub const UNKNOWN_RETAINED_PARAMETER: &str = "RS0007";
1111
pub const MISSING_PARAMETER_EFFECT: &str = "RS0008";
12+
pub const INVALID_PURE_EFFECT: &str = "RS0009";
1213
pub const FILE_MODE_VIOLATION: &str = "RS0101";
1314
pub const UNNAMED_ARGUMENT: &str = "RS0201";
1415
pub const MISSING_DATA_EFFECT: &str = "RS0202";
@@ -236,6 +237,11 @@ static DIAGNOSTIC_EXPLANATIONS: &[DiagnosticExplanation] = &[
236237
title: "missing parameter data effect",
237238
explanation: "Non-Copy parameters must declare `read`, `mut`, or `take` in the function signature so call effects are review-visible.",
238239
},
240+
DiagnosticExplanation {
241+
code: code::INVALID_PURE_EFFECT,
242+
title: "invalid pure effect",
243+
explanation: "`effects(pure)` is a guarantee that the function does not mutate reachable managed state and does not retain parameters.",
244+
},
239245
DiagnosticExplanation {
240246
code: code::FILE_MODE_VIOLATION,
241247
title: "file mode violation",
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// expect: RS0009
2+
mode: managed
3+
4+
struct Image {
5+
pixels: Buffer
6+
}
7+
8+
fn normalize(image: mut Image) -> Image
9+
effects(pure)
10+
{
11+
return image
12+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// expect: RS0009
2+
mode: managed
3+
4+
struct Image {
5+
pixels: Buffer
6+
}
7+
8+
fn memoize(image: read Image) -> Image
9+
effects(pure, retains(image))
10+
{
11+
return image
12+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
mode: managed
2+
3+
struct StringView {
4+
value: String
5+
}
6+
7+
fn normalize_path(path: read String) -> fresh StringView
8+
effects(pure)
9+
{
10+
return StringView(value: read path)
11+
}

0 commit comments

Comments
 (0)