[cfe-dev] Need info about ProgramState, SymbolReaper, etc

[Daniel Marjamäki]

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 at evidente.se

www.evidente.se