[LLVMdev] Formal spec for LLVM IR (Was: LLVM Language Reference Strictness)

[Vikram Adve]

Reed,

Are you working on a grammar of the LLVM syntax or also on a full semantics?

Steve Zdancewic's group at U. Penn. is working on a formal operational semantics for LLVM.  It is partially complete and Greg Morrisett at Harvard is planning to build further on it.

Regards,

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




On Oct 20, 2011, at 11:56 AM, <llvmdev-request at cs.uiuc.edu>
 <llvmdev-request at cs.uiuc.edu> wrote:

> Date: Thu, 20 Oct 2011 09:47:58 -0700
> From: Reed Kotler <rkotler at mips.com>
> Subject: Re: [LLVMdev] LLVM Language Reference Strictness
> To: <llvmdev at cs.uiuc.edu>
> Message-ID: <4EA050BE.70006 at mips.com>
> Content-Type: text/plain; charset="ISO-8859-1"; format=flowed
> 
> On 10/20/2011 07:42 AM, Duncan Sands wrote:
>>> For the level of specificity you're looking for, just the source code itself. The LLVM IR language documentation is not, and isn't intended to be, a true language standard document in the same way that the C or C++ standards are. For any given case, check the docs first, and if your question isn't answered there, check the source code of the target(s) you're interested in.
>> And once you've understood, submit a doc patch explaining it :)
>> 
>> Ciao, Duncan.
>> _______________________________________________
>> LLVM Developers mailing list
>> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
> I'm in the process of writing a formal spec for LLVM IR.
> 
> I have a lot of the grammar done and a tool for checking the grammar for 
> completeness
> and generating cross reference and such. I'm using a nice extended 
> regular expression form of BNF.
> 
> My intent is to open source it at google code when it's done but if 
> other people want to help me with this project I could do that now.
> 
> About 80% of it is done.
> 
> I have documented it mostly from reading the source code.
> 
> Beyond just using the grammar to document things I have some tools in 
> mind later for specifying various optimizations using grammatical 
> transformations that are then translated in C++ code for LLVM.
> 
> I think also that I could replace the adhoc parser in LLVM with 
> something better once we have a clean grammar for it using a parser 
> generator tool.
> 
> My little tool can be expanded to be a parser generator tool. I've 
> written regular expression YACC type equivalents and can do any of those 
> type. I probably will do a special one for this project because YACC is 
> a dinosaur and some of the newer ones are not exactly what I want either.
> 
> I would like to see the many adhoc parsers in LLVM get replaced by ones 
> generated from grammars.
> 
> Reed