test: add support for features in the sat resolver

This commit is contained in:
x-hgg-x 2024-09-24 23:12:18 +02:00
parent aece1f4623
commit 6f1315be84
2 changed files with 402 additions and 100 deletions

View File

@ -1,7 +1,7 @@
#![allow(clippy::print_stderr)]
use std::cmp::{max, min};
use std::collections::{BTreeMap, HashMap, HashSet};
use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
use std::fmt;
use std::fmt::Write;
use std::sync::OnceLock;
@ -10,12 +10,14 @@ use std::time::Instant;
use cargo::core::dependency::DepKind;
use cargo::core::resolver::{self, ResolveOpts, VersionOrdering, VersionPreferences};
use cargo::core::Resolve;
use cargo::core::FeatureMap;
use cargo::core::ResolveVersion;
use cargo::core::{Dependency, PackageId, Registry, Summary};
use cargo::core::{FeatureValue, Resolve};
use cargo::core::{GitReference, SourceId};
use cargo::sources::source::QueryKind;
use cargo::sources::IndexSummary;
use cargo::util::interning::{InternedString, INTERNED_DEFAULT};
use cargo::util::{CargoResult, GlobalContext, IntoUrl};
use proptest::collection::{btree_map, vec};
@ -25,7 +27,12 @@ use proptest::string::string_regex;
use varisat::ExtendFormula;
pub fn resolve(deps: Vec<Dependency>, registry: &[Summary]) -> CargoResult<Vec<PackageId>> {
resolve_with_global_context(deps, registry, &GlobalContext::default().unwrap())
Ok(
resolve_with_global_context(deps, registry, &GlobalContext::default().unwrap())?
.into_iter()
.map(|(pkg, _)| pkg)
.collect(),
)
}
// Verify that the resolution of cargo resolver can pass the verification of SAT
@ -33,7 +40,7 @@ pub fn resolve_and_validated(
deps: Vec<Dependency>,
registry: &[Summary],
sat_resolver: &mut SatResolver,
) -> CargoResult<Vec<PackageId>> {
) -> CargoResult<Vec<(PackageId, Vec<InternedString>)>> {
let resolve =
resolve_with_global_context_raw(deps.clone(), registry, &GlobalContext::default().unwrap());
@ -66,7 +73,7 @@ pub fn resolve_and_validated(
}));
}
}
let out = resolve.sort();
let out = collect_features(&resolve);
assert_eq!(out.len(), used.len());
if !sat_resolver.sat_is_valid_solution(&out) {
@ -80,13 +87,21 @@ pub fn resolve_and_validated(
}
}
fn collect_features(resolve: &Resolve) -> Vec<(PackageId, Vec<InternedString>)> {
resolve
.sort()
.iter()
.map(|&pkg| (pkg, resolve.features(pkg).to_vec()))
.collect()
}
pub fn resolve_with_global_context(
deps: Vec<Dependency>,
registry: &[Summary],
gctx: &GlobalContext,
) -> CargoResult<Vec<PackageId>> {
) -> CargoResult<Vec<(PackageId, Vec<InternedString>)>> {
let resolve = resolve_with_global_context_raw(deps, registry, gctx)?;
Ok(resolve.sort())
Ok(collect_features(&resolve))
}
pub fn resolve_with_global_context_raw(
@ -201,7 +216,7 @@ fn log_bits(x: usize) -> 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]) {
fn sat_at_most_one(solver: &mut varisat::Solver<'_>, vars: &[varisat::Var]) {
if vars.len() <= 1 {
return;
} else if vars.len() == 2 {
@ -226,48 +241,201 @@ fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Va
}
fn sat_at_most_one_by_key<K: std::hash::Hash + Eq>(
cnf: &mut impl varisat::ExtendFormula,
solver: &mut varisat::Solver<'_>,
data: impl Iterator<Item = (K, varisat::Var)>,
) -> HashMap<K, Vec<varisat::Var>> {
// no two packages with the same links set
// no two packages with the same keys set
let mut by_keys: HashMap<K, Vec<varisat::Var>> = HashMap::new();
for (p, v) in data {
by_keys.entry(p).or_default().push(v)
}
for key in by_keys.values() {
sat_at_most_one(cnf, key);
sat_at_most_one(solver, key);
}
by_keys
}
fn find_compatible_dep_summaries_by_name_in_toml(
pkg_dependencies: &[Dependency],
by_name: &HashMap<InternedString, Vec<Summary>>,
) -> HashMap<InternedString, Vec<Summary>> {
let empty_vec = vec![];
pkg_dependencies
.iter()
.map(|dep| {
let name_in_toml = dep.name_in_toml();
let compatible_summaries = by_name
.get(&dep.package_name())
.unwrap_or(&empty_vec)
.iter()
.filter(|s| dep.matches_id(s.package_id()))
.filter(|s| dep.features().iter().all(|f| s.features().contains_key(f)))
.cloned()
.collect::<Vec<_>>();
(name_in_toml, compatible_summaries)
})
.collect()
}
fn process_pkg_features(
solver: &mut varisat::Solver<'_>,
var_for_is_packages_used: &HashMap<PackageId, varisat::Var>,
var_for_is_packages_features_used: &HashMap<PackageId, HashMap<InternedString, varisat::Var>>,
pkg_feature_var_map: &HashMap<InternedString, varisat::Var>,
pkg_features: &FeatureMap,
compatible_dep_summaries_by_name_in_toml: &HashMap<InternedString, Vec<Summary>>,
) {
// add clauses for package features
for (&feature_name, feature_values) in pkg_features {
for feature_value in feature_values {
let pkg_feature_var = pkg_feature_var_map[&feature_name];
match *feature_value {
FeatureValue::Feature(other_feature_name) => {
solver.add_clause(&[
pkg_feature_var.negative(),
pkg_feature_var_map[&other_feature_name].positive(),
]);
}
FeatureValue::Dep { dep_name } => {
let dep_clause = compatible_dep_summaries_by_name_in_toml[&dep_name]
.iter()
.map(|dep| var_for_is_packages_used[&dep.package_id()].positive())
.chain([pkg_feature_var.negative()])
.collect::<Vec<_>>();
solver.add_clause(&dep_clause);
}
FeatureValue::DepFeature {
dep_name,
dep_feature: dep_feature_name,
weak,
} => {
for dep in &compatible_dep_summaries_by_name_in_toml[&dep_name] {
let dep_var = var_for_is_packages_used[&dep.package_id()];
let dep_feature_var =
var_for_is_packages_features_used[&dep.package_id()][&dep_feature_name];
solver.add_clause(&[
pkg_feature_var.negative(),
dep_var.negative(),
dep_feature_var.positive(),
]);
}
if !weak {
let dep_clause = compatible_dep_summaries_by_name_in_toml[&dep_name]
.iter()
.map(|dep| var_for_is_packages_used[&dep.package_id()].positive())
.chain([pkg_feature_var.negative()])
.collect::<Vec<_>>();
solver.add_clause(&dep_clause);
}
}
}
}
}
}
fn process_pkg_dependencies(
solver: &mut varisat::Solver<'_>,
var_for_is_packages_used: &HashMap<PackageId, varisat::Var>,
var_for_is_packages_features_used: &HashMap<PackageId, HashMap<InternedString, varisat::Var>>,
pkg_var: varisat::Var,
pkg_dependencies: &[Dependency],
compatible_dep_summaries_by_name_in_toml: &HashMap<InternedString, Vec<Summary>>,
) {
for dep in pkg_dependencies {
let compatible_dep_summaries =
&compatible_dep_summaries_by_name_in_toml[&dep.name_in_toml()];
// add clauses for package dependency features
for dep_summary in compatible_dep_summaries {
let dep_package_id = dep_summary.package_id();
let default_feature = if dep.uses_default_features()
&& dep_summary.features().contains_key(&*INTERNED_DEFAULT)
{
Some(&INTERNED_DEFAULT)
} else {
None
};
for &feature_name in default_feature.into_iter().chain(dep.features()) {
solver.add_clause(&[
pkg_var.negative(),
var_for_is_packages_used[&dep_package_id].negative(),
var_for_is_packages_features_used[&dep_package_id][&feature_name].positive(),
]);
}
}
// active packages need to activate each of their non-optional dependencies
if !dep.is_optional() {
let dep_clause = compatible_dep_summaries
.iter()
.map(|d| var_for_is_packages_used[&d.package_id()].positive())
.chain([pkg_var.negative()])
.collect::<Vec<_>>();
solver.add_clause(&dep_clause);
}
}
}
/// Resolution can be reduced to the SAT problem. So this is an alternative implementation
/// of the resolver that uses a SAT library for the hard work. This is intended to be easy to read,
/// as compared to the real resolver.
///
/// For the subset of functionality that are currently made by `registry_strategy` this will,
/// find a valid resolution if one exists. The big thing that the real resolver does,
/// that this one does not do is work with features and optional dependencies.
/// For the subset of functionality that are currently made by `registry_strategy`,
/// this will find a valid resolution if one exists.
///
/// The SAT library does not optimize for the newer version,
/// so the selected packages may not match the real resolver.
pub struct SatResolver {
solver: varisat::Solver<'static>,
old_root_vars: Vec<varisat::Var>,
var_for_is_packages_used: HashMap<PackageId, varisat::Var>,
by_name: HashMap<&'static str, Vec<PackageId>>,
var_for_is_packages_features_used: HashMap<PackageId, HashMap<InternedString, varisat::Var>>,
by_name: HashMap<InternedString, Vec<Summary>>,
}
impl SatResolver {
pub fn new(registry: &[Summary]) -> Self {
let mut cnf = varisat::CnfFormula::new();
let mut solver = varisat::Solver::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
let var_for_is_packages_used = registry
.iter()
.map(|s| (s.package_id(), cnf.new_var()))
.collect();
.map(|s| (s.package_id(), solver.new_var()))
.collect::<HashMap<_, _>>();
// That represents each feature of each package version, which is set to "true" if the package feature is used.
let var_for_is_packages_features_used = registry
.iter()
.map(|s| {
(
s.package_id(),
(s.features().keys().map(|&f| (f, solver.new_var()))).collect(),
)
})
.collect::<HashMap<_, HashMap<_, _>>>();
// if a package feature is used, then the package is used
for (package, pkg_feature_var_map) in &var_for_is_packages_features_used {
for (_, package_feature_var) in pkg_feature_var_map {
let package_var = var_for_is_packages_used[package];
solver.add_clause(&[package_feature_var.negative(), package_var.positive()]);
}
}
// no two packages with the same links set
sat_at_most_one_by_key(
&mut cnf,
&mut solver,
registry
.iter()
.map(|s| (s.links(), var_for_is_packages_used[&s.package_id()]))
@ -276,47 +444,46 @@ impl SatResolver {
// no two semver compatible versions of the same package
sat_at_most_one_by_key(
&mut cnf,
&mut solver,
var_for_is_packages_used
.iter()
.map(|(p, &v)| (p.as_activations_key(), v)),
);
let mut by_name: HashMap<&'static str, Vec<PackageId>> = HashMap::new();
let mut by_name: HashMap<InternedString, Vec<Summary>> = HashMap::new();
for p in registry.iter() {
by_name
.entry(p.name().as_str())
.or_default()
.push(p.package_id())
for p in registry {
by_name.entry(p.name()).or_default().push(p.clone())
}
let empty_vec = vec![];
for pkg in registry {
let pkg_id = pkg.package_id();
let pkg_dependencies = pkg.dependencies();
let pkg_features = pkg.features();
// 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() {
let mut matches: Vec<varisat::Lit> = by_name
.get(dep.package_name().as_str())
.unwrap_or(&empty_vec)
.iter()
.filter(|&p| dep.matches_id(*p))
.map(|p| var_for_is_packages_used[&p].positive())
.collect();
// ^ the `dep` is satisfied or `p` is not active
matches.push(var_for_is_packages_used[&p.package_id()].negative());
cnf.add_clause(&matches);
}
let compatible_dep_summaries_by_name_in_toml =
find_compatible_dep_summaries_by_name_in_toml(pkg_dependencies, &by_name);
process_pkg_features(
&mut solver,
&var_for_is_packages_used,
&var_for_is_packages_features_used,
&var_for_is_packages_features_used[&pkg_id],
pkg_features,
&compatible_dep_summaries_by_name_in_toml,
);
process_pkg_dependencies(
&mut solver,
&var_for_is_packages_used,
&var_for_is_packages_features_used,
var_for_is_packages_used[&pkg_id],
pkg_dependencies,
&compatible_dep_summaries_by_name_in_toml,
);
}
let mut solver = varisat::Solver::new();
solver.add_formula(&cnf);
// We dont need to `solve` now. We know that "use nothing" will satisfy all the clauses so far.
// We don't need to `solve` now. We know that "use nothing" will satisfy all the clauses so far.
// But things run faster if we let it spend some time figuring out how the constraints interact before we add assumptions.
solver
.solve()
@ -324,60 +491,80 @@ impl SatResolver {
SatResolver {
solver,
old_root_vars: Vec::new(),
var_for_is_packages_used,
var_for_is_packages_features_used,
by_name,
}
}
pub fn sat_resolve(&mut self, root_dependencies: &[Dependency]) -> bool {
let mut assumption = vec![];
let mut this_call = None;
let SatResolver {
solver,
old_root_vars,
var_for_is_packages_used,
var_for_is_packages_features_used,
by_name,
} = self;
// the starting `deps` need to be satisfied
for dep in root_dependencies {
let empty_vec = vec![];
let matches: Vec<varisat::Lit> = self
.by_name
.get(dep.package_name().as_str())
.unwrap_or(&empty_vec)
.iter()
.filter(|&p| dep.matches_id(*p))
.map(|p| self.var_for_is_packages_used[p].positive())
.collect();
if matches.is_empty() {
return false;
} else if matches.len() == 1 {
assumption.extend_from_slice(&matches)
} else {
if this_call.is_none() {
let new_var = self.solver.new_var();
this_call = Some(new_var);
assumption.push(new_var.positive());
}
let mut matches = matches;
matches.push(this_call.unwrap().negative());
self.solver.add_clause(&matches);
}
}
let root_var = solver.new_var();
self.solver.assume(&assumption);
// root package is always used
// root vars from previous runs are deactivated
let assumption = old_root_vars
.iter()
.map(|v| v.negative())
.chain([root_var.positive()])
.collect::<Vec<_>>();
self.solver
old_root_vars.push(root_var);
let compatible_dep_summaries_by_name_in_toml =
find_compatible_dep_summaries_by_name_in_toml(root_dependencies, &by_name);
process_pkg_dependencies(
solver,
var_for_is_packages_used,
var_for_is_packages_features_used,
root_var,
root_dependencies,
&compatible_dep_summaries_by_name_in_toml,
);
solver.assume(&assumption);
solver
.solve()
.expect("docs say it can't error in default config")
}
pub fn sat_is_valid_solution(&mut self, pids: &[PackageId]) -> bool {
for p in pids {
if p.name().as_str() != "root" && !self.var_for_is_packages_used.contains_key(p) {
pub fn sat_is_valid_solution(&mut self, pkgs: &[(PackageId, Vec<InternedString>)]) -> bool {
let contains_pkg = |pkg| pkgs.iter().any(|(p, _)| p == pkg);
let contains_pkg_feature =
|pkg, f| pkgs.iter().any(|(p, flist)| p == pkg && flist.contains(f));
for (p, _) in pkgs {
if p.name() != "root" && !self.var_for_is_packages_used.contains_key(p) {
return false;
}
}
let assumption: Vec<_> = self
.var_for_is_packages_used
.iter()
.map(|(p, v)| v.lit(pids.contains(p)))
.collect();
// root vars from previous runs are deactivated
let assumption = (self.old_root_vars.iter().map(|v| v.negative()))
.chain(
self.var_for_is_packages_used
.iter()
.map(|(p, v)| v.lit(contains_pkg(p))),
)
.chain(
self.var_for_is_packages_features_used
.iter()
.flat_map(|(p, fmap)| {
fmap.iter()
.map(move |(f, v)| v.lit(contains_pkg_feature(p, f)))
}),
)
.collect::<Vec<_>>();
self.solver.assume(&assumption);
@ -393,13 +580,32 @@ impl SatResolver {
.filter(|l| l.is_positive())
.map(|l| l.var())
.collect();
let mut out = String::new();
out.push_str("used:\n");
for (p, v) in self.var_for_is_packages_used.iter() {
let mut used_packages = BTreeMap::<PackageId, BTreeSet<InternedString>>::new();
for (&p, v) in self.var_for_is_packages_used.iter() {
if lits.contains(v) {
writeln!(&mut out, " {}", p).unwrap();
used_packages.entry(p).or_default();
}
}
for (&p, map) in &self.var_for_is_packages_features_used {
for (&f, v) in map {
if lits.contains(v) {
used_packages
.get_mut(&p)
.expect("the feature is activated without the package being activated")
.insert(f);
}
}
}
let mut out = String::from("used:\n");
for (package, feature_names) in used_packages {
writeln!(&mut out, " {package}").unwrap();
for feature_name in feature_names {
writeln!(&mut out, " + {feature_name}").unwrap();
}
}
out
})
}

View File

@ -6,9 +6,10 @@ use cargo::util::GlobalContext;
use cargo_util::is_ci;
use resolver_tests::{
assert_contains, assert_same, dep, dep_kind, dep_loc, dep_req, loc_names, names, pkg, pkg_id,
pkg_loc, registry, registry_strategy, remove_dep, resolve, resolve_and_validated,
resolve_with_global_context, PrettyPrintRegistry, SatResolver, ToDep, ToPkgId,
assert_contains, assert_same, dep, dep_kind, dep_loc, dep_req, loc_names, names, pkg, pkg_dep,
pkg_dep_with, pkg_id, pkg_loc, registry, registry_strategy, remove_dep, resolve,
resolve_and_validated, resolve_with_global_context, PrettyPrintRegistry, SatResolver, ToDep,
ToPkgId,
};
use proptest::prelude::*;
@ -446,7 +447,10 @@ fn test_resolving_minimum_version_with_transitive_deps() {
&reg,
&gctx,
)
.unwrap();
.unwrap()
.into_iter()
.map(|(pkg, _)| pkg)
.collect::<Vec<_>>();
assert_contains(
&res,
@ -1214,7 +1218,7 @@ fn off_by_one_bug() {
let reg = registry(input);
let mut sat_resolver = SatResolver::new(&reg);
let _ = resolve_and_validated(vec![dep("f")], &reg, &mut sat_resolver);
assert!(resolve_and_validated(vec![dep("f")], &reg, &mut sat_resolver).is_ok());
}
#[test]
@ -1255,7 +1259,7 @@ fn conflict_store_bug() {
let reg = registry(input);
let mut sat_resolver = SatResolver::new(&reg);
let _ = resolve_and_validated(vec![dep("j")], &reg, &mut sat_resolver);
assert!(resolve_and_validated(vec![dep("j")], &reg, &mut sat_resolver).is_err());
}
#[test]
@ -1284,7 +1288,7 @@ fn conflict_store_more_then_one_match() {
];
let reg = registry(input);
let mut sat_resolver = SatResolver::new(&reg);
let _ = resolve_and_validated(vec![dep("nA")], &reg, &mut sat_resolver);
assert!(resolve_and_validated(vec![dep("nA")], &reg, &mut sat_resolver).is_err());
}
#[test]
@ -1310,7 +1314,99 @@ fn bad_lockfile_from_8249() {
];
let reg = registry(input);
let mut sat_resolver = SatResolver::new(&reg);
let _ = resolve_and_validated(vec![dep("foo")], &reg, &mut sat_resolver);
assert!(resolve_and_validated(vec![dep("foo")], &reg, &mut sat_resolver).is_err());
}
#[test]
fn registry_with_features() {
let reg = registry(vec![
pkg!("a"),
pkg!("b"),
pkg_dep_with(
"image",
vec!["a".to_opt_dep(), "b".to_opt_dep(), "jpg".to_dep()],
&[("default", &["a"]), ("b", &["dep:b"])],
),
pkg!("jpg"),
pkg!("log"),
pkg!("man"),
pkg_dep_with("rgb", vec!["man".to_opt_dep()], &[("man", &["dep:man"])]),
pkg_dep_with(
"dep",
vec![
"image".to_dep_with(&["b"]),
"log".to_opt_dep(),
"rgb".to_opt_dep(),
],
&[
("default", &["log", "image/default"]),
("man", &["rgb?/man"]),
],
),
]);
for deps in [
vec!["dep".to_dep_with(&["default", "man", "log", "rgb"])],
vec!["dep".to_dep_with(&["default"])],
vec!["dep".to_dep_with(&[])],
vec!["dep".to_dep_with(&["man"])],
vec!["dep".to_dep_with(&["man", "rgb"])],
] {
let mut sat_resolver = SatResolver::new(&reg);
assert!(resolve_and_validated(deps, &reg, &mut sat_resolver).is_ok());
}
}
#[test]
fn missing_feature() {
let reg = registry(vec![pkg!("a")]);
let mut sat_resolver = SatResolver::new(&reg);
assert!(resolve_and_validated(vec!["a".to_dep_with(&["f"])], &reg, &mut sat_resolver).is_err());
}
#[test]
fn conflict_feature_and_sys() {
let reg = registry(vec![
pkg(("a-sys", "1.0.0")),
pkg(("a-sys", "2.0.0")),
pkg_dep_with(
("a", "1.0.0"),
vec![dep_req("a-sys", "1.0.0")],
&[("f", &[])],
),
pkg_dep_with(
("a", "2.0.0"),
vec![dep_req("a-sys", "2.0.0")],
&[("g", &[])],
),
pkg_dep("dep", vec![dep_req("a", "2.0.0")]),
]);
let deps = vec![dep_req("a", "*").to_dep_with(&["f"]), dep("dep")];
let mut sat_resolver = SatResolver::new(&reg);
assert!(resolve_and_validated(deps, &reg, &mut sat_resolver).is_err());
}
#[test]
fn conflict_weak_features() {
let reg = registry(vec![
pkg(("a-sys", "1.0.0")),
pkg(("a-sys", "2.0.0")),
pkg_dep("a1", vec![dep_req("a-sys", "1.0.0").to_opt_dep()]),
pkg_dep("a2", vec![dep_req("a-sys", "2.0.0").to_opt_dep()]),
pkg_dep_with(
"dep",
vec!["a1".to_opt_dep(), "a2".to_opt_dep()],
&[("a1", &["a1?/a-sys"]), ("a2", &["a2?/a-sys"])],
),
]);
let deps = vec![dep("dep").to_dep_with(&["a1", "a2"])];
// The following asserts should be updated when support for weak dependencies
// is added to the dependency resolver.
assert!(resolve(deps.clone(), &reg).is_err());
assert!(SatResolver::new(&reg).sat_resolve(&deps));
}
#[test]