Reports
At the end of an analysis, Mopsa prints a report that summarizes the checks it performed, the corresponding diagnostics, and the possible assumptions made and threats to soundness. Reports are in human-readable form by default, but can also be output in JSON format.
Checks
During the analysis, the abstract domains perform a number of checks to verify the correctness of some safety properties.
The list of checks supported by an analysis is language-dependent (and even configuration-dependent), and can be obtained with the option -list checks
.
For instance, on C:
$ mopsa-c -list checks
Checks:
Assertion failure
Stub condition
Invalid memory access
Division by zero
Integer overflow
Invalid shift
Invalid pointer comparison
Invalid pointer subtraction
Double free
Insufficient variadic arguments
Insufficient format arguments
Invalid type of format argument
Invalid floating-point operation
Floating-point division by zero
Floating-point overflow
and on Python:
$ mopsa-python -list checks
Checks:
Assertion failure
Uncaught Python exception
Some checks can be enabled and disabled using command-line options, and some checks (such as floating-point errors) may not be enabled by default. See the C analysis options for instance for the list of options pertaining to C run-time errors.
Diagnostics
A diagnostic is the outcome of a check at some program location. Three outcomes are possible:
Safe
The check is valid for all execution flows reaching the program location.
Error
The check is invalid for all executions flows reaching the program location.
Warning
The validity of the check cannot be determined. This may correspond to an actual error in the program for some execution flows, or to a spurious warning caused by a too coarse abstraction.
By default, Mopsa prints only errors and warnings.
Safe checks can be display with the option -show-safe-checks
.
Soundness and Assumptions
During an analysis, the hypotheses under which the analyzer is sound and takes into account all possible executions may suddenly not longer hold. This is the case, for instance, if the program calls an undefined function, uses an unsupported language feature, or, in certain cases, due to a catastrophic loss of precision in the abstraction (such as being unable to track the possible targets of a pointer after a complex operation). In those cases, Mopsa nevertheless continues the analysis, with a best-effort strategy. In the final report, Mopsa indicates explicitly that the analysis may not be sound and lists the assumptions it made during the analysis.
For instance, the following program assumption.c
calls an undefined function f
:
1int main(int argc, char* argv[]) {
2 int i = 0;
3 i = f(12);
4}
Running mopsa-c assumption.c
, we get the following report:
Unsound analysis
✔ No alarm
Analysis time: 0.026s
Checks summary: 0 total
1 assumption:
resources/code/assumption.c:3.6-11: ignoring side-effects of calling undefined function 'f'
The first line,
Unsound analysis
(replacingAnalysis terminated successfully
), indicates that at least one assumption was made.The last line explains the assumption. The analysis assumed that the undefined function
f
simply returned an arbitrary value in the range of the return type without any side-effect (modification of other variables, errors).
Mopsa is careful to explicitly report any possible threat to soundness.
It is then the responsibility of the user to check whether the assumptions were indeed correct or to fix the analysis (e.g., by providing the source code from f
).
File Output
The output can be redirected to a file with the -output FILE
option.
Return Value
The analyzer exits with a 0 return code when the analysis completes without any warning or error, and 1 otherwise.
The -silent
option causes the analysis to always return 0, even in case of error.
JSON Output
By default, Mopsa uses a human-readable output in colored text (unless the -no-color
option is used).
Alternatively, Mopsa can export the analysis report in JSON format, using the option -format=json
.
This is useful for post-processing the analysis result with a tool or GUI, and it is generally used in combination with the -output
option to output into a file.
The JSON output is structured as follows:
The boolean field
success
indicates whether the analysis terminated successfully. The analysis may fail due to an unsupported language feature or due to an internal error. In such cases, anexception
field contains the error message.The float field
time
contains the total analysis duration.The fields
mopsa_version
andmopsa_dev_version
allow retrieving the Mopsa version used in the analysis.The field
files
contains the list of analyzed files.When
success
istrue
, the fieldalarms
contains the list of potential alarms detected during the analysis. Each alarm is structured as follows:The field
title
is a normalized string describing the alarm kind (as returned by the-list checks
option).The field
messages
gives additional, free-form information on the cause of the alarm, such as the variables involved, the values of the offending arguments, etc.The field
range
indicates the positions in the program that surround the offending statement or expression. It is composed of two positionsstart
andend
. Each position has fieldsfile
,line
, andcolumn
(line numbers start at 1, columns at 0).The field
callstacks
contains callstacks, that is, lists representing the traces of function calls from the entry point until the offending statement. Each element of a callstack has:The field
function
representing the name of the called function.The field
range
representing the location of the call site to this function.
The field may contain several callstacks, in case the alarm location can be reached by several different sequences of calls during the execution.
The field
assumptions
lists the soundness assumptions that the analysis made, if any.
Here is an example JSON output as returned by mopsa-c -format=json hello.c
, using the analysis of hello.c
from the basic usage section:
1{
2 "success": true,
3 "time": 0.024172,
4 "mopsa_version": "1.0~pre1",
5 "mopsa_dev_version":
6 "git branch:fix/c/isnan commit:6ec207a4f commit-date:2021-06-15 13:33:01 +0200",
7 "files": [ "hello.c" ],
8 "alarms": [
9 {
10 "title": "Invalid memory access",
11 "messages":
12 "accessing 4 bytes at offsets [4,400] of variable 'a' of size 400 bytes",
13 "range": {
14 "start": { "file": "hello.c", "line": 5, "column": 4 },
15 "end": { "file": "hello.c", "line": 5, "column": 8 }
16 },
17 "callstacks": [
18 [
19 {
20 "function": "main",
21 "range": {
22 "start": { "file": "hello.c", "line": 2, "column": 4 },
23 "end": { "file": "hello.c", "line": 2, "column": 8 }
24 }
25 }
26 ]
27 ]
28 }
29 ],
30 "assumptions": []
31}