Skip to content
Open
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
68 changes: 58 additions & 10 deletions compiler/crates/hy-check/src/channel_liveness.rs
Original file line number Diff line number Diff line change
Expand Up @@ -95,10 +95,28 @@ impl ChannelLivenessChecker {
}
}

fn register_param_cap(&mut self, name: String, is_send: bool, def_span: Span) {
let pipe = PipeInfo {
tx: if is_send { name.clone() } else { String::new() },
rx: if !is_send { name.clone() } else { String::new() },
tx_state: if is_send { ChannelTypestate::Fresh } else { ChannelTypestate::Closed },
rx_state: if !is_send { ChannelTypestate::Fresh } else { ChannelTypestate::Drained },
def_span,
};

let p_idx = self.pipes_all.len();
self.pipes_all.push(pipe.clone());
self.cap_to_pipe.insert(name, p_idx);

if let Some(cur) = self.scope_stack.last_mut() {
cur.pipes.push(pipe);
}
}

fn check_terminal_invariants(&mut self, scope: &ScopeState) {
for pipe in &scope.pipes {
// Check send capability terminal state
if !scope.moved_caps.contains(&pipe.tx) && pipe.tx_state != ChannelTypestate::Closed {
if !pipe.tx.is_empty() && !scope.moved_caps.contains(&pipe.tx) && pipe.tx_state != ChannelTypestate::Closed {
self.diags.push(Diagnostic::error(
"HYB-E4004",
&self.file_path,
Expand All @@ -112,7 +130,7 @@ impl ChannelLivenessChecker {

// Check receive capability terminal state
// If rx was moved into a subtask, the subtask assumed lifecycle responsibility
if !scope.moved_caps.contains(&pipe.rx) && pipe.rx_state != ChannelTypestate::Drained {
if !pipe.rx.is_empty() && !scope.moved_caps.contains(&pipe.rx) && pipe.rx_state != ChannelTypestate::Drained {
self.diags.push(Diagnostic::error(
"HYB-E4005",
&self.file_path,
Expand All @@ -127,7 +145,19 @@ impl ChannelLivenessChecker {
}

fn check_fn(&mut self, f: &FnDecl) {
self.scope_stack.clear();
self.cap_to_pipe.clear();
self.pipes_all.clear();
self.push_scope();

for param in &f.params {
if is_send_cap(&param.ty) {
self.register_param_cap(param.name.clone(), true, param.span);
} else if is_recv_cap(&param.ty) {
self.register_param_cap(param.name.clone(), false, param.span);
}
}

if let Some(body) = &f.body {
for stmt in &body.stmts {
self.check_stmt(stmt);
Expand Down Expand Up @@ -396,8 +426,15 @@ impl ChannelLivenessChecker {
Expr::Try { operand, .. } => {
self.check_expr(operand);
}
Expr::FnLit { body, .. } => {
Expr::FnLit { params, body, .. } => {
self.push_scope();
for param in params {
if is_send_cap(&param.ty) {
self.register_param_cap(param.name.clone(), true, param.span);
} else if is_recv_cap(&param.ty) {
self.register_param_cap(param.name.clone(), false, param.span);
}
}
for s in &body.stmts {
self.check_stmt(s);
}
Expand Down Expand Up @@ -438,13 +475,6 @@ impl ChannelLivenessChecker {
self.check_expr(&a.value);
}
}
Expr::FnLit { body, .. } => {
self.push_scope();
for s in &body.stmts {
self.check_stmt(s);
}
self.pop_scope();
}
Expr::Receive { chan, span } => {
if let Some(cap) = self.get_cap_name(chan) {
if self.is_moved(&cap) {
Expand Down Expand Up @@ -602,3 +632,21 @@ impl ChannelLivenessChecker {
}
}
}

fn is_send_cap(ty: &TypeExpr) -> bool {
match ty {
TypeExpr::Named { name, .. } => {
name.starts_with("hy.send_cap") || name.starts_with("send_cap")
}
_ => false,
}
}

fn is_recv_cap(ty: &TypeExpr) -> bool {
match ty {
TypeExpr::Named { name, .. } => {
name.starts_with("hy.recv_cap") || name.starts_with("recv_cap")
}
_ => false,
}
}
152 changes: 152 additions & 0 deletions compiler/crates/hy-check/tests/channel_liveness_4200.rs
Original file line number Diff line number Diff line change
Expand Up @@ -718,3 +718,155 @@ fn main() {
res.diagnostics
);
}

#[test]
fn test_param_cap_unclosed_sender_reject() {
let src = r#"
fn worker(tx hy.send_cap[int]) {
tx.send(42)
// tx is never closed or moved before function returns
}

fn main() {
tx, rx := hy.pipe[int]()
task worker(move tx)
rx.drain()
}
"#;
let res = check_src(src);
assert_eq!(res.verdict, Verdict::Reject);
assert!(
res.diagnostics.iter().any(|d| d.code == "HYB-E4004"),
"Expected HYB-E4004 for unclosed send capability parameter: {:?}",
res.diagnostics
);
}

#[test]
fn test_param_cap_undrained_receiver_reject() {
let src = r#"
fn receiver(rx hy.recv_cap[int]) {
v := rx.recv()
_ = v
// rx is never drained or moved before function returns
}

fn main() {
tx, rx := hy.pipe[int]()
tx.close()
task receiver(move rx)
}
"#;
let res = check_src(src);
assert_eq!(res.verdict, Verdict::Reject);
assert!(
res.diagnostics.iter().any(|d| d.code == "HYB-E4005"),
"Expected HYB-E4005 for undrained receive capability parameter: {:?}",
res.diagnostics
);
}

#[test]
fn test_param_cap_double_move_reject() {
let src = r#"
fn sub(tx hy.send_cap[int]) {
tx.close()
}

fn forwarder(tx hy.send_cap[int]) {
task sub(move tx)
task sub(move tx)
}

fn main() {
tx, rx := hy.pipe[int]()
task forwarder(move tx)
rx.drain()
}
"#;
let res = check_src(src);
assert_eq!(res.verdict, Verdict::Reject);
assert!(
res.diagnostics.iter().any(|d| d.code == "HYB-E3001"),
"Expected HYB-E3001 for double move of parameter capability: {:?}",
res.diagnostics
);
}

#[test]
fn test_param_cap_use_after_move_reject() {
let src = r#"
fn sub(tx hy.send_cap[int]) {
tx.close()
}

fn forwarder(tx hy.send_cap[int]) {
task sub(move tx)
tx.send(10)
}

fn main() {
tx, rx := hy.pipe[int]()
task forwarder(move tx)
rx.drain()
}
"#;
let res = check_src(src);
assert_eq!(res.verdict, Verdict::Reject);
assert!(
res.diagnostics.iter().any(|d| d.code == "HYB-E3001"),
"Expected HYB-E3001 for use-after-move of parameter capability: {:?}",
res.diagnostics
);
}

#[test]
fn test_param_cap_unmoved_task_capture_reject() {
let src = r#"
fn sub(tx hy.send_cap[int]) {
tx.close()
}

fn forwarder(tx hy.send_cap[int]) {
task sub(tx)
tx.close()
}

fn main() {
tx, rx := hy.pipe[int]()
task forwarder(move tx)
rx.drain()
}
"#;
let res = check_src(src);
assert_eq!(res.verdict, Verdict::Reject);
assert!(
res.diagnostics.iter().any(|d| d.code == "HYB-E3002"),
"Expected HYB-E3002 for unmoved capture of parameter capability across task boundary: {:?}",
res.diagnostics
);
}

#[test]
fn test_param_cap_valid_worker_lifecycle_accept() {
let src = r#"
fn proxy(tx hy.send_cap[int], rx hy.recv_cap[int]) {
v := rx.recv()
tx.send(v)
rx.drain()
tx.close()
}

fn main() {
tx, rx := hy.pipe[int]()
task proxy(move tx, move rx)
}
"#;
let res = check_src(src);
assert_eq!(
res.verdict,
Verdict::Accept,
"Valid parameter capabilities lifecycle must accept cleanly: {:?}",
res.diagnostics
);
}
Loading