Example-based Synthesis of Static Analysis Rules

We are given a set of violating or buggy code examples $\mathscr{V}=\{V_{1},\cdots,V_{m}\}$ and a set of conforming or non-buggy code examples $\mathscr{C}=\{C_{1},\cdots,C_{n}\}$, for a single code quality issue. The problem is to synthesize a rule $R$ from a subset of examples such that $R(V_{i})$ = True and $R(C_{j})$ = False, for all $i$ and $j$ in the held-out test set. We consider code examples at the granularity of a method. This offers sufficient code context to precisely capture a wide range of code quality issues (Tufano et al., 2018; Sobreira et al., 2018), while at the same time being simple enough to facilitate efficient rule synthesis.

The corpus of code changes made by developers is a natural source of positive and negative examples. In such a corpus, common code quality issues will have multiple code changes that fix those issues. It is possible to obtain examples for single code quality issues in an automated manner by clustering code changes (Kreutzer et al., 2016; Paletov et al., 2018; Bader et al., 2019). Code changes in the input consist of pairs $(B_{i},A_{i})$ where $B_{i}$ is the code-before and $A_{i}$ is the code-after. To synthesize a rule $R$, we consider code-befores as violating examples and code-afters as conforming examples.

A user can also provide additional conforming examples corresponding to variations in correct code that may not be captured by the code changes.

Consider the two code changes shown in Figure 1(a)-(b). The code before the change does not handle the case when the cursor accessing the result set of a database query is empty. Without this check, the app might crash when subsequent operations are called on the cursor (e.g., getString call on line $8$ in Figure 1(a). In these code changes, the developer adds this check by handling the case when Cursor.moveToFirst() returns False.

As mentioned earlier, RhoSynth first synthesizes the precondition from buggy code examples and then synthesizes the postcondition from non-buggy code examples.

These variations are not part of the initial examples. When we run the synthesized rule on code corpus, we encounter examples such as the ones shown in Figure 3(a)-(b) that check the cursor using these code variations. Note these examples are not accompanied by buggy code. We propose rule refinement that uses these additional non-buggy examples to improve the rule. Specifically, we re-synthesize the postcondition by constructing an UAPDG $\mathscr{A}_{\textit{pc}}$, in a way similar to the UAPDG construction in rule precondition synthesis. However, it turns out that $\mathscr{A}_{\textit{pc}}$ is too general and accepts even the buggy examples. We use this as a forcing function to partition the non-buggy examples and synthesize a conjunctive postcondition for each partition.

Figure 4(a)-(c) illustrate the UAPDGs for the synthesized precondition and the two disjuncts in the postcondition. Figure 4(d) provides the exact rule, expressed as a logical formula. Informally, the synthesized $R$ satisfies all code examples that call Cursor.moveToFirst such that they do not check the value returned by this call, nor call Cursor.isAfterLast or Cursor. getCount. When we run this rule again on the code examples, it correctly accepts all the buggy examples and rejects all non-buggy examples, including the additional examples that were used for rule refinement.

We represent code examples at a method granularity using PDGs (Ferrante et al., 1987). PDG is a labeled graph that captures all data and control dependencies in a program. Nodes in the PDG are classified as data nodes and action nodes. Data nodes are, optionally, labeled with the data types and values for literals, and action nodes are labeled with the operations they correspond to, for e.g., method name for method call nodes, etc. Edges in the PDG correspond to data-flow and control dependencies and are labeled as recv (connects receiver object to a method call node), para_i (connects the $i^{th}$ parameter to the operation), def (connects an action node to the data value it defines), dep (connects an action node to all nodes that are directly control dependent on it) and throw (connects a method call node to a catch node indicating exceptional control flow). See Figure 6 in Appendix B for the PDG of code-after in Figure 1(a).

In this work, we express rules as quantified first-order logic formulas over PDGs (refer to Figure 5 for a detailed syntax of rules). A rule is a formula of the form $\exists\vec{x}.{pre}(\vec{x})\wedge\neg\big{(}\bigvee\exists\vec{y}.post(\vec{x},\vec{y})\big{)}$, where $\vec{x}$ and $\vec{y}$ are a set of quantified variables that range over distinct nodes in a PDG. The precondition $\textit{pre}(\vec{x})$ evaluates to True on buggy code and the postcondition $\textit{post}_{i}(\vec{x},\vec{y})$ evaluates to True on correct code, with appropriate instantiations for $\vec{x}$, $\vec{y}$. Because of the negation before the postcondition, the entire formula evaluates to True on buggy code and False on correct code. Intuitively, the precondition captures code elements of interest in buggy, and possibly correct, code, and the postcondition captures the same in correct code. The elements appear as existentially quantified variables. This is a rich format that can express a wide range of code quality issues.

Formulas $pre(\vec{x})$ and $post_{i}(\vec{x},\vec{y})$ are quantifier-free sub-rules comprising a conjunction of atomic edge predicates $\epsilon(\vec{x})$ that correspond to edges $x_{1}\xrightarrow{e}x_{2}$ in the PDG, and atomic node predicates $\eta(\vec{x})$. $\eta({\vec{x}})$ express various properties at PDG nodes including the node label, data-type, data values for literals, number of parameters for method calls (num-para(x)), declaring class type for static method calls (declaring-type(x)), the set of nodes on which $x$ is transitively control dependent (trans-control-dep(x)) and, finally, whether a method call’s output is/is not ignored (output-ignored(x) and its negation)⁴⁴4Predicate output-ignored(x) is True for a method call when it does not return a value or the returned value has no users, and False otherwise..

Note, we exclude disjunctions in preconditions since a rule with a disjunctive precondition can be expressed as multiple rules without a disjunctive precondition, in the rule syntax. Further, a rule with a precondition comprising a negated code pattern (e.g., $\neg x_{1}\xrightarrow{e}x_{2}$) is expressed using a positive pattern in the rule postcondition, and vice-versa. The rule syntax, while mostly captures first-order logic properties over PDGs, includes some higher-order properties, e.g., transitive control dependence.

Rules are formulas that accept or reject code examples represented as PDGs. From the rule syntax (Figure 5), a rule is expressed using a precondition and a postcondition. Both the precondition and the postcondition can be expressed as a collection of quantified formulas $\mathcal{P}_{Q}=\exists\vec{y}.\varphi(\vec{x},\vec{y})$, where $\varphi$ is a conjunctive subrule defined over free variables $\vec{x}$ and bound variables $\vec{y}$. To represent rules, we need a representation for $\mathcal{P}_{Q}$. We arrive at a representation for $\mathcal{P}_{Q}$, from a PDG representation, in two steps. We first introduce Valuated PDGs (VPDGs; also, sometimes, referred as valuated examples) that are PDGs extended with variables. VPDGs capture a single PDG that is accepted by $\mathcal{P}_{Q}$. We then introduce Unified Annotated PDGs (UAPDGs) that accept sets of VPDGs and represent the quantified formula $\mathcal{P}_{Q}$.

Let Var be a set of variables. A Valuated PDG is a PDG with a subset of its nodes mapped to distinct variables in Var. Informally, a Valuated PDG is a PDG with a valuation for variables.

As mentioned above, a Unified Annotated PDG is defined over a set of free variables $\textit{Var}_{f}\subseteq\textit{Var}$ and bound variables $\textit{Var}_{b}\subseteq\textit{Var}$, and represents an existentially quantified conjunctive formula over PDGs of the form $\exists\textit{Var}_{b}.\varphi(\textit{Var}_{f},\textit{Var}_{b})$. Note that $\varphi$ is a conjunctive subrule that is defined over a set of node predicates ($\eta(\vec{x})$ in Figure 5). These node predicates are expressed using lattices annotating different nodes in a UAPDG (see Section 5 for details). Formally,

Note that bound variables $\textit{Var}_{b}$ can be permuted in the map $\textit{M}_{b}$ without affecting the semantics of a UAPDG. On the other hand, variables $\textit{Var}_{f}$ cannot be permuted or renamed in the map $\textit{M}_{f}$, since these variables are free (they are bound to an outer existential quantifier in the rule $R$). We call nodes in $\textit{M}_{f}$, mapped to variables in $\textit{Var}_{f}$, frozen since the variables mapped to these nodes are fixed for a given UAPDG.

For constructing a UAPDG from a set of VPDGs, we need to first identify corresponding nodes in VPDGs and then unify the node predicates at the corresponding nodes. We identify corresponding nodes through graph alignment using ILP (see Section 4.1) and the unification of node predicates is performed by generalization over the lattice. We describe the use of UAPDG representation to synthesize rule preconditions and postconditions in Section 4.

Graph alignment amongst the violating examples or conforming examples is one of the key steps in synthesizing the rule precondition or postcondition respectively. Since both the precondition and postcondition formulas are existentially quantified, the synthesis problem is NP-hard (Haussler, 1989). Its hardness stems from different choices available for mapping existential variables to nodes in the example graphs. Alternatively, the synthesis problem can be seen as a search over graph alignments such that aligned nodes in different examples are mapped to the same existential variable. Note that different graph alignments will result in different synthesized formulas. Given multiple graphs, we iteratively align two graphs at a time⁵⁵5This is an instance of a “multi-graph matching” problem. This requires optimization techniques beyond ILP, for e.g., alternating optimization (Yan et al., 2013). We did not explore these solutions since pairwise graph alignment worked well for our application.. We frame the problem of choosing a desirable graph alignment for a pair of example graphs as an ILP optimization problem. Since we want to synthesize formulas that precisely capture the code examples, we choose alignments that maximize the number of aligned nodes and edges.

The ILP objective to maximize graph alignment can also be viewed as minimizing the graph edit distance between code examples. Consequently, our reduction to ILP follows the binary linear programming formulation to compute the exact graph edit distance between two graphs (Lerouge et al., 2017). The node and edge substitutions are considered cost $0$ and node/edge additions and deletions are cost $1$ operations. We include a detailed reduction to the ILP optimization problem in Appendix C. Below, we describe some constraints on the ILP optimization that are specific to our application:

• •

  We align action nodes only if they have the same label. So, a method call foo in one example cannot align with method bar in another example. However, data nodes that are,optionally, labeled with their types do not have this restriction. This allows us to align data nodes even when their types do not resolve, or when their types are related in the class hierarchy, for e.g., InputStream and FileInputStream.

• •

  Two data nodes align only if they have at least one aligned incoming or outgoing edge. This restricts alignment of data nodes to only occurrences when they are defined or used by aligned action nodes.

• •

  When synthesizing the postcondition, nodes frozen to the same variables in $\vec{x}$ are constrained to be aligned.

When synthesizing rules from code changes, we use the ILP formulation described in this section to perform a fine-grained graph differencing over PDGs in a code change (similar to the GumTree tree differencing algorithm (Falleri et al., 2014)). Graph differencing labels nodes in the PDGs with change tags: unchanged, deleted or added, depending upon whether the node is present in both code-before and code-after, in only code-before, and in only code-after. Now, while aligning the violating code-before’s for synthesizing the precondition, we require that the node alignment respect these change tags, i.e., nodes are aligned only if their change tags are the same. This constraint helps to focus the synthesized precondition formula on the changed code. This constraint is removed when synthesizing the postcondition. This is because even variables $\vec{x}$ frozen in the conforming examples, by design, may not respect these change tags.

In this section, we describe the procedure getConjunctiveSubRule to synthesize a conjunctive subrule from a given set of valuated examples. It has two main steps. First, UAPDGs that correspond to input valuated examples are iteratively merged pairwise to obtain a UAPDG $\mathscr{A}$. Second, we project $\mathscr{A}$ to nodes present in all input examples to obtain UAPDG $\mathscr{A}_{c}$. Given UAPDGs $\mathscr{A}_{1}$ and $\mathscr{A}_{2}$, $\mathscr{A}_{c}$ obtained by calling merge followed by a project over-approximates $\mathscr{A}_{1}\vee\mathscr{A}_{2}$. This property ensures that $\mathscr{A}_{c}$ obtained after merging a set of input valuated examples is saltisfied by all of them. We first describe the merge operation, followed by project.

Let $\mathscr{A}_{1}=(N_{1},E_{1},Lat_{1},M_{f1},M_{b1})$ and $\mathscr{A}_{2}=(N_{2},E_{2},Lat_{2}$, $M_{f2},M_{b2})$ be two UAPDGs over the same set of free variables $\textit{Var}_{f}$. Let $NM\subseteq N_{1}\times N_{2}$ and $EM\subseteq E_{1}\times E_{2}$ be the node and edge mappings that are obtained from the graph alignment step. We first extend these mappings to relations $\textit{NM}^{\epsilon}\subseteq N_{1}\cup\{\epsilon\}\times N_{2}\cup\{\epsilon\}$ and $\textit{EM}^{\epsilon}\subseteq E_{1}\cup\{\epsilon\}\times E_{2}\cup\{\epsilon\}$ such that $\textit{NM}^{\epsilon}=\textit{NM}\cup\{(n_{1},\epsilon)\mid(n_{1},\_)\not\in NM\}\cup\{(\epsilon,n_{2})\mid(\_,n_{2})\not\in NM\}$, and $\textit{EM}^{\epsilon}=\textit{EM}\cup\{(e_{1},\epsilon)\mid(e_{1},\_)\not\in EM\}\cup\{(\epsilon,e_{2})\mid(\_,e_{2})\not\in EM\}$. Then, $\texttt{merge}_{(NM^{\epsilon},EM^{\epsilon})}(\mathscr{A}_{1},\mathscr{A}_{2})$ returns a UAPDG $\mathscr{A}=(N,E,Lat,M_{f},M_{b})$ constructed as follows:

• •

  $N=\{(n_{1},n_{2})|(n_{1},n_{2})\in NM^{\epsilon}\}$

• •

  We first compute $E^{\prime}=\{(n_{1},n_{2})\xrightarrow{(e_{1},e_{2})}(n_{1}^{\prime},n_{2}^{\prime})|(e_{1},e_{2})\in EM^{\epsilon},e_{i}\neq\epsilon\Leftrightarrow n_{i}\xrightarrow{e_{i}}n_{i}^{\prime}\}$. Since $EM$ is an edge mapping obtained from the graph alignment step, it follows that $e_{1}\neq\epsilon\wedge e_{2}\neq\epsilon\Rightarrow\textit{label}(e_{1})=\textit{label}(e_{2})$. Further, from definition of $EM^{\epsilon}$, it follows that $e_{1}\neq\epsilon\vee e_{2}\neq\epsilon$. Once $E^{\prime}$ is computed, $E=\{(n_{1},n_{2})\xrightarrow{e}(n_{1}^{\prime},n_{2}^{\prime})|(n_{1},n_{2})\xrightarrow{(e_{1},e_{2})}(n_{1}^{\prime},n_{2}^{\prime})\in E^{\prime},e=\{\textit{label}(e_{1}),\textit{label}(e_{2})\}\textbackslash\{\epsilon\}\}$.

• •

  $Lat(n_{1},n_{2})=Lat_{1}(n_{1})\sqcup Lat_{2}(n_{2})$ where the join is applied point-wise to each node predicate at $n_{1}$ and $n_{2}$ (we assume that $Lat(\epsilon)=\bot$)

• •

  $M_{f}(n_{1},n_{2})=x$, if $M_{f1}(n_{1})=M_{f2}(n_{2})=x\in\textit{Var}_{f}$

• •

  Nodes not mapped to free variables are mapped to distinct fresh variables– if $(n_{1},n_{2})\not\in\textit{domain}(M_{f})$, then $M_{b}(n_{1},n_{2})=x_{i}$ for a distinct variable $x_{i}\not\in\textit{Var}_{b}$.

Method project with respect to $\mathscr{A}_{1}$ and $\mathscr{A}_{2}$ projects the merged UAPDG $\mathscr{A}$ to $\mathscr{A}_{c}$ which has nodes (resp. edges) that map to nodes (resp. edges) in both $\mathscr{A}_{1}$ and $\mathscr{A}_{2}$, i.e., nodes in $\mathscr{A}_{c}$ are of the form $(n_{1},n_{2})$ where $n_{i}\in N_{i}$ and edges are of the form $(e_{1},e_{2})$ where $e_{i}\in E_{i}$.

The proof outline for the above theorem is presented in Appendix D. Besides, returning the formula for $\mathscr{A}_{c}$, method getConjunctiveSubrule also returns the set of valuated examples labeled with bound variables used for constructing $\mathscr{A}$. This is achieved by projecting $\mathscr{A}$ to nodes (resp. edges) that map to nodes (resp. edges) in each example. Note, to synthesize conjunctive subrules from a single example (possible in the case of postcondition synthesis), we heuristically include in the subrule all nodes at distance $d=1$ from nodes bound to free variables $\vec{x}$.

In this section, we describe the method generateCandidatePartitions. This method returns a list of low entropy partitions of the input examples $\mathscr{C}$, based on the clustering algorithm in (Li et al., 2004). Let $N$ be the set of nodes in $\mathscr{A}$ and $N_{c}$ be the set of nodes in $\mathscr{A}_{c}$, where $\mathscr{A}$ and $\mathscr{A}_{c}$ are the UAPDGs obtained after calling merge and then calling project on examples in $\mathscr{C}$ respectively. For $n\in N$, let $\mathscr{C}_{n}=\{C_{i}\}\subseteq\mathscr{C}$ be the set of examples such that $n$ maps to a node in $C_{i}$ and let $\mathscr{C}_{\neg n}=\mathscr{C}\backslash\mathscr{C}_{n}$. Entropy of a partition with respect to $n$ is:
$H(\mathscr{C},\mathscr{C}_{n},\mathscr{C}_{\neg n})=\frac{\mid\mathscr{C}_{n}\mid}{\mid\mathscr{C}\mid}.H(\mathscr{C}_{n})+\frac{\mid\mathscr{C}_{\neg n}\mid}{\mid\mathscr{C}\mid}.H(\mathscr{C}_{\neg n})$,
$H(\mathscr{C})=\sum\limits_{n^{\prime}}H_{n^{\prime}}(\mathscr{C})$, where $H_{n^{\prime}}(\mathscr{C})=-p.logp-(1-p).log(1-p)$,
where $p=\mid\mathscr{C}_{n^{\prime}}\mid/\mid\mathscr{C}\mid$. Nodes in $N_{c}$ by definition are mapped to nodes in all input examples. Since code patterns in a rule are often localized, we consider partitions with respect to nodes in $N$ that neighbor nodes in $N_{c}$. Further, we return the set of all partitions whose entropy is within a $\delta$ margin of the smallest entropy partition. Each of these partitions is explored in a BFS manner in method synthesizePC. The process stops at the first partition that synthesizes a postcondition that is unsatisfied by all violating examples.

We present a proof outline in Appendix E. It is easy to argue Algorithm 1’s soundness with respect to violating examples. To argue soundness with respect to conforming examples, we rely on the soundness of the merge algorithm (theorem 2). Using Theorem 2, we argue that all valuated conforming examples satisfy the synthesized postcondition. Since the rule negates the synthesized postcondition, none of them satisfy the synthesized rule.

In both cases, the users label them as "Useful", "Not Useful" or "Not Sure". In live code review, developers also provide textual feedback. The offline evaluation involves $10$ expert developers and does not involve the paper authors.

In our offline evaluation, $91\%$ detections ($107$ out of $117$) were labeled "Useful". We have also received feedback from developers on detections generated by these rules during live code reviews. Over a period of $5$ months, detections from $25$ out of the $31$ rules received developer feedback. $75.8\%$ of these labeled detections ($273$ out of $360$) were categorized as "Useful" by the developers⁶⁶6Most rules that did not receive developer feedback during live code reviews involved detecting code context with deprecated or legacy APIs. These rules trigger rarely during a code review and are thus more appropriate for a code scanning tool. All these rules were validated during offline evaluation.. Some of the textual feedback from live code reviews are: "Interesting, that is helpful", "Will add this check.", and "we have a separate task to look into the custom polling solution https://XX". A high developer acceptance during code reviews shows that RhoSynth is capable of synthesizing code quality rules which are effective in the real-world.

Table 1 provides more information about these synthesized rules. The synthesis time for these rules range from $30ms$ to $13s$, with an average of $1.5s$. Most of these rules are synthesized from few code changes. Rules that only consist of a precondition correspond to a code anti-pattern. $9$ rules consist of both a precondition and a postcondition. Of these, $4$ rules have a disjunctive postcondition. These disjuncts correspond to different ways of writing code that is correct with respect to the rule. One example of such a rule is check-movetofirst, described in Section 2.2. Another example is executor-graceful-shutdown that intuitively checks if ExecutorService.shutdownNow() call is accompanied by a graceful wait implemented by calling ExecutorService.awaitTermination() or ExecutorService.invokeAll(). Besides the supplementary material, we include visualizations for few synthesized rules in Appendix F.

We describe all the rules synthesized by RhoSynth in Table 6.3. A large number of these rules are supported by code documentation or discussions on online forums. They cover a wide range of code quality issues and recommendation categories:

• •

  performance: e.g., use-parcelable, use-guava-hashmap

• •

  concurrency: e.g., conc-hashmap-put, countdown-latch-await

• •

  use of deprecated or legacy APIs: e.g., deprecated-base64, upgrade-enumerator

• •

  bugs: e.g., check-movetofirst, start-activity

• •

  code modernization: e.g., view-binding, layout-inflater

• •

  code simplification: e.g., deseriaize-json-array, use-collectors-joining

• •

  debuggability: e.g., countdownlatch-await, exception-invoke