Bound Analysis for Whiley Programs

详细信息    查看全文

• 作者：Min-Hsien Weng^a ; ^{mw169@students.waikato.ac.nz" class="auth_mail" title="E-mail the corresponding author} ; Mark Utting^a ; ^b ; ^{marku@waikato.ac.nz" class="auth_mail" title="E-mail the corresponding author} ; Bernhard Pfahringer^a ; ^{bernhard@waikato.ac.nz" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Static Analysis ; Range Analysis ; Abstract Interpretation ; Bound Consistency ; Widening Operator ; Symbolic Analysis ; Pattern matching ; Program Transformation
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2016
• 出版时间：26 February 2016
• 年：2016
• 卷：320
• 期：Complete
• 页码：53-67
• 全文大小：211 K

文摘

The Whiley compiler can generate naive C code, but the code is inefficient because it uses infinite integers and dynamic array sizes. Our project goal is to build up a compiler that can translate Whiley programs into efficient OpenCL code with fixed-size integer types and fixed-size arrays, for parallel execution on GPUs. This paper presents an abstract interpretation-based bound inference approach along with symbolic analysis for Whiley programs. The source Whiley program is first analyzed by using our symbolic analyzer to find the matching pattern and make any necessary program transformation. Then the bound analyzer is used to analyze the transformed program to make use of primitive integer types rather than third-party infinite integer type (e.g. using GMP arbitrary precision library). The bound analysis results provide conservative estimates of the ranges of integer variables and array sizes so that efficient code can be generated and integer overflows avoided. The bound analyzer combines the bound consistency technique along with a widening operator to give fast time of solving program constraints and of converging to the fixed point. Several example programs are used to illustrate the bound analyzer algorithm and the program transformation.