From d46e2746fd5702e79696606129a42bd094234507 Mon Sep 17 00:00:00 2001 From: remimimimimi Date: Thu, 22 May 2025 23:21:52 +0300 Subject: [PATCH] draft --- Cargo.toml | 3 + src/internal/arena.rs | 76 ++++++++++++++++++++ src/internal/id.rs | 3 +- src/internal/mapping.rs | 143 ++++++++++++++++++++++++++++++------- src/lib.rs | 3 + src/solver/clause.rs | 21 +++++- src/solver/decision_map.rs | 51 ++++++++++++- 7 files changed, 268 insertions(+), 32 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index b102dea7..06ef187e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -61,3 +61,6 @@ tracing-test = { version = "0.2.5", features = ["no-env-filter"] } tokio = { version = "1.42.0", features = ["time", "rt"] } resolvo = { path = ".", features = ["tokio", "version-ranges"] } serde_json = "1.0" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/src/internal/arena.rs b/src/internal/arena.rs index 2ec95a04..d113c9ef 100644 --- a/src/internal/arena.rs +++ b/src/internal/arena.rs @@ -217,3 +217,79 @@ impl<'a, TId: ArenaId, TValue> Iterator for ArenaIterMut<'a, TId, TValue> { } } } + +/// For testing purposes. +impl ArenaId for usize { + fn from_usize(x: usize) -> Self { + x + } + + fn to_usize(self) -> usize { + self + } +} + +#[cfg(kani)] +mod verification { + use super::*; + + #[kani::proof] + #[kani::unwind(3)] + fn arena_correct() { + // FIXME (some time later): Produce arbitrary arena. + let mut arena: Arena = Arena::new(); + let number_of_allocations: usize = kani::any(); + + kani::assume(number_of_allocations < 3); + + let values: Vec = kani::bounded_any::<_, 2>(); + + let ids: Vec = values.iter().map(|v| arena.alloc(*v)).collect::>(); + + for (i, id) in ids.into_iter().enumerate() { + assert_eq!(values.get(i), Some(&arena[id])); + arena[id] = !arena[id]; + assert_eq!(values.get(i).map(|x| !x), Some(arena[id])); + } + } + + #[kani::proof] + #[kani::unwind(3)] + fn arena_get_two_mut_correct() { + let mut arena: Arena = Arena::new(); + let number_of_allocations: u8 = kani::any(); + + kani::assume(number_of_allocations < 3); + + let values: Vec = kani::bounded_any::<_, 2>(); + + let ids = values.iter().map(|v| arena.alloc(*v)).collect::>(); + let id_pairs = ids.as_slice().chunks_exact(2); + + for (i, idxs) in id_pairs.enumerate() { + let (a_idx, b_idx) = (idxs[0], idxs[1]); + assert_eq!(values.get(2 * i), Some(&arena[a_idx])); + assert_eq!(values.get(2 * i + 1), Some(&arena[b_idx])); + let (a, b) = arena.get_two_mut(a_idx, b_idx); + *a = !*a; + *b = !*b; + assert_eq!(values.get(2 * i).map(|x| !x), Some(arena[a_idx])); + assert_eq!(values.get(2 * i + 1).map(|x| !x), Some(arena[b_idx])); + } + } + + #[kani::proof] + #[kani::unwind(3)] + fn arena_iterator_correct() { + let mut arena: Arena = Arena::new(); + let number_of_allocations: usize = kani::any(); + + kani::assume(number_of_allocations < 3); + + let values: Vec = kani::bounded_any::<_, 2>(); + + let ids: Vec = values.iter().map(|v| arena.alloc(*v)).collect::>(); + + assert_eq!(values, arena.iter().map(|p| *p.1).collect::>()) + } +} diff --git a/src/internal/id.rs b/src/internal/id.rs index 24835717..49c2b738 100644 --- a/src/internal/id.rs +++ b/src/internal/id.rs @@ -3,7 +3,7 @@ use std::{ num::NonZeroU32, }; -use crate::{Interner, internal::arena::ArenaId}; +use crate::{internal::arena::ArenaId, Interner}; /// The id associated to a package name #[repr(transparent)] @@ -165,6 +165,7 @@ impl ArenaId for DependenciesId { /// A unique identifier for a variable in the solver. #[repr(transparent)] #[derive(Copy, Clone, Debug, Eq, PartialEq, Hash, PartialOrd, Ord)] +#[cfg_attr(kani, derive(kani::Arbitrary))] pub struct VariableId(u32); impl VariableId { diff --git a/src/internal/mapping.rs b/src/internal/mapping.rs index fac003c2..a16b0906 100644 --- a/src/internal/mapping.rs +++ b/src/internal/mapping.rs @@ -8,28 +8,41 @@ const VALUES_PER_CHUNK: usize = 128; /// `TId`s. You can think of it as a HashMap, optimized for the /// case in which we know the `TId`s are contiguous. #[derive(Clone)] -pub struct Mapping { - chunks: Vec<[Option; VALUES_PER_CHUNK]>, +pub struct Mapping { + /// Hi + pub chunks: Vec<[Option; CHUNK_SIZE]>, len: usize, max: usize, _phantom: PhantomData, } -impl Default for Mapping { +impl< + #[cfg(not(kani))] TId: ArenaId, + #[cfg(kani)] TId: ArenaId + Clone, + TValue, + const CHUNK_SIZE: usize, + > Default for Mapping +{ fn default() -> Self { Self::new() } } #[allow(unused)] -impl Mapping { +impl< + #[cfg(not(kani))] TId: ArenaId, + #[cfg(kani)] TId: ArenaId + Clone, + TValue, + const CHUNK_SIZE: usize, + > Mapping +{ pub(crate) fn new() -> Self { Self::with_capacity(1) } /// Returns the total number of values that can be stored in the mapping without reallocating. pub fn capacity(&self) -> usize { - self.chunks.len() * VALUES_PER_CHUNK + self.chunks.len() * CHUNK_SIZE } /// Returns the total number of bytes allocated by this instance. @@ -40,7 +53,7 @@ impl Mapping { /// Constructs a new arena with a capacity for `n` values pre-allocated. pub fn with_capacity(n: usize) -> Self { let n = cmp::max(1, n); - let n_chunks = (n - 1) / VALUES_PER_CHUNK + 1; + let n_chunks = (n - 1) / CHUNK_SIZE + 1; let mut chunks = Vec::new(); chunks.resize_with(n_chunks, || std::array::from_fn(|_| None)); Self { @@ -54,8 +67,8 @@ impl Mapping { /// Get chunk and offset for specific id #[inline] pub const fn chunk_and_offset(id: usize) -> (usize, usize) { - let chunk = id / VALUES_PER_CHUNK; - let offset = id % VALUES_PER_CHUNK; + let chunk = id / CHUNK_SIZE; + let offset = id % CHUNK_SIZE; (chunk, offset) } @@ -109,7 +122,10 @@ impl Mapping { } /// Get a mutable specific value in the mapping with bound checks - pub fn get_mut(&mut self, id: TId) -> Option<&mut TValue> { + pub fn get_mut(&mut self, id: TId) -> Option<&mut TValue> + where + TId: Clone, + { let (chunk, offset) = Self::chunk_and_offset(id.to_usize()); if chunk >= self.chunks.len() { return None; @@ -130,6 +146,7 @@ impl Mapping { /// The caller must uphold most of the safety requirements for /// `get_unchecked`. i.e. the id having been inserted into the Mapping /// before. + #[cfg_attr(kani, kani::requires(id.clone().to_usize() < self.len))] pub unsafe fn get_unchecked(&self, id: TId) -> &TValue { let (chunk, offset) = Self::chunk_and_offset(id.to_usize()); unsafe { self.chunks.get_unchecked(chunk).get_unchecked(offset) } @@ -143,6 +160,7 @@ impl Mapping { /// The caller must uphold most of the safety requirements for /// `get_unchecked_mut`. i.e. the id having been inserted into the Mapping /// before. + #[cfg_attr(kani, kani::requires(id.clone().to_usize() < self.len))] pub unsafe fn get_unchecked_mut(&mut self, id: TId) -> &mut TValue { let (chunk, offset) = Self::chunk_and_offset(id.to_usize()); unsafe { @@ -172,11 +190,11 @@ impl Mapping { /// Defines the number of slots that can be used /// theses slots are not initialized pub fn slots(&self) -> usize { - self.chunks.len() * VALUES_PER_CHUNK + self.chunks.len() * CHUNK_SIZE } /// Returns an iterator over all the existing key value pairs. - pub fn iter(&self) -> MappingIter<'_, TId, TValue> { + pub fn iter(&self) -> MappingIter<'_, TId, TValue, CHUNK_SIZE> { MappingIter { mapping: self, offset: 0, @@ -184,12 +202,19 @@ impl Mapping { } } -pub struct MappingIter<'a, TId, TValue> { - mapping: &'a Mapping, +pub struct MappingIter<'a, TId, TValue, const CHUNK_SIZE: usize> { + mapping: &'a Mapping, offset: usize, } -impl<'a, TId: ArenaId, TValue> Iterator for MappingIter<'a, TId, TValue> { +impl< + 'a, + #[cfg(not(kani))] TId: ArenaId, + #[cfg(kani)] TId: ArenaId + Clone, + TValue, + const CHUNK_SIZE: usize, + > Iterator for MappingIter<'a, TId, TValue, CHUNK_SIZE> +{ type Item = (TId, &'a TValue); fn next(&mut self) -> Option { @@ -198,7 +223,7 @@ impl<'a, TId: ArenaId, TValue> Iterator for MappingIter<'a, TId, TValue> { return None; } - let (chunk, offset) = Mapping::::chunk_and_offset(self.offset); + let (chunk, offset) = Mapping::::chunk_and_offset(self.offset); let id = TId::from_usize(self.offset); self.offset += 1; @@ -216,10 +241,33 @@ impl<'a, TId: ArenaId, TValue> Iterator for MappingIter<'a, TId, TValue> { } } -impl FusedIterator for MappingIter<'_, TId, TValue> {} +// impl< +// #[cfg(not(kani))] TId: ArenaId, +// #[cfg(kani)] TId: ArenaId + Clone, +// TValue, +// const CHUNK_SIZE: usize, +// > MappingIter<'static, TId, TValue, CHUNK_SIZE> +// { +// fn next_ptr() -> fn( +// &mut MappingIter<'static, TId, TValue, CHUNK_SIZE>, +// ) -> std::option::Option< +// as Iterator>::Item, +// > { +// ::next +// } +// } + +impl< + #[cfg(not(kani))] TId: ArenaId, + #[cfg(kani)] TId: ArenaId + Clone, + TValue, + const CHUNK_SIZE: usize, + > FusedIterator for MappingIter<'_, TId, TValue, CHUNK_SIZE> +{ +} #[cfg(feature = "serde")] -impl serde::Serialize for Mapping { +impl serde::Serialize for Mapping { fn serialize(&self, serializer: S) -> Result { self.chunks .iter() @@ -231,7 +279,9 @@ impl serde::Serialize for Mapping { } #[cfg(feature = "serde")] -impl<'de, K: ArenaId, V: serde::Deserialize<'de>> serde::Deserialize<'de> for Mapping { +impl<'de, K: ArenaId, V: serde::Deserialize<'de>, const CHUNK_SIZE: usize> serde::Deserialize<'de> + for Mapping +{ fn deserialize(deserializer: D) -> Result where D: serde::Deserializer<'de>, @@ -301,15 +351,13 @@ mod tests { let values = [1, 3, 6, 9, 2, 4, 6, 1, 2, 3]; let json = to_value(values).unwrap(); - let mapping = - values - .iter() - .copied() - .enumerate() - .fold(Mapping::new(), |mut mapping, (i, v)| { - mapping.insert(Id::from_usize(i), v); - mapping - }); + let mapping = values.iter().copied().enumerate().fold( + Mapping::new(), + |mut mapping: Mapping, (i, v)| { + mapping.insert(Id::from_usize(i), v); + mapping + }, + ); assert_eq!(json, to_value(&mapping).unwrap()); itertools::assert_equal( @@ -318,3 +366,44 @@ mod tests { ); } } + +#[cfg(kani)] +mod verification { + use super::*; + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub_verified(Mapping::<_, _, _>::get_unchecked)] + #[kani::stub_verified(Mapping::<_, _, _>::get_unchecked_mut)] + // #[kani::stub_verified(MappingIter<_, _, _, _>::next_ptr)] + fn map_correct() { + let mut map: Mapping = Mapping::with_capacity(1); + + let n = kani::any_where(|x| *x < 2); + + let mut pairs = vec![]; + + for _ in 0..n { + pairs.push((kani::any_where(|idx| *idx < 2), kani::any())); + } + + // let pairs: Vec<(usize, bool)> = kani::bounded_any::<_, 2>(); + // kani::assume(pairs.iter().all(|(idx, _)| *idx < 2)); + + for (i, v) in pairs { + let _ = map.insert(i, v); + } + // &map.chunks.get(0).and_then(|c| c.get(0)); + let kvs = map + .iter() + .map(|(k, v)| (k, *v)) + .collect::>(); + + for (k, v) in kvs.iter() { + assert_eq!(map.get(*k), Some(v)); + let p = map.get_mut(*k).unwrap(); + *p = !*p; + assert_eq!(map.get(*k), Some(&!v)); + } + } +} diff --git a/src/lib.rs b/src/lib.rs index ff98b2a7..af5b85f4 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,3 +1,6 @@ +#![cfg_attr(kani, feature(proc_macro_hygiene))] +#![cfg_attr(kani, feature(stmt_expr_attributes))] + //! Implements a SAT solver for dependency resolution based on the CDCL //! algorithm (conflict-driven clause learning) //! diff --git a/src/solver/clause.rs b/src/solver/clause.rs index 8a28d2ed..d56cd075 100644 --- a/src/solver/clause.rs +++ b/src/solver/clause.rs @@ -8,15 +8,15 @@ use std::{ use elsa::FrozenMap; use crate::{ - Interner, NameId, Requirement, internal::{ arena::{Arena, ArenaId}, id::{ClauseId, LearntClauseId, StringId, VersionSetId}, }, solver::{ - VariableId, decision_map::DecisionMap, decision_tracker::DecisionTracker, - variable_map::VariableMap, + decision_map::DecisionMap, decision_tracker::DecisionTracker, variable_map::VariableMap, + VariableId, }, + Interner, NameId, Requirement, }; /// Represents a single clause in the SAT problem @@ -823,3 +823,18 @@ mod test { ); } } + +#[cfg(kani)] +mod verification { + use super::*; + + // TODO: Remove panic + #[kani::proof] + fn literal_from_usize_correct() { + let x: usize = kani::any(); + // If we don't assume it, try_into will handle expectional situation by panicking + kani::assume(x < (u32::MAX as usize)); + let y = Literal::from_usize(x); + assert_eq!(y.to_usize(), x); + } +} diff --git a/src/solver/decision_map.rs b/src/solver/decision_map.rs index 6f6cc2ed..bdd4269b 100644 --- a/src/solver/decision_map.rs +++ b/src/solver/decision_map.rs @@ -11,6 +11,7 @@ use crate::internal::id::VariableId; /// `< 0`: level of decision when the variable is set to false #[repr(transparent)] #[derive(Copy, Clone)] +#[cfg_attr(kani, derive(kani::Arbitrary))] struct DecisionAndLevel(i32); impl DecisionAndLevel { @@ -38,7 +39,9 @@ impl DecisionAndLevel { /// A map of the assignments to solvables. #[derive(Default)] +#[cfg_attr(kani, derive(kani::BoundedArbitrary))] pub(crate) struct DecisionMap { + #[cfg_attr(kani, bounded)] map: Vec, } @@ -60,7 +63,7 @@ impl DecisionMap { let variable_id = variable_id.to_usize(); if variable_id >= self.map.len() { self.map - .resize_with(variable_id + 1, DecisionAndLevel::undecided); + .resize(variable_id + 1, DecisionAndLevel::undecided()); } // SAFE: because we ensured that vec contains at least the correct number of @@ -82,3 +85,49 @@ impl DecisionMap { self.map.get(variable_id.to_usize()).and_then(|d| d.value()) } } + +#[cfg(kani)] +mod verification { + use super::*; + + #[kani::proof] + fn decision_map_reset_correct() { + let mut decision_map: DecisionMap = kani::bounded_any::<_, 8>(); + let initial_length = decision_map.map.len(); + let variable_id: VariableId = kani::any(); + + decision_map.reset(variable_id); + + assert!(decision_map.value(variable_id).is_none()); + assert_eq!(initial_length, decision_map.map.len()); + } + + #[kani::proof] + #[kani::unwind(10)] + #[kani::solver(kissat)] // Faster for this check + fn decision_map_set_correct() { + let mut decision_map: DecisionMap = kani::bounded_any::<_, 8>(); + let initial_length = decision_map.map.len(); + let variable_id: VariableId = kani::any(); + let value: bool = kani::any(); + let level: u32 = kani::any(); + + // Since vector gets extended we want to limit its maximal + // length, otherwise we will face unwinding issues. + kani::assume(variable_id.to_usize() < 10); + + kani::assume(level <= (i32::MAX as u32)); + + decision_map.set(variable_id, value, level); + + assert!( + (decision_map.map.len() == variable_id.to_usize() + 1) + || (decision_map.map.len() == initial_length), + ); + assert!( + (level != 0 && decision_map.value(variable_id) == Some(value)) + != (level == 0 && decision_map.value(variable_id).is_none()) + ); + assert_eq!(decision_map.level(variable_id), level) + } +}