differential-datalog
differential-datalog copied to clipboard
Fix unsoundness in DDValue traits
The implementations of PartialEq
, PartialOrd
and PartialOrd
for DDValue
(seen here) are unsound since they allow what's essentially transmuting types into the incorrect type and using them with an innocuous ==
or <
call. To fix this the trait implementations should have checks added to them and new *_unchecked()
methods (eg. .partial_eq_unchecked()
) should be added and used within generated code, since generated code statically knows the types of things that will be compared against each other (still with the debug_assert!()
s for posterity's sake)
Problem is, these traits are used internally by DD, which cannot be told to use our custom methods instead.
That is very unfortunate and complicates things significantly. Do you think we could at least push the unsoundness back a level (and hopefully out of the range of normal users) by directly implementing the exposed DD traits such as PartialOrder
?
Not sure I understand. Any value passed to DD must implement Ord
, and hence PartialOrd
and Eq
: https://docs.rs/differential-dataflow/0.11.0/differential_dataflow/trait.Data.html
There's probably a way to add another wrapper around DDValue with unsafe implementation of Ord
and make sure that we strip this wrapper before returning the value to the user. Or we could go in the other direction and add a safe wrapper around unsafe DDValue
.
I have a partial solution that allows users to be checked and internals not to be
// This is what is currently DDValue would become
struct DDValueInner {
...
}
#[repr(transparent)] // Allows soundly transmuting between a `DDValue<Checked>` and `DDValue<Unchecked>`
pub struct DDValue<C: DDlogChecked = Checked>(
DDValue,
PhantomData<C>,
);
impl PartialEq for DDValue<Checked> {
fn eq(&self, other: &Other) -> bool {
if self.type_id() == other.type_id() {
...
} else {
panic!();
}
}
}
impl PartialEq for DDValue<Unchecked> {
fn eq(&self, other: &Other) -> bool {
...
}
}
pub struct Checked;
pub struct Unchecked;
mod sealed {
use super::{Checked, Unchecked};
pub trait DDlogChecked {}
impl DDlogChecked for Checked {}
impl DDlogChecked for Unchecked {}
}
Then we make our user-facing apis return DDValue<Checked>
and internally DDValue<Unchecked>
s are moved around, used and stored