vj-codegen 0.1.0

//! T12 (`docs/superpowers/plans/2026-10-03-sva.md`): named sequence
//! declarations, LRM 16.8/16.8.1 -- the cyclic-dependency check. (Instance
//! expansion and formal-argument substitution live in [`super::build`].)
//!
//! ## Deviation from the plan: slang's own graph, not a second one
//!
//! The plan says to build the named-sequence dependency graph and reject its
//! cycles. The graph 16.8 defines needs name resolution (which declaration an
//! identifier in a sequence body, a default actual or an actual argument
//! names, honouring formal-argument shadowing and scoping). `sv-lang` exposes
//! no accessor from a `SequenceSymbol` to its declaration body, so a graph
//! built here would have to re-derive that resolution from syntax -- a second,
//! divergent implementation of what slang already does. slang already
//! implements exactly 16.8's edge rule, including both of its non-obvious
//! edges (an instance within a default actual argument, and an instance within
//! an actual argument), and reports a cycle as a `RecursiveSequence` error
//! for EVERY cyclic declaration, whether or not anything instantiates it
//! (checked live for `s1`/`s2` unused, `s(s(a))`, and a default-argument
//! loop; one gap, below). [`check_named_sequence_cycles`] converts that
//! diagnostic into this crate's named [`LoweringError`] and recovers the cycle
//! it quotes from the diagnostic's own `while expanding sequence 'X'` notes
//! (the expansion stack at the point of detection, innermost first), which are
//! only exposed as rendered text.
//!
//! **Known gap.** `s(s(a))` written inside ANOTHER sequence's declaration
//! raises no slang diagnostic (pinned by a test below). The automaton builder
//! closes it: it walks 16.8's declaration graph while expanding (an actual
//! argument hangs off the chain of its call site) and refuses a declaration
//! already on the chain.
//!
//! ## Formal-argument rules (16.8.1)
//!
//! Likewise the typing rules for actual arguments -- `$` only for an untyped
//! formal used as an upper bound, constant actuals for delay/repetition
//! bounds, `shortint`/`int`/`longint` for a typed bound formal, `event`
//! formals, no goto repetition of an instance, an actual per formal without a
//! default, cast compatibility with a typed formal (16.8.1 c), no event
//! expression for a `sequence` formal (16.8.1 a), and the arity/naming errors of
//! the argument list -- are slang errors; [`check_formal_argument_rules`] reports them
//! with the clause they enforce rather than re-implementing them.
//!
//! Nothing calls these checks outside tests until sva T29 wires the builder
//! into lowering (same as `build`/`ranges`).
#![allow(dead_code)]

use sv_lang::Diagnostics;

use crate::error::LoweringError;

/// The slang diagnostic code for a cyclic dependency among named sequences
/// (16.8): "sequence 'X' is recursive".
const RECURSIVE_SEQUENCE: &str = "RecursiveSequence";

/// Rejects a design whose named sequences have a cyclic dependency (LRM 16.8:
/// "It shall be an error if a cyclic dependency among named sequences results
/// from their instantiations"). `diags` is `Design::diagnostics()` -- slang
/// reports the cycle at elaboration of the declaration itself, so it is
/// present whether or not any assertion instantiates the cycle.
///
/// The error is [`LoweringError`] naming the sequence slang reports and, when
/// the diagnostic's expansion notes are available, the cycle as a closed walk
/// (`s1 -> s2 -> s1`).
pub fn check_named_sequence_cycles(diags: &Diagnostics) -> Result<(), LoweringError> {
    let Some(first) = diags
        .items()
        .iter()
        .find(|d| d.is_error() && d.code_name() == RECURSIVE_SEQUENCE)
    else {
        return Ok(());
    };
    let reported = quoted_name(&first.message)
        .unwrap_or("<unknown>")
        .to_string();
    let chain = expansion_chain(diags.rendered(), &first.message);
    let cycle = match chain.as_slice() {
        [] => format!("sequence `{reported}` is recursive"),
        [head, ..] => {
            let mut walk = chain.join(" -> ");
            walk.push_str(" -> ");
            walk.push_str(head);
            walk
        }
    };
    Err(LoweringError {
        message: format!(
            "cyclic dependency among named sequences (LRM 16.8): {cycle} (slang reports \
             sequence `{reported}` recursive; {} such diagnostic(s) in this design)",
            diags
                .items()
                .iter()
                .filter(|d| d.is_error() && d.code_name() == RECURSIVE_SEQUENCE)
                .count()
        ),
        at: "sva::named::check_named_sequence_cycles".into(),
    })
}

/// The slang error codes that carry LRM 16.8/16.8.1's rules on formal and
/// actual arguments of a named sequence, each with the clause it enforces.
/// slang implements them while it binds the instance, so they are present in
/// `Design::diagnostics()` exactly when the design violates the rule; this
/// crate does not re-derive them.
const FORMAL_ARGUMENT_RULES: &[(&str, &str)] = &[
    (
        "UnboundedNotAllowed",
        "a `$` actual argument must bind an untyped formal argument whose every reference is \
         an upper bound of a delay/repetition range or itself an actual argument of another \
         named sequence instance (LRM 16.8.1)",
    ),
    (
        "ConstEvalNonConstVariable",
        "an actual argument bound to a formal that is used in a cycle delay or a repetition \
         bound must be an elaboration-time constant (LRM 16.8.1: delay_example)",
    ),
    (
        "EventExprAssertionArg",
        "an `event`-typed formal argument is bound to an event expression and referenced only \
         where an event expression is allowed (LRM 16.8.1)",
    ),
    (
        "SeqInstanceRepetition",
        "a goto/nonconsecutive repetition cannot be applied to a named sequence instance \
         (LRM 16.9.2)",
    ),
    (
        "AssertionDelayFormalType",
        "a typed formal argument used in a cycle delay or repetition bound must be `shortint`, \
         `int` or `longint` (LRM 16.8.1)",
    ),
    (
        "TooFewArguments",
        "an instance must supply an actual argument for every formal argument that has no \
         default (LRM 16.8)",
    ),
    (
        "AssertionArgTypeMismatch",
        "an actual argument bound to a typed formal argument must be cast compatible with the \
         formal's type (LRM 16.8.1 rule c)",
    ),
    (
        "InvalidSignalEventInSeq",
        "an event expression may be an actual argument only for an `event`-typed or untyped \
         formal that is used where an event expression is allowed, never for a `sequence` \
         formal (LRM 16.8.1 rule a)",
    ),
    // The rest are slang's generic argument-list codes: it raises them for
    // subroutine calls and ports as well, so the quoted callee in the message
    // says whether the offending list is a named sequence's.
    (
        "TooManyArguments",
        "an instance may not supply more actual arguments than the declaration has formal \
         arguments (LRM 16.8)",
    ),
    (
        "ArgDoesNotExist",
        "a named actual argument must name a formal argument of the declaration (LRM 16.8)",
    ),
    (
        "UnconnectedArg",
        "every formal argument without a default needs an actual argument, by position or by \
         name (LRM 16.8)",
    ),
    (
        "DuplicateArgAssignment",
        "a formal argument may be bound by only one actual argument (LRM 16.8)",
    ),
    (
        "ArgCannotBeEmpty",
        "an empty actual argument is legal only for a formal argument that has a default \
         (LRM 16.8)",
    ),
];

/// Rejects a design that violates LRM 16.8/16.8.1's rules on formal and actual
/// arguments of a named sequence -- the ones [`FORMAL_ARGUMENT_RULES`] lists.
/// The first violation is the error's subject; the count of all of them is
/// quoted.
///
/// This is the other half of the builder's own loudness: for the same inputs
/// the builder (`build::build_automaton`) refuses to fold a non-constant
/// bound too, but the diagnostic is what says WHICH LRM rule the design broke.
/// Callers must check this (or `diagnostics().has_errors()`) before trusting
/// an automaton: `Design::has_fatal_errors` stays false for all of them.
pub fn check_formal_argument_rules(diags: &Diagnostics) -> Result<(), LoweringError> {
    let violations: Vec<_> = diags
        .items()
        .iter()
        .filter(|d| d.is_error())
        .filter_map(|d| {
            FORMAL_ARGUMENT_RULES
                .iter()
                .find(|(code, _)| *code == d.code_name())
                .map(|(code, rule)| (d, *code, *rule))
        })
        .collect();
    let Some((first, code, rule)) = violations.first() else {
        return Ok(());
    };
    Err(LoweringError {
        message: format!(
            "illegal formal/actual argument of a named sequence: {rule} -- slang: {} ({code}; \
             {} such diagnostic(s) in this design)",
            first.message,
            violations.len()
        ),
        at: "sva::named::check_formal_argument_rules".into(),
    })
}

/// The text between the first pair of single quotes of `message`.
fn quoted_name(message: &str) -> Option<&str> {
    let start = message.find('\'')? + 1;
    let len = message[start..].find('\'')?;
    Some(&message[start..start + len])
}

/// The sequences on the expansion stack at the point slang detected the cycle
/// reported by the error whose message is `message`, outermost first: the
/// `note: while expanding sequence 'X'` lines slang attaches to that error in
/// `rendered`, reversed (slang prints the stack innermost first). Empty when
/// the error or its notes cannot be found, in which case the caller falls back
/// to naming the single reported sequence.
fn expansion_chain(rendered: &str, message: &str) -> Vec<String> {
    let mut lines = rendered.lines();
    let header = format!("error: {message}");
    if !lines.any(|l| l.contains(&header)) {
        return Vec::new();
    }
    let mut chain = Vec::new();
    for line in lines {
        // The next diagnostic of any severity other than a note ends this
        // error's block.
        if line.contains(": error: ") || line.contains(": warning: ") {
            break;
        }
        if let Some(pos) = line.find("note: while expanding sequence '")
            && let Some(name) = quoted_name(&line[pos..])
        {
            chain.push(name.to_string());
        }
    }
    chain.reverse();
    chain
}

#[cfg(test)]
mod tests {
    use super::*;
    use sv_lang::{Compilation, Session};

    /// Compiles a module whose body is `decls` and runs the cycle check over
    /// the compilation's own diagnostics.
    fn cycle_check(decls: &str) -> Result<(), LoweringError> {
        let src = format!(
            "module m;\n\
             logic sysclk, clk, a, b, c, x, y, z;\n\
             {decls}\n\
             endmodule\n"
        );
        let session = Session::new();
        let mut comp = Compilation::new(&session).unwrap();
        comp.add_source(&src).unwrap();
        let design = comp.compile().unwrap();
        check_named_sequence_cycles(&design.diagnostics())
    }

    /// 16.8's own illegal example, verbatim: `s1` instantiates `s2` and `s2`
    /// instantiates `s1`. The error must NAME the cycle (both members and the
    /// closing edge), not just say "recursive".
    #[test]
    fn cyclic_named_sequences_rejected_with_named_cycle() {
        let err = cycle_check(
            "sequence s1;\n\
                @(posedge sysclk) (x ##1 s2);\n\
             endsequence\n\
             sequence s2;\n\
                @(posedge sysclk) (y ##1 s1);\n\
             endsequence",
        )
        .expect_err("a cyclic dependency among named sequences must be rejected");
        let msg = err.to_string();
        assert!(
            msg.contains("cyclic dependency among named sequences"),
            "{msg}"
        );
        // The quoted cycle is a closed walk through both members.
        assert!(
            msg.contains("s1 -> s2 -> s1") || msg.contains("s2 -> s1 -> s2"),
            "the error must quote the cycle `s1 -> s2 -> s1`, got: {msg}"
        );
    }

    /// The LRM's edge rule (16.8) has a second kind of edge: "an instance of
    /// the first named sequence that instantiates the second named sequence
    /// within an actual argument". `s(s(a))` is therefore a self-edge.
    #[test]
    fn cycle_through_an_instance_inside_an_actual_argument_is_rejected() {
        let err = cycle_check(
            "sequence s(p); p ##1 b; endsequence\n\
             assert property (@(posedge sysclk) s(s(a)));",
        )
        .expect_err("s(s(a)) is a cyclic dependency under 16.8's actual-argument edge");
        let msg = err.to_string();
        assert!(msg.contains("s -> s"), "{msg}");
    }

    /// Pinned, named gap (see the module doc): the same `s(s(a))`, written
    /// inside ANOTHER sequence's declaration (`user`) rather than directly in
    /// the assertion, raises no slang diagnostic at all even when `user` is
    /// instantiated -- so [`check_named_sequence_cycles`] cannot see it. The
    /// automaton builder closes the gap itself (it refuses a named sequence
    /// already on its 16.8 dependency chain, see
    /// `build::tests::actual_argument_cycle_through_another_sequence_is_rejected`);
    /// this test exists so that a slang upgrade that starts reporting it is
    /// noticed and the gap removed from the module doc.
    #[test]
    fn actual_argument_cycle_inside_another_sequence_is_not_reported_by_slang_known_gap() {
        cycle_check(
            "sequence s(p); p ##1 b; endsequence\n\
             sequence user; s(s(a)); endsequence\n\
             assert property (@(posedge sysclk) user);",
        )
        .expect("slang 0.1.9 raises no RecursiveSequence for this shape");
    }

    /// 16.8's edge rule also counts "an instance within the declaration of a
    /// default actual argument": `s`'s default is `t`, and `t` instantiates
    /// `s`.
    #[test]
    fn cycle_through_a_default_actual_argument_is_rejected() {
        let err = cycle_check(
            "sequence s(p = t); p ##1 b; endsequence\n\
             sequence t; s ##1 c; endsequence",
        )
        .expect_err("a default-argument instance closing a loop is a cyclic dependency");
        let msg = err.to_string();
        assert!(
            msg.contains("s") && msg.contains("t") && msg.contains("->"),
            "{msg}"
        );
    }

    /// A cycle in a declaration nobody instantiates is still a cycle ("if,
    /// and only if, there is a cycle in the directed graph whose nodes are
    /// the named sequences").
    #[test]
    fn an_unused_cyclic_pair_is_still_rejected() {
        cycle_check(
            "sequence s1; @(posedge sysclk) (x ##1 s2); endsequence\n\
             sequence s2; @(posedge sysclk) (y ##1 s1); endsequence",
        )
        .expect_err("no instantiation of s1/s2 anywhere, still a cycle");
    }

    /// Compiles `decls` into module `m` and runs the formal-argument check.
    fn rules_check(decls: &str) -> Result<(), LoweringError> {
        let src = format!(
            "module m;\n\
             logic clk, a, b, x, y;\n\
             int zz;\n\
             {decls}\n\
             endmodule\n"
        );
        let session = Session::new();
        let mut comp = Compilation::new(&session).unwrap();
        comp.add_source(&src).unwrap();
        let design = comp.compile().unwrap();
        check_formal_argument_rules(&design.diagnostics())
    }

    /// Each rule of 16.8/16.8.1 that slang enforces is surfaced, with the rule
    /// named, and a design obeying all of them is accepted (so the check is
    /// not one that matches everything or nothing).
    #[test]
    fn formal_argument_rules_are_reported_with_their_clause() {
        let cases: &[(&str, &str, &str)] = &[
            (
                "sequence s(k, p); p ##[k:5] b; endsequence\n\
                 assert property (@(posedge clk) s($, a));",
                "`$`",
                "UnboundedNotAllowed",
            ),
            (
                "sequence s(k, p); p ##k b; endsequence\n\
                 assert property (@(posedge clk) s(zz, a));",
                "elaboration-time constant",
                "ConstEvalNonConstVariable",
            ),
            (
                "int n;\n\
                 sequence s(event ev, p); @(ev) p ##1 b; endsequence\n\
                 assert property (s(n, a));",
                "`event`-typed",
                "EventExprAssertionArg",
            ),
            (
                "sequence s(sequence q); q[->2]; endsequence\n\
                 assert property (@(posedge clk) s(a));",
                "goto/nonconsecutive",
                "SeqInstanceRepetition",
            ),
            (
                "sequence s(bit k, p); p ##k b; endsequence\n\
                 assert property (@(posedge clk) s(1, a));",
                "`shortint`",
                "AssertionDelayFormalType",
            ),
            (
                "sequence s(p, q); p ##1 q; endsequence\n\
                 assert property (@(posedge clk) s(a));",
                "every formal argument",
                "TooFewArguments",
            ),
            // 16.8.1 rule (c): not cast compatible with the typed formal.
            (
                "int arr[2];\n\
                 sequence s(int k, p); p ##1 (k == 1); endsequence\n\
                 assert property (@(posedge clk) s(arr, a));",
                "rule c",
                "AssertionArgTypeMismatch",
            ),
            // 16.8.1 rule (a): an event expression for a `sequence` formal.
            (
                "sequence s(sequence q); q; endsequence\n\
                 assert property (@(posedge clk) s(posedge clk));",
                "rule a",
                "InvalidSignalEventInSeq",
            ),
            (
                "sequence s(p, q); p ##1 q; endsequence\n\
                 assert property (@(posedge clk) s(a, b, x));",
                "more actual arguments",
                "TooManyArguments",
            ),
            (
                "sequence s(p, q); p ##1 q; endsequence\n\
                 assert property (@(posedge clk) s(.p(a), .q(b), .zzz(x)));",
                "must name a formal",
                "ArgDoesNotExist",
            ),
            (
                "sequence s(p, q); p ##1 q; endsequence\n\
                 assert property (@(posedge clk) s(.p(a)));",
                "by position or by name",
                "UnconnectedArg",
            ),
            (
                "sequence s(p, q); p ##1 q; endsequence\n\
                 assert property (@(posedge clk) s(.p(a), .q(b), .p(x)));",
                "only one actual",
                "DuplicateArgAssignment",
            ),
            (
                "sequence s(p, q); p ##1 q; endsequence\n\
                 assert property (@(posedge clk) s(, b));",
                "empty actual argument",
                "ArgCannotBeEmpty",
            ),
        ];
        for (decls, clause, code) in cases {
            let err = rules_check(decls).expect_err(decls);
            let msg = err.to_string();
            assert!(msg.contains(clause), "{code}: {msg}");
            assert!(msg.contains(code), "{code}: {msg}");
        }
    }

    /// The legal counterparts of every case above.
    #[test]
    fn legal_formal_arguments_are_accepted() {
        rules_check(
            "sequence s(max, int d, p); p ##d b ##[1:max] x; endsequence\n\
             sequence u(m2, p); s(m2, 2, p); endsequence\n\
             sequence t(event ev, untyped p); @(ev) p; endsequence\n\
             sequence r(p); p[*2]; endsequence\n\
             assert property (@(posedge clk) u($, a));\n\
             assert property (@(posedge clk) s(3, 1, a));\n\
             assert property (@(posedge clk) r(a)[*2]);\n\
             cover property (t(posedge clk, a));",
        )
        .expect("every rule of 16.8/16.8.1 is obeyed");
    }

    /// The same check must NOT fire on legal dependency shapes: a chain, a
    /// diamond (two sequences sharing one callee), and the LRM's own
    /// `rule`/`s` pair.
    #[test]
    fn acyclic_dependency_graphs_are_accepted() {
        cycle_check(
            "sequence s; a ##1 b ##1 c; endsequence\n\
             sequence rule; @(posedge sysclk) x ##1 y ##1 s ##1 z; endsequence\n\
             sequence left; s ##1 a; endsequence\n\
             sequence right; s ##2 b; endsequence\n\
             sequence top; left ##1 right; endsequence",
        )
        .expect("a chain and a diamond are acyclic");
    }
}