Static Value-Flow Analysis
Loading...
Searching...
No Matches
AbstractState.h
Go to the documentation of this file.
1//===- AbstractExeState.h ----Interval Domain-------------------------//
2//
3// SVF: Static Value-Flow Analysis
4//
5// Copyright (C) <2013-2022> <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 * IntervalExeState.h
24 *
25 * Created on: Jul 9, 2022
26 * Author: Xiao Cheng, Jiawei Wang
27 *
28 * [-oo,+oo]
29 * / / \ \
30 * [-oo,1] ... [-oo,10] ... [-1,+oo] ... [0,+oo]
31 * \ \ / /
32 * \ [-1,10] /
33 * \ / \ /
34 * ... [-1,1] ... [0,10] ...
35 * \ | \ / \ /
36 * ... [-1,0] [0,1] ... [1,9] ...
37 * \ | \ | \ /
38 * ... [-1,-1] [0,0] [1,1] ...
39 * \ \ \ / /
40 * ⊥
41 */
42// The implementation is based on
43// Xiao Cheng, Jiawei Wang and Yulei Sui. Precise Sparse Abstract Execution via Cross-Domain Interaction.
44// 46th International Conference on Software Engineering. (ICSE24)
45
46#ifndef Z3_EXAMPLE_INTERVAL_DOMAIN_H
47#define Z3_EXAMPLE_INTERVAL_DOMAIN_H
48
51#include "Util/GeneralType.h"
52#include <algorithm>
53
54namespace SVF
55{
57{
58 friend class SVFIR2AbsState;
59 friend class RelationSolver;
60public:
65 {
66 }
67
69
75
76 virtual ~AbstractState() = default;
77
78 // initObjVar
79 void initObjVar(const ObjVar* objVar);
80
81
87
89 static inline bool isVirtualMemAddress(u32_t val)
90 {
92 }
93
99
102 _addrToAbsVal(std::move(rhs._addrToAbsVal)),
103 _freedAddrs(std::move(rhs._freedAddrs))
104 {
105
106 }
107
110 {
111 AbstractState inv = *this;
112 for (auto &item: inv._varToAbsVal)
113 {
114 if (item.second.isInterval())
115 item.second.getInterval().set_to_bottom();
116 }
117 return inv;
118 }
119
122 {
123 AbstractState inv = *this;
124 for (auto &item: inv._varToAbsVal)
125 {
126 if (item.second.isInterval())
127 item.second.getInterval().set_to_top();
128 }
129 return inv;
130 }
131
134 {
136 for (u32_t id: sl)
137 inv._varToAbsVal[id] = _varToAbsVal[id];
138 return inv;
139 }
140
141 static inline bool isNullMem(u32_t addr)
142 {
143 assert(isVirtualMemAddress(addr) && "needs to be a virtual memory address");
144 return addr == NullMemAddr;
145 }
146
147 static inline bool isBlackHoleObjAddr(u32_t addr)
148 {
149 assert(isVirtualMemAddress(addr) && "needs to be a virtual memory address");
150 return addr == BlackHoleObjAddr;
151 }
152
154 static inline bool isNullOrBlackHoleAddr(u32_t addr)
155 {
157 }
158
159
160protected:
164
165public:
166
167
170 {
171 assert(!isVirtualMemAddress(varId) && "varId is a virtual memory address, use load() instead");
172 return _varToAbsVal[varId];
173 }
174
176 inline virtual const AbstractValue &operator[](u32_t varId) const
177 {
178 assert(!isVirtualMemAddress(varId) && "varId is a virtual memory address, use load() instead");
179 return _varToAbsVal.at(varId);
180 }
181
182 inline virtual AbstractValue &load(u32_t addr)
183 {
184 assert(isVirtualMemAddress(addr) && "not virtual address?");
186 return _addrToAbsVal[objId];
187 }
188
189 inline virtual const AbstractValue &load(u32_t addr) const
190 {
191 assert(isVirtualMemAddress(addr) && "not virtual address?");
193 return _addrToAbsVal.at(objId);
194 }
195
196 inline void store(u32_t addr, const AbstractValue &val)
197 {
198 assert(isVirtualMemAddress(addr) && "not virtual address?");
201 }
202
204 inline bool inVarToAddrsTable(u32_t id) const
205 {
206 if (_varToAbsVal.find(id)!= _varToAbsVal.end())
207 {
208 if (_varToAbsVal.at(id).isAddr())
209 return true;
210 }
211 return false;
212 }
213
215 inline virtual bool inVarToValTable(u32_t id) const
216 {
217 if (_varToAbsVal.find(id) != _varToAbsVal.end())
218 {
219 if (_varToAbsVal.at(id).isInterval())
220 return true;
221 }
222 return false;
223 }
224
226 inline bool inAddrToAddrsTable(u32_t id) const
227 {
228 if (_addrToAbsVal.find(id)!= _addrToAbsVal.end())
229 {
230 if (_addrToAbsVal.at(id).isAddr())
231 {
232 return true;
233 }
234 }
235 return false;
236 }
237
239 inline virtual bool inAddrToValTable(u32_t id) const
240 {
241 if (_addrToAbsVal.find(id) != _addrToAbsVal.end())
242 {
243 if (_addrToAbsVal.at(id).isInterval())
244 {
245 return true;
246 }
247 }
248 return false;
249 }
250
252 inline const VarToAbsValMap&getVarToVal() const
253 {
254 return _varToAbsVal;
255 }
256
258 inline const AddrToAbsValMap&getLocToVal() const
259 {
260 return _addrToAbsVal;
261 }
262
265
268
270 void joinWith(const AbstractState&other);
271
274 {
276 _freedAddrs = other._freedAddrs;
277 }
278
280 void meetWith(const AbstractState&other);
281
283 {
284 _freedAddrs.insert(addr);
285 }
286
288 {
289 return _freedAddrs;
290 }
291
293 {
294 return _freedAddrs.find(addr) != _freedAddrs.end();
295 }
296
297
298 void printAbstractState() const;
299
300 std::string toString() const;
301
302 u32_t hash() const;
303
304 // lhs == rhs for varToValMap
305 bool eqVarToValMap(const VarToAbsValMap&lhs, const VarToAbsValMap&rhs) const;
306 // lhs >= rhs for varToValMap
307 bool geqVarToValMap(const VarToAbsValMap&lhs, const VarToAbsValMap&rhs) const;
308 // lhs == rhs for AbstractState
309 bool equals(const AbstractState&other) const;
310
313 {
314 if (&rhs != this)
315 {
317 _addrToAbsVal = rhs._addrToAbsVal;
318 _freedAddrs = rhs._freedAddrs;
319 }
320 return *this;
321 }
322
325 {
326 if (&rhs != this)
327 {
328 _varToAbsVal = std::move(rhs._varToAbsVal);
329 _addrToAbsVal = std::move(rhs._addrToAbsVal);
330 _freedAddrs = std::move(rhs._freedAddrs);
331 }
332 return *this;
333 }
334
335 bool operator==(const AbstractState&rhs) const
336 {
337 return eqVarToValMap(_varToAbsVal, rhs.getVarToVal()) &&
338 eqVarToValMap(_addrToAbsVal, rhs.getLocToVal()) &&
339 _freedAddrs == rhs._freedAddrs;
340 }
341
342 bool operator!=(const AbstractState&rhs) const
343 {
344 return !(*this == rhs);
345 }
346
347 bool operator<(const AbstractState&rhs) const
348 {
349 return !(*this >= rhs);
350 }
351
352 bool operator>=(const AbstractState&rhs) const
353 {
354 return geqVarToValMap(_varToAbsVal, rhs.getVarToVal()) &&
355 geqVarToValMap(_addrToAbsVal, rhs.getLocToVal()) &&
356 std::all_of(rhs._freedAddrs.begin(), rhs._freedAddrs.end(),
357 [this](NodeID addr)
358 {
359 return _freedAddrs.count(addr) != 0;
360 });
361 }
362
363 void clear()
364 {
365 _addrToAbsVal.clear();
366 _varToAbsVal.clear();
367 _freedAddrs.clear();
368 }
369
375 {
376 _varToAbsVal.clear();
377 }
378
379
380};
381
382}
383
384
385#endif //Z3_EXAMPLE_INTERVAL_DOMAIN_H
#define NullMemAddr
#define BlackHoleObjAddr
cJSON * item
Definition cJSON.h:222
const AddrToAbsValMap & getLocToVal() const
get loc2val map
const VarToAbsValMap & getVarToVal() const
get var2val map
u32_t getIDFromAddr(u32_t addr) const
Return the internal index if addr is an address otherwise return the value of idx.
bool operator>=(const AbstractState &rhs) const
void store(u32_t addr, const AbstractValue &val)
friend class SVFIR2AbsState
static bool isNullMem(u32_t addr)
AbstractState bottom() const
Set all value bottom.
virtual bool inAddrToValTable(u32_t id) const
whether the memory address stores abstract value
std::string toString() const
void printAbstractState() const
bool inAddrToAddrsTable(u32_t id) const
whether the memory address stores memory addresses
virtual const AbstractValue & load(u32_t addr) const
void joinWith(const AbstractState &other)
domain join with other, important! other widen this.
static bool isBlackHoleObjAddr(u32_t addr)
bool eqVarToValMap(const VarToAbsValMap &lhs, const VarToAbsValMap &rhs) const
AbstractState(const AbstractState &rhs)
copy constructor
bool operator!=(const AbstractState &rhs) const
static bool isNullOrBlackHoleAddr(u32_t addr)
Whether addr has no concrete backing memory object.
const Set< NodeID > & getFreedAddrs() const
virtual const AbstractValue & operator[](u32_t varId) const
get abstract value of variable
bool equals(const AbstractState &other) const
bool geqVarToValMap(const VarToAbsValMap &lhs, const VarToAbsValMap &rhs) const
AbstractState(AbstractState &&rhs)
move constructor
VarToAbsValMap _varToAbsVal
Map a variable (symbol) to its abstract value.
bool isFreedMem(u32_t addr) const
Set< NodeID > _freedAddrs
void initObjVar(const ObjVar *objVar)
AddrToAbsValMap _addrToAbsVal
Map a memory address to its stored abstract value.
AbstractState & operator=(AbstractState &&rhs)
operator= move constructor
virtual AbstractValue & load(u32_t addr)
AbstractState(VarToAbsValMap &_varToValMap, AddrToAbsValMap &_locToValMap)
bool inVarToAddrsTable(u32_t id) const
whether the variable is in varToAddrs table
static u32_t getVirtualMemAddress(u32_t idx)
The physical address starts with 0x7f...... + idx.
virtual AbstractValue & operator[](u32_t varId)
get abstract value of variable
AbstractState narrowing(const AbstractState &other)
domain narrow with other, and return the narrowed domain
AbstractState()
default constructor
void addToFreedAddrs(NodeID addr)
virtual bool inVarToValTable(u32_t id) const
whether the variable is in varToVal table
Map< u32_t, AbstractValue > VarToAbsValMap
virtual ~AbstractState()=default
VarToAbsValMap AddrToAbsValMap
void updateAddrStateOnly(const AbstractState &other)
Replace address-taken (ObjVar) state with other's, preserving ValVar state.
AbstractState top() const
Set all value top.
bool operator==(const AbstractState &rhs) const
AbstractState & operator=(const AbstractState &rhs)
Assignment operator.
static bool isVirtualMemAddress(u32_t val)
Check bit value of val start with 0x7F000000, filter by 0xFF000000.
void meetWith(const AbstractState &other)
domain meet with other, important! other widen this.
bool operator<(const AbstractState &rhs) const
AbstractState sliceState(Set< u32_t > &sl)
Copy some values and return a new IntervalExeState.
AbstractState widening(const AbstractState &other)
domain widen with other, and return the widened domain
static u32_t getInternalID(u32_t idx)
Return the internal index if idx is an address otherwise return the value of idx.
static u32_t getVirtualMemAddress(u32_t idx)
The physical address starts with 0x7f...... + idx.
static bool isVirtualMemAddress(u32_t val)
Check bit value of val start with 0x7F000000, filter by 0xFF000000.
for isBitcode
Definition BasicTypes.h:70
u32_t NodeID
Definition GeneralType.h:76
llvm::IRBuilder IRBuilder
Definition BasicTypes.h:76
unsigned u32_t
Definition GeneralType.h:67