Skip to content

Commit

Permalink
PCC: switch "max" facts to "range" facts with two-sided ranges. (#7263)
Browse files Browse the repository at this point in the history 
This is needed for soundness when verifying accesses to memtype fields:
it's not enough to know that we're accessing an offset in `0` up to
`field_offset` inclusive, we need to know the access is actually to
`field_offset`.

The simplest change that validates this turned out to be the most
general one: making ranges two-sided rather than one-sided. The
transform is *mostly* mechanical, but a few new tests verify that ranges
are updated on both sides, and some fail-tests verify that "fuzzily
imprecise" pointers to struct fields fail to validate.
  • Loading branch information
@cfallin
cfallin authored Oct 17, 2023
1 parent d0b053e commit 39a33d2
Show file tree
Hide file tree
Showing 21 changed files with 335 additions and 243 deletions.
224 changes: 141 additions & 83 deletions cranelift/codegen/src/ir/pcc.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,36 +128,52 @@ pub enum PccError {
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
pub enum Fact {
/// A bitslice of a value (up to a bitwidth) is less than or equal
/// to a given maximum value.
/// A bitslice of a value (up to a bitwidth) is within the given
/// integer range.
///
/// The slicing behavior is needed because this fact can describe
/// both an SSA `Value`, whose entire value is well-defined, and a
/// `VReg` in VCode, whose bits beyond the type stored in that
/// register are don't-care (undefined).
ValueMax {
Range {
/// The bitwidth of bits we care about, from the LSB upward.
bit_width: u16,
/// The minimum value that the bitslice can take
/// (inclusive). The range is unsigned: the specified bits of
/// the actual value will be greater than or equal to this
/// value, as evaluated by an unsigned integer comparison.
min: u64,
/// The maximum value that the bitslice can take
/// (inclusive). The range is unsigned: the bits of the value
/// will be within the range `0..=max`.
/// (inclusive). The range is unsigned: the specified bits of
/// the actual value will be less than or equal to this value,
/// as evaluated by an unsigned integer comparison.
max: u64,
},

/// A pointer to a memory type.
Mem {
/// The memory type.
ty: ir::MemoryType,
/// The offset into the memory type.
offset: i64,
/// The minimum offset into the memory type, inclusive.
min_offset: u64,
/// The maximum offset into the memory type, inclusive.
max_offset: u64,
},
}

impl fmt::Display for Fact {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match self {
Fact::ValueMax { bit_width, max } => write!(f, "max({}, {:#x})", bit_width, max),
Fact::Mem { ty, offset } => write!(f, "mem({}, {:#x})", ty, offset),
Fact::Range {
bit_width,
min,
max,
} => write!(f, "range({}, {:#x}, {:#x})", bit_width, min, max),
Fact::Mem {
ty,
min_offset,
max_offset,
} => write!(f, "mem({}, {:#x}, {:#x})", ty, min_offset, max_offset),
}
}
}
Expand All @@ -166,20 +182,24 @@ impl Fact {
/// Try to infer a minimal fact for a value of the given IR type.
pub fn infer_from_type(ty: ir::Type) -> Option<&'static Self> {
static FACTS: [Fact; 4] = [
Fact::ValueMax {
Fact::Range {
bit_width: 8,
min: 0,
max: u8::MAX as u64,
},
Fact::ValueMax {
Fact::Range {
bit_width: 16,
min: 0,
max: u16::MAX as u64,
},
Fact::ValueMax {
Fact::Range {
bit_width: 32,
min: 0,
max: u32::MAX as u64,
},
Fact::ValueMax {
Fact::Range {
bit_width: 64,
min: 0,
max: u64::MAX,
},
];
Expand Down Expand Up @@ -231,24 +251,25 @@ impl<'a> FactContext<'a> {
(l, r) if l == r => true,

(
Fact::ValueMax {
Fact::Range {
bit_width: bw_lhs,
min: min_lhs,
max: max_lhs,
},
Fact::ValueMax {
Fact::Range {
bit_width: bw_rhs,
min: min_rhs,
max: max_rhs,
},
) => {
// If the bitwidths we're claiming facts about are the
// same, and if the value is less than or equal to
// `max_lhs`, and if `max_rhs` is less than `max_lhs`,
// then it is certainly less than or equal to
// `max_rhs`.
// same, and if the right-hand-side range is larger
// than the left-hand-side range, than the LHS
// subsumes the RHS.
//
// In other words, we can always expand the claimed
// possible value range.
bw_lhs == bw_rhs && max_lhs <= max_rhs
bw_lhs == bw_rhs && max_lhs <= max_rhs && min_lhs >= min_rhs
}

_ => false,
Expand All @@ -275,39 +296,58 @@ impl<'a> FactContext<'a> {
pub fn add(&self, lhs: &Fact, rhs: &Fact, add_width: u16) -> Option<Fact> {
match (lhs, rhs) {
(
Fact::ValueMax {
Fact::Range {
bit_width: bw_lhs,
max: lhs,
min: min_lhs,
max: max_lhs,
},
Fact::ValueMax {
Fact::Range {
bit_width: bw_rhs,
max: rhs,
min: min_rhs,
max: max_rhs,
},
) if bw_lhs == bw_rhs && add_width >= *bw_lhs => {
let computed_max = lhs.checked_add(*rhs)?;
let computed_min = min_lhs.checked_add(*min_rhs)?;
let computed_max = max_lhs.checked_add(*max_rhs)?;
let computed_max = std::cmp::min(max_value_for_width(add_width), computed_max);
Some(Fact::ValueMax {
Some(Fact::Range {
bit_width: *bw_lhs,
min: computed_min,
max: computed_max,
})
}

(
Fact::ValueMax {
Fact::Range {
bit_width: bw_max,
min,
max,
},
Fact::Mem { ty, offset },
Fact::Mem {
ty,
min_offset,
max_offset,
},
)
| (
Fact::Mem { ty, offset },
Fact::ValueMax {
Fact::Mem {
ty,
min_offset,
max_offset,
},
Fact::Range {
bit_width: bw_max,
min,
max,
},
) if *bw_max >= self.pointer_width && add_width >= *bw_max => {
let offset = offset.checked_add(i64::try_from(*max).ok()?)?;
Some(Fact::Mem { ty: *ty, offset })
let min_offset = min_offset.checked_add(*min)?;
let max_offset = max_offset.checked_add(*max)?;
Some(Fact::Mem {
ty: *ty,
min_offset,
max_offset,
})
}

_ => None,
Expand All @@ -322,14 +362,20 @@ impl<'a> FactContext<'a> {
// bit_width and from_bits are exactly contiguous, then we
// have defined values in 0..to_bits (and because this is
// a zero-extend, the max value is the same).
Fact::ValueMax { bit_width, max } if *bit_width == from_width => Some(Fact::ValueMax {
Fact::Range {
bit_width,
min,
max,
} if *bit_width == from_width => Some(Fact::Range {
bit_width: to_width,
min: *min,
max: *max,
}),
// Otherwise, we can at least claim that the value is
// within the range of `to_width`.
Fact::ValueMax { .. } => Some(Fact::ValueMax {
Fact::Range { .. } => Some(Fact::Range {
bit_width: to_width,
min: 0,
max: max_value_for_width(to_width),
}),
_ => None,
Expand All @@ -342,9 +388,13 @@ impl<'a> FactContext<'a> {
// If we have a defined value in bits 0..bit_width, and
// the MSB w.r.t. `from_width` is *not* set, then we can
// do the same as `uextend`.
Fact::ValueMax { bit_width, max }
if *bit_width == from_width && (*max & (1 << (*bit_width - 1)) == 0) =>
{
Fact::Range {
bit_width,
// We can ignore `min`: it is always <= max in
// unsigned terms, and we check max's LSB below.
min: _,
max,
} if *bit_width == from_width && (*max & (1 << (*bit_width - 1)) == 0) => {
self.uextend(fact, from_width, to_width)
}
_ => None,
Expand All @@ -353,23 +403,20 @@ impl<'a> FactContext<'a> {

/// Scales a value with a fact by a known constant.
pub fn scale(&self, fact: &Fact, width: u16, factor: u32) -> Option<Fact> {
// The minimal (loosest) fact we can claim: the value will be
// within the range implied by its bitwidth.
let minimal_fact = Fact::ValueMax {
bit_width: width,
max: max_value_for_width(width),
};
match fact {
Fact::ValueMax { bit_width, max } if *bit_width == width => {
let max = match max.checked_mul(u64::from(factor)) {
Some(max) => max,
None => return Some(minimal_fact),
};
Fact::Range {
bit_width,
min,
max,
} if *bit_width == width => {
let min = min.checked_mul(u64::from(factor))?;
let max = max.checked_mul(u64::from(factor))?;
if *bit_width < 64 && max > max_value_for_width(width) {
return Some(minimal_fact);
return None;
}
Some(Fact::ValueMax {
Some(Fact::Range {
bit_width: *bit_width,
min,
max,
})
}
Expand All @@ -388,36 +435,38 @@ impl<'a> FactContext<'a> {

/// Offsets a value with a fact by a known amount.
pub fn offset(&self, fact: &Fact, width: u16, offset: i64) -> Option<Fact> {
match fact {
Fact::ValueMax { bit_width, max } if *bit_width == width => {
// If we eventually support two-sided ranges, we can
// represent (0..n) + m -> ((0+m)..(n+m)). However,
// right now, all ranges start with zero, so any
// negative offset could underflow, and removes all
// claims of constrained range.
let offset = u64::try_from(offset).ok()?;

let max = match max.checked_add(offset) {
Some(max) => max,
None => {
return Some(Fact::ValueMax {
bit_width: width,
max: max_value_for_width(width),
})
}
};
// Any negative offset could underflow, and removes
// all claims of constrained range, so for now we only
// support positive offsets.
let offset = u64::try_from(offset).ok()?;

Some(Fact::ValueMax {
match fact {
Fact::Range {
bit_width,
min,
max,
} if *bit_width == width => {
let min = min.checked_add(offset)?;
let max = max.checked_add(offset)?;

Some(Fact::Range {
bit_width: *bit_width,
min,
max,
})
}
Fact::Mem {
ty,
offset: mem_offset,
min_offset: mem_min_offset,
max_offset: mem_max_offset,
} => {
let offset = mem_offset.checked_sub(offset)?;
Some(Fact::Mem { ty: *ty, offset })
let min_offset = mem_min_offset.checked_sub(offset)?;
let max_offset = mem_max_offset.checked_sub(offset)?;
Some(Fact::Mem {
ty: *ty,
min_offset,
max_offset,
})
}
_ => None,
}
Expand All @@ -427,23 +476,31 @@ impl<'a> FactContext<'a> {
/// a memory access of the given size, is valid.
///
/// If valid, returns the memory type and offset into that type
/// that this address accesses.
fn check_address(&self, fact: &Fact, size: u32) -> PccResult<(ir::MemoryType, i64)> {
/// that this address accesses, if known, or `None` if the range
/// doesn't constrain the access to exactly one location.
fn check_address(&self, fact: &Fact, size: u32) -> PccResult<Option<(ir::MemoryType, u64)>> {
match fact {
Fact::Mem { ty, offset } => {
let end_offset: i64 = offset
.checked_add(i64::from(size))
Fact::Mem {
ty,
min_offset,
max_offset,
} => {
let end_offset: u64 = max_offset
.checked_add(u64::from(size))
.ok_or(PccError::Overflow)?;
let end_offset: u64 =
u64::try_from(end_offset).map_err(|_| PccError::OutOfBounds)?;
match &self.function.memory_types[*ty] {
ir::MemoryTypeData::Struct { size, .. }
| ir::MemoryTypeData::Memory { size } => {
ensure!(end_offset <= *size, OutOfBounds)
}
ir::MemoryTypeData::Empty => bail!(OutOfBounds),
}
Ok((*ty, *offset))
let specific_ty_and_offset = if min_offset == max_offset {
Some((*ty, *min_offset))
} else {
None
};
Ok(specific_ty_and_offset)
}
_ => bail!(OutOfBounds),
}
Expand All @@ -456,9 +513,10 @@ impl<'a> FactContext<'a> {
fact: &Fact,
access_ty: ir::Type,
) -> PccResult<Option<&'b ir::MemoryTypeField>> {
let (ty, offset) = self.check_address(fact, access_ty.bytes())?;
let offset =
u64::try_from(offset).expect("valid access address cannot have a negative offset");
let (ty, offset) = match self.check_address(fact, access_ty.bytes())? {
Some((ty, offset)) => (ty, offset),
None => return Ok(None),
};

if let ir::MemoryTypeData::Struct { fields, .. } = &self.function.memory_types[ty] {
let field = fields
Expand Down
Loading

0 comments on commit 39a33d2

Please sign in to comment.