Introduce termination categories by 251 · Pull Request #1343 · klee/klee

251 · 2020-11-06T16:31:07Z

Introduce `StateTerminationClass/Type` and assign type to every state termination

The reasoning here is to track all path terminations: esp. for debugging or visualising a persistent process tree (with or without full MoKlee integration) it is helpful to know the exact reason (StateTerminationType) why a path terminated.

Thank you for contributing to KLEE. We are looking forward to reviewing your PR. However, given the small number of active reviewers and our limited time, it might take a while to do so. We aim to get back to each PR within one month, and often do so within one week.

To help expedite the review please ensure the following, by adding an "x" for each completed item:

The PR addresses a single issue. In other words, if some parts of a PR could form another independent PR, you should break this PR into multiple smaller PRs.
There are no unnecessary commits. For instance, commits that fix issues with a previous commit in this PR are unnecessary and should be removed (you can find documentation on squashing commits here).
Larger PRs are divided into a logical sequence of commits.
Each commit has a meaningful message documenting what it does.
The code is commented. In particular, newly added classes and functions should be documented.
The patch is formatted via clang-format (see also git-clang-format for Git integration). Please only format the patch itself and code surrounding the patch, not entire files. Divergences from clang-formatting are only rarely accepted, and only if they clearly improve code readability.
Add test cases exercising the code you added or modified. We expect system and/or unit test cases for all non-trivial changes. After you submit your PR, you will be able to see a Codecov report telling you which parts of your patch are not covered by the regression test suite. You will also be able to see if the Travis CI and Cirrus CI tests have passed. If they don't, you should examine the failures and address them before the PR can be reviewed.
Spellcheck all messages added to the codebase, all comments, as well as commit messages.

codecov · 2020-11-06T20:41:29Z

Codecov Report

Merging #1343 (ed57818) into master (a38ee31) will increase coverage by 0.00%.
The diff coverage is 61.00%.

❗ Current head ed57818 differs from pull request most recent head be783e0. Consider uploading reports for the commit be783e0 to get more accurate results

@@           Coverage Diff           @@
##           master    #1343   +/-   ##
=======================================
  Coverage   69.34%   69.35%           
=======================================
  Files         155      155           
  Lines       18473    18479    +6     
  Branches     4098     4098           
=======================================
+ Hits        12811    12816    +5     
+ Misses       3888     3886    -2     
- Partials     1774     1777    +3

Impacted Files	Coverage Δ
lib/Core/Executor.h	`77.27% <ø> (-1.90%)`	⬇️
lib/Core/SpecialFunctionHandler.cpp	`71.82% <51.61%> (ø)`
lib/Core/Executor.cpp	`77.48% <64.70%> (+0.03%)`	⬆️
lib/Core/MergeHandler.cpp	`93.50% <100.00%> (ø)`

ccadar

Hi @251 I took a look at the first (giant) commit and I like the changes quite a lot, although I have quite a number of small comments, which I'll do later directly in the code.

However, what I don't like is the removal of --silent-klee-assume and --dump-states-on-halt. I don't think the new --write-tests option can be used to replicate them exactly.

For --silent-klee-assume there are scenarios where you just want to ignore invalid klee-assumes while still dumping early test cases.

Similarly, for --dump-states-on-halt there are scenarios where you don't want to dump states on halt but still want to write other types of early test cases.

Unless I misunderstand the changes, I also don't like the fact that you now don't output states on solver errors.

Thanks again for these nice changes!

251 · 2021-01-23T13:13:48Z

@ccadar

For --silent-klee-assume there are scenarios where you just want to ignore invalid klee-assumes while still dumping early test cases.

I made a copy/paste mistake in the description above. A failed assume is in the "User"(-error) category that only contains things like failing assumes or wrong number of arguments provided to KLEE's API functions. Suppressing this category after initial testing might be fine. So, should I split that category or keep the option? I'd prefer keeping the user category as the number of handled cases is small and very specific and getting rid of the --silent-klee-assume option.

Similarly, for --dump-states-on-halt there are scenarios where you don't want to dump states on halt but still want to write other types of early test cases.

That sounds like I should split that category but what are those use cases? MaxDepth and Replay are a little specific but in general all states within that category were terminated for no other reason than hitting a limit (time, memory, depth, ...).

Unless I misunderstand the changes, I also don't like the fact that you now don't output states on solver errors.

It's off by default. I think it's probably not the best idea to query the solver for a state when a previous query failed but I can change that of course.

ccadar · 2021-02-16T18:35:05Z

@251 I took another look at this PR, and while I think the first commit requires a longer discussion, I think commits 2 and 4 should each form a separate PR, and could be merged quickly.

251 · 2021-05-07T19:26:57Z

@ccadar

Could you please have another look to discuss this? I trimmed the PR down as requested and added the solver category.

I've kept UncaughtException and UnexpectedException but have no idea where those are ever used... 🤷‍♂️

ccadar · 2021-11-06T19:47:49Z

Hi @251 , again, thanks again for this PR. I still like it, but it's way too large, both in terms of number of API changes as well as sheer lines of code, to review effectively.

If you are willing to give it another try, here is what I suggest:

Let's not remove any option for now, and keep the very same behaviour for them. Of course, if underneath you can make use of the new categories, that's great (although I believe it won't always be possible)
Don't make any unnecessary changes. I see a lot of nice refactorings, such as early returns, modern C++ features, and reformatting, but please make them in a follow-up PR, to keep the commit size manageable and make it possible to focus on the fundamental changes. If you prefer, I'm also happy with such a refactoring PR preceding this one.

251 · 2021-12-15T15:12:06Z

@ccadar I've removed the test generation part.

ccadar

Almost there, just some minor comments.

ccadar · 2021-12-20T17:48:18Z

include/klee/Core/TerminationTypes.h

+
+
+#define TERMINATION_TYPES \
+  TTYPE(RUNNING,0U,"") \


This doesn't look clang-formatted. Also, why 0U and not just 0?

Thanks for having a look!

Also, why 0U and not just 0?

Because I want unsigned literals.

But I don't see why here you need to be explicit with the "U" suffix. It looks ugly, unnecessarily.

Maybe not here but in the future one might re-use the macros in a different context and I'd prefer to assign the correct type to the literal instead of relying on implicit conversions (which cause too many bugs).

Can I ask why you force unsigned to begin with? All the code that I've seen uses ints, and avoids the ugly "1U". I'd be curious to understand your choice.

Can I ask why you force unsigned to begin with?

Because this is intended domain and I store it in a 1 byte unsigned enum directly below.

All the code that I've seen uses ints

For what? E.g. Misra C/C++ enforces 'U' for unsigned constants. For literals >2^31 C (imho) doesn't even specify what you actually get (signed or unsigned) and for smaller values you have to rely on the word width of the host. Too many rules to remember for me...

enum class'es are by default backed by signed ints in C++11. I feel you're over-optimising here -- as far as space goes, we won't have more than 100 termination reasons. But as I said, if you really like this, ok, it's minor.

we won't have more than 100 termination reasons

But we might have a lot of leaf nodes with termination reason in svg files or sqlite databases.

Ah, I see what you mean, but I don't understand what this has to do with signed vs unsigned, we will not need so many termination reasons.

Anyway, you seem to really like this optimization, so we can keep it, although as a reader I was wondering why we need the explicit unsigned constants, when we have so few different termination categories.

ccadar · 2021-12-20T17:48:35Z

lib/Core/Executor.cpp

+        clEnumValN(StateTerminationType::ReportError, "ReportError",
                   "klee_report_error called"),
-        clEnumValN(Executor::User, "User", "Wrong klee_* functions invocation"),
-#ifdef SUPPORT_KLEE_EH_CXX


Why did you remove these?

I couldn't find a single use. Did I miss one?

No, but perhaps it's something that we might need in the future? Can you see when this was added?

c09306f in #966 - I mean, we can add it in the future...

OK, if there are no (planned) uses, I'm fine with this.

lib/Core/Executor.h

lib/Core/SpecialFunctionHandler.cpp

251 · 2021-12-20T19:15:42Z

@ccadar I added a reformat commit.

ccadar · 2021-12-20T21:59:03Z

OK, let's try to merge this tonight! Just add those empty lines, reformat and squash the commits, and we can merge it!

Track all path terminations: esp. for debugging or visualising a persistent process tree (with or without full MoKlee integration) it is helpful to know the exact reason (StateTerminationType) why a path terminated.

ccadar · 2021-12-21T10:24:52Z

Alright, ready to merge!

There are quite a number of uncovered lines (which is why codecov fails), and it would be nice to have test cases for each termination criteria. But since this is mostly a refactoring, we'll leave this under what you call Catch-22 and won't ask you to add tests ;) Of course, if you'd like to do this, let me know.

Thanks again for this useful change, looking forward to the ones that had this as a dependency.

251 · 2021-12-23T11:14:34Z

@ccadar

Of course, if you'd like to do this, let me know.

I'd like to postpone it to another PR. The next will introduce BranchTypes and the following one the necessary statistics to test those cases more easily.

ccadar · 2021-12-23T17:43:08Z

@251 Sounds good, looking forward to the next ones (keep them small too!)
Great to see this finally merged!

251 force-pushed the termination_categories branch 3 times, most recently from 00e21de to 57c564d Compare November 6, 2020 20:36

251 force-pushed the termination_categories branch 5 times, most recently from db25738 to 215b441 Compare November 18, 2020 20:24

This was referenced Nov 18, 2020

Introduce BranchTypes (requires #1343) #1348

Merged

Introduce persistent process tree #1349

Closed

ccadar requested changes Dec 21, 2020

View reviewed changes

251 mentioned this pull request Feb 24, 2021

Fix path stats for disabled state dumping and output completed/partially completed paths at the end #1387

Merged

8 tasks

251 marked this pull request as draft March 5, 2021 09:50

251 force-pushed the termination_categories branch from 215b441 to 3e13f8a Compare May 7, 2021 18:51

251 force-pushed the termination_categories branch from 3e13f8a to 8d57080 Compare May 8, 2021 09:47

251 force-pushed the termination_categories branch from 8d57080 to 2ed9d6c Compare December 15, 2021 14:37

ccadar requested changes Dec 20, 2021

View reviewed changes

251 force-pushed the termination_categories branch from ed57818 to b0ed918 Compare December 20, 2021 22:04

Introduce termination categories

be783e0

Track all path terminations: esp. for debugging or visualising a persistent process tree (with or without full MoKlee integration) it is helpful to know the exact reason (StateTerminationType) why a path terminated.

251 force-pushed the termination_categories branch from b0ed918 to be783e0 Compare December 20, 2021 22:11

251 marked this pull request as ready for review December 20, 2021 22:13

ccadar approved these changes Dec 21, 2021

View reviewed changes

ccadar merged commit 799ab80 into klee:master Dec 23, 2021

251 deleted the termination_categories branch December 23, 2021 18:27

ccadar mentioned this pull request Jan 18, 2022

Support UBSan-enabled binaries #1378

Merged

8 tasks

Conversation

251 commented Nov 6, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Introduce StateTerminationClass/Type and assign type to every state termination

Uh oh!

codecov bot commented Nov 6, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

ccadar left a comment

Choose a reason for hiding this comment

Uh oh!

251 commented Jan 23, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ccadar commented Feb 16, 2021

Uh oh!

251 commented May 7, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ccadar commented Nov 6, 2021

Uh oh!

251 commented Dec 15, 2021

Uh oh!

ccadar left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

251 Dec 20, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

251 commented Dec 20, 2021

Uh oh!

ccadar commented Dec 20, 2021

Uh oh!

ccadar commented Dec 21, 2021

Uh oh!

251 commented Dec 23, 2021

Uh oh!

ccadar commented Dec 23, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

251 commented Nov 6, 2020 •

edited

Loading

Introduce `StateTerminationClass/Type` and assign type to every state termination

codecov bot commented Nov 6, 2020 •

edited

Loading

251 commented Jan 23, 2021 •

edited

Loading

251 commented May 7, 2021 •

edited

Loading

251 Dec 20, 2021 •

edited

Loading