Dynamic Invariant Generation and Nonlinear Properties

Automatically inferring invariant specifications has proven valuable in enabling a wide range of software verification and validation approaches over the past two decades. Recent approaches have shifted from using observation of concrete program states to exploiting symbolic encodings of sets of concrete program states in order to improve the quality of inferred invariants.

In this work, we demonstrate that working directly with symbolic states generated by symbolic execution approaches can improve invariant inference further. Our technique uses a counterexample-based algorithm that iteratively creates concrete states from symbolic states, infers candidate invariants from both concrete and symbolic states, and then validates or refutes candidate invariants using symbolic states. The refutation process serves both to eliminate spurious invariants and to drive the inference process to produce more precise invariants. This framework can be employed to infer complex invariants that capture nonlinear polynomial relations among program variables.

The open-source DIG; tool implements these ideas to automatically generate invariants at arbitrary locations in Java or C programs. Our results show that across a collection of four benchmarks DIG; improves on the state-of-the-art by efficiently inferring more informative invariants than prior work.

Program Invariants, Numerical Invariants, Dynamic Analysis, Symbolic Execution, CounterExample Guided Refinement, Program Testing and Verification

The expressive power of programs lies in their ability to concisely represent repeated sub-computations that arise due to iteration or recursion. Developing software that correctly orchestrates those sub-computations is challenging as programmers learn when they study even basic sorting algorithms. Classic approaches for defining, and understanding, the correctness of such algorithms rely on specification of \emph{program invariants} which define relationships that must hold between program variables at a given location in the program~\cite{hoare1969axiomatic,cormen2009introduction,hoare1971proof}.

While invariants play a role in educating programmers about complex algorithms, they also offer the potential to improve programming practice. Research has demonstrated how invariant specifications can be leveraged for fault-detection and verification~\cite{hoare1971proof,perkins2009automatically}, detecting security vulnerabilities~\cite{bodik2000abcd}, automating the repair of faults~\cite{cashin2019understanding}, and synthesizing low-level implementations~\cite{srivastava2013template}. A number of industrial-strength tools provide support for reasoning about invariant specifications~\cite{coverityscan,fbinfer}.

Despite the fact that programmers are exposed to the concept of invariants early in their education, writing specifications is viewed as a burden and developers don't generally add them to their code base~\cite{das2002esp}. One approach to addressing this is to define implicit specifications, e.g., that a null pointer should never be dereferenced or an array should never be indexed out of bounds. While valuable, this does not address the potential benefit from \emph{program specific invariants}.

The seminal work by Ernst et al. on Daikon~\cite{ernst2007daikon,ernst2000dynamically} addressed this problem by observing that invariants can be thought of as latent properties of program behavior that can be inferred by observing sets of program runs. Techniques like Daikon can only determine \emph{candidate invariants} – since there may be executions that are not observed which falsify the candidate. Nevertheless, these techniques have proven valuable in overcoming the specification burden and generating candidate invariants that can be subsequently verified or falsified by other techniques~\cite{csallner2008dysy}. Moreover, the ability to reveal these latent properties serves as a rich source of information for understanding undocumented code~\cite{ernst2001dynamically}, generating more formal documentation~\cite{ernst2007daikon}, localizing bugs~\cite{b2016learning}, and even proving program termination and non-termination properties~\cite{le2020dynamite}.

Daikon~\cite{ernst2000dynamically,ernst2001dynamically} works by observing \emph{concrete program states} that capture the values of variables at designated \emph{locations of interest} in the program when a program is run on a given input. By sampling large numbers of inputs, Daikon can efficiently determine relationships that may hold among variables across those samples. Confirming that those relationships constitute a true invariant has been a focus of follow-on work to Daikon. Several invariant generation approaches (e.g., iDiscovery~\cite{zhang2014feedback}, PIE~\cite{padhi2016data}, ICE~\cite{garg2016learning}, NumInv~\cite{nguyen2017counterexample}, G-CLN~\cite{yao2020learning}) use a hybrid approach that dynamically infers candidate invariants and then attempts to verify that they hold for all inputs. When verification fails, counterexamples are generated which help to refine the invariant inference process to obtain more accurate results – reporting only true invariants. This \emph{CounterExample Guided Invariant Generation} (CEGIR) approach iterates the inference and verification processes until achieving stable results.

An important class of invariants capture numerical relations among program variables. Such \emph{numerical invariants} can take on different mathematical forms. Daikon can infer conjunctive numerical invariant candidates, but its template matching engine makes it inefficient to infer disjunctive invariants. Disjunctive invariants are required to encode properties of programs, but fortunately rich forms of disjunction can be captured by more complex numerical relations. \emph{Nonlinear polynomial} relations, e.g., \(x^2 \le y^2\), arise in many scientific, engineering, and safety- and security-critical software~\cite{cousot2005astree}, and can encode disjunctive information, e.g., \(x^2 \le y^2\) implies \(x\le -y \vee x\le y\). \emph{Max/min-plus} relations encode properties that can be expressed in ``tropical'' algebra~\cite{maclagan2015introduction,allamigeon2008inferring} and are able to encode a complementary form of disjunctive information, e.g., the max inequality \(\max(x,y) \ge 2\) is equivalent to \((x \ge y \land x \ge 2) \lor (x < y \land y \ge 2)\). As we demonstrate, when used together nonlinear and max/min invariants can express complex program properties, e.g., permutation and sortedness (§\ref{sec:rq3}), that cannot be expressed with purely conjunctive formulae.

In this work, we present DIG;, a CEGIR technique that targets the inference of rich forms of numerical invariants using \emph{symbolic program states} as a basis. Our key insight is that symbolic states generated by a symbolic execution engine are (1) compact encodings of large (potentially infinite) sets of concrete states, (2) naturally diverse since they arise along different execution paths, (3) explicit in encoding relationships between program variables, (4) amenable to direct manipulation and optimization, and (5) reusable across many different reasoning tasks within CEGIR algorithms.

We define algorithms for symbolic CEGIR that can be instantiated using different symbolic execution engines, and the DIG; implementation uses symbolic states generated from Symbolic PathFinder~\cite{anand2007jpf} (SPF)—a symbolic executor for Java—and CIVL~\cite{siegel2015civl}—a symbolic executor for C. DIG; uses symbolic states for both invariant inference and verification. For inference, DIG; uses symbolic states to obtain concrete states to bootstrap a set of candidate invariants using DIG~\cite{nguyen2012using,nguyen2014using,nguyen2014dig}—a dynamic analysis framework for inferring expressive numerical invariants. For verification, DIG; formulates verification conditions from symbolic states to confirm or refute an invariant, solves those using an SMT solver, and produces counterexamples to refine the inference process.

We evaluated DIG; over 4 distinct benchmarks, consisting of 108 programs, and compared its performance to state-of-the-art numerical invariant approaches. We find that the use of symbolic states allows DIG; to overcome several limitations of existing CEGIR approaches. iDiscovery, which uses Daikon for inference, does not support nonlinear properties, and both ICE and PIE timeout frequently when nonlinear arithmetic is involved. NumInv also uses DIG to infer invariants, but it invokes KLEE~\cite{cadar2008klee} as a black box verifier for candidate invariants and which causes it to underperform relative to DIG; for nonlinear and disjunctive invariant inference. G-CLN can infer nonlinear invariants for loops, but it requires manual problem-specific configuration to generate and prove invariants, and even then DIG; infers more relevant invariants. Our evaluation demonstrates that DIG; establishes the state-of-the-art for inference of complex nonlinear invariants. Across the benchmarks it is able to infer the ground truth specifications for 106 of 108 programs; the next best tool can infer only 89.%\tvn{Is this too strong to explicitly say this number? Technically we were not able to get other tools, e.g., G-CLN, on other benchmarks like DISJ or COMPLEXITY}.

Our prior work~\cite{nguyen2017syminfer} made an initial step in exploiting symbolic states for invariant inference. This paper significantly extends those results to include: (1) a novel efficient algorithm to generate inequalities; (2) support for \emph{max}- and \emph{min-plus} formulae to represent disjunctive invariants; (3) proofs of correctness and termination for the presented algorithms; (4) support for Java and C programs; and (5) a broader experimental evaluation that demonstrates the cost-effectiveness of the approach and its superiority to existing invariant inference techniques. The implementation of DIG; and all experimental data reported in this paper are available at \url{https://github.com/unsat/dig/}. These results strongly suggest that symbolic states form a powerful basis for computing program invariants. They permit an approach that blends the best features of dynamic inference techniques and purely symbolic techniques to enable a new state-of-the-art.

% \IEEEPARstart{T}{he} automated discovery of \emph{program invariants}—relations among variables that are guaranteed to hold at certain locations of a program—is an important research area in program analysis, verification, and synthesis. % Generated invariants can help understand undocumented programs, prove correctness assertions, reason about program termination, check resource usage, establish security properties, provide formal documentation, repair programs, and more~\cite{le2020dynamite,slam,henzinger2002lazy,das2002esp,demoura:tacas08:z3,leroy:popl06:,ernst2000dynamically,nguyen2020using}.

% A particularly useful class of invariants is \emph{numerical invariants}, which involve relations among numerical program variables. % Within numerical invariants, \emph{nonlinear polynomial} relations, e.g., \(x \le y^2\), \(x = qy + r\), arise in many scientific, engineering, and safety- and security-critical software, e.g., to prove the absence of errors in Airbus avionic systems~\cite{cousot2005astree}. % Nonlinear relations can also encode certain form of disjunctive information, e.g., \(x\le y^2\) is \(x\le -y \vee x\le y\). % \emph{Min/max-plus} relations are another class of numerical informations that can represent a different form of disjunction, e.g., the max inequality \(\max(x,y) \ge 2\) represents \((x > y \land x \ge 2) \lor (x < y \land y \ge 2)\). % When used together nonlinear and min/max invariants can be complimentary and help reason about complex but useful program properties, e.g., permutation and sortedness (§\ref{sec:rq3}).

% %Another complemtary class of numerical invariants that can represent disjuctions is \emph{min/max-plus} relations .

% %Disjunctive invariants, which represent the semantics of branching, are more difficult to analyze but crucial to many programs. For example, after if (p) {a=1;} else {a=2;} neither a = 1 nor a = 2 is an invariant, but (p ∧ a = 1) ∨ (¬p∧a = 2) is a disjunctive invariant. Disjunctive invariants thus capture path-sensitive reasoning, such as those found in most sorting and searching tasks, as well as functions like strncpy in the C standard library.

% Daikon~\cite{ernst2000dynamically,ernst2001dynamically} demonstrated that dynamic analysis is a practical approach to infer numerical and other invariants from \emph{concrete program states} that program execution traces observed when running the program on sample inputs. % Dynamic inference is typically efficient and supports expressive invariants, but can often produce spurious invariants that do not hold for all possible inputs. % Several numerical invariant generation approaches (e.g., iDiscovery~\cite{zhang2014feedback}, PIE~\cite{padhi2016data}, ICE~\cite{garg2016learning}, NumInv~\cite{nguyen2017counterexample}, G-CLN~\cite{yao2020learning}) use a hybrid approach that dynamically infers candidate invariants and then statically checks that they hold for all inputs. % For a spurious invariant, the checker produces counterexamples, which help the inference process avoid this invariant and obtain more accurate results. % This CEGIR \emph{(CounterExample Guided Invariant Generation)} approach iterates the inference and checking processes until achieving stable results.

% In this work, we present DIG;, a CEGIR technique and tool that uses \emph{symbolic program states}. % Our key insight is that symbolic states generated by a symbolic execution engine are % (1) compact encodings of large (potentially infinite) sets of concrete states, % (2) naturally diverse since they arise along different execution paths, % (3) explicit in encoding relationships between program variables, % (4) amenable to direct manipulation and optimization, and %such as combining sets of states into a single joint encoding, and % (5) reusable across many different reasoning tasks within CEGIR algorithms.

% We define algorithms for symbolic CEGIR that can be instantiated % using different symbolic execution engines, and the DIG; implementation uses symbolic states generated from Symbolic PathFinder~\cite{anand:tacas07:spf} (SPF)—a symbolic executor for Java—and CIVL~\cite{siegel2015civl}—a symbolic executor for C. % DIG; uses symbolic states for both invariant inference and % validation. % For inference, DIG; uses symbolic states to obtain concrete states to bootstrap a set of candidate invariants using % DIG~\cite{nguyen:icse12:dig,nguyen2014using,nguyen:tosem14:dig}—a dynamic analysis framework for inferring expressive numerical invariants. % For validation, DIG; formulates verification conditions from symbolic states to confirm or refute an invariant, solves those using an SMT solver, and produces counterexamples to refine the inference process.

% %TODO: min/max invariants % Symbolic states allow DIG; to overcome several limitations of existing CEGIR approaches. % iDiscovery, ICE, and PIE are limited to computing relatively simple numerical invariants and often do not consider programs with complex nonlinear arithmetic and properties. % such as \(x=qy+r, x^2+y^2=z^2\). % As our evaluation of DIG; demonstrates in Section~\ref{sec:eval}, % iDiscovery, which uses Daikon for inference, does not support nonlinear properties, and both ICE and PIE timeout frequently when nonlinear arithmetic is involved. % The tool NumInv~\cite{nguyen2017counterexample} also uses DIG to infer invariants, but it invokes KLEE~\cite{cadar2008klee} as a blackbox % verifier for candidate invariants. Since KLEE is unaware of the goals % of its verification it will attempt to explore the entire program state space % and must recompute that state space for each candidate invariant. % In contrast, DIG; incrementally constructs a fragment of the state space % that generates a set of symbolic states that is sufficiently diverse % for invariant verification and it reuses symbolic states for all invariants. % The recent work G-CLN~\cite{yao2020learning} learns nonlinear invariants for loops using neural networks, but it requires the user to provide strong postconditions and manual tweaks to generate and prove invariants, whereas DIG; only requires the implementation. % % and generate counterexamples

% We evaluated DIG; over 4 distinct benchmarks which consist of 108 programs. % The study shows that DIG;: % (1) can generate the complex nonlinear invariants expected in 28/28 of the NLA benchmarks; % (2) can generate nonlinear relations and min/max invariants to represent interesting disjunctive properties (e.g., permutation); % (3) is effective in finding nontrivial complexity bounds for 18/19 programs, with 4 of those improving on the best known bounds from the literature; % (4) can generate invariants whose combination establish asserted properties involving relations not supported directly by DIG; for 45/46 programs; and % (5) effectively uses symbolic execution at various depths to incrementally improve results; and % (6) outperforms existing numerical invariant generation works, especially in generating rich invariants capturing nonlinear and disjunctive information.

% These results strongly suggest that symbolic states form a powerful basis for computing program invariants. % They permit an approach that blends the best features of dynamic inference techniques and purely symbolic techniques. % The key contribution of our work lies in (i) the identification of the value % of symbolic states in CEGIR, (ii) developing an algorithmic framework for % adaptively computing a sufficient set of symbolic states for invariant % inference, (iii) developing and releasing DIG; as an open-source implementation of this framework, % and (iv) demonstrating, through our evaluation of % DIG;, that it improves on the best known techniques.

% Our prior work~\cite{nguyen2017syminfer} made an initial step in exploiting % symbolic states for invariant inference. % This paper significantly extends those results to include: % (1) a novel efficient algorithm to generate inequalities; % (2) support for \emph{max}- and \emph{min-plus} formulae to represent disjunctive invariants; % (3) proofs of correctness and termination for the presented algorithms; % (4) support for Java, Java bytecode, and C programs; and % (5) a broader experimental evaluation that demonstrates the cost-effectiveness of the approach. % The implementation of DIG; and all experimental data reported in this paper are available at \url{https://github.com/unsat/dig/}. % % \matt{I see that we dropped pre/post discussion so I dropped it here.}