Dynamic Symbolic Execution of Higher-Order Functions

TL;DR

This paper introduces a novel concolic testing approach for higher-order functions, enabling effective bug detection by modeling inputs with canonical shapes and leveraging SMT solvers, addressing limitations of traditional methods.

Contribution

It presents the first design, semantics, and prototype for concolic testing of higher-order functions, capturing complex interactions with inputs for bug detection.

Findings

Proves that the concolic tester will find bugs if they exist in higher-order functions.

Implemented a prototype that successfully discovers bugs in literature programs.

Demonstrates the effectiveness of the approach through validation on real higher-order programs.

Abstract

The effectiveness of concolic testing deteriorates as the size of programs increases. A promising way out is to test programs modularly, e.g., on a per function or class basis. Alas, this idea hits a roadblock in modern programming languages In modern languages, components expect functions, objects, and even classes as inputs. The crux of the problem is that existing concolic testing techniques cannot faithfully capture the complex interactions between a higher-order program and its inputs in order to distill it in a first-order formula that an SMT solver can work with. In this paper, we take the first step towards solving the problem; we offer a design, semantics, and prototype for concolic testing of higher-order functions. Inspired by work on higher-order symbolic execution, our model constructs inputs for higher-order functions with a canonical shape. This enables the concolic tester to keep track of which pieces of the control-flow path of the higher-order function depend on the shape of its input and which do not. The concolic tester encodes the pieces that do not depend on the shape of the input as a first-order formula. Subsequently, similar to a first-order concolic tester, it leverages an SMT solver to produce another input with the same shape but that explores a different control-flow path of the higher-order function. As a separate dimension, the concolic tester iteratively explores the canonical shapes for the input and, investigating all the ways a higher-order function can interact with its input, searching for bugs. To validate our design, we prove that if a higher-order function has a bug, our concolic tester will eventually construct an input that triggers the bug. Using our design as a blueprint, we implement a prototype concolic tester and confirm that it discovers bugs in a variety of higher-order programs from the literature.