@@ -785,6 +785,26 @@ module GoCfg {
785785 c .hasLabel ( lbl .getLabel ( ) )
786786 )
787787 or
788+ // A `break` in a communication clause body terminates the enclosing
789+ // `select` statement, continuing after it. This mirrors the shared
790+ // library's handling of `break` in a `switch` case body, but `select` is
791+ // modelled language-specifically (it is not a `Switch`), so the break
792+ // must be caught here. The break completion bubbles up the AST until it
793+ // reaches a top-level statement of the comm clause body, at which point
794+ // flow resumes after the `select`. An unlabeled `break` targets the
795+ // innermost enclosing construct; a labeled `break` only targets this
796+ // `select` if it (or a `LabeledStmt` wrapping it) carries that label.
797+ exists ( Go:: SelectStmt sel , Go:: CommClause cc |
798+ cc = sel .getACommClause ( ) and
799+ ast = cc .getStmt ( _) and
800+ n .isAfter ( sel ) and
801+ c .getSuccessorType ( ) instanceof BreakSuccessor
802+ |
803+ not c .hasLabel ( _)
804+ or
805+ exists ( Label l | c .hasLabel ( l ) and hasLabel ( sel , l ) )
806+ )
807+ or
788808 exists ( Go:: FuncDef fd |
789809 ast = fd .getBody ( ) and
790810 not funcHasDefer ( fd ) and
@@ -1482,20 +1502,43 @@ module GoCfg {
14821502 )
14831503 }
14841504
1505+ /**
1506+ * Holds if there is a control-flow step from `n1` to `n2` for the
1507+ * communication operation of a comm clause of `sel` that has been selected.
1508+ *
1509+ * The channel operands (and, for a send, the value) of every clause are
1510+ * evaluated up front in the prep phase (see `selectCommPrepStart` and
1511+ * friends), and the `select` then non-deterministically dispatches to one
1512+ * clause via `In(sel) -> Before(cc)`. The communication node itself
1513+ * (`In(recv.getExpr())` for a receive, `In(send)` for a send) is therefore
1514+ * only reached through that dispatch, never by ordinary left-to-right
1515+ * evaluation of the clause.
1516+ *
1517+ * The `Before(...) -> ...` edges below are deliberately dead (their source
1518+ * nodes are unreachable): they exist solely to suppress the shared
1519+ * library's default left-to-right child sequencing for these AST nodes,
1520+ * which is keyed off the presence of an explicit step out of a node's
1521+ * `Before` node. Without them, the default sequencing would, for example,
1522+ * wire `After(channel) -> In(send)`, spuriously connecting the prep phase
1523+ * straight to the communication and bypassing the dispatch.
1524+ */
14851525 private predicate selectedCommStep (
14861526 Go:: SelectStmt sel , PreControlFlowNode n1 , PreControlFlowNode n2
14871527 ) {
14881528 exists ( Go:: RecvStmt recv | recv = sel .getACommClause ( ) .getComm ( ) |
1529+ // Suppress default sequencing of the receive statement and of the
1530+ // receive expression (both source nodes are unreachable).
14891531 n1 .isBefore ( recv ) and n2 .isIn ( recv .getExpr ( ) )
14901532 or
14911533 n1 .isBefore ( recv .getExpr ( ) ) and n2 .isBefore ( recv .getExpr ( ) .getOperand ( ) )
14921534 )
14931535 or
14941536 exists ( Go:: SendStmt send | send = sel .getACommClause ( ) .getComm ( ) |
1537+ // Suppress default sequencing of the send statement (source unreachable).
14951538 n1 .isBefore ( send ) and n2 .isBefore ( send .getChannel ( ) )
14961539 or
1497- n1 . isAfter ( send . getChannel ( ) ) and n2 . isBefore ( send . getValue ( ) )
1498- or
1540+ // The send communication happens at `In (send)`; flow then continues to
1541+ // the clause body via `selectStmt`.
14991542 n1 .isIn ( send ) and n2 .isAfter ( send )
15001543 )
15011544 }
0 commit comments