Skip to content

Commit 669e537

Browse files
authored
fix(types): emit A07003 when effects appear in must-not (#1539)
Source `must-not { io }` was parsed (`ClauseKind::MustNot`) and then ignored. Spec A07003 is "Effect E in must-not list." A contract could declare `effects { io }` and `must-not { io }` and type-check. ## Change - Collect `must-not` effect names from contract/fn/extern clauses. - Unknown names on that list are A07003 (same as unknown `effects`). - If a declared, inferred, or callee effect (after group expansion) is on the list, emit A07003. ## Validation - `cargo test -p assura-types --locked --lib must_not` - `cargo clippy -p assura-types --lib --locked -- -D warnings` Signed-off-by: Sebastien Tardif <SebTardif@ncf.ca>
1 parent f24d193 commit 669e537

2 files changed

Lines changed: 143 additions & 2 deletions

File tree

crates/assura-types/src/checkers/effects.rs

Lines changed: 95 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -344,6 +344,32 @@ impl EffectChecker {
344344
pub fn is_known(&self, effect: &str) -> bool {
345345
self.known_effects.contains(effect)
346346
}
347+
348+
/// A07003 when a used effect (or its expansion) is on the `must-not` list.
349+
pub fn check_must_not(
350+
&self,
351+
used: &EffectSet,
352+
forbidden: &EffectSet,
353+
span: &Range<usize>,
354+
) -> Vec<EffectError> {
355+
let used_exp = self.expand(used);
356+
let forbidden_exp = self.expand(forbidden);
357+
let mut errors = Vec::new();
358+
let mut names: Vec<&str> = used_exp
359+
.iter()
360+
.filter(|name| forbidden_exp.contains(name))
361+
.collect();
362+
names.sort_unstable();
363+
names.dedup();
364+
for name in names {
365+
errors.push(EffectError {
366+
code: "A07003".into(),
367+
message: format!("effect `{name}` is in the must-not list"),
368+
span: span.clone(),
369+
});
370+
}
371+
errors
372+
}
347373
}
348374

349375
impl EffectChecker {
@@ -357,6 +383,18 @@ impl EffectChecker {
357383
continue;
358384
};
359385
let (declared, actual) = Self::extract_effects_from_clauses(clauses);
386+
let must_not = Self::extract_must_not_from_clauses(clauses);
387+
if let Some(ref forbidden) = must_not {
388+
for ee in checker.check_known(forbidden, &decl.span) {
389+
errors.push(TypeError {
390+
code: ee.code,
391+
message: ee.message,
392+
span: ee.span,
393+
secondary: None,
394+
suggestion: None,
395+
});
396+
}
397+
}
360398
if let Some(ref declared_set) = declared {
361399
for ee in checker.check_known(declared_set, &decl.span) {
362400
errors.push(TypeError {
@@ -368,8 +406,8 @@ impl EffectChecker {
368406
});
369407
}
370408
if matches!(&decl.node, Decl::FnDef(_)) {
371-
if let Some(actual_set) = actual {
372-
for ee in checker.check_containment(declared_set, &actual_set, &decl.span) {
409+
if let Some(ref actual_set) = actual {
410+
for ee in checker.check_containment(declared_set, actual_set, &decl.span) {
373411
errors.push(TypeError {
374412
code: ee.code,
375413
message: ee.message,
@@ -389,6 +427,47 @@ impl EffectChecker {
389427
suggestion: None,
390428
});
391429
}
430+
if let Some(ref forbidden) = must_not {
431+
for ee in checker.check_must_not(declared_set, forbidden, &decl.span) {
432+
errors.push(TypeError {
433+
code: ee.code,
434+
message: ee.message,
435+
span: ee.span,
436+
secondary: None,
437+
suggestion: None,
438+
});
439+
}
440+
if let Some(ref actual_set) = actual {
441+
for ee in checker.check_must_not(actual_set, forbidden, &decl.span) {
442+
errors.push(TypeError {
443+
code: ee.code,
444+
message: ee.message,
445+
span: ee.span,
446+
secondary: None,
447+
suggestion: None,
448+
});
449+
}
450+
}
451+
for ee in checker.check_must_not(&callee_effects, forbidden, &decl.span) {
452+
errors.push(TypeError {
453+
code: ee.code,
454+
message: ee.message,
455+
span: ee.span,
456+
secondary: None,
457+
suggestion: None,
458+
});
459+
}
460+
}
461+
} else if let Some(ref forbidden) = must_not {
462+
for ee in checker.check_must_not(declared_set, forbidden, &decl.span) {
463+
errors.push(TypeError {
464+
code: ee.code,
465+
message: ee.message,
466+
span: ee.span,
467+
secondary: None,
468+
suggestion: None,
469+
});
470+
}
392471
}
393472
}
394473
}
@@ -423,6 +502,20 @@ impl EffectChecker {
423502
map
424503
}
425504

505+
fn extract_must_not_from_clauses(clauses: &[assura_parser::ast::Clause]) -> Option<EffectSet> {
506+
let mut names = Vec::new();
507+
for clause in clauses {
508+
if clause.kind == ClauseKind::MustNot {
509+
names.extend(Self::extract_effect_names_from_expr(&clause.body));
510+
}
511+
}
512+
if names.is_empty() {
513+
None
514+
} else {
515+
Some(EffectSet::from_effect_names(names))
516+
}
517+
}
518+
426519
/// Extract declared and actual effect sets from a list of clauses.
427520
pub fn extract_effects_from_clauses(
428521
clauses: &[assura_parser::ast::Clause],

crates/assura-types/src/checks/effects_tests.rs

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,3 +39,51 @@ fn test_effect_polymorphism_basic() {
3939
"effect variable E should not produce A07003, got: {a07003_errors:?}"
4040
);
4141
}
42+
43+
#[test]
44+
fn must_not_io_with_effects_io_a07003() {
45+
let sf = parse_source(
46+
r#"contract Forbidden {
47+
effects { io }
48+
must-not { io }
49+
requires { true }
50+
}"#,
51+
);
52+
let errs = run_effect_checks(&sf);
53+
assert!(
54+
errs.iter()
55+
.any(|e| e.code == "A07003" && e.message.contains("must-not")),
56+
"effects(io) + must-not(io) must be A07003, got: {errs:?}"
57+
);
58+
}
59+
60+
#[test]
61+
fn must_not_database_allows_effects_io() {
62+
let sf = parse_source(
63+
r#"contract OkIo {
64+
effects { io }
65+
must-not { database }
66+
requires { true }
67+
}"#,
68+
);
69+
let errs = run_effect_checks(&sf);
70+
assert!(
71+
!errs.iter().any(|e| e.message.contains("must-not")),
72+
"io is not in must-not database, got: {errs:?}"
73+
);
74+
}
75+
76+
#[test]
77+
fn must_not_unknown_name_a07003() {
78+
let sf = parse_source(
79+
r#"contract BadForbid {
80+
must-not { teleport }
81+
requires { true }
82+
}"#,
83+
);
84+
let errs = run_effect_checks(&sf);
85+
assert!(
86+
errs.iter().any(|e| e.code == "A07003"),
87+
"unknown must-not name must be A07003, got: {errs:?}"
88+
);
89+
}

0 commit comments

Comments
 (0)