Skip to content

Latest commit

 

History

History
82 lines (72 loc) · 3.24 KB

boogie-code.md

File metadata and controls

82 lines (72 loc) · 3.24 KB
Raw

Inline Boogie Code

In order to pass custom Boogie code through SMACK's translation from C code, SMACK interprets calls to the following procedures (declared in smack.h) specially:

  • void __SMACK_code(const char *fmt, ...);

  • void __SMACK_decl(const char *fmt, ...);

  • void __SMACK_top_decl(const char *fmt, ...);

SMACK translates the call __SMACK_code("assume x == y;") directly into the Boogie statement assume x == y;. For variable declarations, SMACK translates the call __SMACK_decl("var x: int;") into a declaration var x: int; in the calling procedure, and the call __SMACK_top_decl("var y: int;") into a global declaration var y: int. This last form can in fact be used for any kind of global declaration, for instance,

__SMACK_top_decl("function f(int,int) returns (int);")
__SMACK_top_decl("axiom f(0,0) == 10;")

declares a Boogie function f constrained by the axiom f(0,0) == 10.

Given this functionality, it can also be useful to write custom Boogie code which uses program values defined in the source-level C code. This is made possible by interpreting the string passed as the first argument to __SMACK_code, __SMACK_decl, and __SMACK_top_decl as a format string, in which each occurrence of the @ symbol is replaced by a subsequent argument. For instance, consider the following implementations of smack.h

void assert(bool v) {
  __SMACK_code("assert @ != 0;", v);
}
void assume(bool v) {
  __SMACK_code("assume @ != 0;", v);
}

SMACK interprets the @ symbol by inserting the value of the C variable v. Since the arguments of variadic functions may be promoted, SMACK allows users to append a format character to the @ symbol as an indicator that the argument, rather than its promoted form, should be used in the format string. We allow the following format characters (inspired by Python and C) for the respective C types: c (char), b (signed char), B (unsigned char), h (signed short), H (unsigned short), i (signed int), I (unsigned int) and f (float).

For example, without using such annotations, the definition of the floorf function is:

float floorf(float x) {
  double ret = __VERIFIER_nondet_double();
  __SMACK_code("@ := ftd($rmode, $round.bvfloat(RTN, dtf($rmode, @)));", ret, x);
   return ret;
 }

where the ftd and dtf functions are conversions between float and double variables that are needed to deal with the promotion of the arguments. Whereas a better definition using these annotations is:

float floorf(float x) {
  float ret = __VERIFIER_nondet_float();
  __SMACK_code("@f := $round.bvfloat(RTN, @f);", ret, x);
   return ret;
 }

One application of this functionality which has been valuable to the authors of SMACK is in encoding concurrency primitives into the generated Boogie code. The following generates four procedure calls marked as asynchronous:

__SMACK_decl("var x: int;");
__SMACK_code("call {:async} @(@);", Push, 1);
__SMACK_code("call {:async} @(@);", Push, 2);
__SMACK_code("call {:async} x := @();", Pop);
__SMACK_code("call {:async} x := @();", Pop);

While the {:async} attributes have no intrinsic meaning in Boogie, they can be used as directives for other tools that interpret concurrency primitives, such as Corral.