CodeSurfer Path Inspector

An extension to CodeSurfer that helps you understand sequencing properties of programs.

Overview

CodeSurfer^® Path Inspector™ is an optional extension to CodeSurfer that answers complex questions about the flow of execution to help you understand a program's behavior.

Example Application

Suppose that your application uses a DNS library, and the library contains an initialization function called initialize_dns. Before calling any other routines in the library, a program must call initialize_dns. You wonder if it is always true that initialize_dns is called before the other routines. Instead of manually wading through the code to answer this question, you can ask the CodeSurfer Path Inspector. The Path Inspector will either tell you that initialize_dns is always called first, or it will show you a counter example—an execution path of the program that calls one of the other functions in the DNS library without first calling initialize_dns.

Query Construction and Evaluation

Twenty-five query templates are provided. Each template is in the form of a state machine. The user specifies the transitions of the state machine by associating a set of program points with each transition. In the DNS example above, the query template used is called P occurs before R and is illustrated below.

P and R are sets of program points that the user specifies. For the DNS check, P and R are the following:

P = {entry of initialize_dns}
R = {entry of lookup_ip, entry of lookup_name, entry of check_reverse_dns}

Although all the program points in this example are the entries of functions, a program point can be almost anything, including any statement in the program. Once the query is specified, it can be run immediately or queued for batch processing at a later time. To evaluate the query, the Path Inspector takes the query automaton, crosses it with an automaton representing the program, and then does a reachability analysis.