DOCSEARCHbyAlgolia
Submit Docs

SVF Static Value-Flow Analysis Tool

repository·master·Indexed 23 days ago

https://github.com/svf-tools/svf

SVF is a static value-flow analysis tool for LLVM-based languages, supporting versions LLVM-4.0.0 through LLVM-10.0.0. It provides capabilities for abstract execution (AE), whole-program analysis (WPA), demand-driven analysis (DDA), memory SSA form construction (MSSA), and memory error checking (SABER). The framework includes support for C++ programs, multithreaded program analysis (MTA), and Context-Free-Reachability analysis (CFL). It allows for the construction of Interprocedural Control Flow Graphs (ICFG) and thread-aware value-flow graphs (SVFG).

Tokens
2.1K
Snippets
1
Records
16
Agent score
82%

What's inside SVF

  1. What is SVF?

    master
    SVF is a static value-flow analysis tool designed for LLVM-based languages. It provides a wide range of analysis capabilities including abstract execution, whole-program analysis, and memory error checking.

  2. Access SVF-Teaching resources

    master

    SVF-Teaching provides educational materials for learning and teaching software analysis, verification, and AI using the SVF framework. You can access specialized courses via the following repositories:

    • Software Security Analysis Course: Focuses on security-oriented analysis.
    • Software Analysis Course: Focuses on general software analysis techniques.
    • Software Verification Course: Focuses on formal verification methods.

  3. SVF analysis capabilities

    master

    SVF supports several categories of static analysis:

    • AE (Abstract Execution): Includes cross-domain execution, recursion analysis, and typestate analysis.
    • WPA (Whole Program Analysis): Includes field-sensitive and flow-sensitive analysis.
    • DDA (Demand-Driven Analysis): Includes flow-sensitive and context-sensitive points-to analysis.
    • MSSA (Memory SSA form construction): Handles memory regions, side-effects, and SSA form.
    • SABER (Memory error checking): Detects memory leaks and double-frees.
    • MTA (Analysis of multithreaded programs): Provides value-flows for multithreaded programs.
    • CFL (Context-Free-Reachability analysis): Includes a standard CFL solver, graph, and grammar.
    • SVFIR and MemoryModel: Provides SVFIR, memory abstraction, and points-to data structures.
    • Graphs: Generates various graphs such as call graphs, ICFG, class hierarchy graphs, constraint graphs, and value-flow graphs for static analyses and code embedding.

  5. How thread-aware interference edges are handled

    master

    The MTASVFGBuilder adds thread-aware (interference) value-flow edges between memory accesses that may happen in parallel and may alias. The logic varies based on whether the accesses are protected by a common lock:

    1. Store $\rightarrow$ Load Interference: An edge is added if the accesses may happen in parallel and alias. If they are protected by a common lock, the edge is only added if the store is a span tail and the load is a span head.
    2. Store $\rightarrow$ Store Interference: Symmetric to the store-load case. If protected by a common lock, edges are added only if one is a span tail and the other is a span head.

    If no common lock is present, the edge is added for any parallel aliasing accesses.

  6. Build the CFL Graph

    master

    The CFL graph is constructed using AliasCFLGraphBuilder. The construction method depends on the provided options:

    • From SVFIR: If Options::CFLGraph() is empty, the graph is built from the SVFIR. If Options::PEGTransfer() is enabled, it builds a Bi-PEG graph (buildBiPEGgraph); otherwise, it builds a standard bigraph (buildBigraph).
    • From Specified Graph: If a graph is provided via Options::CFLGraph(), the builder uses that input along with the grammarBase.

    After construction, a CFLGramGraphChecker is used to ensure the resulting CFL graph is consistent with the defined grammar.

  7. Build and normalize CFL grammar

    master

    The CFL analysis workflow involves building a grammar from a file and optionally normalizing it.

    1. Build Grammar: Uses GrammarBuilder to parse the file specified by Options::GrammarFilename() and construct the grammarBase.
    2. Normalize Grammar: Uses CFGNormalizer to transform the grammarBase into a normalized grammar object.

    These steps prepare the formal language rules used during the graph construction and solving phases.

  8. Configure Memory Partitioning for MTASVFGBuilder

    master

    The MTASVFGBuilder uses a MRGenerator (Memory SSA mod/ref generator) that is layered with FSAM fork/join effects. The specific strategy used is determined by the Options::MemPar() configuration.

    Supported memory partition strategies:

    • MemSSA::MemPartition::Distinct
    • MemSSA::MemPartition::IntraDisjoint
    • MemSSA::MemPartition::InterDisjoint

  9. Understand ICFG Node types and their visual representations

    master

    The ICFG is composed of several specialized node types. When visualizing the graph (e.g., via DOT), these nodes are often color-coded to distinguish their roles:

    Node TypeDescriptionVisual Color
    IntraICFGNodeStandard intraprocedural nodeBlack
    FunEntryICFGNodeEntry point of a functionYellow
    FunExitICFGNodeExit point of a functionGreen
    CallICFGNodeRepresents a call siteRed
    RetICFGNodeRepresents a return siteBlue
    GlobalICFGNodeA global/top-level block nodePurple

  10. Understand ICFG Edge types and their visual representations

    master

    ICFG edges define the flow between nodes. They are categorized by whether they stay within a function or cross function boundaries:

    Edge TypeDescriptionVisual Style
    IntraCFGEdgeIntraprocedural flow (within a function)Solid
    CallCFGEdgeInterprocedural call edge (from call site to callee entry)Solid, Red
    RetCFGEdgeInterprocedural return edge (from callee exit to return site)Solid, Blue

  11. Identify lock-span head and tail nodes

    master

    The MTASVFGBuilder provides methods to determine if a StmtSVFGNode is the first or last write within its assigned lock spans:

    • isHeadOfSpan(const StmtSVFGNode* n): Returns true if n is the first write for all lock spans it belongs to (i.e., no preceding writes exist in the same span).
    • isTailOfSpan(const StmtSVFGNode* n): Returns true if n is the last write for all lock spans it belongs to (i.e., no succeeding writes exist in the same span).

  12. Manage the Interprocedural Control Flow Graph (ICFG) with the ICFG class

    master

    The ICFG class represents the Interprocedural Control Flow Graph, which connects intraprocedural control flow with interprocedural call and return edges. It provides methods to build the graph by adding nodes and edges, and to query the relationships between them.

    Key Operations

    • Add Nodes: Use addICFGNode for general nodes or addGlobalICFGNode to set a global block node.
    • Add Intraprocedural Edges: Use addIntraEdge for standard control flow or addConditionalIntraEdge for edges involving branch conditions.
    • Add Interprocedural Edges: Use addCallEdge to connect a call site to a function entry, and addRetEdge to connect a function exit back to a return site.
    • Query Edges: Use hasIntraICFGEdge, hasInterICFGEdge, or hasThreadICFGEdge to check for the existence of specific edge types between nodes.
    • Visualization: Use dump(file, simple) to write the graph to a file or view() to open it in a graph viewer.