Universal Options
Mopsa includes a Universal language that supports commonly used constructs (e.g., integers, loops, function calls) and provides ready-to-use abstractions and iterators. These domains are commonly used in configurations for both C and Python. We describe here the most important domains used in C and Python, as well as their command-line options.
Numeric Domains
In Universal, numeric values can be either mathematical (i.e., unbounded) integers or floating-point numbers (with proper rounding). Mopsa proposes several non-relational and relational numeric abstractions:
Zero
The simple domain universal.numeric.values.zero
is a value abstraction that distinguishes between null and non-null integer values.
Powerset
The domain universal.numeric.values.powerset
keeps a finite number of integer values per variable, which can be controlled with the option:
- -max-set-size <int>
The maximal number of values in the set for a variable (default:
10
).
Congruences
The domain universal.numeric.values.congruences
represents a set of integer values as a congruence \(a\mathbb{Z} + b\), where \(a \in \mathbb{N}\) and \(b \in \mathbb{Z}\).
Integer Intervals
The domain universal.numeric.values.intervals.integer
uses (possibly unbounded) intervals to abstract integer values.
Float Intervals
The domain universal.numeric.values.intervals.float
uses intervals to abstract floating-point values.
Additionally, flags indicate the possible presence of special floating-point values (positive and negative infinities, not-a-number).
The abstraction does not distinguish between positive and negative zeros.
The domain has one option:
- -float-rounding-mode (near | zero | up | down | rnd)
Set the IEEE rounding mode of floating-point computations (default:
near
).rnd
indicates that the rounding mode is not fixed and can change arbitrarily during program execution. It is useful to analyze soundly the program when the rounding mode is unknown.
Relational Domains
In addition to the previous non-relational abstractions, Mopsa provides a numeric relational domain universal.numeric.relation
that is a wrapper around the Apron library.
- -numeric (lineq | octagon | polyhedra)
Select the relational numeric abstraction used by the domain: affine equalities, unit-two-variables-per-inequality (a.k.a. octagons), or affine inequalities (default:
polyhedra
).
Loops
A generic iterator for while
loops is implemented by the domain universal.iterators.loops
.
It supports unrolling and widening, which can be controlled with the options below.
As C and Python loops are translated into Universal while
loops, they are also affected by these options.
- -loop-decr-it
Enable a single decreasing iteration after loop stabilisation.
- -loop-full-unrolling <bool>
Unroll loops without applying widening (default:
false
).
- -loop-full-unrolling-at [<file1>:]<line1>,...,[<filen>:]<linen>
Fully unroll loops at specific program locations (default: empty).
- -loop-no-cache
Disable the cache of previous loops fixpoints.
- -loop-unrolling <int>
Set the number of unrolling iterations before joining the environments (default:
1
).
- -loop-unrolling-at [<file1>:]<line1>:<unrolling1>,...,[<filen>:]<linen>:<unrollingn>
Set the number of unrolling iterations at a specific program locations (default: empty).
- -widening-delay <int>
Set the number of iterations using joins before applying a widening (default:
0
).
Inter-procedural Analysis
Both the C
and Python
analyzers rely on common generic inter-procedural iterators for analyzing function calls:
Inlining
The domain universal.iterators.interproc.inlining
implements a precise iterator that inlines function calls.
Cache
The domain universal.iterators.interproc.sequential_cache
improves the performance of inlining by caching the last calls and reuse them when possible.
- -mod-interproc-size <int>
Set the size of the cache (default:
10
).
Heap Recency
Heap allocation can be abstracted by the domain universal.heap.recency
that implements the recency abstraction algorithm [SAS06], that operates as follows:
Firstly, the user fixes an allocation partitioning policy that specifies how heap addresses are partitioned, e.g. by grouping all the allocations at a program location into one partition.
For each partition, the domain creates only two abstract addresses: one for the most recent allocation and another one for all previous allocations.
The domain also supports block deallocation and resizing (useful for C programs). The recency abstraction is also used to model other kinds of dynamic resources, such as C files. Such resources are managed in stub contacts.
- -default-alloc-pol (all | range | callstack | range_callstack)
Select the allocation partitioning policy (default:
range_callstack
).all
merge all allocations into a unique partitionrange
merge only allocations at the same program locationcallstack
merge only allocations on the same call stackrange_callstack
merge only allocations at the same program location and call stack
- -hash-heap-address <bool>
Display heap addresses as their hash (default:
false
).By default, addresses are displayed with the full information about their partition, which can be large (e.g., if it includes a call stack). With this option, addresses are displayed as a hash of the partition, which makes the output more readable.
Unit Tests
Mopsa has a special mode to perform unit tests.
In this mode, instead of analyzing the source from the top-level entry point (e.g., main
for C), Mopsa will run a sequence of test functions and report the total number of successes and failures.
Every (global) C or Python function with a name starting with test_
is considered to be a test and will be run.
Functional properties can be checked using language-specific assertion built-ins (such as _mopsa_assert
in C, or mopsa.assert
in Python).
The return code of the analysis is 0 if all tests passed, and 1 in case of a failure.
The Mopsa distribution includes some regression tests, which you can run with make tests
.
They are contained in analyzer/tests/ and use this unit test mode.
An example unit test of C is described in this section.
- -unittest
Activate unit test mode.
- -unittest-filter <f1>,<f2>,...,<fn>
List of test functions to analyze (default: empty).
If not specified, all the global functions starting with
test_
will be considered as test functions.
Contract-Based Stubs
Stubs can actually be written in alternate languages, based on contracts, pre- and post-conditions, and logic formulas, instead of imperative statements. For instance, there is a specific syntax for C contracts. However, a large part of the analysis of contracts is independent from the host language and implemented in Universal domains as a result.
- -stub-ignore-case <function1>.<case1>,...,<functionn>.<casen>
List of cases to ignore in specific stubs (default: empty).
Stub contracts can feature
case
statements to indicate alternate behaviors for the function. Each case is labeled with a string. By default, analyzing a stub will join all the possible cases. With this option, it is possible to ignore certain cases, given by their label, of given function stubs. This is useful, for instance, to assume that library functions (such asmalloc
oropen
) never fail (by ignoring, respectively, casesmalloc.failure
oropen.failure
).
- -stub-use-forall-loop-evaluation
Use a fallback evaluation of universally quantified formulas, using loops.
Gogul Balakrishnan, Thomas W. Reps: Recency-Abstraction for Heap-Allocated Storage. SAS 2006: 221–239.