Improved error messages from clingo (#26719)

This PR adds error message sentinels to the clingo solve, attached to each of the rules that could fail a solve. The unsat core is then restricted to these messages, which makes the minimization problem tractable. Errors that can only be generated by a bug in the logic program or generating code are prefaced with "Internal error" to make clear to users that something has gone wrong on the Spack side of things.

* minimize unsat cores manually

* only errors messages are choices/assumptions for performance

* pre-check for unreachable nodes

* update tests for new error message

* make clingo concretization errors show up in cdash reports fully

* clingo: make import of clingo.ast parsing routines robust to clingo version

Older `clingo` has `parse_string`; newer `clingo` has `parse_files`.  Make the
code work wtih both.

* make AST access functions backward-compatible with clingo 5.4.0

Clingo AST API has changed since 5.4.0; make some functions to help us
handle both versions of the AST.

Co-authored-by: Todd Gamblin <tgamblin@llnl.gov>

lib/spack/spack/cmd/solve.py

@@ -109,10 +109,7 @@ def solve(parser, args):
         return
 
     # die if no solution was found
-    # TODO: we need to be able to provide better error messages than this
+    result.raise_if_unsat()
-    if not result.satisfiable:
-        result.print_cores()
-        tty.die("Unsatisfiable spec.")
 
     # dump the solutions as concretized specs
     if 'solutions' in dump:

lib/spack/spack/concretize.py

@@ -728,11 +728,7 @@ def concretize_specs_together(*abstract_specs, **kwargs):
 def _concretize_specs_together_new(*abstract_specs, **kwargs):
     import spack.solver.asp
     result = spack.solver.asp.solve(abstract_specs)
-
+    result.raise_if_unsat()
-    if not result.satisfiable:
-        result.print_cores()
-        tty.die("Unsatisfiable spec.")
-
     return [s.copy() for s in result.specs]
 
 

lib/spack/spack/error.py

@@ -117,11 +117,24 @@ class SpecError(SpackError):
 
 
 class UnsatisfiableSpecError(SpecError):
-    """Raised when a spec conflicts with package constraints.
+    """
-       Provide the requirement that was violated when raising."""
+    Raised when a spec conflicts with package constraints.
-    def __init__(self, provided, required, constraint_type):
+
-        super(UnsatisfiableSpecError, self).__init__(
+    For original concretizer, provide the requirement that was violated when
-            "%s does not satisfy %s" % (provided, required))
+    raising.
+    """
+    def __init__(self, provided, required=None, constraint_type=None, conflicts=None):
+        # required is only set by the original concretizer.
+        # clingo concretizer handles error messages differently.
+        if required is not None:
+            assert not conflicts  # can't mix formats
+            super(UnsatisfiableSpecError, self).__init__(
+                "%s does not satisfy %s" % (provided, required))
+        else:
+            indented = ['  %s\n' % conflict for conflict in conflicts]
+            conflict_msg = ''.join(indented)
+            msg = '%s is unsatisfiable, conflicts are:\n%s' % (provided, conflict_msg)
+            super(UnsatisfiableSpecError, self).__init__(msg)
         self.provided = provided
         self.required = required
         self.constraint_type = constraint_type

lib/spack/spack/solver/asp.py

@@ -52,6 +52,25 @@
 else:
     from collections import Sequence
 
+# these are from clingo.ast and bootstrapped later
+ASTType = None
+parse_files = None
+
+
+# backward compatibility functions for clingo ASTs
+def ast_getter(*names):
+    def getter(node):
+        for name in names:
+            result = getattr(node, name, None)
+            if result:
+                return result
+        raise KeyError("node has no such keys: %s" % names)
+    return getter
+
+
+ast_type = ast_getter("ast_type", "type")
+ast_sym = ast_getter("symbol", "term")
+
 
 #: Enumeration like object to mark version provenance
 version_provenance = collections.namedtuple(  # type: ignore
@@ -205,6 +224,9 @@ def __init__(self, specs, asp=None):
         self.warnings = None
         self.nmodels = 0
 
+        # Saved control object for reruns when necessary
+        self.control = None
+
         # specs ordered by optimization level
         self.answers = []
         self.cores = []
@@ -218,11 +240,85 @@ def __init__(self, specs, asp=None):
         # Concrete specs
         self._concrete_specs = None
 
-    def print_cores(self):
+    def format_core(self, core):
-        for core in self.cores:
+        """
-            tty.msg(
+        Format an unsatisfiable core for human readability
-                "The following constraints are unsatisfiable:",
+
-                *sorted(str(symbol) for symbol in core))
+        Returns a list of strings, where each string is the human readable
+        representation of a single fact in the core, including a newline.
+
+        Modeled after traceback.format_stack.
+        """
+        assert self.control
+
+        symbols = dict(
+            (a.literal, a.symbol)
+            for a in self.control.symbolic_atoms
+        )
+
+        core_symbols = []
+        for atom in core:
+            sym = symbols[atom]
+            if sym.name in ("rule", "error"):
+                # these are special symbols we use to get messages in the core
+                sym = sym.arguments[0].string
+            core_symbols.append(sym)
+
+        return sorted(str(symbol) for symbol in core_symbols)
+
+    def minimize_core(self, core):
+        """
+        Return a subset-minimal subset of the core.
+
+        Clingo cores may be thousands of lines when two facts are sufficient to
+        ensure unsatisfiability. This algorithm reduces the core to only those
+        essential facts.
+        """
+        assert self.control
+
+        min_core = core[:]
+        for fact in core:
+            # Try solving without this fact
+            min_core.remove(fact)
+            ret = self.control.solve(assumptions=min_core)
+            if not ret.unsatisfiable:
+                min_core.append(fact)
+        return min_core
+
+    def minimal_cores(self):
+        """
+        Return a list of subset-minimal unsatisfiable cores.
+        """
+        return [self.minimize_core(core) for core in self.cores]
+
+    def format_minimal_cores(self):
+        """List of facts for each core
+
+        Separate cores are separated by an empty line
+        """
+        string_list = []
+        for core in self.minimal_cores():
+            if string_list:
+                string_list.append('\n')
+            string_list.extend(self.format_core(core))
+        return string_list
+
+    def raise_if_unsat(self):
+        """
+        Raise an appropriate error if the result is unsatisfiable.
+
+        The error is a UnsatisfiableSpecError, and includes the minimized cores
+        resulting from the solve, formatted to be human readable.
+        """
+        if self.satisfiable:
+            return
+
+        constraints = self.abstract_specs
+        if len(constraints) == 1:
+            constraints = constraints[0]
+        conflicts = self.format_minimal_cores()
+
+        raise spack.error.UnsatisfiableSpecError(constraints, conflicts=conflicts)
 
     @property
     def specs(self):
@@ -276,6 +372,22 @@ def _normalize_packages_yaml(packages_yaml):
     return normalized_yaml
 
 
+def bootstrap_clingo():
+    global clingo, ASTType, parse_files
+
+    if not clingo:
+        with spack.bootstrap.ensure_bootstrap_configuration():
+            spack.bootstrap.ensure_clingo_importable_or_raise()
+            import clingo
+
+    from clingo.ast import ASTType
+    try:
+        from clingo.ast import parse_files
+    except ImportError:
+        # older versions of clingo have this one namespace up
+        from clingo import parse_files
+
+
 class PyclingoDriver(object):
     def __init__(self, cores=True, asp=None):
         """Driver for the Python clingo interface.
@@ -286,11 +398,8 @@ def __init__(self, cores=True, asp=None):
             asp (file-like): optional stream to write a text-based ASP program
                 for debugging or verification.
         """
-        global clingo
+        bootstrap_clingo()
-        if not clingo:
+
-            with spack.bootstrap.ensure_bootstrap_configuration():
-                spack.bootstrap.ensure_clingo_importable_or_raise()
-                import clingo
         self.out = asp or llnl.util.lang.Devnull()
         self.cores = cores
 
@@ -311,15 +420,22 @@ def h2(self, name):
     def newline(self):
         self.out.write('\n')
 
-    def fact(self, head):
+    def fact(self, head, assumption=False):
-        """ASP fact (a rule without a body)."""
+        """ASP fact (a rule without a body).
+
+        Arguments:
+            head (AspFunction): ASP function to generate as fact
+            assumption (bool): If True and using cores, use this fact as a
+                choice point in ASP and include it in unsatisfiable cores
+        """
         symbol = head.symbol() if hasattr(head, 'symbol') else head
 
         self.out.write("%s.\n" % str(symbol))
 
         atom = self.backend.add_atom(symbol)
-        self.backend.add_rule([atom], [], choice=self.cores)
+        choice = self.cores and assumption
-        if self.cores:
+        self.backend.add_rule([atom], [], choice=choice)
+        if choice:
             self.assumptions.append(atom)
 
     def solve(
@@ -347,6 +463,22 @@ def solve(
         # read in the main ASP program and display logic -- these are
         # handwritten, not generated, so we load them as resources
         parent_dir = os.path.dirname(__file__)
+
+        # extract error messages from concretize.lp by inspecting its AST
+        with self.backend:
+            def visit(node):
+                if ast_type(node) == ASTType.Rule:
+                    for term in node.body:
+                        if ast_type(term) == ASTType.Literal:
+                            if ast_type(term.atom) == ASTType.SymbolicAtom:
+                                if ast_sym(term.atom).name == "error":
+                                    arg = ast_sym(ast_sym(term.atom).arguments[0])
+                                    self.fact(fn.error(arg.string), assumption=True)
+
+            path = os.path.join(parent_dir, 'concretize.lp')
+            parse_files([path], visit)
+
+        # Load the file itself
         self.control.load(os.path.join(parent_dir, 'concretize.lp'))
         self.control.load(os.path.join(parent_dir, "display.lp"))
         timer.phase("load")
@@ -367,6 +499,7 @@ def on_model(model):
         solve_kwargs = {"assumptions": self.assumptions,
                         "on_model": on_model,
                         "on_core": cores.append}
+
         if clingo_cffi:
             solve_kwargs["on_unsat"] = cores.append
         solve_result = self.control.solve(**solve_kwargs)
@@ -409,18 +542,8 @@ def stringify(x):
             result.nmodels = len(models)
 
         elif cores:
-            symbols = dict(
+            result.control = self.control
-                (a.literal, a.symbol)
+            result.cores.extend(cores)
-                for a in self.control.symbolic_atoms
-            )
-            for core in cores:
-                core_symbols = []
-                for atom in core:
-                    sym = symbols[atom]
-                    if sym.name == "rule":
-                        sym = sym.arguments[0].string
-                    core_symbols.append(sym)
-                result.cores.append(core_symbols)
 
         if timers:
             timer.write_tty()
@@ -1372,6 +1495,14 @@ def setup(self, driver, specs, tests=False):
             virtuals=self.possible_virtuals,
             deptype=spack.dependency.all_deptypes
         )
+
+        # Fail if we already know an unreachable node is requested
+        for spec in specs:
+            missing_deps = [d for d in spec.traverse()
+                            if d.name not in possible and not d.virtual]
+            if missing_deps:
+                raise spack.spec.InvalidDependencyError(spec.name, missing_deps)
+
         pkgs = set(possible)
 
         # driver is used by all the functions below to add facts and

lib/spack/spack/solver/concretize.lp

@@ -18,7 +18,8 @@ version_declared(Package, Version, Weight) :- version_declared(Package, Version,
 % We can't emit the same version **with the same weight** from two different sources
 :- version_declared(Package, Version, Weight, Origin1),
    version_declared(Package, Version, Weight, Origin2),
-   Origin1 != Origin2.
+   Origin1 != Origin2,
+   error("Internal error: two versions with identical weights").
 
 % versions are declared w/priority -- declared with priority implies declared
 version_declared(Package, Version) :- version_declared(Package, Version, _).
@@ -26,7 +27,7 @@ version_declared(Package, Version) :- version_declared(Package, Version, _).
 % If something is a package, it has only one version and that must be a
 % declared version.
 1 { version(Package, Version) : version_declared(Package, Version) } 1
- :- node(Package).
+ :- node(Package), error("Each node must have exactly one version").
 
 % A virtual package may have or not a version, but never has more than one
 :- virtual_node(Package), 2 { version(Package, _) }.
@@ -38,12 +39,13 @@ possible_version_weight(Package, Weight)
  :- version(Package, Version),
     version_declared(Package, Version, Weight).
 
-1 { version_weight(Package, Weight) : possible_version_weight(Package, Weight) } 1 :- node(Package).
+1 { version_weight(Package, Weight) : possible_version_weight(Package, Weight) } 1 :- node(Package), error("Internal error: Package version must have a unique weight").
 
 % version_satisfies implies that exactly one of the satisfying versions
 % is the package's version, and vice versa.
 1 { version(Package, Version) : version_satisfies(Package, Constraint, Version) } 1
-  :- version_satisfies(Package, Constraint).
+  :- version_satisfies(Package, Constraint),
+     error("no version satisfies the given constraints").
 version_satisfies(Package, Constraint)
   :- version(Package, Version), version_satisfies(Package, Constraint, Version).
 
@@ -122,14 +124,17 @@ node(Dependency) :- node(Package), depends_on(Package, Dependency).
 % dependencies) and get a two-node unconnected graph
 needed(Package) :- root(Package).
 needed(Dependency) :- needed(Package), depends_on(Package, Dependency).
-:- node(Package), not needed(Package).
+:- node(Package), not needed(Package),
+   error("All dependencies must be reachable from root").
 
 % Avoid cycles in the DAG
 % some combinations of conditional dependencies can result in cycles;
 % this ensures that we solve around them
 path(Parent, Child) :- depends_on(Parent, Child).
 path(Parent, Descendant) :- path(Parent, A), depends_on(A, Descendant).
-:- path(A, B), path(B, A).
+:- path(A, B), path(B, A), error("Cyclic dependencies are not allowed").
+
+#defined error/1.
 
 #defined dependency_type/2.
 #defined dependency_condition/3.
@@ -141,7 +146,8 @@ path(Parent, Descendant) :- path(Parent, A), depends_on(A, Descendant).
    not external(Package),
    conflict(Package, TriggerID, ConstraintID),
    condition_holds(TriggerID),
-   condition_holds(ConstraintID).
+   condition_holds(ConstraintID),
+   error("A conflict was triggered").
 
 #defined conflict/3.
 
@@ -164,7 +170,7 @@ virtual_node(Virtual)
 % 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_node(Virtual), error("Virtual packages must be satisfied by a unique provider").
 
 % virtual roots imply virtual nodes, and that one provider is a root
 virtual_node(Virtual) :- virtual_root(Virtual).
@@ -188,7 +194,8 @@ virtual_condition_holds(Provider, 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 virtual_condition_holds(Package, Virtual).
+:- provider(Package, Virtual), not virtual_condition_holds(Package, Virtual),
+   error("Internal error: virtual when provides not respected").
 
 #defined possible_provider/2.
 
@@ -201,7 +208,7 @@ virtual_condition_holds(Provider, Virtual) :-
 % we select the weight, among the possible ones, that minimizes the overall objective function.
 1 { provider_weight(Dependency, Virtual, Weight, Reason) :
     possible_provider_weight(Dependency, Virtual, Weight, Reason) } 1
- :- provider(Dependency, Virtual).
+ :- provider(Dependency, Virtual), error("Internal error: package provider weights must be unique").
 
 % Get rid or the reason for enabling the possible weight (useful for debugging)
 provider_weight(Dependency, Virtual, Weight) :- provider_weight(Dependency, Virtual, Weight, _).
@@ -299,7 +306,7 @@ attr("node_compiler_version_satisfies", Package, Compiler, Version)
 % if a package is external its version must be one of the external versions
 1 { external_version(Package, Version, Weight):
     version_declared(Package, Version, Weight, "external") } 1
-    :- external(Package).
+    :- external(Package), error("External package version does not satisfy external spec").
 
 version_weight(Package, Weight) :- external_version(Package, Version, Weight).
 version(Package, Version) :- external_version(Package, Version, Weight).
@@ -318,7 +325,8 @@ external(Package) :- external_spec_selected(Package, _).
 :- version(Package, Version),
    version_weight(Package, Weight),
    version_declared(Package, Version, Weight, "external"),
-   not external(Package).
+   not external(Package),
+   error("Internal error: external weight used for internal spec").
 
 % determine if an external spec has been selected
 external_spec_selected(Package, LocalIndex) :-
@@ -330,7 +338,8 @@ external_conditions_hold(Package, LocalIndex) :-
 
 % it cannot happen that a spec is external, but none of the external specs
 % conditions hold.
-:- external(Package), not external_conditions_hold(Package, _).
+:- external(Package), not external_conditions_hold(Package, _),
+   error("External package does not satisfy external spec").
 
 #defined possible_external/3.
 #defined external_spec_index/3.
@@ -348,7 +357,8 @@ external_conditions_hold(Package, LocalIndex) :-
 } 1
  :- node(Package),
     variant(Package, Variant),
-    variant_single_value(Package, Variant).
+    variant_single_value(Package, Variant),
+    error("Single valued variants must have a single value").
 
 % at least one variant value for multi-valued variants.
 1 {
@@ -357,13 +367,15 @@ external_conditions_hold(Package, LocalIndex) :-
 }
  :- node(Package),
     variant(Package, Variant),
-    not variant_single_value(Package, Variant).
+    not variant_single_value(Package, Variant),
+    error("Internal error: All variants must have a value").
 
 % if a variant is set to anything, it is considered 'set'.
 variant_set(Package, Variant) :- variant_set(Package, Variant, _).
 
 % A variant cannot have a value that is not also a possible value
-:- variant_value(Package, Variant, Value), not variant_possible_value(Package, Variant, Value).
+:- variant_value(Package, Variant, Value), not variant_possible_value(Package, Variant, Value),
+   error("Variant set to invalid value").
 
 % Some multi valued variants accept multiple values from disjoint sets.
 % Ensure that we respect that constraint and we don't pick values from more
@@ -372,7 +384,8 @@ variant_set(Package, Variant) :- variant_set(Package, Variant, _).
    variant_value(Package, Variant, Value2),
    variant_value_from_disjoint_sets(Package, Variant, Value1, Set1),
    variant_value_from_disjoint_sets(Package, Variant, Value2, Set2),
-   Set1 != Set2.
+   Set1 != Set2,
+   error("Variant values selected from multiple disjoint sets").
 
 % variant_set is an explicitly set variant value. If it's not 'set',
 % we revert to the default value. If it is set, we force the set value
@@ -437,7 +450,8 @@ variant_default_value(Package, Variant, Value) :- variant_default_value_from_cli
 % Treat 'none' in a special way - it cannot be combined with other
 % values even if the variant is multi-valued
 :- 2 {variant_value(Package, Variant, Value): variant_possible_value(Package, Variant, Value)},
-   variant_value(Package, Variant, "none").
+   variant_value(Package, Variant, "none"),
+   error("Variant value 'none' cannot be combined with any other value").
 
 % patches and dev_path are special variants -- they don't have to be
 % declared in the package, so we just allow them to spring into existence
@@ -467,7 +481,7 @@ variant_single_value(Package, "dev_path")
 %-----------------------------------------------------------------------------
 
 % one platform per node
-:- M = #count { Platform : node_platform(Package, Platform) }, M !=1, node(Package).
+:- M = #count { Platform : node_platform(Package, Platform) }, M !=1, node(Package), error("A node must have exactly one platform").
 
 % if no platform is set, fall back to the default
 node_platform(Package, Platform)
@@ -488,7 +502,7 @@ node_platform_set(Package) :- node_platform_set(Package, _).
 % OS semantics
 %-----------------------------------------------------------------------------
 % one os per node
-1 { node_os(Package, OS) : os(OS) } 1 :- node(Package).
+1 { node_os(Package, OS) : os(OS) } 1 :- node(Package), error("Each node must have exactly one OS").
 
 % node_os_set implies that the node must have that os
 node_os(Package, OS) :- node(Package), node_os_set(Package, OS).
@@ -515,11 +529,11 @@ node_os(Package, OS)
 % Target semantics
 %-----------------------------------------------------------------------------
 % one target per node -- optimization will pick the "best" one
-1 { node_target(Package, Target) : target(Target) } 1 :- node(Package).
+1 { node_target(Package, Target) : target(Target) } 1 :- node(Package), error("Each node must have exactly one target").
 
 % node_target_satisfies semantics
 1 { node_target(Package, Target) : node_target_satisfies(Package, Constraint, Target) } 1
-  :- node_target_satisfies(Package, Constraint).
+  :- node_target_satisfies(Package, Constraint), error("Each node must have exactly one target").
 node_target_satisfies(Package, Constraint)
   :- node_target(Package, Target), node_target_satisfies(Package, Constraint, Target).
 #defined node_target_satisfies/3.
@@ -546,7 +560,8 @@ target_weight(Target, Package, Weight)
 :- node_target(Package, Target),
    not compiler_supports_target(Compiler, Version, Target),
    node_compiler(Package, Compiler),
-   node_compiler_version(Package, Compiler, Version).
+   node_compiler_version(Package, Compiler, Version),
+   error("No satisfying compiler available is compatible with a satisfying target").
 
 % if a target is set explicitly, respect it
 node_target(Package, Target)
@@ -583,7 +598,7 @@ compiler(Compiler) :- compiler_version(Compiler, _).
 % There must be only one compiler set per node. The compiler
 % is chosen among available versions.
 1 { node_compiler_version(Package, Compiler, Version)
-    : compiler_version(Compiler, Version) } 1 :- node(Package).
+    : compiler_version(Compiler, Version) } 1 :- node(Package), error("Each node must have exactly one compiler").
 
 % Sometimes we just need to know the compiler and not the version
 node_compiler(Package, Compiler) :- node_compiler_version(Package, Compiler, _).
@@ -591,14 +606,15 @@ node_compiler(Package, Compiler) :- node_compiler_version(Package, Compiler, _).
 % We can't have a compiler be enforced and select the version from another compiler
 :- node_compiler(Package, Compiler1),
    node_compiler_version(Package, Compiler2, _),
-   Compiler1 != Compiler2.
+   Compiler1 != Compiler2,
+   error("Internal error: mismatch between selected compiler and compiler version").
 
 % define node_compiler_version_satisfies/3 from node_compiler_version_satisfies/4
 % version_satisfies implies that exactly one of the satisfying versions
 % is the package's version, and vice versa.
 1 { node_compiler_version(Package, Compiler, Version)
     : node_compiler_version_satisfies(Package, Compiler, Constraint, Version) } 1
-  :- node_compiler_version_satisfies(Package, Compiler, Constraint).
+  :- node_compiler_version_satisfies(Package, Compiler, Constraint), error("Internal error: node compiler version mismatch").
 node_compiler_version_satisfies(Package, Compiler, Constraint)
   :- node_compiler_version(Package, Compiler, Version),
      node_compiler_version_satisfies(Package, Compiler, Constraint, Version).
@@ -614,7 +630,8 @@ node_compiler_version(Package, Compiler, Version) :- node_compiler_version_set(P
 % are excluded from this check
 :- node_compiler_version(Package, Compiler, Version), node_os(Package, OS),
    not compiler_supports_os(Compiler, Version, OS),
-   not allow_compiler(Compiler, Version).
+   not allow_compiler(Compiler, Version),
+   error("No satisfying compiler available is compatible with a satisfying os").
 
 % If a package and one of its dependencies don't have the
 % same compiler there's a mismatch.

lib/spack/spack/spec.py

@@ -2608,10 +2608,7 @@ def _new_concretize(self, tests=False):
             return
 
         result = spack.solver.asp.solve([self], tests=tests)
-        if not result.satisfiable:
+        result.raise_if_unsat()
-            result.print_cores()
-            raise spack.error.UnsatisfiableSpecError(
-                self, "unknown", "Unsatisfiable!")
 
         # take the best answer
         opt, i, answer = min(result.answers)

lib/spack/spack/test/cmd/install.py

@@ -515,7 +515,7 @@ def test_cdash_report_concretization_error(tmpdir, mock_fetch, install_mockery,
             # new or the old concretizer
             expected_messages = (
                 'Conflicts in concretized spec',
-                'does not satisfy'
+                'A conflict was triggered',
             )
             assert any(x in content for x in expected_messages)