libre-chip/cpu
2
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity

reduce formal proof depth to avoid z3 eating all our memory

Browse source
This commit is contained in:
Jacob Lifshay 2024-10-15 23:50:51 -07:00
parent b54e40561f
commit a305ad51b2
Signed by: programmerjake
SSH key fingerprint: SHA256:B1iRVvUJkvd7upMIiMqn6OyxvD2SgJkAH3ZnUOj6z+c
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
crates/cpu/src/reg_alloc/unit_free_regs_tracker.rs
View file

@ -131,17 +131,20 @@ mod tests {
alloc_at_once: NonZeroUsize, alloc_at_once: NonZeroUsize,
reg_num_width: usize, reg_num_width: usize,
) { ) {
let reg_count = 1usize << reg_num_width;
// enough time to completely allocate all regs, free whatever we please, // enough time to completely allocate all regs, free whatever we please,
// allocate one, then completely free the rest // allocate one, then completely free the rest
let history_len = (3 + 2 * (1 << reg_num_width)).max(5); let mut history_len = 1;
history_len += reg_count.div_ceil(alloc_at_once.get());
history_len += reg_count.div_ceil(free_at_once.get());
assert_formal( assert_formal(
format_args!( format_args!(
"test_unit_free_regs_tracker_{free_at_once}_{alloc_at_once}_{reg_num_width}" "test_unit_free_regs_tracker_{free_at_once}_{alloc_at_once}_{reg_num_width}"
), ),
unit_free_regs_tracker_test(free_at_once, alloc_at_once, reg_num_width, history_len), unit_free_regs_tracker_test(free_at_once, alloc_at_once, reg_num_width, history_len),
FormalMode::Prove, FormalMode::Prove,
history_len as u64 + 2, history_len as u64,
None, Some("z3"),
ExportOptions { ExportOptions {
simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts), simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
..ExportOptions::default() ..ExportOptions::default()