-
Notifications
You must be signed in to change notification settings - Fork 38
AE Python APIs
Lab-Exercise-3 uses its dense AbstractState value object directly.
Assignment-3 instead stores an Assignment-owned AEState wrapper at each
ICFG node (see below).
| API | Introduction |
|---|---|
getNodeID(variable: str) -> int |
Retrieves the node ID of the specified variable (helper defined in the lab's AEMgr). |
IntervalValue(lower: int, upper: int) |
Creates an interval value. |
AbstractValue.getInterval() -> IntervalValue |
Retrieves the interval value of the abstract value. |
AbstractValue.join_with(value: AbstractValue) |
Merges the current value with another value. |
getMemObjAddress(variable: str) -> AddressValue |
Retrieves the memory object address of the specified variable (helper). |
AddressValue(getMemObjAddress(variable: str)) |
Creates an address value initialized to the memory object address of the specified variable. |
AbstractState.widening(other: AbstractState) -> AbstractState |
Returns a new AbstractState that is the widening of self with other. |
AbstractState.narrowing(other: AbstractState) -> AbstractState |
Returns a new AbstractState that is the narrowing of self with other. |
AbstractState.joinWith(other: AbstractState) |
Joins (in place) the current state with another state. |
AbstractValue.meet_with(value: AbstractValue) |
Performs an intersection operation between the current value and another value. |
getGepObjAddress(variable: str, offset: int) -> AddressValue |
Retrieves the GEP (GetElementPtr) object address of the specified variable with the given offset (helper). |
AbstractState.store(addr: int, val: AbstractValue) |
Store an AbstractValue at virtual address addr. (Lab-Exercise-3's AEState.storeValue(varId, val) is a thin wrapper around this.) |
AbstractState.load(addr: int) -> AbstractValue |
Load the AbstractValue at virtual address addr. (Lab-Exercise-3's AEState.loadValue(varId) is a thin wrapper.) |
AbstractState.printAbstractState() |
Prints the abstract state for debugging purposes. |
This section matches the current Assignment-3 skeleton. The authoritative
interfaces are in Assignment-3/Python/AEState.py, AEHelper.py,
AEReporter.py, and Assignment_3.py.
Assignment 3 owns both traces:
self.pre_abs_trace = {} # ICFGNode -> AEState
self.post_abs_trace = {} # ICFGNode -> AEStateAbstractExecution does not keep a pysvf.AbstractInterpretation instance,
and there is no self.ai or getAbsStateFromTrace() API.
state = self.getAEState(node) # returns an AEState from post_abs_trace-
getAEState(node)creates an empty post-state if the node has no entry. - Index the maps directly as
self.post_abs_trace[node]; they are data attributes, not functions. -
AEStatecontains onepysvf.AbstractStateand exposes it asstate.raw. -
AEState(raw)wraps the supplied object without cloning it. - Delegated
state.clone()returns a rawpysvf.AbstractState, not anAEState.
Create an independent trace snapshot explicitly:
state = self.getAEState(node)
snapshot = AEState(state.raw.clone())
self.post_abs_trace[other_node] = snapshotThe pre-implemented Assignment3._storePostState(node, state) performs the
same clone-and-wrap operation.
-
self.getAEState(node)obtains the current node's post-state. - Call value, memory, GEP, and allocation operations on an
AEState, for examplestate.loadValue(pointer)andstate.getGepElementIndex(gep).
Use isinstance(obj, pysvf.TypeName) to test statement and node subtypes.
| API | Meaning |
|---|---|
AEState() |
Construct a wrapper containing a new empty pysvf.AbstractState. |
AEState(raw_state) |
Wrap the supplied raw state without cloning it. |
state.raw |
Access the contained pysvf.AbstractState. |
unwrap_state(state) |
Return the raw state contained by an AEState, or an already-raw state unchanged. |
state.clone() |
Clone the delegated raw state; the result is a pysvf.AbstractState. |
state[var_id] / state[var_id] = value
|
Read or update a variable's pysvf.AbstractValue. |
state.getAbsValue(var) / state.updateAbsValue(var, value)
|
Read or update an SVF variable. |
state.loadValue(pointer) / state.storeValue(pointer, value)
|
Load or store through an abstract pointer. |
state.load(addr) / state.store(addr, value)
|
Access one virtual memory address. |
state.initObjVar(obj) |
Initialise an object variable. |
state.getIDFromAddr(addr) |
Convert a virtual address to its PAG node ID. |
state.inVarToValTable(id) / state.inVarToAddrsTable(id)
|
Test variable-table membership. |
state.inAddrToValTable(id) / state.inAddrToAddrsTable(id)
|
Test memory-table membership. |
| API | Meaning |
|---|---|
state.getGepElementIndex(gep) |
Compute the flattened element-index interval for a GEP. |
state.getGepByteOffset(gep) |
Compute the byte-offset interval for a GEP. |
state.getGepObjAddrs(pointer, offset) |
Materialise GEP object addresses. |
state.getAllocaInstByteSize(addr) |
Compute the byte size represented by an AddrStmt allocation. |
state.getPointeeElement(pointer_id) |
Return the pointee element type when available. |
getElementIndex() and getByteOffset() are aliases for
getGepElementIndex() and getGepByteOffset().
| Statement | APIs used by Assignment 3 |
|---|---|
pysvf.AddrStmt |
getICFGNode(), getLHSVarID(), getRHSVar(), getArrSize()
|
pysvf.CopyStmt |
getICFGNode(), getLHSVarID(), getRHSVarID(), getCopyKind(), isValueCopy(), isZext(), isSext(), isInt2Ptr(), isPtr2Int(), isBitcast()
|
pysvf.BinaryOPStmt |
getResId(), getOpVar(index), getOpcode()
|
pysvf.CmpStmt |
getResId(), getOpVarId(index), getOpVar(index), getPredicate()
|
pysvf.LoadStmt |
getICFGNode(), getLHSVarID(), getRHSVarID(), getRHSVar()
|
pysvf.StoreStmt |
getICFGNode(), getLHSVarID(), getLHSVar(), getRHSVarID(), getRHSVar()
|
pysvf.GepStmt |
getICFGNode(), getLHSVarID(), getRHSVarID(), getRHSVar(), constant/dynamic offset queries |
pysvf.PhiStmt |
getResId(), getOpVarNum(), getOpVar(index), getOpICFGNode(index)
|
pysvf.CallPE |
getResId(), getOpVarNum(), getOpVarId(index), getOpCallICFGNode(index)
|
pysvf.RetPE |
getLHSVarID(), getRHSVarID()
|
pysvf.SelectStmt |
getResId(), getCondition(), getTrueValue(), getFalseValue()
|
The Python binding uses getResId() and getOpVarId(), not the C++
getResID() and getOpVarID().
| Type | Common APIs |
|---|---|
pysvf.AbstractValue |
constructors, getInterval(), getAddrs(), isInterval(), isAddr(), join_with(), equals(), clone()
|
pysvf.IntervalValue |
constructors, top(), lb(), ub(), isBottom(), is_numeral(), is_zero(), getIntNumeral(), arithmetic, meet_with()
|
pysvf.AddressValue |
constructors, insert(), hasIntersect()
|
pysvf.AbstractState |
clone(), joinWith(), widening(), narrowing(), equality, load(), store(), clear()
|
Copy and load/store transfers can be expressed directly through the node's
AEState:
state = self.getAEState(stmt.getICFGNode())
state[lhs_id] = state[rhs_id]state[load.getLHSVarID()] = state.loadValue(load.getRHSVar())
state.storeValue(store.getLHSVar(), state[store.getRHSVarID()])-
node.getInEdges()andedge.getSrcNode()enumerate incoming states. -
pysvf.IntraCFGEdgecondition and successor-value queries identify the branch represented by an edge. - Refine a cloned predecessor state according to the edge condition before joining it. The organisation of that refinement is part of your solution.
-
self.post_abs_tracesupplies predecessor post-states;self.pre_abs_traceholds function-entry input.
| API | Meaning |
|---|---|
node.getInEdges() |
Enumerate predecessor edges. |
edge.getSrcNode() |
Obtain the predecessor node. |
edge.getCondition() |
Obtain an intra-edge branch condition, if any. |
edge.getSuccessorCondValue() |
Obtain the edge's branch or switch value. |
condition.getInEdges() |
Find statements defining a condition variable. |
self.icfg.getICFGEdge(src, dst, kind) |
Query a specific ICFG edge. |
state.joinWith(other) |
Join an AEState or raw state in place. |
interval.meet_with(value) |
Refine an interval by intersection. |
Clone and refine one predecessor state before joining it:
candidate = AEState(
self.post_abs_trace[edge.getSrcNode()].raw.clone())
condition = edge.getCondition()
successor = edge.getSuccessorCondValue()
# Intersect the condition or comparison-operand values in candidate with the
# constraint represented by successor, then write each refined value back,
# for example:
# candidate[refined_var_id] = pysvf.AbstractValue(refined_interval)
# If a required meet is bottom, this edge is infeasible and candidate must
# not be joined. The line below represents the feasible, non-bottom case.
incoming.joinWith(candidate)Comparison predicates are queried through pysvf.CmpStmt.getPredicate().
The abstract-domain operations listed under Feature 1 can be used to compare,
meet, and join refined values.
-
initWto,self.func_to_wto,ICFGWTONode, andICFGWTOCycleprovide the interprocedural WTO. -
self.widen_delaycontrols the number of precise iterations before widening. -
getCallGraphSCCandself.inSameCallGraphSCC(caller, callee)provide call-graph SCC operations and identify recursive calls. -
self.getAEState,self.pre_abs_trace, andself.post_abs_tracehold cycle snapshots and results.
| Area | APIs |
|---|---|
| WTO traversal |
self.func_to_wto[fun.getId()], wto.components, ICFGWTONode.node/getICFGNode(), ICFGWTOCycle.head, ICFGWTOCycle.components
|
| Fixpoint control |
self.widen_delay, AEState.widening(), AEState.narrowing(), state equality |
| Recursion |
call.getCaller(), getCallGraphSCC, self.inSameCallGraphSCC(caller, callee)
|
AEState.widening() and narrowing() return raw
pysvf.AbstractState values. Wrap them before storing them in a trace:
raw_next = self.getAEState(head).widening(candidate)
self.post_abs_trace[head] = AEState(raw_next)Use AEState(raw_next.clone()) if raw_next may be mutated elsewhere.
-
handleStubFunction,handleCheckpointStubs,isExternalCallForAssignment,pysvf.isExtCall,updateStateOnCall,inSameCallGraphSCC, and_storePostStateare supplied by the harness. -
self.buf_overflow_helperprovides memory and string summary helpers. - State operations from Feature 1 model the values and memory changed by a summary.
| Area | APIs |
|---|---|
| Call dispatch |
getCalledFunction(), getCaller(), getArgument(index), arg_size(), getRetICFGNode(), getActualRet()
|
| Call classification |
pysvf.isExtCall(fun), isExternalCallForAssignment, inSameCallGraphSCC
|
| Harness dispatch |
handleStubFunction(call), handleCheckpointStubs(call), updateStateOnCall(call_pe), _storePostState(node, state)
|
| Value and memory effects |
getAbsValue, updateAbsValue, loadValue, storeValue, getGepObjAddrs, interval arithmetic |
For external memory and string summaries, self.buf_overflow_helper is an
AEReporter:
| API | Meaning |
|---|---|
handleMemcpy(state, dst, src, length, start_idx) |
Copy modelled cells. start_idx is a destination element index. |
getStrlen(state, value) |
Return a string-length interval, with a conservative fallback when no precise length is available. |
getGepObjAddrs(state, var_id, offset) |
Compute GEP addresses for an integer variable ID. |
Use _storePostState when propagating a state to a return node so the new
trace entry does not alias a mutable source entry.
For an external call with a return value, a summary can set that value to top and propagate the state to the return node:
summary = AEState(self.getAEState(call).raw.clone())
ret_node = call.getRetICFGNode()
summary.updateAbsValue(
ret_node.getActualRet(),
pysvf.AbstractValue(pysvf.IntervalValue.top()))
self._storePostState(ret_node, summary)-
state.getGepByteOffset,state.getGepElementIndex,state.getGepObjAddrs, andstate.getAllocaInstByteSizerecover access offsets and sizes. -
self.svfir.getBaseObject(id)andself.svfir.getGNode(id)resolve objects. -
BaseObjVarexposes size and black-hole metadata. -
self.reportBufOverflow(node)records a finding.
| API | Use |
|---|---|
self.svfir.getBaseObject(id) |
Resolve a PAG object to its base object. |
self.svfir.getGNode(id) |
Resolve a PAG node ID. |
base.isConstantByteSize() |
Test whether object byte size is known. |
base.getByteSizeOfObj() |
Read a known object byte size. |
base.isBlackHoleObj() |
Test for an unknown or black-hole object. |
state.getGepByteOffset(gep) |
Compute the current GEP's byte-offset interval. |
state.getGepElementIndex(gep) |
Compute the current GEP's element-index interval. |
state.getGepObjAddrs(pointer, offset) |
Materialise addresses for a base pointer and offset. |
state.getAllocaInstByteSize(addr) |
Obtain an allocation's byte size. |
self.reportBufOverflow(node) |
Record a buffer-overflow finding. |
GepObjVar.getConstantFieldIdx() is a field index, not a general accumulated
byte offset. Use state.getGepByteOffset(gep) and maintain any required
offset across GEP chains explicitly.
Given a resolved base-object ID, compare a direct GEP's byte-offset interval with the object size. A complete checker must additionally account for chained GEPs and external memory operations.
state = self.getAEState(gep.getICFGNode())
offset = state.getGepByteOffset(gep)
base = self.svfir.getBaseObject(object_id)
size = base.getByteSizeOfObj()
if int(offset.lb()) < 0 or int(offset.ub()) >= size:
self.reportBufOverflow(gep.getICFGNode())-
pysvf.NullMemAddrandvar.isConstNullPtrValVar()identify explicit null values. -
pysvf.AbstractState.isNullMem,pysvf.AbstractState.isBlackHoleObjAddr, andstate.isFreedMemclassify addresses. - Load, store, GEP, and call queries expose dereferenced pointers.
-
self.reportNullDeref(node)records a finding.
| API | Use |
|---|---|
value.getAddrs() |
Enumerate the addresses represented by a pointer value. |
pysvf.AbstractState.isNullMem(addr) |
Test whether an address is null. |
pysvf.AbstractState.isBlackHoleObjAddr(addr) |
Test whether an address denotes an unknown object. |
state.isFreedMem(addr) |
Test whether an address denotes freed memory. |
load.getRHSVar() |
Obtain the pointer read by a load. |
store.getLHSVar() |
Obtain the pointer written by a store. |
gep.getRHSVar() |
Obtain the base pointer used by a GEP. |
call.getArgument(index) |
Obtain pointer arguments used by an external operation. |
self.reportNullDeref(node) |
Record a null-pointer-dereference finding. |
For a load, inspect the abstract addresses represented by its pointer operand:
pointer = load.getRHSVar()
state = self.getAEState(load.getICFGNode())
value = state.getAbsValue(pointer)
if value.isAddr():
for addr in value.getAddrs():
if pysvf.AbstractState.isNullMem(addr) or state.isFreedMem(addr):
self.reportNullDeref(load.getICFGNode())The solution's private helper names are examples of decomposition, not required APIs. Students may organise these features differently or implement additional features.