Skip to content

Boogie

Jump to bottom
Matthias Heizmann edited this page Oct 8, 2022 · 24 revisions

Deviations

We deviate from the original Boogie specification as follows.

  • We extended Boogie by structs (see Markus Lindemann master thesis, or an example that illustrates the extension).

  • According to the Boogie specification the operators for division / and modulo % do not have a meaning. We use a fixed semantics, namely the euclidean division (as used in SMT-LIB2)

  • If the program has a procedure with the identifier ULTIMATE.start, Ultimate will only consider program executions that start in this procedure.

  • Each quantifier introduces its own scope. In Section 4.4 the Boogie specification says:

    The bound variables among the IdsType ’s must be distinct and must be different from local variables, parameters, and other bound variables in scope (but they may have the same names as constants and global variables).

    We omit this restriction and assume that each quantifier starts a new scope in which variables that have the same name as quantified variables are shadowed.

Extensions

  • We extended Boogie by reals (according to the extension proposed by Rustan)
  • We extended by Boogie by structs. (TODO documentation needed) A struct is syntactic sugar for a list of variables. The BoogiePreprocessor will replace the struct by the list of variables.
  • We allow attributes on call statements, i.e., call {:some_id "some_string"} bar(); is a valid call statement.
  • We extended Boogie by an atomic statement. This extension is yet (2018-12-03) tentative.
    Motivation: We want to allow a programmer to specify that several statements are executed in one step. This is relevant for the following applications.
    1. Concurrent programs: the active thread must not change while an atomic statement is executed.
    2. Temporal logic: atomic propositions must not be evaluated while an atomic block is executed.
    3. Fault localization: if the Boogie program was obtained from a C program we do not want to analyze if a single Boogie statement is responsible for a bug, instead we want to do this analysis for a sequence of Boogie statements that stem from the same C statement.
      Syntax: atomic { <stmt> } where <stmt> is a statement (which can be a composition of statements)
      Semantics: (yet to be defined in the terminology of Boogie) The atomic statement may only contain code that does not allow infinite executions (no loops) The code inside an atomic statement is executed in one step.
      Limitations of our implementation: The code that occurs inside an atomic statement must not contain branches. Currently, only the following is allowed: Assume statements, Assignment statements, Havoc statements, Gotos whose target is a single label and this label is the successor of the Goto, and Calls to procedures that neither have an implementation nor a non-free requires clause.
      Example: See atomic.bpl
  • We introduced a fork statement and a join statement to allow a concurrent execution of code and dynamic thread creation. This extension is documented here.

Semantics of attributes

Attribute-defined directives

  • If a function func has the attribute {:inline true} the BoogiePreprocessor will inline this function (in case the function has a body).

  • If a function func has the attribute {:overapproximation "bar"} our model checkers will never output a counterexample that contains func. Instead our model checkers will say unknown and will say that an overapproximation of bar is the reason for saying unknown.

Using SMT-LIB semantics for functions

If a function func has the attribute {:builtin "foo"} the RCFGBuilder will

  • assume that the SMT-LIB logic that the user selected has a function foo
  • translate the function func to an SMT function with the name foo.

If a function func has the attribute {:indices k_1 k_2 ... k_n} where each k_i is an IntegerLiteral the RCFGBuilder will translate func to an SMT function that has the indices k_1 k_2 ... k_n.

If a function func has the attribute {:const_array}, the RCFGBuilder will replace all calls to that function with a built-in SMT function that creates constant array. The function func must take one argument of some boogie type T and must return a Boogie array type [...]T. For an example, see ConstArray.bpl.

If a function func has the attribute {:smtdefined "<term>"}, the RCFGBuilder will replace all calls to that function with an inlining of the SMT term <term>. The user has to take care that the parameter and return types and the parameter names of the Boogie function definition match the sort of the term and the free variables of the term. If one of the types is a struct type, one can use the :expand_struct attribute. For an example, see StructFunctionAttributesTest.bpl.

A function can use the attribute { :expand_struct "<fieldid>" } to define how a struct return type should be expanded when using {:smtdefined "<term>"}. Consider the following example taken from StructFunctionAttributesTest.bpl.

type rational = { n, d: int, v:real };
function 
  { :expand_struct "n" } { :smtdefined "(+ n 0)" } 
  { :expand_struct "d" } { :smtdefined "(+ d 0)" } 
  { :expand_struct "v" } { :smtdefined "(/ (to_real n) (to_real d))" } 
  foo(n:int, d:int) returns (out:rational);

The function foo has two parameters of type int and returns a rational. rational is a struct with three fields. Normally, we can just eliminate all struct types during our preprocessing and replace this function with three new ones, one for each struct field. But because we want to be able to use the attribute { :smtdefined "<term>" }, we need a way to tell the preprocessor how to fill each field of the struct. We do that with { :expand_struct "<fieldid>" }. This attribute specifies that all following attributes until the next { :expand_struct "<fieldid>" } should be copied to the function that is created for the struct field named <fieldid>. The preprocessor then creates the following Boogie code for the example above.

function { :smtdefined "(+ n 0)" } foo.n(n : int, d : int) returns (out : int);
function { :smtdefined "(+ d 0)" } foo.d(n : int, d : int) returns (out : int);
function { :smtdefined "(/ (to_real n) (to_real d))" } foo.v(n : int, d : int) returns (out : real);

If you use nested struct types, you have to specify the fully expanded field id, e.g. n.x1.x2.

LTL specifications

  • If the program contains a statement of the form assume { :ltl_step } true, then all statements between two assume { :ltl_step } true statements of each execution will be considered as one step. Furthermore, the statements between the beginning of an execution and the first assume { :ltl_step } true will be considered as one step.
  • It is not allowed to use the attribute ltl_step for other statements than assume true.
  • If the program does not contain any statement of the form assume { :ltl_step } true, then every statement in the result of the BoogiePreprocessor will be considered as one step. Hence, the semantics can only be understood by people that know the internal details of the BoogiePreprocessor. We recommend to use only LTL formulas without the next step operator or to use assume { :ltl_step } true statements.
Clone this wiki locally