Producing Execution Traces for Dynamic Invariant Detection

This paper describes three contributions I made to our system which collectively produce the execution traces that Daikon needs to derive useful invariants. The high level architecture of the tool is discussed in Section 2. The first component is a tool to instrument C/C++ programs so that variable values are dumped to disk during execution (Section 3). Programmers may use the resulting invariants to reason directly about the source. The instrumentor is particular to C/C++ programs; however, a significant portion of the legacy code that programmers are currently maintaining is C/C++. The second contribution is a module that employs type inference to produce lists of comparable variables that Daikon uses to selectively perform invariant checks (Section 4). Use of the type inference results are shown to reduce the runtime of Daikon and the number of spurious invariants that it reports. The final contribution is some initial insights on cheaply generating test cases to produce execution traces from instrumented programs (Section 5). We must guide users on how to produce good invariants from our system for programs which lack test suites. The paper ends with some potential future work (Section 6) and conclusions (Section 7)