Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions third_party/move/move-compiler-v2/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -625,6 +625,8 @@ pub fn stackless_bytecode_check_pipeline(options: &Options) -> FunctionTargetPip
if options.experiment_on(Experiment::LINT_CHECKS) {
// Some lint checks need live variable analysis.
pipeline.add_processor(Box::new(LiveVarAnalysisProcessor::new(false)));
// Some lint checks need reachability annotations.
pipeline.add_processor(Box::new(UnreachableCodeProcessor {}));
pipeline.add_processor(Box::new(LintProcessor {}));
}

Expand Down
5 changes: 5 additions & 0 deletions third_party/move/move-model/src/model.rs
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,11 @@ impl Loc {
self.inlined_from_loc.is_some()
}

/// Returns the immediate `inlined-from` link of this location, if any.
pub fn inlined_from_loc(&self) -> Option<&Loc> {
Comment thread
vineethk marked this conversation as resolved.
self.inlined_from_loc.as_deref()
}

// If `self` is an inlined `Loc`, then add the same
// inlining info to the parameter `loc`.
fn inline_if_needed(&self, loc: Loc) -> Loc {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,19 @@
// Licensed pursuant to the Innovation-Enabling Source Code License, available at https://github.com/aptos-labs/aptos-core/blob/main/LICENSE

//! This module (and its submodules) contain various stackless-bytecode-based lint checks.
//! Live variable analysis is a prerequisite for this lint processor.
//!
//! Prerequisite analyses (must be registered before the lint processor in the pipeline):
//! - Live variable analysis.
//! - Reachable state analysis.
//!
//! When adding a new lint check that depends on additional analyses, register
//! those analyses as prerequisites and document them here.
//!
//! The lint checks also assume that all the correctness checks have already been performed.

mod avoid_copy_on_identity_comparison;
mod needless_mutable_reference;
mod unreachable_code;

use move_compiler_v2::external_checks::StacklessBytecodeChecker;
Comment thread
vineethk marked this conversation as resolved.
use std::collections::BTreeMap;
Expand All @@ -19,6 +27,7 @@ pub fn get_default_linter_pipeline(
let checks: Vec<Box<dyn StacklessBytecodeChecker>> = vec![
Box::new(avoid_copy_on_identity_comparison::AvoidCopyOnIdentityComparison {}),
Box::new(needless_mutable_reference::NeedlessMutableReference {}),
Box::new(unreachable_code::UnreachableCode {}),
];
let checks_category = config.get("checks").map_or("default", |s| s.as_str());
if checks_category == "strict" || checks_category == "experimental" {
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,114 @@
// Copyright (c) Aptos Foundation
// Licensed pursuant to the Innovation-Enabling Source Code License, available at https://github.com/aptos-labs/aptos-core/blob/main/LICENSE

//! Lint that warns on user-written code that is definitely unreachable.
//!
//! Prerequisite: `ReachableStateAnnotation`, produced by `UnreachableCodeProcessor`
//! (registered in the lint pipeline as a prereq, alongside live variable analysis).

use move_binary_format::file_format::CodeOffset;
use move_compiler_v2::{
external_checks::StacklessBytecodeChecker,
pipeline::unreachable_code_analysis::ReachableStateAnnotation,
};
use move_model::model::Loc;
use move_stackless_bytecode::function_target::FunctionTarget;
use std::collections::BTreeSet;

pub struct UnreachableCode {}

impl StacklessBytecodeChecker for UnreachableCode {
fn get_name(&self) -> String {
"unreachable_code".to_string()
}

fn check(&self, target: &FunctionTarget) {
let annotation = target
.get_annotations()
.get::<ReachableStateAnnotation>()
.expect(
"ReachableStateAnnotation missing: \
UnreachableCodeProcessor must run before the lint pipeline",
);
let code = target.get_bytecode();

// Two passes: a dead instruction can carry a Loc that encloses a
// *later* reachable Loc (e.g. a synthesized jump using the surrounding
// loop's Loc, emitted before the loop's reachable back-edge target),
// so we need every reachable Loc in hand before applying the filter.
// For inlined instructions, also record their call-site Loc. A
// function whose body is entirely inlined ends with a synthesized
// `Ret` whose Loc is the caller's body; without the call site in
// the reachable set, that Loc encloses nothing reachable (the
// inlinee Locs sit elsewhere) and we'd false-positive.
let mut reachable_locs: BTreeSet<Loc> = BTreeSet::new();
for (offset, instr) in code.iter().enumerate() {
if !annotation.is_definitely_not_reachable(offset as CodeOffset) {
let loc = target.get_bytecode_loc(instr.get_attr_id());
reachable_locs.insert(call_site_loc(&loc));
reachable_locs.insert(loc);
}
}

let mut current_run: Vec<Loc> = Vec::new();
for (offset, instr) in code.iter().enumerate() {
if annotation.is_definitely_not_reachable(offset as CodeOffset) {
let loc = target.get_bytecode_loc(instr.get_attr_id());
// The two skip paths below use `continue` rather than flushing the
// current run on purpose: when two dead instructions are split only
// by skipped ones, we still want them reported as a single warning
// instead of two adjacent ones.
// Skip code from inlining — not actionable at this site.
if loc.is_inlined() {
continue;
}
// Skip Locs of compiler-synthesized scaffolding (merge labels,
// back-jumps, trailing `Ret`): they reuse a parent AST node's
// Loc that physically wraps a reachable sibling instruction.
if reachable_locs.iter().any(|r| encloses_by_span(&loc, r)) {
Comment thread
vineethk marked this conversation as resolved.
continue;
}
Comment thread
vineethk marked this conversation as resolved.
Comment on lines +55 to +70
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The continue in the inlined and scaffolding skip paths intentionally doesn't flush current_run, so dead instructions separated only by skipped instructions merge into one warning. This seems correct — the user perceives them as one dead region. But a reader might wonder whether flush should happen before continue. Worth a one-line comment like:

// NB: `continue` (not `flush`) — skipped instructions are transparent
// to run-merging so the user sees one contiguous warning.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

current_run.push(loc);
} else {
self.flush(target, std::mem::take(&mut current_run));
}
}
self.flush(target, current_run);
}
}

impl UnreachableCode {
fn flush(&self, target: &FunctionTarget, run: Vec<Loc>) {
if run.is_empty() {
return;
}
// `Loc::enclosing` takes min-start / max-end, so duplicates and
// unsorted input are fine — many bytecode instructions share one
// statement Loc.
let loc = Loc::enclosing(&run);
self.report(target.global_env(), &loc, "unreachable code");
}
}

/// Outermost Loc in the inlined-from chain — the user-visible call site.
fn call_site_loc(loc: &Loc) -> Loc {
let mut cur = loc;
while let Some(next) = cur.inlined_from_loc() {
cur = next;
}
cur.clone()
}

/// Span-only enclosure (ignores `inlined_from_loc`, unlike `Loc::is_enclosing`).
///
/// The scaffolding-skip heuristic in `check` relies on a compiler invariant:
/// synthesized bytecode instructions (merge labels, back-jumps, trailing `Ret`)
/// inherit the `Loc` of their enclosing AST node rather than getting a distinct
/// `Loc`. The filter detects such instructions by checking whether a dead
/// instruction's `Loc` physically wraps a reachable instruction's `Loc`.
/// If that compiler invariant ever changes, this heuristic will need updating.
fn encloses_by_span(outer: &Loc, inner: &Loc) -> bool {
outer.file_id() == inner.file_id()
&& inner.span().start() >= outer.span().start()
&& inner.span().end() <= outer.span().end()
}
Comment on lines +100 to +114
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This heuristic relies on a compiler invariant: synthesized bytecode instructions (merge labels, back-jumps, trailing Ret) inherit the Loc of their parent AST node rather than getting a distinct Loc. The filter detects this by checking whether a dead instruction's Loc physically wraps a reachable instruction's Loc.

Consider adding a brief doc note about this assumption, e.g.:

/// This works because the compiler assigns synthesized instructions the
/// Loc of their enclosing AST node; if that ever changes, this heuristic
/// will need updating.

This would help future maintainers understand why the filter exists and when it might break.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@

Diagnostics:
warning: [lint] unreachable code
┌─ tests/default-only/unreachable_code_abort_or_return_always.move:8:9
8 │ 42
│ ^^
= To suppress this warning, annotate the function/module with the attribute `#[lint::skip(unreachable_code)]`.
= For more information, see https://aptos.dev/en/build/smart-contracts/linter#unreachable_code.
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
module 0xc0ffee::m {
public fun test(p: bool): u64 {
if (p) {
abort 0
} else {
return 1
};
42
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@

Diagnostics:
warning: [lint] unreachable code
┌─ tests/default-only/unreachable_code_after_abort.move:4:9
4 │ 0
│ ^
= To suppress this warning, annotate the function/module with the attribute `#[lint::skip(unreachable_code)]`.
= For more information, see https://aptos.dev/en/build/smart-contracts/linter#unreachable_code.
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
module 0xc0ffee::m {
public fun test(): u32 {
abort 0;
0
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@

Diagnostics:
warning: [lint] unreachable code
┌─ tests/default-only/unreachable_code_break_unreachable.move:8:17
8 │ i = i + 1; // unreachable
│ ^^^^^^^^^
= To suppress this warning, annotate the function/module with the attribute `#[lint::skip(unreachable_code)]`.
= For more information, see https://aptos.dev/en/build/smart-contracts/linter#unreachable_code.

warning: [lint] unreachable code
┌─ tests/default-only/unreachable_code_break_unreachable.move:11:17
11 │ ╭ i = i + 1; // unreachable
12 │ │ };
13 │ │ i = i + 1; // unreachable
│ ╰─────────────────────^
= To suppress this warning, annotate the function/module with the attribute `#[lint::skip(unreachable_code)]`.
= For more information, see https://aptos.dev/en/build/smart-contracts/linter#unreachable_code.
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
module 0xc0ffee::m {
public fun test() {
let i = 0;
loop {
i = i + 1;
if (i == 10) {
break;
i = i + 1; // unreachable
} else {
continue;
i = i + 1; // unreachable
};
i = i + 1; // unreachable
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@

Diagnostics:
warning: [lint] unreachable code
┌─ tests/default-only/unreachable_code_conditional_loop.move:8:17
8 │ ╭ noop(); // dead region 1
9 │ │ noop();
│ ╰──────────────────────^
= To suppress this warning, annotate the function/module with the attribute `#[lint::skip(unreachable_code)]`.
= For more information, see https://aptos.dev/en/build/smart-contracts/linter#unreachable_code.

warning: [lint] unreachable code
┌─ tests/default-only/unreachable_code_conditional_loop.move:13:13
13 │ ╭ noop(); // dead region 2
14 │ │ noop();
│ ╰──────────────────^
= To suppress this warning, annotate the function/module with the attribute `#[lint::skip(unreachable_code)]`.
= For more information, see https://aptos.dev/en/build/smart-contracts/linter#unreachable_code.
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
module 0xc0ffee::m {
public fun noop() {}

public fun test(p: bool, q: bool) {
while (p) {
if (q) {
loop {};
noop(); // dead region 1
noop();
} else {
break;
};
noop(); // dead region 2
noop();
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@

Diagnostics:
warning: [lint] unreachable code
┌─ tests/default-only/unreachable_code_control_exp_as_term.move:8:23
8 │ 1 + loop {} + 2;
│ ╭───────────────────────^
9 │ │ 1 + return + 0;
10 │ │
11 │ │ foo(&if (cond) 0 else 1);
12 │ │ foo(&loop {});
13 │ │ foo(&return);
14 │ │ foo(&abort 0);
│ ╰─────────────────────^
= To suppress this warning, annotate the function/module with the attribute `#[lint::skip(unreachable_code)]`.
= For more information, see https://aptos.dev/en/build/smart-contracts/linter#unreachable_code.
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
#[lint::skip(simpler_numeric_expression)]
module 0x42::M {
fun foo(_: &u64) {}

#[lint::skip(unused_function)]
public fun t(cond: bool) {
1 + if (cond) 0 else { 1 } + 2;
1 + loop {} + 2;
1 + return + 0;

foo(&if (cond) 0 else 1);
foo(&loop {});
foo(&return);
foo(&abort 0);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

No errors or warnings!
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
// Dead code that originates from an inlined call should NOT warn — the
// synthesized trailing `Ret` is an inlining artifact.
//
// Genuinely dead code inside an inline function body is also not flagged at the
// call site: this is a known false negative.
module 0xc0ffee::m {
inline fun terminator() {
abort 0
}

public fun caller() {
terminator();
}

inline fun dead_in_body(): u64 {
abort 0;
42 // genuinely dead, but won't warn because it's inlined at the call site
}

public fun caller2(): u64 {
dead_in_body()
}
}
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice test for the false-positive prevention on inlined terminators. Consider adding a complementary test where the inline function itself has genuinely dead code in its body, e.g.:

inline fun dead_in_body(): u64 {
    abort 0;
    42  // genuinely dead, but won't warn because it's inlined at call site
}
public fun caller2(): u64 { dead_in_body() }

Currently the is_inlined() skip means such dead code is a known false negative. Documenting that in a test expectation would make the design decision explicit and prevent a future maintainer from treating it as a bug.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@

Diagnostics:
warning: [lint] unreachable code
┌─ tests/default-only/unreachable_code_loop_labels.move:9:21
9 │ break
│ ^^^^^
= To suppress this warning, annotate the function/module with the attribute `#[lint::skip(unreachable_code)]`.
= For more information, see https://aptos.dev/en/build/smart-contracts/linter#unreachable_code.

warning: [lint] unreachable code
┌─ tests/default-only/unreachable_code_loop_labels.move:12:13
12 │ break
│ ^^^^^
= To suppress this warning, annotate the function/module with the attribute `#[lint::skip(unreachable_code)]`.
= For more information, see https://aptos.dev/en/build/smart-contracts/linter#unreachable_code.
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
#[lint::skip(while_true)]
module 0x815::test {
public fun f1() {
'outer: loop {
// unlabeled loop, but counts in nesting in AST
loop {
'inner: loop if (true) loop {
if (false) continue 'outer else break 'inner;
break
} else continue 'outer
};
break
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@

Diagnostics:
warning: [lint] unreachable code
┌─ tests/default-only/unreachable_code_loop_only.move:4:9
4 │ 42
│ ^^
= To suppress this warning, annotate the function/module with the attribute `#[lint::skip(unreachable_code)]`.
= For more information, see https://aptos.dev/en/build/smart-contracts/linter#unreachable_code.
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
module 0xc0ffee::m {
public fun test(): u64 {
loop {};
42
}
}
Loading
Loading