# Program Structure Aware Precondition Generation

Elizabeth Dinella  University of PennsylvaniaPhiladelphiaPAUSA ,  Shuvendu
Lahiri  Microsoft ResearchRedmondWAUSA and  Mayur Naik  University of
PennsylvaniaPhiladelphiaPAUSA

###### Abstract.

We introduce a novel approach for inferring natural preconditions from code.
Our technique produces preconditions of high quality in terms of both
correctness (modulo a test generator) and naturalness. Prior works generate
preconditions from scratch through combinations of boolean predicates, but
fall short in readability and ease of comprehension. Our innovation lies in,
instead, leveraging the structure of a target method as a seed to infer a
precondition through program transformations. Our evaluation shows that humans
can more easily reason over preconditions inferred using our approach. Lastly,
we instantiate our technique into a framework which can be applied at scale.
We present a dataset of $\sim$18k Java (method, precondition) pairs obtained
by applying our framework to 87 real-world projects. We use this dataset to
both evaluate our approach and draw useful insights for future research in
precondition inference.

††conference: The 32st ACM Joint European Software Engineering Conference and
Symposium on the Foundations of Software Engineering; 15 - 19 July, 2024;
Porto de Galinas, Brazil

##  1\. Introduction

Methods in programming languages are partial functions that map a subset of
inputs to an output value. Unlike mathematical functions, a method is expected
(according to the designer of the method) to be invoked on only a subset of
all possible input values. Invoking a method on illegal inputs can result in
an exception, crash, or undefined behavior. A boolean function which accepts
all legal inputs and rejects all illegal inputs is a precondition.

Preconditions serve a valuable purpose for both software engineering tools and
programmers. Preconditions assist programmers in comprehension and correct
usage of an API (Yun et al., 2016). Reasoning about which inputs are legal vs.
illegal is critical to software correctness (Cousot et al., 2011; Sutton,
1995). Preconditions also enable effective application of automated testing
(Pacheco et al., 2007; Godefroid et al., 2005; Tillmann and de Halleux, 2008;
Fraser and Arcuri, 2011), static analysis (cla, [n. d.]; Xie and Aiken, 2005)
and verification (Leino, 2010). In general, preconditions are essential for
precise modular analysis. Ultimately, they play a significant role for both
tools and programmers alike.

Various approaches have been proposed to automatically infer preconditions.
Static approaches are conservative and lead to false positives (Chandra et
al., 2009; Cousot et al., 2013; Seghir and Kröning, 2013). Dynamic approaches,
which employ a test generator (Padhi et al., 2016; Sankaranarayanan et al.,
2008; Ernst et al., 2007; Astorga et al., 2018), have been successful in
generating correct and precise preconditions. In this setting, a correct
precondition accepts legal inputs and rejects illegal ones, modulo a test
generator. However, the inferred preconditions are often unnatural and
difficult for humans to reason over. Such approaches involve combining
“features” to construct a boolean predicate. Features can be defined as
predicates over a method’s inputs (e.g. x > 0) (Padhi et al., 2016) or object
state (e.g. foo.size() > 0) (Astorga et al., 2019). By combining these
features, we show that the resulting predicate can become unnecessarily
complex and difficult to comprehend, and ultimately, unnatural.

Natural preconditions are desirable for a variety of reasons. Firstly, they
are easier for programmers to consume and comprehend. Natural preconditions
are better suited for human-in-the-loop settings such as integrated
development environments and interactive program verifiers. In general,
natural preconditions are easier to understand and therefore easier to specify
and refine, contributing to a more effective and accurate development or
analysis (Fava et al., 2016). Likewise, natural preconditions phrased in a
similar language to the original method are likely to be preferred by
statistical models for code that increasingly underlie software engineering
tools (Hindle et al., 2012). Leveraging natural preconditions aligns well with
the evolving landscape of software engineering tools and statistical modeling
to enhance the efficacy of human-involved processes (Sutton et al., 2023;
Hellendoorn et al., 2019; Zhai et al., 2020).

In this paper, we propose a dynamic approach for inferring natural and correct
preconditions. In contrast to existing approaches, we infer a precondition by
performing transformations to the target method. Rather than constructing
preconditions from scratch through feature combination, we leverage the
structure of the method to seed and guide inference. We introduce a pragmatic
and efficient framework that tackles the intricacies of real-world constructs
found in modern programming languages including complex control flow, heap
manipulations, interprocedural calls, and lengthy call chains. Furthermore, we
discuss the challenges involved in developing an algorithm to infer
preconditions through program transformation. To illustrate this, we present
alternate naive approaches and illustrate pitfalls of these algorithms.
Through this, we arrive upon an algorithm which iterates between input
generation and refined program transformation, ultimately converging on a
correct and natural precondition.

We evaluate our approach in terms of both naturalness and correctness by
performing a comparative study to prior work. We find that our preconditions
are comparably correct yet strongly preferred by humans in terms of ability to
reason over. By conducting a user study, we find that human participants were
able to more accurately reason over our preconditions in a shorter time span
versus the state-of-the-art approach. Consumers of our preconditions completed
reasoning tasks more accurately (92.86%) with an average total duration of 109
seconds. In contrast, consumers of the preconditions inferred by prior work
took twice as long (217 seconds) to finish the study and answered with lower
accuracy (85.61%).

Finally, we present the implementation of our approach as a tool and
demonstrate its application on a significant scale across 87 real-world Java
projects. This yields $\sim$18k (method, precondition) pairs, obtaining the
first large-scale dataset of preconditions (Zhai et al., 2020; Fava et al.,
2016). This dataset not only underscores the viability and effectiveness of
applying our tool at scale, but also provides a rigorous benchmark for
evaluation. In this paper, we use this benchmark to conduct a large-scale
evaluation of the design decisions made to enhance effectiveness of our
approach. We also present characteristics of the dataset which in turn offers
valuable insights to guide future research efforts in the field of
precondition inference.

##### Contributions

In summary, our work makes the following contributions:

  1. (1)

We introduce a novel methodology for inferring correct and natural
preconditions through program transformation.

  2. (2)

We present an instantiation of our approach as a tool which can be applied at
scale.

  3. (3)

We perform a comparative evaluation to the state-of-the-art precondition
generation approach and show that ours are more easily reasoned over by humans
through a user study.

  4. (4)

We curate a substantial dataset of $\sim$18k samples as a benchmark for large-
scale evaluation, accompanied by an exploratory study of its characteristics.

  5. (5)

We perform a large-scale evaluation of the decisions made to design our
approach, showing they contribute to higher quality preconditions.

Our tool and dataset are included anonymously as supplementary material in the
submission. We plan to open-source and publicly release both upon publication.

##  2\. Motivating Examples

⬇

1 public BigInteger[] DivideAndRemainder(BigInteger val) {

2 if (val.m_sign == 0)

3 throw new ArithmeticException("Division by zero error");

4 BigInteger[] biggies = new BigInteger[2];

5 if (m_sign == 0) {

6 biggies[0] = Zero;

7 biggies[1] = Zero;

8 } else if (val.QuickPow2Check()) {

9 int e = val.Abs().getBitLength() - 1;

10 NetBigInteger quotient = Abs().ShiftRight(e);

11 int[] remainder = LastNBits(e);

12 biggies[0] =

13 val.m_sign == m_sign ? quotient : quotient.Negate();

14 biggies[1] =

15 new BigInteger(m_sign, remainder, true);

16 } else {

17 int[] remainder = (int[]) m_magnitude.clone();

18 int[] quotient = Divide(remainder, val.m_magnitude);

19 biggies[0] =

20 new BigInteger(m_sign * val.m_sign, quotient, true);

21 biggies[1] =

22 new BigInteger(m_sign, remainder, true);

23 }

24 return biggies;

25 }

⬇

1 boolean M_pre(NetBigInteger val) {

2 if (val == null)

3 return false;

4 if (val.m_sign == 0)

5 return false;

6 return true;

7 }

(a) Generated by our approach.

⬇

1 (not (val == null))

2 and (

3 (val.getIntValue() == val.m_sign and (

4 (val.getIntValue() <= -1) or

5 ((not (val.getIntValue() <= -1)) and

6 (not (val.getIntValue() <= 0))

7 ))

8 ) or

9 (not (val.getIntValue() == val.m_sign))

10 )

(b) Generated by Proviso.

Figure 1. A method and its corresponding preconditions.

In this section, we motivate and illustrate our approach using the example in
Figure 1. Consider a Java method DivideAndRemainder, for which we aim to infer
a precondition. The target method implementation for dividing arbitrary-
precision integers is shown on the left of the figure. A correct precondition
for this method does not allow inputs where the denominator argument val is
either the BigInteger Zero or null. Indeed, the method explicitly throws an
ArithmeticException when the denominator is zero, which is captured by the
check (val.m_sign == 0) on line 3. Additionally, the method implicitly throws
a NullPointerException upon execution of line 2 when val is null.

Without an explicit precondition, it may be difficult to reason about which
inputs are illegal. From a cursory analysis of a method’s implementation it
may be evident from the explicit throw expression that an input val with
m_sign equal to 0 is an illegal input. However, the second exceptional input,
a val equal to null, is less obvious. This exception is checked for and thrown
implicitly by the JVM during the evaluation of expression val.m_sign. The
challenge of inspecting the implementation is further compounded by the need
for interprocedural reasoning since exceptions could be thrown by callees of
the target method.

Our approach is based on the observation that methods usually contain
sufficient structure of the precondition to seed and guide the inference
process. By leveraging this insight, our approach is able to generate the
precondition shown in Figure 1(a) through a series of program transformations.
The precondition is not only correct (modulo a test generator) but also
natural. In contrast, existing approaches attempt to synthesize the
precondition from scratch through boolean combinations of predicates. Figure
1(b) shows such a precondition synthesized by a state-of-the-art approach
Proviso (Astorga et al., 2019), which is unnatural albeit semantically
equivalent.

Proviso generates the precondition using a combination of predicates and
inequalities over numeric primitives as well as boolean and integer returning
observer methods. By combining such predicates, the precondition can become
unnecessarily complex. In particular, the numeric inequalities and negations
on lines 4-6 can be simplified to the equivalent clause: val.getIntValue() !=
0. Further simplification results in the semantically equivalent predicate val
!= null and val.m_sign != 0.

In contrast, we find that leveraging the program structure and performing
program transformations often leads to more natural preconditions. Such an
approach gives rise to two subproblems: (1) lifting implicit JVM checks to
explicit source code checks and (2) removing code irrelevant to the
precondition. In Figure 1(a), this amounted to inserting the nullness check
prior to line 2 and removing lines 4-24 (in the target method) which are
unrelated to the precondition. We also include an example, Figure 2, from our
dataset to illustrate the complexity of real-world preconditions. In this
example, the subproblems amounted to (1) inserting three nullness checks
corresponding to the field accesses marked in red (Figure 2) and (2) removing
the initialization and modification of votes. In Section 3 we discuss the
challenges of these two subproblems as well as a discussion of our design
decisions in Section 4.

⬇

1 boolean isAuthorized(AuthorizationContext context, AuthorizedAction action)
{

2 Map<AuthorizationModule, AuthorizationVote> votes =

3 new HashMap<AuthorizationModule, AuthorizationVote>( .size());

4 for (AuthorizationModule module : this.authorizationModules) {

5 if ( .supports(action)) {

6 AuthorizationVote vote = module.isAuthorized(context, action);

7 votes.put(module, vote);

8 }

9 }

10 return .isAuthorized(context, action, votes);

11 }

Listing 1: Method from the JSecurity Project.

⬇

1 boolean M_pre(AuthorizationContext context, AuthorizedAction action) {

2 if (authorizationModules == null)

3 return false;

4 for (AuthorizationModule module : authorizationModules) {

5 if (module == null)

6 return false;

7 }

8 if (strategy == null)

9 return false;

10 return true;

11 }

(a) Our Inferred Precondition.

Listing 2: A real-world example from our dataset.

##  3\. Problem Formulation

In this section, we formulate the problem of inferring preconditions through
program transformation. Given a deterministic method M, we infer a
precondition, M_pre. Following the definition of correctness from (Astorga et
al., 2019), we aim to generate a precondition which is _safe_ and _maximal_. A
safe M_pre is one that rejects any illegal input while a maximal M_pre is one
that accepts any legal input.

Given an exhaustive tester T which generates a set of input environments E, we
aim to infer an M_pre with the following correctness properties for every
$e\in\texttt{E}$:

> $\texttt{M\\_pre}{}(e)\rightarrow True$ iff M exits normally on $e$ and
> $\texttt{M\\_pre}{}(e)\rightarrow False$ iff M throws an exception on $e$.

###  3.1. Sub-Problems

Deriving an algorithm for M_pre inference, through a conjunction of program
transformation and test generation, comes with challenges.

##### Lifting Implicit Exception Checks

In order for M_pre to be safe, it must include a check to guard against all
feasible crashes. To design an algorithm for check insertion, one must
consider (1) when $T$ should be invoked to generate $E$, (2) when guards
should be inserted, and (3) the design of program transformations to insert
guards which are crash type specific. One obvious algorithm is exhaustive up-
front transformation which systematically inserts checks, prior to invoking
$T$. Presumably, it is possible for a static exploration to find all JVM level
exception checks which can then be translated to exhaustive source level
checks. We also present an alternate single step non-iterative algorithm. This
algorithm begins by invoking $T$ once, and insert checks for crashing inputs
to create M_pre in a non-iterative process. However, neither of these
approaches are effective in practice: the former does not guarantee
correctness, whereas the latter can result in a poor-quality test suite E. We
illustrate these issues in Section 4.4 and propose to address them by
inserting exception checks both iteratively and dynamically. In particular,
our algorithm interleaves program transformation and test generation in an
iterative process until convergence. Lastly, regardless of the algorithm, it
is not obvious how to design program transformations to guard against a
variety of crash types. For instance, it is unclear how to insert source
checks for interprocedural crashes.

##### Removing Irrelevant Computation

Upon lifting exception checks, our transformed precondition is correct modulo
the test generator. However, it contains many program segments which are
unrelated to the precondition. For illustration, consider the example from
Figure 1. Lines 4-24 are unrelated to the precondition. We present a dual
rationale for eliminating these segments. Firstly, we emphasize the importance
of removal for naturalness. To ensure that M_pre is conducive to human
reasoning it should not include program segments which are unrelated to the
precondition and incur additional cognitive load (Astorga et al., 2018).
Secondly, these extraneous segments might encompass statements or expressions
with side effects. A pure (i.e., side-effect free) precondition is desirable
in both ease of understanding and in tool usage. In tool usage, a precondition
with side effects must be run in a sandbox environment as to preserve the
state of the program being analyzed. The challenge of maintaining purity is
unique to our approach. Prior works have the benefit of ensuring purity by
construction. That is, their precondition features are designed to only
include observer methods which do not change the program state. The challenge
of removing irrelevant computation can be tackled in a number of ways, both
statically and dynamically. In Section 4 we describe a set of program
transformations we employ for efficient removal of irrelevant computation.

##  4\. Technique

In this section, we present the details of our general approach as well as our
instantiated framework. We describe the phases involved in inferring a
precondition through program transformation. We address sub-problems (1)
lifting implicit exception checks and (2) removing code irrelevant to the
precondition. Our overall technique, which comprises three main phases, is
illustrated in Figure 2. The initial source transformation phase, described in
Section 4.1, creates a seed for inference. This up-front transformation
retains the structure of M creating an initial boolean returning function
M_pre_i. The second phase, described in Section 4.2, is the main phase of
inference. It tackles sub-problem (1) by adding explicit checks in the source
of M_pre_i through an iterative transformation process. We present an
algorithm for program transformation detailing the process of iterative
covergage guided test generation and transformation. The last phase, described
in Section 4.3, tackles sub-problem (2) by leveraging a syntax-guided program
reducer. The final transformed program M_pre contains explicit exception
checks and does not contain irrelevant computation.

Figure 2. Overall architecture of our approach.

Each phase works in synergy benefiting from design choices made in other
phases. The seed generation phase localizes expressions for precise exception
check insertion and syntax-guided reduction. The second phase, benefits from
the first, and relies on the reducer’s (third phase) properties to remove
conservative checks. The reducer benefits from the previous phases as it
receives a M_pre with localized exception checks with a reducer-aware
structure. Ultimately, this results in a natural and correct precondition.
Lastly, in Section 4.4 we motivate the need for an iterative transformation
process by illustrating the incorrectness incurred through alternate
approaches presented in Section 3.

###  4.1. Seed Generation

Our overall technique begins by creating a seed through an up-front source
transformation on M. We begin with the method body and make transformations to
satisfy our problem formulation, requiring M_pre to be a non-exceptional,
boolean returning function. Furthermore, our seed generation process makes
semantics preserving transformations for precise exception check insertion and
syntax-guided reduction in later stages. Figure 3 illustrates the source
transformation on an example method Sqrt. The source transformation is
designed such that the seed has the following desirable qualities:

⬇

1BigInteger Sqrt() {

2 if (m_sign < 0)

3 throw new ArithmeticException();

4

5 return Round(Sqrt(this));

6}

(b) Target method M.

⬇

1boolean Sqrt_pre_init() {

2 if (m_sign < 0)

3 return false;

4

5 BigInteger var_a = Sqrt(this);

6 Round(var_a);

7 return true;

8}

(c) M after seed transformation.

Figure 3. Illustration of seed generation.

  1. (1)

The M_pre must be boolean returning:
We transform ${\tt M}$ to be a boolean returning function by modifying the
method signature and adding the statement return true at all exit points. If M
returns a type other than boolean, we maintain the original expression return
value by lifting it to an expression statement prior to the newly inserted
return statement. This is essential as the return expression in M itself may
be exceptional.

  2. (2)

The M_pre must be non-exceptional:
Our problem formulation requires M_pre to either return true or false,
implying that it exits normally on all inputs. At times, programmers will
explicitly guard against precondition violations, by explicitly throwing an
exception. For example, in Figure 2(b) an ArithmeticException is thrown on a
Zero input. To ensure the M_pre exits normally, we replace any throw
expression with a return false indicating an illegal input. Any implicitly
thrown exceptions are handled in phase two described in Section 4.2 and
illustrated in the dotted box in Figure 2.

  3. (3)

The M_pre localizes crashes:
One challenge described in Section 3 sub-problem (1) is in regards to
interprocedural crashes. In Section 4.2 we describe and motivate our approach
to tackle this through a predefined program transformation. In short, this
transformation amounts to wrapping an exceptional call in a try-catch block.
As a product of this transformation we perform call normalization on our seed.
The process of call normalization is essential for crash localization during
the next phase of transformation. The normalization transformation lifts each
call to its own source line. Call normalization ultimately results in a more
readable precondition. This is illustrated in Figure 4. Suppose Sqrt throws a
general type Exception on an input. Without call normalization, the final
M_pre is shown in Figure 3(a). It is not clear whether the exception is
occurring in the method Sqrt or the method Round. On the other hand,
performing call normalization (Figure 3(b)) localizes the exception in Sqrt.
By localizing the crash we reduce the cognitive load of interprocedural
inspection of the exceptional callee.

For localized crashes, intraprocedural crashes must also be considered.
Potentially exceptional expressions in loop conditions and updates must be
precisely guarded against. Consider the example in Figure 5 in which a
NullPointerException may potentially occur upon the field access on a. Without
normalization (Figure 4(b)), inserting a check prior to the loop declaration
does not guard against exceptions which may occur during loop execution. Since
taz() may return null, a guard prior to entry of the loop is not sufficient.
During seed generation, we normalize potentially exceptional expressions in
loop conditions (Figure 4(c)) such that guards can be precisely inserted
(Figure 4(d)) in the next phase of inference.

⬇

1public boolean Sqrt_pre() {

2 if (m_sign < 0)

3 return false;

4 try {

5 Round(Sqrt(this));

6 } catch (Exception e) {

7 return false;

8 }

9 return true;

10}

(a) M_pre without call normalization.

⬇

1public boolean Sqrt_pre() {

2 if (m_sign < 0)

3 return false;

4 try {

5 Sqrt(this);

6 } catch (Exception e) {

7 return false;

8 }

9 return true;

10}

(b) M_pre with call normalization.

Figure 4. Illustration of call normalization in seed generation.

⬇

1void foo(Object a) {

2 int i = 0;

3 while (i < a.bar)

4 a = taz(); //taz may return null

5 i += 1;

6 }

7

8}

(a) Exceptional loop condition.

⬇

1void foo_pre(Object a) {

2 int i =0;

3 if (a == null) return false;

4 while (i < a.bar)

5 a = taz(); //taz may return null

6 i += 1;

7 }

8}

(b) Incorrect exception check insertion.

⬇

1void foo(Object a) {

2 while (true)

3 if (i < a.bar) {

4 a = taz(); //taz may return null

5 } else {

6 break;

7 }

8 i += 1;

9 }

10

11}

(c) M after seed transformation.

⬇

1void foo_pre(Object a) {

2 while (true)

3 if (a == null) return false;

4 if (i < a.bar) {

5 a = taz(); //taz may return null

6 } else {

7 break;

8 }

9 i += 1;

10 }

11}

(d) Correct exception check insertion.

Figure 5. Illustration of intraprocedural normalization in seed generation.

We perform this initial source transformation up-front to create a seed M_pre
for our forthcoming phases. All transformations beyond the boolean returning
behavior are semantic preserving transformations.

###  4.2. Explicit Exception Check Insertion

In this section we describe our solution to sub-problem (1), lifting implicit
JVM exception checks to source level. We do this by iteratively interleaving
program transformation and test generation. This phase of our approach is
shown in the dotted box in Figure 2. It begins by operating on the seed
program $\texttt{M\\_pre}{}\\_i$. In order to discover feasible implicit
crashes, we invoke the test generator to obtain a set of tests, ${\tt
Tests}\\_i$. We then execute the tests and observe the stack trace(s) of all
crashing inputs. If crashing inputs do indeed exist in ${\tt Tests}\\_i$, then
the $\texttt{M\\_pre}{}\\_i$ should be transformed such that any crash instead
exits normally with a return value of false. To do so, we invoke the check
instrumentor which performs program transformations to satisfy this
formulation. The check instrumentor modifies the semantics of
$\texttt{M\\_pre}{}\\_i$ to produce an $\texttt{M\\_pre}{}\\_i+1$, by adding
checks (false returning if-statement guards) prior to any crash found by the
test generator. After transformation, we again invoke the test generator on
the newly produced $\texttt{M\\_pre}{}\\_i+1$ to yield a new set of tests
${\tt Tests}\\_i+1$. If this new set of tests contains new crashing inputs
which are not already guarded against, we continue in the loop and invoke the
check instrumentor to guard against any new crashes. We continue this
iterative process until convergence. That is, when we no longer observe
crashes during execution of the current ${\tt Tests}\\_i$. Upon convergence,
we are guaranteed to have a safe and maximal precondition, modulo the test
generator. In Section 4.4 we illustrate the need for such an iterative process
to produce correct and high quality preconditions.

##### Check Instrumentor.

Here, we describe the process for inserting false returning guards prior to
crashes found by the test generator. These are inserted such that the M_pre
will exit normally on an illegal input rather than throwing an exception. The
check instrumentor parses a stack trace produced from the execution of the
current tests ${\tt Tests}\\_i$. The stack trace provides a crash type and
location, which allows us to make precise AST transformations. By only
guarding against the given crash type at the given location, we maintain
maximality and do not reject any legal inputs. We categorize and design our
program transformations in a data-driven fashion. We define six
transformations which guard against 99% of the crashes the test generator
found on 87 real-world Java projects. Our technique performs AST
transformations according to the Algorithm 1. This algorithm works in synergy
with our seed generation as it expects localized statements to match the given
line number. The first transformation, on Lines 4-7, is performed when the
crash occurs in a callee of M. This amounts to wrapping the crashing call in a
try-catch block. The seed generation call normalization guarantees that $S$ is
a single method call to ensure precise localization. Lines 8-34 handle the
cases where the crash occurs directly in the target method. Here, the
statement on Line $L$ can contain multiple child expressions which are
iterated over in order of execution. Our algorithm similarly transforms the
program segment based on crash and expression types. For instance, given an
ArrayOutOfBoundsException crash type, the transformation on line 20 is
performed for each ArrayIndexExpression on line $L$. If multiple index
expressions are present as children of $S$, guards are conservatively added
for each. Working in synergy with the reducer, if the checks are unnecessary,
they will be removed in a later stage of the technique. The other four
transformation types follow similarly.

##### A Note on Interprocedural Wraps.

It is not obvious how to add explicit checks for crashes that occur within
callees in M. One possibility is to inline any calls. We experimented with
inlining method calls, but found it to lead to lower quality or equivalent
preconditions for two reasons. Firstly, inlining can quickly hit a library or
framework boundry where the source code is not included. Secondly, even when
all source is available, inlining often leads to potentially complex
precondition logic due to long call chains with large method bodies. Through a
manual inspection of 10 random samples from our dataset, we found that only
one sample benefited from inlining. Furthermore, we found that over 85% of the
exceptional callees in our dataset are at a source boundary and cannot be
inlined. For these reasons, we choose to handle exceptions in the callee by
wrapping the crashing call in a try-catch block.

Algorithm 1 Transformation to replace a crashing program fragment on Line L
with a new program fragment that guards the crashing exception type.

1:procedure CheckInstrumentorAlgorithm(Exception Type T, Line L, bool
isInCallee)

2: S $\leftarrow$ statement on line L

3: P $\leftarrow$ S

4: if isInCallee then $\triangleright$ Interprocedural Exception

5: P $\leftarrow$ try { S } catch (T exc) { return false; }

6: return;

7: end if

8: Let (expr_1, ..., expr_n) be the list of all expressions in S in the normal
order of execution

9: for $i=1:n$ do

10: switch T do

11: case java.lang.NullPointerException

12: if expr_i is a field access expression of the form object_expr.field then

13: P $\leftarrow$ if (object_expr == null) return false; P

14: end if

15: if expr_i is an array access expression of the form array_expr[index_expr]
then

16: P $\leftarrow$ if (array_expr == null) return false; P

17: end if

18: case java.lang.ArrayIndexOutOfBoundsException

19: if expr_i is an array access expression of the form array_expr[index_expr]
then

20: P $\leftarrow$ if (index_expr < 0 || index_expr >= array_expr.length)
return false; P

21: end if

22: case java.lang.ClassCastException

23: if expr_i is a class cast expression of the form (cast_type) expr_to_cast
then

24: P $\leftarrow$ if !(expr_to_cast instanceof cast_type) return false; P

25: end if

26: case java.lang.NegativeArraySizeException

27: if expr_i is an array creation expression of the form new
array_expr[index_expr] then

28: P $\leftarrow$ if (index_expr < 0) return false; P

29: end if

30: case java.lang.ArithmeticException

31: if expr_i is a binary operator DIVIDE expression of the form numer/denom
then

32: P $\leftarrow$ if (denom == 0) return false; P

33: end if

34: end for

35:end procedure

###  4.3. Removing Irrelevant Computation

Lastly, we wish to remove program components which are unrelated to the
precondition. This is an important step as it reduces cognitive load of
reasoning over the precondition and removes unrelated statements which
potentially have side effects. We consider a program segment to be unrelated
to the precondition if, when removed, the behavior of M_pre (modulo the test
generator) does not change. We formulate this sub-problem as program reduction
and leverage an off-the-shelf program reducer. A program reducer takes as
input a program to reduce and a set of constraints. It then outputs the
smallest sub-program which satisfies the given constraints. In our setting,
the constraint is maintaining the behavior of M_pre (every generated test must
pass). After the reduction phase, we have inferred a natural and correct
M_pre. We evaluate the impact of this reduction on the resulting preconditions
in Section 6.3.

###  4.4. Alternate Check Insertion Approaches

Lifting implicit exception checks requires much thought. It is not obvious
when and where to insert source checks. In this section, we describe two
alternate approaches and illustrate why an iterative, dynamic transformation
process is necessary for correctness and efficiency. We assume an equivalent
technique in terms of seed generation and transformation types in order to
draw attention to the necessity of iteration.

####  4.4.1. Exhaustive Up-Front Transformation.

One naive algorithm would be to exhaustively insert source checks at each
point which may throw an exception, prior to invoking $T$. All implicit JVM
checks would be lifted to explicit source checks regardless of if it is a
feasible crash (i.e. add a null pointer check before every field access). In
this section, we will illustrate that this approach is inefficient and can
even lead to incorrect preconditions. Consider the M, Decrement in Figure
5(a). Intuitively, it takes a val and subtracts one. The developers of the
method guarded against the case in which val is null through a try-catch
block. In the case of a null input, the program returns the BigInteger
representing -1. Assuming Sub (called on a non-null target) and the BigInteger
constructors always exit normally, Decrement is non-crashing and has a
precondition of true.

An exhaustive approach would analyze the field access on the call to Sub as a
potential Null Pointer Exception and insert a nullness check before the access
(Figure 5(b) even though the exception is not reachable. After the check is
inserted, $T$ is invoked. Since the $M\\_pre\\_i$ is non-exceptional, the test
generator outputs a test suite with only assertions on true or false return
behavior. Suppose the tests generated are shown in Figure 5(d). Program
reduction is invoked with this generated test suite as a correctness oracle.
Due to the eagerly inserted null check, the tests do not match our formulation
of M_pre as an input of null is legal but has a return value of false. So, the
program reducer removes segments to satisfy the incorrect behavior described
in the test suite. The resulting M_pre (Figure 5(d)) inferred through this
exhaustive up-front check insertion approach, is incorrect (non-maximal)
compared to our manually derived precondition as it rejects the non-
exceptional input val == null.

⬇

1BigInteger Decrement(BigInteger val) {

2

3 BigInteger One = BigInteger(1);

4

5 try {

6 return val.Sub(One);

7 } catch (NullPointerException e) {

8 return BigInteger(-1);

9 }

10

11}

(a) Target M.

⬇

1boolean M_pre_i(BigInteger val) {

2 BigInteger One = BigInteger(1);

3 try {

4 if (val == null)

5 return false;

6 val.Sub(One);

7 } catch (NullPointerException e) {

8 BigInteger(-1);

9 return true;

10 }

11}

(b) $\texttt{M\\_pre}{}\\_i$ with exhaustive checks.

⬇

1void test() {

2 boolean b1 = M_pre_i(null);

3 assertFalse(b1); //legal input!

4

5 boolean b2 = M_pre_i(BigInteger(1));

6 assertTrue(b2);

7}

(c) Tests for $\texttt{M\\_pre}{}\\_i$.

⬇

1boolean M_pre(BigInt val) {

2 if (val == null)

3 return false;

4 return true;

5}

(d) Resulting M_pre.

Figure 6. Alternate Approach 1: Up-front exhaustive guard insertion.

##### Single Step Non-Iterative Test Generation and Transformation.

Here we detail the second alternate algorithm presented in Section 3. This
approach involves a single step non-iterative process. In this approach, $T$
is invoked once on the seed program to obtain a suite of tests. As in our
algorithm, tests are executed and the Check Instrumentor is invoked to insert
guards parsed from the stack trace, creating $M\\_pre\\_1$. In contrast to our
approach, after Check Instrumentation, $T$ is not invoked again. Instead, the
reducer is invoked on $M\\_pre\\_1$. Due to coverage guided nature of test
generation, we show that an iterative process obtains a higher coverage, more
robust test suite.

To illustrate the problems with a two-step process, we use a sample from our
real-world datasest (Figure 7) which required multiple iterations to find new
exceptional inputs. In a single step process, we begin with the seed program
in Figure 6(a) and invoke $T$ to find the crashing input y == null. After
executing the test and parsing the stack trace, we insert a null checking
guard prior to the field access on y to create $M\\_pre\\_1$ (Figure 6(b)). In
this alternate non-iterative process, no additional rounds of test generation
would occur, and $M\\_pre\\_1$ would be fed to the program reducer. The
following two Sub-figures 6(c) and 6(d) illustrate the additional checks that
are inserted when we continue to invoke the test generator until convergence.
By only invoking $T$ as a single non-active step, we do not find the crashes
in diff and redateBy, leading to a lower quality precondition which does not
guard against illegal inputs. In Section 6 we evaluate the empirical advantage
of multiple iterative steps.

In summary, inserting exception checks both iteratively and dynamically is
necessary to guarantee correctness. Furthermore, inserting exception checks on
demand creates higher quality preconditions by driving the test generator to
progressively higher coverage inputs. This allows for the discovery of
additional crashes and insertion of corresponding explicit checks. We quantify
the number of iterations before convergence in section 6. An iteration number
greater than 1 is evidence that a single-step approach is not sufficient for
inferring high quality preconditions.

⬇

1boolean M_pre(Year y) {

2 int var_a = y.diff(this.end);

3 redateBy(var_a);

4 return false;

5}

(a) Seed Program.

⬇

1boolean M_pre(Year y) {

2 if (y == null) return false;

3 int var_a = y.diff(this.end);

4 redateBy(var_a);

5 return false;

6}

(b) M_pre_1.

⬇

1boolean M_pre(Year y) {

2 if (y == null) return false;

3 int var_a;

4 try {

5 var_a = y.diff(this.end);

6 } catch (NullPointerException e) {

7 return true;

8 }

9

10 redateBy(var_a);

11

12

13

14 return false;

15}

(c) M_pre_2 requiring 2 steps.

⬇

1boolean M_pre(Year y) {

2 if (y == null) return false;

3 int var_a;

4 try {

5 var_a = y.diff(this.end);

6 } catch (NullPointerException e) {

7 return true;

8 }

9 try {

10 redateBy(var_a);

11 } catch (NullPointerException e) {

12 return true;

13 }

14 return false;

15}

(d) M_pre_3 requiring 3 steps.

Figure 7. Alternate Approach 2: Single-step non-iterative test generation.

##### Framework Instantiation Details.

In our framework, we instantiate the test generator as EvoSuite (Fraser and
Arcuri, 2011) and leverage the Javaparser (jav, [n. d.]) library to perform
AST transformations. We instantiate the reducer as Perses (Sun et al., 2018),
as we experimented with the C-Reduce (Regehr et al., 2012) program reducer but
found it to be time-inefficient as it considers syntactically invalid sub-
programs in the search space.

##  5\. Comparative Case Study

In this section, we perform an in-depth comparative evaluation to the state-
of-the-art approach on a single real-world project. Here, we evaluate and
compare the resulting preconditions inferred by both approaches on two
aspects. We aim to answer the following research questions:

  1. RQ1

Correctness: Are the inferred preconditions safe and maximal?

  2. RQ2

Naturalness: Can humans easily reason over the inferred preconditions?

###  5.1. Experimental Setup

Baseline. We evaluate in comparison to Proviso(Astorga et al., 2019) as it is
the state-of-the-art and instantiated in C# which is most similar to our
target language.
Benchmark. We evaluate on 39 $({\tt M},\texttt{M\\_pre}{})$ pairs from the
NetBigInteger C# project. Although our framework is designed for Java, we
choose NetBigInteger as a common benchmark to compare to Proviso(Astorga et
al., 2019). In order to evaluate our technique, we manually translate the
NetBigInteger class to a semantically equivalent class in Java. Although
Proviso evaluates on 5 projects, 3 are synthetically constructed benchmarks,
and 2 are real-world. We select a single project to evaluate on as manual
effort is required in inspection and semantically equivalent conversion to
Java. As such, we perform an in-depth evaluation on this single project.

###  5.2. RQ1: Correctness

Following the definition of correctness in (Astorga et al., 2019), we evaluate
the safety and maximally of our inferred preconditions on the benchmark,
modulo a test generator. For a rigorous evaluation, we evaluate correctness
modulo the industrial test generator, Pex (Tillmann and de Halleux, 2008). By
instantiating $T$ with a differing tool from the $T$ used in our technique
(EvoSuite), we perform a higher quality evaluation as Pex has a fundamentally
different input generation algorithm, and will likely produce differing
inputs. We invoke Pex on M to generate crashing and non-crashing inputs. If
Pex can generate an invalid input for which M_pre returns true, we consider
M_pre to be unsafe. If Pex generates a valid input for which M_pre returns
false, we consider M_pre to be non-maximal. If a precondition is both safe and
maximal, we consider it to be correct. We perform this evaluation for the 39
M_pres inferred by our approach. For Proviso, we use the correctness results
reported (pro, [n. d.]). We find that our inferred preconditions are safe for
33 methods, maximal for 29 methods, and both safe and maximal for 29 of the 39
methods. In comparison, Proviso’s preconditions are safe for 37 methods,
maximal for 34 methods, and both safe and maximal for 34 methods. Through
manual inspection, we find that the 10 incorrect M_pre our approach infers are
due to EvoSuite incompleteness.

Result 1: Our approach infers correct (both safe and maximal) preconditions
for 29 of the 39 methods in the benchmark. The 10 incorrect preconditions were
due to EvoSuite incompleteness.

###  5.3. RQ2: Naturalness

In this section, we evaluate the naturalness of our preconditions. To better
understand if our inferred preconditions are natural, we study a human’s
ability to reason over its behavior. We evaluate and compare to Proviso, by
conducting a user evaluation. Each user is asked to review a given
precondition and three inputs. We ask the user to classify each input as legal
or illegal. The accuracy of their answers as well as the time taken to derive
the answer are metrics of how natural or easy the precondition is to reason
over.

##### User Study Design

We identify 5 preconditions from our comparative evaluation to use filtered by
the following criteria:

  1. (1)

Both our approach and Proviso infer a correct precondition.

  2. (2)

The precondition inferred by the tools are syntactically different.

  3. (3)

The precondition is non-trivial (there exists at least 1 illegal and 1 legal
input).

We split participants into two groups. Group A was presented with our
preconditions while Group B was presented with the preconditions inferred by
Proviso. The inputs for each precondition remained the same across both
groups. For illustration, we include one of the (precondition, input) pairs
from our study. Figure 8 shows an input given to Group A, while Figure 9 shows
one of the inputs given to Group B. We include any necessary code context for
completing the task. For brevity, we only show a single input, but each user
was presented with three inputs for each precondition. The user was asked to
classify each input as True or False (legal or illegal).

⬇

1Input:

2

3value: NetBigInteger target: NetBigInteger

4\--------------------- \-----------------------------------------

5m_sign: int = -25 m_sign: int = 25

6m_magnitude: int[] = {0, 0, 0, 0, 0, 0} m_magnitude: int[] = {0, 0, 0, 0, 0,
0}

7\-----------------------------------------
\-----------------------------------------

⬇

1boolean M_pre(NetBigInteger value) {

2 if (m_sign == 0)

3 return true;

4 if (value == null)

5 return false;

6 return true;

7}

Figure 8. Precondition 3, Input 2, Group A.

⬇

1Input:

2

3value: NetBigInteger target: NetBigInteger

4\--------------------- \-----------------------------------------

5m_sign: int = -25 m_sign: int = 25

6m_magnitude: int[] = {0, 0, 0, 0, 0, 0} m_magnitude: int[] = {0, 0, 0, 0, 0,
0}

7\-----------------------------------------
\-----------------------------------------

⬇

1Precondition:

2

3(

4 (value == null)

5 and (

6 (not (target.getSignValue() <= -1))

7 and

8 ((target.getSignValue() <= 0))

9 )

10) or (

11 (not (value == null))

12)

⬇

1Context:

2

3

4

5int getSignValue() {

6 return m_sign;

7}

8

9

10

11

12.

Figure 9. Precondition 3, Input 2, Group B.

##### Protocol

The user study was conducted through a Qualtrics survey. We used fine grained
timing for each participant. To reduce cognitive load, participants were
randomly presented with three out of the five preconditions, using qualtrics
randomization feature. Our survey included a ‘‘Don’t Know’’ option to avoid
random guessing. Any participant which selected ‘‘Don’t Know’’ was not
included in our results. The resulting valid participants comprised of 22
users including computer science PhD students, undergraduates, and industry
software engineers split evenly between the two groups.

##### User Study Results

On average, we found that users were able to more accurately reason over our
preconditions in a shorter amount of time. Participants of Group A had an
average accuracy of 92.9% while participants in Group B made more mistakes
leading to a lower average accuracy of 85.6%. In terms of speed of reasoning,
participants in Group A took an average total time of 109 seconds.
Participants in Group B took double the amount of time to complete the study
(217 seconds). Our results show that Preconditions 1 and 3 inferred by our
approach were significantly easier to reason over in terms of both accuracy
and speed. Precondition 4 had comparable results from both groups. However, on
Preconditions 2 and 5, results were still superior, but weaker. On
Precondition 2, Group A achieved higher accuracy, but took more than 2x the
average time as Group B (176.32 seconds vs 72.10 seconds). On Precondition 5,
Group A achieved only slightly higher accuracy (only 3.17% difference), but
took a shorter amount of time than Group B. Preconditions 2 and 5 were the
only samples in our study which included try-catch blocks, and thus,
interprocedural reasoning. This indicates that although our preconditions are
on average, easier to reason over, future research should address the
additional cognitive load and lower level of naturalness due to
interprocedural crashes. We include all five preconditions from both groups A
and B in this paper. Precondition 1 is shown in Figure 1, Precondition 3 is
shown in Figures 8 and 9, and we include Precondition 2 (Figure 10),
Precondition 4 (Figure 11), and Precondition 5 (Figure 11(a)) in the appendix.

Result 2: On average, users were able to more accurately reason over our
preconditions in a shorter time span. Participants of Group A had an average
accuracy of 92.86% while participants in Group B committed more errors,
leading to a lower average accuracy of 85.61%. In terms of speed of reasoning,
participants in Group A completed the task with an average total duration of
109.52 seconds. Participants in Group B took twice as long (217.06 seconds) to
finish the study. Our results were not as strong on preconditions which
included interprocedural try-catch blocks.

| Accuracy | Time Taken (Sec)
---|---|---
| Ours | Proviso | Ours | Proviso
Precondition 1 | 100% | 88.89% | 43.18 | 271.49
Precondition 2 | 88.33% | 76.19% | 176.32 | 72.10
Precondition 3 | 100% | 85.19% | 77.08 | 367.46
Precondition 4 | 100% | 100% | 48.31 | 62.92
Precondition 5 | 80.95% | 77.78% | 202.73 | 311.34
Overall | 92.86% | 85.61% | 109.52 | 217.06
Table 1. User study results.

##  6\. Design Decision Evaluation On a Large Scale Dataset

In this section, we evaluate the design decisions of our technique at scale.
We aim to evaluate our technique’s design decisions in both sub-problems.
First, we evaluate our choice of iterative, dynamic, exception check insertion
over the two-step approach presented in Section 4.4.1. It is difficult to
evaluate exhaustive up-front transformation approach presented in Section
4.4.1 since our definition of correctness is modulo a test generator. For
this, we default to an illustrative example by contradiction of correctness in
Figure 6. Secondly, we motivate and evaluate our solution to removing
irrelevant program segments in terms of complexity. To do so, we gather a
substantial dataset of real-world Java preconditions and answer the following
research questions:

  1. RQ1

How do different choices of the explicit exception insertion algorithm impact
the quality of test suite and resulting precondition?

  2. RQ2

How does removing irrelevant program segments affect the resulting
precondition in terms of complexity?

###  6.1. Experimental Setup: Benchmark

We evaluate on a large scale dataset we’ve constructed of Java methods from
popular, stable, projects. Our dataset consists of 17,871
$(\texttt{M}{},\texttt{M\\_pre}{})$ pairs inferred from 87 projects. The
projects are from the SF100 (Fraser and Arcuri, 2013) with an additional 13
projects popular projects from the Maven repository 111The projects were
collected in order of number of downloads as of April 2022.. In order to
provide further insight into our benchmark, we present the following
characteristics of our dataset:

| Number | Percent
---|---|---
non-trivial | 6,790 | 37.99%
true | 10,791 | 60.38%
false | 290 | 1.62%
Total | 17,871
(a) Overall Precondition Categorization.

Crash Type | # of Checks
---|---
Intraprocedural Exception | 8,079
NullPointerException | 5,535
ArrayIndexOutOfBoundsException | 793
ClassCastException | 443
NegativeArraySizeException | 65
ArithmeticException | 17
Overall | 14,932
(b) Breakdown by Crash Type.

Table 2. Dataset statistics.

##### Crash Occurrence:

Since our dataset is real-world and diverse, it contains methods which accept
all inputs, reject all inputs, or have a non-trivial precondition which
accepts some inputs and rejects others. We characterize the dataset, in Table
9(a) by the precondition "type". In our dataset, more than half of the methods
have a precondition of true indicating that any input is legal. A small
percentage, ($\sim$1%) of samples are always exceptional and have a
precondition of false. Through manual inspection, we find these methods
typically contain a single explicit throws expression. For example, a method
with a body of: throw new UnsupportedOperationException would always be
exceptional and have a precondition of false. The remaining samples,
($\sim$40%), are non-trivial in that there exists at least one legal input and
one illegal input.

##### Crash Types:

EvoSuite found a diverse set of crashes which fit into the 6 crash type
categories presented in Section 4.2. In Table 9(b), we present the total
number of explicit exception checks inserted and the occurrence of each type.
These checks were dynamic lifted to explicit guards by the Check Instrumentor
and were not present in the source of M. Nearly 15,000 checks were added
through program transformation. This emphasizes the need for a dynamic tester
to find crashing inputs rather than being able to parse out explicit checks as
in Figure 1 line 3. We also note that over half of crashes found by EvoSuite
occurred in a callee, indicating a potential fruitful research direction in
natural precondition inference.

##### Defensive Checks:

Here, we ask, how often do developers explicitly guard for precondition
violations? This is in converse to the previous characterization in that we
study only the checks which were included in the untransformed M. Through this
study, we motivate the necessity of a dynamic tester to find legal and illegal
inputs beyond the explicitly written exceptions. Previous approaches have
attempted to statically create such a dataset of preconditions through
parsing. One static parsing approach (Hellendoorn et al., 2020) attempts to
generate a dataset of invariants. The authors do this by considering an if-
statement’s guard condition to be an invariant of the guarded block. Although
they were able to collect these invariants on a large scale (2.5 million
invariants), such a dataset cannot capture implicit specifications that are
not expressed directly in if conditions. Although our setting is slightly
different in that we are collecting preconditions rather than invariants, the
approach still stands as a naive evaluation.

Through an AST walk over the target methods in our dataset we find 1,451
explicitly coded illegal input guards. This, in conjunction with the nearly
15,000 implicit crashes found shows that high quality preconditions cannot be
constructed by simple scraping of if conditions. It also indicates that
developers do not sufficiently guard against illegal inputs

We find that only 1,451 guards were explicitly written by developers. The
remaining 14,932 crashes were not explicitly guarded against and were found by
EvoSuite.

###  6.2. RQ1: Impact of Iterative Dynamic Check Insertion

Here, we aim to answer RQ1 using the dataset presented above. In Section 4.4
we illustrated the necessity for an iterative approach to produce a high
quality test suite. Here, we quantitatively motivate it on a large scale. We
measure the number of samples which required iteration. That is, the number of
samples for which EvoSuite finds new crashing inputs when it is invoked on
$M\\_pre\\_1$ which includes inserted checks. We find that 2,198 samples
required additional iterations beyond a single step process. This amounts to
32.37% of our non-trivial samples. During the inference of these 2k samples,
they required on average, 1.73 additional iterations (beyond the initial
step). In total, 4,517 additional crashes were found due to additional
iterations.

Result 1: We find that over 1/3rd of non-trivial samples require additional
iterations beyond a single step (test and transform) approach. A total of
4,517 additional crashes were found due to the iterative approach.

###  6.3. RQ2: Impact of Program Reduction

In this section, we evaluate the effect of removing irrelevant computation.
The goal of removing irrelevant program segments is to reduce cognitive load
and remove unrelated statements which potentially have side effects. In short,
program reduction should reduce complexity. We evaluate this along three axis:
number of program paths, precondition size, and purity. For each axis, we
compare the unreduced M_pre (post-instrumentation) to the reduced M_pre.

##### Cyclometic Complexity.

In order to quantify the complexity of a precondition’s control flow, we
measure the cyclomatic complexity (McCabe, 1976) using checkstyle (che, [n.
d.]). The average cyclometic complexity of an unreduced sample is 2.86. After
reduction, the complexity drops to 1.77. This shows the computational load is
reduced by around one path through program reduction. For non-trivial samples
with at least one illegal and one legal input, the average complexity is 4.99
and drops to 2.46 after reduction. For this sub-class of samples, complexity
is more significantly lowered through reduction.

##### Precondition Size.

In order to quantify a precondition’s size, we measure the number of AST
nodes. The average number of unreduced nodes is 56.27 and the average number
of AST nodes in the reduced sample is 15.41 This shows that we removed around
1/3 of the AST nodes through program reduction, greatly reducing computational
load of a consumer of the precondition.

##### Purity.

Ideally, a precondition should not have side effects. Impure statements
increase cognitive load, forcing the consumer to reason about state, and add
complications for precondition execution during software testing. We measure
the number of samples which are impure pre-reduction, but pure post-reduction
to quantify impact of program reduction on side effects. To do so, we use the
Facebook Infer (Distefano et al., 2019) purity checker. We find that only
50.63% of pre-reduction samples are pure, while 81.3% post-reduction samples
do not contain side effects. This demonstrates the impact of reduction on the
purity of inferred preconditions.

Result 2: We find that by employing a program reducer we produce preconditions
which are of lower complexity, smaller, and display a higher level of purity.
Cyclometic complexity drops by around 1 program path after reduction. For non-
trivial samples, this is more significant, with reduction lowering complexity
by half. The number of AST nodes is reduced by 1/3rd. Post reduction, there is
a 60% increase in number of pure samples. This motivates the use of program
reduction across three axis of complexity.

##  7\. Limitations

Our approach, like many other precondition inference techniques, is limited by
program analysis capabilities. Firstly, our approach heavily relies on the
target method implementation. If the source code is not available, or does not
compile and execute, then our technique cannot infer a precondition. Likewise,
if the method has a bug related to the precondition, it may be inherited in
the resulting M_pre.

Secondly, while instantiating our technique as a tool, we found that program
analysis tools are very brittle. We applied our technique at scale on a total
of 126,699 methods and only obtained 17,868 $({\tt M},\texttt{M\\_pre}{})$
pairs ($\sim$14% of the target methods). The methods we could not extract
preconditions for failed due to limitations of the program analysis tools in
our pipeline. Failures largely occurred due to automated testing challenges in
EvoSuite. For example, EvoSuite often could not generate a well-formed object
as a target for M. EvoSuite struggled to generate test suites in some cases
due to resource limits, I/O and file system mocking, concurrency, and missing
environment dependencies (Fraser and Arcuri, 2013).

A limitation unique to our approach is the possibility of side effects. Since
our approach relies on the structure and program segments that appear in the
original M, there is no guarantee that the precondition we produce is pure. In
practice, we find that most preconditions infer are pure in nature. Although,
if purity is critical, a purity checker such as FBInfer (Distefano et al.,
2019) can be invoked to avoid the rare case where the method’s precondition
has side effects.

##  8\. Conclusion

We have presented a novel approach for inferring natural preconditions through
program transformations over the target method. Our findings reveal that the
preconditions inferred by our approach are more easily reasoned over by humans
than template based tools which build the precondition from scratch. Looking
ahead, the potential of natural preconditions extends to diverse applications
such as serving as training data or integrating with large language models.
This exciting direction is underscored by the promising advancements in the
realm of program specification representations as evidenced in (Odena and
Sutton, 2020), along with the high accuracy demonstrated by large language
models in inferring Daikon invariants, as showcased in (Sutton et al., 2023).
The concept of natural preconditions is in alignment with the evolving
landscape of statistical software engineering tools, especially within the
domain of large language models. As this synergy continues to unfold, we
anticipate implications for the future of software correctness.

## References

  * (1)
  * che ([n. d.]) [n. d.].  checkstyle CyclomaticComplexity.  https://checkstyle.sourceforge.io/checks/metrics/cyclomaticcomplexity.html.
  * cla ([n. d.]) [n. d.].  Clang Static Analyzer - Cross Translation Unit (CTU) Analysis.  https://clang.llvm.org/docs/analyzer/user-docs/CrossTranslationUnit.html.
  * jav ([n. d.]) [n. d.].  JavaParser.  https://github.com/javaparser/javaparser.
  * pro ([n. d.]) [n. d.].  Proviso Preconditions Results.  https://sites.google.com/site/learnprecond/.  Accessed: 2023-08-23.
  * Astorga et al. (2019) Angello Astorga, P. Madhusudan, Shambwaditya Saha, Shiyu Wang, and Tao Xie. 2019.  Learning Stateful Preconditions modulo a Test Generator. In _Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Phoenix, AZ, USA) _(PLDI 2019)_. Association for Computing Machinery, New York, NY, USA, 775–787.  https://doi.org/10.1145/3314221.3314641
  * Astorga et al. (2018) Angello Astorga, Siwakorn Srisakaokul, Xusheng Xiao, and Tao Xie. 2018.  PreInfer: Automatic Inference of Preconditions via Symbolic Analysis. In _2018 48th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)_. 678--689.  https://doi.org/10.1109/DSN.2018.00074
  * Chandra et al. (2009) Satish Chandra, Stephen J. Fink, and Manu Sridharan. 2009\.  Snugglebug: A Powerful Approach to Weakest Preconditions.  _SIGPLAN Not._ 44, 6 (jun 2009), 363–374.  https://doi.org/10.1145/1543135.1542517
  * Cousot et al. (2013) Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Francesco Logozzo. 2013.  Automatic Inference of Necessary Preconditions. In _in Proceedings of the 14th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’13)_ (in proceedings of the 14th conference on verification, model checking and abstract interpretation (vmcai’13) ed.). Springer Verlag.  https://www.microsoft.com/en-us/research/publication/automatic-inference-of-necessary-preconditions/
  * Cousot et al. (2011) Patrick Cousot, Radhia Cousot, and Francesco Logozzo. 2011\.  Precondition Inference from Intermittent Assertions and Application to Contracts on Collections. In _Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation_ (Austin, TX, USA) _(VMCAI’11)_. Springer-Verlag, Berlin, Heidelberg, 150–168.
  * Distefano et al. (2019) Dino Distefano, Manuel Fähndrich, Francesco Logozzo, and Peter W. O’Hearn. 2019.  Scaling Static Analyses at Facebook.  _Commun. ACM_ 62, 8 (jul 2019), 62–70.  https://doi.org/10.1145/3338112
  * Ernst et al. (2007) Michael D Ernst, Jeff H Perkins, Philip J Guo, Stephen McCamant, Carlos Pacheco, Matthew S Tschantz, and Chen Xiao. 2007.  The Daikon system for dynamic detection of likely invariants.  _Science of computer programming_ 69, 1-3 (2007), 35--45.
  * Fava et al. (2016) Daniel Fava, Dan Shapiro, Joseph Osborn, Martin Schäef, and E. James Whitehead. 2016.  Crowdsourcing Program Preconditions via a Classification Game. In _Proceedings of the 38th International Conference on Software Engineering_ (Austin, Texas) _(ICSE ’16)_. Association for Computing Machinery, New York, NY, USA, 1086–1096.  https://doi.org/10.1145/2884781.2884865
  * Fraser and Arcuri (2011) Gordon Fraser and Andrea Arcuri. 2011.  Evolutionary Generation of Whole Test Suites. In _International Conference On Quality Software (QSIC)_. IEEE Computer Society, Los Alamitos, CA, USA, 31--40.  https://doi.org/10.1109/QSIC.2011.19
  * Fraser and Arcuri (2013) Gordon Fraser and Andrea Arcuri. 2013.  EvoSuite: On the Challenges of Test Case Generation in the Real World. In _2013 IEEE Sixth International Conference on Software Testing, Verification and Validation_. 362--369.  https://doi.org/10.1109/ICST.2013.51
  * Godefroid et al. (2005) Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005\.  DART: directed automated random testing. In _Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005_ , Vivek Sarkar and Mary W. Hall (Eds.). ACM, 213--223.  https://doi.org/10.1145/1065010.1065036
  * Hellendoorn et al. (2020) Vincent Josua Hellendoorn, Premkumar Devanbu, Alex Polozov, and mark marron. 2020.  Learning to Infer Run-Time Invariants from Source code. In _NeurIPS 2020 Workshop on Computer-Assisted Programming_.  https://openreview.net/forum?id=AiJ2UxYE4cQ
  * Hellendoorn et al. (2019) Vincent J. Hellendoorn, Premkumar T. Devanbu, Oleksandr Polozov, and Mark Marron. 2019.  Are My Invariants Valid? A Learning Approach.  _CoRR_ abs/1903.06089 (2019).  arXiv:1903.06089 http://arxiv.org/abs/1903.06089
  * Hindle et al. (2012) Abram Hindle, Earl T. Barr, Zhendong Su, Mark Gabel, and Premkumar Devanbu. 2012.  On the Naturalness of Software. In _Proceedings of the 34th International Conference on Software Engineering_ (Zurich, Switzerland) _(ICSE ’12)_. IEEE Press, 837–847.
  * Leino (2010) Rustan Leino. 2010\.  Dafny: An Automatic Program Verifier for Functional Correctness. In _16th International Conference, LPAR-16, Dakar, Senegal_ (16th international conference, lpar-16, dakar, senegal ed.). Springer Berlin Heidelberg, 348--370.  https://www.microsoft.com/en-us/research/publication/dafny-automatic-program-verifier-functional-correctness-2/
  * McCabe (1976) T.J. McCabe. 1976\.  A Complexity Measure.  _IEEE Transactions on Software Engineering_ SE-2, 4 (1976), 308--320.  https://doi.org/10.1109/TSE.1976.233837
  * Odena and Sutton (2020) Augustus Odena and Charles Sutton. 2020.  Learning to Represent Programs with Property Signatures.  _CoRR_ abs/2002.09030 (2020).  arXiv:2002.09030 https://arxiv.org/abs/2002.09030
  * Pacheco et al. (2007) Carlos Pacheco, Shuvendu K. Lahiri, Michael D. Ernst, and Thomas Ball. 2007.  Feedback-directed random test generation. In _ICSE 2007, Proceedings of the 29th International Conference on Software Engineering_. Minneapolis, MN, USA, 75--84.
  * Padhi et al. (2016) Saswat Padhi, Rahul Sharma, and Todd Millstein. 2016\.  Data-Driven Precondition Inference with Learned Features.  _SIGPLAN Not._ 51, 6 (jun 2016), 42–56.  https://doi.org/10.1145/2980983.2908099
  * Regehr et al. (2012) John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison, and Xuejun Yang. 2012\.  Test-Case Reduction for C Compiler Bugs. In _Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Beijing, China) _(PLDI ’12)_. Association for Computing Machinery, New York, NY, USA, 335–346.  https://doi.org/10.1145/2254064.2254104
  * Sankaranarayanan et al. (2008) Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivancic, and Aarti Gupta. 2008.  Dynamic inference of likely data preconditions over predicates by tree learning. In _Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008, Seattle, WA, USA, July 20-24, 2008_ , Barbara G. Ryder and Andreas Zeller (Eds.). ACM, 295--306.  https://doi.org/10.1145/1390630.1390666
  * Seghir and Kröning (2013) Mohamed Nassim Seghir and Daniel Kröning. 2013.  Counterexample-Guided Precondition Inference. In _Proceedings of the 22nd European Symposium on Programming_ _(Lecture Notes in Computer Science, Vol. 7792)_ , Matthias Felleisen and Philippa Gardner (Eds.). Springer International Publishing, 451--471.  https://doi.org/10.1007/978-3-642-37036-6_25
  * Sun et al. (2018) Chengnian Sun, Yuanbo Li, Qirun Zhang, Tianxiao Gu, and Zhendong Su. 2018.  Perses: Syntax-Guided Program Reduction. In _Proceedings of the 40th International Conference on Software Engineering_. Association for Computing Machinery, 361–371.  https://doi.org/10.1145/3180155.3180236
  * Sutton et al. (2023) Charles Sutton, David Bieber, Kensen Shi, Kexin Pei, and Pengcheng Yin. 2023.  Can Large Language Models Reason About Program Invariants?
  * Sutton (1995) S. M. J Sutton. 1995\.  _Preconditions, Postconditions, and Provisional Execution in Software Processes_.  Technical Report. USA.
  * Tillmann and de Halleux (2008) Nikolai Tillmann and Peli de Halleux. 2008.  Pex - White Box Test Generation for .NET. In _Proc. of Tests and Proofs (TAP’08)_ (proc. of tests and proofs (tap’08) ed.) _(LNCS, Vol. 4966)_. Springer Verlag, 134--153.  https://www.microsoft.com/en-us/research/publication/pex-white-box-test-generation-for-net/
  * Xie and Aiken (2005) Yichen Xie and Alex Aiken. 2005.  Saturn: A SAT-Based Tool for Bug Detection. In _Proceedings of the 17th International Conference on Computer Aided Verification_ (Edinburgh, Scotland, UK) _(CAV’05)_. Springer-Verlag, Berlin, Heidelberg, 139–143.  https://doi.org/10.1007/11513988_13
  * Yun et al. (2016) Insu Yun, Changwoo Min, Xujie Si, Yeongjin Jang, Taesoo Kim, and Mayur Naik. 2016\.  APISan: Sanitizing API Usages through Semantic Cross-Checking. In _25th USENIX Security Symposium (USENIX Security 16)_. USENIX Association, Austin, TX, 363--378.  https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/yun
  * Zhai et al. (2020) Juan Zhai, Yu Shi, Minxue Pan, Guian Zhou, Yongxiang Liu, Chunrong Fang, Shiqing Ma, Lin Tan, and Xiangyu Zhang. 2020.  C2S: Translating Natural Language Comments to Formal Program Specifications. In _Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering_ (Virtual Event, USA) _(ESEC/FSE 2020)_. Association for Computing Machinery, New York, NY, USA, 25–37.  https://doi.org/10.1145/3368089.3409716

##  9\. Appendix

⬇

1Precondition:

2

3boolean M_pre(NetBigInteger value) {

4 try {

5 CompareTo(value);

6 } catch (NullPointerException e) {

7 return false;

8 }

9 return true;

10}

(c) Precondition 2, Group A

⬇

1Context:

2

3int CompareTo(NetBigInteger value) {

4 return m_sign < value.m_sign ? -1 :

5 m_sign > value.m_sign ? 1 :

6 m_sign == 0 ? 0 :

7 m_sign * CompareNoLeadingZeroes(0, m_magnitude,

8 0, value.m_magnitude);

9}

10.

(d) Context 2, Group A

⬇

1((not (value == null)))

(e) Precondition 2, Group B.

Figure 10. Precondition 2.

⬇

1boolean M_pre(NetBigInteger m) {

2 if (m == null)

3 return false;

4 if (m.m_sign < 1)

5 return false;

6 return true;

7}

(a) Group A.

⬇

1(not (m == null)) and (not (m.m_sign <= 0))

(b) Group B.

Figure 11. Precondition 4.

⬇

1Precondition:

2

3boolean M_pre(NetBigInteger value) {

4 if (value == null)

5 return false;

6 if (m_sign == 0)

7 return true;

8 NetBigInteger r;

9 NetBigInteger u = this;

10 NetBigInteger v = value;

11 while (v.m_sign != 0) {

12 try {

13 r = u.Mod(v);

14 } catch (ArithmeticException e) {

15 return false;

16 }

17 v = r;

18 }

19 return true;

20}

(a) Precondition 5, Group A.

⬇

1Context:

2

3

4

5

6

7

8NetBigInteger Mod(NetBigInteger m) {

9 if (m.m_sign < 1)

10 throw new ArithmeticException("Modulus must be positive");

11 NetBigInteger biggie = Remainder(m);

12 return (biggie.m_sign >= 0 ? biggie : biggie.Add(m));

13}

14

15

16

17

18

19

20.

(b) Context 5, Group A.

⬇

1((not (value == null)) and (not (target == null)))

2and (

3 (-target.m_sign + -value.m_sign <= 1) and (

4 (not (-target.m_sign + value.m_sign <= -2))

5 )

6)

(c) Precondition 5, Group B.

Figure 12. Precondition 5.