itsscb/cargo
1
0
Fork 0
mirror of https://github.com/rust-lang/cargo.git synced 2025-10-01 11:30:39 +00:00
Code Issues Packages Projects Releases Wiki Activity

Auto merge of #13977 - linyihai:doc-resolver-tests, r=Eh2406

Browse Source 
doc: Add README for resolver-tests

### What does this PR try to resolve?

This collect the comments from `@Eh2406` about the resolver-tests and add a README to it.

### How should we test and review this PR?

### Additional information

Maybe Fixed https://github.com/rust-lang/cargo/issues/13319
See  https://github.com/rust-lang/cargo/pull/11938#issuecomment-1868426431
This commit is contained in:
bors 2024-06-03 15:14:46 +00:00
commit d503f744bc
2 changed files with 25 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
crates/resolver-tests/README.md Normal file
View File

@ -0,0 +1,13 @@
# resolver-tests
## The aim
This crate aims to test the resolution of Cargo's resolver. It implements a [SAT solver](https://en.wikipedia.org/wiki/SAT_solver) to compare with resolution of Cargo's resolver.
This ensures that Cargo's dependency resolution is proven valid by lowering to [SAT problem](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem).
## About the test
The Cargo's resolver is very sensitive to what order it tries to evaluate constraints. This makes it incredibly difficult
to be sure that a handful of tests actually covers all the important permutations of decision-making. The tests not only needs
to hit all the corner cases, it needs to try all of the orders of evaluation. So we use fuzz testing to cover more permutations.

13
crates/resolver-tests/src/lib.rs
View File

@ -31,6 +31,7 @@ pub fn resolve(deps: Vec<Dependency>, registry: &[Summary]) -> CargoResult<Vec<P
resolve_with_global_context(deps, registry, &GlobalContext::default().unwrap())
}
// Verify that the resolution of cargo resolver can pass the verification of SAT
pub fn resolve_and_validated(
deps: Vec<Dependency>,
registry: &[Summary],
@ -198,6 +199,9 @@ fn log_bits(x: usize) -> usize {
(num_bits::<usize>() as u32 - x.leading_zeros()) as usize
}
// At this point is possible to select every version of every package.
// So we need to mark certain versions as incompatible with each other.
// We could add a clause not A, not B for all A and B that are incompatible,
fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Var]) {
if vars.len() <= 1 {
return;
@ -210,6 +214,8 @@ fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Va
solver.add_clause(&[vars[1].negative(), vars[2].negative()]);
return;
}
// There are more efficient ways to do it for large numbers of versions.
//
// use the "Binary Encoding" from
// https://www.it.uu.se/research/group/astra/ModRef10/papers/Alan%20M.%20Frisch%20and%20Paul%20A.%20Giannoros.%20SAT%20Encodings%20of%20the%20At-Most-k%20Constraint%20-%20ModRef%202010.pdf
let bits: Vec<varisat::Var> = solver.new_var_iter(log_bits(vars.len())).collect();
@ -257,6 +263,7 @@ struct SatResolveInner {
impl SatResolve {
pub fn new(registry: &[Summary]) -> Self {
let mut cnf = varisat::CnfFormula::new();
// That represents each package version which is set to "true" if the packages in the lock file and "false" if it is unused.
let var_for_is_packages_used: HashMap<PackageId, varisat::Var> = registry
.iter()
.map(|s| (s.package_id(), cnf.new_var()))
@ -290,6 +297,10 @@ impl SatResolve {
let empty_vec = vec![];
// Now different versions can conflict, but dependencies might not be selected.
// So we need to add clauses that ensure that if a package is selected for each dependency a version
// that satisfies that dependency is selected.
//
// active packages need each of there `deps` to be satisfied
for p in registry.iter() {
for dep in p.dependencies() {
@ -681,7 +692,7 @@ pub fn registry_strategy(
vers
});
// each version of each crate can depend on each crate smaller then it.
// each version of each crate can depend on each crate smaller than it.
// In theory shrinkage should be 2, but in practice we get better trees with a larger value.
let max_deps = max_versions * (max_crates * (max_crates - 1)) / shrinkage;