Skip to content

AE Python APIs

Jump to bottom
bjjwwang edited this page Jun 4, 2026 · 12 revisions

Essential API Documentation for Labs and Assignments (Python Version)

Lab-Exercise-3

Lab-Exercise-3 still uses the dense AbstractState value object directly — loadValue / storeValue are local convenience wrappers around store / load. In Assignment-3 the same operations route through AbstractInterpretation (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

Naming note. In Assignment-3's Python skeleton, AbstractExecution keeps a reference to the pysvf.AbstractInterpretation instance under the field name self.ai (the dense GEP / load / store / pointer helpers live on pysvf.AbstractInterpretation). The per-ICFGNode value object is still a pysvf.AbstractState; you get one with getAbsStateFromTrace(node) or by indexing the post-trace (self.post_abs_trace[node]). The bug reporter that used to be called AbstractExecutionHelper is now called AEReporter; the AbstractExecution base class still exposes it as self.buf_overflow_helper for backwards compatibility.

The tables below list the pysvf Python APIs the Assignment-3 solution actually calls. They are grouped by what they operate on (statements, abstract state, IR queries, harness facade) so you can scan them in the order you will use them while writing Assignment_3.py.

SVF statement & ICFG queries

API Introduction
isinstance(stmt, pysvf.GepStmt) / isinstance(node, pysvf.CallICFGNode) Type-test for SVFStmt and ICFGNode subtypes (replaces the C++ SVFUtil::isa<T>).
stmt.getICFGNode() Containing ICFG node of a statement (look up its state with self.getAbsStateFromTrace(node) or self.post_abs_trace[node]).
AssignStmt.getLHSVar() / getRHSVar() LHS / RHS pysvf.SVFVar of CopyStmt, LoadStmt, StoreStmt, GepStmt, PhiStmt, SelectStmt.
AssignStmt.getLHSVarID() / getRHSVarID() int NodeID for the same operands.
pysvf.IRGraph.NullPtr (if exposed) / var.isConstNullPtrValVar() Detect null-pointer operands (compare a NodeID or test the variable directly).
BinaryOPStmt.getOpcode() / getOpVarId(index) / getResId() Opcode (compare against constants from pysvf.enums.OpCode), operand IDs, and result ID.
CmpStmt.getOpVarID(index) / getResID() / getPredicate() Comparison operands, result, and predicate (pysvf.enums.Predicate).
SelectStmt.getCondition() / getTrueValue() / getFalseValue() Operands of a select.
PhiStmt.getOpVarNum() / getOpVar(index) / getOpICFGNode(index) Number of incoming values, the value at index, and the predecessor ICFG node it came from.
CallPE.getResId() / getOpVarNum() / getOpVarId(index) / getOpCallICFGNode(index) CallPE is phi-like: result is the formal parameter; each operand pairs an actual parameter with its call site.
RetPE.getLHSVarID() / getRHSVarID() Caller-side LHS and callee-side return-value variables for a return-edge statement.
CallICFGNode.getCalledFunction() / getCaller() / getArgument(i) / arg_size() / getRetICFGNode() Static callee FunObjVar, caller FunObjVar, ith argument ValVar, argument count, matching return ICFG node.
RetICFGNode.getActualRet() The actual-return SVFVar; used to write nondeterministic return values to TOP.
ICFGNode.getInEdges() / getOutEdges() / getSVFStmts() / getId() / getFun() ICFG node iteration.
ICFG.getGlobalICFGNode() / getFunEntryICFGNode(fun) Global initialisation node, function entry node.
self.svfir.getBaseObject(id) / getGNode(id) / getFunObjVar(name) Resolve NodeID → base object, NodeID → pysvf.SVFVar, function name → pysvf.FunObjVar.
pysvf.BaseObjVar.isConstantByteSize() / getByteSizeOfObj() / isBlackHoleObj() Object metadata used by the buffer-overflow checker.
pysvf.GepObjVar.getConstantFieldIdx() Accumulated byte offset of a derived GEP object from its base.
pysvf.isExtCall(func) Whether func is an external (library) function (mirrors the C++ SVFUtil::isExtCall).

Abstract values, intervals, addresses

API Introduction
pysvf.IntervalValue(lo, hi) / IntervalValue.top() Construct an interval; the universal interval.
IntervalValue.lb() / ub() / is_numeral() / is_zero() / is_infinite() / isBottom() / isTop() / equals(other) Bound queries used by the transfer functions and the branch refinement.
IntervalValue.getIntNumeral() / lb().getNumeral() / ub().getNumeral() Concrete integer for a singleton interval (or for a bound).
pysvf.AbstractValue() / .getInterval() / .getAddrs() / .isInterval() / .isAddr() Construct an empty value; project to interval / address-set views.
AbstractValue.join_with(other) / meet_with(other) / equals(other) Lattice operations on AbstractValue.
pysvf.AddressValue Set-of-addresses value; iterate with a for addr in addrs: loop.
pysvf.NullMemAddr / pysvf.BlackHoleObjAddr Sentinel virtual addresses; combine with AbstractState.isNullMem(addr) / isBlackHoleObjAddr(addr) when iterating address sets.
AbstractState.widening(other) / narrowing(other) / joinWith(other) / meetWith(other) Lattice ops on the per-node state used by handleICFGCycle.
AbstractState.isBlackHoleObjAddr(addr) / isNullMem(addr) / isFreedMem(addr) Filter sentinel / null / freed addresses out of an AddressValue iteration.
AbstractState.getIDFromAddr(addr) Recover the base-object NodeID from a virtual address.
AbstractState.inVarToValTable(id) / inVarToAddrsTable(id) Whether id has a recorded value / address-set (use before indexing as[id]).
as[id] / as[id] = value Read / write the AbstractValue for NodeID id in an AbstractState.
AbstractState.printAbstractState() Debug-print the entire state.
AbstractState.clone() Independent copy — call this before mutating a state you also stored in self.post_abs_trace.

AbstractExecution facade (call as self.<method>(...) from Assignment_3.py)

API Introduction
self.getAbsStateFromTrace(node) Returns the AbstractState for node (lives inside the underlying pysvf.AbstractInterpretation's trace).
self.post_abs_trace[node] / self.pre_abs_trace[node] Pre- and post-trace dicts (the post one is an alias of self.ai). Indexing the post-trace returns a reference to a C++ AbstractState; save previous loop states with .clone() before calling code that mutates the trace.
self.ai.loadValue(pointer, node) Load through pointer (a pysvf.ValVar). Replaces the old AEState.loadValue(varId).
self.ai.storeValue(pointer, val, node) Store val through pointer. Replaces the old AEState.storeValue(varId, val).
self.ai.getGepElementIndex(gep) / self.ai.getGepByteOffset(gep) Element-index / byte-offset of a GepStmt (use the byte version for buffer-bound math).
self.ai.getGepObjAddrs(pointer, offset) Resolve a ValVar + IntervalValue offset into the set of derived GEP-object addresses.
self.ai.getAllocaInstByteSize(addr_stmt) Byte size of the object created by an AddrStmt (alloca).
self.reportBufOverflow(node, msg=None) / self.reportNullDeref(node, msg=None) Record a bug; routes through the AEReporter instance.
self.buf_overflow_helper.handleMemcpy(abstract_state, dst, src, length, start_idx) Reusable element-wise memcpy summary on AEReporter. Copies length bytes from src to dst starting at start_idx. Only objects present in abstract_state are copied.
self.buf_overflow_helper.getStrlen(abstract_state, str_value) Computes the null-terminated string length starting at str_value.
self.buf_overflow_helper.getGepObjAddrs(abstract_state, var_id, offset) / getByteOffset(abstract_state, gep) / getAllocaInstByteSize(abstract_state, addr_stmt) / getPointeeElement(abstract_state, var_id) Convenience helpers on AEReporter that forward to self.ai (kept for the memcpy / strlen flows).

Harness driver hooks (entry points the harness calls into)

API Introduction
self.handleGlobalNode() Replay the global ICFG node so global state is initialised before main is entered.
self.handleFunction(funEntry) Iterate one function's interprocedural WTO; dispatch singletons to handleICFGNode and cycles to handleICFGCycle.
self.handleICFGNode(node) Merge predecessor states, run the per-statement transfer functions, dispatch call sites via self.handleCallSite, run the bug checkers; return whether the post-state changed.
self.handleICFGCycle(cycle) Drive a WTO cycle (loop head or recursive-function entry) to a fixpoint with widening / narrowing.
self.handleCallSite(callNode) Dispatch a call ICFG node (see the comment block above the method in Assignment_3.py for the full dispatch table).
self.handleStubFunction(callNode) / self.handleCheckpointStubs(callNode) Sub-dispatchers for svf_assert / svf_assert_eq and the SAFE_* / UNSAFE_* ground-truth checkpoints (defined in AEHelper.py — call them from your handleCallSite).
self.isExternalCallForAssignment(func) Whether func belongs to the assignment's external-API whitelist (the memory / string family plus mem_insert / str_insert).
self.inSameCallGraphSCC(caller, callee) Andersen-based SCC check used to skip recursive callsites (the outer WTO cycle drives the recursion).

CallPE — phi-like formal-parameter resolution

def updateStateOnCall(self, call: pysvf.CallPE):
    abstract_state = self.post_abs_trace[call.getICFGNode()]
    formal = call.getResId()
    result = pysvf.AbstractValue()
    for i in range(call.getOpVarNum()):
        call_site = call.getOpCallICFGNode(i)
        if call_site in self.post_abs_trace:
            actual = call.getOpVarId(i)
            result.join_with(self.post_abs_trace[call_site][actual])
    abstract_state[formal] = result

loadValue / storeValue through a ValVar pointer

def updateStateOnLoad(self, load: pysvf.LoadStmt):
    node = load.getICFGNode()
    abstract_state = self.post_abs_trace[node]
    if abstract_state.inVarToAddrsTable(load.getRHSVarID()):
        abstract_state[load.getLHSVarID()] = self.ai.loadValue(load.getRHSVar(), node)

def updateStateOnStore(self, store: pysvf.StoreStmt):
    node = store.getICFGNode()
    abstract_state = self.post_abs_trace[node]
    if abstract_state.inVarToAddrsTable(store.getLHSVarID()):
        val = (_null_address_value()
               if store.getRHSVar().isConstNullPtrValVar()
               else abstract_state[store.getRHSVarID()])
        self.ai.storeValue(store.getLHSVar(), val, node)

GEP arithmetic (getGepElementIndex, getGepByteOffset, getGepObjAddrs)

def updateStateOnGep(self, gep: pysvf.GepStmt):
    node = gep.getICFGNode()
    abstract_state = self.post_abs_trace[node]
    if abstract_state.inVarToAddrsTable(gep.getRHSVarID()):
        offset = self.ai.getGepElementIndex(gep)
        abstract_state[gep.getLHSVarID()] = self.ai.getGepObjAddrs(gep.getRHSVar(), offset)
  • getGepElementIndex(gep) / getGepByteOffset(gep) return IntervalValues.
  • getGepObjAddrs(pointer, offset) resolves the derived address set; iterate the result and call abstract_state.getIDFromAddr(addr) to walk each base object.

Buffer-bound math: getBaseObject / getConstantFieldIdx 

for addr in ptr_val.getAddrs():
    if pysvf.AbstractState.isBlackHoleObjAddr(addr) or pysvf.AbstractState.isNullMem(addr):
        continue
    obj_id = abstract_state.getIDFromAddr(addr)
    base_obj = self.svfir.getBaseObject(obj_id)
    if base_obj is None or not base_obj.isConstantByteSize():
        continue
    size = base_obj.getByteSizeOfObj()
    gnode = self.svfir.getGNode(obj_id)
    base_offset = (pysvf.IntervalValue(gnode.getConstantFieldIdx())
                   if isinstance(gnode, pysvf.GepObjVar)
                   else pysvf.IntervalValue(0))
    # ... compare base_offset + access_offset against size

Call-site dispatch (the handleCallSite student TODO)

def handleCallSite(self, node: pysvf.CallICFGNode):
    fun = node.getCalledFunction()
    if fun is None:
        return
    name = fun.getName()
    if name in ("svf_assert", "svf_assert_eq"):
        self.handleStubFunction(node)
    elif name in ("UNSAFE_BUFACCESS", "SAFE_BUFACCESS",
                  "UNSAFE_PTRDEREF", "SAFE_PTRDEREF"):
        self.handleCheckpointStubs(node)
    elif name in ("nd", "rand"):
        lhs_id = node.getRetICFGNode().getActualRet().getId()
        self.post_abs_trace[node][lhs_id] = pysvf.AbstractValue(pysvf.IntervalValue.top())
    elif name in ("mem_insert", "str_insert") or pysvf.isExtCall(fun):
        self.updateStateOnExtCall(node)
    else:
        caller = node.getCaller()
        if caller is not None and self.inSameCallGraphSCC(caller, fun):
            return  # outer WTO cycle drives the recursion
        self.handleFunction(self.svfir.getICFG().getFunEntryICFGNode(fun))
        ret_node = node.getRetICFGNode()
        if node in self.post_abs_trace:
            self.post_abs_trace[ret_node] = self.post_abs_trace[node]

AEReporter.handleMemcpy(abstract_state, dst, src, length, start_idx)

Simulates memcpy by copying length bytes from src to dst starting at offset start_idx. Element size is determined automatically from the destination type; only objects present in abstract_state are copied.

# dst, src are pysvf.SVFVar (array or pointer)
# length is an IntervalValue; the lower bound is copied
# start_idx is an int offset

self.buf_overflow_helper.handleMemcpy(
    abstract_state, dst, src, pysvf.IntervalValue(5, 5), 2)
# e.g. dst[2..6] are overwritten from src[0..4], other indices untouched.

AEReporter.getStrlen(abstract_state, str_value)

length = self.buf_overflow_helper.getStrlen(
    abstract_state, extCallNode.getArgument(1))

Returns an IntervalValue for the null-terminated string length at str_value. Falls back to [0, Options.max_field_limit()] when the length cannot be determined precisely.

Clone this wiki locally