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

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

One possible answer is to see if these programs are clean as far as tis-interpeter can see. If no, then we get more confirmation that something is wrong. If yes, then we can use C-Reduce to minimize under the criterion that KCC thinks there's a problem but tis-interpreter does not. 

John



On 5/14/19 4:21 PM, Xuejun Yang 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,
-Xuejun
On Tue, May 14, 2019 at 7:06 AM John Regehr <regehr@cs.utah.edu <mailto:regehr@cs.utah.edu>> wrote: 

    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
    <mailto:radu.ometita@iohk.io>>
    To:     John Regehr <regehr@cs.utah.edu <mailto:regehr@cs.utah.edu>>
    CC:     Chris Hathhorn <chris.hathhorn@runtimeverification.com
    <mailto:chris.hathhorn@runtimeverification.com>>, Philip
    Wadler <wadler@inf.ed.ac.uk <mailto:wadler@inf.ed.ac.uk>>, Philip
    Wadler <philip.wadler@iohk.io <mailto: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://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
    <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>