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

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

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,
-Xuejun


On 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,

-Xuejun

On 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: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.
---

Best regards,





Radu Ometita
FUNCTIONAL COMPILERS ENGINEER | CLUJ-NAPOCA

Website: www.iohk.io
Skype: rganogork
Twitter: @raduom
PGP Key ID: 0xD82CE70A


Input Output

Twitter Github LinkedIn YouTube Facebook Reddit Meetup CardanoAnnouncements
On 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,
-Xuejun

On 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 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

Skype: rganogork
Twitter: @raduom
PGP Key ID: 0xD82CE70A


Input Output <http://iohk.io>

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.facebook.com/iohk.io/> Reddit
         <https://www.reddit.com/r/cardano/> Meetup
         <https://www.meetup.com/pro/cardano/> CardanoAnnouncements