Hi Xuejun et al.,Please see the attached Csmith-generated programs and some associated defect reports. The claim is that Csmith is emitting ill-formed programs. We should try to figure out what's going on here, and whether we want to fix things.
John -------- Forwarded Message -------- Subject: Re: KCC, CSmith and undefined behaviour questions. Date: Tue, 7 May 2019 19:25: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!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://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>
On 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 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://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>
Attachment:
example.tar.gz
Description: Binary data