Spurious failure on harness from s2n-quic #2650
Assignees
Labels
[C] Bug
This is a bug. Something isn't working.
[F] Spurious Failure
Issues that cause Kani verification to fail despite the code being correct.
T-CBMC
Issue related to an existing CBMC issue
T-High Priority
Tag issues that have high priority
T-User
Tag user issues / requests
Comments
zhassan-aws
added
[C] Bug
|
Hi, I went as far back as kani 0.17.0 and cbmc 5.72.0 and the problem persists so this does not seem new. Looking at the trace, it appears that the pub struct F {
values: [u8; 2],
len: usize,
}
impl std::ops::Deref for F {
type Target = [u8];
fn deref(&self) -> &Self::Target {
&self.values[..self.len]
}
}
impl std::ops::DerefMut for F {
fn deref_mut(&mut self) -> &mut Self::Target {
&mut self.values[..self.len]
}
}
pub struct G {
values: [F; 2],
len: usize,
}
impl std::ops::Deref for G {
type Target = [F];
fn deref(&self) -> &Self::Target {
&self.values[..self.len]
}
}
impl std::ops::DerefMut for G {
fn deref_mut(&mut self) -> &mut Self::Target {
&mut self.values[..self.len]
}
}
//
// from = [[aaa][bbbbb][cc][ddddd]]
// to = [[xx][xxx][xxxxx][xxxxxxxxx]]
//
// result:
// to' = [[aa][abb][bbbcc][ddddddxxx]]
//
pub fn vectored_copy(from: &[F], to: &mut [F])
{
let mut from_index = 0;
let mut from_offset = 0;
let mut to_index = 0;
let mut to_offset = 0;
// iterate until we reach one of the ends
while from_index < from.len() && to_index < to.len() {
let f_from: &F = unsafe {
// Safety: this length is already checked in the while condition
debug_assert!(from.len() > from_index);
from.get_unchecked(from_index)
};
let f_to: &mut F = unsafe {
// Safety: this length is already checked in the while condition
debug_assert!(to.len() > to_index);
to.get_unchecked_mut(to_index)
};
// fails here with
let _dummy_from_index = from_index; // 1
let _dummy_from_offset = from_offset; // 0
let _dummy_to_index = to_index; // 1
let _dummy_to_offset = to_offset; // 0
let _dummy_to_len = f_to.len; // 18374686479671623680ul
// this should hold but does not because
// the output of to.get_unchecked_mut(to_index) is unconstrained
assert!(f_to.len <= 2);
// this fixes the problem downstream
kani::assume(f_to.len <= 2);
{
// copy the bytes in the current views
let u8_from: &[u8] = unsafe {
// Safety: the slice offsets are checked at the end of the while loop
debug_assert!(f_from.len() >= from_offset);
f_from.get_unchecked(from_offset..)
};
let u8_to: &mut [u8] = unsafe {
// Safety: the slice offsets are checked at the end of the while loop
debug_assert!(f_to.len() >= to_offset);
f_to.get_unchecked_mut(to_offset..)
};
let len = u8_from.len().min(u8_to.len());
unsafe {
// Safety: by using the min of the two lengths we will never exceed
// either slice's buffer
debug_assert!(u8_from.len() >= len);
debug_assert!(u8_to.len() >= len);
u8_to.get_unchecked_mut(..len)
.copy_from_slice(u8_from.get_unchecked(..len));
}
// increment the offsets
from_offset += len;
to_offset += len;
}
// check if the `from` is done
if f_from.len() == from_offset {
from_index += 1;
from_offset = 0;
}
// check if the `to` is done
if f_to.len() == to_offset {
to_index += 1;
to_offset = 0;
}
}
}
#[kani::proof]
#[kani::unwind(5)]
fn main() {
let ndlen = kani::any_where(|l| *l <= 2);
let from = G { values: [F { values: [255, 255], len: ndlen }, F { values: [255, 255], len: 2}], len: 2};
let mut to = G { values: [F { values: [255, 255], len: 1 }, F { values: [255, 255], len: 1}], len: 2};
vectored_copy(&from, &mut to);
}Looking at the This is the variable representing This is the variable representing the return value of The only constraint we have for it is of the form The variable that actually defines the return value of the function is this one: In the SSA it shows up as: So equation -4799 should have been this instead: Here is the relevant This looks like a CBMC bug, @tautschnig can you take a second look ? |
|
A slightly reduced version: use std::ops::{Deref, DerefMut};
pub fn vectored_copy<B>(from: &[&[u8]], to: &mut [B])
where
B: Deref<Target = [u8]> + DerefMut,
{
let mut from_index = 0;
let mut from_offset = 0;
let mut to_index = 0;
let mut to_offset = 0;
// iterate until we reach one of the ends
while from_index < from.len() && to_index < to.len() {
let from = unsafe {
from.get_unchecked(from_index)
};
let to = unsafe {
to.get_unchecked_mut(to_index)
};
{
// copy the bytes in the current views
let from = unsafe {
from.get_unchecked(from_offset..)
};
let to = unsafe {
to.get_unchecked_mut(to_offset..)
};
let len = from.len().min(to.len());
unsafe {
to.get_unchecked_mut(..len)
.copy_from_slice(from.get_unchecked(..len));
}
// increment the offsets
from_offset += len;
to_offset += len;
}
// check if the `from` is done
if from.len() == from_offset {
from_index += 1;
from_offset = 0;
}
// check if the `to` is done
if to.len() == to_offset {
to_index += 1;
to_offset = 0;
}
}
}
struct F {
values: [u8; 2],
len: usize,
}
impl std::ops::Deref for F {
type Target = [u8];
fn deref(&self) -> &Self::Target {
&self.values[..self.len]
}
}
impl std::ops::DerefMut for F {
fn deref_mut(&mut self) -> &mut Self::Target {
&mut self.values[..self.len]
}
}
struct G {
values: [F; 2],
_len: usize,
}
impl std::ops::Deref for G {
type Target = [F];
fn deref(&self) -> &Self::Target {
&self.values
}
}
impl std::ops::DerefMut for G {
fn deref_mut(&mut self) -> &mut Self::Target {
&mut self.values
}
}
#[kani::proof]
#[kani::unwind(5)]
fn main() {
let ndlen = kani::any_where(|l| *l == 2);
let from1 = [255, 255];
let from2 = [255, 255];
let from = [&from1[..ndlen], &from2[..]];
let mut to = G { values: [F { values: [255, 255], len: 1 }, F { values: [255, 255], len: 1}], _len: 2};
vectored_copy(&from, &mut to);
} |
|
@tautschnig full reproducer posted above |
4 tasks
|
This is caused by a bug in CBMC's handling of byte updates of non-constant width (which are generated from |
|
diffblue/cbmc#7855 was merged. This issue should get fixed once we get a new CBMC release. |
zhassan-aws
added a commit
that referenced
this issue
Sep 29, 2023
Upgrade CBMC version to latest (5.93.0). Resolves #2650
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This bug was reported by @camshaft on s2n-quic. I've extracted a stand-alone example for easy debugging:
using the following command line invocation:
with Kani version: a2a1e85
I expected to see this happen: Verification successful
Instead, this happened: Verification failed:
Running concrete playback using the following command:
generates the following test:
If I run this test, it doesn't fail:
Also, if I replace
ndlenin the harness with 2 as the playback test suggests and run Kani, verification succeeds:The text was updated successfully, but these errors were encountered: