[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[csmith-dev] Fwd: Re: KCC, CSmith and undefined behaviour questions.



A few more details.


-------- Forwarded Message --------
Subject: 	Re: KCC, CSmith and undefined behaviour questions.
Date: 	Mon, 13 May 2019 23:09:41 +0300
From: 	Radu Ometita <radu.ometita@iohk.io>
To: 	John Regehr <regehr@cs.utah.edu>
CC: Chris Hathhorn <chris.hathhorn@runtimeverification.com>, Philip Wadler <wadler@inf.ed.ac.uk>, Philip Wadler <philip.wadler@iohk.io>



Hi everyone!

We care about any statement that a program contains undefined behaviours in any of the attached programs. Here are some examples:

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:9
         in func_28 at program.c:683:6
         in func_1 at program.c:254:6
         in main at program.c:1595:5

     Undefined behavior (UB-EIO10):
         see C11 section 6.5:7 http://rvdoc.org/C11/6.5
         see C11 section J.2:1 item 37 http://rvdoc.org/C11/J.2
         see CERT-C section EXP39-C http://rvdoc.org/CERT-C/EXP39-C
         see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Another example for the same file is:

Indeterminate value used in an expression:
       > in func_57 at program.c:1235:9
         in func_28 at program.c:683:6
         in func_1 at program.c:254:6
         in main at program.c:1595:5

     Undefined behavior (UB-CEE2):
         see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4
         see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9
         see C11 section 6.8 http://rvdoc.org/C11/6.8
         see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2
         see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C
         see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9
         see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

And 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:13

     Undefined behavior (UB-EIO10):
         see C11 section 6.5:7 http://rvdoc.org/C11/6.5
         see C11 section J.2:1 item 37 http://rvdoc.org/C11/J.2
         see CERT-C section EXP39-C http://rvdoc.org/CERT-C/EXP39-C
         see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Please feel free to ask any other questions that might help figure out this discrepancy.

Thanks a lot for your help,


*Radu Ometita*
FUNCTIONAL COMPILERS ENGINEER | CLUJ-NAPOCA, ROMANIA

Website: www.iohk.io <http://iohk.io>
Skype: rganogork
Twitter: @raduom
PGP Key ID: 0xD82CE70A <http://pgp.mit.edu/pks/lookup?op=get&search=0x2C79BBB4D82CE70A>

Input Output <http://iohk.io>

Twitter <https://twitter.com/InputOutputHK> Github <https://github.com/input-output-hk> LinkedIn <https://www.linkedin.com/company/input-output-global>


This e-mail and any file transmitted with it are confidential and intended solely for the use of the recipient(s) to whom it is addressed. Dissemination, distribution, and/or copying of the transmission by anyone other than the intended recipient(s) is prohibited. If you have received this transmission in error please notify IOHK immediately and delete it from your system. E-mail transmissions cannot be guaranteed to be secure or error free. We do not accept liability for any loss, damage, or error arising from this transmission

On 10 May 2019, at 17:40, John Regehr <regehr@cs.utah.edu <mailto:regehr@cs.utah.edu>> wrote:

Hi Radu, there's a lot of stuff in the tarball you sent. If you don't mind, please identify something in particular that we should look at.

John


On 5/7/19 10:25 AM, Radu Ometita wrote:
Hi everyone!
I am coming back with some specific cases where KCC detects undefined behaviours 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 a null pointer or overflowing a signed integer—that destroy the meaning of a program ... Programs emitted by Csmith must avoid all of these behaviors or, in certain cases such as argument-evaluation order, be independent of the choices that will be made by the compiler. Many undefined and unspecified behaviors can be avoided structurally by generating programs in such a way that problems never arise. However, a number of important undefined and unspecified behaviors are not easy to avoid in a structural fashion. In these cases, Csmith solves the problem using 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 the paper's claim. Do you agree? I have attached an archive where each directory is the seed used to generate 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-NAPOCA
Website:www.iohk.io <http://www.iohk.io/><http://iohk.io <http://iohk.io/>>
Skype: rganogork
Twitter: @raduom
PGP Key ID: 0xD82CE70A
Input Output <http://iohk.io <http://iohk.io/>>
Twitter <https://twitter.com/InputOutputHK> Github <https://github.com/input-output-hk> LinkedIn <https://www.linkedin.com/company/input-output-global> YouTube <https://www.youtube.com/channel/UCBJ0p9aCW-W82TwNM-z3V2w> Facebook <https://www.facebook.com/iohk.io/> Reddit <https://www.reddit.com/r/cardano/> Meetup <https://www.meetup.com/pro/cardano/> CardanoAnnouncements <https://t.me/CardanoAnnouncements> On May 7 2019, at 7:25 am, John Regehr <regehr@cs.utah.edu <mailto: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 of
   the generated program, the alarms emitted by KCC, and the C standard(s).
   John
   On 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 undefined
       behaviours. We currently have a few hypotheses, but we would
       appreciate
       your help with deciding which one is most probably true.
       (1) KCC yields false positives (that is, it labels well-defined
       code as
       having undefined behaviours) .
       (2) CSmith does not check for constraint violations when
       generating code.
       (3) CSmith does not avoid all possible undefined behaviours.
       Best regards,
       *Radu Ometita*
       FUNCTIONAL COMPILERS ENGINEER | CLUJ-NAPOCA
       Website: www.iohk.io <http://www.iohk.io> <http://iohk.io>
       Skype: rganogork
       Twitter: @raduom
       PGP Key ID: 0xD82CE70A
       Input Output <http://iohk.io>
       Twitter <https://twitter.com/InputOutputHK> Github
       <https://github.com/input-output-hk> LinkedIn
       <https://www.linkedin.com/company/input-output-global> YouTube
       <https://www.youtube.com/channel/UCBJ0p9aCW-W82TwNM-z3V2w> Facebook
       <https://www.facebook.com/iohk.io/> Reddit
       <https://www.reddit.com/r/cardano/> Meetup
       <https://www.meetup.com/pro/cardano/> CardanoAnnouncements
       <https://t.me/CardanoAnnouncements>