max / shop
| 1 | //! The grid's contract with untrusted bytes, written as an executable assertion. |
| 2 | //! |
| 3 | //! A normal public module rather than something behind a `fuzzing` feature, |
| 4 | //! because two callers need it and neither is the fuzzer: the committed |
| 5 | //! regression replay in `tests/regressions.rs` runs it on stable, and the |
| 6 | //! libFuzzer target in `fuzz/` runs it on nightly. A property asserted in one |
| 7 | //! and not the other is a property that drifts. |
| 8 | //! |
| 9 | //! ## Why this lives here and not in `shop-vt` |
| 10 | //! |
| 11 | //! `shop-vt` contains no `unsafe`. Fuzzing it with a no-op `Perform` asserts |
| 12 | //! only that it does not panic, which is the weakest thing a target can say and |
| 13 | //! reads as a defended path forever. The bytes reach real unchecked stores one |
| 14 | //! crate downstream: [`Grid::place_char`] writes through `get_unchecked_mut` on |
| 15 | //! the strength of invariants that the CSI cursor, DECSTBM, scroll and resize |
| 16 | //! paths maintain from those same bytes. So the parser is driven with the grid |
| 17 | //! as its `Perform`, and what is asserted is the preconditions of that store. |
| 18 | //! |
| 19 | //! ## The properties |
| 20 | //! |
| 21 | //! 1. **Structural invariants** ([`check_invariants`]) — the exact |
| 22 | //! preconditions the `SAFETY` comment in `place_char` names, plus the ones |
| 23 | //! the ring layout and history rest on. Checked after every chunk. |
| 24 | //! 2. **Row totality** — `row(r)` yields exactly `cols` cells for every visible |
| 25 | //! row, which exercises the ring and region origin arithmetic rather than |
| 26 | //! trusting it. |
| 27 | //! 3. **Wide pairs are whole** — a wide lead is never in the last column and is |
| 28 | //! always followed by its spacer. This is what `heal_pair` is for, and a |
| 29 | //! half-pair is how a renderer reads past the end of a row. |
| 30 | //! 4. **Damage is in range** — every row `take_damage` reports exists, and a |
| 31 | //! second drain with no input in between reports nothing. |
| 32 | //! 5. **Resize keeps all of the above**, including a resize back to the |
| 33 | //! original size, which is where `rewrap_history` runs. |
| 34 | //! 6. **The parser's buffers are bounded**, twice over: by the input, via |
| 35 | //! [`MAX_RETAINED_PER_INPUT_BYTE`], and absolutely, via |
| 36 | //! [`MAX_RETAINED_BYTES`]. The second is the one that catches an |
| 37 | //! accumulator growing 1:1 with a stream nobody terminates, which the |
| 38 | //! first cannot see. |
| 39 | //! 7. **Ground is always reachable** — after any byte sequence, `ESC \` then |
| 40 | //! `ESC [ 0 m` returns the parser to Ground from every state. Cheap, and it |
| 41 | //! catches a transition-table edit that strands a stream. |
| 42 | |
| 43 | use crate::; |
| 44 | use Parser; |
| 45 | |
| 46 | /// Bytes the parser may hold per byte of input before the oracle calls it a |
| 47 | /// finding. |
| 48 | /// |
| 49 | /// 4 is set from the worst case, which is a body buffer caught just past a |
| 50 | /// doubling: 2.0 bytes of capacity per byte pushed, plus the parameter list and |
| 51 | /// the OSC index table on top. The caps that hold it there are |
| 52 | /// `shop_vt::MAX_PARAMS`, `shop_vt::MAX_STRING_BYTES` and |
| 53 | /// `shop_vt::MAX_OSC_PARAMS`. Anything that pushes this back over 4 is either a |
| 54 | /// new accumulator or a cap that stopped being enforced. |
| 55 | pub const MAX_RETAINED_PER_INPUT_BYTE: usize = 4; |
| 56 | |
| 57 | /// Slack for the buffers a fresh parser allocates up front (two 2 KiB bodies), |
| 58 | /// the parameter list's own spine, and the OSC field index table, which costs |
| 59 | /// 16 bytes per `;` and so amplifies hard against a stream of nothing else. |
| 60 | pub const RETAINED_BASE_BYTES: usize = 64 * 1024; |
| 61 | |
| 62 | /// Bytes the parser may hold after any input at all, however long. |
| 63 | /// |
| 64 | /// The ratio ceiling above cannot see an unterminated OSC or APC body: it |
| 65 | /// accumulates 1:1, so no per-input-byte limit above 1 fires, while the buffer |
| 66 | /// grows for as long as the writer keeps writing. This is the absolute bound |
| 67 | /// that catches that. |
| 68 | /// |
| 69 | /// Set from the caps rather than guessed: one body buffer at |
| 70 | /// `shop_vt::MAX_STRING_BYTES`, the other resting at its initial 2 KiB, the OSC |
| 71 | /// index table at `shop_vt::MAX_OSC_PARAMS` doubled, and `shop_vt::MAX_PARAMS` |
| 72 | /// slots. That is about 8.42 MiB; 12 MiB leaves room for allocator rounding |
| 73 | /// without leaving room for an accumulator that does not stop. |
| 74 | pub const MAX_RETAINED_BYTES: usize = 12 * 1024 * 1024; |
| 75 | |
| 76 | /// Panics if `grid` has broken anything `place_char`'s unchecked store rests on. |
| 77 | /// |
| 78 | /// # Panics |
| 79 | /// |
| 80 | /// By design. It is an oracle, and a panic is how it reports. |
| 81 | |
| 82 | let cols = grid.cols as usize; |
| 83 | let rows = grid.rows as usize; |
| 84 | assert!; |
| 85 | |
| 86 | // 1. Both screens are exactly rows * cols. This is the bound the unchecked |
| 87 | // store is checked against and everything below assumes it. |
| 88 | assert_eq!; |
| 89 | assert_eq!; |
| 90 | assert_eq!; |
| 91 | assert_eq! |
| 92 | grid.main_wrapped.len, |
| 93 | rows, |
| 94 | "main_wrapped is not one per row" |
| 95 | ; |
| 96 | assert_eq! |
| 97 | grid.alt_wrapped.len, |
| 98 | rows, |
| 99 | "alt_wrapped is not one per row" |
| 100 | ; |
| 101 | |
| 102 | // 2. The cursor is on the screen. `place_char` clamps col on entry and |
| 103 | // relies on row having been kept in range by whoever moved it. |
| 104 | assert! |
| 105 | < rows, |
| 106 | "cursor row {} outside {rows} rows", |
| 107 | grid.cursor.row |
| 108 | ; |
| 109 | assert! |
| 110 | < cols, |
| 111 | "cursor col {} outside {cols} cols", |
| 112 | grid.cursor.col |
| 113 | ; |
| 114 | |
| 115 | // 3. The scroll region is a region, and it is inside the screen. DECSTBM |
| 116 | // takes both bounds from the parameter list, so this is untrusted input |
| 117 | // reaching the modulus in `phys_row`. |
| 118 | assert! |
| 119 | grid.scroll_top <= grid.scroll_bottom, |
| 120 | "scroll region inverted: {}..={}", |
| 121 | grid.scroll_top, |
| 122 | grid.scroll_bottom |
| 123 | ; |
| 124 | assert! |
| 125 | < rows, |
| 126 | "scroll bottom {} outside {rows} rows", |
| 127 | grid.scroll_bottom |
| 128 | ; |
| 129 | |
| 130 | // 4. Ring origins are rotations, not offsets into nothing. |
| 131 | assert! |
| 132 | < rows, |
| 133 | "main_origin out of range" |
| 134 | ; |
| 135 | assert!; |
| 136 | let region = as usize; |
| 137 | assert! |
| 138 | < region, |
| 139 | "region_origin {} outside a region of {region}", |
| 140 | grid.region_origin |
| 141 | ; |
| 142 | |
| 143 | // 5. The cached row start is either invalid or a real row start. It is fed |
| 144 | // straight to the unchecked store as `start`. |
| 145 | if grid.cur_row_start != CUR_ROW_INVALID |
| 146 | let start = grid.cur_row_start as usize; |
| 147 | assert_eq!; |
| 148 | assert! |
| 149 | start + cols <= grid.main.len, |
| 150 | "cur_row_start {start} leaves no row" |
| 151 | ; |
| 152 | |
| 153 | |
| 154 | // 6. History is bounded and every row of it is exactly the current width. |
| 155 | // `row()` hands these out as if they came off the live screen, so a |
| 156 | // short one is a short slice under every reader above it. |
| 157 | assert! |
| 158 | grid.history.len <= grid.history_limit, |
| 159 | "history {} exceeds its limit {}", |
| 160 | grid.history.len, |
| 161 | grid.history_limit |
| 162 | ; |
| 163 | for in grid.history.iter.enumerate |
| 164 | assert_eq!; |
| 165 | |
| 166 | assert! |
| 167 | grid.view_offset as usize <= grid.history.len, |
| 168 | "view_offset {} is past {} rows of history", |
| 169 | grid.view_offset, |
| 170 | grid.history.len |
| 171 | ; |
| 172 | if grid.on_alt |
| 173 | assert_eq!; |
| 174 | |
| 175 | |
| 176 | // 7. Every visible row is a whole row, and every wide pair is whole. A lead |
| 177 | // in the last column, or a lead with no spacer after it, is a character |
| 178 | // claiming a column that is not there. |
| 179 | for r in 0..grid.rows |
| 180 | let row = grid.row; |
| 181 | assert_eq! |
| 182 | row.len, |
| 183 | cols, |
| 184 | "row {r} is {} cells, not {cols}", |
| 185 | row.len |
| 186 | ; |
| 187 | for in row.iter.enumerate |
| 188 | if cell.is_wide |
| 189 | assert!; |
| 190 | assert! |
| 191 | row.is_spacer, |
| 192 | "wide lead at {r},{c} has no spacer after it" |
| 193 | ; |
| 194 | |
| 195 | |
| 196 | |
| 197 | |
| 198 | |
| 199 | /// Panics if the damage report names a row that does not exist, or if a second |
| 200 | /// drain with no input in between still reports one. |
| 201 | /// |
| 202 | /// # Panics |
| 203 | /// |
| 204 | /// By design. |
| 205 | |
| 206 | let d = grid.take_damage; |
| 207 | for r in &d.dirty_rows |
| 208 | assert!; |
| 209 | |
| 210 | let again = grid.take_damage; |
| 211 | assert! |
| 212 | again.dirty_rows.is_empty, |
| 213 | "damage repeated {} rows with no input between drains", |
| 214 | again.dirty_rows.len |
| 215 | ; |
| 216 | |
| 217 | |
| 218 | /// Feed `input` to a grid through the real parser and hold both to everything |
| 219 | /// above. |
| 220 | /// |
| 221 | /// Returns the number of bytes that reached the parser, for the same reason |
| 222 | /// `git_command::oracle::check_line` returns a bool: without a return value |
| 223 | /// nothing can observe this function running at all, and `cargo mutants` |
| 224 | /// replacing the body with `()` would leave every test passing. A silently |
| 225 | /// empty oracle is the one failure this arrangement cannot afford. |
| 226 | /// |
| 227 | /// # Panics |
| 228 | /// |
| 229 | /// By design, on any violation. |
| 230 | |
| 231 | // The first two bytes choose the screen size, so one corpus covers the |
| 232 | // one-column and one-row grids as well as ordinary ones. Everything after |
| 233 | // them is the byte stream. |
| 234 | let = match input |
| 235 | => , |
| 236 | _ => , |
| 237 | ; |
| 238 | |
| 239 | let mut grid = new; |
| 240 | let mut parser = new; |
| 241 | check_invariants; |
| 242 | |
| 243 | // Chunked rather than one call, because the parser's own state is what |
| 244 | // survives a chunk boundary and a corpus of whole-sequence inputs would |
| 245 | // never exercise a split one. Sixteen is small enough to land inside a |
| 246 | // typical CSI. |
| 247 | for chunk in stream.chunks |
| 248 | parser.advance; |
| 249 | check_invariants; |
| 250 | |
| 251 | check_damage; |
| 252 | check_invariants; |
| 253 | |
| 254 | // The amplification ceiling. See MAX_RETAINED_PER_INPUT_BYTE for why it is |
| 255 | // set above today's behaviour rather than at it. |
| 256 | let retained = parser.buffered_bytes; |
| 257 | let ceiling = RETAINED_BASE_BYTES + stream.len.saturating_mul; |
| 258 | assert! |
| 259 | retained <= ceiling, |
| 260 | "parser holds {retained} bytes after {} bytes of input, over the {ceiling} ceiling", |
| 261 | stream.len |
| 262 | ; |
| 263 | assert! |
| 264 | retained <= MAX_RETAINED_BYTES, |
| 265 | "parser holds {retained} bytes, over the {MAX_RETAINED_BYTES} absolute ceiling" |
| 266 | ; |
| 267 | |
| 268 | // Ground is reachable from every state these two sequences can leave the |
| 269 | // parser in: `ESC \` closes any string state, and a complete CSI closes the |
| 270 | // DCS passthrough that `\` opens from a DCS parameter state. |
| 271 | parser.advance; |
| 272 | parser.advance; |
| 273 | assert! |
| 274 | parser.in_ground, |
| 275 | "parser did not return to Ground after a terminator and a complete CSI" |
| 276 | ; |
| 277 | check_invariants; |
| 278 | |
| 279 | // Resize is the other path into the unchecked store's preconditions, and |
| 280 | // the only one that rewraps history. Sizes come from the input so the |
| 281 | // corpus can steer them. |
| 282 | let = match stream |
| 283 | => , |
| 284 | _ => , |
| 285 | ; |
| 286 | grid.resize; |
| 287 | check_invariants; |
| 288 | grid.resize; |
| 289 | check_invariants; |
| 290 | check_damage; |
| 291 | |
| 292 | stream.len |
| 293 | |
| 294 |