llvm dev - Oct 2011 - [LLVMdev] Formal spec for LLVM IR (Was: LLVM Language Reference Strictness)

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

Hi VIkram,

Here is roughly my plan.

The first thing is a grammar and English description.

With this I can produce a more complete reference manual and have 
grammar cross reference and such.

The extended bnf to write the grammar is variant of the one that 
Pennello and Deremer used in their Translator Writing System (TWS).

Then I want to implement a basic TWS so that this LLVM language can be 
parsed with a tool and not with ad hoc recursive descent. I've started 
this but have done just enough so that I can check the grammar and make 
sure all the non terminals are defined and such and produce cross reference.
I thought about using YACC or ANTLR or some other tools but non of them 
were what I wanted. YACC is too old and ANTLR has too much other 
baggage, doesn't really work well with C++ and is a whole other project. 
This tool is just for LLVM. If the tool can be used for other things 
later, that would be okay but I'm not interested in starting another 
general parser generator project.

The next step is to augment the grammar meta language (of the TWS) so 
that I can write high level grammar transformations and other processing 
on LLVM IR and translate them into C++ code for LLVM. I would like to be 
able to express optimizations that look like they would in a paper and 
not have to be shackled by the expressive limitations of C++.

I also want to augment the grammar so that I can insert descriptive 
information in it with the eventual ability to produce the reference 
manual from the augmented grammar.

I'm still at the beginning stage which is a complete grammar but that 
part is 80% or more done.
I could finish it in a week if I could find a week.

I'm not really sure what they are doing with the formal semantics so I 
can't say if we are trying to do the same things.

I'm mostly interesting on nailing down the syntax and semantics of LLVM 
IR and to start to develop some tools that let it be manipulated in a 
higher level and more intuitive way then just writing C++ code.

Reed


On 10/20/2011 11:27 AM, Vikram Adve wrote:
> 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
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev