solver: dump output specs to file if not satisfied (#50019)

When the solver produces specs that do not satisfy the input
constraints, dump both input and output specs as json in an temporary
dir and ask the user to upload these files in a bug report.

lib/spack/spack/main.py

@@ -20,6 +20,7 @@
 import signal
 import subprocess as sp
 import sys
+import tempfile
 import traceback
 import warnings
 from typing import List, Tuple
@@ -41,6 +42,7 @@
 import spack.paths
 import spack.platforms
 import spack.repo
+import spack.solver.asp
 import spack.spec
 import spack.store
 import spack.util.debug
@@ -1046,6 +1048,10 @@ def main(argv=None):
     try:
         return _main(argv)
 
+    except spack.solver.asp.OutputDoesNotSatisfyInputError as e:
+        _handle_solver_bug(e)
+        return 1
+
     except spack.error.SpackError as e:
         tty.debug(e)
         e.die()  # gracefully die on any SpackErrors
@@ -1069,5 +1075,45 @@ def main(argv=None):
         return 3
 
 
+def _handle_solver_bug(
+    e: spack.solver.asp.OutputDoesNotSatisfyInputError, out=sys.stderr, root=None
+) -> None:
+    # when the solver outputs specs that do not satisfy the input and spack is used as a command
+    # line tool, we dump the incorrect output specs to json so users can upload them in bug reports
+    wrong_output = [(input, output) for input, output in e.input_to_output if output is not None]
+    no_output = [input for input, output in e.input_to_output if output is None]
+    if no_output:
+        tty.error(
+            "internal solver error: the following specs were not solved:\n    - "
+            + "\n    - ".join(str(s) for s in no_output),
+            stream=out,
+        )
+    if wrong_output:
+        msg = (
+            "internal solver error: the following specs were concretized, but do not satisfy the "
+            "input:\n    - "
+            + "\n    - ".join(str(s) for s, _ in wrong_output)
+            + "\n    Please report a bug at https://github.com/spack/spack/issues"
+        )
+        # try to write the input/output specs to a temporary directory for bug reports
+        try:
+            tmpdir = tempfile.mkdtemp(prefix="spack-asp-", dir=root)
+            files = []
+            for i, (input, output) in enumerate(wrong_output, start=1):
+                in_file = os.path.join(tmpdir, f"input-{i}.json")
+                out_file = os.path.join(tmpdir, f"output-{i}.json")
+                files.append(in_file)
+                files.append(out_file)
+                with open(in_file, "w", encoding="utf-8") as f:
+                    input.to_json(f)
+                with open(out_file, "w", encoding="utf-8") as f:
+                    output.to_json(f)
+
+            msg += " and attach the following files:\n    - " + "\n    - ".join(files)
+        except Exception:
+            msg += "."
+        tty.error(msg, stream=out)
+
+
 class SpackCommandError(Exception):
     """Raised when SpackCommand execution fails."""

lib/spack/spack/solver/asp.py

@@ -1287,12 +1287,8 @@ def on_model(model):
             result.raise_if_unsat()
 
             if result.satisfiable and result.unsolved_specs and setup.concretize_everything:
-                unsolved_str = Result.format_unsolved(result.unsolved_specs)
+                raise OutputDoesNotSatisfyInputError(result.unsolved_specs)
-                raise InternalConcretizerError(
+
-                    "Internal Spack error: the solver completed but produced specs"
-                    " that do not satisfy the request. Please report a bug at "
-                    f"https://github.com/spack/spack/issues\n\t{unsolved_str}"
-                )
             if conc_cache_enabled:
                 CONC_CACHE.store(problem_repr, result, self.control.statistics, test=setup.tests)
             concretization_stats = self.control.statistics
@@ -4651,13 +4647,9 @@ def solve_in_rounds(
                 break
 
             if not result.specs:
-                # This is also a problem: no specs were solved for, which
+                # This is also a problem: no specs were solved for, which means we would be in a
-                # means we would be in a loop if we tried again
+                # loop if we tried again
-                unsolved_str = Result.format_unsolved(result.unsolved_specs)
+                raise OutputDoesNotSatisfyInputError(result.unsolved_specs)
-                raise InternalConcretizerError(
-                    "Internal Spack error: a subset of input specs could not"
-                    f" be solved for.\n\t{unsolved_str}"
-                )
 
             input_specs = list(x for (x, y) in result.unsolved_specs)
             for spec in result.specs:
@@ -4687,6 +4679,19 @@ def __init__(self, msg):
         self.constraint_type = None
 
 
+class OutputDoesNotSatisfyInputError(InternalConcretizerError):
+
+    def __init__(
+        self, input_to_output: List[Tuple[spack.spec.Spec, Optional[spack.spec.Spec]]]
+    ) -> None:
+        self.input_to_output = input_to_output
+        super().__init__(
+            "internal solver error: the solver completed but produced specs"
+            " that do not satisfy the request. Please report a bug at "
+            f"https://github.com/spack/spack/issues\n\t{Result.format_unsolved(input_to_output)}"
+        )
+
+
 class SolverError(InternalConcretizerError):
     """For cases where the solver is unable to produce a solution.
 

lib/spack/spack/test/concretization/core.py

@@ -1831,10 +1831,7 @@ def test_solve_in_rounds_all_unsolved(self, monkeypatch, mock_packages):
         monkeypatch.setattr(spack.solver.asp.Result, "unsolved_specs", simulate_unsolved_property)
         monkeypatch.setattr(spack.solver.asp.Result, "specs", list())
 
-        with pytest.raises(
+        with pytest.raises(spack.solver.asp.OutputDoesNotSatisfyInputError):
-            spack.solver.asp.InternalConcretizerError,
-            match="a subset of input specs could not be solved for",
-        ):
             list(solver.solve_in_rounds(specs))
 
     def test_coconcretize_reuse_and_virtuals(self):

lib/spack/spack/test/concretization/errors.py

@@ -2,11 +2,15 @@
 #
 # SPDX-License-Identifier: (Apache-2.0 OR MIT)
 
+from io import StringIO
+
 import pytest
 
 import spack.concretize
 import spack.config
+import spack.main
 import spack.solver.asp
+import spack.spec
 
 version_error_messages = [
     "Cannot satisfy",
@@ -60,3 +64,31 @@ def test_error_messages(error_messages, config_set, spec, mock_packages, mutable
 
     for em in error_messages:
         assert em in str(e.value)
+
+
+def test_internal_error_handling_formatting(tmp_path):
+    log = StringIO()
+    input_to_output = [
+        (spack.spec.Spec("foo+x"), spack.spec.Spec("foo@=1.0~x")),
+        (spack.spec.Spec("bar+y"), spack.spec.Spec("x@=1.0~y")),
+        (spack.spec.Spec("baz+z"), None),
+    ]
+    spack.main._handle_solver_bug(
+        spack.solver.asp.OutputDoesNotSatisfyInputError(input_to_output), root=tmp_path, out=log
+    )
+
+    output = log.getvalue()
+    assert "the following specs were not solved:\n    - baz+z\n" in output
+    assert (
+        "the following specs were concretized, but do not satisfy the input:\n"
+        "    - foo+x\n"
+        "    - bar+y\n"
+    ) in output
+
+    files = {f.name: str(f) for f in tmp_path.glob("spack-asp-*/*.json")}
+    assert {"input-1.json", "input-2.json", "output-1.json", "output-2.json"} == set(files.keys())
+
+    assert spack.spec.Spec.from_specfile(files["input-1.json"]) == spack.spec.Spec("foo+x")
+    assert spack.spec.Spec.from_specfile(files["input-2.json"]) == spack.spec.Spec("bar+y")
+    assert spack.spec.Spec.from_specfile(files["output-1.json"]) == spack.spec.Spec("foo@=1.0~x")
+    assert spack.spec.Spec.from_specfile(files["output-2.json"]) == spack.spec.Spec("x@=1.0~y")