Skip to content

Introduce BranchTypes (requires #1343)#1348

Merged
ccadar merged 1 commit intoklee:masterfrom
251:branch_types
Jan 5, 2022
Merged

Introduce BranchTypes (requires #1343)#1348
ccadar merged 1 commit intoklee:masterfrom
251:branch_types

Conversation

@251
Copy link
Contributor

@251 251 commented Nov 18, 2020 •
edited
Loading

This PR extends #1343 and keeps track of the different branch types.

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.

@251 251 changed the title Branch types (requires #1343) Introduce BranchTypes (requires #1343) Nov 18, 2020
@251 251 changed the title Introduce BranchTypes (requires #1343) Introduce BranchTypes (requires #1343) Nov 18, 2020
@251 251 mentioned this pull request Nov 18, 2020
Closed
8 tasks
@codecov
Copy link

codecov bot commented Nov 19, 2020 •
edited
Loading

Codecov Report

Merging #1348 (8d4a0a3) into master (62e27ff) will decrease coverage by 0.00%.
The diff coverage is 95.00%.

@@            Coverage Diff             @@
##           master    #1348      +/-   ##
==========================================
- Coverage   69.35%   69.34%   -0.01%     
==========================================
  Files         155      155              
  Lines       18479    18476       -3     
  Branches     4098     4098              
==========================================
- Hits        12816    12813       -3     
  Misses       3886     3886              
  Partials     1777     1777
Impacted Files Coverage Δ
lib/Core/Executor.h 77.27% <ø> (ø)
lib/Core/PTree.h 100.00% <ø> (ø)
lib/Core/Executor.cpp 77.48% <93.75%> (ø)
lib/Core/PTree.cpp 78.66% <100.00%> (ø)
lib/Core/SpecialFunctionHandler.cpp 71.58% <100.00%> (-0.24%) ⬇️

@251 251 marked this pull request as draft February 24, 2021 20:03
@251 251 marked this pull request as ready for review December 23, 2021 18:31
@251
Copy link
Contributor Author

251 commented Dec 23, 2021

@ccadar Ready for review. The argument in PTree::attach is currently unused, I'll implement it in one of the next PRs.

MartinNowack
MartinNowack reviewed Jan 5, 2022
View reviewed changes
Copy link
Contributor

@MartinNowack MartinNowack left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@251 Changes look great!

Maybe rename branch type Br to Branch (and maybe IndirectBr to IndirectBranch). That improves readability.

Beside that, I'm more than happy with those changes.

ccadar
ccadar requested changes Jan 5, 2022
View reviewed changes
Copy link
Contributor

@ccadar ccadar left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, @251, I like the changes too.

But could you add a bit of documentation about each branch type? E.g., what is BranchType::Exact, it's not an intuitive name? Why do we have BranchType::UNKNOWN?

Also, do you ever use BrachType::Alloc?

BrachType::Branch sounds funny: maybe BranchType::DirectBranch (and BranchType::IndirectBranch)?

BranchType::Memop should be BranchType::MemOp to be consistent with the capitalization.

Thanks!

@251
Copy link
Contributor Author

251 commented Jan 5, 2022

@ccadar @MartinNowack

Thanks for the review.

Maybe rename branch type Br to Branch (and maybe IndirectBr to IndirectBranch).

Done. I initially kept the LLVM instruction names.

But could you add a bit of documentation about each branch type?

I've added a doxygen table in the header file.

ccadar
ccadar requested changes Jan 5, 2022
View reviewed changes
Copy link
Contributor

@ccadar ccadar left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, @251 , I love the table, really useful as high-level documentation too.
A few more small comments, as we'll stick with these names:

  • I still find UNKNOWN confusing, as well as the explanation "no branch yet". As far as I can see, it's only used in unit tests, and doesn't occur during regular execution. Should we perhaps say it's for test purposes? Or do you see other future uses?
  • I missed the capitalization for Getval, should be GetVal
  • I think Resolve would be more meaningful than Exact, which I find confusing
  • Can you make the comments for Alloc and Realloc similar?
  • I find the order weird. I would propose: DirectBranch, IndirectBranch, Switch, Call, MemOp, Resolve, Alloc, Realloc, UNKNOWN.

Thanks again!

@MartinNowack
Copy link
Contributor

MartinNowack commented Jan 5, 2022

@251 Great updates, maybe one thing: DirectBranch -> ConditionalBranch. That describes better what's actually tracked.

@251
Copy link
Contributor Author

251 commented Jan 5, 2022

@ccadar

and doesn't occur during regular execution

It does. The goal is to track branches in ptree nodes. E.g. for a concrete execution or in leave nodes there is "no branch yet". Would "NONE" be better?

I think Resolve would be more meaningful than Exact, which I find confusing

ResolvePointer?

@MartinNowack

Great updates, maybe one thing: DirectBranch -> ConditionalBranch.

Fine with me.

@ccadar
Copy link
Contributor

ccadar commented Jan 5, 2022

@251 Thanks, everything looks good to me now! I still find the explanation about NONE somewhat confusing, but perhaps it can be explained better once more uses are added.

@ccadar
Copy link
Contributor

ccadar commented Jan 5, 2022

So let's merge it now!

@ccadar ccadar merged commit 27cfe79 into klee:master Jan 5, 2022
@251 251 deleted the branch_types branch January 5, 2022 22:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@MartinNowack MartinNowack MartinNowack left review comments

@ccadar ccadar ccadar approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@251 @MartinNowack @ccadar