Merge branch 'release-1.3.1'

Makefile.common.in

@@ -1,6 +1,6 @@
 # Set the name of the project here
 PROJECT_NAME := smack
-PROJ_VERSION := 1.3.0
+PROJ_VERSION := 1.3.1
 
 # Set this variable to the top of the LLVM source tree.
 LLVM_SRC_ROOT = @LLVM_SRC@

Makefile.llvm.config.in

@@ -59,7 +59,7 @@ PROJ_SRC_DIR := $(call realpath, $(PROJ_SRC_ROOT)/$(patsubst $(PROJ_OBJ_ROOT)%,%
 prefix          := $(PROJ_INSTALL_ROOT)
 PROJ_prefix     := $(prefix)
 ifndef PROJ_VERSION
-PROJ_VERSION := 1.3.0
+PROJ_VERSION := 1.3.1
 endif
 
 PROJ_bindir     := $(PROJ_prefix)/bin

bin/llvm2bpl.py

@@ -7,7 +7,7 @@
 import io
 import platform
 
-VERSION = '1.3.0'
+VERSION = '1.3.1'
 
 
 def is_valid_file(parser, arg):
@@ -75,6 +75,12 @@ def llvm2bpl(scriptPathName, infile, debugFlag, memmod):
   output = p.communicate()[1]
   bplStartIndex = output.find('// SMACK-PRELUDE-BEGIN')
   debug = output[0:bplStartIndex]
+  if p.returncode != 0:
+    if debugFlag:
+      print debug
+    print >> sys.stderr, "LLVM/SMACK encountered an error:"
+    print >> sys.stderr, output[0:1000], "... (output truncated)"
+    sys.exit("LLVM/SMACK returned exit status %s" % p.returncode)
   bpl = output[bplStartIndex:]
   return debug, bpl
 

bin/smack-verify.py

@@ -8,7 +8,7 @@
 import platform
 from smackgen import *
 
-VERSION = '1.3.0'
+VERSION = '1.3.1'
 
 
 def generateSourceErrorTrace(boogieOutput, bpl):

bin/smackgen.py

@@ -7,7 +7,7 @@
 import platform
 from llvm2bpl import *
 
-VERSION = '1.3.0'
+VERSION = '1.3.1'
 
 
 def smackParser():

configure

@@ -1,6 +1,6 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.69 for SMACK 1.3.0.
+# Generated by GNU Autoconf 2.69 for SMACK 1.3.1.
 #
 # Report bugs to <smack-dev@googlegroups.com>.
 #
@@ -580,8 +580,8 @@ MAKEFLAGS=
 # Identity of this package.
 PACKAGE_NAME='SMACK'
 PACKAGE_TARNAME='smack'
-PACKAGE_VERSION='1.3.0'
-PACKAGE_STRING='SMACK 1.3.0'
+PACKAGE_VERSION='1.3.1'
+PACKAGE_STRING='SMACK 1.3.1'
 PACKAGE_BUGREPORT='smack-dev@googlegroups.com'
 PACKAGE_URL='http://github.com/smackers/smack'
 
@@ -1406,7 +1406,7 @@ if test "$ac_init_help" = "long"; then
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF
-\`configure' configures SMACK 1.3.0 to adapt to many kinds of systems.
+\`configure' configures SMACK 1.3.1 to adapt to many kinds of systems.
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
@@ -1472,7 +1472,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
-     short | recursive ) echo "Configuration of SMACK 1.3.0:";;
+     short | recursive ) echo "Configuration of SMACK 1.3.1:";;
    esac
   cat <<\_ACEOF
 
@@ -1621,7 +1621,7 @@ fi
 test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
-SMACK configure 1.3.0
+SMACK configure 1.3.1
 generated by GNU Autoconf 2.69
 
 Copyright (C) 2012 Free Software Foundation, Inc.
@@ -2170,7 +2170,7 @@ cat >config.log <<_ACEOF
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
-It was created by SMACK $as_me 1.3.0, which was
+It was created by SMACK $as_me 1.3.1, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   $ $0 $@
@@ -13430,7 +13430,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # report actual input values of CONFIG_FILES etc. instead of their
 # values after options handling.
 ac_log="
-This file was extended by SMACK $as_me 1.3.0, which was
+This file was extended by SMACK $as_me 1.3.1, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
@@ -13487,7 +13487,7 @@ _ACEOF
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
 ac_cs_version="\\
-SMACK config.status 1.3.0
+SMACK config.status 1.3.1
 configured by $0, generated by GNU Autoconf 2.69,
   with options \\"\$ac_cs_config\\"
 

examples/failing/Makefile

@@ -2,7 +2,8 @@ CC = clang
 INC = ../../include/smack
 CFLAGS = -c -Wall -emit-llvm -O0 -g -I$(INC)
 
-SOURCES = globals_func_ptr.c
+SOURCES = globals_func_ptr.c \
+          struct_return.c
 
 BITCODE = $(SOURCES:.c=.bc)
 

examples/failing/struct_return.c

@@ -0,0 +1,20 @@
+#include "smack.h"
+
+struct a {
+  long i;
+  long j;
+};
+
+struct a foo(struct a bar) {
+  bar.i = 10;
+  bar.j = 20;
+  return bar;
+}
+
+int main(void) {
+  struct a x;
+  x = foo(x);
+  __SMACK_assert(x.j == 20);
+  return 0;
+}
+

include/smack/SmackRep.h

@@ -200,7 +200,7 @@ class SmackRep {
   const Expr* undef();
   const Expr* lit(const llvm::Value* v);
   const Expr* lit(unsigned v);
-  const Expr* ptrArith(llvm::Value* p, vector<llvm::Value*> ps,
+  const Expr* ptrArith(const llvm::Value* p, vector<llvm::Value*> ps,
                        vector<llvm::Type*> ts);
   const Expr* expr(const llvm::Value* v);
   const Expr* op(llvm::BinaryOperator& o);

lib/AssistDS/DSNodeEquivs.cpp

@@ -245,7 +245,12 @@ const DSNode *DSNodeEquivs::getMemberForValue(const Value *V) {
     std::deque<const User *> WL;
     SmallSet<const User *, 8> Visited;
 
-    WL.insert(WL.end(), V->use_begin(), V->use_end());
+    // BEGIN BANDAGE: caught a bug here after upgrade to OSX Mavericks
+    // ORIGINAL: WL.insert(WL.end(), V->use_begin(), V->use_end());
+    for ( llvm::Value::const_use_iterator i = V->use_begin(); i != V->use_end(); ++i )
+      WL.push_back(*i);
+    // END BANDAGE
+
     do {
       const User *TheUser = WL.front();
       WL.pop_front();

lib/smack/SmackRep.cpp

@@ -461,7 +461,7 @@ const Expr* SmackRep::lit(unsigned v) {
 }
 
 const Expr* SmackRep::ptrArith(
-  llvm::Value* p, vector<llvm::Value*> ps, vector<llvm::Type*> ts) {
+  const llvm::Value* p, vector<llvm::Value*> ps, vector<llvm::Type*> ts) {
 
   assert(ps.size() > 0 && ps.size() == ts.size());
 
@@ -782,16 +782,26 @@ void SmackRep::addStaticInit(const llvm::Value* v) {
   if (const GlobalVariable* g = dyn_cast<const GlobalVariable>(v)) {
 
     if (g->hasInitializer()) {
-      const Value* i = g->getInitializer();
+      const Constant* init = g->getInitializer();
 
-      if (isInt(i))
-        staticInits.push_back(Stmt::assign(mem(g),expr(i)));
+      if (isInt(init))
+        staticInits.push_back(Stmt::assign(mem(g),expr(init)));
 
-      else if (i->getType()->isArrayTy()) {
-        ArrayType* t = (ArrayType*) i->getType();
+      else if (init->getType()->isArrayTy()) {
+        ArrayType* t = (ArrayType*) init->getType();
         extraDecls.push_back(Decl::axiom(Expr::eq(
           Expr::fn("$size",Expr::id(id(g))),lit(t->getNumElements()))));
       }
+
+      else if (init->getType()->isStructTy()) {
+        StructType* t = (StructType*) init->getType();
+        for (unsigned i = 0, e = t->getNumElements(); i != e; ++i) {
+          Constant* c = init->getAggregateElement(i);
+          assert(isInt(c));
+          staticInits.push_back(Stmt::assign(Expr::sel(
+              Expr::id(memReg(getRegion(g))), pa(expr(g), 1, fieldOffset(t, i))),expr(c)));
+        }
+      }
     }
   }
 }

test/Makefile

@@ -24,6 +24,7 @@ SOURCES = simple.c simple_fail.c \
           nested_struct.c nested_struct_fail.c \
           nested_struct1.c nested_struct1_fail.c \
           nested_struct2.c nested_struct2_fail.c \
+          struct_assign.c struct_assign_fail.c \
           func_ptr.c func_ptr_fail.c \
           func_ptr1.c func_ptr1_fail.c \
           array.c \

test/regtest-corral.py

@@ -44,6 +44,8 @@
   ('nested_struct1_fail',r'This assertion can fail'),
   ('nested_struct2',     r'Program has no bugs'),
   ('nested_struct2_fail',r'This assertion can fail'),
+  ('struct_assign',      r'Program has no bugs'),
+  ('struct_assign_fail', r'This assertion can fail'),
   ('func_ptr',           r'Program has no bugs'),
   ('func_ptr_fail',      r'This assertion can fail'),
   ('func_ptr1',          r'Program has no bugs'),

test/regtest.py

@@ -44,6 +44,8 @@
   ('nested_struct1_fail',r'0 verified, 1 errors?'),
   ('nested_struct2',     r'1 verified, 0 errors?'),
   ('nested_struct2_fail',r'0 verified, 1 errors?'),
+  ('struct_assign',      r'1 verified, 0 errors?'),
+  ('struct_assign_fail', r'0 verified, 1 errors?'),
   ('func_ptr',           r'1 verified, 0 errors?'),
   ('func_ptr_fail',      r'0 verified, 1 errors?'),
   ('func_ptr1',          r'1 verified, 0 errors?'),

test/struct_assign.c

@@ -0,0 +1,13 @@
+#include "smack.h"
+
+struct a {
+  int i;
+  int j;
+};
+
+int main(void) {
+  struct a x = {10, 20};
+  __SMACK_assert(x.j == 20);
+  return 0;
+}
+

test/struct_assign_fail.c

@@ -0,0 +1,13 @@
+#include "smack.h"
+
+struct a {
+  int i;
+  int j;
+};
+
+int main(void) {
+  struct a x = {10, 20};
+  __SMACK_assert(x.j == 10);
+  return 0;
+}
+