MetAcsl

MetAcsl is a plugin that extends the usual ACSL syntax to allow the specification of so-called meta-properties. A meta-property can express program properties pertaining to a large set of functions and can express memory-related constraints easily. For more information, see 2(#paper).

Installation

If your Frama-C is installed via opam, you just have to run opam install .
Otherwise, run the usual autoconf && ./configure && make && make install

Usage

In MetAcsl, every declaration is a command preceded by the meta keyword followed by its arguments. A command can appear anywhere as a global property, as long as every used term is in scope.

The only available command for now is \prop, which declares a meta-property.

The translation of such meta-properties into regular ACSL specifications can then be requested on the Frama-C command-line using the -meta option.
Every other option (such as -wp or -print) must be after -meta -then-last for the result to be correct.

Every assertion generated by MetAcsl is identified by : property_name: meta:. The meta prefix can be removed with -meta-no-add-prefix.

Furthermore, option -meta-number-assertions can be used to add another name to each assertion generated from a given meta-property. This name is of the form _nnn, where nnn is unique within each annotated function. Hence, with this option, each generated meta assertion is identified uniquely by the property_name, the function to which it belongs, and this id.

Finally, generated annotations are normally tied to the statement upon which they apply. Option -meta-separate-annots will generate no-op instructions and tie each annotation to a separate instruction, forcing the order in which they ought to be considered.

Several other options are available: use frama-c -meta-h for more information.

Basic meta-property

A meta-property is declared with the \prop command and must be in the following form, where \flags(f), is optional:

meta \prop, \name(str), \targets(TS), \context(C), \flags(f), P;

• str is a C string or an identifier and will be used to distinguish the generated ACSL annotations related to this meta-property
• TS is a target set
• C a context,
• f a list of flags
• P an ACSL predicate, potentially referring to meta-variables (see Context).

Some simple examples can be found in tests/ and more complete case studies can be found in examples/

Target

The target set is the set of functions for which the defined property will have to hold. It is specified using the usual ACSL set constructs such as {a, b} (where a and b are C function names), \union and \intersect.

We also add the \diff function to specify the difference between two sets and the builtin \ALL set, the set of every function in the program.

One can also use the \in_file function to select all functions defined in a given file.

Finally, it is possible to use \callees(s) to refer to the functions in s and all their callees recursively. Of course, \callers(s) will include s and all their callers recursively up to the main entry point. In presence of function pointers, MetAcsl will rely on the Callgraph plugin, which either uses the results of Eva if an analysis has been launched before, or considers the set of all functions that have a type compatible with the pointer.

For example, the target set \diff(\ALL, \union({foo, bar}, \in_file("main.c"))) describes all functions except foo, bar or any function defined in main.c.

By default, if a function name does not correspond to a function in the program under analysis, Frama-C will be aborted. This can be changed by setting the status of warning category unknown-func to a suitable value, e.g. -meta-warn-key unknown-func=enable, to keep a warning when such a case occurs, or -meta-warn-key unknown-func=disable to silently ignore this fact.

Note that if you disable the warning in order to use the same meta-properties on a full code base and on a reduced one where some functions have been removed, the resulting targets in the reduced case might not be the intersection of the targets in full case with the functions of the reduced case. For instance, if f1 calls f2 and only f2 is included in the reduced case, \callees({f1}) will be the empty set (since f1 is ignored as unknown function) in the reduced case, and { f1, f2 } in the full case. Similarly \diff(\ALL,\callees({f1})) will include f2 in the reduced case, but not in the full case.

Context

The context is the situation in a target function in which the property must hold. It can be one of the following :

• \conditional_invariant : the property P is guaranteed to be verified at the end of the target function if it is verified at the begining.
• \precond : the property P is a precondition of the target function and it must hold at each of its callsites.
• \postcond : the property P holds at the end of the target function for every initial state satisfying the preconditions of the function.
• \weak_invariant : the property P is guaranteed to be verified at the beginning and end of the target function.
• \strong_invariant : the property P must hold at every point of the target function.
  • A statement (and its children) can be ignored and left unchecked by adding meta lenient to its contract, in case the invariant needs to be locally broken.
• \writing : P is to be valid each time the memory is written to in the body of the target function. In this context, P can use the \written meta-variable, which is the address of the location (or set of locations) being modified.
  • By default, if f calls g and g has no definition, every state modification that could happen in g (according to its assigns specification) is considered by being equivalent to assignements in the body of f and thus will be checked.
  • In that case, if g does not specify a memory footprint, it is assumed that it respects all related meta-properties.
  • This can be disabled with option -meta-no-check-ext
• \reading : symmetrical to \writing. P can use the \read variable.
  • Undefined callees are checked using their \from specification if existing.
• \calling : the property must hold at each function call and can refer to the \called variable.

In all contexts, the property can refer to the \func variable to denote the current target function.

Flags

The processing of a meta-property is parameterized by a set of flags that can be modified through the \flags directive, which should be inserted between \context and the predicate.

Currently, two flags can be set:

• proof : how the meta-property should be proved. It can have one of three values
  • local (by default) : the meta-property is proved iff every generated instance is proved (by some other plugin)
  • axiom : the meta-property is admitted
  • deduce : the plugin tries to deduce the property from the other meta-properties (see Deduction)
• translate : toggles the translation of the property into local assertions
  • no, false : disabled (forbidden if proof is local)
  • yes, true (by default) : enabled with default mode
  • check : enabled, forcing mode to checks (property proved then forgotten)
  • assert : enabled, forcing mode to assertions (property proved then used for future proofs)
  • Note: the default mode can be configured via -meta-checks or -meta-asserts respectively. Default is to generate asserts.

Example : deduce the property at high-level and do not generate low-level assertions for it

meta \prop, \name(deduced_property),
    \targets(\ALL), \context(\weak_invariant),
    \flags(proof:deduce, translate:false),
    A == B

Extensions

Labels

The default location assumed in P when referring to a variable is before any statement relevant to the chosen context. However, this can be made explicit using the Before and After labels in conjunction to the \at ACSL construct.

For example, the following meta-property ensure that the variable x never decreases. To express that, we say that for every memory modification, either x is not modified or it has not decreased before and after the modification.

meta \prop, \name(no_decrease)),
    \targets(\ALL), \context(\writing),
    \separated(\written, &x) ||
    \at(x, Before) >= \at(x, After)

Note Beware that currently, if there is at least one After label used in P, then the default location assumed becomes After as well and any reference to the Before state must be made explicitely.

Relaxing strong invariants

When using the strong invariant context, the property must be valid at every point of the target functions. As this is not always possible, we provide a way to locally relax a strong invariant: adding //@ imeta lenient before the beginning of a block will disable checks for any strong invariants inside that block.

For example, say we want to check that A == B is a strong invariant, but allow updating the value of both. As A and B cannot be updated at the same time, we have to relax the invariant during that update:

void set_AB(int v) {
    //@ imeta lenient
    {
        A = v;
        B = v;
    }
}

Beware that this construct effectively reduces the strength of a strong invariant: use it with parcimony.

Guarding against type errors

When using the writing, read or calling contexts, nothing is known about the type of \written, \read and \called at specification time, except that those are (sets of) pointers to unknown types. Any use of those variables that is not generic enough may provoke a crash at translation time.

However, such uses are sometimes necessary (for example when referring to formals). In that case, we allow to guard an unsafe expression with either \tguard or \fguard. When the inner expression is ill-typed, it is respectively replaced by \true or \false.

For example a meta-property with the predicate \tguard(\written->foo == 0) will ensure that no modification of structures having a foo field will be done if that field is nonzero. For the other variables, nothing will be checked (\true).

Furthermore, to explicitely assert that a meta-variable must be of a certain type, one can use \assert_type((type) variable), which will either be replaced by \true if the variable has the correct type , or will throw a typing error (to be guarded with the above predicates).

For example, the following predicate will ensure that all variables of some enumeration type can only have a restricted set of values :

    \tguard(\assert_type((enum Foo*) \written) ==>
        (\at(*\written, After) == ONE ||
        \at(*\written, After) == TWO)

Referring to function parameters

When it is known that a set of functions have a common parameter (with the same name), it can be useful to use that parameter (or formal) in a meta-property, using the \formal(parameter_name) construct.

Upon translation, it is replaced by the parameter if it is available in a particular function, and throw a typing error otherwise. Hence, the expression using \formal should be surrounded by a guard.

Referring to call parameters

When using the \calling context and targetting a specific called function, it is possible to refer to the value provided for a formal at every call site, using \called_arg(parameter_name). It throws a type error when the called function does not have the specified formal, is indirectly called (through a function pointer) or is a variadic function. Thus it should be surrounded by a guard.

For example, the following meta-property states that parameter x of float sqrt(float x) should never be provided with a negative value.

meta \prop,
    \name(sqrt_pos),
    \targets(\ALL),
    \context(\calling),
    \tguard(\called == sqrt ==> \fguard(\called_arg(x) >= 0.));

Referring to bound names (experimental)

If it is not possible to rely on a consistent naming of formals across functions, there is a notion of binding in MetAcsl, achieved through two special functions, \bind and \bound.

The first one is to be used outside of a meta-property, in an //@ imeta annotation in the body of a C function, to bind a name to the value of a C expression at that point. This name can then be used in a meta-property to formulate an interesting property about the value it refers to, using \bound as a meta-variable. A name can actually be bound multiple times to different value at different points of a program, meaning that the name inside a meta-property refers to the whole set of associated values. Note that the bound values are constant but may be pointers referring to changing memory.

As an example, see the following code where we bind every pointer returned by create_cell, and formulate a property about that set of values in the meta-property.

int lock;
int* create_cell() {
	char* c = malloc(1);
	//@ imeta \bind(c, cells);
	return c;
}
int safe_modify_cell
(int* cell, int val) {
	if(!lock) {
		lock = 1;
		*cell = val;
		lock = 0;
		return 0;
	}
	else return -1;
}
void unsafe_modify_cell
(int* cl, int val) {
	*cll = val;
}

/*@ //Pointers returned by create_cell
	//are not modified if the lock is on
	meta \prop,
	\name(cell_modif_is_critical),
	\targets(\ALL), \context(\writing),
	\separated(\written, \bound(cells)) || lock;
*/

The specification is instrumented with ghost code and dynamic arrays to represent the bound sets.

Note Since the instrumentation of that construct is made using ghost code, expect static proofs to be difficult, especially using WP. Dynamic arrays in particular may pose problem. If a limit on the size of the set can be determined, on can use -meta-static-bindings L to use static arrays of size L instead.

Deduction (experimental)

In some specific cases, MetAcsl is able to deduce a meta-property from others. Such a deduction must be manually requested by the proof:deduce flag. For the feature to work, swi-prolog must be installed on your system, as the deduction engine is in Prolog. The validity of that engine is guaranteed by Why3 proofs available in proofs/

This deduction at high-level can be useful for global properties that are hard to prove at low level but easy to deduce. While proved at high level, deduced properties can still be translated into admitted low-level assertions, which can in turn be used to prove other properties at low level.

Currently, two deductions can be made :

• if it is proved that a function and all of its callees do not modify a global variable (via meta-properties in the form of \separated(\written, &v)), then we can deduce that the value of that variable is unchanged after each of these functions.
• if the right conditions are met (unclear for now), an invariant that is proved on one function can be extended to others that do not modify the free variables of the invariant

Note This functionnality uses the {log} CLP, included in the distribution of MetAcsl in share/ and released under the GPLv3 licence (see the SETLOG_LICENSE file).

Bibliography

[1] MetAcsl: Specification and Verification of High-Level Properties, TACAS, 2019 (pdf)
[2] Tame Your Annotations with MetAcsl: Specifying, Testing, and Proving High-Level Properties (pdf)