Input Erlang Programs

A typical Erlang module that can be analysed by Soter looks like the following:

-module(example).
-compile(export_all).

-include_lib("soter.hrl").

-soter_config(peano).

-uncoverable("wrong_incipit > 0").

main() ->
    N = any_nat(),
    P = spawn(fun()-> f(N) end),
    P ! {hi, self()} ,
    receive
        X -> X
    end.

any_nat() -> ?SoterChoice(
        fun()-> 0 end,
        fun()-> any_nat()+1 end
    ).

f(N) ->
    receive
        {hi, P} ->
            P ! {hey, N}
            start_protocol(N, P);
        bla ->
            ?label(wrong_incipit),
            complain(N)
    end.

...

The soter.hrl library is included and makes the Soter macros such as ?SoterChoice or ?label, available.

The directive -soter_config sets some Soter options.

The -uncoverable directive is one way of specifying a property to be proved by Soter.

There is a main/0 function which serves as entry point for the program.

The definition of any_nat makes use of one of the Soter macros which introduce a non-deterministic choice; in this example any_nat would be able to non-deterministically generate every positive integer.

The other definitions are standard Erlang definitions which must meet some constraints outlined in the Limitations section.

All the modules accepted by Soter can be executed with the Erlang interpreter without modification and are valid Erlang programs.

Limitations

Soter deals with a `pure' core fragment of the Erlang language.

A partial list of the unsupported features follows:

• The rich module system of Erlang is not handled. Calls to external modules and module variables are not supported.

• Built in functions are not supported apart from send, self and error. In particular, arithmetic functions are treated as external unknown calls. Limited manipulation of natural numbers is available via the --peano switch (see below).

• Guards (when) and type-checking functions are not supported.

• Monitors, links, exception handling are currently not supported.

• Impure features such as process dictionaries or registration of names is not supported.

• Timeouts in receives are simply ignored.

• Multi node distributed behaviour is not taken in account.

Recent versions of the Erlang compiler introduced some breaking changes to Core Erlang. The latest version of Erlang known to be (mostly) compatible with Soter is version 20.

If you encounter errors, a common source of incompatibility is compiler annotations around generated variables, a situation that arises from using the catch-all pattern _. Try and use a throw-away variable name like _1 instead. For example, a pattern like:

case {a,b} of
    _ -> ok
end.

might need to be rewritten as

case {a,b} of
    {_1, _2} -> ok
end.

The peano Option

Since arithmetic operations are not currently supported, all the data-types need to be constructed as trees using the tuple and list constructors plus atoms. For example, integers can be encoded using the atom zero as a representation for 0 and {s, N} as a representation for the successor of a number N. Since writing numbers and operations with this notation can be cumbersome, Soter offers the --peano option which treats integer literals as syntactic sugar for numbers encoded as illustrated above. Addition/subtraction to a constant is translated in the corresponding operation on peano numbers. These are the only supported arithmetic operations when the peano option is selected.

From the code the peano option can be activated by inserting the directive

-soter_config(peano).

Note: if the peano option is switched off, any call to + or - will be translated to a "dead-end" node representing a call to an unknown function.

The Soter Macros

In order to write assertions in an Erlang module, Soter provides a set of macros defined in the file soter.hrl that can be imported by putting

-include_lib("soter.hrl").

after the -module directive and before any definition.

The header file grammars.hrl defines some commonly used non-deterministic generator of inputs. It depends on soter.hrl and must be imported with

-include_lib("grammars.hrl").

after every other include since it defines functions rather than macros.

Important: The inclusion of soter.hrl and grammars.hrl is automatic and implicit in the web interface; the -module and the -include_lib directives should not be used in the web interface.