package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Core.Alarm

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.

type check = ..
val pp_check : Format.formatter -> check -> unit

Print a check

val register_check : ((Format.formatter -> check -> unit) -> 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.

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

Create an alarm

val check_of_alarm : alarm -> check

Return the check associate to an alarm

val range_of_alarm : alarm -> Mopsa_utils.Core.Location.range

Return the range of an alarm

val callstack_of_alarm : alarm -> Mopsa_utils.Core.Callstack.callstack

Return the callstack of an alarm

val compare_alarm : alarm -> alarm -> int

Compare two alarms

val pp_alarm : Format.formatter -> alarm -> unit

Print an alarm

val compare_alarm_kind : alarm_kind -> alarm_kind -> int

Compare two kinds of alarms

val pp_alarm_kind : Format.formatter -> alarm_kind -> unit

Print an alarm kind

val join_alarm_kind : alarm_kind -> alarm_kind -> alarm_kind option

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

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

Register a comparison function for alarms

val register_alarm_pp : ((Format.formatter -> alarm_kind -> unit) -> Format.formatter -> alarm_kind -> unit) -> unit

Register a print function for alarms

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

Register a function giving the check of an alarm

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

Register a join function for alarms

type alarm_info = {
  1. check : (alarm_kind -> check) -> alarm_kind -> check;
  2. compare : (alarm_kind -> alarm_kind -> int) -> alarm_kind -> alarm_kind -> int;
  3. print : (Format.formatter -> alarm_kind -> unit) -> 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

val 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

type 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

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

Create a diagnostic that says that a check is safe

val 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

val pp_diagnostic_kind : Format.formatter -> diagnostic_kind -> unit

Print a diagnostic kind

val pp_diagnostic : Format.formatter -> diagnostic -> unit

Print a diagnostic

val subset_diagnostic : diagnostic -> diagnostic -> bool

Check whether a diagnostic is covered by another

val join_diagnostic : diagnostic -> diagnostic -> diagnostic

Compute the union of two diagnostics

val meet_diagnostic : diagnostic -> diagnostic -> diagnostic

Compute the intersection of two diagnostics

val add_alarm_to_diagnostic : alarm -> diagnostic -> diagnostic

Add an alarm to a diagnostic

val 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.

type assumption_scope =
  1. | A_local of Mopsa_utils.Core.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

type assumption_kind = ..

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

type assumption_kind +=
  1. | A_ignore_unsupported_stmt of Core.Ast.Stmt.stmt

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

type assumption_kind +=
  1. | A_ignore_unsupported_expr of Core.Ast.Expr.expr
type assumption_kind +=
  1. | A_prototype_domain of string
type assumption_kind +=
  1. | A_no_guaranteed_termination_domain of string
type assumption = {
  1. assumption_scope : assumption_scope;
  2. assumption_kind : assumption_kind;
}
val register_assumption : assumption_kind Mopsa_utils.Core.TypeExt.info -> unit

Register a new kind of assumptions

val pp_assumption_kind : Format.formatter -> assumption_kind -> unit

Print an assumption kind

val pp_assumption : Format.formatter -> assumption -> unit

Print an assumption

val compare_assumption_kind : assumption_kind -> assumption_kind -> int

Compare two assumption kinds

val compare_assumption : assumption -> assumption -> int

Compare two assumptions

val 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.

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

Return an empty report

val is_empty_report : report -> bool

Checks whether a report is empty

val is_safe_report : report -> bool

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

val is_sound_report : report -> bool

Checks whether a report is sound

val pp_report : Format.formatter -> report -> unit

Print a report

val subset_report : report -> report -> bool

subset_report r1 r2 checks whether report r1 is included in r2

val join_report : report -> report -> report

Compute the union of two reports

val meet_report : report -> report -> report

Compute the intersection of two reports

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

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

val singleton_report : alarm -> report

Create a report with a single true alarm

val 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.

val 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.

val 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.

val 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

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

Check whether any diagnostic verifies a predicate

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

Check whether all diagnostics verify a predicate

val 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

val add_assumption : assumption -> report -> report

Add an assumption to a report

val add_global_assumption : assumption_kind -> report -> report

Add a global assumption to a report

val add_local_assumption : assumption_kind -> Mopsa_utils.Core.Location.range -> report -> report

Add a local assumption to a report

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