rucc_rules/ast.rs
1//! What a rule is, once it has been read.
2
3use std::fmt;
4
5/// A term: the pattern a rule matches, the replacement it produces, and the two clauses that
6/// constrain it are all one shape.
7#[derive(Debug, Clone, PartialEq, Eq)]
8pub struct Term {
9 /// Which of the three kinds this is.
10 pub kind: TermKind,
11 /// The line it starts on, counted from one.
12 pub line: u32,
13 /// The column it starts at, counted from one.
14 pub column: u32,
15}
16
17/// The three kinds of term.
18#[derive(Debug, Clone, PartialEq, Eq)]
19pub enum TermKind {
20 /// A name standing for whatever the pattern bound it to.
21 Var(String),
22 /// A literal.
23 Int(i128),
24 /// A head applied to arguments, which is every opcode, every constructor and every operator
25 /// in a specification.
26 App {
27 /// The name in head position.
28 head: String,
29 /// What it is applied to, possibly nothing, as in `(result)`.
30 args: Vec<Term>,
31 },
32}
33
34impl Term {
35 /// Walk this term and everything under it, outermost first.
36 ///
37 /// The lifetime is written out so that what the visitor is handed lives as long as the term
38 /// does, which is what lets a caller collect the places it found rather than only count them.
39 pub fn walk<'t>(&'t self, visit: &mut impl FnMut(&'t Term)) {
40 visit(self);
41 if let TermKind::App { args, .. } = &self.kind {
42 for arg in args {
43 arg.walk(visit);
44 }
45 }
46 }
47}
48
49impl fmt::Display for Term {
50 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
51 match &self.kind {
52 TermKind::Var(name) => f.write_str(name),
53 TermKind::Int(value) => write!(f, "{value}"),
54 TermKind::App { head, args } => {
55 write!(f, "({head}")?;
56 for arg in args {
57 write!(f, " {arg}")?;
58 }
59 f.write_str(")")
60 }
61 }
62 }
63}
64
65/// What a rule rewrites into.
66///
67/// The three kinds are matched by the same trie and verified by the same obligation, and the only
68/// thing that separates them is what the replacement is written in. Keeping them one language
69/// rather than three is the whole reason `spec/09-optimizer.md` section 9.3 and
70/// `spec/10-backend.md` section 10.2 ask for a rule DSL at all, because a rewrite and a
71/// lowering are the same claim about two terms and there is no reason to say it twice.
72#[derive(Debug, Clone, Copy, PartialEq, Eq)]
73pub enum RuleKind {
74 /// IR to IR. The replacement is IR, so a rewrite can be applied over and over and the
75 /// result is still something later rules match. `spec/optimizer/13-rewrite-rules.md`.
76 Simplify,
77 /// IR to machine. The replacement is a machine term, so a lowering is the last thing that
78 /// happens to a value and nothing matches what it produces. `spec/10-backend.md`.
79 Lower,
80 /// A question about a safety check, answered yes. The pattern is not an instruction: it is a
81 /// term a pass builds out of what it has worked out about two checks, and the replacement is
82 /// the constant one, so the rule says that under its guard the answer to the question is yes
83 /// and the check the question was about does not have to happen.
84 ///
85 /// It is a kind of its own rather than a `simplify` because a table of these is not matched
86 /// against the IR and would be wrong to put in the simplifier, and because
87 /// `spec/safe-memory/07-check-elimination.md` section 7.7 asks for exactly this split: the
88 /// walk that establishes the context is ordinary code nobody proves, and the condition under
89 /// which a check may go is data somebody proves.
90 Discharge,
91}
92
93impl RuleKind {
94 /// The keyword that introduces a rule of this kind.
95 #[must_use]
96 pub const fn as_str(self) -> &'static str {
97 match self {
98 Self::Simplify => "simplify",
99 Self::Lower => "lower",
100 Self::Discharge => "discharge",
101 }
102 }
103}
104
105impl fmt::Display for RuleKind {
106 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
107 f.write_str(self.as_str())
108 }
109}
110
111/// One rule: what it matches, what it produces, and what makes that sound.
112#[derive(Debug, Clone, PartialEq, Eq)]
113pub struct Rule {
114 /// Whether the replacement is IR or a machine term.
115 pub kind: RuleKind,
116 /// The term to match, which is IR for a rewrite and IR for a lowering.
117 pub pattern: Term,
118 /// A condition on the match, which is where a rule that only holds for some constants says
119 /// so. It sits between the pattern and the replacement because it is part of deciding
120 /// whether the rule fires, not part of what firing produces.
121 pub guard: Option<Term>,
122 /// What to put in the matched term's place.
123 pub replacement: Term,
124 /// The bitvector claim relating the two, which is what `rucc-verify` discharges. It is not
125 /// optional, because a rule set that lets one rule through without a specification is a rule
126 /// set with an unverified rule in it.
127 pub spec: Term,
128 /// Why a proof at narrower widths is enough for this rule, when there is a reason to think
129 /// the solver will not manage the real one. A rule carrying this is not excused anything:
130 /// it is still asked at its own width first, and the clause only says what a person is
131 /// willing to sign for if the answer comes back as a shrug.
132 pub bounded: Option<String>,
133 /// The line the rule starts on.
134 pub line: u32,
135 /// The column the rule starts at.
136 pub column: u32,
137}
138
139impl fmt::Display for Rule {
140 /// Prints the rule back in the shape `spec/10-backend.md` writes it: one clause to a line,
141 /// with the continuation lines under the pattern.
142 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
143 writeln!(f, "(rule ({} {})", self.kind, self.pattern)?;
144 if let Some(guard) = &self.guard {
145 writeln!(f, " (if {guard})")?;
146 }
147 writeln!(f, " {}", self.replacement)?;
148 match &self.bounded {
149 Some(why) => {
150 writeln!(f, " (spec {})", self.spec)?;
151 write!(f, " (bounded \"{why}\"))")
152 }
153 None => write!(f, " (spec {}))", self.spec),
154 }
155 }
156}