search

kframework / llvm-semantics

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

empty the llvm folder and leave only the llvm test cases in the folder #4

Closed liyili2 closed 9 years ago

liyili2 commented 9 years ago

@grosu, please review

grosu commented 9 years ago

@liyili2 this is pretty much what we discussed, namely to start from scratch, keeping only the tests from the old LLVM. The first step is to define the concrete syntax of LLVM in K directly, and be able to parse all these LLVM tests. However, before that, I think you should spend a bit of time trying to understand where the various tests come from, and add a small README's to each category saying where they come from. This will help us in the future. If you cannot figure it out, ask Chucky and David. Note that almost each file has a preamble of the form

; ModuleID = '/home/david/src/c-semantics/tests/unitTests/arithConversions.c'

I think you want to also put your hands on those C programs, and put them in the repository as well (but in a different folder following the same structure). These will be very useful when you will define the LLVM compiler in K later on.

liyili2 commented 9 years ago

@grosu, I added all c-test cases in a ctests directory.

grosu commented 9 years ago

I don't understand the README in llvm-semantics/tests/needs-attention. It's saying that those are "all test cases which are generated by c programs that are in the c-semantics/tests directory". This cannot be correct, because there are a lot more C programs in c-semantics/tests. Also, please write C instead of c.

grosu commented 9 years ago

Typo in the README file at llvm-semantics/tests/vellvm/

grosu commented 9 years ago

In the top README file, you say "The k2 branch is compatible with K version 2.6-2.7." Is this the semantics of David and Chucky which is now in the llvm-semantics-old repo? If yes, then I think you should remove this branch all together and simply put a link in the README file of llvm-semantics to the old semantics. Regardless, you should still put a link to it there, saying that the new semantics roots into that old one (and give credit to David and Chucky for it). Then, in the rest of the llvm-semantics-repo refer to it as "llvm-semantics-old" instead of "The previous LLVM semantics defined by Chucky and David".

grosu commented 9 years ago

Liyi, please use clear sentences in these public READMEs. Lots of people are going to read them. If not sure, have somebody else help you with that. This README at llvm-semantics/tests/c-semantics-tests/ is completely misleading:

This directory contains all test cases which are generated by c programs that are in the c-semantics/tests directory.

The C (again, capital C) programs in the c-semantics/tests generate no test cases. And are they really ALL of them? I thought that some of them went to "needs-attention" and even other places, not sure. I would rephrase as follows:

Here are test cases corresponding to C programs that are in the c-programs/c-semantics directory.

You are going to collect lots of C programs in this project, so I suggest that you create a top folder, named c-programs. In fact, rename your current "ctests" to "c-programs". Then rename the "ctests/c-semantics-tests" to "c-programs/c-semantics".

Also, now that you have the c-programs folder, the folder llvm-semantics/tests/c-tests/ does not make much sense there. In fact, it is a duplication of c-programs/c-tests anyway. PLEASE revise the English in the README of llvm-semantics/tests/c-tests/ and add it as the README of c-programs/c-tests.

grosu commented 9 years ago

There is some very meaningful information in https://github.com/kframework/llvm-semantics-old/tree/master/tests. Have you decided to eliminate it on purpose, because you believe it is unnecessary, or you just forgot? I think it is very very important to know how to produce LLVM files. My suggestion is for you to redo what's explained there and re-generate yourself all those LLVM files; maybe even use a diff program to make sure that you are generating the right files. Then, once you do that, write a similar text as that at https://github.com/kframework/llvm-semantics-old/tree/master/tests and add it to our new README. Keep it in mind that we are going to generate LLVM files over and over again, so we want to make it crystal clear how this will be done, to spend no time in the future to re-do it.

grosu commented 9 years ago

Probably this will be solved by what I proposed in my previous message, but just in case I re-repeat it: Many files start with a line of the form

; ModuleID = '/home/david/src/c-semantics/tests/cil/test15.c'

That path is wrong. We should only use paths that exist in our repo.

liyili2 commented 9 years ago

@grosu, I have already done the things you suggested and you can review them again.

For the issue that you asked me to delete all the old-semantics, I will do it after you merge this pull-request into master branch. After that, the master branch will only contain the things in java_engine_empty_new_start branch. I deleted two other branchs (java_engine and java_engine1 branchs). The only other branch which belongs to the old-semantics of LLVM is the K2 branch. If you want, I can delete that also.

Liyi Li

liyili2 commented 9 years ago

@grosu , after you merge this branch with the master branch, I will remove this branch. I have already removed the K2 branch and there is no any old branch in this repo.

grosu commented 9 years ago

I still have some comments, mainly related to the incorrect paths you put now in all the .ll files to their original .c versions, but let's not delay this anymore. Merge this and move on.