ASP-based solver: fix provider logic (#24351)

This commit fixes a subtle bug that may occur when
a package is a "possible_provider" of a virtual but
no "provides_virtual" can be deduced. In that case
the cardinality constraint on "provides_virtual"
may arbitrarily assign a package the role of provider
even if the constraints for it to be one are not fulfilled.

The fix reworks the logic around three concepts:
- "possible_provider": a package may provide a virtual if some constraints are met
- "provides_virtual": a package meet the constraints to provide a virtual
- "provider": a package selected to provide a virtual

lib/spack/spack/solver/concretize.lp

@@ -145,7 +145,7 @@ path(Parent, Descendant) :- path(Parent, A), depends_on(A, Descendant).
 % provider for that virtual then it depends on the provider
 depends_on(Package, Provider, Type)
   :- dependency_holds(Package, Virtual, Type),
-     provides_virtual(Provider, Virtual),
+     provider(Provider, Virtual),
      not external(Package).
 
 % dependencies on virtuals also imply that the virtual is a virtual node
@@ -153,14 +153,24 @@ virtual_node(Virtual)
   :- dependency_holds(Package, Virtual, Type),
      virtual(Virtual), not external(Package).
 
-% if there's a virtual node, we must select one provider
-1 { provides_virtual(Package, Virtual) : possible_provider(Package, Virtual) } 1
+% If there's a virtual node, we must select one and only one provider.
+% The provider must be selected among the possible providers.
+1 { provider(Package, Virtual) : possible_provider(Package, Virtual) } 1
  :- virtual_node(Virtual).
 
 % virtual roots imply virtual nodes, and that one provider is a root
 virtual_node(Virtual) :- virtual_root(Virtual).
-1 { root(Package) : provides_virtual(Package, Virtual) } 1
-  :- virtual_root(Virtual).
+
+% If we asked for a virtual root and we have a provider for that,
+% then the provider is the root package.
+root(Package) :- virtual_root(Virtual), provider(Package, Virtual).
+
+% If we asked for a root package and that root provides a virtual,
+% the root is a provider for that virtual. This rule is mostly relevant
+% for environments that are concretized together (e.g. where we
+% asks to install "mpich" and "hdf5+mpi" and we want "mpich" to
+% be the mpi provider)
+provider(Package, Virtual) :- root(Package), provides_virtual(Package, Virtual).
 
 % The provider provides the virtual if some provider condition holds.
 provides_virtual(Provider, Virtual) :-
@@ -168,12 +178,15 @@ provides_virtual(Provider, Virtual) :-
    condition_holds(ID),
    virtual(Virtual).
 
-% a node that provides a virtual is a provider
-provider(Package, Virtual)
-  :- node(Package), provides_virtual(Package, Virtual).
+% A package cannot be the actual provider for a virtual if it does not
+% fulfill the conditions to provide that virtual
+:- provider(Package, Virtual), not provides_virtual(Package, Virtual).
 
-% for any virtual, there can be at most one provider in the DAG
-0 { node(Package) : provides_virtual(Package, Virtual) } 1 :- virtual(Virtual).
+% If a package is selected as a provider, it is provider of all
+% the virtuals it provides
+:- provides_virtual(Package, V1), provides_virtual(Package, V2), V1 != V2,
+   provider(Package, V1), not provider(Package, V2),
+   virtual_node(V1), virtual_node(V2).
 
 #defined possible_provider/2.
 

lib/spack/spack/test/concretize.py

@@ -1253,3 +1253,11 @@ def test_version_badness_more_important_than_default_mv_variants(self):
         # criteria.
         s = spack.spec.Spec('root').concretized()
         assert s['gmt'].satisfies('@2.0')
+
+    @pytest.mark.regression('24205')
+    def test_provider_must_meet_requirements(self):
+        # A package can be a provider of a virtual only if the underlying
+        # requirements are met.
+        s = spack.spec.Spec('unsat-virtual-dependency')
+        with pytest.raises((RuntimeError, spack.error.UnsatisfiableSpecError)):
+            s.concretize()

var/spack/repos/builtin.mock/packages/unsat-provider/package.py

@@ -0,0 +1,15 @@
+# Copyright 2013-2021 Lawrence Livermore National Security, LLC and other
+# Spack Project Developers. See the top-level COPYRIGHT file for details.
+#
+# SPDX-License-Identifier: (Apache-2.0 OR MIT)
+class UnsatProvider(Package):
+    """This package has a dependency on a virtual that cannot be provided"""
+    homepage = "http://www.example.com"
+    url = "http://www.example.com/v1.0.tgz"
+
+    version('1.0', sha256='foobarbaz')
+
+    variant('foo', default=True, description='')
+
+    provides('unsatvdep', when='+foo')
+    conflicts('+foo')

var/spack/repos/builtin.mock/packages/unsat-virtual-dependency/package.py

@@ -0,0 +1,12 @@
+# Copyright 2013-2021 Lawrence Livermore National Security, LLC and other
+# Spack Project Developers. See the top-level COPYRIGHT file for details.
+#
+# SPDX-License-Identifier: (Apache-2.0 OR MIT)
+class UnsatVirtualDependency(Package):
+    """This package has a dependency on a virtual that cannot be provided"""
+    homepage = "http://www.example.com"
+    url = "http://www.example.com/v1.0.tgz"
+
+    version('1.0', sha256='foobarbaz')
+
+    depends_on('unsatvdep')