SSI and ABCD for LLVM

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,

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 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

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

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@cs.uiuc.edu http://llvm.cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
    
_______________________________________________
LLVM Developers mailing list
LLVMdev@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.

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

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:

Hi André,

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.

there is a plan to replace the zext and sext parameter attributes with
attributes that tell you how many top bits are zero / sign extended.
For example, if an i32 parameter is marked with the "zext from i27"
attribute that means that the upper 5 bits are always zero. Your
proposed pass to calculate which bits are in use could both use this
information and calculate it. This is also gives some info useful
for bounds checking. It might also be useful to extend these attributes
to give more precise range information on parameters. Then the ABCD
algorithm could set and use them, giving a cheap form of
inter-procedural ABCD.

Ciao,

Duncan.