The CiaoPP low-level interface

Author(s): The Ciao Development Team.

This module includes the low-level predicates for interacting with CiaoPP. In this interaction model the user performs a sequence of commands to obtain a certain result (e.g., load program, analyze, check assertions).

The basic commands are:

  • module(File): loads a (main) module into the preprocessor.

  • analyze(A): perform analysis A (see Available abstract domains) on the loaded module.

  • acheck: check assertions (using current analysis information).

  • transform(T): perform transformation T on the loaded module.

  • output: output a file with the current program state (i.e., the output includes transformations, analysis info, assertion checking, etc. as controlled by the flags set and the actions performed).

  • output(File): same as output/0 but output to File.

The analyses and transformations are controlled by preprocessor flags. These flags can be modified or consulted with:

  • current_pp_flag(F, V): consult the current value V of flag F.
  • set_pp_flag(F, V): change the value of flag F to V.
  • pp_flag(F): F is a preprocessor flag.
  • dump_flags(K): dump the set of flags identified by K (all for all).

Other commands useful when developing or debugging CiaoPP:

  • show_asr(File): displays the content of a .asr file.

  • show_dump(File): displays the content of a .dump file.

  • show_types: display all current types (inferred or read).

Usage and interface

  • Library usage:
    :- use_module(ciaopp(ciaopp)).

Documentation on exports

Usage:current_pp_flag(Name,Value)

Preprocess flag Name has the value Value.

  • The following properties should hold at call time:
    (pp_flag/1)Name is a valid preprocessor flag.
  • The following properties should hold upon exit:
    (valid_flag_value/2)Value is a valid value for preprocessor flag Name.

Usage:current_pp_flag(Name,Value)

Preprocess flag Name has the value Value.

  • The following properties should hold at call time:
    (pp_flag/1)Name is a valid preprocessor flag.
  • The following properties should hold upon exit:
    (valid_flag_value/2)Value is a valid value for preprocessor flag Name.

PREDICATEset_pp_flag/2

Usage:set_pp_flag(Name,Value)

Sets Value for preprocessor flag Name.

  • The following properties should hold at call time:
    (pp_flag/1)Name is a valid preprocessor flag.
    (valid_flag_value/2)Value is a valid value for preprocessor flag Name.

Usage:push_pp_flag(Flag,Value)

Sets Value for preprocessor flag Flag, storing the current value to restore it with pop_pp_flag/1.

  • The following properties should hold at call time:
    (pp_flag/1)Flag is a valid preprocessor flag.
    (valid_flag_value/2)Value is a valid value for preprocessor flag Flag.

PREDICATEpop_pp_flag/1

Usage:pop_pp_flag(Flag)

Restores the value of the preprocessor flag Flag previous to the last non-canceled push_pp_flag/2 on it.

  • The following properties should hold at call time:
    (pp_flag/1)Flag is a valid preprocessor flag.

PREDICATEpp_flag/1
Valid flags:
(This list is outdated -- see source code for a complete description)

  • for the output:
    • analysis_info (off, on) Whether to output the results of analysis.
    • point_info (off,on) Whether to output analysis information for program points within clauses.
    • collapse_ai_vers (off, on) to output all the versions of call/success patterns inferred by analysis or just one version (summing-up all of them).
    • type_output (defined, all) to output the types inferred for predicates in terms only of types defined by the user or including types inferred anew.
    • simplify_checks (on, off) to output simplified check assertions after verification or not.
  • for analysis:
    • fixpoint (plai, dd, di, check_di, check_di2, check_di3, check_di4) The kind of fixpoint computation used.
    • multi_success (off, on) Whether to allow success multivariance.
    • widen (off, on) Whether to perform widening.
    • intermod (off, on, auto) The policy for inter-modular analysis.
    • success_policy (best, first, all, top, botfirst, botbest, botall, bottom) The policy for obtaining success information for imported predicates during inter-modular analysis.
    • entry_policy (all, top_level, force, force_assrt) The policy for obtaining entry call patterns for exported predicates during inter-modular analysis.
    • process_libraries (on, off, no_engine) Whether to perform the analysis of Ciao system libraries when a modular user program is analyzed.
    • initial_guess (botfirst, botbest, botall, bottom) The policy for obtaining initial guess when computing the analysis of a predicate from the current module.
    • use_check_assrt (off, on) Whether to use check assertions for imported predicates as if they were trust assertions.
    • depth (a non-negative integer) The maximum depth of abstractions in analyses based on term depth.
    • type_eval (on, off) Whether to attempt concrete evaluation of types being inferred.
    • type_precision (defined, all) to use during type analysis only types defined by the user or also types inferred anew.
    • entry_points_auto (none, calls, all) What kind of assertions to use as entry points: entry/1 will always be used, calls/1 and calls/2 will be used if the flag is not set to none; and success/1, success/2, comp/1 and comp/2 will be used if the flag is set to all.
    • entry_calls_scope (exported, all) What non-entry assertions to use as entry points. If the flag takes the value exported, only assertions from exported predicates will be used; if it takes the value all, exported and non-exported assertions will be used.
  • for partial evaluation:
    • global_control (off, id, inst, hom_emb) The abstraction function to use to control the creation of new patterns to analyze as a result of unfolding.
    • comp_rule (leftmost, safe_jb, bind_ins_jb, no_sideff_jb, jump_builtin, eval_builtin, local_emb) The computation rule for the selection of atoms in a goal.
    • local_control (off, orig, inst, det, det_la, depth, first_sol, first_sol_d, all_sol, hom_emb, hom_emb_anc, hom_emb_as, df_hom_emb_as, df_tree_hom_emb, df_hom_emb) The unfolding rule to use during partial evaluation.
    • unf_depth (a non-negative integer) The depth limit for unfolding.
    • rem_use_cls (off, pre, post, both) Whether to remove useless clauses.
    • abs_spec_defs (off, rem, exec, all) Whether to exploit abstract substitutions while obtaining specialized definitions on unfolding.
    • filter_nums (off, on) Whether to filter away numbers in partial evaluation.
    • exec_unif (off, on) Whether to execute unifications during specialization time or not.
    • pres_inf_fail (off, on) Whether infinite failure should be preserved in the specialized program.
    • part_concrete (off, mono, multi) The kind of partial concretization to be performed.
  • for parallelization and granularity control:
    • granularity_threshold (a non-negative integer) The threshold on computational cost at which parallel execution pays off.

Usage:flag_value(V)

V is a value for a flag.

    Usage:valid_flag_value(Name,Value)

    Value is a valid value for preprocessor flag Name.

    • If the following properties should hold at call time:
      (pp_flag/1)Name is a valid preprocessor flag.
      (flag_value/1)Value is a value for a flag.

    (UNDOC_REEXPORT)get_data/2
    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)clean_ciaopp_db/1
    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)clean_all_ciaopp_db/0
    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)dump/2
    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)dump_dir/1
    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)add_to_db/1
    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)show_dump/1
    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)restore/2
    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)restore/1
    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)dump/1
    Imported from frontend_driver (see the corresponding documentation for details).

    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)write_one_type/2
    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)output_by_ext/2
    Imported from frontend_driver (see the corresponding documentation for details).

    (UNDOC_REEXPORT)output_ext/1
    Imported from frontend_driver (see the corresponding documentation for details).

    PREDICATEoutput/1

    Usage:output(Output)

    Outputs the current module preprocessing state to a file Output. The output format (which should be valid for the loaded program) is guessed from the file extension.

    • The following properties should hold at call time:
      (nonvar/1)Output is currently a term which is not a free variable.

    PREDICATEoutput/0

    Usage:

    Outputs the current Module preprocessing state to a file named Module_opt.ext, where Module is the current module.

      Imported from frontend_driver (see the corresponding documentation for details).

      PREDICATEmodule/1

      Usage 1:module(FileName)

      Reads the code of FileName and its preprocessing unit, and sets it as the current module.

      • The following properties should hold at call time:
        (nonvar/1)FileName is currently a term which is not a free variable.
        (sourcename/1)FileName is a source name.

      Usage 2:module(FileNameList)

      Reads the code of the list of file names FileNameList (and their preprocessing units), and sets them as the current modules.

      • The following properties should hold at call time:
        (nonvar/1)FileNameList is currently a term which is not a free variable.
        (list/2)FileNameList is a list of atms.

      (UNDOC_REEXPORT)detect_language/2
      Imported from frontend_driver (see the corresponding documentation for details).

      Imported from frontend_driver (see the corresponding documentation for details).

      PREDICATEtransform/1

      Usage 1:transform(Trans)

      Returns on backtracking all available program transformation identifiers.

      • The following properties should hold at call time:
        (var/1)Trans is a free variable.
      • The following properties should hold upon exit:
        (transformation/1)Trans is a valid transformation identifier.

      Usage 2:transform(Trans)

      Performs transformation Trans on the current module.

      • The following properties should hold at call time:
        (nonvar/1)Trans is currently a term which is not a free variable.
        (transformation/1)Trans is a valid transformation identifier.

      (UNDOC_REEXPORT)cleanup_for_codegen/0
      Imported from analyze_driver (see the corresponding documentation for details).

      (UNDOC_REEXPORT)clean_analysis_info0/0
      Imported from analyze_driver (see the corresponding documentation for details).

      (UNDOC_REEXPORT)acheck/2
      Imported from analyze_driver (see the corresponding documentation for details).

      PREDICATEacheck/0

      Usage:

      Checks assertions w.r.t. analysis information, obtains from domain/1 which analyses were run.

        (UNDOC_REEXPORT)acheck_summary/1
        Imported from analyze_driver (see the corresponding documentation for details).

        (UNDOC_REEXPORT)ctcheck_sum/1
        Imported from analyze_driver (see the corresponding documentation for details).

        (UNDOC_REEXPORT)analyze1/2
        Imported from analyze_driver (see the corresponding documentation for details).

        PREDICATEanalyze/1

        Usage:analyze(Analysis)

        Analyzes the current module with Analysis. If the intermod flag is not off, this predicate may call module/1.

        • The following properties should hold at call time:
          (nonvar/1)Analysis is currently a term which is not a free variable.
          (analysis/1)Analysis is a valid analysis identifier.
        • The following properties should hold globally:
          (not_fails/1)All the calls of the form analyze(Analysis) do not fail.
          (no_choicepoints/1)A call to analyze(Analysis) does not leave new choicepoints.

        (UNDOC_REEXPORT)last_domain_used/1
        Imported from analyze_driver (see the corresponding documentation for details).

        (UNDOC_REEXPORT)assert_domain/1
        Imported from analyze_driver (see the corresponding documentation for details).

        (UNDOC_REEXPORT)menu_branch/4
        Imported from auto_interface (see the corresponding documentation for details).

        (UNDOC_REEXPORT)menu_branch/3
        Imported from auto_interface (see the corresponding documentation for details).

        (UNDOC_REEXPORT)true/2
        Imported from auto_interface (see the corresponding documentation for details).

        (UNDOC_REEXPORT)true1/1
        Imported from auto_interface (see the corresponding documentation for details).

        (UNDOC_REEXPORT)functor1/2
        Imported from auto_interface (see the corresponding documentation for details).

        Imported from auto_interface (see the corresponding documentation for details).

        (UNDOC_REEXPORT)customize/0
        Imported from auto_interface (see the corresponding documentation for details).

        Documentation on multifiles

        No further documentation available for this predicate. The predicate is multifile.

        No further documentation available for this predicate. The predicate is multifile.

        No further documentation available for this predicate. The predicate is multifile.

        Documentation on internals

        The current supported transformations are in Available program transformations.

        Usage:transformation(Transformation)

        Transformation is a valid transformation identifier.

          PROPERTYanalysis/1
          The current supported analyses are in Available abstract domains.

          Usage:analysis(Analysis)

          Analysis is a valid analysis identifier.