vj-sim 0.3.0

//! The assertion control system tasks' registry (LRM 1800-2023 §20.11:
//! `$assertcontrol` and the `$asserton`/`$assertoff`/`$assertkill`/
//! `$assertpasson`/... conveniences built on it).
//!
//! Every assertion the run can control is a *site*: a concurrent assertion
//! statement, a simple/deferred immediate assertion, an `expect`, or one of
//! the `unique`/`unique0`/`priority` violation checkers. A site is described by
//! its Table 20-5 `assertion_type` bit, its Table 20-6 `directive_type` bit
//! (0: the directive type is not checked -- it does not apply to `expect` and
//! violation reports), the hierarchical scope that holds it and its label (the
//! assertion's full hierarchical name; empty when it has none).
//!
//! The control tasks themselves are an append-only *log*. A site's state is
//! the fold of the matching entries over [`SiteState::DEFAULT`], applied lazily
//! the next time the site is asked about: the log order is the order the tasks
//! executed in, so a `$assertlock` makes every later entry that matches the
//! site a no-op until the matching unlock, exactly as §20.11 words it. A site
//! the control tasks never name costs one empty-log test.
//!
//! Only `$assertkill`-class entries need an immediate effect (they flush
//! queued reports and procedural instances of the sites they kill):
//! [`control`] returns those sites. Everything else is *polled*: the
//! assertion's executor reads its [`SiteState`] where it acts.

use std::cell::RefCell;
use std::collections::HashMap;

/// Table 20-5 `assertion_type` bits.
pub const ASSERT_CONCURRENT: u32 = 1;
pub const ASSERT_SIMPLE_IMMEDIATE: u32 = 2;
pub const ASSERT_OBSERVED_DEFERRED: u32 = 4;
pub const ASSERT_FINAL_DEFERRED: u32 = 8;
pub const ASSERT_EXPECT: u32 = 16;
pub const ASSERT_UNIQUE: u32 = 32;
pub const ASSERT_UNIQUE0: u32 = 64;
pub const ASSERT_PRIORITY: u32 = 128;
/// The violation report types (`unique`/`unique0`/`priority`).
pub const ASSERT_VIOLATION: u32 = ASSERT_UNIQUE | ASSERT_UNIQUE0 | ASSERT_PRIORITY;
/// `assertion_type` default of `$assertcontrol` (every type).
pub const ASSERT_ALL: u32 = 255;

/// Table 20-6 `directive_type` bits.
pub const DIR_ASSERT: u32 = 1;
pub const DIR_COVER: u32 = 2;
pub const DIR_ASSUME: u32 = 4;
/// `directive_type` default of `$assertcontrol` (every directive).
pub const DIR_ALL: u32 = 7;

/// [`SiteState::query_bits`]: reporting on, nonvacuous pass action on, vacuous
/// pass action on, fail action on.
pub const Q_CHECKING: u32 = 1;
pub const Q_PASS_NONVACUOUS: u32 = 2;
pub const Q_PASS_VACUOUS: u32 = 4;
pub const Q_FAIL: u32 = 8;
/// Every query bit set: no control task has touched the site.
pub const Q_ALL: u32 = Q_CHECKING | Q_PASS_NONVACUOUS | Q_PASS_VACUOUS | Q_FAIL;

/// The term an `expect`'s blocked process is resumed with when its property was
/// decided but the control tasks switched off the action that would run (0: the
/// pass statement, 1: the `else` statement).
pub const EXPECT_NO_ACTION_TERM: i64 = 2;

/// A registry index of one site.
pub type SiteId = u32;

/// `control_type` values of Table 20-5.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub enum Control {
    Lock,
    Unlock,
    On,
    Off,
    Kill,
    PassOn,
    PassOff,
    FailOn,
    FailOff,
    NonvacuousOn,
    VacuousOff,
}

impl Control {
    /// The `control_type` value `n` names, `None` for anything outside 1..=11
    /// (LRM: an illegal value is an error).
    pub const fn from_value(n: i64) -> Option<Control> {
        Some(match n {
            1 => Control::Lock,
            2 => Control::Unlock,
            3 => Control::On,
            4 => Control::Off,
            5 => Control::Kill,
            6 => Control::PassOn,
            7 => Control::PassOff,
            8 => Control::FailOn,
            9 => Control::FailOff,
            10 => Control::NonvacuousOn,
            11 => Control::VacuousOff,
            _ => return None,
        })
    }
}

/// What one site is, as the registry sees it.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct SiteDesc {
    /// Exactly one `ASSERT_*` bit.
    pub assertion_type: u32,
    /// Exactly one `DIR_*` bit, or 0: not checked.
    pub directive_type: u32,
    /// The hierarchical scope holding the site.
    pub scope: String,
    /// The assertion's full hierarchical name; empty when unlabeled (a
    /// statement-level site then carries `#<source offset>`, which tells the
    /// unlabeled assertions of one scope apart).
    pub label: String,
}

impl SiteDesc {
    /// The text compiled code carries for the site (`sv_rt_assert_ctl`'s query).
    pub fn encode(&self) -> String {
        format!(
            "{}|{}|{}|{}",
            self.assertion_type, self.directive_type, self.scope, self.label
        )
    }

    /// The inverse of [`SiteDesc::encode`].
    pub fn parse(text: &str) -> Result<SiteDesc, String> {
        let mut parts = text.splitn(4, '|');
        let (Some(a), Some(d), Some(scope), Some(label)) =
            (parts.next(), parts.next(), parts.next(), parts.next())
        else {
            return Err(format!("assertion site descriptor `{text}` is malformed"));
        };
        let num = |s: &str| {
            s.parse::<u32>()
                .map_err(|_| format!("assertion site descriptor `{text}` is malformed"))
        };
        Ok(SiteDesc {
            assertion_type: num(a)?,
            directive_type: num(d)?,
            scope: scope.to_string(),
            label: label.to_string(),
        })
    }
}

/// One executed control task.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Op {
    pub control: Control,
    /// OR of `ASSERT_*` bits.
    pub assertion_type: u32,
    /// OR of `DIR_*` bits.
    pub directive_type: u32,
    /// Scope depth below each named scope the task reaches; `<= 0`: all.
    pub levels: i64,
    /// The named scopes and assertions (hierarchical paths); empty: the whole
    /// design.
    pub targets: Vec<String>,
}

/// A site's control state.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct SiteState {
    /// `$assertlock`ed: every control task but unlock is ignored.
    pub locked: bool,
    /// New attempts start / new reports are made (`$asserton`), as opposed to
    /// `$assertoff`/`$assertkill`.
    pub checking: bool,
    /// The pass action of a nonvacuous success runs.
    pub pass_nonvacuous: bool,
    /// The pass action of a vacuous success runs.
    pub pass_vacuous: bool,
    /// The fail action (the default `$error` included) runs.
    pub fail: bool,
    /// How many `$assertkill`s have reached the site.
    pub kills: u64,
}

impl SiteState {
    pub const DEFAULT: SiteState = SiteState {
        locked: false,
        checking: true,
        pass_nonvacuous: true,
        pass_vacuous: true,
        fail: true,
        kills: 0,
    };

    /// The `Q_*` bits of this state.
    pub fn query_bits(&self) -> u32 {
        let mut bits = 0;
        if self.checking {
            bits |= Q_CHECKING;
        }
        if self.pass_nonvacuous {
            bits |= Q_PASS_NONVACUOUS;
        }
        if self.pass_vacuous {
            bits |= Q_PASS_VACUOUS;
        }
        if self.fail {
            bits |= Q_FAIL;
        }
        bits
    }
}

/// The target text naming the unlabeled assertion at source `offset` in the
/// instance `scope` (`vpi_control` on an unnamed assertion, 39.5).
pub fn anonymous_target(scope: &str, offset: u64) -> String {
    format!("#{offset}@{scope}")
}

/// Path components of a hierarchical name.
fn depth(path: &str) -> usize {
    if path.is_empty() {
        0
    } else {
        path.split('.').count()
    }
}

/// Whether `target` (one name of the task's list) reaches `desc` within
/// `levels`: it names the assertion itself, or a scope the assertion sits in at
/// most `levels` scopes below (1: the named scope's own assertions; `<= 0`: no
/// limit).
fn target_reaches(target: &str, levels: i64, desc: &SiteDesc) -> bool {
    if let Some(anon) = target.strip_prefix('#') {
        // `#<offset>@<scope>` (`anonymous_target`): one unlabeled assertion.
        let Some((offset, scope)) = anon.split_once('@') else {
            return false;
        };
        return desc.label.strip_prefix('#') == Some(offset)
            && (desc.scope == scope
                || (desc.scope.starts_with(scope) && desc.scope[scope.len()..].starts_with('.')));
    }
    if !desc.label.is_empty() && desc.label == target {
        return true;
    }
    let inside = desc.scope == target
        || (desc.scope.starts_with(target) && desc.scope[target.len()..].starts_with('.'));
    if !inside {
        return false;
    }
    let below = (depth(&desc.scope) - depth(target) + 1) as i64;
    levels <= 0 || below <= levels
}

/// Whether `op` applies to the site `desc` (before the lock is considered).
fn op_reaches(op: &Op, desc: &SiteDesc) -> bool {
    if op.assertion_type & desc.assertion_type == 0 {
        return false;
    }
    if desc.directive_type != 0 && op.directive_type & desc.directive_type == 0 {
        return false;
    }
    if op.targets.is_empty() {
        // The whole design: the top modules are the first scope level.
        let below = depth(&desc.scope) as i64;
        return op.levels <= 0 || below <= op.levels;
    }
    op.targets
        .iter()
        .any(|t| target_reaches(t, op.levels, desc))
}

/// `state` after `op`, for the site `desc`.
fn fold(mut state: SiteState, desc: &SiteDesc, op: &Op) -> SiteState {
    if !op_reaches(op, desc) {
        return state;
    }
    match op.control {
        Control::Lock => state.locked = true,
        Control::Unlock => state.locked = false,
        _ if state.locked => {}
        Control::On | Control::Off | Control::Kill => {
            // §20.11: these do not affect `expect`.
            if desc.assertion_type == ASSERT_EXPECT {
                return state;
            }
            state.checking = op.control == Control::On;
            if op.control == Control::Kill {
                state.kills += 1;
            }
        }
        Control::PassOn
        | Control::PassOff
        | Control::FailOn
        | Control::FailOff
        | Control::NonvacuousOn
        | Control::VacuousOff => {
            // §20.11: the action controls affect neither the violation report
            // types nor statistics counters.
            if desc.assertion_type & ASSERT_VIOLATION != 0 {
                return state;
            }
            match op.control {
                Control::PassOn => {
                    state.pass_nonvacuous = true;
                    state.pass_vacuous = true;
                }
                Control::PassOff => {
                    state.pass_nonvacuous = false;
                    state.pass_vacuous = false;
                }
                Control::FailOn => state.fail = true,
                Control::FailOff => state.fail = false,
                Control::NonvacuousOn => state.pass_nonvacuous = true,
                Control::VacuousOff => state.pass_vacuous = false,
                Control::Lock | Control::Unlock | Control::On | Control::Off | Control::Kill => {}
            }
        }
    }
    state
}

struct Site {
    desc: SiteDesc,
    state: SiteState,
    /// How much of the log `state` already folds.
    applied: usize,
}

#[derive(Default)]
struct Registry {
    log: Vec<Op>,
    sites: Vec<Site>,
    by_text: HashMap<String, SiteId>,
}

impl Registry {
    fn sync(&mut self, id: SiteId) -> SiteState {
        let Registry { log, sites, .. } = self;
        let site = &mut sites[id as usize];
        while site.applied < log.len() {
            site.state = fold(site.state, &site.desc, &log[site.applied]);
            site.applied += 1;
        }
        site.state
    }
}

thread_local! {
    static REGISTRY: RefCell<Registry> = RefCell::new(Registry::default());
}

/// Forgets every site and control task (the start of a run).
pub fn reset() {
    REGISTRY.with(|r| *r.borrow_mut() = Registry::default());
}

/// The id of the site `desc`, registering it the first time. Two descriptors
/// that are equal are one site.
pub fn intern(desc: SiteDesc) -> SiteId {
    let text = desc.encode();
    REGISTRY.with(|r| {
        let mut r = r.borrow_mut();
        if let Some(&id) = r.by_text.get(&text) {
            return id;
        }
        let id = r.sites.len() as SiteId;
        r.sites.push(Site {
            desc,
            state: SiteState::DEFAULT,
            applied: 0,
        });
        r.by_text.insert(text, id);
        id
    })
}

/// The id of the site whose [`SiteDesc::encode`] text is `text`.
pub fn intern_text(text: &str) -> Result<SiteId, String> {
    let known = REGISTRY.with(|r| r.borrow().by_text.get(text).copied());
    match known {
        Some(id) => Ok(id),
        None => Ok(intern(SiteDesc::parse(text)?)),
    }
}

/// The current state of the site `id`.
pub fn state(id: SiteId) -> SiteState {
    REGISTRY.with(|r| r.borrow_mut().sync(id))
}

/// The `Q_*` bits of the site `text` names: [`Q_ALL`] without touching the
/// registry while no control task has run.
pub fn query_text(text: &str) -> Result<u32, String> {
    if REGISTRY.with(|r| r.borrow().log.is_empty()) {
        return Ok(Q_ALL);
    }
    Ok(state(intern_text(text)?).query_bits())
}

/// A change a control task made to one site's state, as the VPI assertion
/// callbacks report it (IEEE 1800-2023 39.4.2).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum ControlEvent {
    Lock,
    Unlock,
    Disable,
    Enable,
    Kill,
    PassOn,
    PassOff,
    FailOn,
    FailOff,
    NonvacuousOn,
    VacuousOff,
}

/// The function told of every site state change a control task makes.
pub type ControlObserver = fn(SiteId, ControlEvent);

thread_local! {
    static OBSERVER: std::cell::Cell<Option<ControlObserver>> =
        const { std::cell::Cell::new(None) };
}

/// Installs (or removes) the function told of every site state change a
/// control task makes, after the registry is released.
pub fn set_control_observer(f: Option<ControlObserver>) {
    OBSERVER.with(|o| o.set(f));
}

/// The events of the change `a` -> `b` of one site's state.
fn changes(a: SiteState, b: SiteState) -> Vec<ControlEvent> {
    let mut out = Vec::new();
    if a.locked != b.locked {
        out.push(if b.locked {
            ControlEvent::Lock
        } else {
            ControlEvent::Unlock
        });
    }
    if b.kills != a.kills {
        out.push(ControlEvent::Kill);
    } else if a.checking != b.checking {
        out.push(if b.checking {
            ControlEvent::Enable
        } else {
            ControlEvent::Disable
        });
    }
    match (
        a.pass_nonvacuous != b.pass_nonvacuous,
        a.pass_vacuous != b.pass_vacuous,
    ) {
        (true, true) => out.push(if b.pass_nonvacuous {
            ControlEvent::PassOn
        } else {
            ControlEvent::PassOff
        }),
        (true, false) if b.pass_nonvacuous => out.push(ControlEvent::NonvacuousOn),
        (false, true) if !b.pass_vacuous => out.push(ControlEvent::VacuousOff),
        // The other halves: reported with the closest action event.
        (true, false) => out.push(ControlEvent::PassOff),
        (false, true) => out.push(ControlEvent::PassOn),
        (false, false) => {}
    }
    if a.fail != b.fail {
        out.push(if b.fail {
            ControlEvent::FailOn
        } else {
            ControlEvent::FailOff
        });
    }
    out
}

/// Executes a control task. Returns the registered sites an `$assertkill` (or an
/// `$assertcontrol` Kill) just reached: the caller flushes what they have queued.
/// The control observer ([`set_control_observer`]) is told of every change.
pub fn control(op: Op) -> Vec<SiteId> {
    let (killed, events) = REGISTRY.with(|r| {
        let mut r = r.borrow_mut();
        let ids: Vec<SiteId> = (0..r.sites.len() as SiteId).collect();
        let before: Vec<SiteState> = ids.iter().map(|&id| r.sync(id)).collect();
        r.log.push(op);
        let mut killed = Vec::new();
        let mut events = Vec::new();
        for (&id, b) in ids.iter().zip(before) {
            let a = r.sync(id);
            if a.kills != b.kills {
                killed.push(id);
            }
            events.extend(changes(b, a).into_iter().map(|e| (id, e)));
        }
        (killed, events)
    });
    if let Some(f) = OBSERVER.with(|o| o.get()) {
        for (id, e) in events {
            f(id, e);
        }
    }
    killed
}

/// Executes a control task and carries out its immediate effects: the queued
/// deferred reports, queued violation reports and pending procedural assertion
/// instances of every site an `$assertkill` reached are discarded (20.11).
/// Executing attempts are aborted by their runners, which notice the kill count
/// ([`SiteState::kills`]) change the next time they run.
pub fn execute(op: Op) {
    let killed = control(op);
    if !killed.is_empty() {
        crate::sched::maturation::flush_sites(&killed);
        crate::sched::proc_assert::clear_sites(&killed);
    }
}

/// `sv_rt_assert_ctl`'s `op` for an assertion control task.
pub const CTL_OP_CONTROL: u32 = 0;
/// `sv_rt_assert_ctl`'s `op` for the state query of one site.
pub const CTL_OP_QUERY: u32 = 1;

/// `u64 sv_rt_assert_ctl(u32 op, i64 a0, i64 a1, i64 a2, i64 a3, ptr text)`, the
/// one entry point compiled code reaches the registry through.
///
/// * [`CTL_OP_CONTROL`]: the control task `a0` (`control_type`) over the
///   assertion types `a1`, directive types `a2` and `a3` levels, on the
///   newline-separated hierarchical names in `text` (empty: the whole design).
///   An illegal `control_type` is ignored with a warning on stderr (the LRM calls
///   it an error; it cannot unwind out of compiled code). Returns 0.
/// * [`CTL_OP_QUERY`]: the `Q_*` bits of the site whose descriptor is `text`.
///
/// # Safety
/// `text` is a valid NUL-terminated C string, or null (then empty).
#[cfg_attr(feature = "aot-exports", unsafe(export_name = "sv_rt_assert_ctl"))]
pub unsafe extern "C" fn real_sv_rt_assert_ctl(
    op: u32,
    a0: i64,
    a1: i64,
    a2: i64,
    a3: i64,
    text: *const std::ffi::c_char,
) -> u64 {
    let text = if text.is_null() {
        std::borrow::Cow::Borrowed("")
    } else {
        // SAFETY: the caller's contract.
        unsafe { std::ffi::CStr::from_ptr(text) }.to_string_lossy()
    };
    match op {
        CTL_OP_CONTROL => {
            let Some(control) = Control::from_value(a0) else {
                eprintln!("vj: warning: $assertcontrol: illegal control_type {a0}; ignored");
                return 0;
            };
            execute(Op {
                control,
                assertion_type: (a1 & 0xFF) as u32,
                directive_type: (a2 & 0x7) as u32,
                levels: a3,
                targets: text
                    .split('\n')
                    .filter(|t| !t.is_empty())
                    .map(str::to_string)
                    .collect(),
            });
            0
        }
        CTL_OP_QUERY => match query_text(&text) {
            Ok(bits) => u64::from(bits),
            Err(why) => {
                eprintln!("vj: internal error: {why}");
                u64::from(Q_ALL)
            }
        },
        _ => {
            eprintln!("vj: internal error: sv_rt_assert_ctl: unknown op {op}");
            0
        }
    }
}

/// The descriptor the site `id` was registered with.
pub fn site_desc(id: SiteId) -> SiteDesc {
    REGISTRY.with(|r| r.borrow().sites[id as usize].desc.clone())
}

#[cfg(test)]
mod tests {
    use super::*;

    fn desc(ty: u32, dir: u32, scope: &str, label: &str) -> SiteDesc {
        SiteDesc {
            assertion_type: ty,
            directive_type: dir,
            scope: scope.into(),
            label: label.into(),
        }
    }

    fn op(control: Control, ty: u32, dir: u32, levels: i64, targets: &[&str]) -> Op {
        Op {
            control,
            assertion_type: ty,
            directive_type: dir,
            levels,
            targets: targets.iter().map(|s| s.to_string()).collect(),
        }
    }

    fn conc(scope: &str, label: &str) -> SiteId {
        intern(desc(ASSERT_CONCURRENT, DIR_ASSERT, scope, label))
    }

    #[test]
    fn site_descriptor_round_trips_and_rejects_garbage() {
        let d = desc(ASSERT_CONCURRENT, DIR_COVER, "top.u1", "top.u1.c1");
        assert_eq!(SiteDesc::parse(&d.encode()), Ok(d));
        let unlabeled = desc(ASSERT_UNIQUE, 0, "top.chk", "");
        assert_eq!(SiteDesc::parse(&unlabeled.encode()), Ok(unlabeled));
        assert!(SiteDesc::parse("1|2|top").is_err());
        assert!(SiteDesc::parse("x|2|top|a").is_err());
    }

    #[test]
    fn control_types_one_to_eleven_are_named_and_the_rest_are_not() {
        let all = [
            Control::Lock,
            Control::Unlock,
            Control::On,
            Control::Off,
            Control::Kill,
            Control::PassOn,
            Control::PassOff,
            Control::FailOn,
            Control::FailOff,
            Control::NonvacuousOn,
            Control::VacuousOff,
        ];
        for (i, c) in all.iter().enumerate() {
            assert_eq!(Control::from_value(i as i64 + 1), Some(*c));
        }
        assert_eq!(Control::from_value(0), None);
        assert_eq!(Control::from_value(12), None);
        assert_eq!(Control::from_value(-1), None);
    }

    #[test]
    fn an_untouched_site_has_every_action_enabled_without_registering() {
        reset();
        assert_eq!(
            query_text("1|1|top|top.a").unwrap(),
            Q_ALL,
            "an empty log answers the default"
        );
        let id = conc("top", "top.a");
        assert_eq!(state(id), SiteState::DEFAULT);
    }

    #[test]
    fn off_then_on_toggles_new_attempts() {
        reset();
        let id = conc("top", "top.a");
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 0, &[]));
        assert!(!state(id).checking);
        control(op(Control::On, ASSERT_ALL, DIR_ALL, 0, &[]));
        assert!(state(id).checking);
        assert_eq!(state(id).kills, 0);
    }

    #[test]
    fn levels_count_scopes_below_the_named_one() {
        reset();
        let top = conc("top", "top.a");
        let u1 = conc("top.u1", "top.u1.a");
        let deep = conc("top.u1.v", "top.u1.v.a");
        // Level 1: only the named scope's own assertions.
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 1, &["top"]));
        assert!(!state(top).checking);
        assert!(state(u1).checking);
        assert!(state(deep).checking);
        control(op(Control::On, ASSERT_ALL, DIR_ALL, 0, &[]));
        // Level 2: one scope deeper as well.
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 2, &["top"]));
        assert!(!state(top).checking);
        assert!(!state(u1).checking);
        assert!(state(deep).checking);
        control(op(Control::On, ASSERT_ALL, DIR_ALL, 0, &[]));
        // Level 0: all of them.
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 0, &["top"]));
        assert!(!state(deep).checking);
    }

    #[test]
    fn a_scope_name_matches_whole_path_components_only() {
        reset();
        let a = conc("top.u1", "top.u1.a");
        let b = conc("top.u10", "top.u10.a");
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 0, &["top.u1"]));
        assert!(!state(a).checking);
        assert!(state(b).checking, "`top.u1` is not a prefix of `top.u10`");
    }

    #[test]
    fn a_label_target_names_one_assertion_and_ignores_levels() {
        reset();
        let a = conc("top", "top.a");
        let b = conc("top", "top.b");
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 1, &["top.a"]));
        assert!(!state(a).checking);
        assert!(state(b).checking);
    }

    #[test]
    fn no_target_with_levels_counts_the_top_modules_as_level_one() {
        reset();
        let top = conc("top", "top.a");
        let u1 = conc("top.u1", "top.u1.a");
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 1, &[]));
        assert!(!state(top).checking);
        assert!(state(u1).checking);
    }

    #[test]
    fn assertion_and_directive_types_filter_the_sites() {
        reset();
        let assert_c = intern(desc(ASSERT_CONCURRENT, DIR_ASSERT, "top", "top.a"));
        let cover_c = intern(desc(ASSERT_CONCURRENT, DIR_COVER, "top", "top.c"));
        let assume_c = intern(desc(ASSERT_CONCURRENT, DIR_ASSUME, "top", "top.m"));
        let assert_i = intern(desc(ASSERT_SIMPLE_IMMEDIATE, DIR_ASSERT, "top", "top.i"));
        control(op(Control::Kill, ASSERT_CONCURRENT, DIR_ASSERT, 0, &[]));
        assert!(!state(assert_c).checking);
        assert!(state(cover_c).checking, "a cover is not an assert");
        assert!(state(assume_c).checking);
        assert!(state(assert_i).checking, "an immediate is not concurrent");
    }

    #[test]
    fn lock_ignores_later_controls_until_unlock_and_unlock_always_applies() {
        reset();
        let a = conc("top", "top.a");
        let b = conc("top", "top.b");
        control(op(Control::Lock, ASSERT_ALL, DIR_ALL, 0, &["top.a"]));
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 0, &[]));
        assert!(state(a).checking, "locked: unaffected");
        assert!(!state(b).checking);
        control(op(Control::FailOff, ASSERT_ALL, DIR_ALL, 0, &[]));
        assert!(state(a).fail);
        assert!(!state(b).fail);
        control(op(Control::Unlock, ASSERT_ALL, DIR_ALL, 0, &["top.a"]));
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 0, &[]));
        assert!(!state(a).checking, "unlocked: affected again");
    }

    #[test]
    fn a_lock_reaches_a_site_registered_after_it() {
        reset();
        control(op(Control::Lock, ASSERT_ALL, DIR_ALL, 0, &["top.late"]));
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 0, &[]));
        let late = conc("top", "top.late");
        assert!(state(late).checking);
    }

    #[test]
    fn kill_reports_the_sites_it_reached_and_counts_per_site() {
        reset();
        let a = conc("top", "top.a");
        let b = conc("top", "top.b");
        let killed = control(op(Control::Kill, ASSERT_ALL, DIR_ALL, 0, &["top.a"]));
        assert_eq!(killed, vec![a]);
        assert_eq!(state(a).kills, 1);
        assert_eq!(state(b).kills, 0);
        assert!(!state(a).checking);
        // A locked site is not reached, so nothing is flushed for it.
        control(op(Control::Lock, ASSERT_ALL, DIR_ALL, 0, &["top.b"]));
        assert!(control(op(Control::Kill, ASSERT_ALL, DIR_ALL, 0, &["top.b"])).is_empty());
        // Off is not a kill.
        assert!(control(op(Control::Off, ASSERT_ALL, DIR_ALL, 0, &["top.a"])).is_empty());
    }

    #[test]
    fn expect_ignores_on_off_kill_but_takes_the_action_controls() {
        reset();
        let e = intern(desc(ASSERT_EXPECT, 0, "top", ""));
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 0, &[]));
        assert!(control(op(Control::Kill, ASSERT_ALL, DIR_ALL, 0, &[])).is_empty());
        assert!(state(e).checking);
        control(op(Control::FailOff, ASSERT_ALL, DIR_ALL, 0, &[]));
        assert!(!state(e).fail);
    }

    #[test]
    fn expect_and_violation_sites_ignore_the_directive_filter() {
        reset();
        let e = intern(desc(ASSERT_EXPECT, 0, "top", ""));
        let u = intern(desc(ASSERT_UNIQUE, 0, "top.chk", ""));
        control(op(Control::FailOff, ASSERT_EXPECT, DIR_COVER, 0, &[]));
        assert!(
            !state(e).fail,
            "directive_type is checked only for assertions"
        );
        control(op(Control::Off, ASSERT_UNIQUE, DIR_COVER, 0, &[]));
        assert!(!state(u).checking);
    }

    #[test]
    fn violation_sites_ignore_the_action_controls_but_take_on_off_kill() {
        reset();
        let u = intern(desc(ASSERT_UNIQUE, 0, "top", ""));
        let p = intern(desc(ASSERT_PRIORITY, 0, "top", ""));
        control(op(Control::PassOff, ASSERT_ALL, DIR_ALL, 0, &[]));
        control(op(Control::FailOff, ASSERT_ALL, DIR_ALL, 0, &[]));
        assert_eq!(state(u), SiteState::DEFAULT);
        assert_eq!(state(p), SiteState::DEFAULT);
        control(op(Control::Off, ASSERT_ALL, DIR_ALL, 0, &[]));
        assert!(!state(u).checking && !state(p).checking);
        // `On` for the concurrent/immediate types alone does not re-enable them.
        control(op(
            Control::On,
            ASSERT_CONCURRENT | ASSERT_SIMPLE_IMMEDIATE | ASSERT_OBSERVED_DEFERRED,
            DIR_ALL,
            0,
            &[],
        ));
        assert!(!state(u).checking);
        control(op(
            Control::On,
            ASSERT_UNIQUE | ASSERT_UNIQUE0 | ASSERT_PRIORITY,
            DIR_ALL,
            0,
            &[],
        ));
        assert!(state(u).checking && state(p).checking);
    }

    #[test]
    fn the_six_action_controls_set_their_own_flags() {
        reset();
        let a = conc("top", "top.a");
        let all = |c| control(op(c, ASSERT_ALL, DIR_ALL, 0, &[]));
        all(Control::PassOff);
        assert_eq!(state(a).query_bits(), Q_CHECKING | Q_FAIL);
        all(Control::NonvacuousOn);
        assert_eq!(
            state(a).query_bits(),
            Q_CHECKING | Q_FAIL | Q_PASS_NONVACUOUS
        );
        all(Control::PassOn);
        assert_eq!(state(a).query_bits(), Q_ALL);
        all(Control::VacuousOff);
        assert_eq!(state(a).query_bits(), Q_ALL & !Q_PASS_VACUOUS);
        all(Control::FailOff);
        assert_eq!(
            state(a).query_bits(),
            Q_CHECKING | Q_PASS_NONVACUOUS,
            "vacuous pass and fail are off"
        );
        all(Control::FailOn);
        assert_eq!(
            state(a).query_bits(),
            Q_CHECKING | Q_PASS_NONVACUOUS | Q_FAIL
        );
        assert_eq!(state(a).kills, 0, "action controls are not kills");
    }

    /// 20.11: with the assertion off no procedural instance is queued; Kill also
    /// empties what is queued; On queues again. Other assertions' instances are
    /// not touched.
    #[test]
    fn off_stops_procedural_instances_being_queued_and_kill_flushes_the_queue() {
        use crate::sched::proc_assert;
        reset();
        proc_assert::reset();
        let a = conc("top", "top.a");
        let b = conc("top", "top.b");
        proc_assert::register_site(0, a);
        proc_assert::register_site(1, b);
        let queue =
            |key: i64| unsafe { proc_assert::real_sv_rt_proc_assert(key, std::ptr::null(), 0) };
        queue(0);
        queue(1);
        execute(op(Control::Off, ASSERT_ALL, DIR_ALL, 0, &["top.a"]));
        queue(0);
        assert_eq!(
            proc_assert::drain().len(),
            2,
            "off: the pending ones stay, no new one"
        );
        queue(0);
        queue(1);
        execute(op(Control::On, ASSERT_ALL, DIR_ALL, 0, &["top.a"]));
        queue(0);
        execute(op(Control::Kill, ASSERT_ALL, DIR_ALL, 0, &["top.a"]));
        let rest = proc_assert::drain();
        assert_eq!(
            rest.iter().map(|e| e.key).collect::<Vec<_>>(),
            vec![1],
            "kill flushed the pending instances of a, not b's"
        );
        // After the kill `a` is off until an On: a new instance is not queued.
        queue(0);
        assert!(proc_assert::drain().is_empty());
        execute(op(Control::On, ASSERT_ALL, DIR_ALL, 0, &["top.a"]));
        queue(0);
        assert_eq!(proc_assert::drain().len(), 1);
        proc_assert::reset();
    }

    /// The compiled-code entry point: control, then query, through C strings; an
    /// illegal `control_type` changes nothing.
    #[test]
    fn the_runtime_entry_point_controls_and_queries() {
        use std::ffi::CString;
        reset();
        let site = desc(ASSERT_CONCURRENT, DIR_ASSERT, "top.u1", "top.u1.a").encode();
        let site = CString::new(site).unwrap();
        let ctl = |op: u32, a: [i64; 4], text: &str| {
            let text = CString::new(text).unwrap();
            // SAFETY: `text` is a NUL-terminated C string.
            unsafe { real_sv_rt_assert_ctl(op, a[0], a[1], a[2], a[3], text.as_ptr()) }
        };
        let q = || unsafe { real_sv_rt_assert_ctl(CTL_OP_QUERY, 0, 0, 0, 0, site.as_ptr()) };
        assert_eq!(q(), u64::from(Q_ALL));
        ctl(CTL_OP_CONTROL, [4, 255, 7, 0], "top.u1\ntop.u2");
        assert_eq!(q(), u64::from(Q_ALL & !Q_CHECKING));
        ctl(CTL_OP_CONTROL, [0, 255, 7, 0], "");
        ctl(CTL_OP_CONTROL, [12, 255, 7, 0], "");
        assert_eq!(q(), u64::from(Q_ALL & !Q_CHECKING), "illegal types ignored");
        ctl(CTL_OP_CONTROL, [3, 255, 7, 0], "");
        assert_eq!(q(), u64::from(Q_ALL));
    }

    #[test]
    fn query_text_reads_the_state_of_the_named_site() {
        reset();
        let d = desc(ASSERT_SIMPLE_IMMEDIATE, DIR_ASSERT, "top", "top.i");
        control(op(
            Control::Off,
            ASSERT_SIMPLE_IMMEDIATE,
            DIR_ASSERT,
            0,
            &[],
        ));
        assert_eq!(query_text(&d.encode()).unwrap(), Q_ALL & !Q_CHECKING);
        let other = desc(ASSERT_CONCURRENT, DIR_ASSERT, "top", "top.c");
        assert_eq!(query_text(&other.encode()).unwrap(), Q_ALL);
        assert!(query_text("garbage").is_err());
    }
}