Address review comments on libcprover-cpp/goto-bmc integration ADR.

Author: NlightNFotis

doc/ADR/cpp_api_modularisation.md

@@ -1,41 +1,51 @@
-\page cpp-api-and-modularisation Libcprover-cpp and Modularisation
+\page cpp-api-and-modularisation libcprover-cpp and Modularisation
 
 **Date**: 22 Jun 2023
 **Updated**: 22 Jun 2023
 **Author**: Fotis Koutoulakis, [email protected]
 **Domain**: Architecture, API
 **Description**: This document outlines our thinking about the rearchitecting of
-    CBMC using the C++ API (`Libcprover-cpp`) as the central module and the
+    CBMC using the C++ API (`libcprover-cpp`) as the central module and the
     transitioning of other tools to use that as a basis.
 
 ## Motivation && Current State of Affairs
 
-CProver is a collection of tools fitting various program analysis needs. It
+CProver is a collection of tools fitting various program analysis needs. CProver
 has been the product of the evolution of the codebase of the model-checking
-tool for C (`CBMC`), after it has been adopted with various front-ends/back-ends
-and various auxilliary tools.
+tool for C (`CBMC`). Since then CProver has been adopted with various
+front-ends/back-ends and auxilliary tools.
 
 During this time, the repository has grown organically, using some guidelines
 for development that were based on tradition and intuition rather than some
-tight development guide. This development model has been successful for most
+agreed architectural approach. This development model has been successful for most
 of CProver's life, based on its nature as a hybrid industrial/academic and
-experimental/applied tool. However, it has had the side-effect of accruing
-some code duplication and technical debt. It has also made the codebase harder
-to understand/develop and integrate with, especially for someone who is new
-to the codebase.
+experimental/applied tool. However, this has had the side-effect of accruing
+some code duplication and technical debt. Consequently, the codebase is complex
+and difficult to understand and develop for. This is a large barrier to new
+developers, new features, and also improving and fixing the existing CProver
+tools.
 
 The above concerns have generated discussions about the breaking down of
 CProver into modules, with cleaner interfaces and tighter boundary control
 between them, making the code easier to integrate in other projects (by making
 the various component modules easier to combine and reuse) and making the
 codebase easier to understand and maintain.
 
+The desire to separate functionality into different functional units
+would also remove duplication and bloat, and prevent issues with the
+same flag behaving in different ways across CProver tools.
+
 ## The Plan Going Forward
 
 Given the above outline, we have reached a point where we are strongly motivated
-to take action to better componentise and modularise CProver.
-
-It's also an opportune time for us, given the existence of `Libcprover-cpp`
+to take action to better componentise and modularise CProver. What we mean by
+"better componentise and modularise" is that right now, even though there
+exists some structure between different CBMC components (at the class level
+or at the code source file level), the different components aren't cleanly
+separated in terms of boundaries/concerns, which hinders their reusability
+or understandability.
+
+It is also an opportune time for us, given the existence of `libcprover-cpp`
 the C++ API that we built to support interfacing with Rust (for now - other
 languages may be coming in the future): we can use this as the basis of
 development for an API exposing the interfaces of the various other modules
@@ -45,7 +55,7 @@ an incremental basis.
 Of course, this is a project that is massive in scope, potentially being
 exposed to further scope creep. We acknowledge that any effort to do what
 we have discussed already is going to be a multi-year effort from our end,
-and that we will need community alignment to achieve the outcome we're
+and that we will need community alignment to achieve the outcome we are
 looking for.
 
 This is why we are looking into testing the approach on a smaller component
@@ -66,38 +76,44 @@ The aim of the PR was not only to allow for the tool with the narrower-scope
 to come to life, but also to see if we could expose just enough of the
 process to the C++ API and use that as the basis of the new tool.
 
-This whole process has been very informational: we found out that not only
+This whole process has been very informative: we found out that not only
 we *can* use the C++ API in that capacity, but also that extending the API
 as and when we need to, and doing the various refactorings to the other tools
 on a Just-In-Time basis is viable.
 
 There have been, however, some limitations:
 
 * The C++ API is still nascent, and as such its support for various workflows
-  is just not present (at first). We can (and do) build things fast, as and
-  when we need them - but it's nowhere near feature complete to provide for
+  is just not present (yet). We can (and do) build things fast, as and
+  when we need them - but it is nowhere near feature complete to provide for
   all of a user's workflows at the time of this writing.
 
+* Still on the C++ API, its usage as the implementation basis for the new
+  tool `goto-bmc` means that the code-structure and patterns in `goto-bmc`
+  are going to differ from other existing tools in the CProver-suite.
+
 * CProver tools have primarily been based on textual output to report on the
   results of their function (be it analysis, or transformations, etc). This
-  hasn't been a problem up until this point (with the caveat that occassionally
+  has not been a problem up until this point (with the caveat that occasionally
   requests for support of new textual formats come up and adding support for
   those has become a laborious process).
 
-  There's a need however for the separation of concerns between the production
+  There is a need however for the separation of concerns between the production
   of the results by the analysis engine and the presentation layer for those.
 
-We're working towards addressing these teething problems, but while we're
+We are working towards addressing these teething problems, but while we are
 still operating on those, we have to accept some compromises in the architecture
-of the code while we're iterating or stabilising several of the new or
+of the code while we are iterating or stabilising several of the new or
 refactored parts.
 
 Be advised that some constructs may pop up in some limited locations
-in the codebase that may appear questionable. We're only asking for
-some patience while we're working out the best way to refactor them into
+in the codebase that may appear questionable. We are only asking for
+some patience while we are working out the best way to refactor them into
 an architecture that is more cohesive with the long term vision for the
 platform.
 
 From our end, we will do our best to avoid any spillover effects to
 other areas of the codebase, and to avoid introducing any behavioural
-regressions while we're implementing the above plan.
+regressions while we are implementing the above plan. Any constructs
+that may feature "questionable" changes to parts will be marked as such
+and be followed with an explanation as to why the decision was made.