Try-Mopsa

`A Guide to Try-Mopsa 📖`

`1. Introduction to Mopsa`

Mopsa -- Modular Open Platform for Static Analysis -- is a research-oriented platform written in OCaml to build sound semantic static analyzers based on Abstract Interpretation.

Our goal with Mopsa is to encourage the research and education in Abstract Interpretation by providing a fully-featured and extensible open-source platform and usable analyses built with it.

Mopsa is language-agnostic and abstraction-independent. 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.

Try-Mopsa is a scaled-down, pure JavaScript version of Mopsa running in your browser. It works on our toy imperative language dubbed "Universal", whose grammar is provided below. You can still choose your configuration of abstract domains (including polyhedra thanks to the VPL!).

`2. Grammar of the 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`

<program> ::= <declaration>* <block> <declaration> ::= <vardecl> | <fundecl> <vardecl> ::= <type> <id>; | <type> <id> = <expr>; <fundecl> ::= <type> <id>(<type> <id>, ...) { <block> }; <type> ::= "int" | "string" <block> ::= <stmt>* <stmt> ::= <lval> = <expr>; | "if" (<expr>) { <block> } | "if" (<expr>) { <block> } "else" { <block> } | "while" (<expr>) { <block> } | "break"; | "continue"; | "return" <expr>; | "print" (); <expr> ::= <int> -- Integer number | <real> -- Real number | "true" -- True constant | "false" -- False constant | <id> -- Variable access | <unop> <expr> -- Unary expression | <expr> <binop> <expr> -- Binary expression | "rand"(<int>, <int>) -- Random integer | "rand" -- Random string | <id>(<expr>, ...) -- Function call | |<expr>| -- String length | () -- Void constructor <unop> ::= "+" | "-" | "!" <binop> ::= "+" | "-" | "*" | "/" | "<" | "==" | "!=" | "<" | "<=" | ">" | ">=" | "@"

`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;
}

// 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.
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.
print();          // Prints the abstract state
assert(y);        // Mopsa will try to prove that these assertion holds

`3. Configuration`

At analysis time, Mopsa parses its JSON configuration to create its abstract state. Each abstract domain in the configuration handle certain language constructs (such as loops or dynamic memory allocation) or provide alternate approximate representations of program states with various cost-precision trade-offs. To achieve a high degree of modularity and multi-language support, configurations are composed of a large set of collaborating domains that can be swapped in and out. This composition is described in more details in our VSTTE'19 paper.

A configuration file in Mopsa specifies:

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

Example configuration

{
    "language": "universal",
    "domain": {
        "switch": [
            // Iterators
            "universal.iterators.program",
            "universal.iterators.intraproc",
            "universal.iterators.loops",
            "universal.iterators.interproc.inlining",
            "universal.iterators.unittest",
            // Reduced product of string abstractions
            {
                "product": [
                    "universal.toy.string_length",
                    "universal.toy.string_summarization"
                ],
                "reductions": [
                    "universal.toy.string_reduction"
                ]
            },
            // Numeric abstraction, based on a reduced product between intervals and polyhedra
            {
                "product": [
                    {
                        "nonrel": {
                            "union": [
                                "universal.numeric.values.intervals.integer",
                                "universal.strings.powerset"
                            ]
                        }
                    },
                    "universal.numeric.relational"
                ],
                "reductions": [
                    "universal.numeric.reductions.intervals_rel"
                ]
            }
        ]
    }
}

`Configuration`

`Options`