Codecov Report

Merging #1349 (b8c6427) into master (fc83f06) will decrease coverage by 0.44%.
The diff coverage is 56.04%.

@@            Coverage Diff             @@
##           master    #1349      +/-   ##
==========================================
- Coverage   70.48%   70.04%   -0.44%     
==========================================
  Files         154      161       +7     
  Lines       18870    19312     +442     
  Branches     4424     4610     +186     
==========================================
+ Hits        13301    13528     +227     
- Misses       3654     3752      +98     
- Partials     1915     2032     +117     

Any ideas what's wrong with the MacOS build?

@251 I believe this PR is now outdated and we can close it? (#1348 was merged)

It's currently outdated but I'd update it after the termination stuff is merged (e.g. #1465).

@ccadar @MartinNowack Ready for review. Slowly we get the puzzle pieces together...

Thanks, Frank! An exciting addition, I'll try to take a look soon.

@251 I took a look, and left a few small comments. In addition to those, I think it would be really useful to add some documentation to the webpage.

Let's merge this soon, it's a great addition!

@ccadar Done.

@251 thanks again for this useful addition. It looks fine, and it's quite modular, so let's merge it!
But can you first add some documentation to the website? The comments you have at the beginning of this PR and in the commit messages (as well as the example at #951 (comment)) would be enough.

In addition, I would like to take this opportunity to propose renaming PTree to ETree, from "Execution Tree", which is the term that we and others are already using in papers to refer to this tree. Furthermore, we use "process" in the documentation in the UNIX sense, so overloading the term like this is particularly confusing. To be clear: I am proposing this for the user-facing options and documentation (e.g., rename write-ptree to write-etree), but if you want to add a refactoring patch changing PTree to ETree in the code, I'd be happy to accept it, as it would be nice to be consistent. Otherwise, we can do that later.

@ccadar

But can you first add some documentation to the website?

klee/klee.github.io#369

Otherwise, we can do that later.

We can do it independently from this PR but it should be consistent everywhere (code, docs, options).

@danielschemmel
Thanks for the comments, I changed the PR accordingly.

Thanks for the documentation, @251 . Can you at least just rename the user-facing options (--write-ptree, ptree.db) here? Seems to be the right time to do it, as this is the PR introducing them. Thanks!

Seems to be the right time to do it, as this is the PR introducing them.

I think that would be rather confusing as we have no such thing as an "etree". I'd propose to keep it for now, choose a proper name (etree, xtree, extree, ...) and than change it consistently everywhere.

So what name do you suggest? I think "execution tree" (with the short form "etree") is the right terminology, as this is what we and others already use in papers. Why introduce users to the concept of ptrees if we will change it anyway? (what we have in the code is a different matter, although I agree we should be consistent and do the rename there too)

So what name do you suggest?

xtree/extree/etree

Why introduce users to the concept of ptrees

There is still time to fix it properly before the next release.

I still think that the best time to decide on the terminology is when we introduce it. But I understand if you don't want to spend more time on this PR, and I offer to add a commit to this branch with the renaming. Let's decide on a name: I kind of like your suggestion for XTree / xtree, should we go with that? (But I'm also happy with ETree/etree, or anything other short form for "execution tree".)

I would like to suggest just using the full name ExecutionTree with full arguments like -write-execution-tree. There is not that much to gain by saving a few keystrokes.

Those are all great suggestions for a follow-up PR.

@251 It should be as part of the same PR, but I offered to write that patch.
I think @danielschemmel's suggestion is reasonable, but perhaps I would go with ExecutionTree, --write-exec-tree, and exec_tree.db. Sounds good?

Again, I'd do it but not as part of this PR. It makes no sense to blow this already large PR up with some unimportant naming stuff. You cannot just rename a flag and a file, you'd also have to change all the error messages, the command line switches/categories, the code comments in several tools, the documentation... It is completely unrelated and no one cared about naming for 15 years - or even the last 3 years since this PR is open.

This is the first time we are introducing this to users; this is why in my opinion the key thing is the user-facing terminology, and this is all I asked for. But I agree having everything in sync is desirable. I also don't think renaming will take that long, but let me give it a try first :)

I would like to break the tie on this. In general I see good arguments from all sides, so thank you for this fruitful discussion.

Here are my two cents on this: The current discussion is around user-facing changes and they should be addressed eventually.

But, this PR is quite old - more than 3 years and we should have managed to merge this one (quite some time) earlier. This PR is quite big as it is. Reviewing it again is quite time consuming. There have been already many change requests for this PR and it has evolved over time.

In general, PRs are changing the development branch of KLEE and it's not part of a release yet. Therefore, I assume that people should be more ok with inconsistencies and breakages in a development branch.

For those reasons and not to postpone further PRs that much longer, I would like to merge this as is.
It has sufficient reviews and was tested multiple times and runs internally.

We can provide a more consistent experience for the end user as a follow-up PR.

What are your thoughts on this?

And I forgot the main important point: it provides some nice features 😄

@MartinNowack I agree with this. But since I have actually implemented the change, so I'll just push it shortly, most likely tonight.

Extended with the rename in #1674