Skip to content

Commit

Permalink
PCC: verification primitives for dynamic range checks. (#7389)
Browse files Browse the repository at this point in the history
* PCC: add memory type and fact annotations needed for dynamic-memory validation.

* PCC: update dynamic fact kinds, add sketch of dynamic-mem case, and add parser.

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

* Working dynamic-range verification on x64 and aarch64.

* Fix x64 shll: output range according to bitwidth, not always-64-bit.

* Review feedback.

* Missing backtick in doc comment.

---------

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>
  • Loading branch information
cfallin and fitzgen authored Oct 27, 2023
1 parent f81e033 commit 2340dff
Show file tree
Hide file tree
Showing 12 changed files with 954 additions and 69 deletions.
19 changes: 14 additions & 5 deletions cranelift/codegen/src/ir/memtype.rs
Original file line number Diff line number Diff line change
Expand Up @@ -51,10 +51,6 @@
//!
//! Eventually we plan to also have:
//!
//! - A dynamic memory is an untyped blob of storage with a size given
//! by a global value (GV). This is otherwise just like the "static
//! memory" variant described above.
//!
//! - A dynamic array is a sequence of struct memory types, with a
//! length given by a global value (GV). This is useful to model,
//! e.g., tables.
Expand All @@ -67,7 +63,7 @@
//! field is not null (all zero bits).

use crate::ir::pcc::Fact;
use crate::ir::Type;
use crate::ir::{GlobalValue, Type};
use alloc::vec::Vec;

#[cfg(feature = "enable-serde")]
Expand Down Expand Up @@ -99,6 +95,15 @@ pub enum MemoryTypeData {
size: u64,
},

/// A dynamically-sized untyped blob of memory, with bound given
/// by a global value plus some static amount.
DynamicMemory {
/// Static part of size.
size: u64,
/// Dynamic part of size.
gv: GlobalValue,
},

/// A type with no size.
Empty,
}
Expand Down Expand Up @@ -135,6 +140,9 @@ impl std::fmt::Display for MemoryTypeData {
Self::Memory { size } => {
write!(f, "memory {size:#x}")
}
Self::DynamicMemory { size, gv } => {
write!(f, "dynamic_memory {}+{:#x}", gv, size)
}
Self::Empty => {
write!(f, "empty")
}
Expand Down Expand Up @@ -175,6 +183,7 @@ impl MemoryTypeData {
match self {
Self::Struct { size, .. } => Some(*size),
Self::Memory { size } => Some(*size),
Self::DynamicMemory { .. } => None,
Self::Empty => Some(0),
}
}
Expand Down
Loading

0 comments on commit 2340dff

Please sign in to comment.