search

kframework / llvm-semantics

Formal semantics of LLVM IR in K
44 stars 9 forks source link

add syntax of LLVM #1

Closed liyili2 closed 9 years ago

liyili2 commented 9 years ago

@grosu, please review.

grosu commented 9 years ago

Liyi, please give very good names to your commits, because they will be used many times in the future; for example, when writing changelogs. This name add syntax of LLVM is not such a good name because it indicates that you add the entire syntax of LLVM. Something like Add preliminary LLVM syntax, or Starting to add LLVM syntax would fit better.

Grigore

From: Liyi Li [notifications@github.com] Sent: Tuesday, December 23, 2014 3:06 PM To: kframework/llvm-semantics Subject: [llvm-semantics] add syntax of LLVM (#1)

You can merge this Pull Request by running

git pull https://github.com/kframework/llvm-semantics java_engine

Or view, comment on, or merge it at:

https://github.com/kframework/llvm-semantics/pull/1

Commit Summary

File Changes

Patch Links:

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/llvm-semantics/pull/1.

liyili2 commented 9 years ago

I will remember your suggestion and make the comment look good next time.

Liyi Li

On Tue, Dec 23, 2014 at 3:27 PM, Grigore Rosu notifications@github.com wrote:

Liyi, please give very good names to your commits, because they will be used many times in the future; for example, when writing changelogs. This name add syntax of LLVM is not such a good name because it indicates that you add the entire syntax of LLVM. Something like Add preliminary LLVM syntax, or Starting to add LLVM syntax would fit better.

Grigore

From: Liyi Li [notifications@github.com] Sent: Tuesday, December 23, 2014 3:06 PM To: kframework/llvm-semantics Subject: [llvm-semantics] add syntax of LLVM (#1)

You can merge this Pull Request by running

git pull https://github.com/kframework/llvm-semantics java_engine

Or view, comment on, or merge it at:

https://github.com/kframework/llvm-semantics/pull/1

Commit Summary

  • add syntax of LLVM

File Changes

Patch Links:

— Reply to this email directly or view it on GitHub< https://github.com/kframework/llvm-semantics/pull/1>.

— Reply to this email directly or view it on GitHub https://github.com/kframework/llvm-semantics/pull/1#issuecomment-68000399 .

grosu commented 9 years ago

Liyi, I just realized that you probably were waiting for me to merge this pull request here. Please never do that again, if I do not react in 2-3 days, ping me immediately.

So your one syntax file does not obey our K conventions. For example, there is no copyright. Also, I'd like to see some very basic comments there, saying that this is the syntax of LLVM as defined in the manual, and provide a link to it in the comments in the syntax file. Finally, why -X and not -EXTENDED if that's what you mean? Is -X what they use in the LLVM manual, or that is your invention? You said you tested it with LLVM programs? Where are they? They should also be in the repo. And how can you test only the extended syntax, without the rest of the syntax? Shouldn't you start with the basic syntax first? Finally, looking into the repository I can still see all the old stuff, 2-3 years old. Haven't we agreed that we start fresh, first defining the syntax, parsing all the existing programs, then we move on the semantics, etc?

liyili2 commented 9 years ago

I will address all these problems. The test programs are in the test directory. I thought you want me to reuse their semantics and make their semantics to fit the newest Java backend of K, then line up with the new syntax we are defining. I am working on making the LLVM semantics work with the Java backend of K. If you want me to define a whole new LLVM semantics, I can throw all old things.

Grigore Rosu notifications@github.com wrote:

Liyi, I just realized that you probably were waiting for me to merge this pull request here. Please never do that again, if I do not react in 2-3 days, ping me immediately.

So your one syntax file does not obey our K conventions. For example, there is no copyright. Also, I'd like to see some very basic comments there, saying that this is the syntax of LLVM as defined in the manual, and provide a link to it in the comments in the syntax file. Finally, why -X and not -EXTENDED if that's what you mean? Is -X what they use in the LLVM manual, or that is your invention? You said you tested it with LLVM programs? Where are they? They should also be in the repo. And how can you test only the extended syntax, without the rest of the syntax? Shouldn't you start with the basic syntax first? Finally, looking into the repository I can still see all the old stuff, 2-3 years old. Haven't we agreed that we start fresh, first defining the syntax, parsing all the existing programs, then we move on the semantics, etc?

Reply to this email directly or view it on GitHub: https://github.com/kframework/llvm-semantics/pull/1#issuecomment-68264582

liyili2 commented 9 years ago

@grosu, would you mind to review the llvm-syntax-real.k file and see if you are satisfied.