Need info about ProgramState, SymbolReaper, etc

Hello!

I am trying to figure out how to make clang warn for this code:

void f(int x) {
    int a[10];
    if (x >= 20)
        a[x] = 7;
}

If the "7" is replaced with "x" then there is a warning.

As far as I see, ArrayBoundChecker works as it should. I believe the problem is related with the ProgramState.

The ProgramState when ArrayBoundChecker::checkLocation is called for 'a[x] = x':

Expressions:
(0x5c2f900,0x5bdb478) a[x] : &element{a,reg_$0<x>,int}
(0x5c2f900,0x5bdb4c8) x : reg_$0<x>
(0x5c2f900,0x5c24930) a[x] = x : reg_$0<x>
Ranges of symbol values:
reg_$0<x> : { [20, 2147483647] }

The ProgramState when ArrayBoundChecker::checkLocation is called for 'a[x] = 7':

Expressions:
(0x5c2f900,0x5bdb340) x : &x
(0x5c2f900,0x5bdb388) x : reg_$0<x>
Ranges are empty.

I believe the "Ranges are empty" message is a problem. I have tried to track down why the ranges are empty. The ranges is removed somehow in the function ProgramStateManager::removeDeadBindings(). I don't understand why "7" will make the ranges empty and "x" will not.. but I assume that the bug is not located in this function but somehow somewhere else (earlier?).

In ProgramStateManager::removeDeadBindings(), the ProgramState will initially be:

Expressions:
(0x5c2f900,0x5bdb3c8) a : &a
(0x5c2f900,0x5bdb3f0) x : &x
(0x5c2f900,0x5bdb448) a : &element{a,0 S32b,int}
(0x5c2f900,0x5bdb460) x : reg_$0<x>
(0x5c2f900,0x5bdb478) a[x] : &element{a,reg_$0<x>,int}
Ranges of symbol values:
reg_$0<x> : { [20, 2147483647] }

After this statement:
  ProgramStateRef Result = getPersistentState(NewState);
The 'Result' is:

Expressions:
(0x5c2f900,0x5bdb478) a[x] : &element{a,reg_$0<x>,int}
Ranges of symbol values:
reg_$0<x> : { [20, 2147483647] }

The next statement is:
  return ConstraintMgr->removeDeadBindings(Result, SymReaper);

Here the ranges are removed.

Do you think I am on the right track? I feel that I need some help to get further. I can't solve this on my own. Could anybody tell me how I should proceed.

Best regards,
Daniel Marjamäki

..................................................................................................................
Daniel Marjamäki Senior Engineer
Evidente ES East AB Warfvinges väg 34 SE-112 51 Stockholm Sweden

Mobile: +46 (0)709 12 42 62
E-mail: Daniel.Marjamaki@evidente.se

www.evidente.se

Hi Daniel,

The ProgramState doesn’t need to track the value ‘7’ because that’s easily recoverable lazily. If you look at the logic in Environment (which is a mapping from expressions to symbolic values), you will see that there is logic for lazily getting the number ‘7’ without the need to explicitly track that in the ProgramState.

In particular:

SVal Environment::getSVal(const EnvironmentEntry &Entry,
                          SValBuilder& svalBuilder) const {

// SNIP

  case Stmt::IntegerLiteralClass:
    // Known constants; defer to SValBuilder.
    return svalBuilder.getConstantVal(cast<Expr>(S)).getValue();
  }
}

When you say “there is a warning”, are you using an unmodified ArrayBoundChecker, or does this involve new logic you have written?

Ted

Hello Ted!

Thanks for your response.

The ProgramState doesn’t need to track the value ‘7’ because that’s easily recoverable lazily.

I am afraid I am confused.

I don't really care about RHS. If I need to track '7' somehow.. then I don't understand why.

To clarify.. the ProgramState is used to track variables.. right?

When I dump ProgramState I can get such output:

Expressions:
(0x5c2f900,0x5bdb478) a[x] : &element{a,reg_$0<x>,int}
(0x5c2f900,0x5bdb4c8) x : reg_$0<x>
(0x5c2f900,0x5c24930) a[x] = x : reg_$0<x>
Ranges of symbol values:
reg_$0<x> : { [20, 2147483647] }

This output above means that the variable 'x' currently has the min value 20 .. right? I hope that is what it means.

The ArrayBoundsChecker uses ProgramState to determine if a variable, for example 'x', is out of bounds ... right?

The ArrayBoundsChecker does not have fundamental problems with 'a[x] = 7'. For example:

void f(int x) {
    int a[10];
    if (x == 20)
        a[x] = 7;
}

The output is:
a.c:5:14: warning: Access out-of-bound array element (buffer overflow)
        a[x] = 7;
        ~~~~ ^

This is good.

But then, when I change the '==' to '>=' then no warning is reported.

void f(int x) {
    int a[10];
    if (x >= 20)
        a[x] = 7;
}

I have the feeling that you have trouble reproducing.

I use this command line:
clang -cc1 -analyze -analyzer-checker=alpha,core a.c

If I need to use some other flags then please let me know.

When you say “there is a warning”, are you using an unmodified ArrayBoundChecker, or does this involve new logic you have written?

This happens both with the latest release (I've installed the official windows binaries) and with svn top (compiled by myself, both in windows and linux).

Best regards,
Daniel Marjamäki