vj-sim 0.3.0

//! The design image's codec for a compiled property ([`PropertyIr`]).
//!
//! `vj build-aot` embeds each assertion's automaton and operator DAG in the
//! `.so` so the slang-free runner can drive the same
//! [`Engine`](super::engine::Engine) `vj run` does. The format is
//! hand-written, little-endian, built on the image's [`Writer`]/[`Reader`], and
//! lives beside the types it encodes: every `put_*` destructures its value
//! exhaustively (no `..`, no wildcard arm), so a field or variant added to the
//! IR without a codec update fails to compile instead of silently dropping out
//! of a built image.

use super::ir::{
    AbortMode, ActionId, Automaton, CallArg, CallId, ClockId, Edge, EndMethod, EndPoint,
    EndPointId, FirstMatchId, LeafId, LocalVarDecl, LocalVarId, State, ThreadStateId, Transition,
};
use super::property::{
    CaseArm, DeclId, NvRule, Prop, PropDecl, PropId, PropertyIr, SeqRef, Strength,
};
use crate::image::codec::{ImageError, Reader, Writer};

fn bad(what: &'static str, tag: u8) -> ImageError {
    ImageError::BadTag { what, tag }
}

fn put_opt_u32(w: &mut Writer, v: Option<u32>) {
    match v {
        None => w.u8(0),
        Some(x) => {
            w.u8(1);
            w.u32(x);
        }
    }
}

fn get_opt_u32(r: &mut Reader<'_>, what: &'static str) -> Result<Option<u32>, ImageError> {
    match r.u8()? {
        0 => Ok(None),
        1 => Ok(Some(r.u32()?)),
        tag => Err(bad(what, tag)),
    }
}

fn put_leaf_pairs(w: &mut Writer, v: &[(LocalVarId, LeafId)]) {
    w.len(v.len());
    for (var, leaf) in v {
        w.u32(var.0);
        w.u32(leaf.0);
    }
}

fn get_leaf_pairs(r: &mut Reader<'_>) -> Result<Vec<(LocalVarId, LeafId)>, ImageError> {
    let n = r.len()?;
    (0..n)
        .map(|_| Ok((LocalVarId(r.u32()?), LeafId(r.u32()?))))
        .collect()
}

fn put_abort_mode(w: &mut Writer, m: AbortMode) {
    w.u8(match m {
        AbortMode::Accept => 0,
        AbortMode::Reject => 1,
        AbortMode::SyncAccept => 2,
        AbortMode::SyncReject => 3,
    });
}

fn get_abort_mode(r: &mut Reader<'_>) -> Result<AbortMode, ImageError> {
    Ok(match r.u8()? {
        0 => AbortMode::Accept,
        1 => AbortMode::Reject,
        2 => AbortMode::SyncAccept,
        3 => AbortMode::SyncReject,
        tag => return Err(bad("abort mode", tag)),
    })
}

fn put_transition(w: &mut Writer, t: &Transition) {
    match t {
        Transition::Delay { min, max } => {
            w.u8(0);
            w.u32(*min);
            put_opt_u32(w, *max);
        }
        Transition::Epsilon => w.u8(1),
        Transition::Abort { leaf, mode } => {
            w.u8(2);
            w.u32(leaf.0);
            put_abort_mode(w, *mode);
        }
        Transition::Match { actions } => {
            w.u8(3);
            w.len(actions.len());
            for ActionId(a) in actions {
                w.u32(*a);
            }
        }
        Transition::LocalVarWrite { var, value } => {
            w.u8(4);
            w.u32(var.0);
            w.u32(value.0);
        }
        Transition::LocalVarCopy { dst, src } => {
            w.u8(5);
            w.u32(dst.0);
            w.u32(src.0);
        }
        Transition::FirstMatchBegin { group } => {
            w.u8(6);
            w.u32(group.0);
        }
        Transition::FirstMatchEnd { group } => {
            w.u8(7);
            w.u32(group.0);
        }
        Transition::LocalVarStep { var, delta } => {
            w.u8(8);
            w.u32(var.0);
            w.u64(*delta as u64);
        }
        Transition::SubroutineCall { call, args } => {
            w.u8(9);
            w.u32(call.0);
            w.len(args.len());
            for a in args {
                match a {
                    CallArg::Value(leaf) => {
                        w.u8(0);
                        w.u32(leaf.0);
                    }
                    CallArg::Ref => w.u8(1),
                    CallArg::Const => w.u8(2),
                }
            }
        }
        Transition::EndPoint { point, flag } => {
            w.u8(10);
            w.u32(point.0);
            put_opt_u32(w, flag.map(|f| f.0));
        }
        Transition::ClockSync { to, strict } => {
            w.u8(11);
            w.u32(to.0);
            w.bool(*strict);
        }
    }
}

fn get_transition(r: &mut Reader<'_>) -> Result<Transition, ImageError> {
    Ok(match r.u8()? {
        0 => Transition::Delay {
            min: r.u32()?,
            max: get_opt_u32(r, "delay bound")?,
        },
        1 => Transition::Epsilon,
        2 => Transition::Abort {
            leaf: LeafId(r.u32()?),
            mode: get_abort_mode(r)?,
        },
        3 => {
            let n = r.len()?;
            Transition::Match {
                actions: (0..n)
                    .map(|_| r.u32().map(ActionId))
                    .collect::<Result<_, _>>()?,
            }
        }
        4 => Transition::LocalVarWrite {
            var: LocalVarId(r.u32()?),
            value: LeafId(r.u32()?),
        },
        5 => Transition::LocalVarCopy {
            dst: LocalVarId(r.u32()?),
            src: LocalVarId(r.u32()?),
        },
        6 => Transition::FirstMatchBegin {
            group: FirstMatchId(r.u32()?),
        },
        7 => Transition::FirstMatchEnd {
            group: FirstMatchId(r.u32()?),
        },
        8 => Transition::LocalVarStep {
            var: LocalVarId(r.u32()?),
            delta: r.u64()? as i64,
        },
        9 => {
            let call = CallId(r.u32()?);
            let n = r.len()?;
            let mut args = Vec::with_capacity(n);
            for _ in 0..n {
                args.push(match r.u8()? {
                    0 => CallArg::Value(LeafId(r.u32()?)),
                    1 => CallArg::Ref,
                    2 => CallArg::Const,
                    tag => return Err(bad("call argument", tag)),
                });
            }
            Transition::SubroutineCall { call, args }
        }
        10 => Transition::EndPoint {
            point: EndPointId(r.u32()?),
            flag: get_opt_u32(r, "end point flag")?.map(LocalVarId),
        },
        11 => Transition::ClockSync {
            to: ClockId(r.u32()?),
            strict: r.bool()?,
        },
        tag => return Err(bad("transition", tag)),
    })
}

/// Writes `a`, end-point automata included.
pub fn put_automaton(w: &mut Writer, a: &Automaton) {
    let Automaton {
        states,
        start,
        admits_empty,
        first_match_groups,
        local_vars,
        end_points,
        entry_clock,
    } = a;
    w.len(states.len());
    for State { edges } in states {
        w.len(edges.len());
        for Edge {
            guard,
            label,
            target,
        } in edges
        {
            put_opt_u32(w, guard.map(|g| g.0));
            put_transition(w, label);
            w.u32(target.0);
        }
    }
    w.u32(start.0);
    w.bool(*admits_empty);
    w.u32(*first_match_groups);
    w.len(local_vars.len());
    for LocalVarDecl { width, signed } in local_vars {
        w.u32(*width);
        w.bool(*signed);
    }
    w.len(end_points.len());
    for EndPoint {
        method,
        site,
        automaton,
        flow_out,
    } in end_points
    {
        w.u8(match method {
            EndMethod::Triggered => 0,
            EndMethod::Matched => 1,
        });
        w.u32(*site);
        put_automaton(w, automaton);
        w.len(flow_out.len());
        for (from, to) in flow_out {
            w.u32(from.0);
            w.u32(to.0);
        }
    }
    w.u32(entry_clock.0);
}

/// The inverse of [`put_automaton`].
pub fn get_automaton(r: &mut Reader<'_>) -> Result<Automaton, ImageError> {
    let n = r.len()?;
    let mut states = Vec::with_capacity(n);
    for _ in 0..n {
        let m = r.len()?;
        let mut edges = Vec::with_capacity(m);
        for _ in 0..m {
            edges.push(Edge {
                guard: get_opt_u32(r, "edge guard")?.map(LeafId),
                label: get_transition(r)?,
                target: ThreadStateId(r.u32()?),
            });
        }
        states.push(State { edges });
    }
    let start = ThreadStateId(r.u32()?);
    let admits_empty = r.bool()?;
    let first_match_groups = r.u32()?;
    let n = r.len()?;
    let local_vars = (0..n)
        .map(|_| {
            Ok(LocalVarDecl {
                width: r.u32()?,
                signed: r.bool()?,
            })
        })
        .collect::<Result<_, ImageError>>()?;
    let n = r.len()?;
    let mut end_points = Vec::with_capacity(n);
    for _ in 0..n {
        let method = match r.u8()? {
            0 => EndMethod::Triggered,
            1 => EndMethod::Matched,
            tag => return Err(bad("end method", tag)),
        };
        let site = r.u32()?;
        let automaton = get_automaton(r)?;
        let m = r.len()?;
        let flow_out = (0..m)
            .map(|_| Ok((LocalVarId(r.u32()?), LocalVarId(r.u32()?))))
            .collect::<Result<_, ImageError>>()?;
        end_points.push(EndPoint {
            method,
            site,
            automaton,
            flow_out,
        });
    }
    let entry_clock = ClockId(r.u32()?);
    Ok(Automaton {
        states,
        start,
        admits_empty,
        first_match_groups,
        local_vars,
        end_points,
        entry_clock,
    })
}

fn put_seq_ref(w: &mut Writer, s: &SeqRef) {
    let SeqRef {
        entry,
        admits_empty,
        clock,
        end_clock,
    } = s;
    w.u32(entry.0);
    w.bool(*admits_empty);
    w.u32(clock.0);
    w.u32(end_clock.0);
}

fn get_seq_ref(r: &mut Reader<'_>) -> Result<SeqRef, ImageError> {
    Ok(SeqRef {
        entry: ThreadStateId(r.u32()?),
        admits_empty: r.bool()?,
        clock: ClockId(r.u32()?),
        end_clock: ClockId(r.u32()?),
    })
}

fn put_prop(w: &mut Writer, p: &Prop) {
    match p {
        Prop::Seq { seq, strength } => {
            w.u8(0);
            put_seq_ref(w, seq);
            w.u8(match strength {
                None => 0,
                Some(Strength::Strong) => 1,
                Some(Strength::Weak) => 2,
            });
        }
        Prop::Not(a) => {
            w.u8(1);
            w.u32(a.0);
        }
        Prop::And(a, b) => {
            w.u8(2);
            w.u32(a.0);
            w.u32(b.0);
        }
        Prop::Or(a, b) => {
            w.u8(3);
            w.u32(a.0);
            w.u32(b.0);
        }
        Prop::If { cond, then, els } => {
            w.u8(4);
            w.u32(cond.0);
            w.u32(then.0);
            put_opt_u32(w, els.map(|e| e.0));
        }
        Prop::Case {
            selector,
            arms,
            default,
        } => {
            w.u8(5);
            w.u32(selector.0);
            w.len(arms.len());
            for CaseArm { labels, body } in arms {
                w.len(labels.len());
                for l in labels {
                    w.u32(l.0);
                }
                w.u32(body.0);
            }
            put_opt_u32(w, default.map(|d| d.0));
        }
        Prop::Implication {
            ante,
            cons,
            overlapped,
        } => {
            w.u8(6);
            put_seq_ref(w, ante);
            w.u32(cons.0);
            w.bool(*overlapped);
        }
        Prop::Nexttime { p, n, strong } => {
            w.u8(7);
            w.u32(p.0);
            w.u32(*n);
            w.bool(*strong);
        }
        Prop::Always { p, lo, hi, strong } => {
            w.u8(8);
            w.u32(p.0);
            w.u32(*lo);
            put_opt_u32(w, *hi);
            w.bool(*strong);
        }
        Prop::Eventually { p, lo, hi, strong } => {
            w.u8(9);
            w.u32(p.0);
            w.u32(*lo);
            put_opt_u32(w, *hi);
            w.bool(*strong);
        }
        Prop::Until { p, q, strong } => {
            w.u8(10);
            w.u32(p.0);
            w.u32(q.0);
            w.bool(*strong);
        }
        Prop::Abort { cond, p, mode } => {
            w.u8(11);
            w.u32(cond.0);
            w.u32(p.0);
            put_abort_mode(w, *mode);
        }
        Prop::Let { writes, body } => {
            w.u8(12);
            put_leaf_pairs(w, writes);
            w.u32(body.0);
        }
        Prop::Clocked { clock, p } => {
            w.u8(13);
            w.u32(clock.0);
            w.u32(p.0);
        }
        Prop::Call { decl, args, inits } => {
            w.u8(14);
            w.u32(decl.0);
            put_leaf_pairs(w, args);
            put_leaf_pairs(w, inits);
        }
    }
}

fn get_prop(r: &mut Reader<'_>) -> Result<Prop, ImageError> {
    let id = |r: &mut Reader<'_>| r.u32().map(PropId);
    Ok(match r.u8()? {
        0 => Prop::Seq {
            seq: get_seq_ref(r)?,
            strength: match r.u8()? {
                0 => None,
                1 => Some(Strength::Strong),
                2 => Some(Strength::Weak),
                tag => return Err(bad("strength", tag)),
            },
        },
        1 => Prop::Not(id(r)?),
        2 => Prop::And(id(r)?, id(r)?),
        3 => Prop::Or(id(r)?, id(r)?),
        4 => Prop::If {
            cond: LeafId(r.u32()?),
            then: id(r)?,
            els: get_opt_u32(r, "else branch")?.map(PropId),
        },
        5 => {
            let selector = LeafId(r.u32()?);
            let n = r.len()?;
            let mut arms = Vec::with_capacity(n);
            for _ in 0..n {
                let m = r.len()?;
                let labels = (0..m)
                    .map(|_| r.u32().map(LeafId))
                    .collect::<Result<_, _>>()?;
                arms.push(CaseArm {
                    labels,
                    body: id(r)?,
                });
            }
            Prop::Case {
                selector,
                arms,
                default: get_opt_u32(r, "case default")?.map(PropId),
            }
        }
        6 => Prop::Implication {
            ante: get_seq_ref(r)?,
            cons: id(r)?,
            overlapped: r.bool()?,
        },
        7 => Prop::Nexttime {
            p: id(r)?,
            n: r.u32()?,
            strong: r.bool()?,
        },
        8 => Prop::Always {
            p: id(r)?,
            lo: r.u32()?,
            hi: get_opt_u32(r, "always bound")?,
            strong: r.bool()?,
        },
        9 => Prop::Eventually {
            p: id(r)?,
            lo: r.u32()?,
            hi: get_opt_u32(r, "eventually bound")?,
            strong: r.bool()?,
        },
        10 => Prop::Until {
            p: id(r)?,
            q: id(r)?,
            strong: r.bool()?,
        },
        11 => Prop::Abort {
            cond: LeafId(r.u32()?),
            p: id(r)?,
            mode: get_abort_mode(r)?,
        },
        12 => Prop::Let {
            writes: get_leaf_pairs(r)?,
            body: id(r)?,
        },
        13 => Prop::Clocked {
            clock: ClockId(r.u32()?),
            p: id(r)?,
        },
        14 => Prop::Call {
            decl: DeclId(r.u32()?),
            args: get_leaf_pairs(r)?,
            inits: get_leaf_pairs(r)?,
        },
        tag => return Err(bad("property operator", tag)),
    })
}

/// Writes `ir`: its automaton, operator DAG, declarations, root, `disable iff`
/// leaf and nonvacuity overrides.
pub fn put_property_ir(w: &mut Writer, ir: &PropertyIr) {
    let PropertyIr {
        automaton,
        props,
        decls,
        root,
        disable,
        nv_rules,
    } = ir;
    put_automaton(w, automaton);
    w.len(props.len());
    for p in props {
        put_prop(w, p);
    }
    w.len(decls.len());
    for PropDecl { name, body } in decls {
        w.str(name);
        w.u32(body.0);
    }
    w.u32(root.0);
    put_opt_u32(w, disable.map(|d| d.0));
    w.len(nv_rules.len());
    for (id, rule) in nv_rules {
        w.u32(id.0);
        w.u8(match rule {
            NvRule::Implies => 0,
            NvRule::UntilWith => 1,
        });
    }
}

/// The inverse of [`put_property_ir`].
pub fn get_property_ir(r: &mut Reader<'_>) -> Result<PropertyIr, ImageError> {
    let automaton = get_automaton(r)?;
    let n = r.len()?;
    let props = (0..n).map(|_| get_prop(r)).collect::<Result<Vec<_>, _>>()?;
    let n = r.len()?;
    let decls = (0..n)
        .map(|_| {
            Ok(PropDecl {
                name: r.str()?,
                body: PropId(r.u32()?),
            })
        })
        .collect::<Result<Vec<_>, ImageError>>()?;
    let root = PropId(r.u32()?);
    let disable = get_opt_u32(r, "disable leaf")?.map(LeafId);
    let n = r.len()?;
    let mut nv_rules = Vec::with_capacity(n);
    for _ in 0..n {
        let id = PropId(r.u32()?);
        nv_rules.push((
            id,
            match r.u8()? {
                0 => NvRule::Implies,
                1 => NvRule::UntilWith,
                tag => return Err(bad("nonvacuity rule", tag)),
            },
        ));
    }
    Ok(PropertyIr {
        automaton,
        props,
        decls,
        root,
        disable,
        nv_rules,
    })
}