Merge branch 'release-1.5.1'

.gitattributes

@@ -0,0 +1,5 @@
+# For more information on this file, please see:
+# http://git-scm.com/docs/gitattributes
+
+# detect all text files and automatically normalize them (convert CRLF to LF)
+*       text=auto

.gitignore

@@ -37,3 +37,7 @@ a.bpl
 # Generated by Boogie
 corral_out_trace.txt
 corraldebug.out
+
+# Generated by Vagrant
+.vagrant
+build

CMakeLists.txt

@@ -6,7 +6,7 @@ cmake_minimum_required(VERSION 2.8)
 project(smack)
 
 if (NOT WIN32 OR MSYS OR CYGWIN)
-  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config PATHS ${LLVM_CONFIG} NO_DEFAULT_PATH DOC "llvm-config")
+  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
 
   if (LLVM_CONFIG_EXECUTABLE STREQUAL "LLVM_CONFIG_EXECUTABLE-NOTFOUND")
     message(FATAL_ERROR "llvm-config could not be found!")
@@ -191,11 +191,19 @@ INSTALL(FILES ${CMAKE_CURRENT_SOURCE_DIR}/bin/boogie
   DESTINATION bin
 )
 
-INSTALL(FILES ${CMAKE_CURRENT_SOURCE_DIR}/include/smack/smack.h
-  ${CMAKE_CURRENT_SOURCE_DIR}/include/smack/smack-contracts.h
-  ${CMAKE_CURRENT_SOURCE_DIR}/include/smack/smack-svcomp.h
+INSTALL(FILES ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/include/smack.h
+  ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/include/smack-contracts.h
+  ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/include/smack-svcomp.h
   PERMISSIONS OWNER_EXECUTE OWNER_WRITE OWNER_READ
   GROUP_EXECUTE GROUP_READ WORLD_EXECUTE WORLD_READ
-  DESTINATION include/smack
+  DESTINATION share/smack/include
+)
+
+INSTALL(FILES ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/Makefile
+  ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack-svcomp.c
+  PERMISSIONS OWNER_EXECUTE OWNER_WRITE OWNER_READ
+  GROUP_EXECUTE GROUP_READ WORLD_EXECUTE WORLD_READ
+  DESTINATION share/smack/lib
 )
 

LICENSE

@@ -1,10 +1,11 @@
 The MIT License
 
-Copyright (c) 2008-2014 Zvonimir Rakamaric ([email protected]),
+Copyright (c) 2008-2015 Zvonimir Rakamaric ([email protected]),
                         Michael Emmi ([email protected])
-Modified work Copyright (c) 2013-2014 Pantazis Deligiannis,
+Modified work Copyright (c) 2013-2015 Pantazis Deligiannis,
                                       Montgomery Carter,
-                                      Arvind Haran
+                                      Arvind Haran,
+                                      Shaobo He
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal
@@ -46,7 +47,7 @@ In addition, a binary distribution of SMACK contains at least the following
 tools and packages, which come with their own licenses:
 - LLVM, clang, LLVM runtime (http://llvm.org/)
 - mono (http://www.mono-project.com/)
-- Boogie (http://boogie.codeplex.com/)
+- Boogie (https://github.com/boogie-org/boogie/)
 - Corral (http://corral.codeplex.com/)
-- Z3 (http://z3.codeplex.com/), Non-Commercial Use Only
+- Z3 (https://github.com/Z3Prover/z3/)
 

Makefile.common.in

@@ -1,6 +1,6 @@
 # Set the name of the project here
 PROJECT_NAME := smack
-PROJ_VERSION := 1.5.0
+PROJ_VERSION := 1.5.1
 
 # Set this variable to the top of the LLVM source tree.
 LLVM_SRC_ROOT = @LLVM_SRC@
@@ -29,3 +29,7 @@ include $(PROJ_SRC_ROOT)/Makefile.llvm.rules
 
 # SMACK-specific scripts
 include $(PROJ_SRC_ROOT)/Makefile.smack.scripts
+
+# SMACK share
+include $(PROJ_SRC_ROOT)/Makefile.smack.share
+

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.5.0
+PROJ_VERSION := 1.5.1
 endif
 
 PROJ_bindir     := $(PROJ_prefix)/bin

Makefile.llvm.rules

@@ -2041,57 +2041,57 @@ ifeq ($(LEVEL),.)
 #------------------------------------------------------------------------
 # Install support for the project's include files:
 #------------------------------------------------------------------------
-ifdef NO_INSTALL
-install-local::
-	$(Echo) Install circumvented with NO_INSTALL
-uninstall-local::
-	$(Echo) Uninstall circumvented with NO_INSTALL
-else
-install-local::
-	$(Echo) Installing include files
-	$(Verb) $(MKDIR) $(DESTDIR)$(PROJ_includedir)
-	$(Verb) if test -d "$(PROJ_SRC_ROOT)/include" ; then \
-	  cd $(PROJ_SRC_ROOT)/include && \
-	  for hdr in `find . -type f \
-	      '(' -name "smack*.h" ')' -print | grep -v CVS | \
-	      grep -v .svn` ; do \
-	    instdir=`dirname "$(DESTDIR)$(PROJ_includedir)/$$hdr"` ; \
-	    if test \! -d "$$instdir" ; then \
-	      $(EchoCmd) Making install directory $$instdir ; \
-	      $(MKDIR) $$instdir ;\
-	    fi ; \
-	    $(DataInstall) $$hdr $(DESTDIR)$(PROJ_includedir)/$$hdr ; \
-	  done ; \
-	fi
-ifneq ($(PROJ_SRC_ROOT),$(PROJ_OBJ_ROOT))
-	$(Verb) if test -d "$(PROJ_OBJ_ROOT)/include" ; then \
-	  cd $(PROJ_OBJ_ROOT)/include && \
-	  for hdr in `find . -type f \
-	      '(' -name "smack*.h" ')' -print | grep -v CVS | \
-	      grep -v .svn` ; do \
-	    instdir=`dirname "$(DESTDIR)$(PROJ_includedir)/$$hdr"` ; \
-	    if test \! -d "$$instdir" ; then \
-	      $(EchoCmd) Making install directory $$instdir ; \
-	      $(MKDIR) $$instdir ;\
-	    fi ; \
-	    $(DataInstall) $$hdr $(DESTDIR)$(PROJ_includedir)/$$hdr ; \
-	  done ; \
-	fi
-endif
-
-uninstall-local::
-	$(Echo) Uninstalling include files
-	$(Verb) if [ -d "$(PROJ_SRC_ROOT)/include" ] ; then \
-	  cd $(PROJ_SRC_ROOT)/include && \
-	    $(RM) -f `find . -path '*/Internal' -prune -o '(' -type f \
-	      '!' '(' -name '*~' -o -name '.#*' \
-        -o -name '*.in' ')' -print ')' | \
-        grep -v CVS | sed 's#^#$(DESTDIR)$(PROJ_includedir)/#'` ; \
-	  cd $(PROJ_SRC_ROOT)/include && \
-	    $(RM) -f `find . -path '*/Internal' -prune -o '(' -type f -name '*.in' \
-      -print ')' | sed 's#\.in$$##;s#^#$(DESTDIR)$(PROJ_includedir)/#'` ; \
-	fi
-endif
+#ifdef NO_INSTALL
+#install-local::
+#	$(Echo) Install circumvented with NO_INSTALL
+#uninstall-local::
+#	$(Echo) Uninstall circumvented with NO_INSTALL
+#else
+#install-local::
+#	$(Echo) Installing include files
+#	$(Verb) $(MKDIR) $(DESTDIR)$(PROJ_includedir)
+#	$(Verb) if test -d "$(PROJ_SRC_ROOT)/include" ; then \
+#	  cd $(PROJ_SRC_ROOT)/include && \
+#	  for hdr in `find . -type f \
+#	      '(' -name "smack*.h" ')' -print | grep -v CVS | \
+#	      grep -v .svn` ; do \
+#	    instdir=`dirname "$(DESTDIR)$(PROJ_includedir)/$$hdr"` ; \
+#	    if test \! -d "$$instdir" ; then \
+#	      $(EchoCmd) Making install directory $$instdir ; \
+#	      $(MKDIR) $$instdir ;\
+#	    fi ; \
+#	    $(DataInstall) $$hdr $(DESTDIR)$(PROJ_includedir)/$$hdr ; \
+#	  done ; \
+#	fi
+#ifneq ($(PROJ_SRC_ROOT),$(PROJ_OBJ_ROOT))
+#	$(Verb) if test -d "$(PROJ_OBJ_ROOT)/include" ; then \
+#	  cd $(PROJ_OBJ_ROOT)/include && \
+#	  for hdr in `find . -type f \
+#	      '(' -name "smack*.h" ')' -print | grep -v CVS | \
+#	      grep -v .svn` ; do \
+#	    instdir=`dirname "$(DESTDIR)$(PROJ_includedir)/$$hdr"` ; \
+#	    if test \! -d "$$instdir" ; then \
+#	      $(EchoCmd) Making install directory $$instdir ; \
+#	      $(MKDIR) $$instdir ;\
+#	    fi ; \
+#	    $(DataInstall) $$hdr $(DESTDIR)$(PROJ_includedir)/$$hdr ; \
+#	  done ; \
+#	fi
+#endif
+#
+#uninstall-local::
+#	$(Echo) Uninstalling include files
+#	$(Verb) if [ -d "$(PROJ_SRC_ROOT)/include" ] ; then \
+#	  cd $(PROJ_SRC_ROOT)/include && \
+#	    $(RM) -f `find . -path '*/Internal' -prune -o '(' -type f \
+#	      '!' '(' -name '*~' -o -name '.#*' \
+#        -o -name '*.in' ')' -print ')' | \
+#        grep -v CVS | sed 's#^#$(DESTDIR)$(PROJ_includedir)/#'` ; \
+#	  cd $(PROJ_SRC_ROOT)/include && \
+#	    $(RM) -f `find . -path '*/Internal' -prune -o '(' -type f -name '*.in' \
+#      -print ')' | sed 's#\.in$$##;s#^#$(DESTDIR)$(PROJ_includedir)/#'` ; \
+#	fi
+#endif
 endif
 
 check-line-length:

Makefile.smack.scripts

@@ -19,7 +19,7 @@ install-local::
          -o -name 'corral' \
 	      ')' -print | grep -v CVS | \
 	      grep -v .svn` ; do \
-	    instdir=`dirname "$(DESTDIR)$(PROJ_includedir)/$$scr"` ; \
+	    instdir=`dirname "$(DESTDIR)$(PROJ_bindir)/$$scr"` ; \
 	    if test \! -d "$$instdir" ; then \
 	      $(EchoCmd) Making install directory $$instdir ; \
 	      $(MKDIR) $$instdir ;\

Makefile.smack.share

@@ -0,0 +1,61 @@
+#------------------------------------------------------------------------
+# Installation of SMACK share
+#------------------------------------------------------------------------
+ifdef NO_INSTALL
+install-local::
+	$(Echo) Install circumvented with NO_INSTALL
+uninstall-local::
+	$(Echo) Uninstall circumvented with NO_INSTALL
+else
+install-local::
+	$(Echo) Installing share
+	$(Verb) $(MKDIR) $(DESTDIR)$(PROJ_datadir)/smack/include
+	$(Verb) if test -d "$(PROJ_SRC_ROOT)/share/smack/include" ; then \
+	  cd $(PROJ_SRC_ROOT)/share/smack/include && \
+	  for hdr in `find . -type f | \
+	      grep -v CVS | grep -v .svn` ; do \
+	    instdir=`dirname "$(DESTDIR)$(PROJ_datadir)/smack/include/$$hdr"` ; \
+	    if test \! -d "$$instdir" ; then \
+	      $(EchoCmd) Making install directory $$instdir ; \
+	      $(MKDIR) $$instdir ;\
+	    fi ; \
+	    $(DataInstall) $$hdr $(DESTDIR)$(PROJ_datadir)/smack/include/$$hdr ; \
+	  done ; \
+	fi
+	$(Verb) $(MKDIR) $(DESTDIR)$(PROJ_datadir)/smack/lib
+	$(Verb) if test -d "$(PROJ_SRC_ROOT)/share/smack/lib" ; then \
+	  cd $(PROJ_SRC_ROOT)/share/smack/lib && \
+	  for hdr in `find . -type f | \
+	      grep -v CVS | grep -v .svn` ; do \
+	    instdir=`dirname "$(DESTDIR)$(PROJ_datadir)/smack/lib/$$hdr"` ; \
+	    if test \! -d "$$instdir" ; then \
+	      $(EchoCmd) Making install directory $$instdir ; \
+	      $(MKDIR) $$instdir ;\
+	    fi ; \
+	    $(DataInstall) $$hdr $(DESTDIR)$(PROJ_datadir)/smack/lib/$$hdr ; \
+	  done ; \
+	fi
+
+uninstall-local::
+	$(Echo) Uninstalling share
+	$(Verb) if [ -d "$(PROJ_SRC_ROOT)/share/smack/include" ] ; then \
+	  cd $(PROJ_SRC_ROOT)/share/smack/include && \
+	    $(RM) -f `find . -path '*/Internal' -prune -o '(' -type f \
+	      '!' '(' -name '*~' -o -name '.#*' \
+        -o -name '*.in' ')' -print ')' | \
+        grep -v CVS | sed 's#^#$(DESTDIR)$(PROJ_datadir)/smack/include/#'` ; \
+	  cd $(PROJ_SRC_ROOT)/share/smack/include && \
+	    $(RM) -f `find . -path '*/Internal' -prune -o '(' -type f -name '*.in' \
+      -print ')' | sed 's#\.in$$##;s#^#$(DESTDIR)$(PROJ_datadir)/smack/include/#'` ; \
+	fi
+	$(Verb) if [ -d "$(PROJ_SRC_ROOT)/share/smack/lib" ] ; then \
+	  cd $(PROJ_SRC_ROOT)/share/smack/lib && \
+	    $(RM) -f `find . -path '*/Internal' -prune -o '(' -type f \
+	      '!' '(' -name '*~' -o -name '.#*' \
+        -o -name '*.in' ')' -print ')' | \
+        grep -v CVS | sed 's#^#$(DESTDIR)$(PROJ_datadir)/smack/lib/#'` ; \
+	  cd $(PROJ_SRC_ROOT)/share/smack/lib && \
+	    $(RM) -f `find . -path '*/Internal' -prune -o '(' -type f -name '*.in' \
+      -print ')' | sed 's#\.in$$##;s#^#$(DESTDIR)$(PROJ_datadir)/smack/lib/#'` ; \
+	fi
+endif

README.md

@@ -1,63 +1,49 @@
-At its core, SMACK is a translator from the [LLVM](http://www.llvm.org)
-compiler's popular intermediate representation (IR) into the
-[Boogie](http://boogie.codeplex.com) intermediate verification language (IVL).
-Sourcing LLVM IR exploits an increasing number of compiler frontends,
-optimizations, and analyses. Targeting Boogie exploits a canonical platform
-which simplifies the implementation of algorithms for verification, model
-checking, and abstract interpretation. The main purpose of SMACK is to decouple
-the implementations of verification algorithms from the details of source
-languages, and enable rapid prototyping on production code.  Our initial
-experience verifying C language programs is encouraging: SMACK is competitive
-in SV-COMP benchmarks, is able to translate large programs (100 KLOC), and is
-used in several verification research prototypes.
-
-*Please drop us a note if using SMACK in your research or teaching. We would
-love to learn more about your experience.*
-
-## A Quick Demo
+[![Build Status](http://kepler.cs.utah.edu:8080/buildStatus/icon?job=smack)](http://kepler.cs.utah.edu:8080/job/smack/)
 
+SMACK is a *bounded software verifier*, verifying the assertions in its
+input programs up to a given bound on loop iterations and recursion depth.
 SMACK can verify C programs, such as the following:
 
-    // simple.c
+    // examples/simple/simple.c
     #include "smack.h"
 
     int incr(int x) {
       return x + 1;
     }
 
     int main(void) {
-      int a;
+      int a, b;
 
-      a = 1;
+      a = b = __VERIFIER_nondet_int();
       a = incr(a);
-      assert(a == 2);
+      assert(a == b + 1);
       return 0;
     }
 
-To do so, SMACK invokes [Clang](http://clang.llvm.org) to compile `simple.c`
-into LLVM bitcode `simple.bc`:
-
-    clang -c -Wall -emit-llvm -O0 -g -I../../include/smack simple.c -o simple.bc
-
-then translates the bitcode `simple.bc` to a program in the
-[Boogie](http://boogie.codeplex.com) verification language,
+The command
 
-    smackgen.py simple.bc -o simple.bpl
+    smackverify.py simple.c
 
-and finally verifies `simple.bpl` with the [Boogie](http://boogie.codeplex.com)
-or [Corral/Duality](http://corral.codeplex.com) verifiers
+reports that the assertion `a == b + 1` cannot be violated. Besides the
+features of this very simple example, SMACK handles every complicated feature
+of the C language, including dynamic memory allocation, pointer arithmetic, and
+bitwise operations.
 
-    boogie simple.bpl
-
-concluding that the original program `simple.c` is verified to be correct.
-While SMACK is designed to be a *modular* verifier, for our convenience, this
-whole process has also been wrapped into a single command in SMACK:
-
-    smackverify.py simple.c -o simple.bpl
-
-which equally reports that the program `simple.c` is verified.
-
-## Further Information
-
-For requirements, installation, usage, and whatever else, please consult the
-[SMACK Wiki on Github](https://github.com/smackers/smack/wiki).
+Under the hood, SMACK is a translator from the [LLVM](http://www.llvm.org)
+compiler’s popular intermediate representation (IR) into the
+[Boogie](http://boogie.codeplex.com) intermediate verification language (IVL).
+Sourcing LLVM IR exploits an increasing number of compiler front-ends,
+optimizations, and analyses. Currently SMACK only supports the C language via
+the [Clang](http://clang.llvm.org) compiler, though we are working on providing
+support for additional languages. Targeting Boogie exploits a canonical
+platform which simplifies the implementation of algorithms for verification,
+model checking, and abstract interpretation. Currently, SMACK leverages the
+[Boogie](http://boogie.codeplex.com) and [Corral](http://corral.codeplex.com)
+verifiers.
+
+Consult [the Wiki](https://github.com/smackers/smack/wiki) for system
+requirements, installation, usage, and everything else.
+
+*We are very interested in your experience using SMACK. Please do contact
+[Zvonimir](mailto:[email protected]) or
+[Michael](mailto:[email protected]) with any possible feedback.*

Vagrantfile

@@ -0,0 +1,26 @@
+Vagrant.configure(2) do |config|
+
+  project_name = File.dirname(__FILE__).split("/").last
+
+  config.vm.provider "virtualbox" do |vb|
+    vb.memory = 6144 # set VM memory to 6GB
+  end
+  config.vm.synced_folder ".", "/home/vagrant/#{project_name}"
+
+  config.vm.define :ubuntu do |ubuntu_config|
+    ubuntu_config.vm.box = "ubuntu/trusty64"
+  end
+
+  # TODO ability to choose between the two?
+  # config.vm.define :opensuse do |opensuse_config|
+  #   opensuse_config.vm.box = "chef/opensuse-13.1"
+  # end
+
+  config.vm.provision "shell", binary: true, inline: <<-SHELL
+    cd /home/vagrant
+    ./#{project_name}/bin/build.sh
+    echo source smack.environment >> .bashrc
+    echo cd #{project_name} >> .bashrc
+  SHELL
+
+end