Basic Usage

To analyze programs, Mopsa provides five binaries:

  • mopsa-c for C programs,

  • mopsa-python performs a value analysis of Python programs, while mopsa-python-types performs a type-only analysis,

  • mopsa-cpython for Python programs relying on custom C libraries,

  • mopsa-universal works on a toy imperative language defined within Mopsa.

C analysis

Consider the following program hello.c:

1#define LEN 100
2int main(int argc, char* argv[]) {
3  int a[LEN];
4  for(int i = 0; i <= LEN; i++)
5    a[i] = 0;
6  return 0;
7}

By running mopsa-c hello.c we get the following report:

Analysis terminated successfully
Analysis time: 0.028s

⚠ Check #2:
resources/code/hello.c: In function 'main':
resources/code/hello.c:5.4-8: warning: Invalid memory access

  5:     a[i] = 0;
         ^^^^
  accessing 4 bytes at offsets [4,400] of variable 'a' of size 400 bytes
  Callstack:
        from resources/code/hello.c:2.4-8: main

Checks summary: 2 total, ✔ 1 safe, ⚠ 1 warning
  Invalid memory access: 1 total, ⚠ 1 warning
  Integer overflow: 1 total, ✔ 1 safe

As expected, Mopsa raises an alarm at line 5, corresponding to the invalid access to array a when index i reaches LEN.

Mopsa indicates the total number of checks of each kind it performed. Here, in addition to the failed memory access check, there is an integer overflow check that passed. It corresponds to the incrementation i++. By default, Mopsa reports the detailed list of unsuccessful checks but only the number of successful checks. Using the -show-safe-checks option, Mopsa will also list the successful checks. More details on checks are available in the reports section.

Changing the <= at line 4 into < (hello-fixed.c) and running again the analysis, Mopsa reports no alarm. This proves that the program is free from invalid memory accesses and integer overflows:

Analysis terminated successfully
✔ No alarm
Analysis time: 0.028s
Checks summary: 2 total, ✔ 2 safe
  Invalid memory access: 1 total, ✔ 1 safe
  Integer overflow: 1 total, ✔ 1 safe

Analyzing a program containing multiple files is performed similarly, by providing the list of all source files to mopsa-c. The C front end in Mopsa understands the -I option to specify preprocessor include directories, and arbitrary C preprocessor and compiler options can be passed with the -ccopt option (for instance -ccopt -DSYMBOL=VALUE). By default, Mopsa starts the analysis with the main C function, and fails if it is not defined. This can be overridden with the -c-entry option

You can jump to the C benchmarks section for more interesting analysis examples in C.

Python analysis

Python programs are also analyzed by simply calling mopsa-python on the list of source files. Consider the following example hello.py:

1def absolute(x):
2    if (x < 0): return -x
3    else: x
4
5a = absolute(absolute(10))

The missing return statement at line 3 makes the function absolute return None, which triggers a TypeError in the second call as indicated by the output of Mopsa:

$ mopsa-python hello.py
Analysis terminated successfully

✗ Check #1:hello.py: In function 'absolute':
hello.py:2.8-13: error: Uncaught Python exception

  2:     if (x < 0): return -x
             ^^^^^
  Uncaught Python exception: TypeError: '__lt__' not supported between instances of 'cb{NoneType}' and 'cb{int}'
  Callstack:
        from hello.py:5.4-26: absolute

Analysis summary:
  Time: 0.015s
  Checks: 1 total, ✗ 1 error
    Uncaught Python exception: 1 total, ✗ 1 error

You can jump to the Python benchmarks section for more interesting analysis examples in Python.

Multilanguage analysis (Python+C)

Analyzing multilanguage programs is a bit more involved, as we need to rely on the mopsa-build tool. We illustrate this approach on the running example of our [SAS21] paper. You will need the files counter.c, setup.py and count.py.

The first thing to do is build the counter.c library. We call the build process with custom wrappers, so that Mopsa stores the relationship between the .so file and the sources, using mopsa-build python3 setup.py build --force --inplace (this first step may require having the packages python3-dev python3-setuptools being installed on your computer).

Once this is done, we can run the actual analysis of count.py shown below, using mopsa-cpython count.py. Note that mopsa-cpython relies the header files of Python 3.8, which are assumed to be in /usr/include/python3.8 (the path can be changed in bin/mopsa-cpython).

 1from counter import Counter
 2import random
 3
 4c = Counter()
 5p = random.randrange(128)
 6print(f"p = {p}")
 7c.incr(2**p-1)
 8c.incr()
 9r = c.counter
10print(f"r = {r}")

The result is shown below. Mopsa detects both the OverflowError that may be raised and a silent integer overflow that may also happen. The last error is a false alarm that should be easily avoided once a partitioning domain is used in Mopsa.

Analysis terminated successfully (with assumptions)
Analysis time: 0.960s

⚠ Check #4:
./counter.c: In function 'CounterIncr':
./counter.c:19.2-18: warning: Integer overflow

  19:   self->count += i;
        ^^^^^^^^^^^^^^^^
  '(@Inst{c class counter.Counter}:kAbt598DpMv9uK!6On%fD[16]:s32 + i)' has value [0,2147483648] that is larger than the range of 'signed int' = [-2147483648,2147483647]
  '(self->count + i)' has value [0,2147483648] that is larger than the range of 'signed int' = [-2147483648,2147483647]
  Callstack:
  	from count.py:8.0-8: CounterIncr


✗ Check #506:
count.py: In function 'PyErr_SetString':
count.py:7.0-14: error: OverflowError exception

  7: c.incr(2**p-1)
     ^^^^^^^^^^^^^^
  Uncaught Python exception: OverflowError: signed integer is greater than maximum
  Uncaught Python exception: OverflowError: Python int too large to convert to C long
  Callstack:
  	from /home/raphael/these/mopsa/share/mopsa/stubs/cpython/python_stubs.c:923.16-34: PyErr_SetString
  	from ./counter.c:17.6-38::convert_single[0]: PyParseTuple_int_helper
  	from count.py:7.0-14: CounterIncr
  +1 other callstack


⚠ Check #507:
count.py:7.0-14: warning: SystemError exception

  7: c.incr(2**p-1)
     ^^^^^^^^^^^^^^
  Uncaught Python exception: SystemError: CounterIncr returned a result with an error set

Checks summary: 574 total, ✔ 571 safe, ✗ 1 error, ⚠ 2 warnings
  Stub condition: 4 total, ✔ 4 safe
  Invalid memory access: 194 total, ✔ 194 safe
  Integer overflow: 186 total, ✔ 185 safe, ⚠ 1 warning
  Invalid shift: 72 total, ✔ 72 safe
  AttributeError exception: 25 total, ✔ 25 safe
  IndexError exception: 3 total, ✔ 3 safe
  ModuleNotFoundError exception: 2 total, ✔ 2 safe
  NameError exception: 26 total, ✔ 26 safe
  OverflowError exception: 1 total, ✗ 1 error
  SystemError exception: 5 total, ✔ 4 safe, ⚠ 1 warning
  TypeError exception: 30 total, ✔ 30 safe
  UnboundLocalError exception: 26 total, ✔ 26 safe

1 assumption:
  ./counter.c:67.26-59: in C/Python analysis, unsupported fields: tp_as_async, tp_hash, tp_clear ...

Multilanguage benchmarks refers to the multilanguage benchmarks we used in our experimental evaluation. They can also be run using the SAS 2021 artefact [SAS21-artefact].

[SAS21]

Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné: Static Type Analysis by Abstract Interpretation of Python Programs. SAS 2021: 323-345

[SAS21-artefact]

Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné: Static Type Analysis by Abstract Interpretation of Python Programs – Artefact. Zenodo