Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Derivative-Guided Symbolic Execution

Yongwei Yuan, Zhe Zhou, Julia Belyakova, Suresh Jagannathan

TL;DR

This work considers the formulation of a symbolic execution procedure for functional programs that interact with effectful, opaque libraries and incorporates the notion of symbolic derivatives, a mechanism that allows the SE procedure to intelligently underapproximate the set of precondition states it needs to explore, based on the automata structures latent in the provided specifications.

Abstract

We consider the formulation of a symbolic execution (SE) procedure for functional programs that interact with effectful, opaque libraries. Our procedure allows specifications of libraries and abstract data type (ADT) methods that are expressed in Linear Temporal Logic over Finite Traces (LTLf), interpreting them as symbolic finite automata (SFAs) to enable intelligent specification-guided path exploration in this setting. We apply our technique to facilitate the falsification of complex data structure safety properties in terms of effectful operations made by ADT methods on underlying opaque representation type(s). Specifications naturally characterize admissible traces of temporally-ordered events that ADT methods (and the library methods they depend upon) are allowed to perform. We show how to use these specifications to construct feasible symbolic input states for the corresponding methods, as well as how to encode safety properties in terms of this formalism. More importantly, we incorporate the notion of symbolic derivatives, a mechanism that allows the SE procedure to intelligently underapproximate the set of precondition states it needs to explore, based on the automata structures implicit in the provided specifications and the safety property that is to be falsified. Intuitively, derivatives enable symbolic execution to exploit temporal constraints defined by trace-based specifications to quickly prune unproductive paths and discover feasible error states. Experimental results on a wide-range of challenging ADT implementations demonstrate the effectiveness of our approach.

Derivative-Guided Symbolic Execution

TL;DR

This work considers the formulation of a symbolic execution procedure for functional programs that interact with effectful, opaque libraries and incorporates the notion of symbolic derivatives, a mechanism that allows the SE procedure to intelligently underapproximate the set of precondition states it needs to explore, based on the automata structures latent in the provided specifications.

Abstract

We consider the formulation of a symbolic execution (SE) procedure for functional programs that interact with effectful, opaque libraries. Our procedure allows specifications of libraries and abstract data type (ADT) methods that are expressed in Linear Temporal Logic over Finite Traces (LTLf), interpreting them as symbolic finite automata (SFAs) to enable intelligent specification-guided path exploration in this setting. We apply our technique to facilitate the falsification of complex data structure safety properties in terms of effectful operations made by ADT methods on underlying opaque representation type(s). Specifications naturally characterize admissible traces of temporally-ordered events that ADT methods (and the library methods they depend upon) are allowed to perform. We show how to use these specifications to construct feasible symbolic input states for the corresponding methods, as well as how to encode safety properties in terms of this formalism. More importantly, we incorporate the notion of symbolic derivatives, a mechanism that allows the SE procedure to intelligently underapproximate the set of precondition states it needs to explore, based on the automata structures implicit in the provided specifications and the safety property that is to be falsified. Intuitively, derivatives enable symbolic execution to exploit temporal constraints defined by trace-based specifications to quickly prune unproductive paths and discover feasible error states. Experimental results on a wide-range of challenging ADT implementations demonstrate the effectiveness of our approach.

Paper Structure

This paper contains 30 sections, 8 theorems, 35 equations, 10 figures, 1 table.

Table of Contents

  1. Introduction
  2. Motivation
  3. Specifications
  4. Trace Specification as Safety Property
  5. SFA Representation of Trace Specifications
  6. Symbolic Derivatives and SFAs
  7. Trace-Based Symbolic Execution
  8. Expressing Hidden States as Traces.
  9. Refinement of Trace-Based Symbolic States.
  10. Symbolic Execution with Symbolic Derivatives
  11. Derivative-Guided Path Exploration
  12. Derivative-Guided Falsification
  13. Preliminaries
  14. Effective Boolean Algebras
  15. Traces
  16. ...and 15 more sections

Key Result

corollary 1

If $\mathcal{R}\xspace{=} \mathsf{D}_{ \Pi\xspace} \mathcal{R}\xspace\xspace$ and $( \Phi\xspace, \Pi\xspace, \mathcal{R}\xspace,e) {\hookrightarrow_{\mathcal{D}}^*} ( \Phi\xspace', \Pi\xspace', \mathcal{R}\xspace',e')$ then $\mathcal{R}\xspace'{=} \mathsf{D}_{ \Pi\xspace'} \mathcal{R}\x

Figures (10)

  • Figure 1: An implementation of a node remove operation in a linked-list ADT using two key-value stores.
  • Figure 2: The SFA representation of remove's trace-based specification.
  • Figure 3: Derivative-guided symbolic execution of remove.
  • Figure 4: Syntax of the core language.
  • Figure 5: Naive trace-augmented semantics.
  • ...and 5 more figures

Theorems & Definitions (17)

  • definition 1: Denotation of Boolean Formulae
  • definition 2: Reachability
  • definition 3: Naı̈ve Falsification
  • definition 4: Inclusion
  • definition 5: Equivalence
  • definition 6
  • definition 7: Symbolic Derivative
  • corollary 1
  • lemma 1
  • corollary 2
  • ...and 7 more