Essential API Documentation for Labs and Assignments (Python Version)

Lab-Exercise-3

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.

Assignment-3

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.

State ownership

Assignment 3 owns both traces:

self.pre_abs_trace = {}   # ICFGNode -> AEState
self.post_abs_trace = {}  # ICFGNode -> AEState

AbstractExecution 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.
• AEState contains one pysvf.AbstractState and exposes it as state.raw.
• AEState(raw) wraps the supplied object without cloning it.
• Delegated state.clone() returns a raw pysvf.AbstractState, not an AEState.

Create an independent trace snapshot explicitly:

state = self.getAEState(node)
snapshot = AEState(state.raw.clone())
self.post_abs_trace[other_node] = snapshot

The pre-implemented Assignment3._storePostState(node, state) performs the same clone-and-wrap operation.

Feature 1: Statement transfer functions

Starter and helper functions

• self.getAEState(node) obtains the current node's post-state.
• Call value, memory, GEP, and allocation operations on an AEState, for example state.loadValue(pointer) and state.getGepElementIndex(gep).

Use isinstance(obj, pysvf.TypeName) to test statement and node subtypes.

State and memory APIs

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.

GEP and allocation APIs

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 queries

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().

Abstract domains

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()

Mini example

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()])

Feature 2: Branch feasibility

Starter and helper functions

• node.getInEdges() and edge.getSrcNode() enumerate incoming states.
• pysvf.IntraCFGEdge condition 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_trace supplies predecessor post-states; self.pre_abs_trace holds function-entry input.

Control-flow and lattice APIs

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.

Mini example

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.

Feature 3: Loop and recursion fixpoint

Starter and helper functions

• initWto, self.func_to_wto, ICFGWTONode, and ICFGWTOCycle provide the interprocedural WTO.
• self.widen_delay controls the number of precise iterations before widening.
• getCallGraphSCC and self.inSameCallGraphSCC(caller, callee) provide call-graph SCC operations and identify recursive calls.
• self.getAEState, self.pre_abs_trace, and self.post_abs_trace hold cycle snapshots and results.

WTO and fixpoint APIs

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)

Mini example

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.

Feature 4: External-API value summaries

Starter and helper functions

• handleStubFunction, handleCheckpointStubs, isExternalCallForAssignment, pysvf.isExtCall, updateStateOnCall, inSameCallGraphSCC, and _storePostState are supplied by the harness.
• self.buf_overflow_helper provides memory and string summary helpers.
• State operations from Feature 1 model the values and memory changed by a summary.

Call and summary APIs

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.

Mini example

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)

Feature 5: Buffer-overflow checker

Starter and helper functions

• state.getGepByteOffset, state.getGepElementIndex, state.getGepObjAddrs, and state.getAllocaInstByteSize recover access offsets and sizes.
• self.svfir.getBaseObject(id) and self.svfir.getGNode(id) resolve objects.
• BaseObjVar exposes size and black-hole metadata.
• self.reportBufOverflow(node) records a finding.

Buffer and object APIs

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.

Mini example

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())

Feature 6: Null-pointer-dereference checker

Starter and helper functions

• pysvf.NullMemAddr and var.isConstNullPtrValVar() identify explicit null values.
• pysvf.AbstractState.isNullMem, pysvf.AbstractState.isBlackHoleObjAddr, and state.isFreedMem classify addresses.
• Load, store, GEP, and call queries expose dereferenced pointers.
• self.reportNullDeref(node) records a finding.

Null and address APIs

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.

Mini example

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.