Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proof-carrying code: change range facts to be more general. #7965

Draft
wants to merge 5 commits into
base: main
Choose a base branch
from
Draft

Proof-carrying code: change range facts to be more general. #7965

Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
0bda5f6
Update PCC test to expose failure.
cfallin Nov 4, 2023
97b2864
Proof-carrying code: change range facts to be more general.
cfallin Feb 20, 2024
995509c
Fix pcc_memory test on aarch64: uextending a Def has an upper bound o…
cfallin Feb 20, 2024
3650d08
Review feedback: remove Expr/BaseExpr distinction.
cfallin Feb 21, 2024
70c0ff6
Some enhancements to derivation rules from testing:
cfallin Feb 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
Update PCC test to expose failure.
  • Loading branch information
@cfallin
cfallin committed Feb 20, 2024
commit 0bda5f63699de836f232a0dc19e38c64a755ad3c
123 changes: 26 additions & 97 deletions tests/pcc_memory.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,132 +8,44 @@ mod pcc_memory_tests {

const TESTS: &'static [&'static str] = &[
r#"
(module
(memory 1 1)
(func (param i32)
local.get 0
i32.load8_u
drop))
drop
"#,
r#"
(module
(memory 1 1)
(func (param i32)
local.get 0
i32.load8_u offset=0x10000
drop))
drop
"#,
r#"
(module
(memory 1 1)
(func (param i32)
local.get 0
i32.load16_u
drop))
drop
"#,
r#"
(module
(memory 1 1)
(func (param i32)
local.get 0
i32.load16_u offset=0x10000
drop))
drop
"#,
r#"
(module
(memory 1 1)
(func (param i32)
local.get 0
i32.load
drop))
drop
"#,
r#"
(module
(memory 1 1)
(func (param i32)
local.get 0
i32.load offset=0x10000
drop))
drop
"#,
r#"
(module
(memory 1 1)
(func (param i32)
local.get 0
i64.load
drop))
drop
"#,
r#"
(module
(memory 1 1)
(func (param i32)
local.get 0
i64.load offset=0x10000
drop))
"#,
r#"
(module
(memory 10 20)
(func (param i32)
local.get 0
i32.load8_u
drop))
"#,
r#"
(module
(memory 10 20)
(func (param i32)
local.get 0
i32.load8_u offset=0x10000
drop))
"#,
r#"
(module
(memory 10 20)
(func (param i32)
local.get 0
i32.load16_u
drop))
"#,
r#"
(module
(memory 10 20)
(func (param i32)
local.get 0
i32.load16_u offset=0x10000
drop))
"#,
r#"
(module
(memory 10 20)
(func (param i32)
local.get 0
i32.load
drop))
"#,
r#"
(module
(memory 10 20)
(func (param i32)
local.get 0
i32.load offset=0x10000
drop))
"#,
r#"
(module
(memory 10 20)
(func (param i32)
local.get 0
i64.load
drop))
"#,
r#"
(module
(memory 10 20)
(func (param i32)
local.get 0
i64.load offset=0x10000
drop))
drop
"#,
];

Expand All @@ -145,7 +57,24 @@ mod pcc_memory_tests {
const MIB: u64 = 1024 * KIB;
const GIB: u64 = 1024 * MIB;

for &test in TESTS {
let mut bodies = vec![];
for (mem_min, mem_max) in [(1, 1), (10, 20)] {
for &snippet in TESTS {
bodies.push(format!(
"(module (memory {mem_min} {mem_max}) (func (param i32) {snippet}))"
));
}
let all_snippets = TESTS
.iter()
.map(|s| s.to_owned())
.collect::<Vec<_>>()
.join("\n");
bodies.push(format!(
"(module (memory {mem_min} {mem_max}) (func (param i32) {all_snippets}))"
));
}

for test in &bodies {
for static_memory_maximum_size in [0, 64 * KIB, 1 * MIB, 4 * GIB, 6 * GIB] {
for guard_size in [0, 64 * KIB, 2 * GIB] {
for enable_spectre in [true /* not yet supported by PCC: false */] {
Expand Down