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

Re: [creduce-dev] reduction using dynamic information

Yang, that would be awesome if you could prototype this! Of course I'll do the perl side (which will be a slight pain since C-Reduce has to be taught to compile and run the program). Your design sounds good. We're definitely interested in the low-hanging fruit here, no need to worry about changing the behavior of programs in corner cases.

I have two small tweaks to suggest. We should print the value only once (or else we might get a lot of output for an expression that lives in a loop) and we should make the value easy to recognize in case the program prints other stuff. So perhaps:

  { int tmp1 = expr1;
    static int _creduce_printed = 0;
    if (!_creduce_printed) {
      printf("creduce_value(%d)\n", tmp1);
      _creduce_printed = 1;
    x = foo(tmp1, expr2);}

Also we'll have to add a prototype for printf() to the compilation unit or maybe it's better to simply include stdio.h.

I think this'll be helpful in working around C-Reduce's lack of constant folding and will help eliminate the setup code needed to observe miscompilations in the wild.


On 7/12/16 12:50 AM, Yang Chen wrote:
Hi John,

On 2016-07-11 15:21, John Regehr wrote:

So what I'm looking for is an easy way to enumerate the expressions in
a C/C++ compilation unit and then, for the specified one, rewrite the
program so that the first value taken on by that expression is printed
out. The other thing we need is to replace the expression with its
value -- creating a C-Reduce variant that can be run through the
interestingness test.

Let me try to hack it up this week. I will make this new transformation
follow our existing convention: it will process the expression based on
the counter value passed from the command line. For now, I may put the
following restrictions on the transformation:

  (1) restrict it on C programs;
  (2) print out the value of the expression only if the expression is of
integer or float type (e.g., char, int, float, double, etc);
  (3) a new local variable will be created for each expression of interest;

Item (3) may need more explanation. Assume that we have the following
code snippet (where expr1 is of type int):

  x = foo(expr1, expr2);

the transformation would turn the code into something like:

  { int tmp1 = expr1;
    printf("%d\n", tmp1);
    x = foo(tmp1, expr2);}

The reason is that expr1 may have side-effect. To make the
transformation have as little impact as possible on the original
semantic, expr1 should only be executed once (note that we may still
change the original semantics because expr2 can be executed before expr1
for the unmodified code).

Once we have the value for tmp1, we can use the following command to
replace the expr1 with the value:

  $ clang_delta --transformation=replace-expr --counter=1 --value=123 foo.c

With this command, we would get:

  x = foo(123, expr2);

Can you check if my description meets the requirement? Thanks.

- Yang