Skip to content

Introduce persistent execution tree (extends #1349 with a rename)#1674

Closed
ccadar wants to merge 3 commits intoklee:masterfrom
ccadar:ptree
Closed

Introduce persistent execution tree (extends #1349 with a rename)#1674
ccadar wants to merge 3 commits intoklee:masterfrom
ccadar:ptree

Conversation

@ccadar
Copy link
Contributor

@ccadar ccadar commented Dec 12, 2023

Summary:

Introduce persistent execution tree (extends #1349 with a rename)

Checklist:

  • The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
  • The PR is divided into a logical sequence of commits OR a single commit is sufficient.
  • There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
  • Each commit has a meaningful message documenting what it does.
  • All messages added to the codebase, all comments, as well as commit messages are spellchecked.
  • The code is commented OR not applicable/necessary.
  • The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
  • There are test cases for the code you added or modified OR no such test cases are required.

251 added 2 commits November 24, 2023 18:12
@251
new: persistent ptree (-write-ptree) and klee-ptree
017c5e1 
Introduce three different kinds of process trees:
1. Noop: does nothing (e.g. no allocations for DFS)
2. InMemory: same behaviour as before (e.g. RandomPathSearcher)
3. Persistent: similar to InMemory but writes nodes to ptree.db
     and tracks information such as branch type, termination
     type or source location (asm) in nodes. Enabled with
     -write-ptree

ptree.db files can be analysed/plotted with the new "klee-ptree"
tool.
@251
SearcherTest: remove redundant root init, fix branch type
b8c6427
@ccadar ccadar force-pushed the ptree branch 4 times, most recently from 59fb493 to 9bbc81e Compare December 12, 2023 23:12
@codecov
Copy link

codecov bot commented Dec 12, 2023 •
edited
Loading

Codecov Report

Merging #1674 (fe2dbd5) into master (fc83f06) will decrease coverage by 0.45%.
The diff coverage is 57.01%.

Additional details and impacted files 
@@            Coverage Diff             @@
##           master    #1674      +/-   ##
==========================================
- Coverage   70.48%   70.04%   -0.45%     
==========================================
  Files         154      161       +7     
  Lines       18870    19313     +443     
  Branches     4424     4610     +186     
==========================================
+ Hits        13301    13528     +227     
- Misses       3654     3753      +99     
- Partials     1915     2032     +117
Files Coverage Δ
lib/Core/ExecutionState.h 84.00% <ø> (ø)
lib/Core/Executor.h 77.27% <ø> (ø)
lib/Core/Searcher.h 100.00% <ø> (ø)
lib/Core/SpecialFunctionHandler.cpp 73.55% <100.00%> (-0.09%) ⬇️
lib/Core/UserSearcher.cpp 88.67% <100.00%> (+0.67%) ⬆️
tools/klee-exec-tree/DFSVisitor.h 100.00% <100.00%> (ø)
tools/klee-exec-tree/Tree.h 100.00% <100.00%> (ø)
tools/klee/main.cpp 64.72% <ø> (ø)
lib/Core/ExecutionTree.h 96.15% <96.15%> (ø)
tools/klee-exec-tree/DFSVisitor.cpp 77.27% <77.27%> (ø)
... and 7 more

... and 2 files with indirect coverage changes

@ccadar ccadar mentioned this pull request Dec 13, 2023
Closed
8 tasks
@251
Copy link
Contributor

251 commented Dec 13, 2023

@ccadar This additional commit e.g. breaks klee-control, removes history of several files and hence breaks git blame, other more important PRs need to be rebased (again!), and the documentation needs to be fixed either. This is exactly what I was afraid of would happen. I'd propose to reopen and merge the old PR and rebase that one on top of the older PRs after merging those.

@ccadar
Copy link
Contributor Author

ccadar commented Dec 13, 2023

@251 let me know what's wrong with klee-control (we also need tests for it!).
I'm not sure I understand your other point or how else one would do the rename.
Happy to solve the various issues together.

@251
Copy link
Contributor

251 commented Dec 13, 2023

what's wrong with klee-control

You've renamed dumpPTree - the variable that klee-control uses:

klee/scripts/klee-control

Line 80 in fc83f06

execCmd(pid, "p dumpPTree = 1", opts)

how else one would do the rename

You've wiped the history of e.g ExecutionTree.h by probably not using git mv.

@ccadar ccadar mentioned this pull request Dec 14, 2023
Merged
8 tasks
@ccadar
Copy link
Contributor Author

ccadar commented Dec 14, 2023

The history wipe, if this is really what happens, is unexpected. Strangely, here's what I see:

$ git status
...
Changes to be committed:
  (use "git reset HEAD <file>..." to unstage)

...
	renamed:    lib/Core/PTree.h -> lib/Core/ExecutionTree.h
...

But then:

$ git commit
...
# Changes to be committed:
...
#       new file:   lib/Core/ExecutionTree.h
...
#       deleted:    lib/Core/PTree.h
...

Thoughts? I guess the file renames need to happen in a separate commit, to be on the safe side.

@ccadar
Copy link
Contributor Author

ccadar commented Dec 14, 2023

OK, I've done the renames separately in #1676 -- that shows more clearly what happens and indicates that history was likely fine in this PR too. Closing this one in favour of #1676

@ccadar ccadar closed this Dec 14, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ccadar @251