AE C++/Python API wikis: refresh to match the AEHelper / AEReporter
split and the new AbstractExecution facade
The wikis still referenced the pre-refactor names: svfStateMgr->...,
AbstractExecutionHelper, bufOverflowHelper, AbsExtAPI utils->handleMemcpy,
plus a few APIs (updateGepObjOffsetFromBase / getAccessOffset /
addToGepObjOffsetFromBase / hasGepObjOffsetFromBase /
getGepObjOffsetFromBase) that students now design themselves.
C++ side
--------
- Drop svfStateMgr-> references; document the bare-method facade on
AbstractExecution (getAbsValue / updateAbsValue / loadValue / storeValue
/ getGepObjAddrs / getGepElementIndex / getGepByteOffset /
getAllocaInstByteSize / getAbsStateFromTrace / postAbsTrace /
reportBufOverflow / reportNullDeref).
- Reorganise the Assignment-3 table by what each API operates on
(SVF statement / ICFG queries, abstract values + intervals + addresses,
the AbstractExecution facade, the harness driver hooks).
- Add the harness driver hooks (handleGlobalNode / handleFunction /
handleICFGNode / handleICFGCycle / handleCallSite / handleStubFunctions
/ handleCheckpointStubs / isExternalCallForAssignment /
ander->inSameCallGraphSCC / getReporter).
- Replace the AbsExtAPI handleMemcpy / getStrlen rows with inline code
examples showing how the solution structures call-site dispatch,
GEP arithmetic, and buffer-bound math.
Python side
-----------
- svf_state_mgr -> self.ai (matches the renamed attribute on
AbstractExecution).
- AbstractExecutionHelper -> AEReporter (kept as
self.buf_overflow_helper on AbstractExecution for backwards
compatibility); document handleMemcpy / getStrlen / getGepObjAddrs /
getByteOffset / getAllocaInstByteSize on AEReporter.
- Mirror the C++ side's grouping and add the same harness driver hooks
for Python (self.handleGlobalNode / handleFunction / handleICFGNode /
handleICFGCycle / handleCallSite / handleStubFunction /
handleCheckpointStubs / inSameCallGraphSCC).
- Add the new sentinel addresses (pysvf.NullMemAddr,
pysvf.BlackHoleObjAddr) and the AbstractState filters
(isBlackHoleObjAddr / isNullMem / isFreedMem) the checkers rely on.
Update Assignment 3 API docs
sync: align API docs with SVF master + SVF-Python pybind (2026-05)
Refresh the C++ and Python API tables against the current upstream
(SVF tip c8c6042738, SVF-Python tip bb6f3d8) so that students working
on Lab-Exercise-3 / Assignment-3 do not see references to symbols
that have been removed or renamed.
C++ (AE-CPP-APIs.md, SVF-CPP-API.md, SVF-CPP-Z3-API.md):
- AbstractStateManager.h is gone in master; methods loadValue /
storeValue / getGepObjAddrs / getElementIndex / getByteOffset now
live on AbstractInterpretation. In Assignment-3 those are reached
via the svfStateMgr pointer, so the wiki uses svfStateMgr->getGep*
/ loadValue(ValVar*, ICFGNode*) / storeValue(...).
- AbsExtAPI::handleMemcpy signature changed to
(ValVar*, ValVar*, IntervalValue, u32_t, ICFGNode*) — no longer
takes AbstractState explicitly.
- getAbstractState(node) was renamed to getAbsStateFromTrace(node)
in Assignment-3 (and to getAbsState(node) on the SVF library side).
- SVFBasicTypes.h pinned-commit link rotted; switched to
svf/include/MemoryModel/PointsTo.h.
- AndersenPTA::addCopyEdge clarified as the Assignment-1 subclass
override of AndersenBase::addCopyEdge.
- Z3ExampleMgr renamed to Z3Examples; Z3 page links moved from
Teaching-Software-Verification and yuleisui/* to the public
SVF-tools/Software-Security-Analysis repo.
Python (Pysvf-API.md, AE-Python-APIs.md):
- pysvf.AbstractState no longer carries isAddr / getElementIndex /
getGepObjAddrs / storeValue / loadValue. Rebuilt the table with
the actual current pybind surface (getVar, setVar, store, load,
joinWith, meetWith, widening, narrowing, getIDFromAddr,
printAbstractState, inVarTo*Table, initObjVar, addToFreedAddrs,
isFreedMem, the static address helpers, and the static
isCmp/SwitchBranchFeasible factories).
- Added a new pysvf.AbstractInterpretation section covering the
helpers that absorbed AbstractStateManager (getAbsState /
updateAbsState / getGepElementIndex / getGepByteOffset /
getGepObjAddrs / loadValue / storeValue / getPointeeElement /
getAllocaInstByteSize / getTrace / __getitem__ / __setitem__ /
__contains__ / analyse / runOnModule).
- Fleshed out AbstractValue / IntervalValue surface and added a
small AddressValue section.
- Dropped the BufOverflowHelper section: there is no such class in
the pybind surface; the helpers live on AbstractExecutionHelper
in Assignment-3/Python/Assignment_3_Helper.py (already covered
by AE-Python-APIs.md).
- AE-Python-APIs.md Lab-Exercise-3 and Assignment-3 tables: the
lab still has its own AEState : AbstractState wrapper, so the
lab table now refers to AbstractState directly (with a note that
AEState.loadValue/storeValue are thin wrappers around store/load);
the assignment table mirrors the C++ changes
(svfStateMgr.getGepByteOffset, etc.) and switches the helper
class name from bufOverflowHelper to AbstractExecutionHelper to
match Assignment_3_Helper.py.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Updated AE Python APIs (markdown)
Updated AE Python APIs (markdown)
Updated AE Python APIs (markdown)
Updated AE Python APIs (markdown)
Updated AE Python APIs (markdown)
Updated AE Python APIs (markdown)
Updated AE Python APIs (markdown)