MOPSA Guide 📖

1. Introduction to MOPSA

MOPSA stands for Modular and Open Platform for Static Analysis, a powerful framework designed to simplify the development and application of static analyzers. At its core, MOPSA leverages the theory of abstract interpretation to provide a generic and sound platform for building static analyses.

What makes MOPSA truly unique is its language-agnostic and abstraction-independent nature. Developers have the freedom to integrate various abstractions—such as numeric, pointer, or memory analyses—and add support for new languages via custom syntax iterators. Moreover, MOPSA fosters a modular approach by encouraging the development of independent abstractions that can seamlessly collaborate or combine to enhance analysis precision.

Currently, MOPSA supports the static analysis of Python, C, and Python+C programs. Its key capabilities include:

• Detecting run-time errors in C programs,
• Identifying uncaught exceptions in Python programs.

MOPSA analyses are flow and context-sensitive, ensuring a deep understanding of control-flow operators and function calls through virtual inlining. While the C analysis is actively maintained, the Python and Python+C analyses, although functional on real-world examples, are not under active development.

Additional Resources

• Explore our benchmarks to see what MOPSA can analyze.
• Access the user manual for detailed instructions.

(Ensure sphinx is installed with pip install sphinx sphinx_rtd_theme.)

2. Universal Grammar

The Universal Grammar defines the structure and syntax for the Universal programming language. A program written in Universal consists of a sequence of variable and function declarations, followed by a main block that represents the core logic of the program.

Grammar Definition

The grammar rules for the Universal language are succinctly expressed using a formal notation. These rules ensure that all components of the language—such as declarations, statements, and expressions—adhere to a consistent syntax, enabling precise parsing and execution. Below is the grammar:

Examples

The following code demonstrates a valid Universal program. It showcases essential features such as variable declarations, function definitions, and basic operations:

                                        
int x = 0;
int y; // Variables can be uninitialized.

// This is a function that computes the successor of an integer.
int successor(int n) {
    return n + 1;
}

// Floating point numbers have type `real`.
real f = 0.1;
real square(real to_square) {
    return to_square * to_square;
}

// Strings have type `string`.
string s1 = "a";
string s2 = "bb";

// The declarations are over, and we have the main code block.

x = successor(x);    // Variables can be set to arbitrary expressions.
f = randf(0.1, 0.2); // `randf(f1, f2)` returns a random real number in the range [f1,f2].
s1 = rand();         // Creates a random string
s1 = s2 @ s2;        // Strings can be concatenated with the `@` and `+` operators.
x = |s1|;            // The |str| operator returns the length of strings.
y = true;            // Boolean constants are converted to integers. `true` is 1 and `false` is 0.
print();             // `print()` makes the analyzer print the abstract state.

                                    

3. Configuration

The first step in setting up an analysis with Mopsa is choosing a configuration. This is done using the -config option, although a default configuration can also be used if the option is not specified (which is what we did implicitly in our previous analyses).

Mopsa is based on the concept of abstract domains: modules that explain how to handle certain language constructs (such as loops or dynamic memory allocation) and provide alternate approximate representations of program states with various cost-precision trade-offs (such as keeping only lower and upper bounds of integer program variables). To achieve a high degree of modularity and multi-language support, an analysis is composed of a large set of collaborating domains that can be swapped in and out. This composition is described in more details in the publication VSTTE19.

A configuration file in Mopsa specifies:

• the language analyzed (currently C, Python, or Universal),
• the list of abstract domains to use and their relationship.

4. Code examples

int_tests.u
Load in code editor Copy
1
void test_int_declaration() { int x = 1; assert(x == 1); } void test_int_addition() { int x = 1; int y = 2; assert(x + y == 3); } void test_int_substraction() { int x = 10; int y = 2; assert(x - y == 8); }
loop_tests.u
Load in code editor Copy
1
void test_simple_widening() { int i = 0; while (i < 100) { i = i + 1; } assert(i == 100); }
function_tests.u
Load in code editor Copy
1
int succ(int x) { return x + 1; } int max(int x, int y) { if (x > y) { return x; } else { return y; } } void test_call() { int x = 1; assert(succ(x) == 2); } void test_call_in_declaration() { int x = succ(0); assert(x == 1); } void test_call_and_binop() { int x = succ(0) + 1; assert(x == 2); } void test_nested() { int x = 1; int y = max(x, max(x+1, x+2)); assert(y == 3); }
string_tests.u
Load in code editor Copy
1
void test_len_of_constant() { string s = "hello"; int l = |s|; assert(l == 5); } void test_len_of_concat() { string s1 = "hello"; string s2 = " "; string s3 = "world"; int l = |s1@s2@s3|; assert(l == 11); }