SpecificationAutomata.md

CPAchecker specification automata

The specification automata language used here is similar to the BLAST Query Language.

Syntax of the specification automata language

Each specification (Specification) consists of one or more automata (Automaton), which alternatively can be presented as an assertion (Assertion).

Each automaton is defined by the following attributes:

• unique automaton identifier;
• type of automaton (OBSERVER or CONTROL);
• automata variables (LocalDefs);
• initial automaton state identifier (InitDef);
• automaton states (StateDefs).

Each automaton state contains the following information:

• state name;
• whether it is a target (error) state or not (StateTypeDef);
• whether it is a nondeterministic state or not (StateNonDetDef);
• automaton transitions (Transitions).

Each automaton transition is determined by:

• trigger (Trigger), which is a boolean expression;
• list of assertions (Assertions), which are checked, if a trigger is evaluated as true;
• list of actions (Actions), which are executed, if assertions are held;
• assumption (Assume), which is a C-expression, that is passed to the other CPAs for evaluation after actions execution;
• identifier of the state, in which automaton will transfer, if assumption is evaluated as true (Goto).

The semantics of the operations are presented in the next section.

The specification automata language grammar

The full grammar is presented in the parser.cup file. Here is a simplified version without actions:

Specification ::= Automaton Specification | Assertion ; Specification |

Automaton ::= OBSERVER Body | CONTROL Body | Body

Body ::= AUTOMATON IDENTIFIER LocalDefs InitDef StateDefs END AUTOMATON

InitDef ::= INITIAL STATE IDENTIFIER ;

LocalDefs ::= LocalDef LocalDefs |

LocalDef ::=
    LOCAL IDENTIFIER IDENTIFIER ;
  | LOCAL IDENTIFIER < IDENTIFIER > IDENTIFIER ;
  | LOCAL IDENTIFIER < IDENTIFIER > IDENTIFIER = SQUAREEXPR ;
  | LOCAL IDENTIFIER IDENTIFIER = ConstantInt ;

StateDefs ::= StateDef StateDefs |

StateDef ::= StateTypeDef STATE StateNonDetDef IDENTIFIER : Transitions

StateTypeDef ::= TARGET |

StateNonDetDef ::= USEFIRST | USEALL |

Transitions ::= Transition Transitions |

Transition ::= Trigger -> Assertions Assume Actions Goto ;

Trigger ::= Bool

Assertions ::= Assertion Assertions |

Assertion ::= ASSERT Bool

Assume ::= ASSUME CURLYEXPR |

Actions ::= Action Actions |

Goto ::= GOTO IDENTIFIER | ERROR | ERROR ( STRING_LITERAL ) | STOP | BREAK

Action ::=
    DO IDENTIFIER = InnerInt
  | DO IDENTIFIER SQUAREEXPR = SetValue
  | PRINT PrintArguments
  | MODIFY ( IDENTIFIER , STRING_LITERAL )

SetValue ::= TRUE | FALSE

PrintArguments ::= Expression PrintArguments |

Int ::= ConstantInt | ( Int ) | IDENTIFIER | InnerInt + InnerInt | InnerInt - InnerInt

InnerInt ::= Int | EVAL ( IDENTIFIER , STRING_LITERAL )

ConstantInt ::= INTEGER_LITERAL

Bool ::=
    TRUE
  | FALSE
  | ! Bool
  | ( Bool )
  | InnerInt == InnerInt
  | InnerInt != InnerInt
  | Bool == Bool
  | Bool != Bool
  | Bool && Bool
  | Bool || Bool
  | MATCH STRING_LITERAL
  | MATCH CURLYEXPR
  | MATCH SQUAREEXPR
  | MATCH LABEL STRING_LITERAL
  | MATCH LABEL SQUAREEXPR
  | MATCH ASSERT
  | MATCH EXIT
  | MATCH ENTRY
  | MATCH FUNCTIONCALL STRING_LITERAL
  | CHECK ( IDENTIFIER , STRING_LITERAL )
  | CHECK ( STRING_LITERAL )
  | CHECK ( IS_TARGET_STATE )
  | COVERS_LINES ( Integers )

Integers ::= ConstantInt Integers |

Expression ::=
    Int
  | Bool
  | STRING_LITERAL
  | EVAL ( IDENTIFIER , STRING_LITERAL )

IDENTIFIER ::= LETTER [DIGIT | LETTER]*
LETTER ::= _$a-zA-Z
DIGIT ::= 0-9
STRING_LITERAL ::= " [^"\n\r]* "
INTEGER_LITERAL ::= 0 | 1-9 DIGIT*
CURLYEXPR ::= { [^{}\n\r]* }
SQUAREEXPR ::= [ [^[]\n\r]* ]

Semantics of the specification automata language

Specification automata represent a property, which can be expressed as a temporal logic formula, and thus indicate a set of correct program executions, for which this formula is evaluated as true. A property is held in a program, if all possible program executions are included into a corresponding set of correct program executions.

CPAchecker creates a CPA for each specification automaton depending on its type. ObserverAutomatonCPA is used if automaton type is OBSERVER, and ControlAutomatonCPA is used if automaton type is CONTROL. Observer automaton cannot modify other CPAs (i.e. it cannot use keywords MODIFY and STOP). By default control automaton is used.

This CPA uses MergeSepOperator, StopSepOperator, BreakOnTargetsPrecisionAdjustment and FlatLatticeDomain. On transfer relation computation this CPA creates a new AutomatonState based on current CFA edge, automaton transitions and other CPA states. If a new state is error (target) state or transition assertion is violated, then automaton CPA sends a BREAK signal to other CPAs. If property is represented as several specification automata, then each of them will be transformed into a separated CPA.

More information about automaton CPA can be found in the third section of the paper On-the-Fly Decomposition of Specifications in Software Model Checking.

Automata variables

Automata variables are defined in the LocalDefs section, then can be read from the Bool sections (which can be part of sections Trigger, Assertions and Actions) and the Assume sections, and can be modified in the Actions section. Supported variables types are int and set.

In order to access automata variable value from the Assume section one should add "$$" as a prefix to the variable name (for example, expression $$var is used to read value of the automaton variable var).

Int variable

Represents an integer number.

Declaration:

LOCAL int var_name;

or

LOCAL int var_name = int_const;

where int_const corresponds to INTEGER_LITERAL in grammar (which is a natural number or zero). If int_const is not specified, then variable value is set to zero.

Integer variable returns its value on access, and changes its value on modification.

Set variable

Represents a set of some elements.

Declaration:

LOCAL set var_name <elem_type>;

or

LOCAL set var_name <elem_type> = set_const;

where elem_type is the type of set elements, set_const is the initial set value. The type of set elements can be either int (corresponds to INTEGER_LITERAL in grammar) or string (corresponds to STRING_LITERAL in grammar). The initial set value is [elem_1, ..., elem_n], where n>=0 and elem_i is either INTEGER_LITERAL or STRING_LITERAL. Note, that type of elem_i must correspond to elem_type.

Access operations:

• var_name[elem] - returns true, if element elem is contained in the var_name set and false otherwise;
• var_name.empty - returns true, if the var_name set is empty and false otherwise.

Modification operations:

var_name[elem]=true|false - on true element elem is added to the var_name set, on false element elem is removed from the var_name set. Note, that type of element elem must be the same as the type of the var_name set elements.

Automata states

There are 3 predefined automata states:

• ERROR represents error (target) state;
• STOP represents BOTTOM state in CPA (transfer relation is not calculated from this state);
• BREAK is used to halt the analysis without being a target state.

One automaton state must be marked as initial in InitDef.

Transition to the error (target) state means property violation. Any user-defined state can be marked as a target state (with keyword TARGET), which then will be treated similar to the ERROR state.

If automaton state is marked with the USEFIRST keyword, then its transitions are applied until the first successful match. Otherwise (i.e. if the USEALL keyword is specified) all matched for the current CFA edge automaton transitions are used.

Each checked property may contain several violation (in different automata transitions or in different automata specifications). In order to differentiate those violations, transitions to the ERROR state can be marked with specific string: ERROR ("error message").

Each automaton transition must have identifier of the state, in which automaton will transfer, if assumption is evaluated as true (the Goto section). If automaton should stay in the same state on some transition, then identifier of the same state should be used.

Transition triggers

Transition trigger is a Bool expression, which is evaluated on transfer relation computation based on the given CFA edge and other CPA states. If this expression is evaluated as true, then transition is taken, otherwise it is rejected.

This expression may contain standard boolean operations (!, (, ), ==, !=, && and ||), constants TRUE and FALSE and specific operations:

• int_1 == int_2 or int_1 != int_2 matches if expression is true, where int_i is an expression of integer constants, automata variables, addition and subtraction operations and EVAL(cpa_name, query) operation. In order to evaluate this query, the CPA with name cpa_name name must present in a CompositeCPA and must implement method evaluateProperty, which can parse string query. If these conditions are not satisfied, then the operation returns warning message as a result. For example, operation EVAL(location, "lineno") sends query lineno to the LocationCPA, which returns line number of the analyzed CFA edge.
• MATCH "stmt" matches if string stmt is equal to the corresponding CFA edge C-statement.
• MATCH {stmt} matches if evaluated C-statement stmt is compared to the CFA edge C-statement with a tree comparison algorithm. Statement stmt must be a correct C-statement. For this match a set of transition variables is created, which are filled with joker expressions ($? and $<number>). If statement stmt contains CFunctionCallExpression or CAssignment inside, joker expressions are substituted to assignment right-hand side or left-hand side or function return value or function arguments. The expression $? is substituted to any pattern, but is not tracked, whereas each substituted name by $<number> is added to transition variables and can be used in this transition later. For example:
  • pattern x = $? matches CFA edge x = 5;, transition variables are {};
  • pattern x = $1 matches CFA edge x = 5;, transition variables are {$1=5};
  • pattern $1 = $? matches CFA edge x = 5;, transition variables are {$1=x};
  • pattern f($?) matches CFA edges f() and f(x, y), transition variables are {};
  • pattern f($1) matches CFA edge f(x), transition variables are {$1=x};
  • pattern $1 = f($?) matches CFA edges y = f(x) and y = f(x1, x2), transition variables are {$1=y};
  • pattern $1 = f($2) matches CFA edge y = f(x), transition variables are {$1=y, $2=x}.
• MATCH [expr] matches if the CFA edge C-statement matches regular expression expr.
• MATCH LABEL name matches if the CFA edge is a label with name name.
• MATCH LABEL [expr] matches if the CFA edge is a label with name, which matches regular expression expr.
• MATCH ASSERT matches special edge "assert fail" added by CPAchecker.
• MATCH EXIT matches if successor state has no leaving edges.
• MATCH ENTRY matches if predecessor state has no entering edges.
• MATCH FUNCTIONCALL functionname matches if the CFA edge contains a functioncall with the given functionname.
• CHECK (cpa_name, query) matches if CompositeCPA contains CPA with name cpa_name, which implements method checkProperty, which returns true for string query. For example, CHECK(location, "functionName==f") returns true, if LocationCPA is inside function f.
• CHECK (query) matches if at least one CPA from CompositeCPA implements method checkProperty, which returns true for string query.
• CHECK (IS_TARGET_STATE) matches if at least on CPA from CompositeCPA is in target state.
• COVERS_LINES (int_1 int_2 ... int_n) matches if lines int_1 int_2 ... int_n are covered.

Transition trigger must present on each automaton transition.

Transition assertions

Transition assertions are Bool expressions, which are checked, if a transition trigger is evaluated as true. This expression is similar to the transition trigger. If this expression is evaluated as false, it is treated similar to transition to the ERROR state, otherwise automaton actions are executed. The automaton assertions may not be specified on automaton transition.

Transition actions

Transition actions are executed after successful checking of transition assertions. The following actions are supported:

• DO action allows to modify values of automata variables based on its type:
  • Int variables: DO var = expr, where var is an integer automata variable name, expr may contain integer automata variables and transition variables (if MATCH {expr} expression was used in the transition). For example, action var = var + 1 increments integer variable var, action var = $1, where transition variables are {$1=1}, assigns 1 to the var variable.
  • Set variables: DO var[elem] = true|false, where elem should be either a constant (INTEGER_LITERAL or STRING_LITERAL correspondingly) or automata integer variable or transition variable (if MATCH {expr} expression was used in the transition). The type of elem element must be the same as the type of the var set elements. For example, assuming that var is the set of strings, action var["elem"]=true adds string element elem to the var set, action var[$1]=false, where transition variables are {$1="x"}, removes string element x from the var set.
• PRINT expr action prints the value of specified expression. It does not affect the analysis. The expression may contain automata variables and transition variables. The following expressions are supported:
  • a boolean expression (the Bool section);
  • an integer expression (the Int section);
  • a string constant (STRING_LITERAL);
  • EVAL (cpa_name, query) expression.
• MODIFY (cpa_name, "expr") action modifies CPA cpa_name with expr. In order to support this operation corresponding CPA must implement method modifyProperty, which can parse string expr. This action can only be executes inside CONTROL automaton. String expr may contain automata variables and transition variables. For example, action MODIFY (ValueAnalysis, "setvalue(x==$$var)") sets to variable x value of automata variable var in ValueAnalysisCPA.

The automaton actions may not be specified on automaton transition.

Transition assumptions

If trigger is evaluated as true and assertion holds for an automaton transition, then transition to the other automaton state will be created on transfer relation computation, but it may contain additional assumption (the Assume section):

ASSUME {expr_1; expr_2; ...; expr_n}, where n>=1, expr_i is a C-expression.

This assumption represent a conjunction of expr_i C-expressions, which are evaluated by other CPAs in general case.

The assumption may either restrict abstract state for the automation transition (for example, by adding assumption as a predicate) or reject the automaton transition, if it never evaluates as true. In order to create disjunction of assumptions one should add several transition, for example:

TRUE -> ASSUME {expr_1} ...
TRUE -> ASSUME {expr_2} ...

In this case 2 automaton transitions will be created with different assumptions, which is equal to the expression expr_1 || expr_2.

Each C-expression expr_i may contain automata variables or transition variable (if MATCH {expr} expression was used in the transition), which are substituted before passing to the other CPAs. It also must be successfully parsed by C-parser. If expression expr_i gets a conflicting type, then it should be casted to required type. Note, that assumptions are evaluated after execution of actions, which may modify automaton variables from assumptions.

Examples of assumptions

Let us consider, that there are int automaton variable var_1 with value 0, set automaton variable of strings var_2 with value ["arg_2"] and transition variables {$1="arg_1", $2="arg_2"}, where type of arg_1 is int, type of arg_2 is size_t.

Then assumption:

• $$var_1 > 0 is evaluated to 0 > 0 - transition will be rejected unconditionally;
• $$var_1 == 0 is evaluated to 0 == 0 - transition will be taken unconditionally;
• $$var_2[$1] is evaluated to 0 - element arg_1 is not contained in the var_2 set - transition will be rejected unconditionally;
• $$var_2[$2] is evaluated to 1 - element arg_2 is contained in the var_2 set - transition will be taken unconditionally;
• $$var_2.empty is evaluated to 0 - the var_2 set is not empty - transition will be rejected unconditionally;
• $1 > $$var_1 is evaluated to arg_1 > 0 - transition will be taken with additional predicate arg_1 > 0;
• $2 > $$var_1 cannot be evaluated due to different types (size_t and int);
• ((int)$2) > $$var_1 is evaluated to (int)arg_2 > 0 - transition will be taken with additional predicate (int)arg_2 > 0;
• $1; ((int)$2) == 0; $$var_2[$2] is evaluated to arg_1 != 0 && (int)arg_2 == 0 && 1 - transition will be taken with additional predicate arg_1 != 0 && (int)arg_2;
• !$1; $$var_2[$1] is evaluated to arg_1 == 0 && 0 — transition will be rejected unconditionally.

Examples of specification automata

The examples of specification automata can be found in the config/specification and test/config/automata directories.