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

Re: [csmith-dev] Floating-point support in csmith



Professor Regehr,

Thanks a lot for your comment. I will use C-Reduce and check as you've said. I've not used this tool before but I think I can make the attempt.

However, I do not know the status of UB detection of FP programs. Can anyone tell me how to do this?

Thanks!

Shafiul

 

On Fri, Nov 6, 2015 at 4:07 PM, John Regehr <regehr@cs.utah.edu> wrote:
Shafiul, one thing you can do is look for a possible wrong code bug in a floating-point program reduce it using C-Reduce.  I'm not sure anyone has done this lately.  The tiny resulting test case will show you right away at least one problem that needs to be solved (assuming it does not reveal a compiler bug).

What's our current story for UB detection of FP programs: Frama-C in interpreter mode as usual?

John




On 11/6/15 11:03 PM, Shafiul Azam wrote:
Thank you All very much for responses! To summarize, csmith with --float
can be used to detect crash bugs for the moment, and should NOT be used
for wrong code bugs. Please correct me if I got it wrong.

Sincerely,
Shafiul



On Wed, Nov 4, 2015 at 3:23 PM, John Regehr <regehr@cs.utah.edu
<mailto:regehr@cs.utah.edu>> wrote:

           - Floating-point support was introduced in version 2.2.0
        according to
        the release note [1]. Floating point support must be turned on
        passing
        --float command-line option. This note acknowledges work of Dr.
        Alastair
        Donaldson for the initial implementation.


    Yes, please check with Ally, he and his people have been doing
    this.  I think basically all of us are interested but it's been a
    matter of making time to work on it.

           - I conducted a run of csmith 2.2.0 with --float argument on
        Ubuntu
        10.04 (gcc 4.4.3). Number of crash-programs is significantly
        more now.
        Running csmith without --float found 3 crash-bugs, while running
        with
        --float found more than 300 crash-bugs within the (almost) same
        runtime.


    Nice.  There are a few things going on here.  As Yang observes,
    there's some number <300 of bugs that are getting triggered multiple
    times.  To find the true set of bugs you can start to report them,
    one at a time.

    Another thing that is going on is that GCC has built up a huge
    resistance to Csmith.   We've beaten it up for years now.  We have
    not beaten on its FP code so of course there's more low-hanging fruit.

        I am interested to know current support-level for floating
        points, any
        limitations and any future works you plan regarding float-point
        support.

        I'll also appreciate any source which explains current support
        level of
        floating-point in csmith.


    Hopefully Ally will chime in.  You should the source code too,
    there's not that much that deals with FP, as far as I know.

    John