Refactor metaval tool-info module:extend BaseTool2 #650

MartinSpiessl · 2020-10-28T12:27:24Z

This updates the metaval tool-info module to inherit from the new BaseTool2 base class.

benchexec/tools/metaval.py

PhilippWendler

I think _in_tool_directory can also be removed?

And note that determine_result also needs to be updated.

PhilippWendler · 2020-10-29T15:57:49Z

benchexec/tools/metaval.py

@@ -8,14 +8,15 @@
 import argparse
 import benchexec.util as util


Suggested change

import benchexec.util as util

Unused import.

benchexec/tools/metaval.py

PhilippWendler · 2020-10-29T16:41:25Z

benchexec/tools/metaval.py

+            wrappedOptions = self.wrappedTools[verifierName].cmdline(
+                wrapped_executable,
+                options,
+                [os.path.relpath(os.path.join(os.getcwd(), "output/ARG.c"))],


This actually always produces ["output/ARG.c"] because you first join it with the current directory and then make it relative to the current directory again. So this can be simplified.

But more importantly, new tool-info modules require a Task instance here.

Hmm, this worked alright at the time we drafted the code (I think it was #602), what changed inbetween?

This was done as part of #592, i.e., the introduction of BaseTool2. The changes to MetaVal's tool-info module were based on an intermediate draft version of that API.

If you are not yet familiar with it, I recommend having a look at our migration guide that covers the full set of differences between BaseTool and BaseTool2.

That migration guide can be improved, it doesn't even list the method signatures. It will be quicker reading the actual code.

This actually always produces ["output/ARG.c"] because you first join it with the current directory and then make it relative to the current directory again. So this can be simplified.

Yeah this is probably broken anyway because it actually has to be ["../output/ARG.c"], because the output folder will actually be created outside of the wrapped tool's directory. I guess this is a result of the refactoring where we replace the context manager. At that time the code probably used the cached working directory of metaval instead of os.getcwd(). I will need to do some tool testing anyway to see whether this still works.

4f1313e should fix this by passing a proper Task object, but I have no way of knowing until #646 is merged, I manually merge that PR into this PR (with high chance that this will cause more work than it will save) or readd the BaseTool checks

Do you mean because you need a working BaseTool2 tool-info module to test your PR? You can do this with CPAchecker's module, it has been upgraded already.

From my point of view, this and the (now 3) unused imports are the only remaining things to do. So please ping me after you finished and tested this, then I will merge.

Note that now #646 was merged, so not only CPAchecker's tool-info module but also others are now available for testing.

Open points should be addressed via:
444a46c
e9ae4f3
8fee3ad

I also found some bugs via testing and fixed those as well:
0bc3605

Accidentally overlooked/reintroduced some unused imports, those should be fine with:
b2adf40

benchexec/tools/metaval.py

In practice if we wrap a tool that still extends BaseTool, we should adapt that tool to the new BaseTool2 instead of having to handle this case inside the tool-info module of MetaVal.

It is probably a bad idea anyway to have this mapping in the tool-info module. For now we just make the names generic, later we might want to move this into the tool instead.

@PhilippWendler

According to @PhilippWendler

PhilippWendler

I have to fix another unused import, but now it seems fine.

PhilippWendler · 2020-11-21T10:18:49Z

For the future: force-pushes make it harder to review on GitHub, essentially I have to reread all the code every time. For keeping the branch up-to-date, a regular merge would mean less effort for me. Furthermore, now you even copied a commit from another committer onto your branch, probably due to a wrong rebase, such that now we have that commit twice in the history.

Force pushes can be a nice tool for cleaning up the history of a branch to remove small fixups etc. (but they were not used in this regard here).

MartinSpiessl · 2020-11-21T11:30:14Z

https://gitlab.com/sosy-lab/software/coveriteam-remote-server/-/merge_requests/6

What makes you thing this could happen by a rebase? I cherry-picked that one because I needed it for testing, and forgot to remove it again when I pushed the last change.

a regular merge would mean less effort for me

Sure, will do next time.

PhilippWendler · 2020-11-21T12:00:29Z

What makes you thing this could happen by a rebase?

Because I have seen such things happen due to rebases. I would happen if rebasing something else onto a branch instead of the branch on something else.

PhilippWendler added the tool support label Oct 28, 2020

MartinSpiessl marked this pull request as draft October 28, 2020 13:17

MartinSpiessl marked this pull request as ready for review October 28, 2020 15:01

PhilippWendler requested changes Oct 29, 2020

View reviewed changes

benchexec/tools/metaval.py Outdated Show resolved Hide resolved

benchexec/tools/metaval.py Outdated Show resolved Hide resolved

MartinSpiessl requested a review from PhilippWendler October 29, 2020 15:53

PhilippWendler requested changes Oct 29, 2020

View reviewed changes

MartinSpiessl force-pushed the tool-locator-metaval branch from 4a2e3f3 to 62289b0 Compare October 29, 2020 17:22

MartinSpiessl closed this Oct 29, 2020

MartinSpiessl reopened this Oct 29, 2020

MartinSpiessl added 13 commits November 16, 2020 20:35

Refactor metaval tool-info module:extend BaseTool2

5c56e3d

Simplify tool-info module of MetaVal

d55811a

In practice if we wrap a tool that still extends BaseTool, we should adapt that tool to the new BaseTool2 instead of having to handle this case inside the tool-info module of MetaVal.

Make MetaVal's wrapped tool folders more generic

a2a8b62

It is probably a bad idea anyway to have this mapping in the tool-info module. For now we just make the names generic, later we might want to move this into the tool instead.

Correct imprecise naming in MetaVal

304f0c0

Remove more BaseTool handling from MetaVal module

3b0c018

Implement some feedback from the metaval PR review

9de5fb6

Refactor metaval tool-info module for less indents

e6fb27b

Remove unused import

a24f7db

Remove check that can never fail

d6404b7

According to @PhilippWendler

Pass a Task object to cmdline() in MetaVal module

444a46c

Simplify path handling in metaval tool-info module

e9ae4f3

Remove unused imports from tool-info mod. metaval

8fee3ad

Fix some bugs in metaval discovered via testing

0bc3605

MartinSpiessl force-pushed the tool-locator-metaval branch from 4f1313e to 0bc3605 Compare November 16, 2020 19:35

MartinSpiessl and others added 4 commits November 21, 2020 02:06

Remove unused import

b2adf40

fix sosy-lab#661: do not return None but empty list

1f6e0b1

Update additional option for MetaVal

001f81d

Remove another unused import

b4acb12

PhilippWendler approved these changes Nov 21, 2020

View reviewed changes

PhilippWendler merged commit 440339d into sosy-lab:master Nov 21, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor metaval tool-info module:extend BaseTool2 #650

Refactor metaval tool-info module:extend BaseTool2 #650

MartinSpiessl commented Oct 28, 2020

PhilippWendler left a comment

PhilippWendler Oct 29, 2020

PhilippWendler Oct 29, 2020

MartinSpiessl Oct 29, 2020

PhilippWendler Oct 29, 2020

MartinSpiessl Oct 29, 2020

MartinSpiessl Oct 29, 2020

MartinSpiessl Oct 29, 2020

PhilippWendler Oct 30, 2020

PhilippWendler Oct 30, 2020

PhilippWendler Nov 3, 2020

MartinSpiessl Nov 21, 2020

PhilippWendler left a comment

PhilippWendler commented Nov 21, 2020

MartinSpiessl commented Nov 21, 2020

PhilippWendler commented Nov 21, 2020

		@@ -8,14 +8,15 @@
		import argparse
		import benchexec.util as util

Refactor metaval tool-info module:extend BaseTool2 #650

Refactor metaval tool-info module:extend BaseTool2 #650

Conversation

MartinSpiessl commented Oct 28, 2020

PhilippWendler left a 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

PhilippWendler left a comment

Choose a reason for hiding this comment

PhilippWendler commented Nov 21, 2020

MartinSpiessl commented Nov 21, 2020

PhilippWendler commented Nov 21, 2020