Skip to content

Commit

Permalink
Implement new AST pattern-matching library (#940)
Browse files Browse the repository at this point in the history
This PR implements a new library to improve the way that we write code
to deconstruct and examine sub-terms of large, nested AST patterns. For
example, consider
[`getLeftHandSide`](https://github.com/runtimeverification/llvm-backend/blob/83a5b3015ac8816076573d3c8ac266b448b78130/lib/ast/AST.cpp#L1379-L1496).
This function is around 120 lines of code _without explanatory
comments_, and at one point closes no fewer than 10 nested scopes at
once.

Reading, writing and reviewing code of this kind is difficult, tedious
and prone to bugs; @Scott-Guest did a good job of untangling the intent
of these functions previously, but it's not ideal to be doing a lot of
that kind of forensics. There is a sufficient quantity of code in the
backend that does this kind of decomposition that I think it's worth
finding a more reusable solution.[^1]

My proposed solution is to implement a template metaprogramming library
that defines a small DSL modelling similar patterns to Scott's
explanatory comments. For example, with a bit of setup, the comment:
```c++
// lhs(\rewrites(\and(\equals(_, _), X), _)) = [X]
```
becomes the following valid C++ code:
```c++
map(rewrites(and_(equals_(any, any), X), any), getSingleton)
```
which matches the structure of the explanation precisely, rather than
losing the intent of the code behind a pile of conditional branches and
imperative code.

By composing several of these patterns together, we are able to shrink
functions like `getLeftHandSide` down to a tiny fraction of their
original size, while also improving their readability and
correctness[^2] and preserving error-checking behaviour.[^3]

The changes in this PR are as follows:
* Extract the functions in `AST.cpp` that perform pattern-matching
functions to a new, separate translation unit.
* Implement the pattern-matching DSL in `pattern_matching.h`; this
implementation is well-documented internally and I hope will be easy to
review as a standalone feature. Additionally, unit tests for this
library are added.
* Refactor the AST pattern-matching code to use the new abstractions.

[^1]: Additionally, `clang-tidy` complains heavily about these functions
- simplifying them will allow more code quality and static analysis
checks to be enabled.
[^2]: I found two cases where the specification comments didn't quite
match the intent of the code. This is - to be clear - a **very good
thing** for the quality of those comments given the complexity of the
code.
[^3]: One function maps a set of "good" patterns to `nullptr` and errors
for "bad" patterns; we can express that behaviour using the new
abstraction.

---------

Co-authored-by: Scott Guest <scott.guest@runtimeverification.com>
  • Loading branch information
Baltoli and Scott-Guest authored Jan 10, 2024
1 parent dbb5820 commit 276afab
Show file tree
Hide file tree
Showing 8 changed files with 817 additions and 334 deletions.
2 changes: 2 additions & 0 deletions include/kllvm/ast/AST.h
Original file line number Diff line number Diff line change
Expand Up @@ -967,6 +967,8 @@ void readMultimap(
std::string const &, KORESymbolDeclaration *,
std::map<std::string, std::set<std::string>> &, std::string const &);

sptr<KOREPattern> stripRawTerm(sptr<KOREPattern> const &term);

template <typename Elem, typename Hash, typename Equal>
std::unordered_map<Elem *, std::unordered_set<Elem *, Hash, Equal>, Hash, Equal>
transitiveClosure(std::unordered_map<
Expand Down
Loading

0 comments on commit 276afab

Please sign in to comment.