From b3711c0d9d07b8b0e673adc49f5742d90cf48a12 Mon Sep 17 00:00:00 2001 From: Greg Becker Date: Tue, 2 Nov 2021 10:55:50 -0700 Subject: 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 --- lib/spack/spack/cmd/solve.py | 5 +- lib/spack/spack/concretize.py | 6 +- lib/spack/spack/error.py | 23 ++++- lib/spack/spack/solver/asp.py | 183 ++++++++++++++++++++++++++++++----- lib/spack/spack/solver/concretize.lp | 71 ++++++++------ lib/spack/spack/spec.py | 5 +- lib/spack/spack/test/cmd/install.py | 2 +- 7 files changed, 223 insertions(+), 72 deletions(-) (limited to 'lib') diff --git a/lib/spack/spack/cmd/solve.py b/lib/spack/spack/cmd/solve.py index d276fa3a43..e2563ef0c8 100644 --- a/lib/spack/spack/cmd/solve.py +++ b/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 - if not result.satisfiable: - result.print_cores() - tty.die("Unsatisfiable spec.") + result.raise_if_unsat() # dump the solutions as concretized specs if 'solutions' in dump: diff --git a/lib/spack/spack/concretize.py b/lib/spack/spack/concretize.py index 905037787f..1b865c32cc 100644 --- a/lib/spack/spack/concretize.py +++ b/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) - - if not result.satisfiable: - result.print_cores() - tty.die("Unsatisfiable spec.") - + result.raise_if_unsat() return [s.copy() for s in result.specs] diff --git a/lib/spack/spack/error.py b/lib/spack/spack/error.py index f0283e27c1..be49656c07 100644 --- a/lib/spack/spack/error.py +++ b/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.""" - def __init__(self, provided, required, constraint_type): - super(UnsatisfiableSpecError, self).__init__( - "%s does not satisfy %s" % (provided, required)) + """ + Raised when a spec conflicts with package constraints. + + For original concretizer, provide the requirement that was violated when + 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 diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py index 8bafa075db..2d70df210f 100644 --- a/lib/spack/spack/solver/asp.py +++ b/lib/spack/spack/solver/asp.py @@ -52,6 +52,25 @@ if sys.version_info >= (3, 3): 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 @@ class Result(object): 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 @@ class Result(object): # Concrete specs self._concrete_specs = None - def print_cores(self): - for core in self.cores: - tty.msg( - "The following constraints are unsatisfiable:", - *sorted(str(symbol) for symbol in core)) + def format_core(self, core): + """ + Format an unsatisfiable core for human readability + + 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 @@ class PyclingoDriver(object): asp (file-like): optional stream to write a text-based ASP program for debugging or verification. """ - global clingo - if not clingo: - with spack.bootstrap.ensure_bootstrap_configuration(): - spack.bootstrap.ensure_clingo_importable_or_raise() - import clingo + bootstrap_clingo() + self.out = asp or llnl.util.lang.Devnull() self.cores = cores @@ -311,15 +420,22 @@ class PyclingoDriver(object): def newline(self): self.out.write('\n') - def fact(self, head): - """ASP fact (a rule without a body).""" + def fact(self, head, assumption=False): + """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) - if self.cores: + choice = self.cores and assumption + self.backend.add_rule([atom], [], choice=choice) + if choice: self.assumptions.append(atom) def solve( @@ -347,6 +463,22 @@ class PyclingoDriver(object): # 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 @@ class PyclingoDriver(object): 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 @@ class PyclingoDriver(object): result.nmodels = len(models) elif cores: - symbols = dict( - (a.literal, a.symbol) - 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) + result.control = self.control + result.cores.extend(cores) if timers: timer.write_tty() @@ -1372,6 +1495,14 @@ class SpackSolverSetup(object): 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 diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp index 83fcd9a908..a65a0d530e 100644 --- a/lib/spack/spack/solver/concretize.lp +++ b/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. diff --git a/lib/spack/spack/spec.py b/lib/spack/spack/spec.py index 692c7522f3..2c5e6086e1 100644 --- a/lib/spack/spack/spec.py +++ b/lib/spack/spack/spec.py @@ -2608,10 +2608,7 @@ class Spec(object): return result = spack.solver.asp.solve([self], tests=tests) - if not result.satisfiable: - result.print_cores() - raise spack.error.UnsatisfiableSpecError( - self, "unknown", "Unsatisfiable!") + result.raise_if_unsat() # take the best answer opt, i, answer = min(result.answers) diff --git a/lib/spack/spack/test/cmd/install.py b/lib/spack/spack/test/cmd/install.py index 7fcf3658aa..b0b10d1287 100644 --- a/lib/spack/spack/test/cmd/install.py +++ b/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) -- cgit v1.2.3-70-g09d2