Static Value-Flow Analysis
SaberCondAllocator.h
Go to the documentation of this file.
1 //===- SaberCondAllocator.h -- Path condition manipulation---------------------//
2 //
3 // SVF: Static Value-Flow Analysis
4 //
5 // Copyright (C) <2013-> <Yulei Sui>
6 //
7 
8 // This program is free software: you can redistribute it and/or modify
9 // it under the terms of the GNU Affero General Public License as published by
10 // the Free Software Foundation, either version 3 of the License, or
11 // (at your option) any later version.
12 
13 // This program is distributed in the hope that it will be useful,
14 // but WITHOUT ANY WARRANTY; without even the implied warranty of
15 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16 // GNU Affero General Public License for more details.
17 
18 // You should have received a copy of the GNU Affero General Public License
19 // along with this program. If not, see <http://www.gnu.org/licenses/>.
20 //
21 //===----------------------------------------------------------------------===//
22 
23 /*
24  * PathAllocator.h
25  *
26  * Created on: Apr 3, 2014
27  * Author: Yulei Sui
28  */
29 
30 #ifndef PATHALLOCATOR_H_
31 #define PATHALLOCATOR_H_
32 
33 #include "SVFIR/SVFModule.h"
34 #include "SVFIR/SVFValue.h"
35 #include "Util/WorkList.h"
36 #include "Graphs/SVFG.h"
37 #include "Util/Z3Expr.h"
38 
39 
40 namespace SVF
41 {
42 
47 {
48 
49 public:
50 
51  typedef Z3Expr Condition;
60 
61 
64 
67  {
68  }
70 
72  {
73  u32_t vmrss, vmsize;
74  if (SVFUtil::getMemoryUsageKB(&vmrss, &vmsize))
75  return std::to_string(vmsize) + "KB";
76  else
77  return "cannot read memory usage";
78  }
79  inline u32_t getCondNum()
80  {
81  return totalCondNum;
82  }
84 
86 
87  inline Condition condAnd(const Condition& lhs, const Condition& rhs)
88  {
89  return Condition::AND(lhs,rhs);
90  }
91  inline Condition condOr(const Condition& lhs, const Condition& rhs)
92  {
93  return Condition::OR(lhs,rhs);
94  }
95  inline Condition condNeg(const Condition& cond)
96  {
97  return Condition::NEG(cond);
98  }
99  inline Condition getTrueCond() const
100  {
101  return Condition::getTrueCond();
102  }
103  inline Condition getFalseCond() const
104  {
105  return Condition::getFalseCond();
106  }
108  inline NodeBS exactCondElem(const Condition& cond)
109  {
110  NodeBS elems;
111  extractSubConds(cond, elems);
112  return elems;
113  }
114 
115  inline std::string dumpCond(const Condition& cond) const
116  {
117  return Condition::dumpStr(cond);
118  }
119 
121  Condition newCond(const ICFGNode* inst);
122 
124  void allocate(const SVFModule* module);
125 
127  //{@
128  inline const ICFGNode* getCondInst(u32_t id) const
129  {
130  IndexToTermInstMap::const_iterator it = idToTermInstMap.find(id);
131  assert(it != idToTermInstMap.end() && "this should be a fresh condition");
132  return it->second;
133  }
134 
135  inline void setCondInst(const Condition &condition, const ICFGNode* inst)
136  {
137  assert(idToTermInstMap.find(condition.id()) == idToTermInstMap.end() && "this should be a fresh condition");
138  idToTermInstMap[condition.id()] = inst;
139  }
141 
142  bool isNegCond(u32_t id) const
143  {
144  return negConds.test(id);
145  }
146 
147  inline bool postDominate(const SVFBasicBlock* bbKey, const SVFBasicBlock* bbValue) const
148  {
149  const SVFFunction* keyFunc = bbKey->getParent();
150  const SVFFunction* valueFunc = bbValue->getParent();
151  bool funcEq = (keyFunc == valueFunc);
152  (void)funcEq; // Suppress warning of unused variable under release build
153  assert(funcEq && "two basicblocks should be in the same function!");
154  return keyFunc->postDominate(bbKey,bbValue);
155  }
156 
157  inline bool dominate(const SVFBasicBlock* bbKey, const SVFBasicBlock* bbValue) const
158  {
159  const SVFFunction* keyFunc = bbKey->getParent();
160  const SVFFunction* valueFunc = bbValue->getParent();
161  bool funcEq = (keyFunc == valueFunc);
162  (void)funcEq; // Suppress warning of unused variable under release build
163  assert(funcEq && "two basicblocks should be in the same function!");
164  return keyFunc->dominate(bbKey,bbValue);
165  }
166 
168 
169  virtual Condition ComputeIntraVFGGuard(const SVFBasicBlock* src, const SVFBasicBlock* dst);
170  virtual Condition ComputeInterCallVFGGuard(const SVFBasicBlock* src, const SVFBasicBlock* dst, const SVFBasicBlock* callBB);
171  virtual Condition ComputeInterRetVFGGuard(const SVFBasicBlock* src, const SVFBasicBlock* dst, const SVFBasicBlock* retBB);
172 
175  virtual Condition getPHIComplementCond(const SVFBasicBlock* BB1, const SVFBasicBlock* BB2, const SVFBasicBlock* BB0);
176 
177  inline void clearCFCond()
178  {
179  bbToCondMap.clear();
180  }
182  inline void setCurEvalSVFGNode(const SVFGNode* node)
183  {
184  curEvalSVFGNode = node;
185  }
187  inline const SVFGNode* getCurEvalSVFGNode() const
188  {
189  return curEvalSVFGNode;
190  }
192 
194  void printPathCond();
195 
197  bool isSatisfiable(const Condition& condition);
198 
200  inline bool isAllPathReachable(Condition& condition)
201  {
202  return isEquivalentBranchCond(condition, Condition::getTrueCond());
203  }
204 
206  bool isEquivalentBranchCond(const Condition &lhs, const Condition &rhs) const;
207 
208  inline ICFG* getICFG() const
209  {
210  return PAG::getPAG()->getICFG();
211  }
212 
214 
215  inline bool setCFCond(const SVFBasicBlock* bb, const Condition& cond)
216  {
217  BBToCondMap::iterator it = bbToCondMap.find(bb);
218  // until a fixed-point is reached (condition is not changed)
219  if(it!=bbToCondMap.end() && isEquivalentBranchCond(it->second, cond))
220  return false;
221 
222  bbToCondMap[bb] = cond;
223  return true;
224  }
225  inline Condition getCFCond(const SVFBasicBlock* bb) const
226  {
227  BBToCondMap::const_iterator it = bbToCondMap.find(bb);
228  if(it==bbToCondMap.end())
229  {
230  return getFalseCond();
231  }
232  return it->second;
233  }
235 
236 
238  inline void setNegCondInst(const Condition &condition, const ICFGNode* inst)
239  {
240  setCondInst(condition, inst);
241  negConds.set(condition.id());
242  }
243 
245  {
246  return removedSUVFEdges;
247  }
248 
249 private:
250 
252  virtual void allocateForBB(const SVFBasicBlock& bb);
253 
255 
256  void setBranchCond(const SVFBasicBlock* bb, const SVFBasicBlock* succ, const Condition& cond);
259  Condition getBranchCond(const SVFBasicBlock* bb, const SVFBasicBlock* succ) const;
261  Condition getEvalBrCond(const SVFBasicBlock* bb, const SVFBasicBlock* succ);
263 
265  Condition evaluateBranchCond(const SVFBasicBlock* bb, const SVFBasicBlock* succ) ;
270  Condition evaluateTestNullLikeExpr(const BranchStmt* branchStmt, const SVFBasicBlock* succ);
272  Condition evaluateProgExit(const BranchStmt* branchStmt, const SVFBasicBlock* succ);
274  void collectBBCallingProgExit(const SVFBasicBlock& bb);
275  bool isBBCallsProgExit(const SVFBasicBlock* bb);
277 
279 
280  bool isEQCmp(const CmpStmt* cmp) const;
283  bool isNECmp(const CmpStmt* cmp) const;
285  bool isTestNullExpr(const ICFGNode* test) const;
287  bool isTestNotNullExpr(const ICFGNode* test) const;
289  bool isTestContainsNullAndTheValue(const CmpStmt* cmp) const;
291 
293  void destroy()
294  {
295 
296  }
297 
299  void extractSubConds(const Condition &condition, NodeBS &support) const;
300 
301 
307  std::vector<Condition> conditionVec;
310 
311 protected:
313 
314 };
315 
316 } // End namespace SVF
317 
318 #endif /* PATHALLOCATOR_H_ */
const char *const string
Definition: cJSON.h:172
Definition: ICFG.h:48
const SVFFunction * getParent() const
Definition: SVFValue.h:584
bool dominate(const SVFBasicBlock *bbKey, const SVFBasicBlock *bbValue) const
Definition: SVFValue.h:505
bool postDominate(const SVFBasicBlock *bbKey, const SVFBasicBlock *bbValue) const
Definition: SVFValue.h:510
static SVFIR * getPAG(bool buildFromFile=false)
Singleton design here to make sure we only have one instance during any analysis.
Definition: SVFIR.h:115
ICFG * getICFG() const
Definition: SVFIR.h:171
void allocate(const SVFModule *module)
Perform path allocation.
virtual ~SaberCondAllocator()
Destructor.
virtual void allocateForBB(const SVFBasicBlock &bb)
Allocate path condition for every basic block.
SVFGNodeToSVFGNodeSetMap removedSUVFEdges
a counter for fresh condition
std::string dumpCond(const Condition &cond) const
Condition newCond(const ICFGNode *inst)
Allocate a new condition.
Map< const SVFGNode *, Set< const SVFGNode * > > SVFGNodeToSVFGNodeSetMap
Map< const SVFFunction *, BasicBlockSet > FunToExitBBsMap
map a function to all its basic blocks calling program exit
bool isAllPathReachable(Condition &condition)
whether condition is satisfiable for all possible boolean guards
Condition evaluateTestNullLikeExpr(const BranchStmt *branchStmt, const SVFBasicBlock *succ)
Return branch condition after evaluating test null like expression.
Condition evaluateProgExit(const BranchStmt *branchStmt, const SVFBasicBlock *succ)
Return condition when there is a branch calls program exit.
Condition condOr(const Condition &lhs, const Condition &rhs)
bool isTestContainsNullAndTheValue(const CmpStmt *cmp) const
Return true if two values on the predicate are what we want.
bool isTestNullExpr(const ICFGNode *test) const
Return true if this is a test null expression.
void printPathCond()
Print out the path condition information.
bool postDominate(const SVFBasicBlock *bbKey, const SVFBasicBlock *bbValue) const
NodeBS negConds
key: z3 expression id, value: instruction
Set< const SVFBasicBlock * > BasicBlockSet
map bb to a Condition
const SVFGNode * curEvalSVFGNode
current llvm value to evaluate branch condition when computing guards
void setBranchCond(const SVFBasicBlock *bb, const SVFBasicBlock *succ, const Condition &cond)
Get/Set a branch condition, and its terminator instruction.
Map< const SVFBasicBlock *, CondPosMap > BBCondMap
void destroy()
Release memory.
virtual Condition getPHIComplementCond(const SVFBasicBlock *BB1, const SVFBasicBlock *BB2, const SVFBasicBlock *BB0)
BBCondMap bbConds
map basic block to its successors/predecessors branch conditions
Condition condNeg(const Condition &cond)
BBToCondMap bbToCondMap
map a basic block to its path condition starting from root
static u32_t totalCondNum
vector storing z3expression
Condition condAnd(const Condition &lhs, const Condition &rhs)
Condition operations.
bool isSatisfiable(const Condition &condition)
whether condition is satisfiable
Condition getBranchCond(const SVFBasicBlock *bb, const SVFBasicBlock *succ) const
Get branch condition.
Map< u32_t, const ICFGNode * > IndexToTermInstMap
z3 condition
NodeBS exactCondElem(const Condition &cond)
Iterator every element of the condition.
virtual Condition ComputeInterRetVFGGuard(const SVFBasicBlock *src, const SVFBasicBlock *dst, const SVFBasicBlock *retBB)
const SVFGNode * getCurEvalSVFGNode() const
Get current value for branch condition evaluation.
Condition getFalseCond() const
bool setCFCond(const SVFBasicBlock *bb, const Condition &cond)
Get/Set control-flow conditions.
void collectBBCallingProgExit(const SVFBasicBlock &bb)
Collect basic block contains program exit function call.
bool isBBCallsProgExit(const SVFBasicBlock *bb)
void extractSubConds(const Condition &condition, NodeBS &support) const
extract subexpression from a Z3 expression
Map< u32_t, Condition > CondPosMap
id to instruction map for z3
bool isEquivalentBranchCond(const Condition &lhs, const Condition &rhs) const
Whether lhs and rhs are equivalent branch conditions.
bool isEQCmp(const CmpStmt *cmp) const
Evaluate test null/not null like expressions.
SVFGNodeToSVFGNodeSetMap & getRemovedSUVFEdges()
bool isNECmp(const CmpStmt *cmp) const
Return true if the predicate of this compare instruction is not equal.
Condition evaluateBranchCond(const SVFBasicBlock *bb, const SVFBasicBlock *succ)
Evaluate branch conditions.
Condition evaluateLoopExitBranch(const SVFBasicBlock *bb, const SVFBasicBlock *succ)
Evaluate loop exit branch.
Condition getTrueCond() const
const ICFGNode * getCondInst(u32_t id) const
Get/Set instruction based on Z3 expression id.
FIFOWorkList< const SVFBasicBlock * > CFWorkList
worklist for control-flow guard computation
bool isTestNotNullExpr(const ICFGNode *test) const
Return true if this is a test not null expression.
std::string getMemUsage()
Statistics.
Condition getCFCond(const SVFBasicBlock *bb) const
FunToExitBBsMap funToExitBBsMap
map a function to all its basic blocks calling program exit
bool isNegCond(u32_t id) const
Map< const SVFBasicBlock *, Condition > BBToCondMap
map a basic block to its condition during control-flow guard computation
void setCurEvalSVFGNode(const SVFGNode *node)
Set current value for branch condition evaluation.
Condition getEvalBrCond(const SVFBasicBlock *bb, const SVFBasicBlock *succ)
Get a condition, evaluate the value for conditions if necessary (e.g., testNull like express)
virtual Condition ComputeInterCallVFGGuard(const SVFBasicBlock *src, const SVFBasicBlock *dst, const SVFBasicBlock *callBB)
IndexToTermInstMap idToTermInstMap
void setNegCondInst(const Condition &condition, const ICFGNode *inst)
mark neg Z3 expression
bool dominate(const SVFBasicBlock *bbKey, const SVFBasicBlock *bbValue) const
void setCondInst(const Condition &condition, const ICFGNode *inst)
virtual Condition ComputeIntraVFGGuard(const SVFBasicBlock *src, const SVFBasicBlock *dst)
Guard Computation for a value-flow (between two basic blocks)
std::vector< Condition > conditionVec
bit vector for distinguish neg
bool test(unsigned Idx) const
void set(unsigned Idx)
static Z3Expr AND(const Z3Expr &lhs, const Z3Expr &rhs)
compute AND, used for branch condition
Definition: Z3Expr.cpp:92
static std::string dumpStr(const Z3Expr &z3Expr)
output Z3 expression as a string
Definition: Z3Expr.cpp:168
static Z3Expr NEG(const Z3Expr &z3Expr)
compute NEG
Definition: Z3Expr.h:301
static Z3Expr getTrueCond()
Return the unique true condition.
Definition: Z3Expr.h:288
static Z3Expr OR(const Z3Expr &lhs, const Z3Expr &rhs)
compute OR, used for branch condition
Definition: Z3Expr.cpp:130
u32_t id() const
get id
Definition: Z3Expr.h:111
static Z3Expr getFalseCond()
Return the unique false condition.
Definition: Z3Expr.h:295
bool getMemoryUsageKB(u32_t *vmrss_kb, u32_t *vmsize_kb)
Get memory usage from system file. Return TRUE if succeed.
Definition: SVFUtil.cpp:177
for isBitcode
Definition: BasicTypes.h:68
std::unordered_map< Key, Value, Hash, KeyEqual, Allocator > Map
Definition: GeneralType.h:101
unsigned u32_t
Definition: GeneralType.h:46
std::unordered_set< Key, Hash, KeyEqual, Allocator > Set
Definition: GeneralType.h:96