Sifa

Sifa stands for Symbolic Interpretation with Fluid Abstractions.

Headers: include/Verification/Sifa/

Implementation: lib/Verification/Sifa/

Tool: sifa in tools/verifier/sifa/sifa.cpp

Overview

Sifa performs symbolic interpretation over procedure graphs and regex-style DAG summaries, with configurable abstract domains and “fluid” policies that control when and how abstraction is applied.

Main components

  • Procedure/ builds procedure graphs and associated resources.

  • Cfg/Transition models the transitions Sifa reasons about.

  • RegexDag/ contains the regex-to-DAG and compression infrastructure used for summary construction.

  • Summarizers/ computes loop and procedure summaries.

  • Domain/ provides abstract domains such as reachability, intervals, octagons, equalities, explicit values, and compound domains.

  • Fluid/ defines policies for controlling abstraction aggressiveness.

  • Worklist/ and Caches/ support scalable summary computation.

Domain choices

The in-tree front-end exposes interval and octagon domains directly, and can also delegate to SymAbs-backed symbolic abstraction.

Typical usage

./build/bin/sifa program.bc
./build/bin/sifa program.bc --function=foo --block=loop.header
./build/bin/sifa program.bc --symabs --abstract-domain=Octagon
./build/bin/sifa program.bc --reachability

See also