zcov: / lib/Checker/BasicConstraintManager.cpp


Files: 1 Branches Taken: 57.8% 37 / 64
Generated: 2010-02-10 01:31 Branches Executed: 68.8% 44 / 64
Line Coverage: 72.9% 70 / 96


Programs: 1 Runs 2897


       1                 : //== BasicConstraintManager.cpp - Manage basic constraints.------*- C++ -*--==//
       2                 : //
       3                 : //                     The LLVM Compiler Infrastructure
       4                 : //
       5                 : // This file is distributed under the University of Illinois Open Source
       6                 : // License. See LICENSE.TXT for details.
       7                 : //
       8                 : //===----------------------------------------------------------------------===//
       9                 : //
      10                 : //  This file defines BasicConstraintManager, a class that tracks simple
      11                 : //  equality and inequality constraints on symbolic values of GRState.
      12                 : //
      13                 : //===----------------------------------------------------------------------===//
      14                 : 
      15                 : #include "SimpleConstraintManager.h"
      16                 : #include "clang/Checker/PathSensitive/GRState.h"
      17                 : #include "clang/Checker/PathSensitive/GRStateTrait.h"
      18                 : #include "clang/Checker/PathSensitive/GRTransferFuncs.h"
      19                 : #include "llvm/Support/raw_ostream.h"
      20                 : 
      21                 : using namespace clang;
      22                 : 
      23                 : 
      24                 : namespace { class ConstNotEq {}; }
      25                 : namespace { class ConstEq {}; }
      26                 : 
      27                 : typedef llvm::ImmutableMap<SymbolRef,GRState::IntSetTy> ConstNotEqTy;
      28                 : typedef llvm::ImmutableMap<SymbolRef,const llvm::APSInt*> ConstEqTy;
      29                 : 
      30                 : static int ConstEqIndex = 0;
      31                 : static int ConstNotEqIndex = 0;
      32                 : 
      33                 : namespace clang {
      34                 : template<>
      35                 : struct GRStateTrait<ConstNotEq> : public GRStatePartialTrait<ConstNotEqTy> {
      36            20131:   static inline void* GDMIndex() { return &ConstNotEqIndex; }
      37                 : };
      38                 : 
      39                 : template<>
      40                 : struct GRStateTrait<ConstEq> : public GRStatePartialTrait<ConstEqTy> {
      41            20450:   static inline void* GDMIndex() { return &ConstEqIndex; }
      42                 : };
      43                 : }
      44                 : 
      45                 : namespace {
      46                 : // BasicConstraintManager only tracks equality and inequality constraints of
      47                 : // constants and integer variables.
      48                 : class BasicConstraintManager
                      866: branch 2 taken
                        0: branch 3 not taken
                        0: branch 7 not taken
                        0: branch 8 not taken
      49              866:   : public SimpleConstraintManager {
      50                 :   GRState::IntSetTy::Factory ISetFactory;
      51                 : public:
      52              866:   BasicConstraintManager(GRStateManager &statemgr, GRSubEngine &subengine)
      53                 :     : SimpleConstraintManager(subengine), 
      54              866:       ISetFactory(statemgr.getAllocator()) {}
      55                 : 
      56                 :   const GRState* AssumeSymNE(const GRState* state, SymbolRef sym,
      57                 :                              const llvm::APSInt& V);
      58                 : 
      59                 :   const GRState* AssumeSymEQ(const GRState* state, SymbolRef sym,
      60                 :                              const llvm::APSInt& V);
      61                 : 
      62                 :   const GRState* AssumeSymLT(const GRState* state, SymbolRef sym,
      63                 :                              const llvm::APSInt& V);
      64                 : 
      65                 :   const GRState* AssumeSymGT(const GRState* state, SymbolRef sym,
      66                 :                              const llvm::APSInt& V);
      67                 : 
      68                 :   const GRState* AssumeSymGE(const GRState* state, SymbolRef sym,
      69                 :                              const llvm::APSInt& V);
      70                 : 
      71                 :   const GRState* AssumeSymLE(const GRState* state, SymbolRef sym,
      72                 :                              const llvm::APSInt& V);
      73                 : 
      74                 :   const GRState* AddEQ(const GRState* state, SymbolRef sym, const llvm::APSInt& V);
      75                 : 
      76                 :   const GRState* AddNE(const GRState* state, SymbolRef sym, const llvm::APSInt& V);
      77                 : 
      78                 :   const llvm::APSInt* getSymVal(const GRState* state, SymbolRef sym) const;
      79                 :   bool isNotEqual(const GRState* state, SymbolRef sym, const llvm::APSInt& V)
      80                 :       const;
      81                 :   bool isEqual(const GRState* state, SymbolRef sym, const llvm::APSInt& V)
      82                 :       const;
      83                 : 
      84                 :   const GRState* RemoveDeadBindings(const GRState* state, SymbolReaper& SymReaper);
      85                 : 
      86                 :   void print(const GRState* state, llvm::raw_ostream& Out,
      87                 :              const char* nl, const char *sep);
      88                 : };
      89                 : 
      90                 : } // end anonymous namespace
      91                 : 
      92                 : ConstraintManager* clang::CreateBasicConstraintManager(GRStateManager& statemgr,
      93              866:                                                        GRSubEngine &subengine) {
      94              866:   return new BasicConstraintManager(statemgr, subengine);
      95                 : }
      96                 : 
      97                 : const GRState*
      98                 : BasicConstraintManager::AssumeSymNE(const GRState *state, SymbolRef sym,
      99             1304:                                     const llvm::APSInt& V) {
     100                 :   // First, determine if sym == X, where X != V.
                      144: branch 1 taken
                     1160: branch 2 taken
     101             1304:   if (const llvm::APSInt* X = getSymVal(state, sym)) {
     102              144:     bool isFeasible = (*X != V);
                        0: branch 0 not taken
                      144: branch 1 taken
     103              144:     return isFeasible ? state : NULL;
     104                 :   }
     105                 : 
     106                 :   // Second, determine if sym != V.
                      323: branch 1 taken
                      837: branch 2 taken
     107             1160:   if (isNotEqual(state, sym, V))
     108              323:     return state;
     109                 : 
     110                 :   // If we reach here, sym is not a constant and we don't know if it is != V.
     111                 :   // Make that assumption.
     112              837:   return AddNE(state, sym, V);
     113                 : }
     114                 : 
     115                 : const GRState *BasicConstraintManager::AssumeSymEQ(const GRState *state,
     116                 :                                                    SymbolRef sym,
     117             1038:                                                    const llvm::APSInt &V) {
     118                 :   // First, determine if sym == X, where X != V.
                       42: branch 1 taken
                      996: branch 2 taken
     119             1038:   if (const llvm::APSInt* X = getSymVal(state, sym)) {
     120               42:     bool isFeasible = *X == V;
                       42: branch 0 taken
                        0: branch 1 not taken
     121               42:     return isFeasible ? state : NULL;
     122                 :   }
     123                 : 
     124                 :   // Second, determine if sym != V.
                      328: branch 1 taken
                      668: branch 2 taken
     125              996:   if (isNotEqual(state, sym, V))
     126              328:     return NULL;
     127                 : 
     128                 :   // If we reach here, sym is not a constant and we don't know if it is == V.
     129                 :   // Make that assumption.
     130              668:   return AddEQ(state, sym, V);
     131                 : }
     132                 : 
     133                 : // These logic will be handled in another ConstraintManager.
     134                 : const GRState *BasicConstraintManager::AssumeSymLT(const GRState *state,
     135                 :                                                    SymbolRef sym,
     136                7:                                                    const llvm::APSInt& V) {
     137                 :   // Is 'V' the smallest possible value?
                        1: branch 5 taken
                        6: branch 6 taken
     138                7:   if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
     139                 :     // sym cannot be any value less than 'V'.  This path is infeasible.
     140                1:     return NULL;
     141                 :   }
     142                 : 
     143                 :   // FIXME: For now have assuming x < y be the same as assuming sym != V;
     144                6:   return AssumeSymNE(state, sym, V);
     145                 : }
     146                 : 
     147                 : const GRState *BasicConstraintManager::AssumeSymGT(const GRState *state,
     148                 :                                                    SymbolRef sym,
     149               84:                                                    const llvm::APSInt& V) {
     150                 : 
     151                 :   // Is 'V' the largest possible value?
                        1: branch 5 taken
                       83: branch 6 taken
     152               84:   if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
     153                 :     // sym cannot be any value greater than 'V'.  This path is infeasible.
     154                1:     return NULL;
     155                 :   }
     156                 : 
     157                 :   // FIXME: For now have assuming x > y be the same as assuming sym != V;
     158               83:   return AssumeSymNE(state, sym, V);
     159                 : }
     160                 : 
     161                 : const GRState *BasicConstraintManager::AssumeSymGE(const GRState *state,
     162                 :                                                    SymbolRef sym,
     163                7:                                                    const llvm::APSInt &V) {
     164                 : 
     165                 :   // Reject a path if the value of sym is a constant X and !(X >= V).
                        0: branch 1 not taken
                        7: branch 2 taken
     166                7:   if (const llvm::APSInt *X = getSymVal(state, sym)) {
     167                0:     bool isFeasible = *X >= V;
                        0: branch 0 not taken
                        0: branch 1 not taken
     168                0:     return isFeasible ? state : NULL;
     169                 :   }
     170                 : 
     171                 :   // Sym is not a constant, but it is worth looking to see if V is the
     172                 :   // maximum integer value.
                        0: branch 5 not taken
                        7: branch 6 taken
     173                7:   if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
     174                 :     // If we know that sym != V, then this condition is infeasible since
     175                 :     // there is no other value greater than V.
     176                0:     bool isFeasible = !isNotEqual(state, sym, V);
     177                 : 
     178                 :     // If the path is still feasible then as a consequence we know that
     179                 :     // 'sym == V' because we cannot have 'sym > V' (no larger values).
     180                 :     // Add this constraint.
                        0: branch 0 not taken
                        0: branch 1 not taken
     181                0:     return isFeasible ? AddEQ(state, sym, V) : NULL;
     182                 :   }
     183                 : 
     184                7:   return state;
     185                 : }
     186                 : 
     187                 : const GRState*
     188                 : BasicConstraintManager::AssumeSymLE(const GRState* state, SymbolRef sym,
     189               82:                                     const llvm::APSInt& V) {
     190                 : 
     191                 :   // Reject a path if the value of sym is a constant X and !(X <= V).
                        0: branch 1 not taken
                       82: branch 2 taken
     192               82:   if (const llvm::APSInt* X = getSymVal(state, sym)) {
     193                0:     bool isFeasible = *X <= V;
                        0: branch 0 not taken
                        0: branch 1 not taken
     194                0:     return isFeasible ? state : NULL;
     195                 :   }
     196                 : 
     197                 :   // Sym is not a constant, but it is worth looking to see if V is the
     198                 :   // minimum integer value.
                       17: branch 5 taken
                       65: branch 6 taken
     199               82:   if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
     200                 :     // If we know that sym != V, then this condition is infeasible since
     201                 :     // there is no other value less than V.
     202               17:     bool isFeasible = !isNotEqual(state, sym, V);
     203                 : 
     204                 :     // If the path is still feasible then as a consequence we know that
     205                 :     // 'sym == V' because we cannot have 'sym < V' (no smaller values).
     206                 :     // Add this constraint.
                       15: branch 0 taken
                        2: branch 1 taken
     207               17:     return isFeasible ? AddEQ(state, sym, V) : NULL;
     208                 :   }
     209                 : 
     210               65:   return state;
     211                 : }
     212                 : 
     213                 : const GRState* BasicConstraintManager::AddEQ(const GRState* state, SymbolRef sym,
     214              683:                                              const llvm::APSInt& V) {
     215                 :   // Create a new state with the old binding replaced.
     216              683:   return state->set<ConstEq>(sym, &V);
     217                 : }
     218                 : 
     219                 : const GRState* BasicConstraintManager::AddNE(const GRState* state, SymbolRef sym,
     220              837:                                              const llvm::APSInt& V) {
     221                 : 
     222                 :   // First, retrieve the NE-set associated with the given symbol.
     223              837:   ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym);
                      107: branch 0 taken
                      730: branch 1 taken
     224              837:   GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
     225                 : 
     226                 :   // Now add V to the NE set.
     227              837:   S = ISetFactory.Add(S, &V);
     228                 : 
     229                 :   // Create a new state with the old binding replaced.
     230              837:   return state->set<ConstNotEq>(sym, S);
     231                 : }
     232                 : 
     233                 : const llvm::APSInt* BasicConstraintManager::getSymVal(const GRState* state,
     234             3753:                                                       SymbolRef sym) const {
     235             3753:   const ConstEqTy::data_type* T = state->get<ConstEq>(sym);
                      402: branch 0 taken
                     3351: branch 1 taken
     236             3753:   return T ? *T : NULL;
     237                 : }
     238                 : 
     239                 : bool BasicConstraintManager::isNotEqual(const GRState* state, SymbolRef sym,
     240             2173:                                         const llvm::APSInt& V) const {
     241                 : 
     242                 :   // Retrieve the NE-set associated with the given symbol.
     243             2173:   const ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym);
     244                 : 
     245                 :   // See if V is present in the NE-set.
                      766: branch 0 taken
                     1407: branch 1 taken
     246             2173:   return T ? T->contains(&V) : false;
     247                 : }
     248                 : 
     249                 : bool BasicConstraintManager::isEqual(const GRState* state, SymbolRef sym,
     250               38:                                      const llvm::APSInt& V) const {
     251                 :   // Retrieve the EQ-set associated with the given symbol.
     252               38:   const ConstEqTy::data_type* T = state->get<ConstEq>(sym);
     253                 :   // See if V is present in the EQ-set.
                        0: branch 0 not taken
                       38: branch 1 taken
     254               38:   return T ? **T == V : false;
     255                 : }
     256                 : 
     257                 : /// Scan all symbols referenced by the constraints. If the symbol is not alive
     258                 : /// as marked in LSymbols, mark it as dead in DSymbols.
     259                 : const GRState*
     260                 : BasicConstraintManager::RemoveDeadBindings(const GRState* state,
     261             4870:                                            SymbolReaper& SymReaper) {
     262                 : 
     263             4870:   ConstEqTy CE = state->get<ConstEq>();
     264             4870:   ConstEqTy::Factory& CEFactory = state->get_context<ConstEq>();
     265                 : 
                      814: branch 4 taken
                     4870: branch 5 taken
     266             5684:   for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) {
     267              814:     SymbolRef sym = I.getKey();
                       54: branch 1 taken
                      760: branch 2 taken
     268              814:     if (SymReaper.maybeDead(sym)) CE = CEFactory.Remove(CE, sym);
     269             4870:   }
     270             4870:   state = state->set<ConstEq>(CE);
     271                 : 
     272             4870:   ConstNotEqTy CNE = state->get<ConstNotEq>();
     273             4870:   ConstNotEqTy::Factory& CNEFactory = state->get_context<ConstNotEq>();
     274                 : 
                     3213: branch 4 taken
                     4870: branch 5 taken
     275             8083:   for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) {
     276             3213:     SymbolRef sym = I.getKey();
                      218: branch 1 taken
                     2995: branch 2 taken
     277             3213:     if (SymReaper.maybeDead(sym)) CNE = CNEFactory.Remove(CNE, sym);
     278             4870:   }
     279                 : 
     280             4870:   return state->set<ConstNotEq>(CNE);
     281                 : }
     282                 : 
     283                 : void BasicConstraintManager::print(const GRState* state, llvm::raw_ostream& Out,
     284                0:                                    const char* nl, const char *sep) {
     285                 :   // Print equality constraints.
     286                 : 
     287                0:   ConstEqTy CE = state->get<ConstEq>();
     288                 : 
                        0: branch 1 not taken
                        0: branch 2 not taken
     289                0:   if (!CE.isEmpty()) {
     290                0:     Out << nl << sep << "'==' constraints:";
                        0: branch 4 not taken
                        0: branch 5 not taken
     291                0:     for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I)
     292                0:       Out << nl << " $" << I.getKey() << " : " << *I.getData();
     293                 :   }
     294                 : 
     295                 :   // Print != constraints.
     296                 : 
     297                0:   ConstNotEqTy CNE = state->get<ConstNotEq>();
     298                 : 
                        0: branch 1 not taken
                        0: branch 2 not taken
     299                0:   if (!CNE.isEmpty()) {
     300                0:     Out << nl << sep << "'!=' constraints:";
     301                 : 
                        0: branch 6 not taken
                        0: branch 7 not taken
     302                0:     for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
     303                0:       Out << nl << " $" << I.getKey() << " : ";
     304                0:       bool isFirst = true;
     305                 : 
     306                0:       GRState::IntSetTy::iterator J = I.getData().begin(),
     307                0:                                   EJ = I.getData().end();
     308                 : 
                        0: branch 2 not taken
                        0: branch 3 not taken
     309                0:       for ( ; J != EJ; ++J) {
                        0: branch 0 not taken
                        0: branch 1 not taken
     310                0:         if (isFirst) isFirst = false;
     311                0:         else Out << ", ";
     312                 : 
     313                0:         Out << (*J)->getSExtValue(); // Hack: should print to raw_ostream.
     314                 :       }
     315                0:     }
     316                 :   }
     317                0: }

Generated: 2010-02-10 01:31 by zcov