An interface for a specific dataflow problem used to generate a Soufflé program.

It is used to express the dataflow problem and serves the same purpose as the transfer function when using the worklist fixpoint algorithm. The join/meet semilattice operations should be expressed implicitly in the Soufflé rules. Maintaining the monotonicity property is a responsibility of the user, i.e. the designed rules must ensure that the dataflow information only grows or remains the same.

When implementing definitions inside the functions of this interface, the user can refer to some fields that have special meanings and are added by the Soufflé solver by default:

  • bb${index} - Basic block with the given index
  • edge - Edge relations between two blocks
interface SouffleMapper {
    addConstraints(ctx: SouffleContext<SrcInfo>): void;
    addDecls(ctx: SouffleContext<SrcInfo>): void;
    addRules(ctx: SouffleContext<SrcInfo>): void;
}

Methods

  • Adds Souffle facts to describe constraints for the dataflow problem.

    Example: var_defined("bb4", "x"). - Variable x is defined within the basic block with index 4

    Parameters

    • ctx: SouffleContext<SrcInfo>

    Returns void

  • Adds Souffle declarations specific for the dataflow problem.

    Example: .decl var_defined(bb: symbol, var: symbol) - Variables defined in dataflow

    Parameters

    • ctx: SouffleContext<SrcInfo>

    Returns void

  • Adds Souffle rules specific for the dataflow problem.

    Example: out(bb, var) :- pred(bb, predBB), in(predBB, var). - Computes the out state based on the in state

    Parameters

    • ctx: SouffleContext<SrcInfo>

    Returns void