HomePhabricator

[analyzer] exploded-graph-rewriter: Implement a --diff mode.

Authored by dergachev.a on Jun 19 2019, 4:33 PM.

Description

[analyzer] exploded-graph-rewriter: Implement a --diff mode.

In this mode the tool would avoid duplicating the contents of the
program state on every node, replacing them with a diff-like dump
of changes that happened on that node.

This is useful because most of the time we only interested in whether
the effect of the statement was modeled correctly. A diffed graph would
also be much faster to load and navigate, being much smaller than
the original graph.

The diffs are computed "semantically" as opposed to plain text diffs.
I.e., the diff algorithm is hand-crafted separately for every state trait,
taking the underlying data structures into account. This is especially nice
for Environment because textual diffs would have been terrible.
On the other hand, it requires some boilerplate to implement.

Differential Revision: https://reviews.llvm.org/D62761

llvm-svn: 363898