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

[Ted Kremenek]

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

On Feb 26, 2014, at 9:43 AM, Daniel Marjamäki <Daniel.Marjamaki at evidente.se> wrote:

> 
> 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
> 
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev