Bound Analysis for Whiley Programs

Min-Hsien Weng; Mark Utting; Bernhard Pfahringer

doi:10.1016/j.entcs.2016.01.005

Back

Journal article

Open access

Peer reviewed

Bound Analysis for Whiley Programs

Min-Hsien Weng, Mark Utting and Bernhard Pfahringer

Electronic Notes in Theoretical Computer Science, Vol.320, pp.53-67

2016

DOI: https://doi.org/10.1016/j.entcs.2016.01.005

Files and links (2)

pdf

PDF - Published Version (Open Access)211.70 kBDownload View

Published VersionPDF - Published Version (Open Access)CC BY-NC-ND V4.0, Open Access

url

https://doi.org/10.1016/j.entcs.2016.01.005View

Published Version

Abstract

static analysis

range analysis

abstract interpretation

bound consistency

widening operator

symbolic analysis

pattern matching

program transformation.

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.

Details

Title: Bound Analysis for Whiley Programs
Authors: Min-Hsien Weng (Author) - Waikato University, New Zealand
Mark Utting (Author) - University of the Sunshine Coast - Faculty of Arts, Business and Law
Bernhard Pfahringer (Author) - Waikato University, New Zealand
Publication details: Electronic Notes in Theoretical Computer Science, Vol.320, pp.53-67
Publisher: Elsevier BV
Date published: 2016
DOI: 10.1016/j.entcs.2016.01.005
ISSN: 1571-0661
Organisation Unit: School of Science and Engineering - Legacy; University of the Sunshine Coast, Queensland
Language: English
Record Identifier: 99449149302621
Output Type: Journal article

Metrics

156 File views/ downloads

1207 Record Views

2 Times Cited - Web of Science

InCites Highlights

These are selected metrics from InCites Benchmarking & Analytics tool, related to this output

Collaboration types: Domestic collaboration; International collaboration
Web Of Science research areas: Computer Science, Theory & Methods