Lightweight precise automatic extraction of exception preconditions in java methods

In summary, the paper makes the following contributions:

This article extends our previous work What Is Thrown? Lightweight Precise Automatic Extraction of Exception Preconditions in Java Methods, published at the ICSME 2022 conference Marcilio and Furia (2022) with improvements to the wit technique and its implementation, as well as a substantial extension to the experimental evaluation, which now includes a significant fraction of Java 11’s JDK libraries. Correspondingly, the experimental evaluation also explicitly investigates the impact of one of wit’s new features: modular analysis (introduced in Section 3.4).

Listing 1 shows an excerpt of two overloaded implementations of method Jbytes2base64, which takes a byte array and represents it as a string in base 64. As we can see from the initial lines in Jbytes2base64’s second implementation, the two methods have fairly detailed preconditions; furthermore, since the first method calls the second with additional fixed argument values, the first’s precondition is a special case of the second’s. Unfortunately, the documentation of these methods does not mention these preconditions: for example, the second method’s Javadoc comment vaguely describes Joff and Jlen as simply “offset” and “length”, without clarifying that they should be non-negative values. This lack of documentation about valid inputs decreases the usability of the methods for users of the library.

Running wit on class JBytes automatically finds the preconditions of these (as well as many other) methods, thus providing a useful form of rigorous documentation. For instance, one of the exception preconditions found by wit for Listing 1’s second method:

corresponds to the path that reaches line 7 in Listing 1. wit also understands that the first method never throws this exception, but it can still throw others such as:

In fact, wit only reports exception preconditions that correspond to feasible paths. Each precondition comes with an example of argument values that make the precondition true. These are not directly usable as test inputs, since they describe the input’s properties without constructing them; but they are useful complements to the precondition expressions, and help users get a concrete idea of the exceptional behavior.

Listing 2 shows the complete Javadoc documentation and a brief excerpt of method Jmin in the latest version of Apache Commons Lang’s class JNumberUtils, which computes the minimum of an Jarray of integers. Unlike the previous example, Jmin’s documentation is detailed and clearly expresses the conditions under which an exception is thrown. Unfortunately, the documentation is partially incorrect: when Jarray is null, Jmin throws a JNullPointerException, not an JIllegalArgumentException, as precisely reported by wit:

This inconsistency is due to a change in the implementation of JvalidateArray, which is called by Jmin to validate its input and uses methods of class JValidate to perform the validation. In version 3.12.0 of the library, JvalidateArray switched⁶ from calling JValidate.isTrue(a!=null) (which throws an JIllegalArgumentException when the check fails) to calling JValidate.notNull(a) (which throws a JNullPointerException instead) to check that Ja is not null.

This information can help detect and debug such inconsistencies, which would be quite valuable to project developers and users. As we discuss in Section 5.6, maintainers of Apache libraries were appreciative of our pull requests which extended the projects’ documentation with some of wit’s exception preconditions.

wit parses the source code given as input using JavaParser,⁷ and constructs a control-flow graph (CFG) of the methods in the input classes using library JGraphT.⁸ More precisely, we build a CFG for each method Jm individually; and annotate branches in the CFG with each branch’s Boolean condition.

Listing 3 shows excerpts of 3 methods of class JArrayUtils⁹ in Apache Commons Lang. Method Jinsert puts some values Jv into an array Ja of Booleans at a given index Jk. The initial part of its implementation calls another method, JisEmpty, of the same class to determine if Jv is empty; in turn, JisEmpty calls method JgetLength. wit builds CFGs for Jinsert, JisEmpty, and JgetLength, since they are all part of the input source code.

When analyzing a method Jm, wit collects its local exception paths (“expaths” for short). These are all simple directed paths^10,11 on Jm’s CFG that end with a node corresponding to a statement that may throw an exception—either explicitly with a Jthrow or indirectly with a a call (which may return exceptionally).

In Listing 3’s example, one of Jinsert’s local expaths p goes through the else branch on lines 2–3 and through the then branch on line 4, ending with the Jthrow on line 5:

After collecting expaths local to each method, wit converts them into global expaths by inlining calls to other methods.

Given a local expath \(\ell \), for each node \(n_{J{x}}\) in \(\ell \) that calls some other method Jx, wit checks whether Jx’s CFG is available (that is, whether Jx’s implementation was part of the input). If it is, wit enumerates all simple paths that go through the CFG of Jx, and splices each of them into \(\ell \) at \(n_{J{x}}\). In other words, it transforms the local path \(\ell \) so that it follows inter-method calls. Since a method usually has multiple paths, one local expath may determine several global expaths after inlining. wit inlines calls recursively (with some limits that we discuss in Section 3.7).

When a called method Jx’s CFG is not available in the current run, wit first looks whether it analyzed Jx’s source code in some of its previous runs. If this is the case, wit replaces the call to Jx with Jx’s exception preconditions it extracted in the previous runs —following the modular analysis procedure we explain in Section 3.4. Otherwise, if no information about Jx is available or the user deliberately disabled modular analysis, wit doesn’t inline calls to it and marks them as “opaque”.

wit inlines the call to JisEmpty in local expath p (Listing 3’s example) since JisEmpty is part of the same analyzed class JArrayUtils. Inlining the call replaces p’s edge \(J{if}_{3} \xrightarrow {J{!isEmpty(v)}} J{if}_{4}\) with JgetLength’s only path: \(J{if}_{3} \xrightarrow {J{!(getLength(v)==0)}} J{if}_{4}\). Since the implementation of JgetLength is available too, wit recursively inlines its two paths, which finally gives two global expaths \(p_1, p_2\) that inline Jinsert’s local expath p’s calls:

By default, wit saves all exception preconditions it extracts—together with their associated global exception paths—in a database, so that they can be reused to perform a modular analysis. This is useful whenever a method Jm in some project A calls another method Jn in some other project B. If we provide A and B in a single run, wit’s analysis has access to all the source code; thus, in principle, it can inline the code of B’s Jn when analyzing A’s Jm. However, this may not scale, as the number of paths to be considered grows like the product of Jm’s and Jn’s paths. To perform modular analysis, we instead first run wit on B alone; then, we run it on A alone. When wit analyzes Jm in A, it finds that it calls an external method Jn in B; thus, it reuses Jn’s saved exception precondition information to analyze the exceptional behavior of Jm when analyzing A without having to analyze Jn again (or without treating it like an opaque method, which may miss information).¹²

More precisely, if modular analysis is enabled, whenever a node \(n_{J{x}}\) in a local expath \(\ell \) calls a method Jx that was analyzed in a previous run, wit replaces the call to Jx by inlining any global exception path associated with Jx’s exception preconditions (and replacing, as usual, Jx’s formal parameters with the actual call arguments). Just like regular inlining (Section 3.3), this may introduce multiple global expaths for a single call to Jx. It is necessary, in general, to consider all available global expaths for a called method, so that all possible side effects of the call are accounted for. wit can use both expres and maybes for modular analysis.¹³ Since maybes are not guaranteed to be correct, any global expath that includes a maybe is automatically also classified as maybe.

As an example of where modular analysis can improve wit’s capabilities, consider Listing 4. Method Jgenerate¹⁴ of class RandomStringGenerator in project Commons Text calls method Validate.isTrue¹⁵ in another project Commons Lang. If we run wit on project Commons Text alone, the call to isTrue is marked as opaque, and hence no exception precondition would be reported for this path. We could run wit on both projects Commons Text and Commons Lang together; this would take a considerable amount of time, and it would not scale to combining even more projects. Instead, we can use wit’s modular analysis and first analyze Commons Lang in isolation; this would report the exception precondition !expr for method validate.isTrue. Then, when wit runs on Commons Text, it would replace the call to isTrue in generate with if (!(length> 0)) throw new IllegalArgumentException(), which leads to inferring exception precondition length \(\mathtt {<= 0}\) for this path in method generate.

As we will demonstrate in Section 5, modular analysis can boost wit’s output and help achieve a better scalability. Implementation-wise, wit persists JSON objects into a MongoDB¹⁶ instance. For JSON serialization and deserialization, we combine JavaParser’s serialization package¹⁷ with the Moshi JSON library.¹⁸

wit builds global expaths only based on syntactic information in the CFGs; therefore, some paths may be infeasible (not executable). To determine whether a global expath is feasible, wit encodes it in logic form as an SMT (Satisfiability Modulo Theory) formula Barrett et al. (2009), and uses the Z3 SMT solver Mendonça de Moura and Bjørner (2008) to determine whether the expath’s induced constraints are feasible.

To this end, it first transforms the path into SSA (static single assignment) form, where complex statements are broken down into simpler steps, and fresh variables store the intermediate values of every expression. We designed a logic encoding of Java’s fundamental types (int, boolean, byte, arrays, strings) with their most common operations (including arithmetic, equality, length, contains, isEmpty), as well as of a few widely used JDK library methods (such as Array.getLength). wit uses this encoding to build an SMT formula \(\phi \) corresponding to each global expath p: if \(\phi \) is satisfiable, then the global expath p is feasible, and hence it corresponds to a possible exceptional behavior of method m.

wit encodes \(\phi \) as a Python program using the Z3 SMT solver’s Z3Py Python API.¹⁹ Listing 5 shows a simplified excerpt of the SMT program encoding the feasibility of insert’s global expath \(p_1\). First, it declares logic variables of the appropriate types to encode program variables (e.g., k), their basic properties (e.g., a_length, which corresponds to the Java expression a.length), and the values passed via method calls (e.g., getLength is an integer variable storing getLength()’s output). Then, it builds a list c of constraints that capture the path constraints and the semantics of the statements along the path. For example, a_length must be nonnegative, since it corresponds to array a’s length (line 5); the properties of array v are copied to those of x, since insert’s argument v is the actual argument for isEmpty’s formal argument x (line 7); and path constraint !isEmpty(v) corresponds to the complement of Boolean variable isEmpty (line 12). In this case, Z3 easily finds that the constraints in c are unsatisfiable, since Not(0 == 0) is identically false. In contrast, the constraints corresponding to path \(p_2\) are satisfiable, and thus Z3 outputs a satisfying assignment of all variables in that case.

Sometimes wit does not have sufficient information to determine with certainty whether a path is feasible. When a path includes a call to an opaque method (whose implementation is not available or when the analysis fails) wit’s feasibility check is underconstrained. In these cases, wit still performs a feasibility check but reports any results as maybe, to warn that the output may not be correct.

In this scenario, based on its signature,

wit would only know that getLength returns an integer without any constraints; therefore it would classify path p as feasible but mark it as maybe since it is just an educated guess without correctness guarantees.

A feasible path p identifies a range of inputs of the analyzed method m that trigger an exception. In order to characterize those inputs as an exception precondition, wit encodes p’s constraints as a formula that only refers to m’s arguments, as well as to any members that are accessible at m’s entry (such as the target object this, if m is an instance method). To this end, it works backward from the last node of exception path p; it collects all path constraints along p, while replacing any reference to local variables with their definition. For example, method void f(int x){int y=x+1; if(y> 0)throw;} has a single feasible expath with path condition y> 0, which becomes x + 1> 0 after backward substitution through the assignment to variable y. Since x + 1> 0 only mentions argument x, it is a suitable exception precondition for method m.

Sometimes wit cannot build an exception precondition expression that only mentions arguments and other visible members. A common case is when a path includes opaque calls: since the semantics or implementation of these calls is not available, any expressions including them may not make sense in a precondition. In all these cases, wit still reports the exception expression obtained by backward substitution, but marks it as a maybe to indicate that it may not be correct. Another, more subtle case occurs when the exception precondition Boolean expression includes calls to methods (as opposed to just variable lookups). If these methods are not pure (that is, they do not change the program state), the precondition may be not well-formed. For instance, a precondition x.inc() == 0, where calling inc increments the value of x. Here too, wit is conservative and marks as maybe any exception precondition that involves calls to methods that are not known to be pure.

Before outputting any exception preconditions to the user, wit simplifies them to remove any redundancies and display them in a form that is easier to read. To this end, it uses SymPy Meurer et al. (2017),²⁰ a Python library for symbolic mathematics. Java’s syntax is sufficiently similar to C’s that we can also enable SymPy’s pretty printing of expressions using C syntax, and then additionally tweak it to amend the remaining differences with Java. While conceptually simple, the simplification step is crucial to have readable exception preconditions. For example, SymPy simplifies the ugly expression

into the much more readable

, which doesn’t repeat

and omits the tautology 0 + 1 == 1.

wit’s final output consists of a series of tuples with: (a) an exception precondition, (b) whether it is a maybe, (c) the thrown exception type, (d) and an example of inputs that satisfy the precondition (given by Z3’s successful satisfiability check).

For debugging, wit can also optionally report the complete throw statement (including any exception message or other arguments used to instantiate the exception object), the line in the analyzed method m where the exception is thrown or propagated, and a sequence of method calls starting from the analyzed method and ending in the throwing method. Moreover, wit reports the generated Z3 and SymPy Python programs’ source code.

Let us now zoom in on a few details of how wit’s implementation works, which clarify its capabilities and limitations. To put these details into the right perspective, let us recall wit’s design goals: it should be precise and lightweight; it’s acceptable if achieving these qualities loses some generality— as long as a sizable fraction of exception preconditions can be precisely determined.

Using maybes As discussed in Section 3.5, wit provides two disjoint sets of exceptional preconditions as output: expres and maybes. In practice, reporting both gives users more flexibility in how to use wit’s output according to different use cases. If correctness is crucial (for example, if one uses wit’s output as formal specification), then users should only consider expres and ignore maybes. On the other hand, if some degree of uncertainty in the correctness of an exception precondition is acceptable in exchange for a higher recall, then users may also consider maybes. The snag is that they may have to spend extra effort to validate the maybes, but this may be acceptable if there exist practical validation means (for example, an extensive test suite). Any kind of hybrid approach is also possible; for instance, one may first only use expres, but consider using maybes selectively for a few methods where wit’s feasibility analysis struggled due to the features used there.

Implicit exceptions wit only tracks exceptions that are explicitly raised by a throw statement; it does not consider low-level errors—such as division by zero, out-of-bound array access, and buffer overflow—that are signaled by exceptions raised by the JVM. This restriction is customary in techniques that infer exceptional behavior, since implicitly thrown exceptions are “generally indicative of programming errors rather than design choices Weimer and Necula (2004)” Raymond and Weimer (2008), and usually do not belong in API-level documentation Forward and Lethbridge (2002) and are best analyzed separately. Extending wit to also track implicit exceptions would not be technically difficult; for example, one could first instrument the code to be analyzed with explicit checks before any statement that may thrown an implicit exception.²¹ However, indiscriminately considering all exceptions that are thrown implicitly would produce a vast number of boilerplate exception preconditions that are not specific to a method’s explicitly programmed behavior; hence, they would be outside wit’s current focus.

Java features wit’s CFG construction currently does not fully support some Java features: instanceof operators, for-each loops, switch statements, and try/catch blocks. When these features are used, the CFG may omit some paths that exist in the actual program. (Supporting the latter three features is possible in principle, but would substantially complicate the CFG construction.)^22,23 The SMT encoding used for path feasibility (Section 3.5) is limited to a core subset of Java features and standard library methods. As a result, wit won’t report exception preconditions that involve unsupported features (or will report them as maybe, that is without correctness guarantee).

Path length and number In large methods, even some local expaths can be too complex, which bogs down the whole analysis process. Therefore, wit only enumerates paths of up to \(N = 50\) nodes, which have a much higher likelihood of being manageable. Complex methods may have thousands of local paths. Therefore, wit analyzes up to \(N = 500\) paths of a given method or constructor.

Inlining limits Inlining can easily lead to a combinatorial explosion in the number and length of the expaths; therefore, a number of heuristics limit inlining. First, a path can be inlined only if it is up to \(N=50\) nodes—the same limit as for local expaths. Second, wit stops inlining a call in a path after it has reached a limit of \(I=100\) inlined paths—that is, it has branched out the call into I different ways. It can still inline other calls in the same path, but this limit avoids recursive inlinings that are likely to blow up. Third, wit enumerates the inlinings of a call in random order; in cases where the limit I is reached, this increases the chance of collecting a more varied set of inlined paths instead of getting stuck in some particularly complex ones (if the limit I is not reached, the enumeration order is immaterial).

Maybes heuristics The feasibility of exception preconditions reported as maybes could not be verified; hence, they are educated guesses. Consequently, wit deploys two simple heuristics that filter out maybes that are overwhelmingly unlikely to be correct. First, wit does not report any maybe assertion that consists of more than six conjuncts or disjuncts; we found that the constraints of such large maybes are usually unsatisfiable. Second, wit drops any maybe that includes constraints over private fields of the JDK’s String and StringBuilder classes. This heuristic only applies when wit uses modular analysis: these two JDK classes have a complex implementation involving native code and JVM internals. Thus, wit’s analysis of String and StringBuilder can only retrieve a few correct maybes; as a result, using them in the modular analysis of other client classes is likely to introduce a large number of spurious maybes—which this heuristic avoids.

Timeouts Z3’s satisfiability checks (to determine if a path is feasible) may occasionally run for a long time. wit limits each call to Z3 to a \(Z=15\)-second timeout; when the timeout expires, Z3 is terminated and the path is assumed to be infeasible. There is also an overall timeout of \(T=10\) minutes per analyzed class. If wit’s analysis still runs after the timeout, it probably means that the class’s methods are particularly intricate and hard to process;to remain lightweight, wit skips to the next class.

Configurable options The parameters regulating these heuristics can be easily changed if one needs to analyze code with peculiar characteristics, when a large running time is not a problem. wit also offers two slightly different Z3 logic encodings of some Java features. By default, it employs a conservative encoding that ensures that all expressions used in an exception precondition are well defined (for example, a.length implicitly requires that a != null). In some complex cases, this encoding may be overly conservative, leading to marking as unsatisfiable exception preconditions that are actually correct. To accommodate these unusual cases, wit also offers a less conservative logic encoding of the same features, which trades off correctness for recall; users can switch to this alternative encoding when analyzing software where a high recall is more important than an absolute correctness guarantee.

Modular analysis wit’s modular analysis (Section 3.4) is also configurable to fit each application scenario. By default, wit performs modular analysis: if it encounters a call to a method that it analyzed in a previous run, it uses the called method’s exception preconditions to determine the exception preconditions of the caller. In contrast, if the user explicitly disables modular analysis, wit analyzes each project in isolation. Section 5.4 describes experimental data that we collected to better understand the practical impact of using wit’s modular analysis. When modular analysis is enabled, wit can reuse only expres or both expres and maybes. This is another parameter that one can choose according to how important a high recall is: reusing also maybes can only increase the number of maybes inferred by wit, which come with no guarantee of being correct. In general, modular analysis is an additional option made available by wit, which need not be used in all situations: whether enabling it is beneficial depends on the projects under analysis and on the user’s requirements.

In our evaluation, we ran wit on two groups of projects: several standard libraries in Java’s JDK and 46 open-source Java projects surveyed by recent papers investigating the (mis)use of Java library APIs Wen et al. (2019); Zhong et al. (2020); Kechagia et al. (2021) and the automatic generation of tests for some of these libraries Nassif et al. (2021). Table 1 lists all our experimental subjects.

JDK modules The JDK (Java Development Kit) includes arguably Java’s most widely used and mature libraries, featuring virtually in every Java project Nassif et al. (2021); Kechagia et al. (2019) and abundantly documented. We selected JDK 11²⁴ to run our experiments, since it’s the most recent LTS (Long Term Support) release that JavaParser can handle at the time of writing. Given the JDK’s gargantuan size and complexity, we selected five of its modules (subdirectories of java.base/share/classes) and ran wit on all of them as if it were a regular Java project: modules com/sun, java, javax, sun, and jdk.

Other projects The other group of 46 experimental subjects includes several projects that are also large, widely-used, mature Java projects in various domains (base libraries, GUI programming, security, databases)—especially the 26 projects from the Apache Software Foundation, which recent empirical research has shown to be extensively documented and thoroughly tested Zhong et al. (2020); Nassif et al. (2021). On the other hand, a few projects taken from Kechagia et al. (2021) are smaller, less used, or both. For instance, projects gae-java-mini-profiler, visualee, and AutomatedCar are no longer maintained. This minority of projects makes the selection more diverse, so that we will be able to evaluate wit’s capabilities in different scenarios.

We used the latest commit/stable release in every project, at the time of writing, with two exceptions: Apache lucene-solr was recently split into two separate projects, and thus we used the last version before the split; we analyzed version 2.6 of Apache Commons IO to match Nassif et al. (2021)’s thorough manual analysis—which we used as ground truth to answer RQ2.

We ran wit on the source code of all projects, after excluding directories that usually contain tests (e.g., +src/test/+) or other auxiliary code. All experiments ran on a Windows 11 Intel i9 laptop with 32GB of RAM. By default, wit only infers the exception preconditions of public methods; if a public method calls a non-public one, wit will also analyze the latter, but will report only public exception preconditions. wit analyzes each class in isolation; then, it combines the results for all classes in the same project and outputs them to the user.

Unless we explicitly state otherwise, wit ran with default options in the experiments. In particular, it performed modular analysis (described in Section 3.4); therefore, we first ran wit on the JDK modules, then on the Apache Commons libraries (lang, io, text, math, configuration, in this order) followed by all other projects in alphabetical order. Since practically all projects use some JDK libraries, and several projects also use Apache Commons libraries, this execution order maximizes the chances that wit can reuse the results of one of its previous runs to perform an effective modular analysis. In contrast, client-of dependencies between projects other than the JDK and Apache Commons libraries are more sparse; therefore, the alphabetical order is somewhat arbitrary, but even following a different order is unlikely to significantly affect wit’s capabilities.

To answer RQ1 (precision), we performed a manual analysis of a sample of all exception preconditions reported by wit to determine if they correctly reflect the exceptional behavior of the implementation. The first author tried to map each inferred exception precondition to the source code of the analyzed method. In nearly all cases, the check was quick and its outcome clear. The few exception preconditions whose correctness was not obvious were analyzed by the other author as well, and the final decision was reached by consensus. We were conservative in checking correctness: we only classified an exception precondition as correct if the evidence was clear and easy to assess.

To answer RQ2 (recall), we used Nassif et al. (2021)’s dataset—henceforth, DSc—as ground truth. DSc includes 844 manually-collected exception preconditions²⁵ (expressed in structured natural language, e.g. “if offset is negative”) for all public methods in Apache Commons IO’s base package collected from all origins (package code, libraries, tests, documentation, ...). We counted the exception preconditions inferred by wit that are semantically equivalent to any in DSc. Matching DSc’s natural-language preconditions to wit’s was generally straightforward, as we didn’t have to deal with subtle semantic ambiguities: since wit only reports correct exception preconditions as expres, we only had to match (usually simple) natural-language expressions to their Java Boolean expression counterparts.

Using DSc as ground truth assesses wit’s recall in a somewhat restricted context: (i) DSc targets exclusively the Commons IO project, whose extensive usage of I/O operations complicates (any) static analysis; (ii) DSc describes all sorts of exceptional behavior, including the “not typically documented” runtime exceptions Nassif et al. (2021). To assess wit’s recall on a more varied collection of projects, we also considered Zhong et al. (2020)’s dataset—henceforth, DPA—which includes 503 so-called “parameter rules” of public methods in 9 projects (a subset of our 46 projects described in Section 4.1). A parameter rule is a pair \(\langle m, p \rangle \), where m is a fully-qualified method name and p is one of m’s arguments; it denotes that calling m with some values of p may throw an exception. Important, parameter rules do not express the values of p that determine an exception, and hence they are much less expressive than preconditions; however, they are still useful to determine “how much” exceptional behavior wit captures. We counted the exception preconditions inferred by wit that match DPa: a precondition c matches a parameter rule \(\langle m, p \rangle \) if c is an exception precondition of method m that depends on the value of p. This is a much weaker correspondence than for DSc, but it’s all the information we can extract from DPa’s parameter rules.

To better characterize the exception preconditions that wit could not infer, we performed an additional manual analysis of: (a) 746 of DSc’s exception preconditions among those that wit did not infer and (a) 218 exception preconditions reported by wit as “maybe” (that is, which may be incorrect). These 964 additional cases help assess what it would take to improve wit’s recall.

To answer RQ3 (features), during the manual analysis of precision we also classified the basic features of each exception precondition r of a method m. We determine whether r corresponds to an exception that is thrown directly by m or propagated by m (and thrown by a called method). We count the number of Boolean connectives

and

in e, which gives an idea of r’s complexity. Then, we determine if each subexpression e of r constraints m’s arguments, or m’s object state; and we classify r’s check according to whether it is: (a) null check (whether a value is null), (b) a value check (whether a value is in a certain set of values), (c) a query check (whether a function call returns certain values). For example, here are expressions of each kind for a method m with arguments int x and String y, whose class includes fields int[] a, int count, and method boolean active():

An exception precondition may combine expressions of different kinds; for instance,

combines a null and a value check.

To answer RQ4 (modularity), we ran wit again on 5 projects with modular analysis disabled, and compared wit’s output on these projects with and without modular analysis. We selected the 5 projects from diverse domains, which demonstrate using different JDK libraries and methods. Besides comparing the number of reported exception preconditions with and without modular analysis, we manually inspected 75 maybes: (a) For each project, among methods for which both the modular and non-modular analysis reported some maybes, we randomly picked 6 maybes reported by the non-modular analysis and 6 maybes reported by the modular analysis for the same methods;²⁶ this sample of 60 maybes (\(6 \times 5 \times 2\)) gives us an idea of how maybes change when modular analysis is enabled. (b) For each project, among methods for which only the modular analysis reported some maybes, we randomly picked 3 maybes; this sample of 15 maybes (\(3 \times 5\)) demonstrates cases where the modular analysis strictly outperforms the non-modular one.

We focused on Javadoc documentation: while we also considered non-structured comments a priori, all cases of documented exceptional behavior that we found used at least some Javadoc syntax.

We also selected 90 inferred exception preconditions among those that were not already documented, and submitted them as 8 pull requests in 5 projects: Accumulo,²⁷Commons Lang,^28,29,30Commons Math,^31,32Commons Text,³³ and Commons IO.³⁴ We selected these five projects as they are very active and routinely spend effort in maintaining a good-quality documentation. Each pull request combines the exception preconditions of methods in the same class or package, and expresses wit’s exception preconditions using Javadoc @throws tags. To compile each pull request, we sometimes complemented the Javadoc with a brief complementary natural-language description, and possibly some tests (expressing wit’s example inputs in the form of unit tests). We also tried to adjust the Javadoc syntax to be consistent with each project’s style (for example, expressing a != null as either a not null or @code a != null). In all cases, reformulating wit’s output was a trivial matter.

In order to validate wit’s feasibility check, we manually analyzed a sample of 742 expres to determine if they are indeed correct. This sample size is sufficient to estimate precision with up to 5% error and 99% probability with the most conservative (i.e., 50%) a priori assumption authorname (1999); thus, it gives our estimate good confidence without requiring an exhaustive manual analysis Zhou et al. (2020); Nassif et al. (2021). We applied stratified sampling to pick the 742 expres: we randomly sampled 10 instances in each of the 49 projects where wit detected some expres.³⁵ This manual analysis found that all expres were indeed correct, that is 100% precision.

As we explained in Section 3, wit’s maybes still have a chance of being correct exception preconditions, but they remain educated guesses in general. We randomly picked 218 maybes uniformly in the 50 projects that report some³⁶

and manually checked them as we did for the expres. We found that 47% (102) of them are indeed correct; thus, wit’s precision remains high (88% \(= (102+742)/(218+742)\)) even if we consider all maybes. As we further discuss in Section 5.2, in most cases, wit could not confirm the maybes as correct because they involve unsupported Java features (see Section 3.7).

We compute the recall on both datasets DSc and DPa in four ways: considering only expres or also maybes; and considering only wit’s supported features or all Java features. Table 2 summarizes the results that we detail in the following.

Section 5.2’s comparison of wit’s preconditions with those in DSc Nassif et al. (2021)’s extensive collection confirmed what also reported by other empirical studies Blasi et al. (2018); Zhou et al. (2020): exception preconditions are often concise and structurally simple. This was also reflected in a manual sample of 412 expres inferred by wit,⁴² which we manually inspected to determine their features. In terms of size, 74% of them are simple expressions without Boolean connectives

/

; and only 7% include more than one connective. In terms of control-flow complexity, 68% of wit’s expres involve exceptions that are thrown directly by the analyzed method (as opposed to propagated from a call).

If we look at maybes, they tend to include query checks more frequently (50%), which is to be expected since a method call can be soundly used in a precondition only when it is provably pure (Section 3.6).

Up to 12% of the expres in the sample are the simplest possible Boolean expression: true. Nine of 13 expres of spring-cloud-gcp are of this kind. These usually correspond to methods that unconditionally throw an UnsupportedOperation exception to signal that they are effectively not available;^43,44

see project lucene-solr’s class ResultSetImpl for an example.⁴⁵ In Java, this is a common idiom to provide “placeholders,” which will be replaced by actual implementations through overriding in subclasses. While this is a common programming pattern that leverages polymorphism, it nominally breaks behavioral substitutability Liskov and Wing (1994); Nguyen et al. (2014): a method’s precondition should only be weakened Meyer (1997), but no Boolean expression is weaker than true.

Some of the exception preconditions that we manually inspected revealed interesting and non-trivial features. wit could infer expres embedded in complex expressions, such as in the case⁴⁶ of an empty string that triggers an exception in the “else” part e of a ternary expression. c ? t : e. It also followed method calls collecting complex conditions and presenting them in a readable, simplified form. For example, for a ConcurrentModification exception,⁴⁷ or after collecting constant values from other classes.⁴⁸

We also found examples of exceptional behavior documented in Javadocs in a way that mirrors wit’s output, such as “IndexOutOufBoundsException \(\mathtt {i < 0}\) or \(\mathtt {i >}\) array.length”.⁴⁹

In all, wit’s output is often concise and to the point—and thus readable and useful.

To answer RQ4 (the impact of modular analysis), Section 5.4.1 first discusses how the output of wit changes when modular analysis is disabled vs. when it is enabled; then, Section 5.4.2 presents the results of a manual comparison of a sample of exception preconditions obtained with and without modular analysis.

Thanks to the heuristics it employs (Section 3.7) and to the nature of exception preconditions wit can infer (which tend to be simpler compared to general program behavior), wit’s analysis is quite lightweight and scalable. As shown in Table 1, its running times are generally short: it processed the entire Apache Commons Lang in just 55 minutes—17 seconds on average for each of the project’s 200 top-level classes. It also scales well to very large projects: it analyzed the 9 780 classes of Apache Camel (the largest project in our collection) in 44 hours—just 16 seconds per class on average. Key to this performance is wit’s capability of analyzing each class in isolation, without requiring any compilation or build of the whole project.

Take method ASMifier.appendAccess()⁶² as an example of how wit’s heuristics are useful. It is from project ASM and embedded under the internal subdirectory of the JDK. The method has several nested if-else branches, that lead to millions of paths. wit’s heuristics are crucial to avoid getting bogged down analyzing such complex pieces of code.

This section discusses to what extent wit’s exception preconditions and the documented exceptional behavior of methods overlap. We first look into all projects except the JDK modules (Section 5.6.1), and then analyze the JDK separately (Section 5.6.2); finally, we discuss how we submitted some of wit’s inferred exception precondition as pull requests (Section 5.6.3).

As we demonstrated in Section 5.6.3, the output of wit’s analysis can be useful to extend, complement, and revise the documentation of public methods’ exceptional behavior. Accurately documenting exceptions is crucial for developers Zhou et al. (2020), but writing documentation is onerous Nassif et al. (2021); Nguyen et al. (2014); as a result, APIs often lack documentation Robillard et al. (2013), especially for exceptions Raymond and Weimer (2008). wit’s high precision ensures that its output can generally be trusted without requiring manual validation, and hence it can directly help the job of developers writing documentation (or tests).

In most cases, wit’s exception preconditions are in a form that can be easily transformed into method documentation—for example by expressing them in natural language using pattern matching Zhou et al. (2020); Blasi et al. (2018); Goffi et al. (2016). In fact, since it uses precise static analysis, we found several cases where wit’s exception preconditions provide more rigorous information than what is available in programmer-written documentation. For example, Listing 10 shows the programmer-written exceptional behavior documentation and the initial part of the implementation of a method from class Conversion in project Apache Commons Lang. wit outputs two exception preconditions for the method:both corresponding to an IllegalArgument exception. At first sight, it may seem that wit’s output is incomplete (it doesn’t mention the preconditions “src is empty” and “src is null” in the Javadoc)⁸⁴ and needlessly verbose (isn’t src.length \(\mathtt {<= 8}\) redundant?). A closer look, however, reveals that several aspects of the natural-language documentation are questionable or inconsistent. First, it mixes explicitly and implicitly thrown exceptions: a NullPointer exception is thrown by the Java runtime when evaluating the expression on line 6, not by the method’s implementation. wit ignores such language-level exceptions by design; as we mentioned in Section 3.7, not including implicit exceptions in API documentation may be preferable Forward and Lethbridge (2002); Raymond and Weimer (2008). A second issue with Listing 10’s documentation is that it is incorrect: if src is empty, the method does not throw an IllegalArgument exception; instead, the Java runtime throws an IndexOutOfBounds exception at line 12 (another system-level implicit exception). Finally, Listing 10’s documentation is inconsistent regarding the order in which the various exception preconditions are checked: whether src is null is checked first (implicitly), followed by src.length \(\mathtt {> 8}\) (explicitly), src.length - srcPos \(\mathtt {< 4}\) (explicitly), and whether src is empty (implicitly)—in this order. Thus, predicate src.length \(\mathtt {<= 8}\) in wit’s second inferred preconditions is not redundant but rather useful to ensure that the precondition precisely captures the conditions under which a certain path is taken. Admittedly, wit may sometimes present preconditions in a form that is harder to understand for a human; for example, it is questionable that the “simplification” of src.length - srcPos \(\mathtt {< 4}\) into srcPos - src.length \(\mathtt {> -4}\) improves readability. However, these are just pretty-printing details that are currently left to SymPy; changing them to generate constraints that follow certain preferred templates could be done following Nguyen et al.’s Nguyen et al. (2014) approach. In fact, one could even let the user decide the output format according to their preference. Overall, this example demonstrates that wit’s output often has all the information needed to generate accurate documentation that avoids ambiguities or other inconsistencies.

Automatically generating tests that exercise⁸⁵ a method’s exceptional behavior is another natural applications of wit. Fully pursuing it is outside this paper’s scope; nevertheless, we briefly discuss this directions on a few concrete examples that we encountered while carrying out Section 4’s empirical evaluation.

As mentioned in Section 3, each exception precondition reported by wit also comes with an example of inputs that satisfy it; for instance, for exception precondition (2), wit outputs the example [src.length=2, srcPos=0]. Writing a test that initializes an array with two elements, calls the method in Listing 10, and checks that an IllegalArgumentException is thrown (and that it contains a specific message) is straightforward. In fact, one could even try to automate the generation of tests and oracles from wit’s examples and preconditions. For example, using property-based testing Claessen and Hughes (2000): after expressing (2) (or even the specific example) as an input property, let a tool like jqwikjqwik: Property-Based Testing in Java: https://​jqwik.​net/​ randomly generate inputs that satisfy it.

can also improve the quality of the tests that are written, as demonstrated by the following example. Listing 11 shows a (simplified) excerpt of method Fraction.getFraction in Apache Commons Lang, which takes three integers whole, num, den, and returns an object representing the fraction \(\texttt {whole} + \texttt {num}/\texttt {den}\). As we can see in Listing 11, getFraction has 4 exception preconditions: (a) (line 2) when den is 0; (b) (line 3) when den is negative; (c) (line 4) when num is negative; (d) (line 8) when the resulting numerator nv exceeds the largest integer in absolute value. Commons Lang is a thoroughly tested project Nassif et al. (2021), and in fact all four exceptional behaviors are tested.https://​github.​com/​apache/​commons-lang/​blob/​ce477d9140f1439c​44c7a852d7df1e06​9e21cb85/​src/​test/​java/​org/​apache/​commons/​lang3/​math/​FractionTest.​java#L437 The 4 behaviors are not evenly tested though: 3 calls cover (a), 6 calls cover (b) (including three identical calls, which is likely a copy-paste error), 1 call covers (c), and 4 calls cover (d). Comments in the test method which refer to the four categories are sometimes misplaced (for example, two calls under “zero denominator” actually cover (d)). In contrast, wit’s example inputs correspond one-to-one and uniquely to each exception precondition: (a) den=0; (b) den=-1; (c) num=-1, den=1; (d) whole=2147483648, num=0, den=1. If we wanted multiple example inputs for the same precondition, we could just ask Z3 to generate more. In all, wit’s output can be quite useful to guide a systematic test-case generation process.

Another situation where wit’s output helps write tests that exercise exceptional behavior is when this requires a combination of inputs for different arguments. One example is Commons Text’s method FormattableUtils.append(),https://​github.​com/​apache/​commons-text/​blob/​04748ac369316368​5e411167e5c689eb​9ae98dac/​src/​main/​java/​org/​apache/​commons/​text/​FormattableUtils​.​java#L90 which takes 6 arguments and comes from Java’s Formatter interface.https://​docs.​oracle.​com/​en/​java/​javase/​18/​docs/​api/​index.​htmlFormattableUtils.append()’s exception precondition involves the negation of a disjunction of three Boolean predicates:

. wit suggests an example input where e.length() is 1, and p is 0, which is easy to implement as a test. Another example is method StringSubstitutor.replace()https://​github.​com/​apache/​commons-text/​blob/​04748ac369316368​5e411167e5c689eb​9ae98dac/​src/​main/​java/​org/​apache/​commons/​text/​StringSubstituto​r.​java#L742 in the same project, which takes three arguments (one character array and two integers) and may throw an exception in a nested call. As regularly seen in Apache Commons projects, the method accepts null or empty arrays; however, when the array is non-null, the exception precondition gets quite complex. wit provides exception triggering inputs for the three arguments, including that the character array must not be null and could be empty. In cases like this, we could reuse parts of wit’s extracted precondition to document the complex exception condition. The complexity of the precondition, together with it being in a nested call, may be the reason why the documentation and tests were missing in the project.