- The CiaoPP Program Processor »
- PART IV - CiaoPP Internals »
- Incremental analysis (high level) »
- Incremental analysis (low level)
ON THIS PAGE
Incremental analysis (low level)
Author(s): Isabel Garcia-Contreras (ported from ciaopp-0.8).This module contains the basic operations for adding or removing clauses to ciaopp (currently working for fixpoint dd) and perform an incremental reanalysis.
The posible actions are:
- Initialize ciaopp for incremental analysis (see init_empty_inc_analysis), for clauses to be added/removed from, they should be implemented in a file passed to this predicate.
- Add clauses to analysis (see td_add_clauses/2). Adds clauses and performs top down reanalysis.
- Remove clauses from analysis, following a top down strategy (see td_delete_clauses/2). Removes clauses and performs top down reanalysis.
- Remove clauses from analysis, following a bottom up strategy (see bu_delete_clauses/2). Removes clauses and reanalyzes according to the strategy defined.
Usage and interface
- Library usage:
:- use_module(ciaopp(plai/incanal/incanal_driver)). - Exports:
Documentation on exports
Usage:init_file_inc_analysis(Files,Cls,Ds)
Initializes incremental analysis with a file.
- The following properties should hold at call time:
(list/1)Files is a list.
Usage:td_add_clauses(ClKeys,AbsInt)
Adds a list of already processed clauses, expressed with their clause id (ClKeys) to the code database and updates the analysis of abstract domain AbsInt with them.
- The following properties should hold at call time:
(list/1)ClKeys is a list.
(atm/1)AbsInt is an atom. - The following properties should hold globally:
(not_fails/1)All the calls of the form td_add_clauses(ClKeys,AbsInt) do not fail.
(is_det/1)All calls of the form td_add_clauses(ClKeys,AbsInt) are deterministic.
Usage:td_delete_clauses(ClKeys,AbsInt)
Removes clauses with ids of list ClKeys for abstract domain AbsInt from analysis using top-down deletion strategy and performs a reanalysis.
- The following properties should hold at call time:
(list/1)ClKeys is a list.
(atm/1)AbsInt is an atom. - The following properties should hold globally:
(not_fails/1)All the calls of the form td_delete_clauses(ClKeys,AbsInt) do not fail.
(is_det/1)All calls of the form td_delete_clauses(ClKeys,AbsInt) are deterministic.
Usage:bu_delete_clauses(ClKeys,AbsInt)
Removes clauses Cls for abstract domain AbsInt from analysis using the bottom up deletion strategy and performs a reanalysis.
- The following properties should hold at call time:
(list/1)ClKeys is a list.
(atm/1)AbsInt is an atom. - The following properties should hold globally:
(not_fails/1)All the calls of the form bu_delete_clauses(ClKeys,AbsInt) do not fail.
(is_det/1)All calls of the form bu_delete_clauses(ClKeys,AbsInt) are deterministic.
Usage:td_rec_delete_complete(Id,Key,AbsInt)
This predicate removes the complete with Id in domain AbsInt and all its dependent information
- The following properties should hold at call time:
(nonvar/1)Id is currently a term which is not a free variable.
(nonvar/1)AbsInt is currently a term which is not a free variable.
(plai_db_id/1)plai_db_id(Id)
(atm/1)AbsInt is an atom. - The following properties should hold globally:
(not_fails/1)All the calls of the form td_rec_delete_complete(Id,Key,AbsInt) do not fail.
Usage:run_inc_fixpoint(AbsInt)
This predicate runs fixpoint for abstract domain AbsInt. It should to be run after adding information from registry files in intermodular analysis.
- The following properties should hold at call time:
(nonvar/1)AbsInt is currently a term which is not a free variable. - The following properties should hold globally:
(not_fails/1)All the calls of the form run_inc_fixpoint(AbsInt) do not fail.
(is_det/1)All calls of the form run_inc_fixpoint(AbsInt) are deterministic.
Usage:incrementally_update_analysis(Mod,AbsInt)
Mod is the module that will be reanalyzed after updating its external completes. To be called in modular analysis, no following analysis needed. This is a top-down strategy update
- The following properties should hold at call time:
(nonvar/1)Mod is currently a term which is not a free variable.
(nonvar/1)AbsInt is currently a term which is not a free variable. - The following properties should hold globally:
(not_fails/1)All the calls of the form incrementally_update_analysis(Mod,AbsInt) do not fail.
(is_det/1)All calls of the form incrementally_update_analysis(Mod,AbsInt) are deterministic.
Usage:process_external_complete_change(AbsInt,NewPrime,SgKey,Sg,Id,Proj)
This predicate updates analysis information given a complete that has changed externally. Typically this is used for updating completes that are outdated as a consequence of modular analysis (the analysis of a module was improved). The complete that has change has key SgKey and id Id. The new answer for the complete is NewPrime and refers to domain AbsInt.
Changes in answers are updated as follows:
- If the new answer is more general than the previous one, the update is as simple as replacing the answer in the complete and adding an event.
- If the new answer is more specific or incompatible, the information that depends on it has to be deleted and recomputed. We are removing the information with a top-down deletion strategy, although a bottom-up deletion strategy could more efficient. The fixpoint has to be runned after this deletion.
- The following properties should hold at call time:
(nonvar/1)AbsInt is currently a term which is not a free variable.
(nonvar/1)NewPrime is currently a term which is not a free variable.
(nonvar/1)SgKey is currently a term which is not a free variable.
(nonvar/1)Sg is currently a term which is not a free variable.
(nonvar/1)Id is currently a term which is not a free variable.
(nonvar/1)Proj is currently a term which is not a free variable.
(atm/1)AbsInt is an atom.
(list/1)NewPrime is a list.
(atm/1)SgKey is an atom.
(plai_db_id/1)plai_db_id(Id) - The following properties should hold globally:
(not_fails/1)All the calls of the form process_external_complete_change(AbsInt,NewPrime,SgKey,Sg,Id,Proj) do not fail.
Documentation on imports
This module has the following direct dependencies:- Application modules:
fixpo_dd, fixpo_ops, transform, domains, tarjan, plai_db, plai, intermod_entry, intermod_ops, frontend_driver, analyze_driver, preprocess_flags, analysis_stats, ciaopp_log, p_dump, tarjan_inc, plai_db_comparator, incanal_deletion, incanal_db, raw_printer. - System library modules:
datafacts_rt, native_props, aggregates, lists, terms_vars, sort, p_unit, program_keys, p_unit_db. - Internal (engine) modules:
term_basic, arithmetic, atomic_basic, basiccontrol, exceptions, term_compare, term_typing, debugger_support, basic_props, hiord_rt, runtime_control, messages_basic. - Packages:
prelude, initial, condcomp, assertions, assertions/assertions_basic, isomodes, datafacts, nativeprops, ciaopp(plai/notrace).