On Sat, Jun 8, 2019 at 11:44 AM Xuejun Yang <nitsnow@gmail.com> wrote:
FWIW, I figured out the kcc message "program2.c:627:6" actually means line 627 and the 6th token.I have logged https://github.com/csmith-project/csmith/issues/74 for this even though I am not entirely sure this is a Csmith bug. @John Regehr what do you think?thanks again for the test cases,-XuejunOn Wed, Jun 5, 2019 at 11:58 PM Xuejun Yang <nitsnow@gmail.com> wrote:Thanks Radu for the verification.Seems the only remaining issue is accessing volatile through a non-volatile pointer,as in seed 2557024983 (see attached):Trying to access an object declared with volatile type through a non-volatile lvalue:
> in func_7 at program2.c:627:6
in func_1 at program2.c:323:5
in main at program2.c:1894:5However, I have a hard time to pinpoint which pointer is pointing to a volatile object at line 627. I need some education here regarding the kcc output: does "program2.c:627:6" means line 627 and column 6, or line 627 and the 6th token? Anyways, I wish kcc was more specific on which variable caused the undefined behavior.If someone can identify the "violating" pointer, please let me know. It definitely makes debugging much easier.Thanks,-XuejunOn Wed, Jun 5, 2019 at 6:40 AM Radu Ometita <radu.ometita@iohk.io> wrote:And the attachment..
Radu Ometita
FUNCTIONAL COMPILERS ENGINEER | CLUJ-NAPOCA
Website: www.iohk.io
Skype: rganogork
Twitter: @raduom
PGP Key ID: 0xD82CE70A![Twitter]()
![Github]()
![LinkedIn]()
![YouTube]()
![Facebook]()
![Reddit]()
![Meetup]()
On Jun 5 2019, at 4:30 pm, Radu Ometita <radu.ometita@iohk.io> wrote:Hi Xuejun.I re-checked the generated files using the master branch of Csmith and noticed a significant reduction of undefined behaviours, but there are still some left.I re-generated the program as program2.c and you can find the output from running the second program in kcc_exec2.txt. One of the programs is free of undefined behaviours.Thanks a lot,Radu OmetitaFUNCTIONAL COMPILERS ENGINEER | CLUJ-NAPOCAWebsite: www.iohk.ioSkype: rganogorkTwitter: @raduomPGP Key ID: 0xD82CE70AOn Jun 4 2019, at 6:31 am, Xuejun Yang <nitsnow@gmail.com> wrote:Hi Radu,The issues are fixed now on the master branch. Please try it again and let us know if there are any remaining undefined behaviors in the generated programs.Thanks,-XuejunOn Sun, May 19, 2019 at 3:47 PM Xuejun Yang <nitsnow@gmail.com> wrote:Hi Radu, thanks for reporting the problem.I have logged two issues: https://github.com/csmith-project/csmith/issues/70 and https://github.com/csmith-project/csmith/issues/71 for the problems you reported. Both are related to unions. I welcome you to try it out after them are fixed to see if I covered all. ETA: one week.Thanks again,-XuejunOn Thu, May 16, 2019 at 1:58 AM Radu Ometita <radu.ometita@iohk.io> wrote:Hi Xuejun!I am not sure if you have access to the original message exchange, but I provided this information to John.Here is the relevant part, quoted from that email:---In directory 4070134944, in the file kcc_exec.txt, that contains output from running the program compiled with kcc we find the following (first) error:Type of lvalue (int) not compatible with the effective type of the object being accessed (union U7):> in func_57 at program.c:1235:9in func_28 at program.c:683:6in func_1 at program.c:254:6in main at program.c:1595:5Undefined behavior (UB-EIO10):see C11 section 6.5:7 http://rvdoc.org/C11/6.5see C11 section J.2:1 item 37 http://rvdoc.org/C11/J.2see CERT-C section EXP39-C http://rvdoc.org/CERT-C/EXP39-Csee MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1Another example for the same file is:Indeterminate value used in an _expression_:> in func_57 at program.c:1235:9in func_28 at program.c:683:6in func_1 at program.c:254:6in main at program.c:1595:5Undefined behavior (UB-CEE2):see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9see C11 section 6.8 http://rvdoc.org/C11/6.8see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-Csee MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1And an example from a different program (in directory 316048733/kcc_exec.txt):Type of lvalue (volatile const unsigned int) not compatible with the effective type of the object being accessed (union U5 [1] [1]):> in main at program.c:1629:13Undefined behavior (UB-EIO10):see C11 section 6.5:7 http://rvdoc.org/C11/6.5see C11 section J.2:1 item 37 http://rvdoc.org/C11/J.2see CERT-C section EXP39-C http://rvdoc.org/CERT-C/EXP39-Csee MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1Please feel free to ask any other questions that might help figure out this discrepancy.---Best regards,Radu OmetitaFUNCTIONAL COMPILERS ENGINEER | CLUJ-NAPOCAWebsite: www.iohk.ioSkype: rganogorkTwitter: @raduomPGP Key ID: 0xD82CE70AOn May 15 2019, at 1:21 am, Xuejun Yang <nitsnow@gmail.com> wrote:Hi Radu,Free of undefined behaviors is a top promise we made for Csmith. We sure will fix it if the problem in on our end. It will be super helpful if you can pinpoint to the exact undefined behaviors in the generated code.Thanks,-XuejunOn Tue, May 14, 2019 at 7:06 AM John Regehr <regehr@cs.utah.edu> wrote:Hi Xuejun et al.,Please see the attached Csmith-generated programs and some associateddefect reports. The claim is that Csmith is emitting ill-formedprograms. We should try to figure out what's going on here, and whetherwe want to fix things.John-------- Forwarded Message --------Subject: Re: KCC, CSmith and undefined behaviour questions.Date: Tue, 7 May 2019 19:25:41 +0300From: Radu Ometita <radu.ometita@iohk.io>To: John Regehr <regehr@cs.utah.edu>CC: Chris Hathhorn <chris.hathhorn@runtimeverification.com>, PhilipWadler <wadler@inf.ed.ac.uk>, Philip Wadler <philip.wadler@iohk.io>Hi everyone!I am coming back with some specific cases where KCC detects undefinedbehaviours for C code generated with CSmith (version 2.3.0).Reading the CSmith paper I found the following paragraph (section 2.2):"The C99 language [11] has 191 undefined behaviors—e.g., dereferencing anull pointer or overflowing a signed integer—that destroy the meaning ofa program ... Programs emitted by Csmith must avoid all of thesebehaviors or, in certain cases such as argument-evaluation order, beindependent of the choices that will be made by the compiler. Manyundefined and unspecified behaviors can be avoided structurally bygenerating programs in such a way that problems never arise. However, anumber of important undefined and unspecified behaviors are not easy toavoid in a structural fashion. In these cases, Csmith solves the problemusing static analysis and by adding run-time checks to the generated code"The three runs I am sending appear to be a counter-example to thepaper's claim. Do you agree?I have attached an archive where each directory is the seed used togenerate the program.c file, and there are <compiler>_compile.txt and<compiler>_exec.txt with the output from compilation and execution.Best regards,*Radu Ometita*FUNCTIONAL COMPILERS ENGINEER | CLUJ-NAPOCAWebsite: www.iohk.io <http://iohk.io>Skype: rganogorkTwitter: @raduomPGP Key ID: 0xD82CE70AInput Output <http://iohk.io>Twitter <https://twitter.com/InputOutputHK> Github<https://github.com/input-output-hk> LinkedIn<https://www.facebook.com/iohk.io/> Reddit<https://www.reddit.com/r/cardano/> Meetup<https://www.meetup.com/pro/cardano/> CardanoAnnouncementsOn May 7 2019, at 7:25 am, John Regehr <regehr@cs.utah.edu> wrote:There is no way to answer this question abstractly.However, it should be easy to answer it by looking at the behaviors ofthe generated program, the alarms emitted by KCC, and the Cstandard(s).JohnOn 5/6/19 2:15 PM, Radu Ometita wrote:Hi everyone,In our test runs, KCC detects `errors` (undefined behaviours *and*constraint violations) in 80% of the C code generated by CSmith,although the CSmith paper claims that CSmith avoids undefinedbehaviours. We currently have a few hypotheses, but we wouldappreciateyour help with deciding which one is most probably true.(1) KCC yields false positives (that is, it labels well-definedcode ashaving undefined behaviours) .(2) CSmith does not check for constraint violations whengenerating code.(3) CSmith does not avoid all possible undefined behaviours.Best regards,*Radu Ometita*FUNCTIONAL COMPILERS ENGINEER | CLUJ-NAPOCAWebsite: www.iohk.io <http://iohk.io>Skype: rganogorkTwitter: @raduomPGP Key ID: 0xD82CE70AInput Output <http://iohk.io>Twitter <https://twitter.com/InputOutputHK> Github<https://github.com/input-output-hk> LinkedIn<https://www.facebook.com/iohk.io/> Reddit<https://www.reddit.com/r/cardano/> Meetup<https://www.meetup.com/pro/cardano/> CardanoAnnouncements