package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install 

dune-project
 Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (3)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.1.tar.gz
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500

doc/core/Core/Alarm/index.html

Module Core.AlarmSource

Alarms - issues found by the analyzer in a program

During the analysis, domains can perform checks to verify whether some property of interest is preserved. Domains declare the list of checks that they are responsible for in their header, and can generate 4 types of diagnostics for a given check and regarding a given location range:

  • Safe indicates that the property of interest is preserved for all execution paths reaching the check location.
  • Error represent issues that are proven true alarms for all execution paths.
  • Warning is used for potential alarms that maybe infeasible in some execution paths.
  • Unreachable indicates that the check location can't be reached in any execution path.

Checks

**********

Domains can add new checks by extending the type check and registering them using register_check. Note that checks should be simple variant constructs without any argument.

Sourcetype check = ..
Sourceval pp_check : Stdlib.Format.formatter -> check -> unit

Print a check

Sourceval register_check : ((Stdlib.Format.formatter -> check -> unit) -> Stdlib.Format.formatter -> check -> unit) -> unit

Register a check with its printer

Alarms

**********

Alarms are issues related to a check in a given range and a given callstack. Domains can add new kinds of alarms to store information related to the issue, such suspect values that raised the alarm. Nevertheless, domains can use the generic alarm A_generic of check if they don't have addition static information to attach to the alarm.

Sourcetype alarm_kind = ..
Sourcetype alarm_kind +=
  1. | A_generic of check
Sourcetype alarm = {
  1. alarm_kind : alarm_kind;
  2. alarm_check : check;
  3. alarm_range : Mopsa_utils.Location.range;
  4. alarm_callstack : Mopsa_utils.Callstack.callstack;
}

Create an alarm

Sourceval check_of_alarm : alarm -> check

Return the check associate to an alarm

Sourceval range_of_alarm : alarm -> Mopsa_utils.Location.range

Return the range of an alarm

Sourceval callstack_of_alarm : alarm -> Mopsa_utils.Callstack.callstack

Return the callstack of an alarm

Sourceval compare_alarm : alarm -> alarm -> int

Compare two alarms

Sourceval pp_alarm : Stdlib.Format.formatter -> alarm -> unit

Print an alarm

Sourceval compare_alarm_kind : alarm_kind -> alarm_kind -> int

Compare two kinds of alarms

Sourceval pp_alarm_kind : Stdlib.Format.formatter -> alarm_kind -> unit

Print an alarm kind

Sourceval join_alarm_kind : alarm_kind -> alarm_kind -> alarm_kind option

Join two alarm kinds by merging the static information attached to them

Sourceval register_alarm_compare : ((alarm_kind -> alarm_kind -> int) -> alarm_kind -> alarm_kind -> int) -> unit

Register a comparison function for alarms

Sourceval register_alarm_pp : ((Stdlib.Format.formatter -> alarm_kind -> unit) -> Stdlib.Format.formatter -> alarm_kind -> unit) -> unit

Register a print function for alarms

Sourceval register_alarm_check : ((alarm_kind -> check) -> alarm_kind -> check) -> unit

Register a function giving the check of an alarm

Sourceval register_alarm_join : ((alarm_kind -> alarm_kind -> alarm_kind option) -> alarm_kind -> alarm_kind -> alarm_kind option) -> unit

Register a join function for alarms

Sourcetype alarm_info = {
  1. check : (alarm_kind -> check) -> alarm_kind -> check;
  2. compare : (alarm_kind -> alarm_kind -> int) -> alarm_kind -> alarm_kind -> int;
  3. print : (Stdlib.Format.formatter -> alarm_kind -> unit) -> Stdlib.Format.formatter -> alarm_kind -> unit;
  4. join : (alarm_kind -> alarm_kind -> alarm_kind option) -> alarm_kind -> alarm_kind -> alarm_kind option;
}

Registration record for a new kind of alarms

Sourceval register_alarm : alarm_info -> unit

Register a new kind of alarms

Diagnostic

**************

A diagnostic gives the status of all alarms raised at the program location for the same check

Set of alarms

Sourcetype diagnostic_kind =
  1. | Warning
    (*

    Some executions may have issues

    *)
  2. | Safe
    (*

    All executions are safe

    *)
  3. | Error
    (*

    All executions do have issues

    *)
  4. | Unreachable
    (*

    No execution reaches the check point

    *)

Kind of a diagnostic

Sourcetype 'a diagnostic_ = {
  1. diag_range : Mopsa_utils.Location.range;
  2. diag_check : check;
  3. diag_kind : diagnostic_kind;
  4. diag_alarms : AlarmSet.t;
  5. diag_callstack : 'a;
}
Sourcetype diagnosticWoCs = unit diagnostic_

Create a diagnostic that says that a check is safe

Sourceval mk_error_diagnostic : alarm -> diagnostic

Create a diagnostic that says that a check is unsafe

Create a diagnostic that says that a check maybe unsafe

Create a diagnostic that says that a check is unreachable

Sourceval pp_diagnostic_kind : Stdlib.Format.formatter -> diagnostic_kind -> unit

Print a diagnostic kind

Sourceval pp_diagnostic : Stdlib.Format.formatter -> diagnostic -> unit

Print a diagnostic

Sourceval subset_diagnostic : diagnostic -> diagnostic -> bool

Check whether a diagnostic is covered by another

Sourceval join_diagnostic : diagnostic -> diagnostic -> diagnostic

Compute the union of two diagnostics

Sourceval meet_diagnostic : diagnostic -> diagnostic -> diagnostic

Compute the intersection of two diagnostics

Sourceval add_alarm_to_diagnostic : alarm -> diagnostic -> diagnostic

Add an alarm to a diagnostic

Sourceval compare_diagnostic : diagnostic -> diagnostic -> int

Compare two diagnostics

Soundness assumption

************************

When a domain can't ensure total soundness when analyzing a piece of code, it can emit assumptions under which the result is still sound.

Sourcetype assumption_scope =
  1. | A_local of Mopsa_utils.Location.range
    (*

    Local assumptions concern a specific location range in the program

    *)
  2. | A_global
    (*

    Global assumptions can concern the entire program

    *)

Scope of an assumption

Sourcetype assumption_kind = ..

Domains can add new kinds of assumptions by extending the type assumption_kind

Sourcetype assumption_kind +=
  1. | A_ignore_unsupported_stmt of Ast.Stmt.stmt

Generic assumptions for specifying potential unsoundness due to unsupported statements/expressions

Sourcetype assumption_kind +=
  1. | A_ignore_unsupported_expr of Ast.Expr.expr
Sourcetype assumption = {
  1. assumption_scope : assumption_scope;
  2. assumption_kind : assumption_kind;
}
Sourceval register_assumption : assumption_kind Mopsa_utils.TypeExt.info -> unit

Register a new kind of assumptions

Sourceval pp_assumption_kind : Stdlib.Format.formatter -> assumption_kind -> unit

Print an assumption kind

Sourceval pp_assumption : Stdlib.Format.formatter -> assumption -> unit

Print an assumption

Sourceval compare_assumption_kind : assumption_kind -> assumption_kind -> int

Compare two assumption kinds

Sourceval compare_assumption : assumption -> assumption -> int

Compare two assumptions

Sourceval mk_global_assumption : assumption_kind -> assumption

Create a global assumption

Create a local assumption

Analysis report

*******************

Alarms are organized in a report that maps each range and each check to a diagnostic. A report also contains the set of soundness assumptions made by the domains.

Sourcetype report = {
  1. report_diagnostics : diagnostic CheckMap.t RangeCallStackMap.t;
  2. report_assumptions : AssumptionSet.t;
}
Sourceval empty_report : report

Return an empty report

Sourceval is_empty_report : report -> bool

Checks whether a report is empty

Sourceval is_safe_report : report -> bool

Checks whether a report is safe, i.e. it doesn't contain an error or a warning

Sourceval is_sound_report : report -> bool

Checks whether a report is sound

Sourceval pp_report : Stdlib.Format.formatter -> report -> unit

Print a report

Sourceval subset_report : report -> report -> bool

subset_report r1 r2 checks whether report r1 is included in r2

Sourceval join_report : report -> report -> report

Compute the union of two reports

Sourceval meet_report : report -> report -> report

Compute the intersection of two reports

Sourceval filter_report : (diagnostic -> bool) -> report -> report

filter_report p r keeps only diagnostics in report r that verify predicate p

Sourceval singleton_report : alarm -> report

Create a report with a single true alarm

Sourceval add_alarm : ?warning:bool -> alarm -> report -> report

add_alarm a r adds alarm a to a report r. If a diagnostic exists for the same range and the same check as a, join_diagnostic is used to join it with an error diagnostic containing a.

Sourceval set_diagnostic : diagnostic -> report -> report

set_diagnostic d r adds diagnostic d to r. Any existing diagnostic for the same range and the same check as d is removed.

Sourceval add_diagnostic : diagnostic -> report -> report

add_diagnostic d r adds diagnostic d to r. If a diagnostic exists for the same range and the same check as d, join_diagnostic is used to join it with d.

Sourceval remove_diagnostic : diagnostic -> report -> report

Remove a diagnostic from a report

find_diagnostic range chk r finds the diagnostic of check chk at location range in report r

Sourceval exists_report : (diagnostic -> bool) -> report -> bool

Check whether any diagnostic verifies a predicate

Sourceval forall_report : (diagnostic -> bool) -> report -> bool

Check whether all diagnostics verify a predicate

Sourceval count_alarms : report -> int * int

Count the number of alarms and warnings in a report

Set of callstacks

Group diagnostics by their range and diagnostic kind

Sourceval add_assumption : assumption -> report -> report

Add an assumption to a report

Sourceval add_global_assumption : assumption_kind -> report -> report

Add a global assumption to a report

Add a local assumption to a report

Sourceval fold2zo_report : (diagnostic -> 'b -> 'b) -> (diagnostic -> 'b -> 'b) -> (diagnostic -> diagnostic -> 'b -> 'b) -> report -> report -> 'b -> 'b
Sourceval exists2zo_report : (diagnostic -> bool) -> (diagnostic -> bool) -> (diagnostic -> diagnostic -> bool) -> report -> report -> bool
Sourceval fold_report : (diagnostic -> 'b -> 'b) -> report -> 'b -> 'b
Sourceval alarms_to_report : alarm list -> report
Sourceval report_to_alarms : report -> alarm list