EPITAXIS A System for Syntactic and Semantic Software Queries using Deductive Retrieval and Symbolic Execution

Abstract

📜 Abstract

Modern computer hardware (multi-core, multi gigahertz processors with gigabytes of RAM and terabytes of disk) along with IDEs allows programmers to build computer programs which are bigger and more complex than they can understand or keep in their working memories. Additionally, the problems these programs are designed to model are ever more complicated. Consequently, programs are full of inconsistencies, mistakes, and incompleteness's. These problems are difficult to detect, difficult to locate, and difficult to correct. Often a change is made by a programmer to fix a problem for which understanding all the repercussions of the change is difficult. Consequently, further bugs are introduced into the code base. Because of the pervasiveness of software in society and the potential severity of the consequences of bugs, software developers need ever better tools to help them understand, navigate, and follow the consequences of their development and maintenance activities. This dissertation presents a novel framework based on tree/graph searching and parsing, deductive retrieval, dynamic analysis, symbolic execution, aspect oriented programming, and an open interpreter to allow a software developer to navigate, locate features, find bugs, and abstract information in software. The system is designed to have a fast modify-test cycle such that the programmer can search and test the software as it is being edited without time consuming recompilation, reinstrumenting, or database repopulating each time an edit is made to the code base. The system is language independent, requiring only files to specify the language grammar, control flow graph transformation, and execution semantics. In addition, because of the flexibility and programmability of the system it is an excellent environment to perform further research on program analysis techniques such as dynamic analysis, symbolic execution and abstract interpretation. A prototype system has been built along with data files for the C programming language which demonstrates the feasibility of the system and its ability to scale to "modern-sized" programs.

Description

✨ Summary

The dissertation presents Epitaxis, an interactive framework for querying and analyzing software across lexical, syntactic, static-semantic, dynamic-semantic, and abstract levels. Its central design is a unified representation combining a complete lexical token list, a bidirectionally linked abstract syntax tree, an executable control-flow graph, and virtual abstract semantic graphs that are constructed through rule-based deduction when needed.

The system uses an object-oriented, Prolog-like search language based on unification, backtracking, structural traversal, rule application, and memoization. Queries can identify lexical patterns, navigate syntax trees, derive control-flow structures, infer relationships through rules, inspect symbolic execution states, and search abstract structures accumulated from earlier analyses. The approach is intended to avoid the need for a separately hard-coded representation for every analysis.

A major contribution is the integration of an open symbolic interpreter with the query engine. The interpreter operates at the source level rather than on compiled machine or assembly code, preserving source constructs, types, declarations, member names, and casting information. It supports concrete and symbolic values, proxy values and addresses, interval-based value representations, symbolic memory, constraint propagation, multi-path execution, configurable loop-step limits, and collection or assertion points. These facilities allow the system to detect runtime singularities such as null dereferences, invalid memory accesses, uninitialized reads, and out-of-bounds indexing, while also collecting higher-level information about values, function calls, structure members, and data-flow relationships.

The prototype was implemented in an augmented LISP environment and supplied with language-specific definitions for C. Incremental reparsing allows a modified source line to be tokenized and integrated into the existing syntax structure without reparsing the entire program. On a 392,690-line C code base, the system reportedly required 88 seconds and 1.3 GB of memory to scan and parse the code, followed by 86 seconds and an additional 97 MB to construct the control-flow graph. Syntactic searches over the code base found 12,180 function definitions in 0.124 seconds, 88,581 function calls in 1.235 seconds, and 1,076 unused local variables in 11.468 seconds.

The symbolic-execution experiments demonstrate both capability and limitations. Epitaxis found the target error in the symbolic string-input example in 0.312 seconds. On the 169-line tr.c utility, it found seven errors and reached approximately 85% code coverage before exhausting memory, with one reported error attributed to malformed input and several others associated with incomplete modeling of argv. On a 1,294-line retrieval function, configurable loop-step limits substantially affected coverage and error detection; the two-step mode reached 91.41% reported code coverage and found 16 null-pointer errors before exhausting available memory. The experiments also expose the expected path-explosion and memory-growth problems of symbolic execution.

The dissertation’s advanced analysis uses collection points and formal concept analysis to summarize information gathered across execution paths. Concept lattices expose relationships among structure fields, predicate types, union usage, nested member accesses, and function-related values. This illustrates how the framework can support analyses concerned with data representation and conceptual invariants rather than only directly observable crashes.

The prototype supports only C, has limited modeling of the external environment and standard library, does not understand the normal structure of argc and argv, lacks embedded-assembly support, and relies on a comparatively weak constraint system. Breadth-first symbolic execution causes path and memory growth, and the dissertation does not provide a broad comparative evaluation against contemporary program-query or symbolic-execution systems.

The University of California, Irvine research repository confirms the dissertation’s 2010 publication metadata and identifies James Benvenuto as its sole author. (its.uci.edu) A quick search did not identify clear, verifiable scholarly citations demonstrating substantial subsequent research adoption or commercial deployment of the Epitaxis system. The work did receive at least one documented community-dissemination event: Papers We Love listed a September 28, 2016 Los Angeles talk by Jim Benvenuto on Epitaxis. (paperswelove.org) The available evidence therefore supports dissemination as a software-research presentation, but not a significant documented downstream influence on industry or later academic systems.