Division with concrete and constant operands causes long verification times #2801

Activity

1. adpaco

   added

   [C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

   [E] PerformanceTrack performance improvement (Time / Memory / CPU)Track performance improvement (Time / Memory / CPU)

   T-CBMCIssue related to an existing CBMC issueIssue related to an existing CBMC issue

   on Oct 2, 2023
2. adpaco commented on Oct 3, 2023

   

   adpaco

   on Oct 3, 2023

   ContributorAuthor

   More actions

   From @remi-delmas-3000:

   It would be interesting to try changing that power of 10 constant with the nearest power of two, because then the operation degenerates into a right-shift operation with a constant shift value. Otherwise the only way to simplify things would be to expand the division circuit and propagate individual bits of the divisor, but symex does not see things at the bit level. The only other thing that could be said about the result of the division is that some top bytes might be pinned to true or false but not much more than that.

   actually tristate numbers can carry and propagate that type of byte-level information: https://arxiv.org/abs/2105.05398

   a bitvector is represented by two bitvectors (m, v), m tells you which bits are known to be constant and which bits are non-deterministic, and v gives the value of the constant bits
3. tautschnig

   self-assigned this

   on Oct 4, 2023
4. roypat commented on Oct 25, 2023

   

   roypat

   on Oct 25, 2023

   More actions

   Hey all,
   I think we managed to run into this one with firecracker/rust-vmm proofs in https://github.com/firecracker-microvm/firecracker/blob/main/src/vmm/src/devices/virtio/queue.rs. For example

   #[kani::proof]
   #[kani::unwind(2)]
   fn verify_write_slice() {
       const MEMORY_SIZE: usize = 1024;
   
       use vm_memory::{*, bitmap::*};
   
       let mut bitmap = Some(AtomicBitmap::default());
   
       let mut vec = kani::vec::exact_vec::<u8, MEMORY_SIZE>();
       let mut slice = unsafe {
           VolatileSlice::with_bitmap(vec.as_mut_ptr(), MEMORY_SIZE, bitmap.slice_at(0), None)
       };
       let value: i16 = 0;
   
       slice.write_slice(value.as_slice(), 1022);
   }

   is slow, but replacing 1022 in the final line with 0 causes verification to pass in under 1 second. Deep in vm-memory code we have https://github.com/rust-vmm/vm-memory/blob/07ab85360b26bf346770f540a1437bb4d4988fb0/src/bitmap/backend/atomic_bitmap.rs#L62-L80, where the first parameter will correspond to the second parameter of write_slice (e.g. 1022 or 0), and the second parameter will always be 2 (the length of the written slice, here 2 bytes because we're writing an i16). self.page_size at this point is always 4096, so only constants are involved in the arithmetic here.
5. adpaco

   added

   T-UserTag user issues / requestsTag user issues / requests

   on Oct 25, 2023
6. adpaco commented on Oct 25, 2023

   

   adpaco

   on Oct 25, 2023

   ContributorAuthor

   More actions

   Hey @roypat , thanks for letting us know about that!

   Do you have data on how long the execution takes for the unmodified harness?

   cc @tautschnig @feliperodri
7. roypat commented on Oct 26, 2023

   

   roypat

   on Oct 26, 2023

   More actions

   With the unmodified harness it takes around 71s. I've attached the logs from both a slow and a fast verification below:
   verification-fast.txt
   verification-slow.txt
   This was on a m6i.metal instance with kani 0.39.0, Amazon Linux 2023 (6.1.55-75.123.amzn2023.x86_64)

   👍React with 👍1Reacted by Adrian Palacios
8. feliperodri

   added the

   Bug

   issue type on Apr 1, 2026
9. feliperodri

   added this to the Extend the Capabilities of GOTO Verification Engines milestone on Nov 5, 2026