BugReport reporter #770

gtrepta · 2023-12-08T19:37:25Z

src/pyk/utils.py

tothtamas28 · 2024-01-29T08:40:21Z

src/pyk/utils.py

+    def add_file(self, finput: Path, arcname: Path) -> None:
+        pass
+
+    def add_file_contents(self, input: str, arcname: Path) -> None:
+        pass
+
+    def add_command(self, args: Iterable[str]) -> None:
+        pass


By organizing the code this way, this will not break:

br = BugReporter(Path('foo')) br.add_file(Path('bar'), Path('baz'))

yet the bug report entry will not be written.

BugReporter should not be a BugReport, and these methods should be removed from BugReport.

Then spurious methods like _check_bug_report can also be removed from BugReporter.

How should users instantiate a bug report? It looks to me that currently the bug_report_arg parameter from cli is the primary use case, and I've ensured that the reporter coming from there works. The intent was to have BugReporter only be instantiated by a call to BugReport.reporter, and have BugReport hold the base interface, file paths, and synchronization primitive to spawn reporters from. Something like your example that doesn't write to a file can certainly be a problem if it isn't discouraged in some way, like renaming the class to _BugReporter so it doesn't get imported or used as easily.

If we want to allow users to directly create a BugReport or a BugReporter then I'll have to think a bit more about what this should look like.

I made BugReporter an inherited class because BugReport is expected in many places like KRun and Kompile, and wanted to keep those interfaces stable.

How should users instantiate a bug report?

In the final design, users should be able to instantiate a BugReport (i.e. the BugReporter factory) directly. On the other hand, BugReporter (i.e. the replacement of the old BugReport) should only be instantiated through BugReporter.

(We can also consider a composite design where a BugReporter can instantiate further BugReporter instances, e.g. a BugReporter for a proof process creates a BugReporter for one of the KoreClient instances it manages.)

BugReport is expected in many places like KRun and Kompile, and wanted to keep those interfaces stable.

I see why this is a good approach, but ultimately the goal is to get rid of the old interface, and instead

Let the user decide where to write the archive: BugReport.

Let the application (e.g. kontrol) decide how to structure the archive: BugReporter.

Let the library (e.g. KoreServer) be responsible only for what's written to the archive.

One way to achieve this:

Turn BugReport into an abstract class

Have two implementations: 1) old behavior 2) BugReporter

Gradually replace old behavior by BugReporter

Do the renamings

All this doesn't have to be achieved in a single PR.

I've force pushed this branch with a change that implements 1 and 2. There's no thread safety over the BugReporter yet, if you're happy with deferring that to a later PR then we should be able to merge this.

tothtamas28 · 2024-01-29T08:42:51Z

src/pyk/utils.py

    _command_id: int
    _defn_id: int
    _file_remap: dict[str, str]
+    _lock: Lock


What properties does this lock ensure?

Assuming the usage pattern expected in my above comment, this Lock should be shared by all BugReporters that were created off of the same BugReport, so that only one of them can write to the file at a time.

What happens in a multiprocessing scenario, i.e. when the Lock gets pickled and sent to another Python process? Will it still ensure mutual exclusion?

By the looks of it, pickling Lock objects isn't supported. Would this be an issue?

Yes, we use multiprocessing quite intensively in kontrol.

An alternative would be a file lock (filelock, cross-platform) or OS level locking (os.lockf, fcntl, only on Unix). Also, please check whether tarfile does any form of locking, maybe it already does.

tothtamas28 · 2024-01-29T08:47:56Z

src/pyk/utils.py

+    def add_command(self, args: Iterable[str]) -> None:
+        pass
+
+    def reporter(self, prefix: Path) -> BugReporter:


Suggested change

def reporter(self, prefix: Path) -> BugReporter:

def reporter(self, prefix: str) -> BugReporter:

What happens if two threads request a reporter to the same prefix?

They will both be writing to the same prefix in the bug report archive. The Lock should ensure that they don't write at the same time, but it is possible that they write to the same path, which in this implementation I believe will work like an append. It should probably be up to the user whether that's an issue or not.

I think we can safely introduce this restriction (i.e. let the BugReporter own its prefix) as the way we use the archive is always adding new things to it.

If the same prefix is requested twice, the call can either fail, or the target directory can be renamed to make it unique:

foo foo_1 foo_2 ...

What do you think?

Renaming while logging a message about it sounds reasonable.

tothtamas28 · 2024-02-02T09:30:14Z

src/pyk/utils.py

@@ -524,3 +521,26 @@ def _remap_arg(_a: str) -> str:
        shebang = '#!/usr/bin/env bash\nset -euxo pipefail\n'
        self.add_file_contents(shebang + ' '.join(remapped_args) + '\n', arcname)
        self._command_id += 1
+
+
+class BugReport(BugReportBase):


Consider this hierarchy instead:

BugReportBase - abstract class without any actual implementation.

BugReport - same as before, but now implements BugReportBase.

BugReport2 - something that can instantiate a BugReporter for a prefix.

BugReporter - a BugReportBase that writes into a folder of an archive.

This is the easy part as so far, nothing breaks. The hard part is eliminating BugReport in favor of the new design, which will be a breaking change in pyk and in downstream projects.

We should only merge the PR with the new classes once we have a plan on how to manage the rest. To get the intuition of what needs to be changed, you can rename BugReport and see where the type checker complains.

gtrepta requested a review from tothtamas28 December 8, 2023 19:37

gtrepta mentioned this pull request Dec 8, 2023

BugReport should not be written directly runtimeverification/k#4189

Open

gtrepta marked this pull request as ready for review December 8, 2023 19:59

tothtamas28 reviewed Dec 11, 2023

View reviewed changes

src/pyk/utils.py Outdated Show resolved Hide resolved

gtrepta requested a review from tothtamas28 December 11, 2023 17:59

tothtamas28 reviewed Jan 29, 2024

View reviewed changes

BugReportBase and BugReporter

078e994

gtrepta force-pushed the bugreport-reporter branch from 56f932e to 078e994 Compare February 1, 2024 20:34

gtrepta and others added 2 commits February 1, 2024 14:34

Merge 078e994 into eb48e22

b7812f0

Set Version: 0.1.612

c12d726

tothtamas28 reviewed Feb 2, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

BugReport reporter #770

BugReport reporter #770

gtrepta commented Dec 8, 2023

tothtamas28 Jan 29, 2024

tothtamas28 Jan 29, 2024

gtrepta Jan 29, 2024

tothtamas28 Jan 30, 2024

gtrepta Feb 1, 2024

tothtamas28 Jan 29, 2024

gtrepta Jan 29, 2024

tothtamas28 Jan 30, 2024

gtrepta Jan 31, 2024

tothtamas28 Feb 1, 2024

tothtamas28 Jan 29, 2024

tothtamas28 Jan 29, 2024

gtrepta Jan 29, 2024

tothtamas28 Jan 30, 2024

gtrepta Jan 31, 2024

tothtamas28 Feb 2, 2024

	def reporter(self, prefix: Path) -> BugReporter:
	def reporter(self, prefix: str) -> BugReporter:

BugReport reporter #770

Are you sure you want to change the base?

BugReport reporter #770

Conversation

gtrepta commented Dec 8, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment