llvm dev - Jun 2009 - [LLVMdev] SSI and ABCD for LLVM

By static array bounds checking, I mean eliminating array bounds checking
which can be proved ``safe'' at compile-time.

Well, even though there are a lot of approaches of doing this, I believe
that having an implementation of ABCD would very useful. It would be even
more useful if LLVM can have a general framework for doing static array
bounds checking -- just like the aliasing framework.

Haohui

-----Original Message-----
From: llvmdev-bounces at cs.uiuc.edu [mailto:llvmdev-bounces at cs.uiuc.edu] On
Behalf Of Andre Tavares
Sent: Thursday, June 04, 2009 8:33 PM
To: LLVM Developers Mailing List
Subject: Re: [LLVMdev] SSI and ABCD for LLVM

Mai, Haohui wrote:
> Dear Nicolas,
>
> I'm curious why you are using ABCD in vmkit. Do you need any features
> from static array bounds checking? As far as I know, SAFECode has a
> number of implementation for that.
>
> Thanks.
>
> Haohui 
>
> On Thu, 2009-06-04 at 20:48 +0200, Nicolas Geoffray wrote:
>   
>> Dear Andre,
>>
>> That's great! Thanks for the blog. I am really looking forward into
>> using ABCD in vmkit!
>>
>> Cheers,
>> Nicolas
>>
>> Andre Tavares wrote:
>>     
>>> Dear Community,
>>>
>>> I'm working on a project for Google Summer of Code, to
implement the
>>> ABCD and Bitwidth analysis in LLVM. I'm not going to extend the
>>> description of the project here, this link shows my proposal 
>>> http://homepages.dcc.ufmg.br/~andrelct/projects/gsoc_2009/proposal.
>>>
>>> I have been in some discussions on this list about Ada and SSI that
>>> helped on my decisions up to this moment.
>>>
>>> This project is due to August, and during this period I will be
posting
>>> my progress in a blog. If someone has interest in following my
progress
>>> I welcome you to read the blog, and I would really appreciate any 
>>> suggestion, critics and opinions on any aspect. I understand that
every
>>> opinion is helpful. So the blog link is 
>>> http://gsoc2009-andrelct.blogspot.com/.
>>>
>>> Best Regards,
>>>
>>>   
>>>       
>> _______________________________________________
>> LLVM Developers mailing list
>> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>>     
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>
>   
Sorry if my description was too short, but I will be removing 
unnecessary array bound checks, not creating them.

-- 
Andre Tavares
Master Student in Computer Science - UFMG - Brasil
http://dcc.ufmg.br/~andrelct

_______________________________________________
LLVM Developers mailing list
LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev

On Jun 5, 2009, at 9:26 AM, Mai, Haohui wrote:
> By static array bounds checking, I mean eliminating array bounds  
> checking
> which can be proved ``safe'' at compile-time.
Even though SAFECode does have such a pass, there are some tradeoffs  
with the current version:

1. It uses an external solver (Omega), which is one more dependence  
for LLVM in general.  I don't have a problem with this myself but some  
users may.

2. The existing algorithm for propagating constraints (inequalities)  
on variables is interprocedural (good) and inefficient (bad).

ABCD has different tradeoffs.  IIRC, ABCD doesn't use an external  
solver, though only because it only handles simple sets of  
inequalities.  The original ABCD algorithm is also intraprocedural,  
which seems extremely limiting in practice.  Is there any plan of  
extending this to work interprocedurally?

--Vikram
Associate Professor, Computer Science
University of Illinois at Urbana-Champaign
http://llvm.org/~vadve

Vikram S. Adve wrote:
> On Jun 5, 2009, at 9:26 AM, Mai, Haohui wrote:
>
>   
>> By static array bounds checking, I mean eliminating array bounds  
>> checking
>> which can be proved ``safe'' at compile-time.
>>     
>
> Even though SAFECode does have such a pass, there are some tradeoffs  
> with the current version:
>
> 1. It uses an external solver (Omega), which is one more dependence  
> for LLVM in general.  I don't have a problem with this myself but some
> users may.
>
> 2. The existing algorithm for propagating constraints (inequalities)  
> on variables is interprocedural (good) and inefficient (bad).
>
> ABCD has different tradeoffs.  IIRC, ABCD doesn't use an external  
> solver, though only because it only handles simple sets of  
> inequalities.  The original ABCD algorithm is also intraprocedural,  
> which seems extremely limiting in practice.  Is there any plan of  
> extending this to work interprocedurally?
>
> --Vikram
> Associate Professor, Computer Science
> University of Illinois at Urbana-Champaign
> http://llvm.org/~vadve
>
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>
>   
Dear Vikram,

we chose ABCD because it is a fast approach to solve the problem. It has 
the drawback that it is intra-procedural. For the Summer of Code 
project, we will stick to the original ABCD algorithm. But we can study 
modifications to make it inter-procedural for later research. Any ideas 
and contributions you might have will be welcome.

-- 
Andre Tavares
Master Student in Computer Science - UFMG - Brasil
http://dcc.ufmg.br/~andrelct