From bbd81b7a870cd977e4abf7e38f343f5f0962fb75 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Sun, 1 Aug 2021 15:34:06 +0100 Subject: [PATCH 1/3] Add FEATURES.md This adds FEATURES.md to gather together new features and research ideas that otherwise would fill the issues/PR backlog. Also provide a simple reference point for finding feature ideas or projects. --- FEATURES.md | 72 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 72 insertions(+) create mode 100644 FEATURES.md diff --git a/FEATURES.md b/FEATURES.md new file mode 100644 index 00000000000..9c77114340b --- /dev/null +++ b/FEATURES.md @@ -0,0 +1,72 @@ +# CBMC Feature Ideas + +The following are features that would be good to add to CBMC. They are +listed here to gather information on them and also as a starting point +for contributors who are interested in undertaking a more comprehensive +project. + +## Refinement-Based Slicing + +**Task**: Implement refinement-based slicing to improve the slicing +of CBMC. + +**Background**: +Some patches have been considered for this, but there is not yet +evidence of performance improvement. See +https://github.com/diffblue/cbmc/issues/28 + +## Refinement-based reduction of partial order constraints + +**Task**: Implement refinement-based reduction of partial order +constraints. + +**Background**: +Some patches have been considered for this, but there needs to also be +work on the performance. See +https://github.com/diffblue/cbmc/issues/29 + + +## Advanced goto-diff + +**Task**: Improve the goto-diff utility to have both syntactic and +semantic diff options for goto programs. + +**Background**: The current `goto-diff` program performs only syntatic +diff of goto programs. Extensions to also consider semantic differences +would be desirable. It would be nice to include: +* deltacheck's change impact analysis +* cemc equivalence checker + +See also https://github.com/diffblue/cbmc/issues/40 + +## Function Summaries + +**Task**: Create function summaries that simplify analysis. The main +goals of the function summaries are: +* context insensitivity (there is one summary applicable in any +context the function is called from) +* transitive closure (effects of all callees are captured in summaries +of the root caller function) +* generalised interface (suitable for many different concrete +summary-computing algorithms) +* language independent (should work for Java, C, C++, ...) + +This also has links to other projects (albeit some may be out of date +at this stage): +* test_gen (our summaries should fit to needs of this tests generation +task) +* 2ls (their summaries should also be expressible in our summaries) +* path-symex (summaries must also be usable for path-based symbolic +execution) + +There are also complexities related to over/under-approximation +for the function summaries. For more details see +https://github.com/diffblue/cbmc/issues/218 + + +## --cover array + +**Task**: Extend the `--cover` option to add coverage goals for each +possible entry of fixed size arrays. For more details see +https://github.com/diffblue/cbmc/issues/265 + From 4054ce5b6c092deca9752809986690b069dde9c1 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Sun, 29 Aug 2021 12:11:50 +0100 Subject: [PATCH 2/3] Combine distinct files into one This removes the two files for FEATURES and MINI_PROJECTS and combines them into a single FEATURE_IDEAS file. --- FEATURES.md | 72 -------------------------- MINI-PROJECTS.md => FEATURE_IDEAS.md | 76 ++++++++++++++++++++++++++++ 2 files changed, 76 insertions(+), 72 deletions(-) delete mode 100644 FEATURES.md rename MINI-PROJECTS.md => FEATURE_IDEAS.md (86%) diff --git a/FEATURES.md b/FEATURES.md deleted file mode 100644 index 9c77114340b..00000000000 --- a/FEATURES.md +++ /dev/null @@ -1,72 +0,0 @@ -# CBMC Feature Ideas - -The following are features that would be good to add to CBMC. They are -listed here to gather information on them and also as a starting point -for contributors who are interested in undertaking a more comprehensive -project. - -## Refinement-Based Slicing - -**Task**: Implement refinement-based slicing to improve the slicing -of CBMC. - -**Background**: -Some patches have been considered for this, but there is not yet -evidence of performance improvement. See -https://github.com/diffblue/cbmc/issues/28 - -## Refinement-based reduction of partial order constraints - -**Task**: Implement refinement-based reduction of partial order -constraints. - -**Background**: -Some patches have been considered for this, but there needs to also be -work on the performance. See -https://github.com/diffblue/cbmc/issues/29 - - -## Advanced goto-diff - -**Task**: Improve the goto-diff utility to have both syntactic and -semantic diff options for goto programs. - -**Background**: The current `goto-diff` program performs only syntatic -diff of goto programs. Extensions to also consider semantic differences -would be desirable. It would be nice to include: -* deltacheck's change impact analysis -* cemc equivalence checker - -See also https://github.com/diffblue/cbmc/issues/40 - -## Function Summaries - -**Task**: Create function summaries that simplify analysis. The main -goals of the function summaries are: -* context insensitivity (there is one summary applicable in any -context the function is called from) -* transitive closure (effects of all callees are captured in summaries -of the root caller function) -* generalised interface (suitable for many different concrete -summary-computing algorithms) -* language independent (should work for Java, C, C++, ...) - -This also has links to other projects (albeit some may be out of date -at this stage): -* test_gen (our summaries should fit to needs of this tests generation -task) -* 2ls (their summaries should also be expressible in our summaries) -* path-symex (summaries must also be usable for path-based symbolic -execution) - -There are also complexities related to over/under-approximation -for the function summaries. For more details see -https://github.com/diffblue/cbmc/issues/218 - - -## --cover array - -**Task**: Extend the `--cover` option to add coverage goals for each -possible entry of fixed size arrays. For more details see -https://github.com/diffblue/cbmc/issues/265 - diff --git a/MINI-PROJECTS.md b/FEATURE_IDEAS.md similarity index 86% rename from MINI-PROJECTS.md rename to FEATURE_IDEAS.md index 136f27f718e..118892ef3ce 100644 --- a/MINI-PROJECTS.md +++ b/FEATURE_IDEAS.md @@ -1,3 +1,79 @@ +This file contains various features and project ideas for CBMC. Below +this are the larger feature ideas. Smaller mini project ideas are +further down. + +# CBMC Feature and Project Ideas + +The following are features that would be good to add to CBMC. They are +listed here to gather information on them and also as a starting point +for contributors who are interested in undertaking a more comprehensive +project. + +## Refinement-Based Slicing + +**Task**: Implement refinement-based slicing to improve the slicing +of CBMC. + +**Background**: +Some patches have been considered for this, but there is not yet +evidence of performance improvement. See +https://github.com/diffblue/cbmc/issues/28 + +## Refinement-based reduction of partial order constraints + +**Task**: Implement refinement-based reduction of partial order +constraints. + +**Background**: +Some patches have been considered for this, but there needs to also be +work on the performance. See +https://github.com/diffblue/cbmc/issues/29 + + +## Advanced goto-diff + +**Task**: Improve the goto-diff utility to have both syntactic and +semantic diff options for goto programs. + +**Background**: The current `goto-diff` program performs only syntatic +diff of goto programs. Extensions to also consider semantic differences +would be desirable. It would be nice to include: +* deltacheck's change impact analysis +* cemc equivalence checker + +See also https://github.com/diffblue/cbmc/issues/40 + +## Function Summaries + +**Task**: Create function summaries that simplify analysis. The main +goals of the function summaries are: +* context insensitivity (there is one summary applicable in any +context the function is called from) +* transitive closure (effects of all callees are captured in summaries +of the root caller function) +* generalised interface (suitable for many different concrete +summary-computing algorithms) +* language independent (should work for Java, C, C++, ...) + +This also has links to other projects (albeit some may be out of date +at this stage): +* test_gen (our summaries should fit to needs of this tests generation +task) +* 2ls (their summaries should also be expressible in our summaries) +* path-symex (summaries must also be usable for path-based symbolic +execution) + +There are also complexities related to over/under-approximation +for the function summaries. For more details see +https://github.com/diffblue/cbmc/issues/218 + + +## --cover array + +**Task**: Extend the `--cover` option to add coverage goals for each +possible entry of fixed size arrays. For more details see +https://github.com/diffblue/cbmc/issues/265 + # CBMC Mini Project Ideas The following projects are short, focussed features that give new CBMC From b8487d45978535b80c052232f2c47bc0b895c416 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Sun, 29 Aug 2021 12:44:32 +0100 Subject: [PATCH 3/3] Add in another feature idea --- FEATURE_IDEAS.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/FEATURE_IDEAS.md b/FEATURE_IDEAS.md index 118892ef3ce..8e2701f2a15 100644 --- a/FEATURE_IDEAS.md +++ b/FEATURE_IDEAS.md @@ -74,6 +74,24 @@ https://github.com/diffblue/cbmc/issues/218 possible entry of fixed size arrays. For more details see https://github.com/diffblue/cbmc/issues/265 + +## Connecting Producers and Consumers of Knowledge about Termination + +There is very limited knowledge about loop termination conditions +and this could be improved. For example, the slicing could be +improved with knoweldge regarding loop termination so that +irrelevant loops can be more effectively sliced. Similarly, in +goto-analyze assertions can only be false if reachable, adding +termination can give crude reachability analysis. + +The overall approach could be to have for each loop and/or +function information: `TERMINATE`, `NON_TERMINATE`, or +`UNKNOWN_TERMINATION`. + +Further details on possible implementations and discussion +can be found here +https://github.com/diffblue/cbmc/issues/618 + # CBMC Mini Project Ideas The following projects are short, focussed features that give new CBMC