Add format characters to __SMACK_code

We updated the syntax supported in `__SMACK_code` to include
format characters for specifying types of the passed arguments.
This way a user can avoid argument promotion that happens
by default when vararg functions are invoked. Also updated
`math.c` to use this new __SMACK_code syntax.

Closes #413

Author: shaobo-he

docs/boogie-code.md

@@ -38,6 +38,33 @@ void assume(bool 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:
+```C
+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:
+```C
+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

lib/smack/SmackRep.cpp

@@ -1002,6 +1002,11 @@ const Stmt* SmackRep::call(llvm::Function* f, const llvm::User& ci) {
   return Stmt::call(procName(f, ci), args, rets);
 }
 
+// we use C-style format characters
+// (https://docs.python.org/2.7/library/struct.html#format-characters)
+// e.g., @f means the variable is a float
+// while @h means the variable is a short
+// absence of a format character means use the promoted type as is
 std::string SmackRep::code(llvm::CallInst& ci) {
 
   llvm::Function* f = ci.getCalledFunction();
@@ -1012,13 +1017,48 @@ std::string SmackRep::code(llvm::CallInst& ci) {
 
   std::string s = fmt;
   for (unsigned i=1; i<ci.getNumOperands()-1; i++) {
-    const Expr* a = arg(f, i, ci.getOperand(i));
+    Value* argV = ci.getOperand(i);
     std::string::size_type idx = s.find('@');
     assert(idx != std::string::npos && "inline code: too many arguments.");
 
+    llvm::Type* targetType = argV->getType();
+    bool isCast = false;
+    if (idx + 1 < s.length()) {
+      switch(s[idx+1]) {
+      case 'c':
+      case 'b':
+      case 'B':
+        targetType = Type::getInt8Ty(argV->getContext());
+        isCast = true;
+        break;
+      case 'f':
+        targetType = Type::getFloatTy(argV->getContext());
+        isCast = true;
+        break;
+      case 'h':
+      case 'H':
+        targetType = Type::getInt16Ty(argV->getContext());
+        isCast = true;
+        break;
+      case 'i':
+      case 'I':
+        targetType = Type::getInt32Ty(argV->getContext());
+        isCast = true;
+        break;
+      default:
+        break;
+      }
+    }
+    if (argV->getType() != targetType) {
+      assert(isa<CastInst>(argV) && "Expected a cast expression.");
+      CastInst* c = llvm::cast<CastInst>(argV);
+      argV = c->getOperand(0);
+      assert(argV->getType() == targetType && "Argument type does not match specified type.");
+    }
+
     std::ostringstream ss;
-    a->print(ss);
-    s = s.replace(idx,1,ss.str());
+    arg(f, i, argV)->print(ss);
+    s = s.replace(idx,(isCast ? 2 : 1),ss.str());
   }
   return s;
 }

share/smack/lib/math.c

@@ -5,23 +5,23 @@
 #include <smack.h>
 
 float fabsf(float x) {
-  double ret = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $abs.bvfloat(dtf($rmode, @)));", ret, x);
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $abs.bvfloat(@f);", ret, x);
   return ret;
 }
 
 float fdimf(float x, float y) {
   if (__isnanf(x) || __isnanf(y)) {
     return nanf(0);
   }
-  double val = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $fsub.bvfloat($rmode, dtf($rmode, @), dtf($rmode, @)));", val, x, y);
+  float val = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $fsub.bvfloat($rmode, @f, @f);", val, x, y);
   return fmaxf(0.0f, val);
 }
 
 float roundf(float x) {
-  double ret = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $round.bvfloat(RNA, dtf($rmode, @)));", ret, x);
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $round.bvfloat(RNA, @f);", ret, x);
   return ret;
 }
 
@@ -30,14 +30,14 @@ long lroundf(float x) {
 }
 
 float rintf(float x) {
-  double ret = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $round.bvfloat($rmode, dtf($rmode, @)));", ret, x);
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $round.bvfloat($rmode, @f);", ret, x);
   return ret;
 }
 
 float nearbyintf(float x) {
-  double ret = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $round.bvfloat($rmode, dtf($rmode, @)));", ret, x);
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $round.bvfloat($rmode, @f);", ret, x);
   return ret;
 }
 
@@ -46,68 +46,68 @@ long lrintf(float x) {
 }
 
 float floorf(float x) {
-  double ret = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $round.bvfloat(RTN, dtf($rmode, @)));", ret, x);
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $round.bvfloat(RTN, @f);", ret, x);
   return ret;
 }
 
 float ceilf(float x) {
-  double ret = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $round.bvfloat(RTP, dtf($rmode, @)));", ret, x);
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $round.bvfloat(RTP, @f);", ret, x);
   return ret;
 }
 
 float truncf(float x) {
-  double ret = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $round.bvfloat(RTZ, dtf($rmode, @)));", ret, x);
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $round.bvfloat(RTZ, @f);", ret, x);
   return ret;
 }
 
 float sqrtf(float x) {
-  double ret = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $sqrt.bvfloat($rmode, dtf($rmode, @)));", ret, x);
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $sqrt.bvfloat($rmode, @f);", ret, x);
   return ret;
 }
 
 float remainderf(float x, float y) {
-  double ret = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $frem.bvfloat(dtf($rmode, @), dtf($rmode, @)));", ret, x, y);
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $frem.bvfloat(@f, @f);", ret, x, y);
   return ret;
 }
 
 float fminf(float x, float y) {
-  double ret = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $min.bvfloat(dtf($rmode, @), dtf($rmode, @)));", ret, x, y);
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $min.bvfloat(@f, @f);", ret, x, y);
   return ret;
 }
 
 float fmaxf(float x, float y) {
-  double ret = __VERIFIER_nondet_double();
-  __SMACK_code("@ := ftd($rmode, $max.bvfloat(dtf($rmode, @), dtf($rmode, @)));", ret, x, y);
+  float ret = __VERIFIER_nondet_float();
+  __SMACK_code("@f := $max.bvfloat(@f, @f);", ret, x, y);
   return ret;
 }
 
 float fmodf(float x, float y) {
    if (__isnanf(x) || __isnanf(y) || __isinff(x) || __iszerof(y)) {
     return nanf(0);
   }
-  double ret = __VERIFIER_nondet_double();
+  float ret = __VERIFIER_nondet_float();
   y = fabsf(y);
   ret = remainderf(fabsf(x), y);
   if (__signbitf(ret)) {
-    __SMACK_code("@ := ftd($rmode, $fadd.bvfloat($rmode, dtf($rmode, @), dtf($rmode, @)));", ret, ret, y);
+    __SMACK_code("@f := $fadd.bvfloat($rmode, @f, @f);", ret, ret, y);
   }
   return copysignf(ret, x);
 }
 
 float modff(float x, float *iPart) {
-  double fPart = __VERIFIER_nondet_double();
+  float fPart = __VERIFIER_nondet_float();
   if (__isinff(x)) {
     *iPart = x;
     fPart = 0.0f;
   } else {
     *iPart = truncf(x);
-    __SMACK_code("@ := ftd($rmode, $fsub.bvfloat($rmode, dtf($rmode, @), dtf($rmode, @)));", fPart, x, *iPart);
+    __SMACK_code("@f := $fsub.bvfloat($rmode, @f, @f);", fPart, x, *iPart);
   }
   if (__iszerof(fPart)) {
     fPart = __signbitf(x) ? -0.0f : 0.0f;
@@ -131,31 +131,31 @@ float nanf(const char *c) {
 
 int __isnormalf(float x) {
   int ret = __VERIFIER_nondet_int();
-  __SMACK_code("@ := if $isnormal.bvfloat.bool(dtf($rmode, @)) then $1 else $0;", ret, x);
+  __SMACK_code("@ := if $isnormal.bvfloat.bool(@f) then $1 else $0;", ret, x);
   return ret;
 }
 
 int __issubnormalf(float x) {
   int ret = __VERIFIER_nondet_int();
-  __SMACK_code("@ := if $issubnormal.bvfloat.bool(dtf($rmode, @)) then $1 else $0;", ret, x);
+  __SMACK_code("@ := if $issubnormal.bvfloat.bool(@f) then $1 else $0;", ret, x);
   return ret;
 }
 
 int __iszerof(float x) {
   int ret = __VERIFIER_nondet_int();
-  __SMACK_code("@ := if $iszero.bvfloat.bool(dtf($rmode, @)) then $1 else $0;", ret, x);
+  __SMACK_code("@ := if $iszero.bvfloat.bool(@f) then $1 else $0;", ret, x);
   return ret;
 }
 
 int __isinff(float x) {
   int ret = __VERIFIER_nondet_int();
-  __SMACK_code("@ := if $isinfinite.bvfloat.bool(dtf($rmode, @)) then $1 else $0;", ret, x);
+  __SMACK_code("@ := if $isinfinite.bvfloat.bool(@f) then $1 else $0;", ret, x);
   return ret;
 }
 
 int __isnanf(float x) {
   int ret = __VERIFIER_nondet_int();
-  __SMACK_code("@ := if $isnan.bvfloat.bool(dtf($rmode, @)) then $1 else $0;", ret, x);
+  __SMACK_code("@ := if $isnan.bvfloat.bool(@f) then $1 else $0;", ret, x);
   return ret;
 }
 

test/bits/smack_code_annot.c

@@ -0,0 +1,44 @@
+#include "smack.h"
+
+// @expect verified
+
+typedef unsigned int u32;
+typedef unsigned short u16;
+typedef unsigned char u8;
+
+u32 u16_to_u32(u16 x) {
+  u32 ret = __VERIFIER_nondet_unsigned_int();
+  __SMACK_code("@i := $zext.bv16.bv32(@h);", ret, x);
+  return ret;
+}
+
+u32 u8_to_u32(u8 x) {
+  u32 ret = __VERIFIER_nondet_unsigned_int();
+  __SMACK_code("@I := $zext.bv8.bv32(@c);", ret, x);
+  return ret;
+}
+
+u16 u16_id(u16 x) {
+  u16 ret = __VERIFIER_nondet_unsigned_short();
+  __SMACK_code("@H := @h;", ret, x);
+  return ret;
+}
+
+u8 u8_id(u8 x) {
+  u8 ret = __VERIFIER_nondet_unsigned_char();
+  __SMACK_code("@b := @B;", ret, x);
+  return ret;
+}
+
+int main(void) {
+  u8 x8 = __VERIFIER_nondet_unsigned_char();
+  u8 y8 = __VERIFIER_nondet_unsigned_char();
+  u16 x16 = __VERIFIER_nondet_unsigned_short();
+  u16 y16 = __VERIFIER_nondet_unsigned_short();
+  assume(u8_id(x8) > u8_id(y8));
+  assume(u16_id(x16) > u16_id(y16));
+  assert(u8_to_u32(x8) > u8_to_u32(y8));
+  assert(u16_to_u32(x16) > u16_to_u32(y16));
+  return 0;
+}
+

test/bits/smack_code_annot_fail.c

@@ -0,0 +1,44 @@
+#include "smack.h"
+
+// @expect error
+
+typedef unsigned int u32;
+typedef unsigned short u16;
+typedef unsigned char u8;
+
+u32 u16_to_u32(u16 x) {
+  u32 ret = __VERIFIER_nondet_unsigned_int();
+  __SMACK_code("@i := $zext.bv16.bv32(@h);", ret, x);
+  return ret;
+}
+
+u32 u8_to_u32(u8 x) {
+  u32 ret = __VERIFIER_nondet_unsigned_int();
+  __SMACK_code("@i := $zext.bv8.bv32(@c);", ret, x);
+  return ret;
+}
+
+u16 u16_id(u16 x) {
+  u16 ret = __VERIFIER_nondet_unsigned_short();
+  __SMACK_code("@H := @h;", ret, x);
+  return ret;
+}
+
+u8 u8_id(u8 x) {
+  u8 ret = __VERIFIER_nondet_unsigned_char();
+  __SMACK_code("@b := @B;", ret, x);
+  return ret;
+}
+
+int main(void) {
+  u8 x8 = __VERIFIER_nondet_unsigned_char();
+  u8 y8 = __VERIFIER_nondet_unsigned_char();
+  u16 x16 = __VERIFIER_nondet_unsigned_short();
+  u16 y16 = __VERIFIER_nondet_unsigned_short();
+  assume(u8_id(x8) > u8_id(y8));
+  assume(u16_id(x16) > u16_id(y16));
+  assert(u8_to_u32(x8) < u8_to_u32(y8));
+  assert(u16_to_u32(x16) > u16_to_u32(y16));
+  return 0;
+}
+

test/float/smack_code_annot.c

@@ -0,0 +1,15 @@
+#include "smack.h"
+
+// @expect verified
+
+double f16_to_f32(float x) {
+  double ret = __VERIFIER_nondet_double();
+  __SMACK_code("@ := ftd(RNE, @f);", ret, x);
+  return ret;
+}
+
+int main(void) {
+  assert(f16_to_f32(2.0f) == 2.0);
+  return 0;
+}
+

test/float/smack_code_annot_fail.c

@@ -0,0 +1,15 @@
+#include "smack.h"
+
+// @expect error
+
+double f16_to_f32(float x) {
+  double ret = __VERIFIER_nondet_double();
+  __SMACK_code("@ := ftd(RNE, @f);", ret, x);
+  return ret;
+}
+
+int main(void) {
+  assert(f16_to_f32(2.0f) != 2.0);
+  return 0;
+}
+