cranelift_codegen/ir/pcc.rs
1//! Proof-carrying code. We attach "facts" to values and then check
2//! that they remain true after compilation.
3//!
4//! A few key design principle of this approach are:
5//!
6//! - The producer of the IR provides the axioms. All "ground truth",
7//! such as what memory is accessible -- is meant to come by way of
8//! facts on the function arguments and global values. In some
9//! sense, all we are doing here is validating the "internal
10//! consistency" of the facts that are provided on values, and the
11//! actions performed on those values.
12//!
13//! - We do not derive and forward-propagate facts eagerly. Rather,
14//! the producer needs to provide breadcrumbs -- a "proof witness"
15//! of sorts -- to allow the checking to complete. That means that
16//! as an address is computed, or pointer chains are dereferenced,
17//! each intermediate value will likely have some fact attached.
18//!
19//! This does create more verbose IR, but a significant positive
20//! benefit is that it avoids unnecessary work: we do not build up a
21//! knowledge base that effectively encodes the integer ranges of
22//! many or most values in the program. Rather, we only check
23//! specifically the memory-access sequences. In practice, each such
24//! sequence is likely to be a carefully-controlled sequence of IR
25//! operations from, e.g., a sandboxing compiler (such as
26//! Wasmtime) so adding annotations here to communicate
27//! intent (ranges, bounds-checks, and the like) is no problem.
28//!
29//! Facts are attached to SSA values in CLIF, and are maintained
30//! through optimizations and through lowering. They are thus also
31//! present on VRegs in the VCode. In theory, facts could be checked
32//! at either level, though in practice it is most useful to check
33//! them at the VCode level if the goal is an end-to-end verification
34//! of certain properties (e.g., memory sandboxing).
35//!
36//! Checking facts entails visiting each instruction that defines a
37//! value with a fact, and checking the result's fact against the
38//! facts on arguments and the operand. For VCode, this is
39//! fundamentally a question of the target ISA's semantics, so we call
40//! into the `LowerBackend` for this. Note that during checking there
41//! is also limited forward propagation / inference, but only within
42//! an instruction: for example, an addressing mode commonly can
43//! include an addition, multiplication/shift, or extend operation,
44//! and there is no way to attach facts to the intermediate values
45//! "inside" the instruction, so instead the backend can use
46//! `FactContext::add()` and friends to forward-propagate facts.
47//!
48//! TODO:
49//!
50//! Deployment:
51//! - Add to fuzzing
52//! - Turn on during wasm spec-tests
53//!
54//! More checks:
55//! - Check that facts on `vmctx` GVs are subsumed by the actual facts
56//! on the vmctx arg in block0 (function arg).
57//!
58//! Generality:
59//! - facts on outputs (in func signature)?
60//! - Implement checking at the CLIF level as well.
61//! - Check instructions that can trap as well?
62//!
63//! Nicer errors:
64//! - attach instruction index or some other identifier to errors
65//!
66//! Text format cleanup:
67//! - make the bitwidth on `max` facts optional in the CLIF text
68//! format?
69//! - make offset in `mem` fact optional in the text format?
70//!
71//! Bikeshed colors (syntax):
72//! - Put fact bang-annotations after types?
73//! `v0: i64 ! fact(..)` vs. `v0 ! fact(..): i64`
74
75use crate::ir;
76use crate::ir::types::*;
77use crate::isa::TargetIsa;
78use crate::machinst::{BlockIndex, LowerBackend, VCode};
79use crate::trace;
80use regalloc2::Function as _;
81use std::fmt;
82
83#[cfg(feature = "enable-serde")]
84use serde_derive::{Deserialize, Serialize};
85
86/// The result of checking proof-carrying-code facts.
87pub type PccResult<T> = std::result::Result<T, PccError>;
88
89/// An error or inconsistency discovered when checking proof-carrying
90/// code.
91#[derive(Debug, Clone)]
92pub enum PccError {
93 /// An operation wraps around, invalidating the stated value
94 /// range.
95 Overflow,
96 /// An input to an operator that produces a fact-annotated value
97 /// does not have a fact describing it, and one is needed.
98 MissingFact,
99 /// A derivation of an output fact is unsupported (incorrect or
100 /// not derivable).
101 UnsupportedFact,
102 /// A block parameter claims a fact that one of its predecessors
103 /// does not support.
104 UnsupportedBlockparam,
105 /// A memory access is out of bounds.
106 OutOfBounds,
107 /// Proof-carrying-code checking is not implemented for a
108 /// particular compiler backend.
109 UnimplementedBackend,
110 /// Proof-carrying-code checking is not implemented for a
111 /// particular instruction that instruction-selection chose. This
112 /// is an internal compiler error.
113 UnimplementedInst,
114 /// Access to an invalid or undefined field offset in a struct.
115 InvalidFieldOffset,
116 /// Access to a field via the wrong type.
117 BadFieldType,
118 /// Store to a read-only field.
119 WriteToReadOnlyField,
120 /// Store of data to a field with a fact that does not subsume the
121 /// field's fact.
122 InvalidStoredFact,
123}
124
125/// A fact on a value.
126#[derive(Clone, Debug, Hash, PartialEq, Eq)]
127#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
128pub enum Fact {
129 /// A bitslice of a value (up to a bitwidth) is within the given
130 /// integer range.
131 ///
132 /// The slicing behavior is needed because this fact can describe
133 /// both an SSA `Value`, whose entire value is well-defined, and a
134 /// `VReg` in VCode, whose bits beyond the type stored in that
135 /// register are don't-care (undefined).
136 Range {
137 /// The bitwidth of bits we care about, from the LSB upward.
138 bit_width: u16,
139 /// The minimum value that the bitslice can take
140 /// (inclusive). The range is unsigned: the specified bits of
141 /// the actual value will be greater than or equal to this
142 /// value, as evaluated by an unsigned integer comparison.
143 min: u64,
144 /// The maximum value that the bitslice can take
145 /// (inclusive). The range is unsigned: the specified bits of
146 /// the actual value will be less than or equal to this value,
147 /// as evaluated by an unsigned integer comparison.
148 max: u64,
149 },
150
151 /// A value bounded by a global value.
152 ///
153 /// The range is in `(min_GV + min_offset)..(max_GV +
154 /// max_offset)`, inclusive on the lower and upper bound.
155 DynamicRange {
156 /// The bitwidth of bits we care about, from the LSB upward.
157 bit_width: u16,
158 /// The lower bound, inclusive.
159 min: Expr,
160 /// The upper bound, inclusive.
161 max: Expr,
162 },
163
164 /// A pointer to a memory type.
165 Mem {
166 /// The memory type.
167 ty: ir::MemoryType,
168 /// The minimum offset into the memory type, inclusive.
169 min_offset: u64,
170 /// The maximum offset into the memory type, inclusive.
171 max_offset: u64,
172 /// This pointer can also be null.
173 nullable: bool,
174 },
175
176 /// A pointer to a memory type, dynamically bounded. The pointer
177 /// is within `(GV_min+offset_min)..(GV_max+offset_max)`
178 /// (inclusive on both ends) in the memory type.
179 DynamicMem {
180 /// The memory type.
181 ty: ir::MemoryType,
182 /// The lower bound, inclusive.
183 min: Expr,
184 /// The upper bound, inclusive.
185 max: Expr,
186 /// This pointer can also be null.
187 nullable: bool,
188 },
189
190 /// A definition of a value to be used as a symbol in
191 /// BaseExprs. There can only be one of these per value number.
192 ///
193 /// Note that this differs from a `DynamicRange` specifying that
194 /// some value in the program is the same as `value`. A `def(v1)`
195 /// fact is propagated to machine code and serves as a source of
196 /// truth: the value or location labeled with this fact *defines*
197 /// what `v1` is, and any `dynamic_range(64, v1, v1)`-labeled
198 /// values elsewhere are claiming to be equal to this value.
199 ///
200 /// This is necessary because we don't propagate SSA value labels
201 /// down to machine code otherwise; so when referring symbolically
202 /// to addresses and expressions derived from addresses, we need
203 /// to introduce the symbol first.
204 Def {
205 /// The SSA value this value defines.
206 value: ir::Value,
207 },
208
209 /// A comparison result between two dynamic values with a
210 /// comparison of a certain kind.
211 Compare {
212 /// The kind of comparison.
213 kind: ir::condcodes::IntCC,
214 /// The left-hand side of the comparison.
215 lhs: Expr,
216 /// The right-hand side of the comparison.
217 rhs: Expr,
218 },
219
220 /// A "conflict fact": this fact results from merging two other
221 /// facts, and it can never be satisfied -- checking any value
222 /// against this fact will fail.
223 Conflict,
224}
225
226/// A bound expression.
227#[derive(Clone, Debug, Hash, PartialEq, Eq)]
228#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
229pub struct Expr {
230 /// The dynamic (base) part.
231 pub base: BaseExpr,
232 /// The static (offset) part.
233 pub offset: i64,
234}
235
236/// The base part of a bound expression.
237#[derive(Clone, Debug, Hash, PartialEq, Eq)]
238#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
239pub enum BaseExpr {
240 /// No dynamic part (i.e., zero).
241 None,
242 /// A global value.
243 GlobalValue(ir::GlobalValue),
244 /// An SSA Value as a symbolic value. This can be referenced in
245 /// facts even after we've lowered out of SSA: it becomes simply
246 /// some symbolic value.
247 Value(ir::Value),
248 /// Top of the address space. This is "saturating": the offset
249 /// doesn't matter.
250 Max,
251}
252
253impl BaseExpr {
254 /// Is one base less than or equal to another? (We can't always
255 /// know; in such cases, returns `false`.)
256 fn le(lhs: &BaseExpr, rhs: &BaseExpr) -> bool {
257 // (i) reflexivity; (ii) 0 <= x for all (unsigned) x; (iii) x <= max for all x.
258 lhs == rhs || *lhs == BaseExpr::None || *rhs == BaseExpr::Max
259 }
260
261 /// Compute some BaseExpr that will be less than or equal to both
262 /// inputs. This is a generalization of `min` (but looser).
263 fn min(lhs: &BaseExpr, rhs: &BaseExpr) -> BaseExpr {
264 if lhs == rhs {
265 lhs.clone()
266 } else if *lhs == BaseExpr::Max {
267 rhs.clone()
268 } else if *rhs == BaseExpr::Max {
269 lhs.clone()
270 } else {
271 BaseExpr::None // zero is <= x for all (unsigned) x.
272 }
273 }
274
275 /// Compute some BaseExpr that will be greater than or equal to
276 /// both inputs.
277 fn max(lhs: &BaseExpr, rhs: &BaseExpr) -> BaseExpr {
278 if lhs == rhs {
279 lhs.clone()
280 } else if *lhs == BaseExpr::None {
281 rhs.clone()
282 } else if *rhs == BaseExpr::None {
283 lhs.clone()
284 } else {
285 BaseExpr::Max
286 }
287 }
288}
289
290impl Expr {
291 /// Constant value.
292 pub fn constant(offset: i64) -> Self {
293 Expr {
294 base: BaseExpr::None,
295 offset,
296 }
297 }
298
299 /// The value of an SSA value.
300 pub fn value(value: ir::Value) -> Self {
301 Expr {
302 base: BaseExpr::Value(value),
303 offset: 0,
304 }
305 }
306
307 /// The value of a global value.
308 pub fn global_value(gv: ir::GlobalValue) -> Self {
309 Expr {
310 base: BaseExpr::GlobalValue(gv),
311 offset: 0,
312 }
313 }
314
315 /// Is one expression definitely less than or equal to another?
316 /// (We can't always know; in such cases, returns `false`.)
317 fn le(lhs: &Expr, rhs: &Expr) -> bool {
318 if rhs.base == BaseExpr::Max {
319 true
320 } else {
321 BaseExpr::le(&lhs.base, &rhs.base) && lhs.offset <= rhs.offset
322 }
323 }
324
325 /// Generalization of `min`: compute some Expr that is less than
326 /// or equal to both inputs.
327 fn min(lhs: &Expr, rhs: &Expr) -> Expr {
328 if lhs.base == BaseExpr::None && lhs.offset == 0 {
329 lhs.clone()
330 } else if rhs.base == BaseExpr::None && rhs.offset == 0 {
331 rhs.clone()
332 } else {
333 Expr {
334 base: BaseExpr::min(&lhs.base, &rhs.base),
335 offset: std::cmp::min(lhs.offset, rhs.offset),
336 }
337 }
338 }
339
340 /// Generalization of `max`: compute some Expr that is greater
341 /// than or equal to both inputs.
342 fn max(lhs: &Expr, rhs: &Expr) -> Expr {
343 if lhs.base == BaseExpr::None && lhs.offset == 0 {
344 rhs.clone()
345 } else if rhs.base == BaseExpr::None && rhs.offset == 0 {
346 lhs.clone()
347 } else {
348 Expr {
349 base: BaseExpr::max(&lhs.base, &rhs.base),
350 offset: std::cmp::max(lhs.offset, rhs.offset),
351 }
352 }
353 }
354
355 /// Add one expression to another.
356 fn add(lhs: &Expr, rhs: &Expr) -> Option<Expr> {
357 if lhs.base == rhs.base {
358 Some(Expr {
359 base: lhs.base.clone(),
360 offset: lhs.offset.checked_add(rhs.offset)?,
361 })
362 } else if lhs.base == BaseExpr::None {
363 Some(Expr {
364 base: rhs.base.clone(),
365 offset: lhs.offset.checked_add(rhs.offset)?,
366 })
367 } else if rhs.base == BaseExpr::None {
368 Some(Expr {
369 base: lhs.base.clone(),
370 offset: lhs.offset.checked_add(rhs.offset)?,
371 })
372 } else {
373 Some(Expr {
374 base: BaseExpr::Max,
375 offset: 0,
376 })
377 }
378 }
379
380 /// Add a static offset to an expression.
381 pub fn offset(lhs: &Expr, rhs: i64) -> Option<Expr> {
382 let offset = lhs.offset.checked_add(rhs)?;
383 Some(Expr {
384 base: lhs.base.clone(),
385 offset,
386 })
387 }
388
389 /// Is this Expr a BaseExpr with no offset? Return it if so.
390 pub fn without_offset(&self) -> Option<&BaseExpr> {
391 if self.offset == 0 {
392 Some(&self.base)
393 } else {
394 None
395 }
396 }
397}
398
399impl fmt::Display for BaseExpr {
400 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
401 match self {
402 BaseExpr::None => Ok(()),
403 BaseExpr::Max => write!(f, "max"),
404 BaseExpr::GlobalValue(gv) => write!(f, "{gv}"),
405 BaseExpr::Value(value) => write!(f, "{value}"),
406 }
407 }
408}
409
410impl BaseExpr {
411 /// Does this dynamic_expression take an offset?
412 pub fn is_some(&self) -> bool {
413 match self {
414 BaseExpr::None => false,
415 _ => true,
416 }
417 }
418}
419
420impl fmt::Display for Expr {
421 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
422 write!(f, "{}", self.base)?;
423 match self.offset {
424 offset if offset > 0 && self.base.is_some() => write!(f, "+{offset:#x}"),
425 offset if offset > 0 => write!(f, "{offset:#x}"),
426 offset if offset < 0 => {
427 let negative_offset = -i128::from(offset); // upcast to support i64::MIN.
428 write!(f, "-{negative_offset:#x}")
429 }
430 0 if self.base.is_some() => Ok(()),
431 0 => write!(f, "0"),
432 _ => unreachable!(),
433 }
434 }
435}
436
437impl fmt::Display for Fact {
438 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
439 match self {
440 Fact::Range {
441 bit_width,
442 min,
443 max,
444 } => write!(f, "range({bit_width}, {min:#x}, {max:#x})"),
445 Fact::DynamicRange {
446 bit_width,
447 min,
448 max,
449 } => {
450 write!(f, "dynamic_range({bit_width}, {min}, {max})")
451 }
452 Fact::Mem {
453 ty,
454 min_offset,
455 max_offset,
456 nullable,
457 } => {
458 let nullable_flag = if *nullable { ", nullable" } else { "" };
459 write!(
460 f,
461 "mem({ty}, {min_offset:#x}, {max_offset:#x}{nullable_flag})"
462 )
463 }
464 Fact::DynamicMem {
465 ty,
466 min,
467 max,
468 nullable,
469 } => {
470 let nullable_flag = if *nullable { ", nullable" } else { "" };
471 write!(f, "dynamic_mem({ty}, {min}, {max}{nullable_flag})")
472 }
473 Fact::Def { value } => write!(f, "def({value})"),
474 Fact::Compare { kind, lhs, rhs } => {
475 write!(f, "compare({kind}, {lhs}, {rhs})")
476 }
477 Fact::Conflict => write!(f, "conflict"),
478 }
479 }
480}
481
482impl Fact {
483 /// Create a range fact that specifies a single known constant value.
484 pub fn constant(bit_width: u16, value: u64) -> Self {
485 debug_assert!(value <= max_value_for_width(bit_width));
486 // `min` and `max` are inclusive, so this specifies a range of
487 // exactly one value.
488 Fact::Range {
489 bit_width,
490 min: value,
491 max: value,
492 }
493 }
494
495 /// Create a dynamic range fact that points to the base of a dynamic memory.
496 pub fn dynamic_base_ptr(ty: ir::MemoryType) -> Self {
497 Fact::DynamicMem {
498 ty,
499 min: Expr::constant(0),
500 max: Expr::constant(0),
501 nullable: false,
502 }
503 }
504
505 /// Create a fact that specifies the value is exactly an SSA value.
506 ///
507 /// Note that this differs from a `def` fact: it is not *defining*
508 /// a symbol to have the value that this fact is attached to;
509 /// rather it is claiming that this value is the same as whatever
510 /// that symbol is. (In other words, the def should be elsewhere,
511 /// and we are tying ourselves to it.)
512 pub fn value(bit_width: u16, value: ir::Value) -> Self {
513 Fact::DynamicRange {
514 bit_width,
515 min: Expr::value(value),
516 max: Expr::value(value),
517 }
518 }
519
520 /// Create a fact that specifies the value is exactly an SSA value plus some offset.
521 pub fn value_offset(bit_width: u16, value: ir::Value, offset: i64) -> Self {
522 Fact::DynamicRange {
523 bit_width,
524 min: Expr::offset(&Expr::value(value), offset).unwrap(),
525 max: Expr::offset(&Expr::value(value), offset).unwrap(),
526 }
527 }
528
529 /// Create a fact that specifies the value is exactly the value of a GV.
530 pub fn global_value(bit_width: u16, gv: ir::GlobalValue) -> Self {
531 Fact::DynamicRange {
532 bit_width,
533 min: Expr::global_value(gv),
534 max: Expr::global_value(gv),
535 }
536 }
537
538 /// Create a fact that specifies the value is exactly the value of a GV plus some offset.
539 pub fn global_value_offset(bit_width: u16, gv: ir::GlobalValue, offset: i64) -> Self {
540 Fact::DynamicRange {
541 bit_width,
542 min: Expr::offset(&Expr::global_value(gv), offset).unwrap(),
543 max: Expr::offset(&Expr::global_value(gv), offset).unwrap(),
544 }
545 }
546
547 /// Create a range fact that specifies the maximum range for a
548 /// value of the given bit-width.
549 pub const fn max_range_for_width(bit_width: u16) -> Self {
550 match bit_width {
551 bit_width if bit_width < 64 => Fact::Range {
552 bit_width,
553 min: 0,
554 max: (1u64 << bit_width) - 1,
555 },
556 64 => Fact::Range {
557 bit_width: 64,
558 min: 0,
559 max: u64::MAX,
560 },
561 _ => panic!("bit width too large!"),
562 }
563 }
564
565 /// Create a range fact that specifies the maximum range for a
566 /// value of the given bit-width, zero-extended into a wider
567 /// width.
568 pub const fn max_range_for_width_extended(from_width: u16, to_width: u16) -> Self {
569 debug_assert!(from_width <= to_width);
570 match from_width {
571 from_width if from_width < 64 => Fact::Range {
572 bit_width: to_width,
573 min: 0,
574 max: (1u64 << from_width) - 1,
575 },
576 64 => Fact::Range {
577 bit_width: to_width,
578 min: 0,
579 max: u64::MAX,
580 },
581 _ => panic!("bit width too large!"),
582 }
583 }
584
585 /// Try to infer a minimal fact for a value of the given IR type.
586 pub fn infer_from_type(ty: ir::Type) -> Option<&'static Self> {
587 static FACTS: [Fact; 4] = [
588 Fact::max_range_for_width(8),
589 Fact::max_range_for_width(16),
590 Fact::max_range_for_width(32),
591 Fact::max_range_for_width(64),
592 ];
593 match ty {
594 I8 => Some(&FACTS[0]),
595 I16 => Some(&FACTS[1]),
596 I32 => Some(&FACTS[2]),
597 I64 => Some(&FACTS[3]),
598 _ => None,
599 }
600 }
601
602 /// Does this fact "propagate" automatically, i.e., cause
603 /// instructions that process it to infer their own output facts?
604 /// Not all facts propagate automatically; otherwise, verification
605 /// would be much slower.
606 pub fn propagates(&self) -> bool {
607 match self {
608 Fact::Mem { .. } => true,
609 _ => false,
610 }
611 }
612
613 /// Is this a constant value of the given bitwidth? Return it as a
614 /// `Some(value)` if so.
615 pub fn as_const(&self, bits: u16) -> Option<u64> {
616 match self {
617 Fact::Range {
618 bit_width,
619 min,
620 max,
621 } if *bit_width == bits && min == max => Some(*min),
622 _ => None,
623 }
624 }
625
626 /// Is this fact a single-value range with a symbolic Expr?
627 pub fn as_symbol(&self) -> Option<&Expr> {
628 match self {
629 Fact::DynamicRange { min, max, .. } if min == max => Some(min),
630 _ => None,
631 }
632 }
633
634 /// Merge two facts. We take the *intersection*: that is, we know
635 /// both facts to be true, so we can intersect ranges. (This
636 /// differs from the usual static analysis approach, where we are
637 /// merging multiple possibilities into a generalized / widened
638 /// fact. We want to narrow here.)
639 pub fn intersect(a: &Fact, b: &Fact) -> Fact {
640 match (a, b) {
641 (
642 Fact::Range {
643 bit_width: bw_lhs,
644 min: min_lhs,
645 max: max_lhs,
646 },
647 Fact::Range {
648 bit_width: bw_rhs,
649 min: min_rhs,
650 max: max_rhs,
651 },
652 ) if bw_lhs == bw_rhs && max_lhs >= min_rhs && max_rhs >= min_lhs => Fact::Range {
653 bit_width: *bw_lhs,
654 min: std::cmp::max(*min_lhs, *min_rhs),
655 max: std::cmp::min(*max_lhs, *max_rhs),
656 },
657
658 (
659 Fact::DynamicRange {
660 bit_width: bw_lhs,
661 min: min_lhs,
662 max: max_lhs,
663 },
664 Fact::DynamicRange {
665 bit_width: bw_rhs,
666 min: min_rhs,
667 max: max_rhs,
668 },
669 ) if bw_lhs == bw_rhs && Expr::le(min_rhs, max_lhs) && Expr::le(min_lhs, max_rhs) => {
670 Fact::DynamicRange {
671 bit_width: *bw_lhs,
672 min: Expr::max(min_lhs, min_rhs),
673 max: Expr::min(max_lhs, max_rhs),
674 }
675 }
676
677 (
678 Fact::Mem {
679 ty: ty_lhs,
680 min_offset: min_offset_lhs,
681 max_offset: max_offset_lhs,
682 nullable: nullable_lhs,
683 },
684 Fact::Mem {
685 ty: ty_rhs,
686 min_offset: min_offset_rhs,
687 max_offset: max_offset_rhs,
688 nullable: nullable_rhs,
689 },
690 ) if ty_lhs == ty_rhs
691 && max_offset_lhs >= min_offset_rhs
692 && max_offset_rhs >= min_offset_lhs =>
693 {
694 Fact::Mem {
695 ty: *ty_lhs,
696 min_offset: std::cmp::max(*min_offset_lhs, *min_offset_rhs),
697 max_offset: std::cmp::min(*max_offset_lhs, *max_offset_rhs),
698 nullable: *nullable_lhs && *nullable_rhs,
699 }
700 }
701
702 (
703 Fact::DynamicMem {
704 ty: ty_lhs,
705 min: min_lhs,
706 max: max_lhs,
707 nullable: null_lhs,
708 },
709 Fact::DynamicMem {
710 ty: ty_rhs,
711 min: min_rhs,
712 max: max_rhs,
713 nullable: null_rhs,
714 },
715 ) if ty_lhs == ty_rhs && Expr::le(min_rhs, max_lhs) && Expr::le(min_lhs, max_rhs) => {
716 Fact::DynamicMem {
717 ty: *ty_lhs,
718 min: Expr::max(min_lhs, min_rhs),
719 max: Expr::min(max_lhs, max_rhs),
720 nullable: *null_lhs && *null_rhs,
721 }
722 }
723
724 _ => Fact::Conflict,
725 }
726 }
727}
728
729macro_rules! ensure {
730 ( $condition:expr, $err:tt $(,)? ) => {
731 if !$condition {
732 return Err(PccError::$err);
733 }
734 };
735}
736
737macro_rules! bail {
738 ( $err:tt ) => {{
739 return Err(PccError::$err);
740 }};
741}
742
743/// The two kinds of inequalities: "strict" (`<`, `>`) and "loose"
744/// (`<=`, `>=`), the latter of which admit equality.
745#[derive(Clone, Copy, Debug, PartialEq, Eq)]
746pub enum InequalityKind {
747 /// Strict inequality: {less,greater}-than.
748 Strict,
749 /// Loose inequality: {less,greater}-than-or-equal.
750 Loose,
751}
752
753/// A "context" in which we can evaluate and derive facts. This
754/// context carries environment/global properties, such as the machine
755/// pointer width.
756pub struct FactContext<'a> {
757 function: &'a ir::Function,
758 pointer_width: u16,
759}
760
761impl<'a> FactContext<'a> {
762 /// Create a new "fact context" in which to evaluate facts.
763 pub fn new(function: &'a ir::Function, pointer_width: u16) -> Self {
764 FactContext {
765 function,
766 pointer_width,
767 }
768 }
769
770 /// Computes whether `lhs` "subsumes" (implies) `rhs`.
771 pub fn subsumes(&self, lhs: &Fact, rhs: &Fact) -> bool {
772 match (lhs, rhs) {
773 // Reflexivity.
774 (l, r) if l == r => true,
775
776 (
777 Fact::Range {
778 bit_width: bw_lhs,
779 min: min_lhs,
780 max: max_lhs,
781 },
782 Fact::Range {
783 bit_width: bw_rhs,
784 min: min_rhs,
785 max: max_rhs,
786 },
787 ) => {
788 // If the bitwidths we're claiming facts about are the
789 // same, or the left-hand-side makes a claim about a
790 // wider bitwidth, and if the right-hand-side range is
791 // larger than the left-hand-side range, than the LHS
792 // subsumes the RHS.
793 //
794 // In other words, we can always expand the claimed
795 // possible value range.
796 bw_lhs >= bw_rhs && max_lhs <= max_rhs && min_lhs >= min_rhs
797 }
798
799 (
800 Fact::DynamicRange {
801 bit_width: bw_lhs,
802 min: min_lhs,
803 max: max_lhs,
804 },
805 Fact::DynamicRange {
806 bit_width: bw_rhs,
807 min: min_rhs,
808 max: max_rhs,
809 },
810 ) => {
811 // Nearly same as above, but with dynamic-expression
812 // comparisons. Note that we require equal bitwidths
813 // here: unlike in the static case, we don't have
814 // fixed values for min and max, so we can't lean on
815 // the well-formedness requirements of the static
816 // ranges fitting within the bit-width max.
817 bw_lhs == bw_rhs && Expr::le(max_lhs, max_rhs) && Expr::le(min_rhs, min_lhs)
818 }
819
820 (
821 Fact::Mem {
822 ty: ty_lhs,
823 min_offset: min_offset_lhs,
824 max_offset: max_offset_lhs,
825 nullable: nullable_lhs,
826 },
827 Fact::Mem {
828 ty: ty_rhs,
829 min_offset: min_offset_rhs,
830 max_offset: max_offset_rhs,
831 nullable: nullable_rhs,
832 },
833 ) => {
834 ty_lhs == ty_rhs
835 && max_offset_lhs <= max_offset_rhs
836 && min_offset_lhs >= min_offset_rhs
837 && (*nullable_lhs || !*nullable_rhs)
838 }
839
840 (
841 Fact::DynamicMem {
842 ty: ty_lhs,
843 min: min_lhs,
844 max: max_lhs,
845 nullable: nullable_lhs,
846 },
847 Fact::DynamicMem {
848 ty: ty_rhs,
849 min: min_rhs,
850 max: max_rhs,
851 nullable: nullable_rhs,
852 },
853 ) => {
854 ty_lhs == ty_rhs
855 && Expr::le(max_lhs, max_rhs)
856 && Expr::le(min_rhs, min_lhs)
857 && (*nullable_lhs || !*nullable_rhs)
858 }
859
860 // Constant zero subsumes nullable DynamicMem pointers.
861 (
862 Fact::Range {
863 bit_width,
864 min: 0,
865 max: 0,
866 },
867 Fact::DynamicMem { nullable: true, .. },
868 ) if *bit_width == self.pointer_width => true,
869
870 // Any fact subsumes a Def, because the Def makes no
871 // claims about the actual value (it ties a symbol to that
872 // value, but the value is fed to the symbol, not the
873 // other way around).
874 (_, Fact::Def { .. }) => true,
875
876 _ => false,
877 }
878 }
879
880 /// Computes whether the optional fact `lhs` subsumes (implies)
881 /// the optional fact `lhs`. A `None` never subsumes any fact, and
882 /// is always subsumed by any fact at all (or no fact).
883 pub fn subsumes_fact_optionals(&self, lhs: Option<&Fact>, rhs: Option<&Fact>) -> bool {
884 match (lhs, rhs) {
885 (None, None) => true,
886 (Some(_), None) => true,
887 (None, Some(_)) => false,
888 (Some(lhs), Some(rhs)) => self.subsumes(lhs, rhs),
889 }
890 }
891
892 /// Computes whatever fact can be known about the sum of two
893 /// values with attached facts. The add is performed to the given
894 /// bit-width. Note that this is distinct from the machine or
895 /// pointer width: e.g., many 64-bit machines can still do 32-bit
896 /// adds that wrap at 2^32.
897 pub fn add(&self, lhs: &Fact, rhs: &Fact, add_width: u16) -> Option<Fact> {
898 let result = match (lhs, rhs) {
899 (
900 Fact::Range {
901 bit_width: bw_lhs,
902 min: min_lhs,
903 max: max_lhs,
904 },
905 Fact::Range {
906 bit_width: bw_rhs,
907 min: min_rhs,
908 max: max_rhs,
909 },
910 ) if bw_lhs == bw_rhs && add_width >= *bw_lhs => {
911 let computed_min = min_lhs.checked_add(*min_rhs)?;
912 let computed_max = max_lhs.checked_add(*max_rhs)?;
913 let computed_max = std::cmp::min(max_value_for_width(add_width), computed_max);
914 Some(Fact::Range {
915 bit_width: *bw_lhs,
916 min: computed_min,
917 max: computed_max,
918 })
919 }
920
921 (
922 Fact::Range {
923 bit_width: bw_max,
924 min,
925 max,
926 },
927 Fact::Mem {
928 ty,
929 min_offset,
930 max_offset,
931 nullable,
932 },
933 )
934 | (
935 Fact::Mem {
936 ty,
937 min_offset,
938 max_offset,
939 nullable,
940 },
941 Fact::Range {
942 bit_width: bw_max,
943 min,
944 max,
945 },
946 ) if *bw_max >= self.pointer_width
947 && add_width >= *bw_max
948 && (!*nullable || *max == 0) =>
949 {
950 let min_offset = min_offset.checked_add(*min)?;
951 let max_offset = max_offset.checked_add(*max)?;
952 Some(Fact::Mem {
953 ty: *ty,
954 min_offset,
955 max_offset,
956 nullable: false,
957 })
958 }
959
960 (
961 Fact::Range {
962 bit_width: bw_static,
963 min: min_static,
964 max: max_static,
965 },
966 Fact::DynamicRange {
967 bit_width: bw_dynamic,
968 min: min_dynamic,
969 max: max_dynamic,
970 },
971 )
972 | (
973 Fact::DynamicRange {
974 bit_width: bw_dynamic,
975 min: min_dynamic,
976 max: max_dynamic,
977 },
978 Fact::Range {
979 bit_width: bw_static,
980 min: min_static,
981 max: max_static,
982 },
983 ) if bw_static == bw_dynamic => {
984 let min = Expr::offset(min_dynamic, i64::try_from(*min_static).ok()?)?;
985 let max = Expr::offset(max_dynamic, i64::try_from(*max_static).ok()?)?;
986 Some(Fact::DynamicRange {
987 bit_width: *bw_dynamic,
988 min,
989 max,
990 })
991 }
992
993 (
994 Fact::DynamicMem {
995 ty,
996 min: min_mem,
997 max: max_mem,
998 nullable: false,
999 },
1000 Fact::DynamicRange {
1001 bit_width,
1002 min: min_range,
1003 max: max_range,
1004 },
1005 )
1006 | (
1007 Fact::DynamicRange {
1008 bit_width,
1009 min: min_range,
1010 max: max_range,
1011 },
1012 Fact::DynamicMem {
1013 ty,
1014 min: min_mem,
1015 max: max_mem,
1016 nullable: false,
1017 },
1018 ) if *bit_width == self.pointer_width => {
1019 let min = Expr::add(min_mem, min_range)?;
1020 let max = Expr::add(max_mem, max_range)?;
1021 Some(Fact::DynamicMem {
1022 ty: *ty,
1023 min,
1024 max,
1025 nullable: false,
1026 })
1027 }
1028
1029 (
1030 Fact::Mem {
1031 ty,
1032 min_offset,
1033 max_offset,
1034 nullable: false,
1035 },
1036 Fact::DynamicRange {
1037 bit_width,
1038 min: min_range,
1039 max: max_range,
1040 },
1041 )
1042 | (
1043 Fact::DynamicRange {
1044 bit_width,
1045 min: min_range,
1046 max: max_range,
1047 },
1048 Fact::Mem {
1049 ty,
1050 min_offset,
1051 max_offset,
1052 nullable: false,
1053 },
1054 ) if *bit_width == self.pointer_width => {
1055 let min = Expr::offset(min_range, i64::try_from(*min_offset).ok()?)?;
1056 let max = Expr::offset(max_range, i64::try_from(*max_offset).ok()?)?;
1057 Some(Fact::DynamicMem {
1058 ty: *ty,
1059 min,
1060 max,
1061 nullable: false,
1062 })
1063 }
1064
1065 (
1066 Fact::Range {
1067 bit_width: bw_static,
1068 min: min_static,
1069 max: max_static,
1070 },
1071 Fact::DynamicMem {
1072 ty,
1073 min: min_dynamic,
1074 max: max_dynamic,
1075 nullable,
1076 },
1077 )
1078 | (
1079 Fact::DynamicMem {
1080 ty,
1081 min: min_dynamic,
1082 max: max_dynamic,
1083 nullable,
1084 },
1085 Fact::Range {
1086 bit_width: bw_static,
1087 min: min_static,
1088 max: max_static,
1089 },
1090 ) if *bw_static == self.pointer_width && (!*nullable || *max_static == 0) => {
1091 let min = Expr::offset(min_dynamic, i64::try_from(*min_static).ok()?)?;
1092 let max = Expr::offset(max_dynamic, i64::try_from(*max_static).ok()?)?;
1093 Some(Fact::DynamicMem {
1094 ty: *ty,
1095 min,
1096 max,
1097 nullable: false,
1098 })
1099 }
1100
1101 _ => None,
1102 };
1103
1104 trace!("add: {lhs:?} + {rhs:?} -> {result:?}");
1105 result
1106 }
1107
1108 /// Computes the `uextend` of a value with the given facts.
1109 pub fn uextend(&self, fact: &Fact, from_width: u16, to_width: u16) -> Option<Fact> {
1110 if from_width == to_width {
1111 return Some(fact.clone());
1112 }
1113
1114 let result = match fact {
1115 // If the claim is already for a same-or-wider value and the min
1116 // and max are within range of the narrower value, we can
1117 // claim the same range.
1118 Fact::Range {
1119 bit_width,
1120 min,
1121 max,
1122 } if *bit_width >= from_width
1123 && *min <= max_value_for_width(from_width)
1124 && *max <= max_value_for_width(from_width) =>
1125 {
1126 Some(Fact::Range {
1127 bit_width: to_width,
1128 min: *min,
1129 max: *max,
1130 })
1131 }
1132
1133 // If the claim is a dynamic range for the from-width, we
1134 // can extend to the to-width.
1135 Fact::DynamicRange {
1136 bit_width,
1137 min,
1138 max,
1139 } if *bit_width == from_width => Some(Fact::DynamicRange {
1140 bit_width: to_width,
1141 min: min.clone(),
1142 max: max.clone(),
1143 }),
1144
1145 // If the claim is a definition of a value, we can say
1146 // that the output has a range of exactly that value.
1147 Fact::Def { value } => Some(Fact::value(to_width, *value)),
1148
1149 // Otherwise, we can at least claim that the value is
1150 // within the range of `from_width`.
1151 Fact::Range { .. } => Some(Fact::max_range_for_width_extended(from_width, to_width)),
1152
1153 _ => None,
1154 };
1155 trace!("uextend: fact {fact:?} from {from_width} to {to_width} -> {result:?}");
1156 result
1157 }
1158
1159 /// Computes the `sextend` of a value with the given facts.
1160 pub fn sextend(&self, fact: &Fact, from_width: u16, to_width: u16) -> Option<Fact> {
1161 match fact {
1162 // If we have a defined value in bits 0..bit_width, and
1163 // the MSB w.r.t. `from_width` is *not* set, then we can
1164 // do the same as `uextend`.
1165 Fact::Range {
1166 bit_width,
1167 // We can ignore `min`: it is always <= max in
1168 // unsigned terms, and we check max's LSB below.
1169 min: _,
1170 max,
1171 } if *bit_width == from_width && (*max & (1 << (*bit_width - 1)) == 0) => {
1172 self.uextend(fact, from_width, to_width)
1173 }
1174 _ => None,
1175 }
1176 }
1177
1178 /// Computes the bit-truncation of a value with the given fact.
1179 pub fn truncate(&self, fact: &Fact, from_width: u16, to_width: u16) -> Option<Fact> {
1180 if from_width == to_width {
1181 return Some(fact.clone());
1182 }
1183
1184 trace!(
1185 "truncate: fact {:?} from {} to {}",
1186 fact, from_width, to_width
1187 );
1188
1189 match fact {
1190 Fact::Range {
1191 bit_width,
1192 min,
1193 max,
1194 } if *bit_width == from_width => {
1195 let max_val = (1u64 << to_width) - 1;
1196 if *min <= max_val && *max <= max_val {
1197 Some(Fact::Range {
1198 bit_width: to_width,
1199 min: *min,
1200 max: *max,
1201 })
1202 } else {
1203 Some(Fact::Range {
1204 bit_width: to_width,
1205 min: 0,
1206 max: max_val,
1207 })
1208 }
1209 }
1210 _ => None,
1211 }
1212 }
1213
1214 /// Scales a value with a fact by a known constant.
1215 pub fn scale(&self, fact: &Fact, width: u16, factor: u32) -> Option<Fact> {
1216 let result = match fact {
1217 x if factor == 1 => Some(x.clone()),
1218
1219 Fact::Range {
1220 bit_width,
1221 min,
1222 max,
1223 } if *bit_width == width => {
1224 let min = min.checked_mul(u64::from(factor))?;
1225 let max = max.checked_mul(u64::from(factor))?;
1226 if *bit_width < 64 && max > max_value_for_width(width) {
1227 return None;
1228 }
1229 Some(Fact::Range {
1230 bit_width: *bit_width,
1231 min,
1232 max,
1233 })
1234 }
1235 _ => None,
1236 };
1237 trace!("scale: {fact:?} * {factor} at width {width} -> {result:?}");
1238 result
1239 }
1240
1241 /// Left-shifts a value with a fact by a known constant.
1242 pub fn shl(&self, fact: &Fact, width: u16, amount: u16) -> Option<Fact> {
1243 if amount >= 32 {
1244 return None;
1245 }
1246 let factor: u32 = 1 << amount;
1247 self.scale(fact, width, factor)
1248 }
1249
1250 /// Offsets a value with a fact by a known amount.
1251 pub fn offset(&self, fact: &Fact, width: u16, offset: i64) -> Option<Fact> {
1252 if offset == 0 {
1253 return Some(fact.clone());
1254 }
1255
1256 let compute_offset = |base: u64| -> Option<u64> {
1257 if offset >= 0 {
1258 base.checked_add(u64::try_from(offset).unwrap())
1259 } else {
1260 base.checked_sub(u64::try_from(-offset).unwrap())
1261 }
1262 };
1263
1264 let result = match fact {
1265 Fact::Range {
1266 bit_width,
1267 min,
1268 max,
1269 } if *bit_width == width => {
1270 let min = compute_offset(*min)?;
1271 let max = compute_offset(*max)?;
1272 Some(Fact::Range {
1273 bit_width: *bit_width,
1274 min,
1275 max,
1276 })
1277 }
1278 Fact::DynamicRange {
1279 bit_width,
1280 min,
1281 max,
1282 } if *bit_width == width => {
1283 let min = Expr::offset(min, offset)?;
1284 let max = Expr::offset(max, offset)?;
1285 Some(Fact::DynamicRange {
1286 bit_width: *bit_width,
1287 min,
1288 max,
1289 })
1290 }
1291 Fact::Mem {
1292 ty,
1293 min_offset: mem_min_offset,
1294 max_offset: mem_max_offset,
1295 nullable: false,
1296 } => {
1297 let min_offset = compute_offset(*mem_min_offset)?;
1298 let max_offset = compute_offset(*mem_max_offset)?;
1299 Some(Fact::Mem {
1300 ty: *ty,
1301 min_offset,
1302 max_offset,
1303 nullable: false,
1304 })
1305 }
1306 Fact::DynamicMem {
1307 ty,
1308 min,
1309 max,
1310 nullable: false,
1311 } => {
1312 let min = Expr::offset(min, offset)?;
1313 let max = Expr::offset(max, offset)?;
1314 Some(Fact::DynamicMem {
1315 ty: *ty,
1316 min,
1317 max,
1318 nullable: false,
1319 })
1320 }
1321 _ => None,
1322 };
1323 trace!("offset: {fact:?} + {offset} in width {width} -> {result:?}");
1324 result
1325 }
1326
1327 /// Check that accessing memory via a pointer with this fact, with
1328 /// a memory access of the given size, is valid.
1329 ///
1330 /// If valid, returns the memory type and offset into that type
1331 /// that this address accesses, if known, or `None` if the range
1332 /// doesn't constrain the access to exactly one location.
1333 fn check_address(&self, fact: &Fact, size: u32) -> PccResult<Option<(ir::MemoryType, u64)>> {
1334 trace!("check_address: fact {:?} size {}", fact, size);
1335 match fact {
1336 Fact::Mem {
1337 ty,
1338 min_offset,
1339 max_offset,
1340 nullable: _,
1341 } => {
1342 let end_offset: u64 = max_offset
1343 .checked_add(u64::from(size))
1344 .ok_or(PccError::Overflow)?;
1345 match &self.function.memory_types[*ty] {
1346 ir::MemoryTypeData::Struct { size, .. }
1347 | ir::MemoryTypeData::Memory { size } => {
1348 ensure!(end_offset <= *size, OutOfBounds)
1349 }
1350 ir::MemoryTypeData::DynamicMemory { .. } => bail!(OutOfBounds),
1351 ir::MemoryTypeData::Empty => bail!(OutOfBounds),
1352 }
1353 let specific_ty_and_offset = if min_offset == max_offset {
1354 Some((*ty, *min_offset))
1355 } else {
1356 None
1357 };
1358 Ok(specific_ty_and_offset)
1359 }
1360 Fact::DynamicMem {
1361 ty,
1362 min: _,
1363 max:
1364 Expr {
1365 base: BaseExpr::GlobalValue(max_gv),
1366 offset: max_offset,
1367 },
1368 nullable: _,
1369 } => match &self.function.memory_types[*ty] {
1370 ir::MemoryTypeData::DynamicMemory {
1371 gv,
1372 size: mem_static_size,
1373 } if gv == max_gv => {
1374 let end_offset = max_offset
1375 .checked_add(i64::from(size))
1376 .ok_or(PccError::Overflow)?;
1377 let mem_static_size =
1378 i64::try_from(*mem_static_size).map_err(|_| PccError::Overflow)?;
1379 ensure!(end_offset <= mem_static_size, OutOfBounds);
1380 Ok(None)
1381 }
1382 _ => bail!(OutOfBounds),
1383 },
1384 _ => bail!(OutOfBounds),
1385 }
1386 }
1387
1388 /// Get the access struct field, if any, by a pointer with the
1389 /// given fact and an access of the given type.
1390 pub fn struct_field<'b>(
1391 &'b self,
1392 fact: &Fact,
1393 access_ty: ir::Type,
1394 ) -> PccResult<Option<&'b ir::MemoryTypeField>> {
1395 let (ty, offset) = match self.check_address(fact, access_ty.bytes())? {
1396 Some((ty, offset)) => (ty, offset),
1397 None => return Ok(None),
1398 };
1399
1400 if let ir::MemoryTypeData::Struct { fields, .. } = &self.function.memory_types[ty] {
1401 let field = fields
1402 .iter()
1403 .find(|field| field.offset == offset)
1404 .ok_or(PccError::InvalidFieldOffset)?;
1405 if field.ty != access_ty {
1406 bail!(BadFieldType);
1407 }
1408 Ok(Some(field))
1409 } else {
1410 // Access to valid memory, but not a struct: no facts can be attached to the result.
1411 Ok(None)
1412 }
1413 }
1414
1415 /// Check a load, and determine what fact, if any, the result of the load might have.
1416 pub fn load<'b>(&'b self, fact: &Fact, access_ty: ir::Type) -> PccResult<Option<&'b Fact>> {
1417 Ok(self
1418 .struct_field(fact, access_ty)?
1419 .and_then(|field| field.fact()))
1420 }
1421
1422 /// Check a store.
1423 pub fn store(
1424 &self,
1425 fact: &Fact,
1426 access_ty: ir::Type,
1427 data_fact: Option<&Fact>,
1428 ) -> PccResult<()> {
1429 if let Some(field) = self.struct_field(fact, access_ty)? {
1430 // If it's a read-only field, disallow.
1431 if field.readonly {
1432 bail!(WriteToReadOnlyField);
1433 }
1434 // Check that the fact on the stored data subsumes the field's fact.
1435 if !self.subsumes_fact_optionals(data_fact, field.fact()) {
1436 bail!(InvalidStoredFact);
1437 }
1438 }
1439 Ok(())
1440 }
1441
1442 /// Apply a known inequality to rewrite dynamic bounds using transitivity, if possible.
1443 ///
1444 /// Given that `lhs >= rhs` (if not `strict`) or `lhs > rhs` (if
1445 /// `strict`), update `fact`.
1446 pub fn apply_inequality(
1447 &self,
1448 fact: &Fact,
1449 lhs: &Fact,
1450 rhs: &Fact,
1451 kind: InequalityKind,
1452 ) -> Fact {
1453 let result = match (
1454 lhs.as_symbol(),
1455 lhs.as_const(self.pointer_width)
1456 .and_then(|k| i64::try_from(k).ok()),
1457 rhs.as_symbol(),
1458 fact,
1459 ) {
1460 (
1461 Some(lhs),
1462 None,
1463 Some(rhs),
1464 Fact::DynamicMem {
1465 ty,
1466 min,
1467 max,
1468 nullable,
1469 },
1470 ) if rhs.base == max.base => {
1471 let strict_offset = match kind {
1472 InequalityKind::Strict => 1,
1473 InequalityKind::Loose => 0,
1474 };
1475 if let Some(offset) = max
1476 .offset
1477 .checked_add(lhs.offset)
1478 .and_then(|x| x.checked_sub(rhs.offset))
1479 .and_then(|x| x.checked_sub(strict_offset))
1480 {
1481 let new_max = Expr {
1482 base: lhs.base.clone(),
1483 offset,
1484 };
1485 Fact::DynamicMem {
1486 ty: *ty,
1487 min: min.clone(),
1488 max: new_max,
1489 nullable: *nullable,
1490 }
1491 } else {
1492 fact.clone()
1493 }
1494 }
1495
1496 (
1497 None,
1498 Some(lhs_const),
1499 Some(rhs),
1500 Fact::DynamicMem {
1501 ty,
1502 min: _,
1503 max,
1504 nullable,
1505 },
1506 ) if rhs.base == max.base => {
1507 let strict_offset = match kind {
1508 InequalityKind::Strict => 1,
1509 InequalityKind::Loose => 0,
1510 };
1511 if let Some(offset) = max
1512 .offset
1513 .checked_add(lhs_const)
1514 .and_then(|x| x.checked_sub(rhs.offset))
1515 .and_then(|x| x.checked_sub(strict_offset))
1516 {
1517 Fact::Mem {
1518 ty: *ty,
1519 min_offset: 0,
1520 max_offset: u64::try_from(offset).unwrap_or(0),
1521 nullable: *nullable,
1522 }
1523 } else {
1524 fact.clone()
1525 }
1526 }
1527
1528 _ => fact.clone(),
1529 };
1530 trace!("apply_inequality({fact:?}, {lhs:?}, {rhs:?}, {kind:?} -> {result:?}");
1531 result
1532 }
1533
1534 /// Compute the union of two facts, if possible.
1535 pub fn union(&self, lhs: &Fact, rhs: &Fact) -> Option<Fact> {
1536 let result = match (lhs, rhs) {
1537 (lhs, rhs) if lhs == rhs => Some(lhs.clone()),
1538
1539 (
1540 Fact::DynamicMem {
1541 ty: ty_lhs,
1542 min: min_lhs,
1543 max: max_lhs,
1544 nullable: nullable_lhs,
1545 },
1546 Fact::DynamicMem {
1547 ty: ty_rhs,
1548 min: min_rhs,
1549 max: max_rhs,
1550 nullable: nullable_rhs,
1551 },
1552 ) if ty_lhs == ty_rhs => Some(Fact::DynamicMem {
1553 ty: *ty_lhs,
1554 min: Expr::min(min_lhs, min_rhs),
1555 max: Expr::max(max_lhs, max_rhs),
1556 nullable: *nullable_lhs || *nullable_rhs,
1557 }),
1558
1559 (
1560 Fact::Range {
1561 bit_width: bw_const,
1562 min: 0,
1563 max: 0,
1564 },
1565 Fact::DynamicMem {
1566 ty,
1567 min,
1568 max,
1569 nullable: _,
1570 },
1571 )
1572 | (
1573 Fact::DynamicMem {
1574 ty,
1575 min,
1576 max,
1577 nullable: _,
1578 },
1579 Fact::Range {
1580 bit_width: bw_const,
1581 min: 0,
1582 max: 0,
1583 },
1584 ) if *bw_const == self.pointer_width => Some(Fact::DynamicMem {
1585 ty: *ty,
1586 min: min.clone(),
1587 max: max.clone(),
1588 nullable: true,
1589 }),
1590
1591 (
1592 Fact::Range {
1593 bit_width: bw_const,
1594 min: 0,
1595 max: 0,
1596 },
1597 Fact::Mem {
1598 ty,
1599 min_offset,
1600 max_offset,
1601 nullable: _,
1602 },
1603 )
1604 | (
1605 Fact::Mem {
1606 ty,
1607 min_offset,
1608 max_offset,
1609 nullable: _,
1610 },
1611 Fact::Range {
1612 bit_width: bw_const,
1613 min: 0,
1614 max: 0,
1615 },
1616 ) if *bw_const == self.pointer_width => Some(Fact::Mem {
1617 ty: *ty,
1618 min_offset: *min_offset,
1619 max_offset: *max_offset,
1620 nullable: true,
1621 }),
1622
1623 _ => None,
1624 };
1625 trace!("union({lhs:?}, {rhs:?}) -> {result:?}");
1626 result
1627 }
1628}
1629
1630fn max_value_for_width(bits: u16) -> u64 {
1631 assert!(bits <= 64);
1632 if bits == 64 {
1633 u64::MAX
1634 } else {
1635 (1u64 << bits) - 1
1636 }
1637}
1638
1639/// Top-level entry point after compilation: this checks the facts in
1640/// VCode.
1641pub fn check_vcode_facts<B: LowerBackend + TargetIsa>(
1642 f: &ir::Function,
1643 vcode: &mut VCode<B::MInst>,
1644 backend: &B,
1645) -> PccResult<()> {
1646 let ctx = FactContext::new(f, backend.triple().pointer_width().unwrap().bits().into());
1647
1648 // Check that individual instructions are valid according to input
1649 // facts, and support the stated output facts.
1650 for block in 0..vcode.num_blocks() {
1651 let block = BlockIndex::new(block);
1652 let mut flow_state = B::FactFlowState::default();
1653 for inst in vcode.block_insns(block).iter() {
1654 // Check any output facts on this inst.
1655 if let Err(e) = backend.check_fact(&ctx, vcode, inst, &mut flow_state) {
1656 log::info!("Error checking instruction: {:?}", vcode[inst]);
1657 return Err(e);
1658 }
1659
1660 // If this is a branch, check that all block arguments subsume
1661 // the assumed facts on the blockparams of successors.
1662 if vcode.is_branch(inst) {
1663 for (succ_idx, succ) in vcode.block_succs(block).iter().enumerate() {
1664 for (arg, param) in vcode
1665 .branch_blockparams(block, inst, succ_idx)
1666 .iter()
1667 .zip(vcode.block_params(*succ).iter())
1668 {
1669 let arg_fact = vcode.vreg_fact(*arg);
1670 let param_fact = vcode.vreg_fact(*param);
1671 if !ctx.subsumes_fact_optionals(arg_fact, param_fact) {
1672 return Err(PccError::UnsupportedBlockparam);
1673 }
1674 }
1675 }
1676 }
1677 }
1678 }
1679 Ok(())
1680}