Songtao Xia, Manuel Fahndrich, and Francesco Logozzo
In SCOPE, a SQL style cloud-level data-mining scripting language, table processing capabilities are often provided by user defined .NET methods. The Scope compiler can optimize its query plan if it knows certain dataflow relations between the input and output tables. Useful relations are dependence or equality between input and output columns, or constraints over the output columns. Automatically and accurately inferring these properties is difficult due to the special compilation scheme of .NET iterators, the need to reason about numerical relations for naming or estimating column numbers, aliasing and escaping, and the need to automatically infer universally quantified loop invariants.
We designed and implemented Scooby, a custom-tailored, abstract interpretation-based, domain specific static analyzer for .NET iterators. We adopt and extend the state-of-the-art abstraction and quantified invariant inference techniques to solve these problems in a way that suits our application domain. Scooby is able to discover these properties for every-day SCOPE programs automatically, efficiently, and accurately.
In Proceeding of the 16th International Static Analysis Symposium (SAS'09)
Publisher Springer Verlag
All copyrights reserved by Springer 2007.