PLAI- Abstract Interpretation-based Analysis

Abstract interpretation based analysis in PLAI is implemented in a parametric fashion: there are four available fixpoint computation algorithms for the analysis which can be used with several abstract domains.

The (basic) organization of the code is as follows:

Module plai is in charge of interfacing with the rest of CiaoPP. Modules tarjan, normalize, and transform support the preprocessing needed for analysis: identify strongly connected components, normalize the program (if required), and assert it in a format suitable for analysis, respectively. Module plai_db stores the final results of analysis. Module trust handles the assertions used during analysis and module domains interfaces to the domain-dependent operations.

Module fixpo_plai implements the classical top-down fixpoint algorithm of PLAI. In the figure, it represents several other fixpoint algorithms available, namely: fixpo_del for delay analysis, and fixpo_dd and fixpo_di for incremental analysis. Module re_analysis supports the recovery of analysis information after transformation of the source program.

Modules trace_fixp and view_fixp implement tracing of the analysis procedure, including a graphic visualization of the and-or graph being constructed during analysis.