Mini projects list update #4119
Conversation
|
Note to reviewers: While porting this list, I found a reference to a lot of names, or WIP notes that I couldn't judge the validity of. These are marked as Also while porting the list, I removed references to a couple of projects like the DALVIK one, judging that it's no longer relevant. If someone thinks otherwise, I'm happy to add it back. |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: df9625a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100110943
|
@tautschnig Could I please get a review on this and get it merged if it looks good? |
There was a problem hiding this comment.
I think this should get a thorough review from @chrisr-diffblue @peterschrammel and whoever else has a good overview of what the status of various bits of work is.
MINI-PROJECTS.md
Outdated
|
|
||
| `goto-instrument` features an instrumentation to track cases of use-before-define, i.e. | ||
| reading of uninitialised variables. At present, the analysis does not take into account | ||
| aliasing information. As such, the following code will yield a spurious counterexample: |
There was a problem hiding this comment.
I actually think that instrumentation could do with some initial work just to make sure it works at all :-)
MINI-PROJECTS.md
Outdated
| CBMC allows to choose among a selection of SMT solvers to use as solving back end. As these | ||
| tools evolve, CBMC's code for running them may need a fresh look from time to time. After | ||
| a first round of manual experiments, these tests should become part of the routine build | ||
| process on `dkr-build`. (Michael Tautschnig knows how to do this.) |
There was a problem hiding this comment.
Today we've got proper CI, no need to resort do dkr-build.
| support for dynamic analysis, calls to external functions and possibly even mixed concrete | ||
| and symbolic execution. It would also be good to be able to interpret traces found by BMC | ||
| to catch mismatches / bugs between the logical model and the bit blasting models. This | ||
| would also be useful for more advanced CEGAR like techniques (also see below). |
There was a problem hiding this comment.
I have no idea what the actual state of the interpreter is today.
There was a problem hiding this comment.
I'd propose a project to implement an interpreter using goto-symex.
There was a problem hiding this comment.
Using the abstract interpreter would also be possible.
MINI-PROJECTS.md
Outdated
| * Use path exploration as the witness generation part of an ACDL process. | ||
| * Perform precondition inference, possibly using ACDL. | ||
|
|
||
| See the work Björn and Alex have done with path-symex. (?) |
There was a problem hiding this comment.
We do now have a single-path symex mode, but the ideas above might still be relevant.
There was a problem hiding this comment.
Unclear what the points above mean, but there is certainly work to be done around the single-path symex, including robustness, efficiency and search strategies.
There was a problem hiding this comment.
I believe the original suggestion (I have a feeling I wrote a number of these) was using ACDL-like reasoning to "learn" invariants from failed symex runs (using UNSAT cores and the like) and add these in to the process, giving something like IMPACT but without the covering relations.
|
|
||
| ## Interact with GDB | ||
|
|
||
| GDB implements a client-server protocol with a GDB instance acting as a server and the |
There was a problem hiding this comment.
There is an open PR on that one (#3983).
There was a problem hiding this comment.
I don't think that covers all the points below.
|
|
||
| ### Error Explanation | ||
|
|
||
| Re-implement the algorithm described in [this paper](http://www.kroening.com/papers/STTT-error-explanation-2005.pdf) |
There was a problem hiding this comment.
This is partly implemented in the fault localizer.
| support for dynamic analysis, calls to external functions and possibly even mixed concrete | ||
| and symbolic execution. It would also be good to be able to interpret traces found by BMC | ||
| to catch mismatches / bugs between the logical model and the bit blasting models. This | ||
| would also be useful for more advanced CEGAR like techniques (also see below). |
There was a problem hiding this comment.
I'd propose a project to implement an interpreter using goto-symex.
MINI-PROJECTS.md
Outdated
| of the Java programming language semantics, such as the Java Memory Model. This will include | ||
| adding models for a subset of the Java concurrency packages in the Java Runtime Library. | ||
|
|
||
| Jade Alglave may have some additional input on this. (?) |
There was a problem hiding this comment.
Cesar and Kurt have done work on that.
MINI-PROJECTS.md
Outdated
|
|
||
| Also look at Google's Native Client, and talk to Matt, who has tried Valgrind. | ||
|
|
||
| Furthermore, talk to Michael, who has got a student who made some progress on this. |
|
@NlightNFotis Is this still going to be worked on and maybe merged? |
| support for dynamic analysis, calls to external functions and possibly even mixed concrete | ||
| and symbolic execution. It would also be good to be able to interpret traces found by BMC | ||
| to catch mismatches / bugs between the logical model and the bit blasting models. This | ||
| would also be useful for more advanced CEGAR like techniques (also see below). |
There was a problem hiding this comment.
Using the abstract interpreter would also be possible.
MINI-PROJECTS.md
Outdated
| * Use path exploration as the witness generation part of an ACDL process. | ||
| * Perform precondition inference, possibly using ACDL. | ||
|
|
||
| See the work Björn and Alex have done with path-symex. (?) |
There was a problem hiding this comment.
I believe the original suggestion (I have a feeling I wrote a number of these) was using ACDL-like reasoning to "learn" invariants from failed symex runs (using UNSAT cores and the like) and add these in to the process, giving something like IMPACT but without the covering relations.
MINI-PROJECTS.md
Outdated
| GCC has a set of 'torture tests' which are intended to stress test and find bugs in their C parser | ||
| and front-end. It would be good to run these through goto-cc / add them to the nightly testing and | ||
| fix any bugs that arise. (Possible overlap with “Front-End Testing” above.). The same is probably | ||
| also true for CSmith and other compiler fuzzing tools. |
There was a problem hiding this comment.
@tautschnig has implemented the CSmith part.
|
@TGWDB Yes, I intend to chase it up and clean this up soon (as soon as I get some time). @martin-cs Thanks for the suggestions and the comments, will incorporate them when I find some time 👍🏻 |
b2c947d to
7c16e7e
Compare
|
Hi @peterschrammel and @tautschnig, could you take a look at this at your latest convenience? I've implemented most of the comments, and changed the file a bit to conform to markdown listing standards. Other than this, it looks good to go to me, what do you think? |
Codecov Report
@@ Coverage Diff @@
## develop #4119 +/- ##
========================================
Coverage 74.95% 74.95%
========================================
Files 1450 1450
Lines 158274 158274
========================================
Hits 118632 118632
Misses 39642 39642 Continue to review full report at Codecov.
|
Port the list of projects available at https://web.archive.org/web/20150530010030/http://www.cprover.org/wiki/doku.php?id=starter_projects to the new markdown file inside the repo.
7c16e7e to
c07c76f
Compare
This fixes #4111. Port of a list of starter projects from the old CPROVER wiki
into the in-repo file tracking them.