Static analysis is a general term in computer science, specifically compiler theory. In the context of the NStatic code analysis, it refers to the identification of errors, warnings and redundancies in source code or intermediate language prior to actual execution at runtime. These errors would occurred at runtime under certain conditions, but they were found earlier at compile (scan) time.
Why use static analysis?
Bugs found earlier in the software development are much easier and less costly to fix.
There is no performance overhead of runtime checking.
All code is checked uniformly including those on rarely executed code paths, where unfound errors most likely reside.
Cost of Fixing
Software
Bugs
Design
Dev
Test
Release
The NStatic code checker is SoftPerson’s static analysis tool for finding a wide variety of semantic errors.
Many semantic errors are automatically detected because they exhibit certain characteristics that indicate illogical behavior:
Redundancy
Exception behavior
Nontermination
Unused code
Failed assertions
In addition, NStatic has plans to include code contracts, which are assertion and invariant code that are specifically added by the developer but may not actually be executed at runtime.
NStatic features a debugger-like interface matching those of Microsoft Visual Studio. The product is essentially a debugger for code at compile time. Instead of raw values, mathematical expressions are displayed instead.
Familiar windows. These include familiar debugger windows such as locals, call stack, immediate window, watch and breakpoints. A simulated exception object is displayed in a locals windows.
Live expressions. The local and watch windows display property values in addition to field values, and method can be called in the immediate window. There is also an assumptions window that contains the clausal conditions that produces the error.
Rich information. The error information is richer than provided by other static analysis tools. Other tools simply emit “file.cs(100): null pointer referenced” with any information about code paths or local values. NStatic’s error description and other information available through windows may even be richer than the actual error.
The images on the right depict some of the windows available for viewing error information in NStatic.
The assumptions window, locals window, and source code editor are all part of the same session. The call stack on the bottom depict an Interprocedural analysis on a different NStatic bug.
The source code editor features execution highlighting to indicate the flow of execution through a function that led to the bug.
Error paths are highlighted with orange curve arrows. Skipped code is dimmed. Important conditions are highlighted with green circles and red strikethroughs for truth and falsity.
Error path highlighted with orange arrows.
Skipped code is dimmed.
Important conditions highlighted with green circles and red strikeouts for truth and falsity.
Execution highlighting also handles loops as in the following example.
Source code editor
Locals window
Assumptions window*
Call stack
The source editor and local variables windows below highlight some more advanced capabilities of the static analysis tool such as the handling of property evaluations and virtual function calls.
NStatic has also been design with specifications in mind. This is similar to the code contracts feature in Microsoft.NET, Spec#, and Eiffel. Specification keywords include preconditions (“require”), postconditions (“ensure”), asserts (“assert” and “assume”), and invariants (“invariants”). These keywords are used for code verification. System.Diagnostics.Contracts functions in .NET are also supported.
Quantifiers in assertions like “forall” and “exists” are recognized with limited support, but are best replaced with actual function calls, which are more natural and have better support. Any side effects in function calls are isolated in assertions.
The reasoning engine is not a theoretically complete, but the problem of verification is known to be intractable or even incomputable (e.g., detecting nontermination) depending on the problem class. The goal of NStatic is to solve the classes of problems that humans can readily solve including proving an implementation of red-black trees is correct—a notoriously tricky problem. Verify red-black trees would involve an assertion “” at the beginning and end of a function, where IsRedBlackTree is a function that recursively calls itself on the children of the node and then verifies that either the node is not colored red or neither of the children are red. This can be proved by inductive reasoning, a technique NStatic is designed to support.
NStatic employs different techniques from most tools. Some products use code flow graphs analysis, so they can’t handle interprocedural calls and pointers well.
NStatic uses a fully symbolic approach, directly translating the code into lambda calculus and using computer algebraic and equational theorem prover techniques.
Loops are converted to recursive lambda expressions. Function calls as well.
Expressions are then simplified to canonical form under the current assumptions. This technique can be used to solve matrices as can be seen in the bottom figure.
