diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 000000000..6c026d6db --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,187 @@ +# +# Copyright (c) 2013 Pantazis Deligiannis (p.deligiannis@imperial.ac.uk) +# This file is distributed under the MIT License. See LICENSE for details. +# + +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") + + if (LLVM_CONFIG_EXECUTABLE STREQUAL "LLVM_CONFIG_EXECUTABLE-NOTFOUND") + message(FATAL_ERROR "llvm-config could not be found!") + endif() + + execute_process( + COMMAND ${LLVM_CONFIG_EXECUTABLE} --cxxflags + OUTPUT_VARIABLE LLVM_CXXFLAGS + OUTPUT_STRIP_TRAILING_WHITESPACE + ) + + set(LLVM_CXXFLAGS "${LLVM_CXXFLAGS} -fno-exceptions -fno-rtti") + + execute_process( + COMMAND ${LLVM_CONFIG_EXECUTABLE} --libs + OUTPUT_VARIABLE LLVM_LIBS + OUTPUT_STRIP_TRAILING_WHITESPACE + ) + + execute_process( + COMMAND ${LLVM_CONFIG_EXECUTABLE} --ldflags + OUTPUT_VARIABLE LLVM_LDFLAGS + OUTPUT_STRIP_TRAILING_WHITESPACE + ) + +else() + set(LLVM_SRC "" CACHE PATH "LLVM source directory") + set(LLVM_BUILD "" CACHE PATH "LLVM build directory") + set(LLVM_BUILD_TYPE "" CACHE STRING "LLVM build type") + + if (NOT EXISTS "${LLVM_SRC}/include/llvm") + message(FATAL_ERROR "Invalid LLVM source directory: ${LLVM_SRC}") + endif() + + set(LLVM_LIBDIR "${LLVM_BUILD}/lib/${LLVM_BUILD_TYPE}") + if (NOT EXISTS "${LLVM_LIBDIR}") + message(FATAL_ERROR "Invalid LLVM build directory: ${LLVM_BUILD}") + endif() + + set(LLVM_CXXFLAGS "\"/I${LLVM_SRC}/include\" \"/I${LLVM_BUILD}/include\" -D_SCL_SECURE_NO_WARNINGS -wd4146 -wd4244 -wd4355 -wd4482 -wd4800") + set(LLVM_LDFLAGS "") + set(LLVM_LIBS "${LLVM_LIBDIR}/LLVMTransformUtils.lib" "${LLVM_LIBDIR}/LLVMipa.lib" "${LLVM_LIBDIR}/LLVMAnalysis.lib" "${LLVM_LIBDIR}/LLVMTarget.lib" "${LLVM_LIBDIR}/LLVMMC.lib" "${LLVM_LIBDIR}/LLVMObject.lib" "${LLVM_LIBDIR}/LLVMBitReader.lib" "${LLVM_LIBDIR}/LLVMCore.lib" "${LLVM_LIBDIR}/LLVMSupport.lib") + +endif() + +include_directories(include) + +add_library(assistDS STATIC + include/assistDS/ArgCast.h + include/assistDS/FuncSimplify.h + include/assistDS/Int2PtrCmp.h + include/assistDS/SimplifyExtractValue.h + include/assistDS/StructReturnToPointer.h + include/assistDS/DSNodeEquivs.h + include/assistDS/FuncSpec.h + include/assistDS/SimplifyGEP.h + include/assistDS/TypeChecks.h + include/assistDS/DataStructureCallGraph.h + include/assistDS/GEPExprArgs.h + include/assistDS/LoadArgs.h + include/assistDS/SimplifyInsertValue.h + include/assistDS/TypeChecksOpt.h + include/assistDS/Devirt.h + include/assistDS/IndCloner.h + include/assistDS/MergeGEP.h + include/assistDS/SimplifyLoad.h + lib/AssistDS/ArgCast.cpp + lib/AssistDS/Devirt.cpp + lib/AssistDS/GEPExprArgs.cpp + lib/AssistDS/LoadArgs.cpp + lib/AssistDS/SimplifyExtractValue.cpp + lib/AssistDS/StructReturnToPointer.cpp + lib/AssistDS/ArgSimplify.cpp + lib/AssistDS/DynCount.cpp + lib/AssistDS/IndCloner.cpp + lib/AssistDS/SimplifyGEP.cpp + lib/AssistDS/TypeChecks.cpp + lib/AssistDS/DSNodeEquivs.cpp + lib/AssistDS/FuncSimplify.cpp + lib/AssistDS/Int2PtrCmp.cpp + lib/AssistDS/MergeGEP.cpp + lib/AssistDS/SimplifyInsertValue.cpp + lib/AssistDS/TypeChecksOpt.cpp + lib/AssistDS/DataStructureCallGraph.cpp + lib/AssistDS/FuncSpec.cpp + lib/AssistDS/SVADevirt.cpp + lib/AssistDS/SimplifyLoad.cpp +) + +add_library(dsa STATIC + include/dsa/AddressTakenAnalysis.h + include/dsa/DSCallGraph.h + include/dsa/DSNode.h + include/dsa/EntryPointAnalysis.h + include/dsa/keyiterator.h + include/dsa/svset.h + include/dsa/AllocatorIdentification.h + include/dsa/DSGraph.h + include/dsa/DSSupport.h + include/dsa/stl_util.h + include/dsa/CallTargets.h + include/dsa/DSGraphTraits.h + include/dsa/DataStructure.h + include/dsa/TypeSafety.h + include/dsa/super_set.h + lib/DSA/AddressTakenAnalysis.cpp + lib/DSA/CallTargets.cpp + lib/DSA/DSTest.cpp + lib/DSA/EquivClassGraphs.cpp + lib/DSA/StdLibPass.cpp + lib/DSA/AllocatorIdentification.cpp + lib/DSA/CompleteBottomUp.cpp + lib/DSA/DataStructure.cpp + lib/DSA/GraphChecker.cpp + lib/DSA/Printer.cpp + lib/DSA/TopDownClosure.cpp + lib/DSA/Basic.cpp + lib/DSA/DSCallGraph.cpp + lib/DSA/DataStructureStats.cpp + lib/DSA/TypeSafety.cpp + lib/DSA/BottomUpClosure.cpp + lib/DSA/DSGraph.cpp + lib/DSA/EntryPointAnalysis.cpp + lib/DSA/Local.cpp + lib/DSA/SanityCheck.cpp +) + +add_library(smackTranslator STATIC + include/smack/smack.h + include/smack/BoogieAst.h + include/smack/BplFilePrinter.h + include/smack/BplPrinter.h + include/smack/DSAAliasAnalysis.h + include/smack/SmackInstGenerator.h + include/smack/SmackModuleGenerator.h + include/smack/SmackOptions.h + include/smack/SmackRep.h + include/smack/SmackRep2dMem.h + include/smack/SmackRepFlatMem.h + lib/smack/BoogieAst.cpp + lib/smack/BplFilePrinter.cpp + lib/smack/BplPrinter.cpp + lib/smack/DSAAliasAnalysis.cpp + lib/smack/SmackInstGenerator.cpp + lib/smack/SmackModuleGenerator.cpp + lib/smack/SmackOptions.cpp + lib/smack/SmackRep.cpp + lib/smack/SmackRep2dMem.cpp + lib/smack/SmackRepFlatMem.cpp +) + +add_executable(smack + tools/smack/smack.cpp +) + +set_target_properties(smack smackTranslator assistDS dsa + PROPERTIES COMPILE_FLAGS "${LLVM_CXXFLAGS}") + +target_link_libraries(smackTranslator ${LLVM_LIBS} ${LLVM_LDFLAGS}) +target_link_libraries(smack smackTranslator assistDS dsa) + +INSTALL(TARGETS smack smackTranslator assistDS dsa + RUNTIME DESTINATION bin + LIBRARY DESTINATION lib + ARCHIVE DESTINATION lib +) + +INSTALL(FILES ${CMAKE_CURRENT_SOURCE_DIR}/bin/boogie + ${CMAKE_CURRENT_SOURCE_DIR}/bin/corral + ${CMAKE_CURRENT_SOURCE_DIR}/bin/llvm2bpl.py + ${CMAKE_CURRENT_SOURCE_DIR}/bin/smackgen.py + ${CMAKE_CURRENT_SOURCE_DIR}/bin/smack-verify.py + PERMISSIONS OWNER_EXECUTE OWNER_WRITE OWNER_READ + GROUP_EXECUTE GROUP_READ WORLD_EXECUTE WORLD_READ + DESTINATION bin +) + \ No newline at end of file diff --git a/Makefile b/Makefile index ae808357b..348e0692b 100644 --- a/Makefile +++ b/Makefile @@ -8,7 +8,7 @@ # Indicates our relative path to the top of the project's root directory. # LEVEL = . -DIRS = lib +DIRS = lib tools EXTRA_DIST = include # diff --git a/Makefile.common.in b/Makefile.common.in index b10598383..a2ee6cac1 100644 --- a/Makefile.common.in +++ b/Makefile.common.in @@ -1,6 +1,6 @@ # Set the name of the project here PROJECT_NAME := smack -PROJ_VERSION := 1.3.1 +PROJ_VERSION := 1.4.0 # Set this variable to the top of the LLVM source tree. LLVM_SRC_ROOT = @LLVM_SRC@ diff --git a/Makefile.llvm.config.in b/Makefile.llvm.config.in index 987ceb557..39fce4d0b 100644 --- a/Makefile.llvm.config.in +++ b/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.1 +PROJ_VERSION := 1.4.0 endif PROJ_bindir := $(PROJ_prefix)/bin diff --git a/autoconf/config.guess b/autoconf/config.guess index f7dd69ecc..40e2c708f 100755 --- a/autoconf/config.guess +++ b/autoconf/config.guess @@ -961,6 +961,9 @@ EOF ppc64:Linux:*:*) echo powerpc64-unknown-linux-gnu exit ;; + ppc64le:Linux:*:*) + echo powerpc64le-unknown-linux-gnu + exit ;; ppc:Linux:*:*) echo powerpc-unknown-linux-gnu exit ;; diff --git a/autoconf/config.sub b/autoconf/config.sub index 994249153..9d22c1e52 100755 --- a/autoconf/config.sub +++ b/autoconf/config.sub @@ -251,7 +251,8 @@ case $basic_machine in | alpha64 | alpha64ev[4-8] | alpha64ev56 | alpha64ev6[78] | alpha64pca5[67] \ | am33_2.0 \ | arc | arm | arm[bl]e | arme[lb] | armv[2345] | armv[345][lb] | avr | avr32 \ - | be32 | be64 \ + | be32 | be64 \ + | aarch64 \ | bfin \ | c4x | clipper \ | d10v | d30v | dlx | dsp16xx \ @@ -359,6 +360,7 @@ case $basic_machine in | alpha64-* | alpha64ev[4-8]-* | alpha64ev56-* | alpha64ev6[78]-* \ | alphapca5[67]-* | alpha64pca5[67]-* | arc-* \ | arm-* | armbe-* | armle-* | armeb-* | armv*-* \ + | aarch64-* \ | avr-* | avr32-* \ | be32-* | be64-* \ | bfin-* | bs2000-* \ diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 29d8a2568..bff9d00d0 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -1,7 +1,7 @@ dnl ************************************************************************** dnl * Initialize dnl ************************************************************************** -AC_INIT([SMACK],[1.0],[zvonimir@cs.utah.edu]) +AC_INIT([[SMACK]],[[1.4.0]],[smack-dev@googlegroups.com],[smack],[http://github.com/smackers/smack]) dnl Identify where LLVM source tree is LLVM_SRC_ROOT="../.." @@ -304,13 +304,14 @@ AC_CACHE_CHECK([target architecture],[llvm_cv_target_arch], sparc*-*) llvm_cv_target_arch="Sparc" ;; powerpc*-*) llvm_cv_target_arch="PowerPC" ;; arm*-*) llvm_cv_target_arch="ARM" ;; + aarch64*-*) llvm_cv_target_arch="AArch64" ;; mips-* | mips64-*) llvm_cv_target_arch="Mips" ;; mipsel-* | mips64el-*) llvm_cv_target_arch="Mips" ;; xcore-*) llvm_cv_target_arch="XCore" ;; msp430-*) llvm_cv_target_arch="MSP430" ;; hexagon-*) llvm_cv_target_arch="Hexagon" ;; - mblaze-*) llvm_cv_target_arch="MBlaze" ;; nvptx-*) llvm_cv_target_arch="NVPTX" ;; + s390x-*) llvm_cv_target_arch="SystemZ" ;; *) llvm_cv_target_arch="Unknown" ;; esac]) @@ -380,6 +381,18 @@ case "$enableval" in *) AC_MSG_ERROR([Invalid setting for --enable-libcpp. Use "yes" or "no"]) ;; esac +dnl --enable-cxx11 : check whether or not to use -std=c++11 on the command line +AC_ARG_ENABLE(cxx11, + AS_HELP_STRING([--enable-cxx11], + [Use c++11 if available (default is NO)]),, + enableval=default) +case "$enableval" in + yes) AC_SUBST(ENABLE_CXX11,[1]) ;; + no) AC_SUBST(ENABLE_CXX11,[0]) ;; + default) AC_SUBST(ENABLE_CXX11,[0]);; + *) AC_MSG_ERROR([Invalid setting for --enable-cxx11. Use "yes" or "no"]) ;; +esac + dnl --enable-optimized : check whether they want to do an optimized build: AC_ARG_ENABLE(optimized, AS_HELP_STRING( --enable-optimized,[Compile with optimizations enabled (default is NO)]),,enableval=$optimize) @@ -407,6 +420,16 @@ else AC_SUBST(DISABLE_ASSERTIONS,[[DISABLE_ASSERTIONS=1]]) fi +dnl --enable-werror : check whether we want Werror on by default +AC_ARG_ENABLE(werror,AS_HELP_STRING( + --enable-werror,[Compile with -Werror enabled (default is NO)]),, enableval="no") +case "$enableval" in + yes) AC_SUBST(ENABLE_WERROR,[1]) ;; + no) AC_SUBST(ENABLE_WERROR,[0]) ;; + default) AC_SUBST(ENABLE_WERROR,[0]);; + *) AC_MSG_ERROR([Invalid setting for --enable-werror. Use "yes" or "no"]) ;; +esac + dnl --enable-expensive-checks : check whether they want to turn on expensive debug checks: AC_ARG_ENABLE(expensive-checks,AS_HELP_STRING( --enable-expensive-checks,[Compile with expensive debug checks enabled (default is NO)]),, enableval="no") @@ -452,12 +475,13 @@ else PowerPC) AC_SUBST(TARGET_HAS_JIT,1) ;; x86_64) AC_SUBST(TARGET_HAS_JIT,1) ;; ARM) AC_SUBST(TARGET_HAS_JIT,1) ;; + AArch64) AC_SUBST(TARGET_HAS_JIT,0) ;; Mips) AC_SUBST(TARGET_HAS_JIT,1) ;; XCore) AC_SUBST(TARGET_HAS_JIT,0) ;; MSP430) AC_SUBST(TARGET_HAS_JIT,0) ;; Hexagon) AC_SUBST(TARGET_HAS_JIT,0) ;; - MBlaze) AC_SUBST(TARGET_HAS_JIT,0) ;; NVPTX) AC_SUBST(TARGET_HAS_JIT,0) ;; + SystemZ) AC_SUBST(TARGET_HAS_JIT,1) ;; *) AC_SUBST(TARGET_HAS_JIT,0) ;; esac fi @@ -511,6 +535,21 @@ case "$enableval" in *) AC_MSG_ERROR([Invalid setting for --enable-pthreads. Use "yes" or "no"]) ;; esac +dnl Allow disablement of zlib +AC_ARG_ENABLE(zlib, + AS_HELP_STRING([--enable-zlib], + [Use zlib for compression/decompression if + available (default is YES)]),, + enableval=default) +case "$enableval" in + yes) AC_SUBST(LLVM_ENABLE_ZLIB,[1]) ;; + no) AC_SUBST(LLVM_ENABLE_ZLIB,[0]) ;; + default) AC_SUBST(LLVM_ENABLE_ZLIB,[1]) ;; + *) AC_MSG_ERROR([Invalid setting for --enable-zlib. Use "yes" or "no"]) ;; +esac +AC_DEFINE_UNQUOTED([LLVM_ENABLE_ZLIB],$LLVM_ENABLE_ZLIB, + [Define if zlib is enabled]) + dnl Allow building without position independent code AC_ARG_ENABLE(pic, AS_HELP_STRING([--enable-pic], @@ -567,42 +606,46 @@ dnl Allow specific targets to be specified for building (or not) TARGETS_TO_BUILD="" AC_ARG_ENABLE([targets],AS_HELP_STRING([--enable-targets], [Build specific host targets: all or target1,target2,... Valid targets are: - host, x86, x86_64, sparc, powerpc, arm, mips, spu, hexagon, - xcore, msp430, nvptx, cbe, and cpp (default=all)]),, + host, x86, x86_64, sparc, powerpc, arm, aarch64, mips, hexagon, + xcore, msp430, nvptx, systemz, r600, and cpp (default=all)]),, enableval=all) if test "$enableval" = host-only ; then enableval=host fi case "$enableval" in - all) TARGETS_TO_BUILD="X86 Sparc PowerPC ARM Mips CellSPU XCore MSP430 Hexagon CppBackend MBlaze NVPTX" ;; + all) TARGETS_TO_BUILD="X86 Sparc PowerPC AArch64 ARM Mips XCore MSP430 CppBackend NVPTX Hexagon SystemZ R600" ;; *)for a_target in `echo $enableval|sed -e 's/,/ /g' ` ; do case "$a_target" in x86) TARGETS_TO_BUILD="X86 $TARGETS_TO_BUILD" ;; x86_64) TARGETS_TO_BUILD="X86 $TARGETS_TO_BUILD" ;; sparc) TARGETS_TO_BUILD="Sparc $TARGETS_TO_BUILD" ;; powerpc) TARGETS_TO_BUILD="PowerPC $TARGETS_TO_BUILD" ;; + aarch64) TARGETS_TO_BUILD="AArch64 $TARGETS_TO_BUILD" ;; arm) TARGETS_TO_BUILD="ARM $TARGETS_TO_BUILD" ;; mips) TARGETS_TO_BUILD="Mips $TARGETS_TO_BUILD" ;; - spu) TARGETS_TO_BUILD="CellSPU $TARGETS_TO_BUILD" ;; + mipsel) TARGETS_TO_BUILD="Mips $TARGETS_TO_BUILD" ;; + mips64) TARGETS_TO_BUILD="Mips $TARGETS_TO_BUILD" ;; + mips64el) TARGETS_TO_BUILD="Mips $TARGETS_TO_BUILD" ;; xcore) TARGETS_TO_BUILD="XCore $TARGETS_TO_BUILD" ;; msp430) TARGETS_TO_BUILD="MSP430 $TARGETS_TO_BUILD" ;; - hexagon) TARGETS_TO_BUILD="Hexagon $TARGETS_TO_BUILD" ;; cpp) TARGETS_TO_BUILD="CppBackend $TARGETS_TO_BUILD" ;; - mblaze) TARGETS_TO_BUILD="MBlaze $TARGETS_TO_BUILD" ;; + hexagon) TARGETS_TO_BUILD="Hexagon $TARGETS_TO_BUILD" ;; nvptx) TARGETS_TO_BUILD="NVPTX $TARGETS_TO_BUILD" ;; + systemz) TARGETS_TO_BUILD="SystemZ $TARGETS_TO_BUILD" ;; + r600) TARGETS_TO_BUILD="R600 $TARGETS_TO_BUILD" ;; host) case "$llvm_cv_target_arch" in x86) TARGETS_TO_BUILD="X86 $TARGETS_TO_BUILD" ;; x86_64) TARGETS_TO_BUILD="X86 $TARGETS_TO_BUILD" ;; Sparc) TARGETS_TO_BUILD="Sparc $TARGETS_TO_BUILD" ;; PowerPC) TARGETS_TO_BUILD="PowerPC $TARGETS_TO_BUILD" ;; + AArch64) TARGETS_TO_BUILD="AArch64 $TARGETS_TO_BUILD" ;; ARM) TARGETS_TO_BUILD="ARM $TARGETS_TO_BUILD" ;; Mips) TARGETS_TO_BUILD="Mips $TARGETS_TO_BUILD" ;; - MBlaze) TARGETS_TO_BUILD="MBlaze $TARGETS_TO_BUILD" ;; - CellSPU|SPU) TARGETS_TO_BUILD="CellSPU $TARGETS_TO_BUILD" ;; XCore) TARGETS_TO_BUILD="XCore $TARGETS_TO_BUILD" ;; MSP430) TARGETS_TO_BUILD="MSP430 $TARGETS_TO_BUILD" ;; Hexagon) TARGETS_TO_BUILD="Hexagon $TARGETS_TO_BUILD" ;; NVPTX) TARGETS_TO_BUILD="NVPTX $TARGETS_TO_BUILD" ;; + SystemZ) TARGETS_TO_BUILD="SystemZ $TARGETS_TO_BUILD" ;; *) AC_MSG_ERROR([Can not set target to build]) ;; esac ;; *) AC_MSG_ERROR([Unrecognized target $a_target]) ;; @@ -792,6 +835,17 @@ AC_ARG_WITH(bug-report-url, AC_DEFINE_UNQUOTED(BUG_REPORT_URL,"$withval", [Bug report URL.]) +dnl --enable-terminfo: check whether the user wants to control use of terminfo: +AC_ARG_ENABLE(terminfo,AS_HELP_STRING( + [--enable-terminfo], + [Query the terminfo database if available (default is YES)]), + [case "$enableval" in + yes) llvm_cv_enable_terminfo="yes" ;; + no) llvm_cv_enable_terminfo="no" ;; + *) AC_MSG_ERROR([Invalid setting for --enable-terminfo. Use "yes" or "no"]) ;; + esac], + llvm_cv_enable_terminfo="yes") + dnl --enable-libffi : check whether the user wants to turn off libffi: AC_ARG_ENABLE(libffi,AS_HELP_STRING( --enable-libffi,[Check for the presence of libffi (default is NO)]), @@ -801,29 +855,6 @@ AC_ARG_ENABLE(libffi,AS_HELP_STRING( *) AC_MSG_ERROR([Invalid setting for --enable-libffi. Use "yes" or "no"]) ;; esac], llvm_cv_enable_libffi=no) - -dnl ************************************************************************** -dnl * Set the location of various third-party software packages -dnl ************************************************************************** - -dnl Specify the location of the poolalloc project -AC_ARG_WITH(poolallocsrc, - AS_HELP_STRING([--with-poolallocsrc], - [Specify location of Pool Allocation source code]), - AC_SUBST(poolallocsrc,"$withval"), - AC_SUBST(poolallocsrc,"$LLVM_SRC_ROOT/projects/poolalloc" - )) - -AC_ARG_WITH(poolallocobj, - AS_HELP_STRING([--with-poolallocobj], - [Specify location of Pool Allocation object code]), - AC_SUBST(poolallocobj,"$withval"), - AC_SUBST(poolallocobj,"$LLVM_OBJ_ROOT/projects/poolalloc" - )) - -dnl Ensure that all pathnames are absolute pathnames -poolallocsrc=`cd $poolallocsrc && pwd` -poolallocobj=`cd $poolallocobj && pwd` dnl===-----------------------------------------------------------------------=== dnl=== @@ -980,7 +1011,7 @@ AC_LINK_GET_VERSION dnl Determine whether the linker supports the -R option. AC_LINK_USE_R -dnl Determine whether the linker supports the -export-dynamic option. +dnl Determine whether the compiler supports the -rdynamic option. AC_LINK_EXPORT_DYNAMIC dnl Determine whether the linker supports the --version-script option. @@ -1056,6 +1087,7 @@ AC_CHECK_LIB(m,sin) if test "$llvm_cv_os_type" = "MingW" ; then AC_CHECK_LIB(imagehlp, main) AC_CHECK_LIB(psapi, main) + AC_CHECK_LIB(shell32, main) fi dnl dlopen() is required for plugin support. @@ -1063,6 +1095,19 @@ AC_SEARCH_LIBS(dlopen,dl,AC_DEFINE([HAVE_DLOPEN],[1], [Define if dlopen() is available on this platform.]), AC_MSG_WARN([dlopen() not found - disabling plugin support])) +dnl Search for the clock_gettime() function. Note that we rely on the POSIX +dnl macros to detect whether clock_gettime is available, this just finds the +dnl right libraries to link with. +AC_SEARCH_LIBS(clock_gettime,rt) + +dnl The curses library is optional; used for querying terminal info +if test "$llvm_cv_enable_terminfo" = "yes" ; then + dnl We need the has_color functionality in curses for it to be useful. + AC_SEARCH_LIBS(setupterm,tinfo curses ncurses ncursesw, + AC_DEFINE([HAVE_TERMINFO],[1], + [Define if the setupterm() function is supported this platform.])) +fi + dnl libffi is optional; used to call external functions from the interpreter if test "$llvm_cv_enable_libffi" = "yes" ; then AC_SEARCH_LIBS(ffi_call,ffi,AC_DEFINE([HAVE_FFI_CALL],[1], @@ -1089,6 +1134,11 @@ if test "$ENABLE_THREADS" -eq 1 && test "$ENABLE_PTHREADS" -eq 1 ; then [Have pthread_getspecific])) fi +dnl zlib is optional; used for compression/uncompression +if test "$LLVM_ENABLE_ZLIB" -eq 1 ; then + AC_CHECK_LIB(z, compress2) +fi + dnl Allow extra x86-disassembler library AC_ARG_WITH(udis86, AS_HELP_STRING([--with-udis86=], @@ -1174,6 +1224,13 @@ if test "$ENABLE_THREADS" -eq 1 && test "$ENABLE_PTHREADS" -eq 1 ; then else AC_SUBST(HAVE_PTHREAD, 0) fi +if test "$LLVM_ENABLE_ZLIB" -eq 1 ; then + AC_CHECK_HEADERS(zlib.h, + AC_SUBST(HAVE_LIBZ, 1), + AC_SUBST(HAVE_LIBZ, 0)) +else + AC_SUBST(HAVE_LIBZ, 0) +fi dnl Try to find ffi.h. if test "$llvm_cv_enable_libffi" = "yes" ; then @@ -1356,7 +1413,6 @@ if test "${prefix}" = "NONE" ; then fi eval LLVM_PREFIX="${prefix}"; eval LLVM_BINDIR="${prefix}/bin"; -eval LLVM_LIBDIR="${prefix}/lib"; eval LLVM_DATADIR="${prefix}/share/llvm"; eval LLVM_DOCSDIR="${prefix}/share/doc/llvm"; eval LLVM_ETCDIR="${prefix}/etc/llvm"; @@ -1366,7 +1422,6 @@ eval LLVM_MANDIR="${prefix}/man"; LLVM_CONFIGTIME=`date` AC_SUBST(LLVM_PREFIX) AC_SUBST(LLVM_BINDIR) -AC_SUBST(LLVM_LIBDIR) AC_SUBST(LLVM_DATADIR) AC_SUBST(LLVM_DOCSDIR) AC_SUBST(LLVM_ETCDIR) @@ -1381,8 +1436,6 @@ AC_DEFINE_UNQUOTED(LLVM_PREFIX,"$LLVM_PREFIX", [Installation prefix directory]) AC_DEFINE_UNQUOTED(LLVM_BINDIR, "$LLVM_BINDIR", [Installation directory for binary executables]) -AC_DEFINE_UNQUOTED(LLVM_LIBDIR, "$LLVM_LIBDIR", - [Installation directory for libraries]) AC_DEFINE_UNQUOTED(LLVM_DATADIR, "$LLVM_DATADIR", [Installation directory for data files]) AC_DEFINE_UNQUOTED(LLVM_DOCSDIR, "$LLVM_DOCSDIR", @@ -1440,7 +1493,7 @@ for a_binding in $BINDINGS_TO_BUILD ; do AC_SUBST(OCAML_LIBDIR,$ocaml_stdlib) else # ocaml stdlib is outside our prefix; use libdir/ocaml - AC_SUBST(OCAML_LIBDIR,$LLVM_LIBDIR/ocaml) + AC_SUBST(OCAML_LIBDIR,${prefix}/lib/ocaml) fi fi ;; @@ -1463,7 +1516,7 @@ AC_SUBST(RPATH) dnl Determine linker rdynamic flag if test "$llvm_cv_link_use_export_dynamic" = "yes" ; then - RDYNAMIC="-Wl,-export-dynamic" + RDYNAMIC="-rdynamic" else RDYNAMIC="" fi @@ -1487,7 +1540,11 @@ dnl Configure project makefiles dnl List every Makefile that exists within your source tree AC_CONFIG_MAKEFILE(Makefile) AC_CONFIG_MAKEFILE(lib/Makefile) +AC_CONFIG_MAKEFILE(lib/AssistDS/Makefile) +AC_CONFIG_MAKEFILE(lib/DSA/Makefile) AC_CONFIG_MAKEFILE(lib/smack/Makefile) +AC_CONFIG_MAKEFILE(tools/Makefile) +AC_CONFIG_MAKEFILE(tools/smack/Makefile) dnl This must be last AC_OUTPUT diff --git a/autoconf/m4/libtool.m4 b/autoconf/m4/libtool.m4 index 36ac3d15d..b8bd4b803 100644 --- a/autoconf/m4/libtool.m4 +++ b/autoconf/m4/libtool.m4 @@ -530,7 +530,7 @@ x86_64-*linux*|ppc*-*linux*|powerpc*-*linux*|s390*-*linux*|sparc*-*linux*) x86_64-*linux*) LD="${LD-ld} -m elf_i386" ;; - ppc64-*linux*|powerpc64-*linux*) + ppc64-*linux*|powerpc64-*linux*|ppc64le-$linux*|powerpc64le-*linux*) LD="${LD-ld} -m elf32ppclinux" ;; s390x-*linux*) diff --git a/autoconf/m4/link_options.m4 b/autoconf/m4/link_options.m4 index 57da4a0d9..b58d61745 100644 --- a/autoconf/m4/link_options.m4 +++ b/autoconf/m4/link_options.m4 @@ -40,23 +40,24 @@ if test "$llvm_cv_link_use_r" = yes ; then ]) # -# Determine if the system can handle the -R option being passed to the linker. +# Determine if the system can handle the -rdynamic option being passed +# to the compiler. # # This macro is specific to LLVM. # AC_DEFUN([AC_LINK_EXPORT_DYNAMIC], -[AC_CACHE_CHECK([for compiler -Wl,-export-dynamic option], +[AC_CACHE_CHECK([for compiler -rdynamic option], [llvm_cv_link_use_export_dynamic], [ AC_LANG_PUSH([C]) oldcflags="$CFLAGS" - CFLAGS="$CFLAGS -Wl,-export-dynamic" + CFLAGS="$CFLAGS -rdynamic" AC_LINK_IFELSE([AC_LANG_PROGRAM([[]],[[]])], [llvm_cv_link_use_export_dynamic=yes],[llvm_cv_link_use_export_dynamic=no]) CFLAGS="$oldcflags" AC_LANG_POP([C]) ]) if test "$llvm_cv_link_use_export_dynamic" = yes ; then - AC_DEFINE([HAVE_LINK_EXPORT_DYNAMIC],[1],[Define if you can use -Wl,-export-dynamic.]) + AC_DEFINE([HAVE_LINK_EXPORT_DYNAMIC],[1],[Define if you can use -rdynamic.]) fi ]) diff --git a/autoconf/m4/ltdl.m4 b/autoconf/m4/ltdl.m4 index 407a16e2d..0a36dbe7c 100644 --- a/autoconf/m4/ltdl.m4 +++ b/autoconf/m4/ltdl.m4 @@ -68,7 +68,6 @@ AC_REQUIRE([AC_HEADER_DIRENT]) AC_REQUIRE([_LT_AC_CHECK_DLFCN]) AC_REQUIRE([AC_LTDL_ENABLE_INSTALL]) AC_REQUIRE([AC_LTDL_SHLIBEXT]) -AC_REQUIRE([AC_LTDL_SHLIBPATH]) AC_REQUIRE([AC_LTDL_SYSSEARCHPATH]) AC_REQUIRE([AC_LTDL_OBJDIR]) AC_REQUIRE([AC_LTDL_DLPREOPEN]) @@ -206,20 +205,6 @@ if test -n "$libltdl_cv_shlibext"; then fi ])# AC_LTDL_SHLIBEXT - -# AC_LTDL_SHLIBPATH -# ----------------- -AC_DEFUN([AC_LTDL_SHLIBPATH], -[AC_REQUIRE([AC_LIBTOOL_SYS_DYNAMIC_LINKER]) -AC_CACHE_CHECK([which variable specifies run-time library path], - [libltdl_cv_shlibpath_var], [libltdl_cv_shlibpath_var="$shlibpath_var"]) -if test -n "$libltdl_cv_shlibpath_var"; then - AC_DEFINE_UNQUOTED([LTDL_SHLIBPATH_VAR], ["$libltdl_cv_shlibpath_var"], - [Define to the name of the environment variable that determines the dynamic library search path.]) -fi -])# AC_LTDL_SHLIBPATH - - # AC_LTDL_SYSSEARCHPATH # --------------------- AC_DEFUN([AC_LTDL_SYSSEARCHPATH], diff --git a/bin/build-cygwin-cmake.sh b/bin/build-cygwin-cmake.sh new file mode 100755 index 000000000..9e997ce9f --- /dev/null +++ b/bin/build-cygwin-cmake.sh @@ -0,0 +1,110 @@ +#!/bin/bash + +################################################################################ +# +# Builds and installs SMACK in BASE_DIR (see shell var below in settings). +# +# Requirements: +# - git +# - python +# - gcc +# - g++ +# - make +# - autoconf +# +################################################################################ + +# Exit on error +set -e + +################################################################################ + +# Settings + +# Change this to the desired path (default uses working-dir/smack-project) +BASE_DIR=`pwd`/smack-project + +# Set these flags to control various installation options +INSTALL_LLVM=1 +INSTALL_SMACK=1 + +# Other dirs +LLVM_DIR="${BASE_DIR}/llvm" +SMACK_DIR="${BASE_DIR}/smack" + +################################################################################ + +# Set up base directory for everything +mkdir -p ${BASE_DIR} +cd ${BASE_DIR} + +################################################################################ + +# LLVM + +if [ ${INSTALL_LLVM} -eq 1 ]; then + +mkdir -p ${LLVM_DIR}/src +mkdir -p ${LLVM_DIR}/build +mkdir -p ${LLVM_DIR}/install + +# Get llvm and extract +wget http://llvm.org/releases/3.4/llvm-3.4.src.tar.gz +wget http://llvm.org/releases/3.4/clang-3.4.src.tar.gz +wget http://llvm.org/releases/3.4/compiler-rt-3.4.src.tar.gz + +tar -C ${LLVM_DIR}/src -xzvf llvm-3.4.src.tar.gz --strip 1 +mkdir -p ${LLVM_DIR}/src/tools/clang +tar -C ${LLVM_DIR}/src/tools/clang -xzvf clang-3.4.src.tar.gz --strip 1 +mkdir -p ${LLVM_DIR}/src/projects/compiler-rt +tar -C ${LLVM_DIR}/src/projects/compiler-rt -xzvf compiler-rt-3.4.src.tar.gz --strip 1 + +# Configure llvm and build +cd ${LLVM_DIR}/build/ +cmake -DCMAKE_INSTALL_PREFIX=${LLVM_DIR}/install -DCMAKE_BUILD_TYPE=Release ../src +make +make install + +cd ${BASE_DIR} + +fi + +################################################################################ + +# SMACK + +if [ ${INSTALL_SMACK} -eq 1 ]; then + +mkdir -p ${SMACK_DIR}/src +mkdir -p ${SMACK_DIR}/build +mkdir -p ${SMACK_DIR}/install + +# Get SMACK +git clone git://github.com/smackers/smack.git ${SMACK_DIR}/src/ + +# Configure SMACK and build +cd ${SMACK_DIR}/build/ +cmake -DLLVM_CONFIG=${LLVM_DIR}/install/bin -DCMAKE_INSTALL_PREFIX=${SMACK_DIR}/install -DCMAKE_BUILD_TYPE=Release ../src +make +make install + +cd ${BASE_DIR} + +# Set required paths and environment variables +export BOOGIE=/cygdrive/c/Users/zvonimir/Boogie/boogie +export CORRAL=/cygdrive/c/projects/corral/corral +export PATH=${LLVM_DIR}/install/bin:$PATH +export PATH=${SMACK_DIR}/install/bin:$PATH + +# Run SMACK regressions +cd ${SMACK_DIR}/src/test +make +./regtest.py +./regtest-corral.py + +cd ${BASE_DIR} + +fi + +################################################################################ + diff --git a/bin/build-cygwin.sh b/bin/build-cygwin.sh old mode 100644 new mode 100755 index 64c767a37..467fcfc7d --- a/bin/build-cygwin.sh +++ b/bin/build-cygwin.sh @@ -34,19 +34,8 @@ SMACK_DIR="${BASE_DIR}/smack" ################################################################################ -# Set up directories - -# Base directory for everything +# Set up base directory for everything mkdir -p ${BASE_DIR} - -# Other dirs -mkdir -p ${LLVM_DIR}/src -mkdir -p ${LLVM_DIR}/build -mkdir -p ${LLVM_DIR}/install -mkdir -p ${SMACK_DIR}/src -mkdir -p ${SMACK_DIR}/build -mkdir -p ${SMACK_DIR}/install - cd ${BASE_DIR} ################################################################################ @@ -55,20 +44,24 @@ cd ${BASE_DIR} if [ ${INSTALL_LLVM} -eq 1 ]; then +mkdir -p ${LLVM_DIR}/src +mkdir -p ${LLVM_DIR}/build +mkdir -p ${LLVM_DIR}/install + # Get llvm and extract -wget http://llvm.org/releases/3.3/llvm-3.3.src.tar.gz -wget http://llvm.org/releases/3.3/cfe-3.3.src.tar.gz -wget http://llvm.org/releases/3.3/compiler-rt-3.3.src.tar.gz +wget http://llvm.org/releases/3.4/llvm-3.4.src.tar.gz +wget http://llvm.org/releases/3.4/clang-3.4.src.tar.gz +wget http://llvm.org/releases/3.4/compiler-rt-3.4.src.tar.gz -tar -C ${LLVM_DIR}/src -xzvf llvm-3.3.src.tar.gz --strip 1 +tar -C ${LLVM_DIR}/src -xzvf llvm-3.4.src.tar.gz --strip 1 mkdir -p ${LLVM_DIR}/src/tools/clang -tar -C ${LLVM_DIR}/src/tools/clang -xzvf cfe-3.3.src.tar.gz --strip 1 +tar -C ${LLVM_DIR}/src/tools/clang -xzvf clang-3.4.src.tar.gz --strip 1 mkdir -p ${LLVM_DIR}/src/projects/compiler-rt -tar -C ${LLVM_DIR}/src/projects/compiler-rt -xzvf compiler-rt-3.3.src.tar.gz --strip 1 +tar -C ${LLVM_DIR}/src/projects/compiler-rt -xzvf compiler-rt-3.4.src.tar.gz --strip 1 # Configure llvm and build cd ${LLVM_DIR}/build/ -${LLVM_DIR}/src/configure --prefix=${LLVM_DIR}/install --enable-shared --enable-optimized +${LLVM_DIR}/src/configure --prefix=${LLVM_DIR}/install --enable-optimized make make install @@ -82,22 +75,26 @@ fi if [ ${INSTALL_SMACK} -eq 1 ]; then +mkdir -p ${SMACK_DIR}/src +mkdir -p ${SMACK_DIR}/build +mkdir -p ${SMACK_DIR}/install + # Get SMACK git clone git://github.com/smackers/smack.git ${SMACK_DIR}/src/ # Configure SMACK and build cd ${SMACK_DIR}/build/ -${SMACK_DIR}/src/configure --with-llvmsrc=${LLVM_DIR}/src --with-llvmobj=${LLVM_DIR}/build --prefix=${SMACK_DIR}/install --enable-shared --enable-optimized +${SMACK_DIR}/src/configure --with-llvmsrc=${LLVM_DIR}/src --with-llvmobj=${LLVM_DIR}/build --prefix=${SMACK_DIR}/install --enable-optimized make make install cd ${BASE_DIR} # Set required paths and environment variables -export BOOGIE=boogie -export CORRAL=corral -export PATH=$PATH:${LLVM_DIR}/install/bin -export PATH=$PATH:${SMACK_DIR}/install/bin +export BOOGIE=/cygdrive/c/Users/zvonimir/Boogie/boogie +export CORRAL=/cygdrive/c/projects/corral/corral +export PATH=${LLVM_DIR}/install/bin:$PATH +export PATH=${SMACK_DIR}/install/bin:$PATH # Run SMACK regressions cd ${SMACK_DIR}/src/test diff --git a/bin/build-linux-cmake.sh b/bin/build-linux-cmake.sh new file mode 100755 index 000000000..11339884e --- /dev/null +++ b/bin/build-linux-cmake.sh @@ -0,0 +1,270 @@ +#!/bin/bash + +################################################################################ +# +# Builds and installs SMACK in BASE_DIR (see shell var below in settings). +# +# Requirements (see "Install required packages" below): +# - git +# - mercurial +# - python +# - gcc +# - g++ +# - make +# - autoconf +# - mono +# +################################################################################ + +# Exit on error +set -e + +################################################################################ + +# Settings + +# Change this to the desired path (default uses working-dir/smack-project) +BASE_DIR=`pwd`/smack-project + +# Set these flags to control various installation options +INSTALL_PACKAGES=1 +INSTALL_CMAKE=1 +INSTALL_MONO=1 +INSTALL_Z3=1 +INSTALL_BOOGIE=1 +INSTALL_CORRAL=1 +INSTALL_LLVM=1 +INSTALL_SMACK=1 + +# Other dirs +MONO_DIR="${BASE_DIR}/mono-3" +Z3_DIR="${BASE_DIR}/z3" +BOOGIE_DIR="${BASE_DIR}/boogie" +CORRAL_DIR="${BASE_DIR}/corral" +LLVM_DIR="${BASE_DIR}/llvm" +SMACK_DIR="${BASE_DIR}/smack" + +################################################################################ + +# Install required packages + +if [ ${INSTALL_PACKAGES} -eq 1 ]; then + +sudo apt-get install -y g++ +sudo apt-get install -y git +sudo apt-get install -y mercurial +sudo apt-get install -y autoconf +sudo apt-get install -y wget + +fi + +################################################################################ + +# Set up base directory for everything +mkdir -p ${BASE_DIR} +cd ${BASE_DIR} + +################################################################################ + +# cmake + +if [ ${INSTALL_CMAKE} -eq 1 ]; then + +cd ${BASE_DIR} +wget http://www.cmake.org/files/v2.8/cmake-2.8.12.2-Linux-i386.sh +sudo sh cmake-2.8.12.2-Linux-i386.sh --prefix=/usr/local --exclude-subdir + +fi + +################################################################################ + +# mono + +if [ ${INSTALL_MONO} -eq 1 ]; then + +mkdir -p ${MONO_DIR} + +# Install mono +sudo apt-get install -y git build-essential autoconf automake bison flex libtool gettext gdb mono-gmcs +cd ${MONO_DIR} +git clone git://github.com/mono/mono.git +cd mono +git checkout mono-3.2.6 +./autogen.sh --prefix=/usr/local +make +sudo make install + +# Install libgdiplus +sudo apt-get install -y libglib2.0-dev libfontconfig1-dev libfreetype6-dev libxrender-dev +sudo apt-get install -y libtiff-dev libjpeg-dev libgif-dev libpng-dev +cd ${MONO_DIR} +git clone git://github.com/mono/libgdiplus.git +cd libgdiplus +./autogen.sh --prefix=/usr/local +make +sudo make install + +cd ${BASE_DIR} + +fi + +################################################################################ + +# Z3 + +if [ ${INSTALL_Z3} -eq 1 ]; then + +mkdir -p ${Z3_DIR}/src +mkdir -p ${Z3_DIR}/install + +# Get Z3 +cd ${Z3_DIR}/src/ +wget "http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?ProjectName=z3&changeSetId=89c1785b73225a1b363c0e485f854613121b70a7" +unzip -o SourceControlFileDownload* +rm -f SourceControlFileDownload* + +# Configure Z3 and build +cd ${Z3_DIR}/src/ +autoconf +./configure --prefix=${Z3_DIR}/install +python scripts/mk_make.py +cd build +make +sudo make install + +cd ${BASE_DIR} + +fi + +################################################################################ + +# Boogie + +if [ ${INSTALL_BOOGIE} -eq 1 ]; then + +mkdir -p ${BOOGIE_DIR} + +# Get Boogie +hg clone -r f59ad49fc3a4 https://hg.codeplex.com/boogie ${BOOGIE_DIR} + +# Build Boogie +cd ${BOOGIE_DIR}/Source +xbuild Boogie.sln +ln -s ${Z3_DIR}/install/bin/z3 ${BOOGIE_DIR}/Binaries/z3.exe + +cd ${BASE_DIR} + +fi + +################################################################################ + +# Corral + +if [ ${INSTALL_CORRAL} -eq 1 ]; then + +mkdir -p ${CORRAL_DIR} + +# Get Corral +git clone https://git01.codeplex.com/corral ${CORRAL_DIR} +cd ${CORRAL_DIR} +git checkout 9311d7273384 + +# Build Corral +cd ${CORRAL_DIR}/references + +cp ${BOOGIE_DIR}/Binaries/AbsInt.dll . +cp ${BOOGIE_DIR}/Binaries/Basetypes.dll . +cp ${BOOGIE_DIR}/Binaries/CodeContractsExtender.dll . +cp ${BOOGIE_DIR}/Binaries/Concurrency.dll . +cp ${BOOGIE_DIR}/Binaries/Core.dll . +cp ${BOOGIE_DIR}/Binaries/ExecutionEngine.dll . +cp ${BOOGIE_DIR}/Binaries/Graph.dll . +cp ${BOOGIE_DIR}/Binaries/Houdini.dll . +cp ${BOOGIE_DIR}/Binaries/Model.dll . +cp ${BOOGIE_DIR}/Binaries/ParserHelper.dll . +cp ${BOOGIE_DIR}/Binaries/Provers.SMTLib.dll . +cp ${BOOGIE_DIR}/Binaries/VCExpr.dll . +cp ${BOOGIE_DIR}/Binaries/VCGeneration.dll . +cp ${BOOGIE_DIR}/Binaries/Boogie.exe . +cp ${BOOGIE_DIR}/Binaries/BVD.exe . +cp ${BOOGIE_DIR}/Binaries/Doomed.dll . +cp ${BOOGIE_DIR}/Binaries/Predication.dll . + +cd ${CORRAL_DIR} +xbuild cba.sln +ln -s ${Z3_DIR}/install/bin/z3 ${CORRAL_DIR}/bin/Debug/z3.exe + +cd ${BASE_DIR} + +fi + +################################################################################ + +# LLVM + +if [ ${INSTALL_LLVM} -eq 1 ]; then + +mkdir -p ${LLVM_DIR}/src +mkdir -p ${LLVM_DIR}/build +mkdir -p ${LLVM_DIR}/install + +# Get llvm and extract +wget http://llvm.org/releases/3.4/llvm-3.4.src.tar.gz +wget http://llvm.org/releases/3.4/clang-3.4.src.tar.gz +wget http://llvm.org/releases/3.4/compiler-rt-3.4.src.tar.gz + +tar -C ${LLVM_DIR}/src -xzvf llvm-3.4.src.tar.gz --strip 1 +mkdir -p ${LLVM_DIR}/src/tools/clang +tar -C ${LLVM_DIR}/src/tools/clang -xzvf clang-3.4.src.tar.gz --strip 1 +mkdir -p ${LLVM_DIR}/src/projects/compiler-rt +tar -C ${LLVM_DIR}/src/projects/compiler-rt -xzvf compiler-rt-3.4.src.tar.gz --strip 1 + +# Configure llvm and build +cd ${LLVM_DIR}/build/ +cmake -DCMAKE_INSTALL_PREFIX=${LLVM_DIR}/install -DCMAKE_BUILD_TYPE=Release ../src +make +make install + +cd ${BASE_DIR} + +fi + +################################################################################ + +# SMACK + +if [ ${INSTALL_SMACK} -eq 1 ]; then + +mkdir -p ${SMACK_DIR}/src +mkdir -p ${SMACK_DIR}/build +mkdir -p ${SMACK_DIR}/install + +# Get SMACK +git clone git://github.com/smackers/smack.git ${SMACK_DIR}/src/ + +# Configure SMACK and build +cd ${SMACK_DIR}/build/ +cmake -DLLVM_CONFIG=${LLVM_DIR}/install/bin -DCMAKE_INSTALL_PREFIX=${SMACK_DIR}/install -DCMAKE_BUILD_TYPE=Release ../src +make +make install + +cd ${BASE_DIR} + +# Set required paths and environment variables +export BOOGIE="mono ${BOOGIE_DIR}/Binaries/Boogie.exe" +export CORRAL="mono ${CORRAL_DIR}/bin/Debug/corral.exe" +export PATH=${LLVM_DIR}/install/bin:$PATH +export PATH=${SMACK_DIR}/install/bin:$PATH + +# Run SMACK regressions +cd ${SMACK_DIR}/src/test +make +./regtest.py +./regtest-corral.py + +cd ${BASE_DIR} + +fi + +################################################################################ + diff --git a/bin/build-linux.sh b/bin/build-linux.sh old mode 100644 new mode 100755 index a71ad1bc3..f491e245c --- a/bin/build-linux.sh +++ b/bin/build-linux.sh @@ -28,6 +28,7 @@ BASE_DIR=`pwd`/smack-project # Set these flags to control various installation options INSTALL_PACKAGES=1 +INSTALL_MONO=1 INSTALL_Z3=1 INSTALL_BOOGIE=1 INSTALL_CORRAL=1 @@ -35,6 +36,7 @@ INSTALL_LLVM=1 INSTALL_SMACK=1 # Other dirs +MONO_DIR="${BASE_DIR}/mono-3" Z3_DIR="${BASE_DIR}/z3" BOOGIE_DIR="${BASE_DIR}/boogie" CORRAL_DIR="${BASE_DIR}/corral" @@ -47,43 +49,66 @@ SMACK_DIR="${BASE_DIR}/smack" if [ ${INSTALL_PACKAGES} -eq 1 ]; then -sudo apt-get install g++ --assume-yes -sudo apt-get install git --assume-yes -sudo apt-get install mercurial --assume-yes -sudo apt-get install autoconf --assume-yes -sudo apt-get install mono-devel --assume-yes +sudo apt-get install -y g++ +sudo apt-get install -y git +sudo apt-get install -y mercurial +sudo apt-get install -y autoconf +sudo apt-get install -y wget fi ################################################################################ -# Set up directories - -# Base directory for everything +# Set up base directory for everything mkdir -p ${BASE_DIR} +cd ${BASE_DIR} -# Other dirs -mkdir -p ${Z3_DIR}/src -mkdir -p ${Z3_DIR}/install -mkdir -p ${BOOGIE_DIR} -mkdir -p ${CORRAL_DIR} -mkdir -p ${LLVM_DIR}/src -mkdir -p ${LLVM_DIR}/build -mkdir -p ${LLVM_DIR}/install -mkdir -p ${SMACK_DIR}/src -mkdir -p ${SMACK_DIR}/build -mkdir -p ${SMACK_DIR}/install +################################################################################ + +# mono + +if [ ${INSTALL_MONO} -eq 1 ]; then + +mkdir -p ${MONO_DIR} + +# Install mono +sudo apt-get install -y git build-essential autoconf automake bison flex libtool gettext gdb mono-gmcs +cd ${MONO_DIR} +git clone git://github.com/mono/mono.git +cd mono +git checkout mono-3.2.6 +./autogen.sh --prefix=/usr/local +make +sudo make install + +# Install libgdiplus +sudo apt-get install -y libglib2.0-dev libfontconfig1-dev libfreetype6-dev libxrender-dev +sudo apt-get install -y libtiff-dev libjpeg-dev libgif-dev libpng-dev +cd ${MONO_DIR} +git clone git://github.com/mono/libgdiplus.git +cd libgdiplus +./autogen.sh --prefix=/usr/local +make +sudo make install cd ${BASE_DIR} +fi + ################################################################################ # Z3 if [ ${INSTALL_Z3} -eq 1 ]; then +mkdir -p ${Z3_DIR}/src +mkdir -p ${Z3_DIR}/install + # Get Z3 -git clone https://git01.codeplex.com/z3 ${Z3_DIR}/src/ +cd ${Z3_DIR}/src/ +wget "http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?ProjectName=z3&changeSetId=89c1785b73225a1b363c0e485f854613121b70a7" +unzip -o SourceControlFileDownload* +rm -f SourceControlFileDownload* # Configure Z3 and build cd ${Z3_DIR}/src/ @@ -104,8 +129,10 @@ fi if [ ${INSTALL_BOOGIE} -eq 1 ]; then +mkdir -p ${BOOGIE_DIR} + # Get Boogie -hg clone https://hg.codeplex.com/boogie ${BOOGIE_DIR} +hg clone -r f59ad49fc3a4 https://hg.codeplex.com/boogie ${BOOGIE_DIR} # Build Boogie cd ${BOOGIE_DIR}/Source @@ -122,8 +149,12 @@ fi if [ ${INSTALL_CORRAL} -eq 1 ]; then +mkdir -p ${CORRAL_DIR} + # Get Corral git clone https://git01.codeplex.com/corral ${CORRAL_DIR} +cd ${CORRAL_DIR} +git checkout 9311d7273384 # Build Corral cd ${CORRAL_DIR}/references @@ -131,6 +162,7 @@ cd ${CORRAL_DIR}/references cp ${BOOGIE_DIR}/Binaries/AbsInt.dll . cp ${BOOGIE_DIR}/Binaries/Basetypes.dll . cp ${BOOGIE_DIR}/Binaries/CodeContractsExtender.dll . +cp ${BOOGIE_DIR}/Binaries/Concurrency.dll . cp ${BOOGIE_DIR}/Binaries/Core.dll . cp ${BOOGIE_DIR}/Binaries/ExecutionEngine.dll . cp ${BOOGIE_DIR}/Binaries/Graph.dll . @@ -147,7 +179,6 @@ cp ${BOOGIE_DIR}/Binaries/Predication.dll . cd ${CORRAL_DIR} xbuild cba.sln -cp ${CORRAL_DIR}/references/UnivBackPred2.smt2 ${CORRAL_DIR}/bin/Debug ln -s ${Z3_DIR}/install/bin/z3 ${CORRAL_DIR}/bin/Debug/z3.exe cd ${BASE_DIR} @@ -160,20 +191,24 @@ fi if [ ${INSTALL_LLVM} -eq 1 ]; then +mkdir -p ${LLVM_DIR}/src +mkdir -p ${LLVM_DIR}/build +mkdir -p ${LLVM_DIR}/install + # Get llvm and extract -wget http://llvm.org/releases/3.3/llvm-3.3.src.tar.gz -wget http://llvm.org/releases/3.3/cfe-3.3.src.tar.gz -wget http://llvm.org/releases/3.3/compiler-rt-3.3.src.tar.gz +wget http://llvm.org/releases/3.4/llvm-3.4.src.tar.gz +wget http://llvm.org/releases/3.4/clang-3.4.src.tar.gz +wget http://llvm.org/releases/3.4/compiler-rt-3.4.src.tar.gz -tar -C ${LLVM_DIR}/src -xzvf llvm-3.3.src.tar.gz --strip 1 +tar -C ${LLVM_DIR}/src -xzvf llvm-3.4.src.tar.gz --strip 1 mkdir -p ${LLVM_DIR}/src/tools/clang -tar -C ${LLVM_DIR}/src/tools/clang -xzvf cfe-3.3.src.tar.gz --strip 1 +tar -C ${LLVM_DIR}/src/tools/clang -xzvf clang-3.4.src.tar.gz --strip 1 mkdir -p ${LLVM_DIR}/src/projects/compiler-rt -tar -C ${LLVM_DIR}/src/projects/compiler-rt -xzvf compiler-rt-3.3.src.tar.gz --strip 1 +tar -C ${LLVM_DIR}/src/projects/compiler-rt -xzvf compiler-rt-3.4.src.tar.gz --strip 1 # Configure llvm and build cd ${LLVM_DIR}/build/ -${LLVM_DIR}/src/configure --prefix=${LLVM_DIR}/install +${LLVM_DIR}/src/configure --prefix=${LLVM_DIR}/install --enable-optimized make make install @@ -187,12 +222,16 @@ fi if [ ${INSTALL_SMACK} -eq 1 ]; then +mkdir -p ${SMACK_DIR}/src +mkdir -p ${SMACK_DIR}/build +mkdir -p ${SMACK_DIR}/install + # Get SMACK git clone git://github.com/smackers/smack.git ${SMACK_DIR}/src/ # Configure SMACK and build cd ${SMACK_DIR}/build/ -${SMACK_DIR}/src/configure --with-llvmsrc=${LLVM_DIR}/src --with-llvmobj=${LLVM_DIR}/build --prefix=${SMACK_DIR}/install +${SMACK_DIR}/src/configure --with-llvmsrc=${LLVM_DIR}/src --with-llvmobj=${LLVM_DIR}/build --prefix=${SMACK_DIR}/install --enable-optimized make make install @@ -201,8 +240,8 @@ cd ${BASE_DIR} # Set required paths and environment variables export BOOGIE="mono ${BOOGIE_DIR}/Binaries/Boogie.exe" export CORRAL="mono ${CORRAL_DIR}/bin/Debug/corral.exe" -export PATH=$PATH:${LLVM_DIR}/install/bin -export PATH=$PATH:${SMACK_DIR}/install/bin +export PATH=${LLVM_DIR}/install/bin:$PATH +export PATH=${SMACK_DIR}/install/bin:$PATH # Run SMACK regressions cd ${SMACK_DIR}/src/test diff --git a/bin/llvm2bpl.py b/bin/llvm2bpl.py index 2e6c58cce..692a43da1 100755 --- a/bin/llvm2bpl.py +++ b/bin/llvm2bpl.py @@ -7,7 +7,7 @@ import io import platform -VERSION = '1.3.1' +VERSION = '1.4.0' def is_valid_file(parser, arg): @@ -30,59 +30,30 @@ def llvm2bplParser(): help='turn on debug info') parser.add_argument('--mem-mod', dest='memmod', choices=['flat', 'twodim'], default='flat', help='set the memory model (flat=flat memory model, twodim=two dimensional memory model)') + parser.add_argument('--mem-impls', dest='memimpls', action="store_true", default=False, + help='use procedure implementations for memory allocation') return parser -def find_install_prefix(smackRoot): - installPrefix = path.join(smackRoot, 'Debug+Asserts') - if not path.exists(installPrefix): - installPrefix = path.join(smackRoot, 'Release+Asserts') - if not path.exists(installPrefix): - installPrefix = smackRoot - assert path.exists(installPrefix) - return installPrefix - - -def find_library_path(installPrefix): - libraryPath = path.join(installPrefix, 'lib', 'smack.so') - if not path.exists(libraryPath): - libraryPath = path.join(installPrefix, 'lib', 'smack.dylib') - if not path.exists(libraryPath): - libraryPath = path.join(installPrefix, 'bin', 'smack.dll') - assert path.exists(libraryPath) - return libraryPath - - -def llvm2bpl(scriptPathName, infile, debugFlag, memmod): - - # find library paths - scriptFullPath = path.abspath(scriptPathName) - smackRoot = path.dirname(scriptFullPath) - installPrefix = find_install_prefix(smackRoot) - libraryPath = find_library_path(installPrefix) - - # invoke SMACK LLVM module - if debugFlag: - p = subprocess.Popen(['opt', '-load=' + libraryPath, '-internalize', '-mem2reg', - '-source-loc-syms', - '-die', '-lowerswitch', '-bpl_print', '-mem-mod=' + memmod, '-debug', '-o=tmp.bc'], - stdin=infile, stderr=subprocess.PIPE) - else: - p = subprocess.Popen(['opt', '-load=' + libraryPath, '-internalize', '-mem2reg', - '-source-loc-syms', - '-die', '-lowerswitch', '-bpl_print', '-mem-mod=' + memmod, '-debug-only=bpl', '-o=tmp.bc'], - stdin=infile, stderr=subprocess.PIPE) - output = p.communicate()[1] - bplStartIndex = output.find('// SMACK-PRELUDE-BEGIN') - debug = output[0:bplStartIndex] +def llvm2bpl(infile, debugFlag, memmod, memImpls): + + cmd = ['smack', '-source-loc-syms', '-mem-mod=' + memmod, infile.name] + if debugFlag: cmd.append('-debug') + if memImpls: cmd.append('-mem-mod-impls') + p = subprocess.Popen(cmd) + + p.wait() if p.returncode != 0: - if debugFlag: - print debug - print >> sys.stderr, "LLVM/SMACK encountered an error:" + print >> sys.stderr, "SMACK encountered an error:" print >> sys.stderr, output[0:1000], "... (output truncated)" - sys.exit("LLVM/SMACK returned exit status %s" % p.returncode) + sys.exit("SMACK returned exit status %s" % p.returncode) + + with open('a.bpl', 'r') as outputFile: + output = outputFile.read() + + bplStartIndex = output.find('// SMACK-PRELUDE-BEGIN') bpl = output[bplStartIndex:] - return debug, bpl + return bpl if __name__ == '__main__': @@ -91,11 +62,7 @@ def llvm2bpl(scriptPathName, infile, debugFlag, memmod): parser = argparse.ArgumentParser(description='Outputs a plain Boogie file generated from the input LLVM file.', parents=[llvm2bplParser()]) args = parser.parse_args() - debug, bpl = llvm2bpl(path.dirname(sys.argv[0]), args.infile, args.debug, args.memmod) - - # print debug info - if args.debug: - print debug + bpl = llvm2bpl(args.infile, args.debug, args.memmod, args.memimpls) # write final output args.outfile.write(bpl) diff --git a/bin/smack-verify.py b/bin/smack-verify.py index 8f494fb95..abf7e57ac 100755 --- a/bin/smack-verify.py +++ b/bin/smack-verify.py @@ -8,7 +8,7 @@ import platform from smackgen import * -VERSION = '1.3.1' +VERSION = '1.4.0' def generateSourceErrorTrace(boogieOutput, bpl): @@ -66,13 +66,13 @@ def generateSourceErrorTrace(boogieOutput, bpl): # parse command line arguments parser = argparse.ArgumentParser(description='Checks the input LLVM file for assertion violations.', parents=[smackParser()]) - parser.add_argument('--unroll', metavar='N', dest='unroll', default='20', type=int, + parser.add_argument('--unroll', metavar='N', dest='unroll', default='2', type=int, help='unroll loops/recursion in Boogie/Corral N number of times') parser.add_argument('--time-limit', metavar='N', dest='timeLimit', default='1200', type=int, help='Boogie time limit in seconds') args = parser.parse_args() - bpl = smackGenerate(path.dirname(sys.argv[0]), args.infile, args.debug, args.memmod, args.verifier, args.entryPoints) + bpl = smackGenerate(path.dirname(sys.argv[0]), args.infile, args.debug, args.memmod, args.memimpls, args.verifier, args.entryPoints) # write final output args.outfile.write(bpl) diff --git a/bin/smackgen.py b/bin/smackgen.py index 55698d777..ccb43d21d 100755 --- a/bin/smackgen.py +++ b/bin/smackgen.py @@ -7,7 +7,7 @@ import platform from llvm2bpl import * -VERSION = '1.3.1' +VERSION = '1.4.0' def smackParser(): @@ -39,13 +39,6 @@ def addEntryPoint(match, entryPoints): return procDef -def replaceDebugInfo(match): - fileName = match.group(1) - line = match.group(2) - col = match.group(3) - return 'assert {:sourcefile "' + fileName + '"} {:sourceline ' + line + '} true;' - - def clang(scriptPathName, inputFile): scriptFullPath = path.abspath(scriptPathName) smackRoot = path.dirname(scriptFullPath) @@ -56,33 +49,31 @@ def clang(scriptPathName, inputFile): p = subprocess.Popen(['clang', '-c', '-Wall', '-emit-llvm', '-O0', '-g', '-I' + smackHeaders, inputFile.name, '-o', fileName + '.bc']) p.wait() + + if p.returncode != 0: + sys.exit("SMACK encountered a clang error. Exiting...") + inputFileName = path.join(path.curdir, fileName + '.bc') inputFile = open(inputFileName, 'r') return inputFile -def smackGenerate(scriptPathName, inputFile, debugFlag, memmod, verifier, entryPoints): +def smackGenerate(scriptPathName, inputFile, debugFlag, memmod, memimpls, verifier, entryPoints): fileExtension = path.splitext(inputFile.name)[1] if fileExtension == '.c': # if input file is .c, then compile it first with clang inputFile = clang(scriptPathName, inputFile) - debug, bpl = llvm2bpl(scriptPathName, inputFile, debugFlag, memmod) + bpl = llvm2bpl(inputFile, debugFlag, memmod, memimpls) inputFile.close() - # print debug info - if debugFlag: - print debug - - p = re.compile('procedure[ ]*([a-zA-Z0-9_$]*)[ ]*\(') + p = re.compile('procedure\s+([^\s(]*)\s*\(') if verifier == 'boogie-inline': # put inline on procedures bpl = p.sub(lambda match: addInline(match, entryPoints), bpl) elif verifier == 'corral': # annotate entry points bpl = p.sub(lambda match: addEntryPoint(match, entryPoints), bpl) - p = re.compile('assume {:sourceloc "(.*)", ([0-9]*), ([0-9]*)} true;') - bpl = p.sub(lambda match: replaceDebugInfo(match), bpl) return bpl @@ -92,7 +83,7 @@ def smackGenerate(scriptPathName, inputFile, debugFlag, memmod, verifier, entryP parser = argparse.ArgumentParser(description='Outputs the appropriately annotated Boogie file generated from the input LLVM file.', parents=[smackParser()]) args = parser.parse_args() - bpl = smackGenerate(path.dirname(sys.argv[0]), args.infile, args.debug, args.memmod, args.verifier, args.entryPoints) + bpl = smackGenerate(path.dirname(sys.argv[0]), args.infile, args.debug, args.memmod, args.memimpls, args.verifier, args.entryPoints) # write final output args.outfile.write(bpl) diff --git a/configure b/configure index f5656f718..3e5f9ef0b 100755 --- a/configure +++ b/configure @@ -1,11 +1,13 @@ #! /bin/sh # Guess values for system-dependent variables and create Makefiles. -# Generated by GNU Autoconf 2.69 for SMACK 1.3.1. +# Generated by GNU Autoconf 2.68 for SMACK 1.4.0. # # Report bugs to . # # -# Copyright (C) 1992-1996, 1998-2012 Free Software Foundation, Inc. +# Copyright (C) 1992, 1993, 1994, 1995, 1996, 1998, 1999, 2000, 2001, +# 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010 Free Software +# Foundation, Inc. # # # This configure script is free software; the Free Software Foundation @@ -134,31 +136,6 @@ export LANGUAGE # CDPATH. (unset CDPATH) >/dev/null 2>&1 && unset CDPATH -# Use a proper internal environment variable to ensure we don't fall - # into an infinite loop, continuously re-executing ourselves. - if test x"${_as_can_reexec}" != xno && test "x$CONFIG_SHELL" != x; then - _as_can_reexec=no; export _as_can_reexec; - # We cannot yet assume a decent shell, so we have to provide a -# neutralization value for shells without unset; and this also -# works around shells that cannot unset nonexistent variables. -# Preserve -v and -x to the replacement shell. -BASH_ENV=/dev/null -ENV=/dev/null -(unset BASH_ENV) >/dev/null 2>&1 && unset BASH_ENV ENV -case $- in # (((( - *v*x* | *x*v* ) as_opts=-vx ;; - *v* ) as_opts=-v ;; - *x* ) as_opts=-x ;; - * ) as_opts= ;; -esac -exec $CONFIG_SHELL $as_opts "$as_myself" ${1+"$@"} -# Admittedly, this is quite paranoid, since all the known shells bail -# out after a failed `exec'. -$as_echo "$0: could not re-execute with $CONFIG_SHELL" >&2 -as_fn_exit 255 - fi - # We don't want this to propagate to other subprocesses. - { _as_can_reexec=; unset _as_can_reexec;} if test "x$CONFIG_SHELL" = x; then as_bourne_compatible="if test -n \"\${ZSH_VERSION+set}\" && (emulate sh) >/dev/null 2>&1; then : emulate sh @@ -192,8 +169,7 @@ if ( set x; as_fn_ret_success y && test x = \"\$1\" ); then : else exitcode=1; echo positional parameters were not saved. fi -test x\$exitcode = x0 || exit 1 -test -x / || exit 1" +test x\$exitcode = x0 || exit 1" as_suggested=" as_lineno_1=";as_suggested=$as_suggested$LINENO;as_suggested=$as_suggested" as_lineno_1a=\$LINENO as_lineno_2=";as_suggested=$as_suggested$LINENO;as_suggested=$as_suggested" as_lineno_2a=\$LINENO eval 'test \"x\$as_lineno_1'\$as_run'\" != \"x\$as_lineno_2'\$as_run'\" && @@ -238,25 +214,21 @@ IFS=$as_save_IFS if test "x$CONFIG_SHELL" != x; then : - export CONFIG_SHELL - # We cannot yet assume a decent shell, so we have to provide a -# neutralization value for shells without unset; and this also -# works around shells that cannot unset nonexistent variables. -# Preserve -v and -x to the replacement shell. -BASH_ENV=/dev/null -ENV=/dev/null -(unset BASH_ENV) >/dev/null 2>&1 && unset BASH_ENV ENV -case $- in # (((( - *v*x* | *x*v* ) as_opts=-vx ;; - *v* ) as_opts=-v ;; - *x* ) as_opts=-x ;; - * ) as_opts= ;; -esac -exec $CONFIG_SHELL $as_opts "$as_myself" ${1+"$@"} -# Admittedly, this is quite paranoid, since all the known shells bail -# out after a failed `exec'. -$as_echo "$0: could not re-execute with $CONFIG_SHELL" >&2 -exit 255 + # We cannot yet assume a decent shell, so we have to provide a + # neutralization value for shells without unset; and this also + # works around shells that cannot unset nonexistent variables. + # Preserve -v and -x to the replacement shell. + BASH_ENV=/dev/null + ENV=/dev/null + (unset BASH_ENV) >/dev/null 2>&1 && unset BASH_ENV ENV + export CONFIG_SHELL + case $- in # (((( + *v*x* | *x*v* ) as_opts=-vx ;; + *v* ) as_opts=-v ;; + *x* ) as_opts=-x ;; + * ) as_opts= ;; + esac + exec "$CONFIG_SHELL" $as_opts "$as_myself" ${1+"$@"} fi if test x$as_have_required = xno; then : @@ -267,10 +239,10 @@ fi $as_echo "$0: be upgraded to zsh 4.3.4 or later." else $as_echo "$0: Please tell bug-autoconf@gnu.org and -$0: zvonimir@cs.utah.edu about your system, including any -$0: error possibly output before this message. Then install -$0: a modern shell, or manually run the script under such a -$0: shell if you do have one." +$0: smack-dev@googlegroups.com about your system, including +$0: any error possibly output before this message. Then +$0: install a modern shell, or manually run the script +$0: under such a shell if you do have one." fi exit 1 fi @@ -359,14 +331,6 @@ $as_echo X"$as_dir" | } # as_fn_mkdir_p - -# as_fn_executable_p FILE -# ----------------------- -# Test if FILE is an executable regular file. -as_fn_executable_p () -{ - test -f "$1" && test -x "$1" -} # as_fn_executable_p # as_fn_append VAR VALUE # ---------------------- # Append the text in VALUE to the end of the definition contained in VAR. Take @@ -488,10 +452,6 @@ as_cr_alnum=$as_cr_Letters$as_cr_digits chmod +x "$as_me.lineno" || { $as_echo "$as_me: error: cannot create $as_me.lineno; rerun with a POSIX shell" >&2; as_fn_exit 1; } - # If we had to re-execute with $CONFIG_SHELL, we're ensured to have - # already done that, so ensure we don't try to do so again and fall - # in an infinite loop. This has already happened in practice. - _as_can_reexec=no; export _as_can_reexec # Don't try to exec as it changes $[0], causing all sort of problems # (the dirname of $[0] is not the place where we might find the # original and so on. Autoconf is especially sensitive to this). @@ -526,16 +486,16 @@ if (echo >conf$$.file) 2>/dev/null; then # ... but there are two gotchas: # 1) On MSYS, both `ln -s file dir' and `ln file dir' fail. # 2) DJGPP < 2.04 has no symlinks; `ln -s' creates a wrapper executable. - # In both cases, we have to default to `cp -pR'. + # In both cases, we have to default to `cp -p'. ln -s conf$$.file conf$$.dir 2>/dev/null && test ! -f conf$$.exe || - as_ln_s='cp -pR' + as_ln_s='cp -p' elif ln conf$$.file conf$$ 2>/dev/null; then as_ln_s=ln else - as_ln_s='cp -pR' + as_ln_s='cp -p' fi else - as_ln_s='cp -pR' + as_ln_s='cp -p' fi rm -f conf$$ conf$$.exe conf$$.dir/conf$$.file conf$$.file rmdir conf$$.dir 2>/dev/null @@ -547,8 +507,28 @@ else as_mkdir_p=false fi -as_test_x='test -x' -as_executable_p=as_fn_executable_p +if test -x / >/dev/null 2>&1; then + as_test_x='test -x' +else + if ls -dL / >/dev/null 2>&1; then + as_ls_L_option=L + else + as_ls_L_option= + fi + as_test_x=' + eval sh -c '\'' + if test -d "$1"; then + test -d "$1/."; + else + case $1 in #( + -*)set "./$1";; + esac; + case `ls -ld'$as_ls_L_option' "$1" 2>/dev/null` in #(( + ???[sx]*):;;*)false;;esac;fi + '\'' sh + ' +fi +as_executable_p=$as_test_x # Sed expression to map a string onto a valid CPP name. as_tr_cpp="eval sed 'y%*$as_cr_letters%P$as_cr_LETTERS%;s%[^_$as_cr_alnum]%_%g'" @@ -580,8 +560,8 @@ MAKEFLAGS= # Identity of this package. PACKAGE_NAME='SMACK' PACKAGE_TARNAME='smack' -PACKAGE_VERSION='1.3.1' -PACKAGE_STRING='SMACK 1.3.1' +PACKAGE_VERSION='1.4.0' +PACKAGE_STRING='SMACK 1.4.0' PACKAGE_BUGREPORT='smack-dev@googlegroups.com' PACKAGE_URL='http://github.com/smackers/smack' @@ -639,13 +619,13 @@ LLVM_INCLUDEDIR LLVM_ETCDIR LLVM_DOCSDIR LLVM_DATADIR -LLVM_LIBDIR LLVM_BINDIR LLVM_PREFIX SHLIBPATH_VAR SHLIBEXT MMAP_FILE HUGE_VAL_SANITY +HAVE_LIBZ HAVE_PTHREAD USE_OPROFILE USE_UDIS86 @@ -701,8 +681,6 @@ CMP LN_S ifGNUmake NM -poolallocobj -poolallocsrc BINUTILS_INCDIR EXTRA_LD_OPTIONS EXTRA_OPTIONS @@ -716,6 +694,7 @@ ENABLE_TIMESTAMPS ENABLE_EMBED_STDCXX ENABLE_SHARED ENABLE_PIC +LLVM_ENABLE_ZLIB ENABLE_PTHREADS ENABLE_THREADS ENABLE_DOXYGEN @@ -726,9 +705,11 @@ DEBUG_SYMBOLS DEBUG_RUNTIME EXPENSIVE_CHECKS ENABLE_EXPENSIVE_CHECKS +ENABLE_WERROR DISABLE_ASSERTIONS ENABLE_PROFILING ENABLE_OPTIMIZED +ENABLE_CXX11 ENABLE_LIBCPP CVSBUILD BUILD_CXX @@ -820,9 +801,11 @@ with_llvmsrc with_llvmobj enable_polly enable_libcpp +enable_cxx11 enable_optimized enable_profiling enable_assertions +enable_werror enable_expensive_checks enable_debug_runtime enable_debug_symbols @@ -831,6 +814,7 @@ enable_docs enable_doxygen enable_threads enable_pthreads +enable_zlib enable_pic enable_shared enable_embed_stdcxx @@ -846,9 +830,8 @@ with_c_include_dirs with_gcc_toolchain with_binutils_include with_bug_report_url +enable_terminfo enable_libffi -with_poolallocsrc -with_poolallocobj with_tclinclude enable_ltdl_install with_udis86 @@ -1321,6 +1304,8 @@ target=$target_alias if test "x$host_alias" != x; then if test "x$build_alias" = x; then cross_compiling=maybe + $as_echo "$as_me: WARNING: if you wanted to set the --build type, don't use --host. + If a cross compiler is detected then cross compile mode will be used" >&2 elif test "x$build_alias" != "x$host_alias"; then cross_compiling=yes fi @@ -1406,7 +1391,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.1 to adapt to many kinds of systems. +\`configure' configures SMACK 1.4.0 to adapt to many kinds of systems. Usage: $0 [OPTION]... [VAR=VALUE]... @@ -1472,7 +1457,7 @@ fi if test -n "$ac_init_help"; then case $ac_init_help in - short | recursive ) echo "Configuration of SMACK 1.3.1:";; + short | recursive ) echo "Configuration of SMACK 1.4.0:";; esac cat <<\_ACEOF @@ -1482,10 +1467,12 @@ Optional Features: --enable-FEATURE[=ARG] include FEATURE [ARG=yes] --enable-polly Use polly if available (default is YES) --enable-libcpp Use libc++ if available (default is NO) + --enable-cxx11 Use c++11 if available (default is NO) --enable-optimized Compile with optimizations enabled (default is NO) --enable-profiling Compile with profiling enabled (default is NO) --enable-assertions Compile with assertion checks enabled (default is YES) + --enable-werror Compile with -Werror enabled (default is NO) --enable-expensive-checks Compile with expensive debug checks enabled (default is NO) @@ -1498,6 +1485,8 @@ Optional Features: --enable-doxygen Build doxygen documentation (default is NO) --enable-threads Use threads if available (default is YES) --enable-pthreads Use pthreads if available (default is YES) + --enable-zlib Use zlib for compression/decompression if available + (default is YES) --enable-pic Build LLVM with Position Independent Code (default is YES) --enable-shared Build a shared library and link tools against it @@ -1508,10 +1497,13 @@ Optional Features: (default is YES) --enable-targets Build specific host targets: all or target1,target2,... Valid targets are: host, x86, - x86_64, sparc, powerpc, arm, mips, spu, hexagon, - xcore, msp430, nvptx, cbe, and cpp (default=all) + x86_64, sparc, powerpc, arm, aarch64, mips, hexagon, + xcore, msp430, nvptx, systemz, r600, and cpp + (default=all) --enable-bindings Build specific language bindings: all,auto,none,{binding-name} (default=auto) + --enable-terminfo Query the terminfo database if available (default is + YES) --enable-libffi Check for the presence of libffi (default is NO) --enable-ltdl-install install libltdl @@ -1536,8 +1528,6 @@ Optional Packages: plugin-api.h file for gold plugin. --with-bug-report-url Specify the URL where bug reports should be submitted (default=http://llvm.org/bugs/) - --with-poolallocsrc Specify location of Pool Allocation source code - --with-poolallocobj Specify location of Pool Allocation object code --with-tclinclude directory where tcl headers are --with-udis86= Use udis86 external x86 disassembler library --with-oprofile= @@ -1558,7 +1548,8 @@ Some influential environment variables: Use these variables to override the choices made by `configure' or to help it to find libraries and programs with nonstandard names/locations. -Report bugs to . +Report bugs to . +SMACK home page: . _ACEOF ac_status=$? fi @@ -1621,10 +1612,10 @@ fi test -n "$ac_init_help" && exit $ac_status if $ac_init_version; then cat <<\_ACEOF -SMACK configure 1.3.1 -generated by GNU Autoconf 2.69 +SMACK configure 1.4.0 +generated by GNU Autoconf 2.68 -Copyright (C) 2012 Free Software Foundation, Inc. +Copyright (C) 2010 Free Software Foundation, Inc. This configure script is free software; the Free Software Foundation gives unlimited permission to copy, distribute and modify it. _ACEOF @@ -1848,7 +1839,7 @@ $as_echo "$ac_try_echo"; } >&5 test ! -s conftest.err } && test -s conftest$ac_exeext && { test "$cross_compiling" = yes || - test -x conftest$ac_exeext + $as_test_x conftest$ac_exeext }; then : ac_retval=0 else @@ -1937,9 +1928,9 @@ $as_echo "$as_me: WARNING: $2: see the Autoconf documentation" >&2;} $as_echo "$as_me: WARNING: $2: section \"Present But Cannot Be Compiled\"" >&2;} { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $2: proceeding with the compiler's result" >&5 $as_echo "$as_me: WARNING: $2: proceeding with the compiler's result" >&2;} -( $as_echo "## ----------------------------------- ## -## Report this to zvonimir@cs.utah.edu ## -## ----------------------------------- ##" +( $as_echo "## ----------------------------------------- ## +## Report this to smack-dev@googlegroups.com ## +## ----------------------------------------- ##" ) | sed "s/^/$as_me: WARNING: /" >&2 ;; esac @@ -2170,8 +2161,8 @@ 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.1, which was -generated by GNU Autoconf 2.69. Invocation command line was +It was created by SMACK $as_me 1.4.0, which was +generated by GNU Autoconf 2.68. Invocation command line was $ $0 $@ @@ -2630,7 +2621,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_CC="$ac_tool_prefix$ac_prog" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -2674,7 +2665,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_ac_ct_CC="$ac_prog" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -3118,7 +3109,8 @@ cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ #include #include -struct stat; +#include +#include /* Most of the following tests are stolen from RCS 5.7's src/conf.sh. */ struct buf { int x; }; FILE * (*rcsopen) (struct buf *, struct stat *, int); @@ -3231,7 +3223,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_CXX="$ac_tool_prefix$ac_prog" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -3275,7 +3267,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_ac_ct_CXX="$ac_prog" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -3958,13 +3950,14 @@ else sparc*-*) llvm_cv_target_arch="Sparc" ;; powerpc*-*) llvm_cv_target_arch="PowerPC" ;; arm*-*) llvm_cv_target_arch="ARM" ;; + aarch64*-*) llvm_cv_target_arch="AArch64" ;; mips-* | mips64-*) llvm_cv_target_arch="Mips" ;; mipsel-* | mips64el-*) llvm_cv_target_arch="Mips" ;; xcore-*) llvm_cv_target_arch="XCore" ;; msp430-*) llvm_cv_target_arch="MSP430" ;; hexagon-*) llvm_cv_target_arch="Hexagon" ;; - mblaze-*) llvm_cv_target_arch="MBlaze" ;; nvptx-*) llvm_cv_target_arch="NVPTX" ;; + s390x-*) llvm_cv_target_arch="SystemZ" ;; *) llvm_cv_target_arch="Unknown" ;; esac fi @@ -4004,7 +3997,7 @@ do for ac_prog in grep ggrep; do for ac_exec_ext in '' $ac_executable_extensions; do ac_path_GREP="$as_dir/$ac_prog$ac_exec_ext" - as_fn_executable_p "$ac_path_GREP" || continue + { test -f "$ac_path_GREP" && $as_test_x "$ac_path_GREP"; } || continue # Check for GNU ac_path_GREP and select it if it is found. # Check for GNU $ac_path_GREP case `"$ac_path_GREP" --version 2>&1` in @@ -4070,7 +4063,7 @@ do for ac_prog in egrep; do for ac_exec_ext in '' $ac_executable_extensions; do ac_path_EGREP="$as_dir/$ac_prog$ac_exec_ext" - as_fn_executable_p "$ac_path_EGREP" || continue + { test -f "$ac_path_EGREP" && $as_test_x "$ac_path_EGREP"; } || continue # Check for GNU ac_path_EGREP and select it if it is found. # Check for GNU $ac_path_EGREP case `"$ac_path_EGREP" --version 2>&1` in @@ -4503,7 +4496,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_BUILD_CC="${ac_build_prefix}gcc" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -4541,7 +4534,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_BUILD_CC="gcc" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -4580,7 +4573,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then if test "$as_dir/$ac_word$ac_exec_ext" = "/usr/ucb/cc"; then ac_prog_rejected=yes continue @@ -4666,7 +4659,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_BUILD_CXX="${ac_build_prefix}g++" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -4704,7 +4697,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_BUILD_CXX="g++" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -4743,7 +4736,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then if test "$as_dir/$ac_word$ac_exec_ext" = "/usr/ucb/c++"; then ac_prog_rejected=yes continue @@ -4815,6 +4808,23 @@ case "$enableval" in *) as_fn_error $? "Invalid setting for --enable-libcpp. Use \"yes\" or \"no\"" "$LINENO" 5 ;; esac +# Check whether --enable-cxx11 was given. +if test "${enable_cxx11+set}" = set; then : + enableval=$enable_cxx11; +else + enableval=default +fi + +case "$enableval" in + yes) ENABLE_CXX11=1 + ;; + no) ENABLE_CXX11=0 + ;; + default) ENABLE_CXX11=0 +;; + *) as_fn_error $? "Invalid setting for --enable-cxx11. Use \"yes\" or \"no\"" "$LINENO" 5 ;; +esac + # Check whether --enable-optimized was given. if test "${enable_optimized+set}" = set; then : enableval=$enable_optimized; @@ -4860,6 +4870,23 @@ else fi +# Check whether --enable-werror was given. +if test "${enable_werror+set}" = set; then : + enableval=$enable_werror; +else + enableval="no" +fi + +case "$enableval" in + yes) ENABLE_WERROR=1 + ;; + no) ENABLE_WERROR=0 + ;; + default) ENABLE_WERROR=0 +;; + *) as_fn_error $? "Invalid setting for --enable-werror. Use \"yes\" or \"no\"" "$LINENO" 5 ;; +esac + # Check whether --enable-expensive-checks was given. if test "${enable_expensive_checks+set}" = set; then : enableval=$enable_expensive_checks; @@ -4931,6 +4958,8 @@ else x86_64) TARGET_HAS_JIT=1 ;; ARM) TARGET_HAS_JIT=1 + ;; + AArch64) TARGET_HAS_JIT=0 ;; Mips) TARGET_HAS_JIT=1 ;; @@ -4939,10 +4968,10 @@ else MSP430) TARGET_HAS_JIT=0 ;; Hexagon) TARGET_HAS_JIT=0 - ;; - MBlaze) TARGET_HAS_JIT=0 ;; NVPTX) TARGET_HAS_JIT=0 + ;; + SystemZ) TARGET_HAS_JIT=1 ;; *) TARGET_HAS_JIT=0 ;; @@ -5022,6 +5051,28 @@ case "$enableval" in *) as_fn_error $? "Invalid setting for --enable-pthreads. Use \"yes\" or \"no\"" "$LINENO" 5 ;; esac +# Check whether --enable-zlib was given. +if test "${enable_zlib+set}" = set; then : + enableval=$enable_zlib; +else + enableval=default +fi + +case "$enableval" in + yes) LLVM_ENABLE_ZLIB=1 + ;; + no) LLVM_ENABLE_ZLIB=0 + ;; + default) LLVM_ENABLE_ZLIB=1 + ;; + *) as_fn_error $? "Invalid setting for --enable-zlib. Use \"yes\" or \"no\"" "$LINENO" 5 ;; +esac + +cat >>confdefs.h <<_ACEOF +#define LLVM_ENABLE_ZLIB $LLVM_ENABLE_ZLIB +_ACEOF + + # Check whether --enable-pic was given. if test "${enable_pic+set}" = set; then : enableval=$enable_pic; @@ -5112,35 +5163,39 @@ if test "$enableval" = host-only ; then enableval=host fi case "$enableval" in - all) TARGETS_TO_BUILD="X86 Sparc PowerPC ARM Mips CellSPU XCore MSP430 Hexagon CppBackend MBlaze NVPTX" ;; + all) TARGETS_TO_BUILD="X86 Sparc PowerPC AArch64 ARM Mips XCore MSP430 CppBackend NVPTX Hexagon SystemZ R600" ;; *)for a_target in `echo $enableval|sed -e 's/,/ /g' ` ; do case "$a_target" in x86) TARGETS_TO_BUILD="X86 $TARGETS_TO_BUILD" ;; x86_64) TARGETS_TO_BUILD="X86 $TARGETS_TO_BUILD" ;; sparc) TARGETS_TO_BUILD="Sparc $TARGETS_TO_BUILD" ;; powerpc) TARGETS_TO_BUILD="PowerPC $TARGETS_TO_BUILD" ;; + aarch64) TARGETS_TO_BUILD="AArch64 $TARGETS_TO_BUILD" ;; arm) TARGETS_TO_BUILD="ARM $TARGETS_TO_BUILD" ;; mips) TARGETS_TO_BUILD="Mips $TARGETS_TO_BUILD" ;; - spu) TARGETS_TO_BUILD="CellSPU $TARGETS_TO_BUILD" ;; + mipsel) TARGETS_TO_BUILD="Mips $TARGETS_TO_BUILD" ;; + mips64) TARGETS_TO_BUILD="Mips $TARGETS_TO_BUILD" ;; + mips64el) TARGETS_TO_BUILD="Mips $TARGETS_TO_BUILD" ;; xcore) TARGETS_TO_BUILD="XCore $TARGETS_TO_BUILD" ;; msp430) TARGETS_TO_BUILD="MSP430 $TARGETS_TO_BUILD" ;; - hexagon) TARGETS_TO_BUILD="Hexagon $TARGETS_TO_BUILD" ;; cpp) TARGETS_TO_BUILD="CppBackend $TARGETS_TO_BUILD" ;; - mblaze) TARGETS_TO_BUILD="MBlaze $TARGETS_TO_BUILD" ;; + hexagon) TARGETS_TO_BUILD="Hexagon $TARGETS_TO_BUILD" ;; nvptx) TARGETS_TO_BUILD="NVPTX $TARGETS_TO_BUILD" ;; + systemz) TARGETS_TO_BUILD="SystemZ $TARGETS_TO_BUILD" ;; + r600) TARGETS_TO_BUILD="R600 $TARGETS_TO_BUILD" ;; host) case "$llvm_cv_target_arch" in x86) TARGETS_TO_BUILD="X86 $TARGETS_TO_BUILD" ;; x86_64) TARGETS_TO_BUILD="X86 $TARGETS_TO_BUILD" ;; Sparc) TARGETS_TO_BUILD="Sparc $TARGETS_TO_BUILD" ;; PowerPC) TARGETS_TO_BUILD="PowerPC $TARGETS_TO_BUILD" ;; + AArch64) TARGETS_TO_BUILD="AArch64 $TARGETS_TO_BUILD" ;; ARM) TARGETS_TO_BUILD="ARM $TARGETS_TO_BUILD" ;; Mips) TARGETS_TO_BUILD="Mips $TARGETS_TO_BUILD" ;; - MBlaze) TARGETS_TO_BUILD="MBlaze $TARGETS_TO_BUILD" ;; - CellSPU|SPU) TARGETS_TO_BUILD="CellSPU $TARGETS_TO_BUILD" ;; XCore) TARGETS_TO_BUILD="XCore $TARGETS_TO_BUILD" ;; MSP430) TARGETS_TO_BUILD="MSP430 $TARGETS_TO_BUILD" ;; Hexagon) TARGETS_TO_BUILD="Hexagon $TARGETS_TO_BUILD" ;; NVPTX) TARGETS_TO_BUILD="NVPTX $TARGETS_TO_BUILD" ;; + SystemZ) TARGETS_TO_BUILD="SystemZ $TARGETS_TO_BUILD" ;; *) as_fn_error $? "Can not set target to build" "$LINENO" 5 ;; esac ;; *) as_fn_error $? "Unrecognized target $a_target" "$LINENO" 5 ;; @@ -5400,6 +5455,18 @@ cat >>confdefs.h <<_ACEOF _ACEOF +# Check whether --enable-terminfo was given. +if test "${enable_terminfo+set}" = set; then : + enableval=$enable_terminfo; case "$enableval" in + yes) llvm_cv_enable_terminfo="yes" ;; + no) llvm_cv_enable_terminfo="no" ;; + *) as_fn_error $? "Invalid setting for --enable-terminfo. Use \"yes\" or \"no\"" "$LINENO" 5 ;; + esac +else + llvm_cv_enable_terminfo="yes" +fi + + # Check whether --enable-libffi was given. if test "${enable_libffi+set}" = set; then : enableval=$enable_libffi; case "$enableval" in @@ -5413,34 +5480,6 @@ fi - -# Check whether --with-poolallocsrc was given. -if test "${with_poolallocsrc+set}" = set; then : - withval=$with_poolallocsrc; poolallocsrc="$withval" - -else - poolallocsrc="$LLVM_SRC_ROOT/projects/poolalloc" - - -fi - - - -# Check whether --with-poolallocobj was given. -if test "${with_poolallocobj+set}" = set; then : - withval=$with_poolallocobj; poolallocobj="$withval" - -else - poolallocobj="$LLVM_OBJ_ROOT/projects/poolalloc" - - -fi - - -poolallocsrc=`cd $poolallocsrc && pwd` -poolallocobj=`cd $poolallocobj && pwd` - - { $as_echo "$as_me:${as_lineno-$LINENO}: checking for BSD-compatible nm" >&5 $as_echo_n "checking for BSD-compatible nm... " >&6; } if ${lt_cv_path_NM+:} false; then : @@ -5551,7 +5590,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_CMP="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -5592,7 +5631,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_CP="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -5633,7 +5672,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_DATE="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -5674,7 +5713,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_FIND="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -5715,7 +5754,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_GREP="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -5756,7 +5795,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_MKDIR="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -5797,7 +5836,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_MV="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -5837,7 +5876,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_RANLIB="${ac_tool_prefix}ranlib" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -5877,7 +5916,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_ac_ct_RANLIB="ranlib" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -5929,7 +5968,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_AR="${ac_tool_prefix}ar" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -5969,7 +6008,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_prog_ac_ct_AR="ar" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6022,7 +6061,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_RM="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6063,7 +6102,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_SED="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6104,7 +6143,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_TAR="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6145,7 +6184,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_BINPWD="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6187,7 +6226,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_GRAPHVIZ="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6241,7 +6280,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_DOT="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6295,7 +6334,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_FDP="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6349,7 +6388,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_NEATO="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6403,7 +6442,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_TWOPI="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6457,7 +6496,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_CIRCO="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6513,7 +6552,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_GV="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6570,7 +6609,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_DOTTY="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6624,7 +6663,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_XDOT_PY="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6698,7 +6737,7 @@ case $as_dir/ in #(( # by default. for ac_prog in ginstall scoinst install; do for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_prog$ac_exec_ext"; then + if { test -f "$as_dir/$ac_prog$ac_exec_ext" && $as_test_x "$as_dir/$ac_prog$ac_exec_ext"; }; then if test $ac_prog = install && grep dspmsg "$as_dir/$ac_prog$ac_exec_ext" >/dev/null 2>&1; then # AIX install. It has an incompatible calling convention. @@ -6777,7 +6816,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_BZIP2="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6817,7 +6856,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_CAT="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6857,7 +6896,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_DOXYGEN="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6897,7 +6936,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_GROFF="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6937,7 +6976,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_GZIPBIN="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -6977,7 +7016,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_POD2HTML="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -7017,7 +7056,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_POD2MAN="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -7057,7 +7096,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_PDFROFF="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -7097,7 +7136,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_RUNTEST="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -7170,7 +7209,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_TCLSH="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -7225,7 +7264,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_ZIP="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -7267,7 +7306,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_OCAMLC="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -7312,7 +7351,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_OCAMLOPT="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -7357,7 +7396,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_OCAMLDEP="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -7402,7 +7441,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_OCAMLDOC="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -7447,7 +7486,7 @@ do IFS=$as_save_IFS test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then ac_cv_path_GAS="$as_dir/$ac_word$ac_exec_ext" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 @@ -7547,8 +7586,8 @@ $as_echo "#define HAVE_LINK_R 1" >>confdefs.h fi -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for compiler -Wl,-export-dynamic option" >&5 -$as_echo_n "checking for compiler -Wl,-export-dynamic option... " >&6; } +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for compiler -rdynamic option" >&5 +$as_echo_n "checking for compiler -rdynamic option... " >&6; } if ${llvm_cv_link_use_export_dynamic+:} false; then : $as_echo_n "(cached) " >&6 else @@ -7559,7 +7598,7 @@ ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $ ac_compiler_gnu=$ac_cv_c_compiler_gnu oldcflags="$CFLAGS" - CFLAGS="$CFLAGS -Wl,-export-dynamic" + CFLAGS="$CFLAGS -rdynamic" cat confdefs.h - <<_ACEOF >conftest.$ac_ext /* end confdefs.h. */ @@ -7681,11 +7720,11 @@ else int main () { - +/* FIXME: Include the comments suggested by Paul. */ #ifndef __cplusplus - /* Ultrix mips cc rejects this sort of thing. */ + /* Ultrix mips cc rejects this. */ typedef int charset[2]; - const charset cs = { 0, 0 }; + const charset cs; /* SunOS 4.1.1 cc rejects this. */ char const *const *pcpcc; char **ppc; @@ -7702,9 +7741,8 @@ main () ++pcpcc; ppc = (char**) pcpcc; pcpcc = (char const *const *) ppc; - { /* SCO 3.2v4 cc rejects this sort of thing. */ - char tx; - char *t = &tx; + { /* SCO 3.2v4 cc rejects this. */ + char *t; char const *s = 0 ? (char *) 0 : (char const *) 0; *t++ = 0; @@ -7720,10 +7758,10 @@ main () iptr p = 0; ++p; } - { /* AIX XL C 1.02.0.0 rejects this sort of thing, saying + { /* AIX XL C 1.02.0.0 rejects this saying "k.c", line 2.27: 1506-025 (S) Operand must be a modifiable lvalue. */ - struct s { int j; const int *ap[3]; } bx; - struct s *b = &bx; b->j = 5; + struct s { int j; const int *ap[3]; }; + struct s *b; b->j = 5; } { /* ULTRIX-32 V3.1 (Rev 9) vcc rejects this */ const int foo = 10; @@ -8563,24 +8601,6 @@ _ACEOF fi -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking which variable specifies run-time library path" >&5 -$as_echo_n "checking which variable specifies run-time library path... " >&6; } -if ${libltdl_cv_shlibpath_var+:} false; then : - $as_echo_n "(cached) " >&6 -else - libltdl_cv_shlibpath_var="$shlibpath_var" -fi -{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $libltdl_cv_shlibpath_var" >&5 -$as_echo "$libltdl_cv_shlibpath_var" >&6; } -if test -n "$libltdl_cv_shlibpath_var"; then - -cat >>confdefs.h <<_ACEOF -#define LTDL_SHLIBPATH_VAR "$libltdl_cv_shlibpath_var" -_ACEOF - -fi - - { $as_echo "$as_me:${as_lineno-$LINENO}: checking for the default library search path" >&5 $as_echo_n "checking for the default library search path... " >&6; } if ${libltdl_cv_sys_search_path+:} false; then : @@ -9190,7 +9210,7 @@ else lt_dlunknown=0; lt_dlno_uscore=1; lt_dlneed_uscore=2 lt_status=$lt_dlunknown cat > conftest.$ac_ext <&5 +$as_echo_n "checking for main in -lshell32... " >&6; } +if ${ac_cv_lib_shell32_main+:} false; then : + $as_echo_n "(cached) " >&6 +else + ac_check_lib_save_LIBS=$LIBS +LIBS="-lshell32 $LIBS" +cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + + +int +main () +{ +return main (); + ; + return 0; +} +_ACEOF +if ac_fn_c_try_link "$LINENO"; then : + ac_cv_lib_shell32_main=yes +else + ac_cv_lib_shell32_main=no +fi +rm -f core conftest.err conftest.$ac_objext \ + conftest$ac_exeext conftest.$ac_ext +LIBS=$ac_check_lib_save_LIBS +fi +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_shell32_main" >&5 +$as_echo "$ac_cv_lib_shell32_main" >&6; } +if test "x$ac_cv_lib_shell32_main" = xyes; then : + cat >>confdefs.h <<_ACEOF +#define HAVE_LIBSHELL32 1 +_ACEOF + + LIBS="-lshell32 $LIBS" + fi fi @@ -9790,6 +9848,124 @@ $as_echo "$as_me: WARNING: dlopen() not found - disabling plugin support" >&2;} fi +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for library containing clock_gettime" >&5 +$as_echo_n "checking for library containing clock_gettime... " >&6; } +if ${ac_cv_search_clock_gettime+:} false; then : + $as_echo_n "(cached) " >&6 +else + ac_func_search_save_LIBS=$LIBS +cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + +/* Override any GCC internal prototype to avoid an error. + Use char because int might match the return type of a GCC + builtin and then its argument prototype would still apply. */ +#ifdef __cplusplus +extern "C" +#endif +char clock_gettime (); +int +main () +{ +return clock_gettime (); + ; + return 0; +} +_ACEOF +for ac_lib in '' rt; do + if test -z "$ac_lib"; then + ac_res="none required" + else + ac_res=-l$ac_lib + LIBS="-l$ac_lib $ac_func_search_save_LIBS" + fi + if ac_fn_c_try_link "$LINENO"; then : + ac_cv_search_clock_gettime=$ac_res +fi +rm -f core conftest.err conftest.$ac_objext \ + conftest$ac_exeext + if ${ac_cv_search_clock_gettime+:} false; then : + break +fi +done +if ${ac_cv_search_clock_gettime+:} false; then : + +else + ac_cv_search_clock_gettime=no +fi +rm conftest.$ac_ext +LIBS=$ac_func_search_save_LIBS +fi +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_search_clock_gettime" >&5 +$as_echo "$ac_cv_search_clock_gettime" >&6; } +ac_res=$ac_cv_search_clock_gettime +if test "$ac_res" != no; then : + test "$ac_res" = "none required" || LIBS="$ac_res $LIBS" + +fi + + +if test "$llvm_cv_enable_terminfo" = "yes" ; then + { $as_echo "$as_me:${as_lineno-$LINENO}: checking for library containing setupterm" >&5 +$as_echo_n "checking for library containing setupterm... " >&6; } +if ${ac_cv_search_setupterm+:} false; then : + $as_echo_n "(cached) " >&6 +else + ac_func_search_save_LIBS=$LIBS +cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + +/* Override any GCC internal prototype to avoid an error. + Use char because int might match the return type of a GCC + builtin and then its argument prototype would still apply. */ +#ifdef __cplusplus +extern "C" +#endif +char setupterm (); +int +main () +{ +return setupterm (); + ; + return 0; +} +_ACEOF +for ac_lib in '' tinfo curses ncurses ncursesw; do + if test -z "$ac_lib"; then + ac_res="none required" + else + ac_res=-l$ac_lib + LIBS="-l$ac_lib $ac_func_search_save_LIBS" + fi + if ac_fn_c_try_link "$LINENO"; then : + ac_cv_search_setupterm=$ac_res +fi +rm -f core conftest.err conftest.$ac_objext \ + conftest$ac_exeext + if ${ac_cv_search_setupterm+:} false; then : + break +fi +done +if ${ac_cv_search_setupterm+:} false; then : + +else + ac_cv_search_setupterm=no +fi +rm conftest.$ac_ext +LIBS=$ac_func_search_save_LIBS +fi +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_search_setupterm" >&5 +$as_echo "$ac_cv_search_setupterm" >&6; } +ac_res=$ac_cv_search_setupterm +if test "$ac_res" != no; then : + test "$ac_res" = "none required" || LIBS="$ac_res $LIBS" + +$as_echo "#define HAVE_TERMINFO 1" >>confdefs.h + +fi + +fi + if test "$llvm_cv_enable_libffi" = "yes" ; then { $as_echo "$as_me:${as_lineno-$LINENO}: checking for library containing ffi_call" >&5 $as_echo_n "checking for library containing ffi_call... " >&6; } @@ -10134,6 +10310,54 @@ fi fi +if test "$LLVM_ENABLE_ZLIB" -eq 1 ; then + { $as_echo "$as_me:${as_lineno-$LINENO}: checking for compress2 in -lz" >&5 +$as_echo_n "checking for compress2 in -lz... " >&6; } +if ${ac_cv_lib_z_compress2+:} false; then : + $as_echo_n "(cached) " >&6 +else + ac_check_lib_save_LIBS=$LIBS +LIBS="-lz $LIBS" +cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + +/* Override any GCC internal prototype to avoid an error. + Use char because int might match the return type of a GCC + builtin and then its argument prototype would still apply. */ +#ifdef __cplusplus +extern "C" +#endif +char compress2 (); +int +main () +{ +return compress2 (); + ; + return 0; +} +_ACEOF +if ac_fn_c_try_link "$LINENO"; then : + ac_cv_lib_z_compress2=yes +else + ac_cv_lib_z_compress2=no +fi +rm -f core conftest.err conftest.$ac_objext \ + conftest$ac_exeext conftest.$ac_ext +LIBS=$ac_check_lib_save_LIBS +fi +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_z_compress2" >&5 +$as_echo "$ac_cv_lib_z_compress2" >&6; } +if test "x$ac_cv_lib_z_compress2" = xyes; then : + cat >>confdefs.h <<_ACEOF +#define HAVE_LIBZ 1 +_ACEOF + + LIBS="-lz $LIBS" + +fi + +fi + # Check whether --with-udis86 was given. if test "${with_udis86+set}" = set; then : @@ -10798,6 +11022,27 @@ done else HAVE_PTHREAD=0 +fi +if test "$LLVM_ENABLE_ZLIB" -eq 1 ; then + for ac_header in zlib.h +do : + ac_fn_c_check_header_mongrel "$LINENO" "zlib.h" "ac_cv_header_zlib_h" "$ac_includes_default" +if test "x$ac_cv_header_zlib_h" = xyes; then : + cat >>confdefs.h <<_ACEOF +#define HAVE_ZLIB_H 1 +_ACEOF + HAVE_LIBZ=1 + +else + HAVE_LIBZ=0 + +fi + +done + +else + HAVE_LIBZ=0 + fi if test "$llvm_cv_enable_libffi" = "yes" ; then @@ -12664,7 +12909,6 @@ if test "${prefix}" = "NONE" ; then fi eval LLVM_PREFIX="${prefix}"; eval LLVM_BINDIR="${prefix}/bin"; -eval LLVM_LIBDIR="${prefix}/lib"; eval LLVM_DATADIR="${prefix}/share/llvm"; eval LLVM_DOCSDIR="${prefix}/share/doc/llvm"; eval LLVM_ETCDIR="${prefix}/etc/llvm"; @@ -12682,7 +12926,6 @@ LLVM_CONFIGTIME=`date` - # Place the various directores into the config.h file as #defines so that we # can know about the installation paths within LLVM. @@ -12696,11 +12939,6 @@ cat >>confdefs.h <<_ACEOF _ACEOF -cat >>confdefs.h <<_ACEOF -#define LLVM_LIBDIR "$LLVM_LIBDIR" -_ACEOF - - cat >>confdefs.h <<_ACEOF #define LLVM_DATADIR "$LLVM_DATADIR" _ACEOF @@ -12787,7 +13025,7 @@ $as_echo "$as_me: WARNING: --enable-bindings=ocaml specified, but ocamlopt not f else # ocaml stdlib is outside our prefix; use libdir/ocaml - OCAML_LIBDIR=$LLVM_LIBDIR/ocaml + OCAML_LIBDIR=${prefix}/lib/ocaml fi fi @@ -12856,7 +13094,7 @@ fi if test "$llvm_cv_link_use_export_dynamic" = "yes" ; then - RDYNAMIC="-Wl,-export-dynamic" + RDYNAMIC="-rdynamic" else RDYNAMIC="" fi @@ -12875,9 +13113,21 @@ ac_config_commands="$ac_config_commands Makefile" ac_config_commands="$ac_config_commands lib/Makefile" +ac_config_commands="$ac_config_commands lib/AssistDS/Makefile" + + +ac_config_commands="$ac_config_commands lib/DSA/Makefile" + + ac_config_commands="$ac_config_commands lib/smack/Makefile" +ac_config_commands="$ac_config_commands tools/Makefile" + + +ac_config_commands="$ac_config_commands tools/smack/Makefile" + + cat >confcache <<\_ACEOF # This file is a shell script that caches the results of configure @@ -13331,16 +13581,16 @@ if (echo >conf$$.file) 2>/dev/null; then # ... but there are two gotchas: # 1) On MSYS, both `ln -s file dir' and `ln file dir' fail. # 2) DJGPP < 2.04 has no symlinks; `ln -s' creates a wrapper executable. - # In both cases, we have to default to `cp -pR'. + # In both cases, we have to default to `cp -p'. ln -s conf$$.file conf$$.dir 2>/dev/null && test ! -f conf$$.exe || - as_ln_s='cp -pR' + as_ln_s='cp -p' elif ln conf$$.file conf$$ 2>/dev/null; then as_ln_s=ln else - as_ln_s='cp -pR' + as_ln_s='cp -p' fi else - as_ln_s='cp -pR' + as_ln_s='cp -p' fi rm -f conf$$ conf$$.exe conf$$.dir/conf$$.file conf$$.file rmdir conf$$.dir 2>/dev/null @@ -13400,16 +13650,28 @@ else as_mkdir_p=false fi - -# as_fn_executable_p FILE -# ----------------------- -# Test if FILE is an executable regular file. -as_fn_executable_p () -{ - test -f "$1" && test -x "$1" -} # as_fn_executable_p -as_test_x='test -x' -as_executable_p=as_fn_executable_p +if test -x / >/dev/null 2>&1; then + as_test_x='test -x' +else + if ls -dL / >/dev/null 2>&1; then + as_ls_L_option=L + else + as_ls_L_option= + fi + as_test_x=' + eval sh -c '\'' + if test -d "$1"; then + test -d "$1/."; + else + case $1 in #( + -*)set "./$1";; + esac; + case `ls -ld'$as_ls_L_option' "$1" 2>/dev/null` in #(( + ???[sx]*):;;*)false;;esac;fi + '\'' sh + ' +fi +as_executable_p=$as_test_x # Sed expression to map a string onto a valid CPP name. as_tr_cpp="eval sed 'y%*$as_cr_letters%P$as_cr_LETTERS%;s%[^_$as_cr_alnum]%_%g'" @@ -13430,8 +13692,8 @@ 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.1, which was -generated by GNU Autoconf 2.69. Invocation command line was +This file was extended by SMACK $as_me 1.4.0, which was +generated by GNU Autoconf 2.68. Invocation command line was CONFIG_FILES = $CONFIG_FILES CONFIG_HEADERS = $CONFIG_HEADERS @@ -13481,17 +13743,18 @@ $config_files Configuration commands: $config_commands -Report bugs to ." +Report bugs to . +SMACK home page: ." _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.1 -configured by $0, generated by GNU Autoconf 2.69, +SMACK config.status 1.4.0 +configured by $0, generated by GNU Autoconf 2.68, with options \\"\$ac_cs_config\\" -Copyright (C) 2012 Free Software Foundation, Inc. +Copyright (C) 2010 Free Software Foundation, Inc. This config.status script is free software; the Free Software Foundation gives unlimited permission to copy, distribute and modify it." @@ -13569,7 +13832,7 @@ fi _ACEOF cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 if \$ac_cs_recheck; then - set X $SHELL '$0' $ac_configure_args \$ac_configure_extra_args --no-create --no-recursion + set X '$SHELL' '$0' $ac_configure_args \$ac_configure_extra_args --no-create --no-recursion shift \$as_echo "running CONFIG_SHELL=$SHELL \$*" >&6 CONFIG_SHELL='$SHELL' @@ -13608,7 +13871,11 @@ do "Makefile.llvm.config") CONFIG_FILES="$CONFIG_FILES Makefile.llvm.config" ;; "Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS Makefile" ;; "lib/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS lib/Makefile" ;; + "lib/AssistDS/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS lib/AssistDS/Makefile" ;; + "lib/DSA/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS lib/DSA/Makefile" ;; "lib/smack/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS lib/smack/Makefile" ;; + "tools/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS tools/Makefile" ;; + "tools/smack/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS tools/smack/Makefile" ;; *) as_fn_error $? "invalid argument: \`$ac_config_target'" "$LINENO" 5;; esac @@ -14036,8 +14303,16 @@ $as_echo "$as_me: executing $ac_file commands" >&6;} ${SHELL} ${llvm_src}/autoconf/install-sh -m 0644 -c ${srcdir}/Makefile Makefile ;; "lib/Makefile":C) ${llvm_src}/autoconf/mkinstalldirs `dirname lib/Makefile` ${SHELL} ${llvm_src}/autoconf/install-sh -m 0644 -c ${srcdir}/lib/Makefile lib/Makefile ;; + "lib/AssistDS/Makefile":C) ${llvm_src}/autoconf/mkinstalldirs `dirname lib/AssistDS/Makefile` + ${SHELL} ${llvm_src}/autoconf/install-sh -m 0644 -c ${srcdir}/lib/AssistDS/Makefile lib/AssistDS/Makefile ;; + "lib/DSA/Makefile":C) ${llvm_src}/autoconf/mkinstalldirs `dirname lib/DSA/Makefile` + ${SHELL} ${llvm_src}/autoconf/install-sh -m 0644 -c ${srcdir}/lib/DSA/Makefile lib/DSA/Makefile ;; "lib/smack/Makefile":C) ${llvm_src}/autoconf/mkinstalldirs `dirname lib/smack/Makefile` ${SHELL} ${llvm_src}/autoconf/install-sh -m 0644 -c ${srcdir}/lib/smack/Makefile lib/smack/Makefile ;; + "tools/Makefile":C) ${llvm_src}/autoconf/mkinstalldirs `dirname tools/Makefile` + ${SHELL} ${llvm_src}/autoconf/install-sh -m 0644 -c ${srcdir}/tools/Makefile tools/Makefile ;; + "tools/smack/Makefile":C) ${llvm_src}/autoconf/mkinstalldirs `dirname tools/smack/Makefile` + ${SHELL} ${llvm_src}/autoconf/install-sh -m 0644 -c ${srcdir}/tools/smack/Makefile tools/smack/Makefile ;; esac done # for ac_tag diff --git a/examples/.gitignore b/examples/.gitignore new file mode 100644 index 000000000..5f36c5029 --- /dev/null +++ b/examples/.gitignore @@ -0,0 +1,4 @@ +*.ll +*.bc +*.o +*.bpl diff --git a/examples/svcomp13/locks/.gitignore b/examples/svcomp13/locks/.gitignore new file mode 100644 index 000000000..5f36c5029 --- /dev/null +++ b/examples/svcomp13/locks/.gitignore @@ -0,0 +1,4 @@ +*.ll +*.bc +*.o +*.bpl diff --git a/examples/svcomp13/locks/regtest-corral.py b/examples/svcomp13/locks/regtest-corral.py index 320aed0ee..b3929507e 100755 --- a/examples/svcomp13/locks/regtest-corral.py +++ b/examples/svcomp13/locks/regtest-corral.py @@ -2,6 +2,7 @@ import subprocess import re +import time # list of regression tests with the expected outputs tests = [ @@ -26,25 +27,37 @@ def red(text): def green(text): return '\033[0;32m' + text + '\033[0m' -passed = failed = 0 -for test in tests: +def runtests(): + passed = failed = 0 + for test in tests: - for mem in ['flat', 'twodim']: + for mem in ['flat']: - print "{0:>20} {1:>8}:".format(test[0], "(" + mem + ")"), - - # invoke SMACK - p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=corral', '--mem-mod=' + mem, '-o', test[0] +'.bpl'], stdout=subprocess.PIPE) - smackOutput = p.communicate()[0] - - # check SMACK output - if re.search(test[1], smackOutput): - print green('PASSED') - passed += 1 - else: - print red('FAILED') - failed += 1 - -print '\nPASSED count: ', passed -print 'FAILED count: ', failed + print "{0:>20} {1:>8}:".format(test[0], "(" + mem + ")"), + + # invoke SMACK + t0 = time.time() + p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=corral', + '--mem-mod=' + mem, '-o', test[0] +'.bpl'], + stdout=subprocess.PIPE) + + smackOutput = p.communicate()[0] + elapsed = time.time() - t0 + + # check SMACK output + if re.search(test[1], smackOutput): + print green('PASSED') + ' [%.2fs]' % round(elapsed, 2) + passed += 1 + else: + print red('FAILED') + failed += 1 + + return passed, failed + +if __name__ == '__main__': + + passed, failed = runtests() + + print '\nPASSED count: ', passed + print 'FAILED count: ', failed diff --git a/examples/svcomp13/locks/regtest.py b/examples/svcomp13/locks/regtest.py index 0bd69b6e4..c49efe90c 100755 --- a/examples/svcomp13/locks/regtest.py +++ b/examples/svcomp13/locks/regtest.py @@ -2,6 +2,7 @@ import subprocess import re +import time # list of regression tests with the expected outputs tests = [ @@ -26,25 +27,37 @@ def red(text): def green(text): return '\033[0;32m' + text + '\033[0m' -passed = failed = 0 -for test in tests: +def runtests(): + passed = failed = 0 + for test in tests: - for mem in ['flat', 'twodim']: + for mem in ['flat']: - print "{0:>20} {1:>8}:".format(test[0], "(" + mem + ")"), - - # invoke SMACK - p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=boogie-inline', '--mem-mod=' + mem, '-o', test[0] +'.bpl'], stdout=subprocess.PIPE) - smackOutput = p.communicate()[0] - - # check SMACK output - if re.search(test[1], smackOutput): - print green('PASSED') - passed += 1 - else: - print red('FAILED') - failed += 1 - -print '\nPASSED count: ', passed -print 'FAILED count: ', failed + print "{0:>20} {1:>8}:".format(test[0], "(" + mem + ")"), + + # invoke SMACK + t0 = time.time() + p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=boogie-inline', + '--mem-mod=' + mem, '-o', test[0] +'.bpl'], + stdout=subprocess.PIPE) + + smackOutput = p.communicate()[0] + elapsed = time.time() - t0 + + # check SMACK output + if re.search(test[1], smackOutput): + print green('PASSED') + ' [%.2fs]' % round(elapsed, 2) + passed += 1 + else: + print red('FAILED') + failed += 1 + + return passed, failed + +if __name__ == '__main__': + + passed, failed = runtests() + + print '\nPASSED count: ', passed + print 'FAILED count: ', failed diff --git a/examples/svcomp13/ntdrivers-simplified/cdaudio_simpl1_safe.cil.c b/examples/svcomp13/ntdrivers-simplified/cdaudio_simpl1_safe.cil.c index c6bbade1a..a1ad31390 100644 --- a/examples/svcomp13/ntdrivers-simplified/cdaudio_simpl1_safe.cil.c +++ b/examples/svcomp13/ntdrivers-simplified/cdaudio_simpl1_safe.cil.c @@ -1,4 +1,4 @@ -#include "smack-svcomp.h" +#include "smack.h" extern char __VERIFIER_nondet_char(void); extern int __VERIFIER_nondet_int(void); extern long __VERIFIER_nondet_long(void); diff --git a/examples/svcomp13/ntdrivers-simplified/cdaudio_simpl1_unsafe.cil.c b/examples/svcomp13/ntdrivers-simplified/cdaudio_simpl1_unsafe.cil.c index 8e447a501..ab8c63d4d 100644 --- a/examples/svcomp13/ntdrivers-simplified/cdaudio_simpl1_unsafe.cil.c +++ b/examples/svcomp13/ntdrivers-simplified/cdaudio_simpl1_unsafe.cil.c @@ -1,4 +1,4 @@ -#include "smack-svcomp.h" +#include "smack.h" extern char __VERIFIER_nondet_char(void); extern int __VERIFIER_nondet_int(void); extern long __VERIFIER_nondet_long(void); diff --git a/examples/svcomp13/ntdrivers-simplified/diskperf_simpl1_safe.cil.c b/examples/svcomp13/ntdrivers-simplified/diskperf_simpl1_safe.cil.c index 9a7559b3d..146ca5ad8 100644 --- a/examples/svcomp13/ntdrivers-simplified/diskperf_simpl1_safe.cil.c +++ b/examples/svcomp13/ntdrivers-simplified/diskperf_simpl1_safe.cil.c @@ -1,4 +1,4 @@ -#include "smack-svcomp.h" +#include "smack.h" extern char __VERIFIER_nondet_char(void); extern int __VERIFIER_nondet_int(void); extern long __VERIFIER_nondet_long(void); diff --git a/examples/svcomp13/ntdrivers-simplified/floppy_simpl3_safe.cil.c b/examples/svcomp13/ntdrivers-simplified/floppy_simpl3_safe.cil.c index 3c5ac5139..cc09ba1d5 100644 --- a/examples/svcomp13/ntdrivers-simplified/floppy_simpl3_safe.cil.c +++ b/examples/svcomp13/ntdrivers-simplified/floppy_simpl3_safe.cil.c @@ -1,4 +1,4 @@ -#include "smack-svcomp.h" +#include "smack.h" extern char __VERIFIER_nondet_char(void); extern int __VERIFIER_nondet_int(void); extern long __VERIFIER_nondet_long(void); diff --git a/examples/svcomp13/ntdrivers-simplified/floppy_simpl3_unsafe.cil.c b/examples/svcomp13/ntdrivers-simplified/floppy_simpl3_unsafe.cil.c index e11428c60..67955ecaf 100644 --- a/examples/svcomp13/ntdrivers-simplified/floppy_simpl3_unsafe.cil.c +++ b/examples/svcomp13/ntdrivers-simplified/floppy_simpl3_unsafe.cil.c @@ -1,4 +1,4 @@ -#include "smack-svcomp.h" +#include "smack.h" extern char __VERIFIER_nondet_char(void); extern int __VERIFIER_nondet_int(void); extern long __VERIFIER_nondet_long(void); diff --git a/examples/svcomp13/ntdrivers-simplified/floppy_simpl4_safe.cil.c b/examples/svcomp13/ntdrivers-simplified/floppy_simpl4_safe.cil.c index 9f9613e27..9ae66f5de 100644 --- a/examples/svcomp13/ntdrivers-simplified/floppy_simpl4_safe.cil.c +++ b/examples/svcomp13/ntdrivers-simplified/floppy_simpl4_safe.cil.c @@ -1,4 +1,4 @@ -#include "smack-svcomp.h" +#include "smack.h" extern char __VERIFIER_nondet_char(void); extern int __VERIFIER_nondet_int(void); extern long __VERIFIER_nondet_long(void); diff --git a/examples/svcomp13/ntdrivers-simplified/floppy_simpl4_unsafe.cil.c b/examples/svcomp13/ntdrivers-simplified/floppy_simpl4_unsafe.cil.c index 57e588949..3758376b3 100644 --- a/examples/svcomp13/ntdrivers-simplified/floppy_simpl4_unsafe.cil.c +++ b/examples/svcomp13/ntdrivers-simplified/floppy_simpl4_unsafe.cil.c @@ -1,4 +1,4 @@ -#include "smack-svcomp.h" +#include "smack.h" extern char __VERIFIER_nondet_char(void); extern int __VERIFIER_nondet_int(void); extern long __VERIFIER_nondet_long(void); diff --git a/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl1_safe.cil.c b/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl1_safe.cil.c index 0d17c4e37..2ea7cb4e7 100644 --- a/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl1_safe.cil.c +++ b/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl1_safe.cil.c @@ -1,4 +1,4 @@ -#include "smack-svcomp.h" +#include "smack.h" extern char __VERIFIER_nondet_char(void); extern int __VERIFIER_nondet_int(void); extern long __VERIFIER_nondet_long(void); diff --git a/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl2_safe.cil.c b/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl2_safe.cil.c index c8404113b..e269af808 100644 --- a/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl2_safe.cil.c +++ b/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl2_safe.cil.c @@ -1,4 +1,4 @@ -#include "smack-svcomp.h" +#include "smack.h" extern char __VERIFIER_nondet_char(void); extern int __VERIFIER_nondet_int(void); extern long __VERIFIER_nondet_long(void); diff --git a/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl2_unsafe.cil.c b/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl2_unsafe.cil.c index f7cef94b5..b756eba21 100644 --- a/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl2_unsafe.cil.c +++ b/examples/svcomp13/ntdrivers-simplified/kbfiltr_simpl2_unsafe.cil.c @@ -1,4 +1,4 @@ -#include "smack-svcomp.h" +#include "smack.h" extern char __VERIFIER_nondet_char(void); extern int __VERIFIER_nondet_int(void); extern long __VERIFIER_nondet_long(void); diff --git a/examples/svcomp13/ntdrivers-simplified/regtest-corral.py b/examples/svcomp13/ntdrivers-simplified/regtest-corral.py index 7b7092a04..ff1fccfc1 100755 --- a/examples/svcomp13/ntdrivers-simplified/regtest-corral.py +++ b/examples/svcomp13/ntdrivers-simplified/regtest-corral.py @@ -2,6 +2,7 @@ import subprocess import re +import time # list of regression tests with the expected outputs tests = [ @@ -23,25 +24,37 @@ def red(text): def green(text): return '\033[0;32m' + text + '\033[0m' -passed = failed = 0 -for test in tests: +def runtests(): + passed = failed = 0 + for test in tests: - for mem in ['flat', 'twodim']: + for mem in ['flat']: - print "{0:>25} {1:>8}:".format(test[0], "(" + mem + ")"), - - # invoke SMACK - p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=corral', '--mem-mod=' + mem, '-o', test[0] +'.bpl'], stdout=subprocess.PIPE) - smackOutput = p.communicate()[0] - - # check SMACK output - if re.search(test[1], smackOutput): - print green('PASSED') - passed += 1 - else: - print red('FAILED') - failed += 1 - -print '\nPASSED count: ', passed -print 'FAILED count: ', failed + print "{0:>25} {1:>8}:".format(test[0], "(" + mem + ")"), + + # invoke SMACK + t0 = time.time() + p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=corral', + '--mem-mod=' + mem, '-o', test[0] +'.bpl'], + stdout=subprocess.PIPE) + + smackOutput = p.communicate()[0] + elapsed = time.time() - t0 + + # check SMACK output + if re.search(test[1], smackOutput): + print green('PASSED') + ' [%.2fs]' % round(elapsed, 2) + passed += 1 + else: + print red('FAILED') + failed += 1 + + return passed, failed + +if __name__ == '__main__': + + passed, failed = runtests() + + print '\nPASSED count: ', passed + print 'FAILED count: ', failed diff --git a/examples/svcomp13/ntdrivers-simplified/regtest.py b/examples/svcomp13/ntdrivers-simplified/regtest.py index 95054b90f..625e93a09 100755 --- a/examples/svcomp13/ntdrivers-simplified/regtest.py +++ b/examples/svcomp13/ntdrivers-simplified/regtest.py @@ -2,6 +2,7 @@ import subprocess import re +import time # list of regression tests with the expected outputs tests = [ @@ -23,25 +24,37 @@ def red(text): def green(text): return '\033[0;32m' + text + '\033[0m' -passed = failed = 0 -for test in tests: +def runtests(): + passed = failed = 0 + for test in tests: - for mem in ['flat', 'twodim']: + for mem in ['flat']: - print "{0:>25} {1:>8}:".format(test[0], "(" + mem + ")"), - - # invoke SMACK - p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=boogie-inline', '--mem-mod=' + mem, '-o', test[0] +'.bpl'], stdout=subprocess.PIPE) - smackOutput = p.communicate()[0] - - # check SMACK output - if re.search(test[1], smackOutput): - print green('PASSED') - passed += 1 - else: - print red('FAILED') - failed += 1 - -print '\nPASSED count: ', passed -print 'FAILED count: ', failed + print "{0:>25} {1:>8}:".format(test[0], "(" + mem + ")"), + + # invoke SMACK + t0 = time.time() + p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=boogie-inline', + '--mem-mod=' + mem, '-o', test[0] +'.bpl'], + stdout=subprocess.PIPE) + + smackOutput = p.communicate()[0] + elapsed = time.time() - t0 + + # check SMACK output + if re.search(test[1], smackOutput): + print green('PASSED') + ' [%.2fs]' % round(elapsed, 2) + passed += 1 + else: + print red('FAILED') + failed += 1 + + return passed, failed + +if __name__ == '__main__': + + passed, failed = runtests() + + print '\nPASSED count: ', passed + print 'FAILED count: ', failed diff --git a/examples/svcomp13/ntdrivers-simplified/smack-svcomp.h b/examples/svcomp13/ntdrivers-simplified/smack-svcomp.h deleted file mode 100644 index 972152b34..000000000 --- a/examples/svcomp13/ntdrivers-simplified/smack-svcomp.h +++ /dev/null @@ -1,22 +0,0 @@ -#ifndef SMACKSVCOMP_H_ -#define SMACKSVCOMP_H_ -#include "smack.h" - -char __VERIFIER_nondet_char(void) { - return __SMACK_nondet(); -} - -int __VERIFIER_nondet_int(void) { - return __SMACK_nondet(); -} - -long __VERIFIER_nondet_long(void) { - return __SMACK_nondet(); -} - -void *__VERIFIER_nondet_pointer(void) { - return __SMACK_nondet(); -} - -#endif /*SMACKSVCOMP_H_*/ - diff --git a/examples/svcomp13/ntdrivers/regtest-corral.py b/examples/svcomp13/ntdrivers/regtest-corral.py new file mode 100755 index 000000000..1d5d14aea --- /dev/null +++ b/examples/svcomp13/ntdrivers/regtest-corral.py @@ -0,0 +1,60 @@ +#! /usr/bin/env python + +import subprocess +import re +import time + +# list of regression tests with the expected outputs +tests = [ + ('cdaudio_safe.i.cil', r'Program has no bugs'), + ('cdaudio_unsafe.i.cil', r'This assertion can fail'), +# ('diskperf_safe.i.cil', r'Program has no bugs'), # fails due to returning structs +# ('diskperf_unsafe.i.cil', r'This assertion can fail'), + ('floppy2_safe.i.cil', r'Program has no bugs'), + ('floppy_safe.i.cil', r'Program has no bugs'), + ('floppy_unsafe.i.cil', r'This assertion can fail'), + ('kbfiltr_unsafe.i.cil', r'This assertion can fail'), + ('parport_safe.i.cil', r'Program has no bugs'), + ('parport_unsafe.i.cil', r'This assertion can fail') +] + +def red(text): + return '\033[0;31m' + text + '\033[0m' + +def green(text): + return '\033[0;32m' + text + '\033[0m' + +def runtests(): + passed = failed = 0 + for test in tests: + + for mem in ['flat']: + + print "{0:>25} {1:>8}:".format(test[0], "(" + mem + ")"), + + # invoke SMACK + t0 = time.time() + p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=corral', + '--mem-mod=' + mem, '-o', test[0] +'.bpl'], + stdout=subprocess.PIPE) + + smackOutput = p.communicate()[0] + elapsed = time.time() - t0 + + # check SMACK output + if re.search(test[1], smackOutput): + print green('PASSED') + ' [%.2fs]' % round(elapsed, 2) + passed += 1 + else: + print red('FAILED') + failed += 1 + + return passed, failed + +if __name__ == '__main__': + + passed, failed = runtests() + + print '\nPASSED count: ', passed + print 'FAILED count: ', failed + diff --git a/examples/svcomp13/ntdrivers/regtest.py b/examples/svcomp13/ntdrivers/regtest.py new file mode 100755 index 000000000..c42881de4 --- /dev/null +++ b/examples/svcomp13/ntdrivers/regtest.py @@ -0,0 +1,60 @@ +#! /usr/bin/env python + +import subprocess +import re +import time + +# list of regression tests with the expected outputs +tests = [ + ('cdaudio_safe.i.cil', r'1 verified, 0 errors?'), + ('cdaudio_unsafe.i.cil', r'0 verified, 1 errors?'), +# ('diskperf_safe.i.cil', r'1 verified, 0 errors?'), +# ('diskperf_unsafe.i.cil', r'0 verified, 1 errors?'), + ('floppy2_safe.i.cil', r'1 verified, 0 errors?'), + ('floppy_safe.i.cil', r'1 verified, 0 errors?'), + ('floppy_unsafe.i.cil', r'0 verified, 1 errors?'), + ('kbfiltr_unsafe.i.cil', r'0 verified, 1 errors?'), + ('parport_safe.i.cil', r'1 verified, 0 errors?'), + ('parport_unsafe.i.cil', r'0 verified, 1 errors?') +] + +def red(text): + return '\033[0;31m' + text + '\033[0m' + +def green(text): + return '\033[0;32m' + text + '\033[0m' + +def runtests(): + passed = failed = 0 + for test in tests: + + for mem in ['flat']: + + print "{0:>25} {1:>8}:".format(test[0], "(" + mem + ")"), + + # invoke SMACK + t0 = time.time() + p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=boogie-inline', + '--mem-mod=' + mem, '-o', test[0] +'.bpl'], + stdout=subprocess.PIPE) + + smackOutput = p.communicate()[0] + elapsed = time.time() - t0 + + # check SMACK output + if re.search(test[1], smackOutput): + print green('PASSED') + ' [%.2fs]' % round(elapsed, 2) + passed += 1 + else: + print red('FAILED') + failed += 1 + + return passed, failed + +if __name__ == '__main__': + + passed, failed = runtests() + + print '\nPASSED count: ', passed + print 'FAILED count: ', failed + diff --git a/include/assistDS/DataStructureCallGraph.h b/include/assistDS/DataStructureCallGraph.h index 9bef18503..67e66609b 100644 --- a/include/assistDS/DataStructureCallGraph.h +++ b/include/assistDS/DataStructureCallGraph.h @@ -25,7 +25,7 @@ namespace llvm { -class DataStructureCallGraph : public ModulePass, public CallGraph { +class DataStructureCallGraph : public CallGraph { // Root is root of the call graph, or the external node if a 'main' function // couldn't be found. CallGraphNode *Root; @@ -43,7 +43,7 @@ class DataStructureCallGraph : public ModulePass, public CallGraph { public: static char ID; DataStructureCallGraph() : - ModulePass(ID), Root(0), ExternalCallingNode(0), CallsExternalNode(0) { } + Root(0), ExternalCallingNode(0), CallsExternalNode(0) { } virtual bool runOnModule(Module &M); @@ -99,7 +99,7 @@ class DataStructureCallGraph : public ModulePass, public CallGraph { delete CallsExternalNode; CallsExternalNode = 0; } - CallGraph::destroy(); + CallGraph::releaseMemory(); } }; diff --git a/include/smack/BoogieAst.h b/include/smack/BoogieAst.h index a041dbaba..0f37b94e1 100644 --- a/include/smack/BoogieAst.h +++ b/include/smack/BoogieAst.h @@ -6,18 +6,24 @@ #ifndef BOOGIEAST_H #define BOOGIEAST_H +#include #include #include +#include namespace smack { using namespace std; +class Block; +class Program; + class Expr { public: virtual void print(ostream& os) const = 0; static const Expr* and_(const Expr* l, const Expr* r); static const Expr* eq(const Expr* l, const Expr* r); + static const Expr* lt(const Expr* l, const Expr* r); static const Expr* fn(string f, const Expr* x); static const Expr* fn(string f, const Expr* x, const Expr* y); static const Expr* fn(string f, const Expr* x, const Expr* y, const Expr* z); @@ -60,7 +66,6 @@ class LitExpr : public Expr { private: const Literal lit; int val; - int width; public: LitExpr(bool b) : lit(b ? True : False) {} LitExpr(int i) : lit(Num), val(i) {} @@ -178,6 +183,7 @@ class Stmt { static const Stmt* havoc(string x); static const Stmt* return_(); static const Stmt* skip(); + static const Stmt* code(string s); virtual void print(ostream& os) const = 0; }; @@ -246,102 +252,121 @@ class ReturnStmt : public Stmt { void print(ostream& os) const; }; +class CodeStmt : public Stmt { + string code; +public: + CodeStmt(string s) : code(s) {} + void print(ostream& os) const; +}; + class Decl { + static unsigned uniqueId; +public: + enum kind { STOR, PROC, FUNC, TYPE, UNNAMED, CODE }; protected: + unsigned id; string name; - string type; - Decl(string n, string t) : name(n), type(t) {} + vector attrs; + Decl(string n, vector ax) : id(uniqueId++), name(n), attrs(ax) { } + Decl(string n) : id(uniqueId++), name(n), attrs(vector()) { } public: virtual void print(ostream& os) const = 0; - string getName() const { - return name; - } - string getType() const { - return type; + unsigned getId() const { return id; } + string getName() const { return name; } + virtual kind getKind() const = 0; + + static Decl* typee(string name, string type); + static Decl* axiom(const Expr* e); + static Decl* constant(string name, string type); + static Decl* constant(string name, string type, bool unique); + static Decl* constant(string name, string type, vector ax, bool unique); + static Decl* variable(string name, string type); + static Decl* procedure(Program& p, string name); + static Decl* procedure(Program& p, string name, + vector< pair > args, vector< pair > rets); + static Decl* code(string s); +}; + +struct DeclCompare { + bool operator()(Decl* a, Decl* b) { + assert(a && b); + if (a->getKind() == b->getKind() && a->getKind() != Decl::UNNAMED) + return a->getName() < b->getName(); + else if (a->getKind() == b->getKind()) + return a->getId() < b->getId(); + else + return a->getKind() < b->getKind(); } - static const Decl* typee(string name, string type); - static const Decl* axiom(const Expr* e); - static const Decl* constant(string name, string type); - static const Decl* constant(string name, string type, bool unique); - static const Decl* variable(string name, string type); - static const Decl* procedure(string name, string arg, string type); }; class TypeDecl : public Decl { + string alias; public: - TypeDecl(string n, string t) : Decl(n,t) {} + TypeDecl(string n, string t) : Decl(n), alias(t) {} + kind getKind() const { return TYPE; } void print(ostream& os) const; }; class AxiomDecl : public Decl { const Expr* expr; + static int uniqueId; public: - AxiomDecl(const Expr* e) : Decl("", ""), expr(e) {} + AxiomDecl(const Expr* e) : Decl(""), expr(e) {} + kind getKind() const { return UNNAMED; } void print(ostream& os) const; }; class ConstDecl : public Decl { + string type; bool unique; public: - ConstDecl(string n, string t, bool u) : Decl(n, t), unique(u) {} - ConstDecl(string n, string t) : Decl(n, t), unique(false) {} + ConstDecl(string n, string t, vector ax, bool u) : Decl(n,ax), type(t), unique(u) {} + kind getKind() const { return STOR; } void print(ostream& os) const; }; class FuncDecl : public Decl { vector< pair > params; + string type; const Expr* body; public: FuncDecl(string n, vector< pair > ps, string t, Expr* b) - : Decl(n, ""), params(ps), body(b) {} + : Decl(n), params(ps), type(t), body(b) {} + kind getKind() const { return FUNC; } void print(ostream& os) const; }; class VarDecl : public Decl { + string type; public: - VarDecl(string n, string t) : Decl(n, t) {} + VarDecl(string n, string t) : Decl(n), type(t) {} + kind getKind() const { return STOR; } void print(ostream& os) const; }; class ProcDecl : public Decl { + Program& prog; vector< pair > params; -public: - ProcDecl(string n, vector< pair > ps, string r) - : Decl(n,r), params(ps) {} - void print(ostream& os) const; -}; - -class Block { - string name; - vector stmts; -public: - Block() : name("") {} - Block(string n) : name(n) {} - void print(ostream& os) const; - void addStmt(const Stmt* s) { - stmts.push_back(s); - } - string getName() { - return name; - } -}; - -class Procedure { - string name; - vector< pair > params; - vector< pair > rets; + vector< pair > rets; vector mods; - vector decls; + vector requires; + vector ensures; + set decls; vector blocks; public: - Procedure(string n) : name(n) {} - void print(ostream& os) const; + ProcDecl(Program& p, string n, vector< pair > ps, vector< pair > rs) + : Decl(n), prog(p), params(ps), rets(rs) {} + kind getKind() const { return PROC; } + Program& getProg() const { return prog; } void addParam(string x, string t) { params.push_back(make_pair(x, t)); } void addRet(string x, string t) { rets.push_back(make_pair(x, t)); } + vector< pair > getRets() { + return rets; + } void addMod(string m) { mods.push_back(m); } @@ -349,51 +374,78 @@ class Procedure { for (unsigned i = 0; i < ms.size(); i++) addMod(ms[i]); } - void addDecl(const Decl* d) { - decls.push_back(d); + void addRequires(const Expr* e) { + requires.push_back(e); } - void addDecls(vector ds) { - for (unsigned i = 0; i < ds.size(); i++) - addDecl(ds[i]); + void addEnsures(const Expr* e) { + ensures.push_back(e); } - bool hasDecl(const Decl* d) { - for (unsigned i = 0; i < decls.size(); i++) - if (d->getName() == decls[i]->getName() - && d->getType() == decls[i]->getType()) - return true; - return false; + void addDecl(Decl* d) { + decls.insert(d); } void addBlock(Block* b) { blocks.push_back(b); } + bool hasBody() { + return decls.size() > 0 || blocks.size() > 0; + } + void print(ostream& os) const; }; -class Program { - string prelude; - vector decls; - vector procs; +class CodeDecl : public Decl { public: - Program(string p) : prelude(p) { } + CodeDecl(string s) : Decl(s) {} + kind getKind() const { return CODE; } void print(ostream& os) const; - void addDecl(const Decl* d) { - decls.push_back(d); - } - void addDecls(vector ds) { - for (unsigned i = 0; i < ds.size(); i++) - addDecl(ds[i]); +}; + +class Block { + ProcDecl& proc; + string name; + vector stmts; +public: + Block(ProcDecl& p) : proc(p), name("") {} + Block(ProcDecl& p, string n) : proc(p), name(n) {} + void print(ostream& os) const; + ProcDecl& getProc() const { return proc; } + void addStmt(const Stmt* s) { + stmts.push_back(s); } - void addProc(Procedure* p) { - procs.push_back(p); + string getName() { + return name; } - vector::const_iterator pbegin() { - return procs.begin(); +}; + +class Program { + // TODO While I would prefer that a program is just a set or sequence of + // declarations, putting the Prelude in a CodeDeclaration does not work, + // and I do not yet understand why; see below. --mje + string prelude; + set decls; +public: + Program() {} + void print(ostream& os) const; + void addDecl(Decl* d) { + decls.insert(d); } - vector::const_iterator pend() { - return procs.end(); + void addDecl(string s) { + // TODO Why does this break to put the prelude string inside of a CodeDecl? + decls.insert( Decl::code(s) ); } void appendPrelude(string s) { prelude += s; } + void addDecls(vector ds) { + for (unsigned i = 0; i < ds.size(); i++) + addDecl(ds[i]); + } + vector getProcs() { + vector procs; + for (set::iterator i = decls.begin(); i != decls.end(); ++i) + if ((*i)->getKind() == Decl::PROC) + procs.push_back((ProcDecl*) (*i)); + return procs; + } }; } diff --git a/include/smack/BplFilePrinter.h b/include/smack/BplFilePrinter.h new file mode 100644 index 000000000..4e28b8291 --- /dev/null +++ b/include/smack/BplFilePrinter.h @@ -0,0 +1,36 @@ +// +// Copyright (c) 2008 Zvonimir Rakamaric (zvonimir@cs.utah.edu), +// Pantazis Deligiannis (p.deligiannis@imperial.ac.uk) +// This file is distributed under the MIT License. See LICENSE for details. +// +#ifndef BPLFILEPRINTER_H +#define BPLFILEPRINTER_H + +#include "smack/SmackModuleGenerator.h" + +namespace smack { + +class BplFilePrinter : public llvm::ModulePass { +private: + llvm::raw_ostream &out; + +public: + static char ID; // Pass identification, replacement for typeid + + BplFilePrinter(llvm::raw_ostream &out) : llvm::ModulePass(ID), out(out) {} + + virtual bool runOnModule(llvm::Module& m); + + virtual const char *getPassName() const { + return "Boogie file printing"; + } + + virtual void getAnalysisUsage(llvm::AnalysisUsage& AU) const { + AU.setPreservesAll(); + AU.addRequired(); + } +}; +} + +#endif // BPLPRINTER_H + diff --git a/include/smack/DSAAliasAnalysis.h b/include/smack/DSAAliasAnalysis.h index 3c1309095..d8eaaf371 100644 --- a/include/smack/DSAAliasAnalysis.h +++ b/include/smack/DSAAliasAnalysis.h @@ -55,15 +55,9 @@ class MemcpyCollector : public llvm::InstVisitor { if (!f1) memcpys.push_back(eqs.getLeaderValue(n1)); if (!f2) memcpys.push_back(eqs.getLeaderValue(n2)); } - - bool has(const llvm::DSNode* n) { - const llvm::EquivalenceClasses &eqs - = nodeEqs->getEquivalenceClasses(); - const llvm::DSNode* nn = eqs.getLeaderValue(n); - for (unsigned i=0; i getMemcpys() { + return memcpys; } }; @@ -72,7 +66,8 @@ class DSAAliasAnalysis : public llvm::ModulePass, public llvm::AliasAnalysis { llvm::TDDataStructures *TD; llvm::BUDataStructures *BU; llvm::DSNodeEquivs *nodeEqs; - MemcpyCollector *memcpys; + vector staticInits; + vector memcpys; public: static char ID; @@ -91,15 +86,19 @@ class DSAAliasAnalysis : public llvm::ModulePass, public llvm::AliasAnalysis { TD = &getAnalysis(); BU = &getAnalysis(); nodeEqs = &getAnalysis(); - memcpys = new MemcpyCollector(nodeEqs); - collectMemcpys(M); + memcpys = collectMemcpys(M, new MemcpyCollector(nodeEqs)); + staticInits = collectStaticInits(M); + return false; } - + virtual AliasResult alias(const Location &LocA, const Location &LocB); private: - void collectMemcpys(llvm::Module &M); + bool isMemcpyd(const llvm::DSNode* n); + bool isStaticInitd(const llvm::DSNode* n); + vector collectMemcpys(llvm::Module &M, MemcpyCollector* mcc); + vector collectStaticInits(llvm::Module &M); llvm::DSGraph *getGraphForValue(const llvm::Value *V); bool equivNodes(const llvm::DSNode* n1, const llvm::DSNode* n2); unsigned getOffset(const Location* l); diff --git a/include/smack/SmackInstGenerator.h b/include/smack/SmackInstGenerator.h index 21848973b..d5211fe13 100644 --- a/include/smack/SmackInstGenerator.h +++ b/include/smack/SmackInstGenerator.h @@ -15,17 +15,13 @@ namespace smack { class SmackInstGenerator : public llvm::InstVisitor { private: - SmackRep* rep; - Procedure& currProc; + SmackRep& rep; + ProcDecl& proc; Block* currBlock; map& blockMap; - set >& missingDecls; - set& moreDecls; int blockNum; int varNum; - const Stmt* generateCall(llvm::Function* f, vector ps, vector rs); - void generatePhiAssigns(llvm::TerminatorInst& i); void generateGotoStmts(llvm::Instruction& i, vector > target); @@ -34,12 +30,10 @@ class SmackInstGenerator : public llvm::InstVisitor { void annotate(llvm::Instruction& i, Block* b); public: - SmackInstGenerator(SmackRep* r, Procedure& p, - map& bm, - set >& md, - set& mmdd) - : rep(r), currProc(p), blockMap(bm), missingDecls(md), moreDecls(mmdd), - blockNum(0), varNum(0) {} + SmackInstGenerator(SmackRep& r, ProcDecl& p, + map& bm) + : rep(r), proc(p), + blockMap(bm), blockNum(0), varNum(0) {} Block* createBlock(); void setCurrBlock(Block* b) { @@ -52,37 +46,55 @@ class SmackInstGenerator : public llvm::InstVisitor { string createVar(); void visitInstruction(llvm::Instruction& i); - void visitAllocaInst(llvm::AllocaInst& i); + + void visitReturnInst(llvm::ReturnInst& i); void visitBranchInst(llvm::BranchInst& i); void visitSwitchInst(llvm::SwitchInst& i); - void visitPHINode(llvm::PHINode& i); - void visitTruncInst(llvm::TruncInst& i); + // TODO implement indirectbr + // TODO implement invoke + // TODO implement resume void visitUnreachableInst(llvm::UnreachableInst& i); - void visitCallInst(llvm::CallInst& i); - void visitReturnInst(llvm::ReturnInst& i); + + void visitBinaryOperator(llvm::BinaryOperator& i); + + // TODO implement extractelement + // TODO implement insertelement + // TODO implement shufflevector + + // TODO implement extractvalue + // TODO implement insertvalue + + void visitAllocaInst(llvm::AllocaInst& i); void visitLoadInst(llvm::LoadInst& i); void visitStoreInst(llvm::StoreInst& i); + // TODO implement fence + void visitAtomicCmpXchgInst(llvm::AtomicCmpXchgInst& i); + void visitAtomicRMWInst(llvm::AtomicRMWInst& i); void visitGetElementPtrInst(llvm::GetElementPtrInst& i); - void visitICmpInst(llvm::ICmpInst& i); + + void visitTruncInst(llvm::TruncInst& i); void visitZExtInst(llvm::ZExtInst& i); void visitSExtInst(llvm::SExtInst& i); - void visitBitCastInst(llvm::BitCastInst& i); - void visitBinaryOperator(llvm::BinaryOperator& i); - void visitPtrToIntInst(llvm::PtrToIntInst& i); - void visitIntToPtrInst(llvm::IntToPtrInst& i); - void visitSelectInst(llvm::SelectInst& i); - void visitMemCpyInst(llvm::MemCpyInst& i); - - void visitFCmpInst(llvm::FCmpInst& i); void visitFPTruncInst(llvm::FPTruncInst& i); void visitFPExtInst(llvm::FPExtInst& i); - void visitFPToSIInst(llvm::FPToSIInst& i); void visitFPToUIInst(llvm::FPToUIInst& i); - void visitSIToFPInst(llvm::SIToFPInst& i); + void visitFPToSIInst(llvm::FPToSIInst& i); void visitUIToFPInst(llvm::UIToFPInst& i); + void visitSIToFPInst(llvm::SIToFPInst& i); + void visitPtrToIntInst(llvm::PtrToIntInst& i); + void visitIntToPtrInst(llvm::IntToPtrInst& i); + void visitBitCastInst(llvm::BitCastInst& i); + // TODO implement addrspacecast - void visitAtomicCmpXchgInst(llvm::AtomicCmpXchgInst& i); - void visitAtomicRMWInst(llvm::AtomicRMWInst& i); + void visitICmpInst(llvm::ICmpInst& i); + void visitFCmpInst(llvm::FCmpInst& i); + void visitPHINode(llvm::PHINode& i); + void visitSelectInst(llvm::SelectInst& i); + void visitCallInst(llvm::CallInst& i); + // TODO implement va_arg + // TODO landingpad + + void visitMemCpyInst(llvm::MemCpyInst& i); }; } diff --git a/include/smack/SmackModuleGenerator.h b/include/smack/SmackModuleGenerator.h index 5c7c8bbde..71943a8f3 100644 --- a/include/smack/SmackModuleGenerator.h +++ b/include/smack/SmackModuleGenerator.h @@ -24,7 +24,7 @@ namespace smack { class SmackModuleGenerator : public llvm::ModulePass { private: - Program* program; + Program program; public: static char ID; // Pass identification, replacement for typeid @@ -37,7 +37,7 @@ class SmackModuleGenerator : public llvm::ModulePass { AU.addRequired(); } - virtual bool runOnModule(llvm::Module& m) { + virtual bool runOnModule(llvm::Module& m) { SmackRep* rep = SmackRep::createRep(&getAnalysis()); generateProgram(m,rep); return false; @@ -45,7 +45,7 @@ class SmackModuleGenerator : public llvm::ModulePass { void generateProgram(llvm::Module& m, SmackRep* rep); - Program* getProgram() const { + Program& getProgram() { return program; } }; diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index 03e85b0c4..71aa90203 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -17,6 +17,7 @@ #include "llvm/Support/GraphWriter.h" #include "llvm/Support/Regex.h" #include +#include namespace smack { @@ -44,12 +45,13 @@ class SmackRep { static const string MEMCPY; static const string PTR; - static const string STATIC; static const string OBJ; static const string OFF; static const string PA; static const string FP; + + static const string TRUNC; static const string B2P; static const string I2P; @@ -116,14 +118,9 @@ class SmackRep { static const string MEM_OP; static const string REC_MEM_OP; - static const string MEM_READ; - static const string MEM_WRITE; + static const string MEM_OP_VAL; static const Expr* NUL; - - static const string BOOGIE_REC_PTR; - static const string BOOGIE_REC_OBJ; - static const string BOOGIE_REC_INT; static const string STATIC_INIT; @@ -132,14 +129,13 @@ class SmackRep { protected: static const string ARITHMETIC; - static const string AUX_PROCS; static const string MEMORY_DEBUG_SYMBOLS; llvm::AliasAnalysis* aliasAnalysis; vector memoryRegions; const llvm::DataLayout* targetData; + Program* program; vector staticInits; - vector extraDecls; unsigned uniqueFpNum; unsigned uniqueUndefNum; @@ -152,20 +148,15 @@ class SmackRep { } public: static SmackRep* createRep(llvm::AliasAnalysis* aa); + void setProgram(Program* p) { program = p; } bool isSmackName(string n); - bool isProcIgnore(string n); - bool isSmackAssert(llvm::Function* f); - bool isSmackAssume(llvm::Function* f); - bool isSmackYield(llvm::Function* f); - bool isSmackAsyncCall(llvm::Function* f); - bool isSmackRecObj(llvm::Function* f); - bool isSmackRecInt(llvm::Function* f); - bool isSmackRecPtr(llvm::Function* f); + bool isSmackGeneratedName(string n); + bool isIgnore(llvm::Function* f); bool isInt(const llvm::Type* t); bool isInt(const llvm::Value* v); bool isBool(llvm::Type* t); - bool isBool(llvm::Value* v); + bool isBool(const llvm::Value* v); bool isFloat(llvm::Type* t); bool isFloat(llvm::Value* v); string type(llvm::Type* t); @@ -178,6 +169,7 @@ class SmackRep { string memReg(unsigned i); const Expr* mem(const llvm::Value* v); + const Expr* mem(unsigned region, const Expr* addr); // const Expr* ptr(const Expr* obj, const Expr* off); // const Expr* obj(const Expr* e); // const Expr* off(const Expr* e); @@ -192,9 +184,9 @@ class SmackRep { const Expr* si2fp(const Expr* e); const Expr* ui2fp(const Expr* e); - const Expr* pa(const Expr* e, int x, int y); - const Expr* pa(const Expr* e, const Expr* x, int y); - const Expr* pa(const Expr* e, const Expr* x, const Expr* y); + const Expr* pa(const Expr* base, int index, int size); + const Expr* pa(const Expr* base, const Expr* index, int size); + const Expr* pa(const Expr* base, const Expr* index, const Expr* size); string id(const llvm::Value* v); const Expr* undef(); @@ -203,22 +195,33 @@ class SmackRep { const Expr* ptrArith(const llvm::Value* p, vector ps, vector ts); const Expr* expr(const llvm::Value* v); - const Expr* op(llvm::BinaryOperator& o); + string getString(const llvm::Value* v); + const Expr* op(const llvm::User* v); const Expr* pred(llvm::CmpInst& ci); + const Expr* arg(llvm::Function* f, unsigned pos, llvm::Value* v); + const Stmt* call(llvm::Function* f, llvm::CallInst& ci); + string code(llvm::CallInst& ci); + ProcDecl* proc(llvm::Function* f, int n); + + virtual const Expr* ptr2ref(const Expr* e) = 0; virtual const Expr* ptr2val(const Expr* e) = 0; virtual const Expr* val2ptr(const Expr* e) = 0; virtual const Expr* ref2ptr(const Expr* e) = 0; - virtual vector globalDecl(const llvm::Value* g) = 0; + virtual const Expr* trunc(const Expr* e, llvm::Type* t) = 0; + + virtual vector globalDecl(const llvm::Value* g) = 0; virtual vector getModifies(); - void addStaticInit(const llvm::Value* g); + unsigned numElements(const llvm::Constant* v); + void addInit(unsigned region, const Expr* addr, const llvm::Constant* val); bool hasStaticInits(); - Procedure* getStaticInit(); - vector getExtraDecls(); + Decl* getStaticInit(); virtual string getPtrType() = 0; virtual string getPrelude(); - + + virtual const Expr* declareIsExternal(const Expr* e) = 0; + virtual string memoryModel() = 0; virtual string mallocProc() = 0; virtual string freeProc() = 0; diff --git a/include/smack/SmackRep2dMem.h b/include/smack/SmackRep2dMem.h index 8cd76315e..4e2d10633 100644 --- a/include/smack/SmackRep2dMem.h +++ b/include/smack/SmackRep2dMem.h @@ -15,22 +15,31 @@ using llvm::SmallVector; using llvm::StringRef; using namespace std; +// NOTE: TwoDim memory model has no good (sound or precise) support for +// ptr2int and int2ptr operations. class SmackRep2dMem : public SmackRep { public: static const string PTR_TYPE; static const string REF_TYPE; static const string POINTERS; + static const string STATIC; + static const string EXTERN; public: SmackRep2dMem(llvm::AliasAnalysis* aa) : SmackRep(aa) {} - virtual vector globalDecl(const llvm::Value* g); + virtual vector globalDecl(const llvm::Value* g); virtual vector getModifies(); virtual string getPtrType(); + const Expr* ptr2ref(const Expr* e); const Expr* ptr2val(const Expr* e); const Expr* val2ptr(const Expr* e); const Expr* ref2ptr(const Expr* e); + const Expr* trunc(const Expr* e, llvm::Type* t); + + const Expr* declareIsExternal(const Expr* e); + virtual string memoryModel(); virtual string mallocProc(); virtual string freeProc(); diff --git a/include/smack/SmackRepFlatMem.h b/include/smack/SmackRepFlatMem.h index f89a64c23..12e01cb57 100644 --- a/include/smack/SmackRepFlatMem.h +++ b/include/smack/SmackRepFlatMem.h @@ -17,23 +17,30 @@ using namespace std; class SmackRepFlatMem : public SmackRep { - int globalsTop; + int bottom; public: static const string CURRADDR; + static const string BOTTOM; + static const string IS_EXT; static const string PTR_TYPE; static const string POINTERS; public: - SmackRepFlatMem(llvm::AliasAnalysis* aa) : SmackRep(aa), globalsTop(0) {} - virtual vector globalDecl(const llvm::Value* g); + SmackRepFlatMem(llvm::AliasAnalysis* aa) : SmackRep(aa), bottom(0) {} + virtual vector globalDecl(const llvm::Value* g); virtual vector getModifies(); virtual string getPtrType(); + const Expr* ptr2ref(const Expr* e); const Expr* ptr2val(const Expr* e); const Expr* val2ptr(const Expr* e); const Expr* ref2ptr(const Expr* e); - + + const Expr* trunc(const Expr* e, llvm::Type* t); + + const Expr* declareIsExternal(const Expr* e); + virtual string memoryModel(); virtual string mallocProc(); virtual string freeProc(); diff --git a/include/smack/smack.h b/include/smack/smack.h index ddcbe68ce..3056e7463 100644 --- a/include/smack/smack.h +++ b/include/smack/smack.h @@ -1,8 +1,32 @@ #ifndef SMACK_H_ #define SMACK_H_ -void __SMACK_assert(int val); -void __SMACK_assume(int val); -int __SMACK_nondet(void); +#include + +void __SMACK_code(const char *fmt, ...); +void __SMACK_decl(const char *fmt, ...); +void __SMACK_top_decl(const char *fmt, ...); + +void __SMACK_assert(bool v) { + __SMACK_code("assert {@} != 0;", v); +} + +void __SMACK_assume(bool v) { + __SMACK_code("assume {@} != 0;", v); +} + +//// PROBLEM: in the 2D memory model, the declaration of boogie_si_record_int +//// should have a type $ptr parameter, not an int. How should we do this? +// void __SMACK_record_int(int i) { +// __SMACK_top_decl("procedure boogie_si_record_int(i:int);"); +// __SMACK_code("call boogie_si_record_int(@);", i); +// } + +int __SMACK_nondet() { + static int XXX; + int x = XXX; + __SMACK_code("havoc @;", x); + return x; +} #endif /*SMACK_H_*/ diff --git a/lib/AssistDS/DataStructureCallGraph.cpp b/lib/AssistDS/DataStructureCallGraph.cpp index 205e631f0..adddd1f99 100644 --- a/lib/AssistDS/DataStructureCallGraph.cpp +++ b/lib/AssistDS/DataStructureCallGraph.cpp @@ -36,8 +36,6 @@ RegisterAnalysisGroup Y(X); } bool DataStructureCallGraph::runOnModule(Module &M) { - CallGraph::initialize(M); - ExternalCallingNode = getOrInsertFunction(0); CallsExternalNode = new CallGraphNode(0); Root = 0; diff --git a/lib/AssistDS/Makefile b/lib/AssistDS/Makefile index 2a0420794..cd90de8ad 100644 --- a/lib/AssistDS/Makefile +++ b/lib/AssistDS/Makefile @@ -9,6 +9,7 @@ LEVEL = ../.. LIBRARYNAME = AssistDS +BUILD_ARCHIVE=1 include $(LEVEL)/Makefile.common diff --git a/lib/DSA/Makefile b/lib/DSA/Makefile index 071dba776..374367297 100644 --- a/lib/DSA/Makefile +++ b/lib/DSA/Makefile @@ -9,6 +9,7 @@ LEVEL = ../.. LIBRARYNAME = LLVMDataStructure +BUILD_ARCHIVE=1 include $(LEVEL)/Makefile.common diff --git a/lib/smack/BoogieAst.cpp b/lib/smack/BoogieAst.cpp index 5c628cfdc..079cfdb78 100644 --- a/lib/smack/BoogieAst.cpp +++ b/lib/smack/BoogieAst.cpp @@ -11,6 +11,8 @@ namespace smack { using namespace std; +unsigned Decl::uniqueId = 0; + const Expr* Expr::and_(const Expr* l, const Expr* r) { return new BinExpr(BinExpr::And, l, r); } @@ -19,6 +21,10 @@ const Expr* Expr::eq(const Expr* l, const Expr* r) { return new BinExpr(BinExpr::Eq, l, r); } +const Expr* Expr::lt(const Expr* l, const Expr* r) { + return new BinExpr(BinExpr::Lt, l, r); +} + const Expr* Expr::fn(string f, const Expr* x) { return new FunExpr(f, vector(1, x)); } @@ -217,23 +223,37 @@ const Stmt* Stmt::skip() { return new AssumeStmt(Expr::lit(true)); } -const Decl* Decl::typee(string name, string type) { +const Stmt* Stmt::code(string s) { + return new CodeStmt(s); +} + +Decl* Decl::typee(string name, string type) { return new TypeDecl(name,type); } -const Decl* Decl::axiom(const Expr* e) { +Decl* Decl::axiom(const Expr* e) { return new AxiomDecl(e); } -const Decl* Decl::constant(string name, string type) { - return Decl::constant(name, type, false); +Decl* Decl::constant(string name, string type) { + return Decl::constant(name, type, vector(), false); +} +Decl* Decl::constant(string name, string type, bool unique) { + return Decl::constant(name, type, vector(), unique); } -const Decl* Decl::constant(string name, string type, bool unique) { - return new ConstDecl(name, type, unique); +Decl* Decl::constant(string name, string type, vector ax, bool unique) { + return new ConstDecl(name, type, ax, unique); } -const Decl* Decl::variable(string name, string type) { +Decl* Decl::variable(string name, string type) { return new VarDecl(name, type); } -const Decl* Decl::procedure(string name, string arg, string type) { - return new ProcDecl(name,vector< pair >(1,make_pair(arg,type)),""); +Decl* Decl::procedure(Program& p, string name) { + return procedure(p,name,vector< pair >(),vector< pair >()); +} +Decl* Decl::procedure(Program& p, string name, + vector< pair > args, vector< pair > rets) { + return new ProcDecl(p,name,args,rets); +} +Decl* Decl::code(string s) { + return new CodeDecl(s); } ostream& operator<<(ostream& os, const Expr& e) { @@ -260,15 +280,11 @@ ostream& operator<<(ostream& os, const Block* b) { b->print(os); return os; } -ostream& operator<<(ostream& os, const Decl* d) { +ostream& operator<<(ostream& os, Decl* d) { d->print(os); return os; } -ostream& operator<<(ostream& os, const Procedure* p) { - p->print(os); - return os; -} -ostream& operator<<(ostream& os, const Program* p) { +ostream& operator<<(ostream& os, Program* p) { if (p == 0) { os << " Program!\n"; } else { @@ -276,7 +292,7 @@ ostream& operator<<(ostream& os, const Program* p) { } return os; } -ostream& operator<<(ostream& os, const Program& p) { +ostream& operator<<(ostream& os, Program& p) { p.print(os); return os; } @@ -295,6 +311,20 @@ template void print_seq(ostream& os, vector ts, string sep) { template void print_seq(ostream& os, vector ts) { print_seq(os, ts, "", "", ""); } +template void print_set(ostream& os, set ts, + string init, string sep, string term) { + + os << init; + for (typename set::iterator i = ts.begin(); i != ts.end(); ++i) + os << (i == ts.begin() ? "" : sep) << *i; + os << term; +} +template void print_set(ostream& os, set ts, string sep) { + print_set(os, ts, "", sep, ""); +} +template void print_set(ostream& os, set ts) { + print_set(os, ts, "", "", ""); +} void BinExpr::print(ostream& os) const { os << "(" << lhs << " "; @@ -483,24 +513,38 @@ void ReturnStmt::print(ostream& os) const { os << "return;"; } +void CodeStmt::print(ostream& os) const { + os << code; +} + void TypeDecl::print(ostream& os) const { - if (type != "") - os << "type " << name << " = " << type << ";"; - else - os << "type " << name << ";"; + os << "type "; + if (attrs.size() > 0) + print_seq(os, attrs, "", " ", " "); + os << name; + if (alias != "") + os << " = " << alias << ";"; + os << ";"; } void AxiomDecl::print(ostream& os) const { - os << "axiom " << expr << ";"; + os << "axiom "; + if (attrs.size() > 0) + print_seq(os, attrs, "", " ", " "); + os << expr << ";"; } void ConstDecl::print(ostream& os) const { - os << "const " << (unique ? "unique " : "") - << name << ": " << type << ";"; + os << "const "; + if (attrs.size() > 0) + print_seq(os, attrs, "", " ", " "); + os << (unique ? "unique " : "") << name << ": " << type << ";"; } void FuncDecl::print(ostream& os) const { os << "function " << name; + if (attrs.size() > 0) + print_seq(os, attrs, "", " ", " "); for (unsigned i = 0; i < params.size(); i++) os << params[i].first << ": " << params[i].second << (i < params.size() - 1 ? ", " : ""); @@ -508,39 +552,27 @@ void FuncDecl::print(ostream& os) const { } void VarDecl::print(ostream& os) const { + if (attrs.size() > 0) + print_seq(os, attrs, "", " ", " "); os << "var " << name << ": " << type << ";"; } void ProcDecl::print(ostream& os) const { - os << "procedure " << name << "("; + os << "procedure "; + if (attrs.size() > 0) + print_seq(os, attrs, "", " ", " "); + os << name << "("; for (unsigned i = 0; i < params.size(); i++) os << params[i].first << ": " << params[i].second << (i < params.size() - 1 ? ", " : ""); os << ")"; - if (type != "") - os << " returns (" << type << ")"; - os << ";"; -} - -void Block::print(ostream& os) const { - if (name != "") - os << name << ":" << endl; - print_seq(os, stmts, " ", "\n ", ""); -} - -void Procedure::print(ostream& os) const { - os << "procedure " << name << "("; - for (unsigned i = 0; i < params.size(); i++) - os << params[i].first << ": " << params[i].second - << (i < params.size() - 1 ? ", " : ""); - os << ") "; if (rets.size() > 0) { os << endl; os << " returns ("; for (unsigned i = 0; i < rets.size(); i++) os << rets[i].first << ": " << rets[i].second << (i < rets.size() - 1 ? ", " : ""); - os << ") "; + os << ")"; } if (blocks.size() == 0) os << ";"; @@ -548,26 +580,40 @@ void Procedure::print(ostream& os) const { if (mods.size() > 0) { os << endl; print_seq(os, mods, " modifies ", ", ", ";"); + } + if (requires.size() > 0) { + os << endl; + print_seq(os, requires, " requires ", ";\n requires ", ";"); + } + if (ensures.size() > 0) { os << endl; + print_seq(os, ensures, " ensures ", ";\n ensures ", ";"); } if (blocks.size() > 0) { + os << endl; os << "{" << endl; if (decls.size() > 0) - print_seq(os, decls, " ", "\n ", "\n"); + print_set(os, decls, " ", "\n ", "\n"); print_seq(os, blocks, "\n"); os << endl << "}"; } - os << endl; +} + +void CodeDecl::print(ostream& os) const { + os << name; +} + +void Block::print(ostream& os) const { + if (name != "") + os << name << ":" << endl; + print_seq(os, stmts, " ", "\n ", ""); } void Program::print(ostream& os) const { - os << "// SMACK-PRELUDE-BEGIN" << endl; os << prelude; - os << "// SMACK-PRELUDE-END" << endl; os << "// BEGIN SMACK-GENERATED CODE" << endl; - print_seq(os, decls, "\n"); - os << endl << endl; - print_seq(os, procs, "\n"); + print_set(os, decls, "\n"); + os << endl; os << "// END SMACK-GENERATED CODE" << endl; } } diff --git a/lib/smack/BplFilePrinter.cpp b/lib/smack/BplFilePrinter.cpp new file mode 100644 index 000000000..575eda631 --- /dev/null +++ b/lib/smack/BplFilePrinter.cpp @@ -0,0 +1,28 @@ +// +// Copyright (c) 2008 Zvonimir Rakamaric (zvonimir@cs.utah.edu), +// Pantazis Deligiannis (p.deligiannis@imperial.ac.uk) +// This file is distributed under the MIT License. See LICENSE for details. +// +#include "smack/BplFilePrinter.h" +#include "llvm/Support/Debug.h" +#include "llvm/Support/GraphWriter.h" +#include + +namespace smack { + +using llvm::errs; +using namespace std; + +char BplFilePrinter::ID = 0; + +bool BplFilePrinter::runOnModule(llvm::Module& m) { + SmackModuleGenerator& smackGenerator = getAnalysis(); + Program& program = smackGenerator.getProgram(); + ostringstream s; + program.print(s); + out << s.str(); + DEBUG_WITH_TYPE("bpl", errs() << "" << s.str()); + return false; +} +} + diff --git a/lib/smack/BplPrinter.cpp b/lib/smack/BplPrinter.cpp index 0578ded15..c6f79591e 100644 --- a/lib/smack/BplPrinter.cpp +++ b/lib/smack/BplPrinter.cpp @@ -17,9 +17,9 @@ char BplPrinter::ID = 0; bool BplPrinter::runOnModule(llvm::Module& m) { SmackModuleGenerator& smackGenerator = getAnalysis(); - Program* program = smackGenerator.getProgram(); + Program& program = smackGenerator.getProgram(); ostringstream s; - program->print(s); + program.print(s); DEBUG_WITH_TYPE("bpl", errs() << "" << s.str()); return false; } diff --git a/lib/smack/DSAAliasAnalysis.cpp b/lib/smack/DSAAliasAnalysis.cpp index 85b032c9e..c07afd9fd 100644 --- a/lib/smack/DSAAliasAnalysis.cpp +++ b/lib/smack/DSAAliasAnalysis.cpp @@ -29,16 +29,54 @@ RegisterPass A("ds-aa", "Data Structure Graph Based Alias Anal RegisterAnalysisGroup B(A); char DSAAliasAnalysis::ID = 0; -void DSAAliasAnalysis::collectMemcpys(llvm::Module &M) { +vector DSAAliasAnalysis::collectMemcpys( + llvm::Module &M, MemcpyCollector *mcc) { + for (llvm::Module::iterator func = M.begin(), e = M.end(); func != e; ++func) { for (llvm::Function::iterator block = func->begin(); block != func->end(); ++block) { - memcpys->visit(*block); + mcc->visit(*block); + } + } + return mcc->getMemcpys(); +} + + +vector DSAAliasAnalysis::collectStaticInits(llvm::Module &M) { + vector sis; + + const llvm::EquivalenceClasses &eqs + = nodeEqs->getEquivalenceClasses(); + for (llvm::Module::const_global_iterator + g = M.global_begin(), e = M.global_end(); g != e; ++g) { + if (g->hasInitializer()) { + sis.push_back(eqs.getLeaderValue(nodeEqs->getMemberForValue(g))); } } + return sis; +} + +bool DSAAliasAnalysis::isMemcpyd(const llvm::DSNode* n) { + const llvm::EquivalenceClasses &eqs + = nodeEqs->getEquivalenceClasses(); + const llvm::DSNode* nn = eqs.getLeaderValue(n); + for (unsigned i=0; i &eqs + = nodeEqs->getEquivalenceClasses(); + const llvm::DSNode* nn = eqs.getLeaderValue(n); + for (unsigned i=0; igetMemberForValue(LocA.Ptr); const DSNode *N2 = nodeEqs->getMemberForValue(LocB.Ptr); - if (N1->isCompleteNode() || N2->isCompleteNode()) { + if ((N1->isCompleteNode() || N2->isCompleteNode()) && + !(N1->isExternalNode() && N2->isExternalNode())) { if (!equivNodes(N1,N2)) return NoAlias; - if (!memcpys->has(N1) && !memcpys->has(N2) && disjoint(&LocA,&LocB)) + if (!isMemcpyd(N1) && !isMemcpyd(N2) + && !isStaticInitd(N1) && !isStaticInitd(N2) + && disjoint(&LocA,&LocB)) return NoAlias; } diff --git a/lib/smack/Makefile b/lib/smack/Makefile index 97f98afae..cdddc76b7 100644 --- a/lib/smack/Makefile +++ b/lib/smack/Makefile @@ -9,9 +9,7 @@ LEVEL=../.. # Give the name of a library. This will build a dynamic version. # LIBRARYNAME=smack -LOADABLE_MODULE=1 BUILD_ARCHIVE=1 -SHARED_LIBRARY=1 USEDLIBS = LLVMDataStructure.a AssistDS.a # diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index bb0bc21c5..fbea397e1 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -11,6 +11,8 @@ #include "llvm/Support/GraphWriter.h" #include +#include + namespace smack { using llvm::errs; @@ -35,8 +37,8 @@ string i2s(llvm::Instruction& i) { Block* SmackInstGenerator::createBlock() { stringstream s; s << SmackRep::BLOCK_LBL << blockNum++; - Block* b = new Block(s.str()); - currProc.addBlock(b); + Block* b = new Block(proc, s.str()); + proc.addBlock(b); return b; } @@ -44,23 +46,21 @@ string SmackInstGenerator::createVar() { stringstream s; s << "$x" << varNum++; string name = s.str(); - currProc.addDecl(new VarDecl(name, rep->getPtrType())); + proc.addDecl(Decl::variable(name, rep.getPtrType())); return name; } void SmackInstGenerator::nameInstruction(llvm::Instruction& inst) { if (!inst.getType()->isVoidTy()) { - if (!inst.hasName()) { - if (rep->isBool(&inst)) + if (!inst.hasName() || !rep.isSmackGeneratedName(inst.getName())) { + if (rep.isBool(&inst)) inst.setName(SmackRep::BOOL_VAR); - else if (rep->isFloat(&inst)) + else if (rep.isFloat(&inst)) inst.setName(SmackRep::FLOAT_VAR); else inst.setName(SmackRep::PTR_VAR); } - VarDecl* d = new VarDecl(rep->id(&inst), rep->type(&inst)); - if (!currProc.hasDecl(d)) - currProc.addDecl(d); + proc.addDecl(Decl::variable(rep.id(&inst), rep.type(&inst))); } } @@ -91,16 +91,6 @@ void SmackInstGenerator::visitInstruction(llvm::Instruction& inst) { assert(false && "Instruction not handled"); } -void SmackInstGenerator::visitAllocaInst(llvm::AllocaInst& ai) { - processInstruction(ai); - unsigned typeSize = rep->storageSize(ai.getAllocatedType()); - llvm::Value* arraySize = ai.getArraySize(); - currBlock->addStmt(Stmt::call( - SmackRep::ALLOCA, - Expr::fn(SmackRep::MUL, rep->lit(typeSize), rep->lit(arraySize)), - rep->id(&ai))); -} - void SmackInstGenerator::generatePhiAssigns(llvm::TerminatorInst& ti) { llvm::BasicBlock* block = ti.getParent(); for (unsigned i = 0; i < ti.getNumSuccessors(); i++) { @@ -116,7 +106,7 @@ void SmackInstGenerator::generatePhiAssigns(llvm::TerminatorInst& ti) { nameInstruction(*phi); currBlock->addStmt(Stmt::assign( - rep->expr(phi), rep->expr(v))); + rep.expr(phi), rep.expr(v))); } } } @@ -145,6 +135,20 @@ void SmackInstGenerator::generateGotoStmts( currBlock->addStmt(Stmt::goto_(targets[0].second)); } +/******************************************************************************/ +/* TERMINATOR INSTRUCTIONS */ +/******************************************************************************/ + +void SmackInstGenerator::visitReturnInst(llvm::ReturnInst& ri) { + processInstruction(ri); + + if (llvm::Value* v = ri.getReturnValue()) + currBlock->addStmt(Stmt::assign( + Expr::id(SmackRep::RET_VAR), rep.expr(v))); + + currBlock->addStmt(Stmt::return_()); +} + void SmackInstGenerator::visitBranchInst(llvm::BranchInst& bi) { processInstruction(bi); @@ -165,7 +169,7 @@ void SmackInstGenerator::visitBranchInst(llvm::BranchInst& bi) { assert(blockMap.count(bi.getSuccessor(0)) != 0); assert(blockMap.count(bi.getSuccessor(1)) != 0); - const Expr* e = rep->expr(bi.getCondition()); + const Expr* e = rep.expr(bi.getCondition()); targets.push_back(make_pair(e, blockMap[bi.getSuccessor(0)]->getName())); targets.push_back(make_pair(Expr::not_(e), @@ -181,14 +185,14 @@ void SmackInstGenerator::visitSwitchInst(llvm::SwitchInst& si) { // Collect the list of tarets vector > targets; - const Expr* e = rep->expr(si.getCondition()); + const Expr* e = rep.expr(si.getCondition()); const Expr* n = Expr::lit(true); for (llvm::SwitchInst::CaseIt i = si.case_begin(); i != si.case_begin(); ++i) { assert(blockMap.count(i.getCaseSuccessor()) != 0); - const Expr* v = rep->expr(i.getCaseValue()); + const Expr* v = rep.expr(i.getCaseValue()); targets.push_back(make_pair(Expr::eq(e, v), blockMap[i.getCaseSuccessor()]->getName())); @@ -205,328 +209,87 @@ void SmackInstGenerator::visitSwitchInst(llvm::SwitchInst& si) { generateGotoStmts(si, targets); } -void SmackInstGenerator::visitPHINode(llvm::PHINode& phi) { - // NOTE: this is really a No-Op, since assignments to the phi nodes - // are handled in the translation of branch/switch instructions. - processInstruction(phi); -} - -void SmackInstGenerator::visitTruncInst(llvm::TruncInst& ti) { - processInstruction(ti); - WARN("ignoring trunc instruction : " + i2s(ti)); - const Expr* res = rep->expr(ti.getOperand(0)); - if (rep->isBool(&ti)) - res = rep->i2b(res); - currBlock->addStmt(Stmt::assign(rep->expr(&ti), res)); -} - void SmackInstGenerator::visitUnreachableInst(llvm::UnreachableInst& ii) { processInstruction(ii); currBlock->addStmt(Stmt::assume(Expr::lit(false))); } -// TODO Should we put this DEBUG info back in ? -// void SmackInstGenerator::processIndirectCall(CallInst& ci) { -// DEBUG(errs() << "Called value: " << *calledValue << "\n"); -// DEBUG(errs() << "Called value type: " << *calledValueType << "\n"); -// DEBUG(errs() << "Called function type: " << *calledFuncType << "\n"); - - -// TODO When will we revive the DSA code ? -// #ifdef USE_DSA -// CallSite callSite = CallSite::get(&ci); -// if (ci.getCalledFunction() != NULL) { -// Function* calledFunction = ci.getCalledFunction(); -// module->addCalledProcedure(calledFunction->getNameStr()); -// CalledFunction* calledFunc = stmt->addCalledFunction(calledFunction); -// -// if ((Common::memoryType == DSA_INDEXED || Common::memoryType == DSA_SPLIT) && -// tdDataStructures->hasDSGraph(*calledFunction)) { -// generateMemoryPairings(callSite, calledFunction, calledFunc); -// } -// } else { -// for (vector::iterator i = callTargetFinder->begin(callSite), -// ei = callTargetFinder->end(callSite); i != ei; ++i) { -// const Function* calledFunction = *i; -// module->addCalledProcedure(calledFunction->getNameStr()); -// if (ci.getCalledValue()->getType() == calledFunction->getType()) { -// CalledFunction* calledFunc = stmt->addCalledFunction(calledFunction); -// -// if ((Common::memoryType == DSA_INDEXED || Common::memoryType == DSA_SPLIT) && -// tdDataStructures->hasDSGraph(*calledFunction)) { -// generateMemoryPairings(callSite, calledFunction, calledFunc); -// } -// } -// } -// } -// #endif -// } - -// TODO Does this function belong here, or in "SmackRep" ? -const Stmt* SmackInstGenerator::generateCall( - llvm::Function* f, vector args, vector rets) { - - string name = rep->id(f); - - if (rep->isSmackAssert(f)) { - assert(args.size() == 1 && rets.size() == 0); - return Stmt::assert_( - Expr::neq(args[0], rep->val2ptr(rep->lit((unsigned) 0)))); - - } else if (rep->isSmackAssume(f)) { - assert(args.size() == 1 && rets.size() == 0); - return Stmt::assume( - Expr::neq(args[0], rep->val2ptr(rep->lit((unsigned) 0)))); - - } else if (rep->isSmackYield(f)) { - assert(rets.size() == 0); - return Stmt::assume(Expr::lit(true), Attr::attr("yield",args)); - - } else if (rep->isSmackAsyncCall(f)) { - assert(args.size() > 0); - string name = ((const VarExpr*) args[0])->name(); - args.erase(args.begin()); - return Stmt::call(name, args, rets, Attr::attr("async")); - - } else if (rep->isSmackRecInt(f)) { - assert(args.size() == 1 && rets.size() == 0); - return Stmt::call(SmackRep::BOOGIE_REC_INT, rep->ptr2val(args[0])); -// -// } else if (rep->isSmackRecObj(f)) { -// assert (args.size() == 1 && rets.size() == 0); -// return Stmt::call(SmackRep::BOOGIE_REC_OBJ, rep->obj(args[0])); -// -// } else if (rep->isSmackRecPtr(f)) { -// assert (args.size() == 1 && rets.size() == 0); -// return Stmt::call(SmackRep::BOOGIE_REC_PTR, args[0]); - - } else if (name == "malloc") { - assert(args.size() == 1); - return Stmt::call(SmackRep::MALLOC, rep->ptr2val(args[0]), rets[0]); - - } else if (name == "free") { - assert(args.size() == 1); - return Stmt::call(SmackRep::FREE, args[0]); +/******************************************************************************/ +/* BINARY OPERATIONS */ +/******************************************************************************/ - } else if (f->isVarArg() && args.size() > 0) { - - // Handle variable argument functions - missingDecls.insert(make_pair(f, args.size())); - stringstream ss; - ss << name << "#" << args.size(); - return Stmt::call(ss.str(), args, rets); - - } else if (f->isDeclaration() && !rep->isSmackName(name)) { - - // Handle functions without bodies (just declarations) - missingDecls.insert(make_pair(f, args.size())); - return Stmt::call(name, args, rets); - - } else { - return Stmt::call(name, args, rets); - } +void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator& bo) { + processInstruction(bo); + currBlock->addStmt(Stmt::assign(rep.expr(&bo), rep.op(&bo))); } -void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { - processInstruction(ci); - - if (ci.isInlineAsm()) { - WARN("unsoundly ignoring inline asm call."); - currBlock->addStmt(Stmt::skip()); - return; - - } else if (llvm::Function* f = ci.getCalledFunction()) { - if (rep->id(f).find("llvm.dbg.") != string::npos) { - // a "skip" statement.. - WARN("ignoring llvm.debug call."); - currBlock->addStmt(Stmt::skip()); - return; - } - } - - vector args; - for (unsigned i = 0; i < ci.getNumOperands() - 1; i++) { - const Expr* arg = rep->expr(ci.getOperand(i)); - if (llvm::Function* f = ci.getCalledFunction()) - if (f->isVarArg() && rep->isFloat(ci.getOperand(i))) - arg = rep->fp2si(arg); - args.push_back(arg); - } - - vector rets; - if (!ci.getType()->isVoidTy()) - rets.push_back(rep->id(&ci)); +/******************************************************************************/ +/* VECTOR OPERATIONS */ +/******************************************************************************/ - if (llvm::Function* f = ci.getCalledFunction()) { - currBlock->addStmt(generateCall(f, args, rets)); +// TODO implement vector operations - } else { - // function pointer call... - vector fs; +/******************************************************************************/ +/* AGGREGATE OPERATIONS */ +/******************************************************************************/ - llvm::Value* c = ci.getCalledValue(); - DEBUG(errs() << "Called value: " << *c << "\n"); +// TODO implement aggregate operations - // special case that happens when some clang warnings are reported - // we can find out the called function exactly - if (llvm::ConstantExpr* ce = llvm::dyn_cast(c)) { - if (ce->isCast()) { - llvm::Value* castValue = ce->getOperand(0); - if (llvm::Function* castFunc = llvm::dyn_cast(castValue)) { - currBlock->addStmt(generateCall(castFunc, args, rets)); - return; - } - } - } +/******************************************************************************/ +/* MEMORY ACCESS AND ADDRESSING OPERATIONS */ +/******************************************************************************/ - // Collect the list of possible function calls - llvm::Type* t = c->getType(); - DEBUG(errs() << "Called value type: " << *t << "\n"); - assert(t->isPointerTy() && "Indirect call value type must be pointer"); - t = t->getPointerElementType(); - DEBUG(errs() << "Called function type: " << *t << "\n"); - - llvm::Module* m = ci.getParent()->getParent()->getParent(); - for (llvm::Module::iterator f = m->begin(), e = m->end(); f != e; ++f) - if (f->getFunctionType() == t) - fs.push_back(f); - - if (fs.size() == 1) { - // Q: is this case really possible? - currBlock->addStmt(generateCall(fs[0], args, rets)); - - } else if (fs.size() > 1) { - Block* tail = createBlock(); - vector targets; - - // Create a sequence of dispatch blocks, one for each call. - for (unsigned i = 0; i < fs.size(); i++) { - Block* disp = createBlock(); - targets.push_back(disp->getName()); - - disp->addStmt(Stmt::assume( - Expr::eq(rep->expr(c), rep->expr(fs[i])))); - disp->addStmt(generateCall(fs[i], args, rets)); - disp->addStmt(Stmt::goto_(tail->getName())); - } - - // Jump to the dispatch blocks. - currBlock->addStmt(Stmt::goto_(targets)); - - // Update the current block for subsequent visits. - currBlock = tail; - - } else { - // In the worst case, we have no idea what function may have - // been called... - WARN("unsoundly ignoring indeterminate call."); - currBlock->addStmt(Stmt::skip()); - } - } -} - -void SmackInstGenerator::visitReturnInst(llvm::ReturnInst& ri) { - processInstruction(ri); - - if (llvm::Value* v = ri.getReturnValue()) - currBlock->addStmt(Stmt::assign( - Expr::id(SmackRep::RET_VAR), rep->expr(v))); - - currBlock->addStmt(Stmt::return_()); +void SmackInstGenerator::visitAllocaInst(llvm::AllocaInst& ai) { + processInstruction(ai); + unsigned typeSize = rep.storageSize(ai.getAllocatedType()); + llvm::Value* arraySize = ai.getArraySize(); + currBlock->addStmt(Stmt::call( + SmackRep::ALLOCA, + Expr::fn(SmackRep::MUL, rep.lit(typeSize), rep.lit(arraySize)), + rep.id(&ai))); } void SmackInstGenerator::visitLoadInst(llvm::LoadInst& li) { processInstruction(li); - const Expr* src = rep->mem(li.getPointerOperand()); - if (rep->isFloat(&li)) - src = rep->si2fp(src); - currBlock->addStmt(Stmt::assign(rep->expr(&li),src)); + const Expr* src = rep.mem(li.getPointerOperand()); + if (rep.isFloat(&li)) + src = rep.si2fp(src); + currBlock->addStmt(Stmt::assign(rep.expr(&li),src)); if (SmackOptions::MemoryModelDebug) { - currBlock->addStmt(Stmt::call(SmackRep::REC_MEM_OP, Expr::id(SmackRep::MEM_READ))); - currBlock->addStmt(Stmt::call(SmackRep::BOOGIE_REC_INT, rep->expr(li.getPointerOperand()))); - currBlock->addStmt(Stmt::call(SmackRep::BOOGIE_REC_INT, rep->expr(&li))); + currBlock->addStmt(Stmt::call(SmackRep::REC_MEM_OP, Expr::id(SmackRep::MEM_OP_VAL))); + currBlock->addStmt(Stmt::call("boogie_si_record_int", Expr::lit(0))); + currBlock->addStmt(Stmt::call("boogie_si_record_int", rep.expr(li.getPointerOperand()))); + currBlock->addStmt(Stmt::call("boogie_si_record_int", rep.expr(&li))); } } void SmackInstGenerator::visitStoreInst(llvm::StoreInst& si) { processInstruction(si); - const Expr* src = rep->expr(si.getOperand(0)); - if (rep->isFloat(si.getOperand(0))) - src = rep->fp2si(src); - currBlock->addStmt(Stmt::assign(rep->mem(si.getPointerOperand()),src)); + const Expr* src = rep.expr(si.getOperand(0)); + if (rep.isFloat(si.getOperand(0))) + src = rep.fp2si(src); + currBlock->addStmt(Stmt::assign(rep.mem(si.getPointerOperand()),src)); if (SmackOptions::MemoryModelDebug) { - currBlock->addStmt(Stmt::call(SmackRep::REC_MEM_OP, Expr::id(SmackRep::MEM_WRITE))); - currBlock->addStmt(Stmt::call(SmackRep::BOOGIE_REC_INT, rep->expr(si.getPointerOperand()))); - currBlock->addStmt(Stmt::call(SmackRep::BOOGIE_REC_INT, rep->expr(si.getOperand(0)))); + currBlock->addStmt(Stmt::call(SmackRep::REC_MEM_OP, Expr::id(SmackRep::MEM_OP_VAL))); + currBlock->addStmt(Stmt::call("boogie_si_record_int", Expr::lit(1))); + currBlock->addStmt(Stmt::call("boogie_si_record_int", rep.expr(si.getPointerOperand()))); + currBlock->addStmt(Stmt::call("boogie_si_record_int", rep.expr(si.getOperand(0)))); } } -void SmackInstGenerator::visitGetElementPtrInst(llvm::GetElementPtrInst& gepi) { - processInstruction(gepi); - - vector ps; - vector ts; - llvm::gep_type_iterator typeI = gep_type_begin(gepi); - for (unsigned i = 1; i < gepi.getNumOperands(); i++, ++typeI) { - ps.push_back(gepi.getOperand(i)); - ts.push_back(*typeI); - } - currBlock->addStmt(Stmt::assign(rep->expr(&gepi), - rep->ptrArith(gepi.getPointerOperand(), ps, ts))); -} - -void SmackInstGenerator::visitICmpInst(llvm::ICmpInst& ci) { - processInstruction(ci); - currBlock->addStmt(Stmt::assign(rep->expr(&ci), rep->pred(ci))); -} - -void SmackInstGenerator::visitFCmpInst(llvm::FCmpInst& ci) { - processInstruction(ci); - WARN("floating point?!?!"); - currBlock->addStmt(Stmt::assign(rep->expr(&ci), rep->pred(ci))); -} - -void SmackInstGenerator::visitZExtInst(llvm::ZExtInst& ci) { - processInstruction(ci); - - const Expr* e = rep->expr(ci.getOperand(0)); - if (rep->isBool(ci.getSrcTy())) e = rep->b2p(e); - currBlock->addStmt(Stmt::assign(rep->expr(&ci), e)); -} - -void SmackInstGenerator::visitSExtInst(llvm::SExtInst& ci) { - processInstruction(ci); - - const Expr* e = rep->expr(ci.getOperand(0)); - if (rep->isBool(ci.getSrcTy())) e = rep->b2p(e); - currBlock->addStmt(Stmt::assign(rep->expr(&ci), e)); -} - -void SmackInstGenerator::visitBitCastInst(llvm::BitCastInst& ci) { - processInstruction(ci); - WARN("ignoring bitcast instruction : " + i2s(ci)); - currBlock->addStmt(Stmt::assign( - rep->expr(&ci), rep->expr(ci.getOperand(0)))); -} - -void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator& bo) { - processInstruction(bo); - currBlock->addStmt(Stmt::assign(rep->expr(&bo), rep->op(bo))); -} - void SmackInstGenerator::visitAtomicCmpXchgInst(llvm::AtomicCmpXchgInst& i) { processInstruction(i); string x = createVar(); const Expr - *res = rep->expr(&i), - *piv = rep->mem(i.getOperand(0)), - *cmp = rep->expr(i.getOperand(1)), - *swp = rep->expr(i.getOperand(2)); + *res = rep.expr(&i), + *piv = rep.mem(i.getOperand(0)), + *cmp = rep.expr(i.getOperand(1)), + *swp = rep.expr(i.getOperand(2)); // NOTE: could also do this with gotos, but perhaps we do not want to // spread atomic instructions across blocks (?) @@ -542,9 +305,9 @@ void SmackInstGenerator::visitAtomicCmpXchgInst(llvm::AtomicCmpXchgInst& i) { void SmackInstGenerator::visitAtomicRMWInst(llvm::AtomicRMWInst& i) { processInstruction(i); - const Expr* res = rep->expr(&i); - const Expr* mem = rep->mem(i.getPointerOperand()); - const Expr* val = rep->expr(i.getValOperand()); + const Expr* res = rep.expr(&i); + const Expr* mem = rep.mem(i.getPointerOperand()); + const Expr* val = rep.expr(i.getValOperand()); const Expr* op; switch (i.getOperation()) { @@ -590,69 +353,131 @@ void SmackInstGenerator::visitAtomicRMWInst(llvm::AtomicRMWInst& i) { currBlock->addStmt(Stmt::assign(mem,op)); } -void SmackInstGenerator::visitPtrToIntInst(llvm::PtrToIntInst& i) { - processInstruction(i); +void SmackInstGenerator::visitGetElementPtrInst(llvm::GetElementPtrInst& gepi) { + processInstruction(gepi); - // TODO review this use of p2i - currBlock->addStmt(Stmt::assign(rep->expr(&i), - rep->p2i(rep->expr(i.getOperand(0))))); + vector ps; + vector ts; + llvm::gep_type_iterator typeI = gep_type_begin(gepi); + for (unsigned i = 1; i < gepi.getNumOperands(); i++, ++typeI) { + ps.push_back(gepi.getOperand(i)); + ts.push_back(*typeI); + } + currBlock->addStmt(Stmt::assign(rep.expr(&gepi), + rep.ptrArith(gepi.getPointerOperand(), ps, ts))); } -void SmackInstGenerator::visitIntToPtrInst(llvm::IntToPtrInst& i) { - processInstruction(i); - WARN("possible loss of precision : " + i2s(i)); +/******************************************************************************/ +/* CONVERSION OPERATIONS */ +/******************************************************************************/ - // TODO review this use of i2p - currBlock->addStmt(Stmt::assign(rep->expr(&i), - rep->i2p(rep->expr(i.getOperand(0))))); +void SmackInstGenerator::visitTruncInst(llvm::TruncInst& ti) { + processInstruction(ti); + currBlock->addStmt(Stmt::assign(rep.expr(&ti), + rep.trunc(rep.expr(ti.getOperand(0)), ti.getType()))); +} + +void SmackInstGenerator::visitZExtInst(llvm::ZExtInst& ci) { + processInstruction(ci); + + const Expr* e = rep.expr(ci.getOperand(0)); + if (rep.isBool(ci.getSrcTy())) e = rep.b2p(e); + currBlock->addStmt(Stmt::assign(rep.expr(&ci), e)); +} + +void SmackInstGenerator::visitSExtInst(llvm::SExtInst& ci) { + processInstruction(ci); + + const Expr* e = rep.expr(ci.getOperand(0)); + if (rep.isBool(ci.getSrcTy())) e = rep.b2p(e); + currBlock->addStmt(Stmt::assign(rep.expr(&ci), e)); } void SmackInstGenerator::visitFPTruncInst(llvm::FPTruncInst& i) { processInstruction(i); WARN("not really handling floating point : " + i2s(i)); - currBlock->addStmt(Stmt::assign(rep->expr(&i), rep->expr(i.getOperand(0)))); + currBlock->addStmt(Stmt::assign(rep.expr(&i), rep.expr(i.getOperand(0)))); } + void SmackInstGenerator::visitFPExtInst(llvm::FPExtInst& i) { processInstruction(i); WARN("not really handling floating point : " + i2s(i)); - currBlock->addStmt(Stmt::assign(rep->expr(&i), rep->expr(i.getOperand(0)))); + currBlock->addStmt(Stmt::assign(rep.expr(&i), rep.expr(i.getOperand(0)))); +} + +void SmackInstGenerator::visitFPToUIInst(llvm::FPToUIInst& i) { + processInstruction(i); + WARN("not really handling floating point : " + i2s(i)); + currBlock->addStmt(Stmt::assign(rep.expr(&i), + rep.fp2ui(rep.expr(i.getOperand(0))))); } void SmackInstGenerator::visitFPToSIInst(llvm::FPToSIInst& i) { processInstruction(i); WARN("not really handling floating point : " + i2s(i)); - currBlock->addStmt(Stmt::assign(rep->expr(&i), - rep->fp2si(rep->expr(i.getOperand(0))))); + currBlock->addStmt(Stmt::assign(rep.expr(&i), + rep.fp2si(rep.expr(i.getOperand(0))))); } -void SmackInstGenerator::visitFPToUIInst(llvm::FPToUIInst& i) { +void SmackInstGenerator::visitUIToFPInst(llvm::UIToFPInst& i) { processInstruction(i); WARN("not really handling floating point : " + i2s(i)); - currBlock->addStmt(Stmt::assign(rep->expr(&i), - rep->fp2ui(rep->expr(i.getOperand(0))))); + currBlock->addStmt(Stmt::assign(rep.expr(&i), + rep.ui2fp(rep.expr(i.getOperand(0))))); } void SmackInstGenerator::visitSIToFPInst(llvm::SIToFPInst& i) { processInstruction(i); WARN("not really handling floating point : " + i2s(i)); - currBlock->addStmt(Stmt::assign(rep->expr(&i), - rep->si2fp(rep->expr(i.getOperand(0))))); + currBlock->addStmt(Stmt::assign(rep.expr(&i), + rep.si2fp(rep.expr(i.getOperand(0))))); } -void SmackInstGenerator::visitUIToFPInst(llvm::UIToFPInst& i) { +void SmackInstGenerator::visitPtrToIntInst(llvm::PtrToIntInst& i) { processInstruction(i); - WARN("not really handling floating point : " + i2s(i)); - currBlock->addStmt(Stmt::assign(rep->expr(&i), - rep->ui2fp(rep->expr(i.getOperand(0))))); + currBlock->addStmt(Stmt::assign(rep.expr(&i), + rep.p2i(rep.expr(i.getOperand(0))))); +} + +void SmackInstGenerator::visitIntToPtrInst(llvm::IntToPtrInst& i) { + processInstruction(i); + currBlock->addStmt(Stmt::assign(rep.expr(&i), + rep.i2p(rep.expr(i.getOperand(0))))); +} + +void SmackInstGenerator::visitBitCastInst(llvm::BitCastInst& ci) { + processInstruction(ci); + currBlock->addStmt(Stmt::assign(rep.expr(&ci), rep.expr(ci.getOperand(0)))); +} + +/******************************************************************************/ +/* OTHER OPERATIONS */ +/******************************************************************************/ + +void SmackInstGenerator::visitICmpInst(llvm::ICmpInst& ci) { + processInstruction(ci); + currBlock->addStmt(Stmt::assign(rep.expr(&ci), rep.pred(ci))); +} + +void SmackInstGenerator::visitFCmpInst(llvm::FCmpInst& ci) { + processInstruction(ci); + WARN("floating point?!?!"); + currBlock->addStmt(Stmt::assign(rep.expr(&ci), rep.pred(ci))); +} + +void SmackInstGenerator::visitPHINode(llvm::PHINode& phi) { + // NOTE: this is really a No-Op, since assignments to the phi nodes + // are handled in the translation of branch/switch instructions. + processInstruction(phi); } void SmackInstGenerator::visitSelectInst(llvm::SelectInst& i) { processInstruction(i); - string x = rep->id(&i); + string x = rep.id(&i); const Expr - *c = rep->expr(i.getOperand(0)), - *v1 = rep->expr(i.getOperand(1)), - *v2 = rep->expr(i.getOperand(2)); + *c = rep.expr(i.getOperand(0)), + *v1 = rep.expr(i.getOperand(1)), + *v2 = rep.expr(i.getOperand(2)); currBlock->addStmt(Stmt::havoc(x)); currBlock->addStmt(Stmt::assume(Expr::and_( @@ -661,17 +486,110 @@ void SmackInstGenerator::visitSelectInst(llvm::SelectInst& i) { ))); } +void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { + processInstruction(ci); + + llvm::Function* f = ci.getCalledFunction(); + + if (ci.isInlineAsm()) { + WARN("unsoundly ignoring inline asm call: " + i2s(ci)); + currBlock->addStmt(Stmt::skip()); + + } else if (f && rep.id(f).find("llvm.dbg.") != string::npos) { + WARN("ignoring llvm.debug call."); + currBlock->addStmt(Stmt::skip()); + + } else if (f && rep.id(f) == "__SMACK_code") { + currBlock->addStmt(Stmt::code(rep.code(ci))); + + } else if (f && rep.id(f) == "__SMACK_decl") { + proc.addDecl(Decl::code(rep.code(ci))); + + } else if (f && rep.id(f) == "__SMACK_top_decl") { + proc.getProg().addDecl(Decl::code(rep.code(ci))); + + } else if (f) { + currBlock->addStmt(rep.call(f, ci)); + + } else { + // function pointer call... + vector fs; + + llvm::Value* c = ci.getCalledValue(); + DEBUG(errs() << "Called value: " << *c << "\n"); + + // special case that happens when some clang warnings are reported + // we can find out the called function exactly + if (llvm::ConstantExpr* ce = llvm::dyn_cast(c)) { + if (ce->isCast()) { + llvm::Value* castValue = ce->getOperand(0); + if (llvm::Function* castFunc = llvm::dyn_cast(castValue)) { + currBlock->addStmt(rep.call(castFunc, ci)); + return; + } + } + } + + // Collect the list of possible function calls + llvm::Type* t = c->getType(); + DEBUG(errs() << "Called value type: " << *t << "\n"); + assert(t->isPointerTy() && "Indirect call value type must be pointer"); + t = t->getPointerElementType(); + DEBUG(errs() << "Called function type: " << *t << "\n"); + + llvm::Module* m = ci.getParent()->getParent()->getParent(); + for (llvm::Module::iterator f = m->begin(), e = m->end(); f != e; ++f) + if (f->getFunctionType() == t && f->hasAddressTaken()) + fs.push_back(f); + + if (fs.size() == 1) { + // Q: is this case really possible? + currBlock->addStmt(rep.call(fs[0], ci)); + + } else if (fs.size() > 1) { + Block* tail = createBlock(); + vector targets; + + // Create a sequence of dispatch blocks, one for each call. + for (unsigned i = 0; i < fs.size(); i++) { + Block* disp = createBlock(); + targets.push_back(disp->getName()); + + disp->addStmt(Stmt::assume( + Expr::eq(rep.expr(c), rep.expr(fs[i])))); + disp->addStmt(rep.call(fs[i], ci)); + disp->addStmt(Stmt::goto_(tail->getName())); + } + + // Jump to the dispatch blocks. + currBlock->addStmt(Stmt::goto_(targets)); + + // Update the current block for subsequent visits. + currBlock = tail; + + } else { + // In the worst case, we have no idea what function may have + // been called... + WARN("unsoundly ignoring indeterminate call: " + i2s(ci)); + currBlock->addStmt(Stmt::skip()); + } + } +} + +/******************************************************************************/ +/* INTRINSIC FUNCTIONS */ +/******************************************************************************/ + void SmackInstGenerator::visitMemCpyInst(llvm::MemCpyInst& mci) { processInstruction(mci); - unsigned dstReg = rep->getRegion(mci.getOperand(0)); - unsigned srcReg = rep->getRegion(mci.getOperand(1)); + unsigned dstReg = rep.getRegion(mci.getOperand(0)); + unsigned srcReg = rep.getRegion(mci.getOperand(1)); vector args; for (unsigned i = 0; i < mci.getNumOperands() - 1; i++) - args.push_back(rep->expr(mci.getOperand(i))); + args.push_back(rep.expr(mci.getOperand(i))); assert(args.size() == 5); - currBlock->addStmt(Stmt::call(rep->memcpyCall(dstReg,srcReg), args)); - moreDecls.insert(rep->memcpyProc(dstReg,srcReg)); + currBlock->addStmt(Stmt::call(rep.memcpyCall(dstReg,srcReg), args)); } -} // namespace smack +} // namespace smack diff --git a/lib/smack/SmackModuleGenerator.cpp b/lib/smack/SmackModuleGenerator.cpp index 820772d46..1bbe82a28 100644 --- a/lib/smack/SmackModuleGenerator.cpp +++ b/lib/smack/SmackModuleGenerator.cpp @@ -12,55 +12,46 @@ char SmackModuleGenerator::ID = 0; void SmackModuleGenerator::generateProgram(llvm::Module& m, SmackRep* rep) { - program = new Program(""); - + rep->setProgram( &program ); + DEBUG(errs() << "Analyzing globals...\n"); for (llvm::Module::const_global_iterator x = m.global_begin(), e = m.global_end(); x != e; ++x) - program->addDecls(rep->globalDecl(x)); + program.addDecls(rep->globalDecl(x)); if (rep->hasStaticInits()) - program->addProc(rep->getStaticInit()); - program->addDecls(rep->getExtraDecls()); + program.addDecl(rep->getStaticInit()); DEBUG(errs() << "Analyzing functions...\n"); - set > missingDecls; - set moreDecls; - for (llvm::Module::iterator func = m.begin(), e = m.end(); func != e; ++func) { - string name = rep->id(func); - - if (rep->isSmackName(name) || rep->isProcIgnore(name)) - continue; - - program->addDecls(rep->globalDecl(func)); - - if (func->isDeclaration()) + if (rep->isIgnore(func)) continue; + + if (!func->isVarArg()) + program.addDecls(rep->globalDecl(func)); - DEBUG(errs() << "Analyzing function: " << name << "\n"); + ProcDecl* proc = rep->proc(func,0); + program.addDecl(proc); - Procedure* proc = new Procedure(name); - program->addProc(proc); - - // BODY if (!func->isDeclaration() && !func->empty() && !func->getEntryBlock().empty()) { + DEBUG(errs() << "Analyzing function: " << rep->id(func) << "\n"); + map known; stack workStack; - SmackInstGenerator igen(rep, *proc, known, missingDecls, moreDecls); + SmackInstGenerator igen(*rep, (ProcDecl&) *proc, known); llvm::BasicBlock& entry = func->getEntryBlock(); workStack.push(&entry); known[&entry] = igen.createBlock(); // First execute static initializers, in the main procedure. - if (name == "main" && rep->hasStaticInits()) + if (rep->id(func) == "main" && rep->hasStaticInits()) known[&entry]->addStmt(Stmt::call(SmackRep::STATIC_INIT)); // INVARIANT: knownBlocks.CONTAINS(b) iff workStack.CONTAINS(b) @@ -85,74 +76,35 @@ void SmackModuleGenerator::generateProgram(llvm::Module& m, SmackRep* rep) { igen.setCurrBlock(known[b]); igen.visit(b); } - } - // PARAMETERS - for (llvm::Function::const_arg_iterator - arg = func->arg_begin(), e = func->arg_end(); arg != e; ++arg) { - proc->addParam(rep->id(arg), rep->type(arg->getType())); + DEBUG(errs() << "Finished analyzing function: " << rep->id(func) << "\n\n"); } - // RETURNS - if (! func->getReturnType()->isVoidTy()) - proc->addRet(SmackRep::RET_VAR, rep->type(func->getReturnType())); - // MODIFIES // ... to do below, after memory splitting is determined. - - DEBUG(errs() << "Finished analyzing function: " << name << "\n\n"); } - // Add any missing procedure declarations - // NOTE: for the moment, these correspond to VARARG procedures. - for (set >::iterator d = missingDecls.begin(); - d != missingDecls.end(); ++d) { - llvm::Function* func = d->first; - int numArgs = d->second; - - stringstream name; - name << rep->id(func); - if (func->isVarArg() && numArgs > 0) { - name << "#" << numArgs; - } - - Procedure* p = new Procedure(name.str()); - - if (func->isVarArg()) { - for (int i = 0; i < numArgs; i++) { - stringstream param; - param << "p" << i; - p->addParam(param.str(), rep->getPtrType()); - } + // MODIFIES + vector procs = program.getProcs(); + for (unsigned i=0; ihasBody()) { + procs[i]->addMods(rep->getModifies()); + } else { - int i = 0; - for (llvm::Function::const_arg_iterator - arg = func->arg_begin(), e = func->arg_end(); arg != e; ++arg, ++i) { - stringstream param; - param << "p" << i; - p->addParam(param.str(), rep->type(arg->getType())); + vector< pair > rets = procs[i]->getRets(); + for (vector< pair >::iterator r = rets.begin(); + r != rets.end(); ++r) { + + // TODO should only do this for returned POINTERS. + // procs[i]->addEnsures(rep->declareIsExternal(Expr::id(r->first))); } } - - if (! func->getReturnType()->isVoidTy()) - p->addRet(SmackRep::RET_VAR, rep->type(func->getReturnType())); - program->addProc(p); - } - - // MODIFIES - for ( vector::const_iterator p = program->pbegin(); - p != program->pend(); ++p ) { - (*p)->addMods(rep->getModifies()); } - - for (set::iterator d = moreDecls.begin(); - d != moreDecls.end(); ++d) { - program->appendPrelude(*d); - } // NOTE we must do this after instruction generation, since we would not // otherwise know how many regions to declare. - program->appendPrelude(rep->getPrelude()); + program.appendPrelude(rep->getPrelude()); } } // namespace smack diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 963d1b437..391c68acb 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -26,13 +26,14 @@ const string SmackRep::FREE = "$free"; const string SmackRep::MEMCPY = "$memcpy"; const string SmackRep::PTR = "$ptr"; -const string SmackRep::STATIC = "$static"; const string SmackRep::OBJ = "$obj"; const string SmackRep::OFF = "$off"; const string SmackRep::PA = "$pa"; const string SmackRep::FP = "$fp"; +const string SmackRep::TRUNC = "$trunc"; + const string SmackRep::B2P = "$b2p"; const string SmackRep::I2P = "$i2p"; const string SmackRep::P2I = "$p2i"; @@ -99,15 +100,10 @@ const string SmackRep::FUNO = "$funo"; // used for memory model debugging const string SmackRep::MEM_OP = "$mop"; const string SmackRep::REC_MEM_OP = "boogie_si_record_mop"; -const string SmackRep::MEM_READ = "$R"; -const string SmackRep::MEM_WRITE = "$W"; +const string SmackRep::MEM_OP_VAL = "$MOP"; const Expr* SmackRep::NUL = Expr::id(NULL_VAL); -const string SmackRep::BOOGIE_REC_PTR = "boogie_si_record_ptr"; -const string SmackRep::BOOGIE_REC_OBJ = "boogie_si_record_obj"; -const string SmackRep::BOOGIE_REC_INT = "boogie_si_record_int"; - const string SmackRep::STATIC_INIT = "$static_init"; const string SmackRep::ARITHMETIC = @@ -186,14 +182,10 @@ const string SmackRep::ARITHMETIC = "function $si2fp(i:int) returns (float);\n" "function $ui2fp(i:int) returns (float);\n" ; -const string SmackRep::AUX_PROCS = - "procedure boogie_si_record_int(i: int);\n"; - const string SmackRep::MEMORY_DEBUG_SYMBOLS = "type $mop;\n" "procedure boogie_si_record_mop(m: $mop);\n" - "const $R: $mop;\n" - "const $W: $mop;\n"; + "const $MOP: $mop;\n"; const int SmackRep::width = 0; @@ -223,14 +215,10 @@ Regex BPL_KW( "|implementation|where|returns|assume|assert|havoc|call|return|while" "|break|goto|if|else|div)$"); Regex SMACK_NAME(".*__SMACK_.*"); -Regex PROC_IGNORE("^(malloc|free|llvm\\.memcpy\\..*|llvm\\.dbg\\..*)$"); -Regex SMACK_ASSERT(".*__SMACK_assert.*"); -Regex SMACK_ASSUME(".*__SMACK_assume.*"); -Regex SMACK_YIELD(".*__SMACK_yield.*"); -Regex SMACK_ASYNC_CALL(".*__SMACK_async_call.*"); -Regex SMACK_REC_OBJ(".*__SMACK_record_obj.*"); -Regex SMACK_REC_INT(".*__SMACK_record_int.*"); -Regex SMACK_REC_PTR(".*__SMACK_record_ptr.*"); +Regex PROC_IGNORE("^(" + "malloc|free|llvm\\.memcpy\\..*|llvm\\.dbg\\..*|" + "__SMACK_code|__SMACK_decl|__SMACK_top_decl" +")$"); bool isBplKeyword(string s) { return BPL_KW.match(s); @@ -240,36 +228,12 @@ bool SmackRep::isSmackName(string n) { return SMACK_NAME.match(n); } -bool SmackRep::isProcIgnore(string n) { - return PROC_IGNORE.match(n); -} - -bool SmackRep::isSmackAssert(llvm::Function* f) { - return SMACK_ASSERT.match(id(f)); +bool SmackRep::isSmackGeneratedName(string n) { + return n.size() > 0 && n[0] == '$'; } -bool SmackRep::isSmackAssume(llvm::Function* f) { - return SMACK_ASSUME.match(id(f)); -} - -bool SmackRep::isSmackYield(llvm::Function* f) { - return SMACK_YIELD.match(id(f)); -} - -bool SmackRep::isSmackAsyncCall(llvm::Function* f) { - return SMACK_ASYNC_CALL.match(id(f)); -} - -bool SmackRep::isSmackRecObj(llvm::Function* f) { - return SMACK_REC_OBJ.match(id(f)); -} - -bool SmackRep::isSmackRecInt(llvm::Function* f) { - return SMACK_REC_INT.match(id(f)); -} - -bool SmackRep::isSmackRecPtr(llvm::Function* f) { - return SMACK_REC_PTR.match(id(f)); +bool SmackRep::isIgnore(llvm::Function* f) { + return PROC_IGNORE.match(id(f)); } bool SmackRep::isInt(const llvm::Type* t) { @@ -284,7 +248,7 @@ bool SmackRep::isBool(llvm::Type* t) { return t->isIntegerTy(1); } -bool SmackRep::isBool(llvm::Value* v) { +bool SmackRep::isBool(const llvm::Value* v) { return isBool(v->getType()); } @@ -317,14 +281,18 @@ unsigned SmackRep::fieldOffset(llvm::StructType* t, unsigned fieldNo) { return targetData->getStructLayout(t)->getElementOffset(fieldNo); } -string SmackRep::memReg(unsigned i) { +string SmackRep::memReg(unsigned idx) { stringstream s; - s << "$M." << i; + s << "$M." << idx; return s.str(); } const Expr* SmackRep::mem(const llvm::Value* v) { - return Expr::sel(Expr::id(memReg(getRegion(v))), expr(v)); + return mem( getRegion(v), expr(v) ); +} + +const Expr* SmackRep::mem(unsigned region, const Expr* addr) { + return Expr::sel( Expr::id(memReg(region)), addr ); } unsigned SmackRep::getRegion(const llvm::Value* v) { @@ -339,6 +307,8 @@ unsigned SmackRep::getRegion(const llvm::Value* v) { string SmackRep::memcpyCall(int dstReg, int srcReg) { stringstream s; s << "$memcpy." << dstReg << "." << srcReg; + + program->addDecl(memcpyProc(dstReg,srcReg)); return s.str(); } @@ -390,16 +360,16 @@ const Expr* SmackRep::ui2fp(const Expr* e) { return Expr::fn(UI2FP, e); } -const Expr* SmackRep::pa(const Expr* e, int x, int y) { - return pa(e, Expr::lit(x), Expr::lit(y)); +const Expr* SmackRep::pa(const Expr* base, int index, int size) { + return pa(base, Expr::lit(index), Expr::lit(size)); } -const Expr* SmackRep::pa(const Expr* e, const Expr* x, int y) { - return pa(e, x, Expr::lit(y)); +const Expr* SmackRep::pa(const Expr* base, const Expr* index, int size) { + return pa(base, index, Expr::lit(size)); } -const Expr* SmackRep::pa(const Expr* e, const Expr* x, const Expr* y) { - return Expr::fn(PA, e, x, y); +const Expr* SmackRep::pa(const Expr* base, const Expr* index, const Expr* size) { + return Expr::fn(PA, base, index, size); } const Expr* SmackRep::undef() { @@ -442,7 +412,7 @@ const Expr* SmackRep::lit(const llvm::Value* v) { else return Expr::lit(val, width); - } else if (const llvm::ConstantFP* cf = llvm::dyn_cast(v)) { + } else if (llvm::isa(v)) { // TODO encode floating point return Expr::fn(FP,Expr::lit((int) uniqueFpNum++)); @@ -532,6 +502,9 @@ const Expr* SmackRep::expr(const llvm::Value* v) { // TODO test this out, formerly Expr::id("$UNDEF"); return p2i(expr(constantExpr->getOperand(0))); + else if (Instruction::isBinaryOp(constantExpr->getOpcode())) + return op(constantExpr); + else { DEBUG(errs() << "VALUE : " << *v << "\n"); assert(false && "constant expression of this type not supported"); @@ -563,9 +536,29 @@ const Expr* SmackRep::expr(const llvm::Value* v) { } } -const Expr* SmackRep::op(llvm::BinaryOperator& o) { +string SmackRep::getString(const llvm::Value* v) { + if (const llvm::ConstantExpr* constantExpr = llvm::dyn_cast(v)) + if (constantExpr->getOpcode() == llvm::Instruction::GetElementPtr) + if (const llvm::GlobalValue* cc = llvm::dyn_cast(constantExpr->getOperand(0))) + if (const llvm::ConstantDataSequential* cds = llvm::dyn_cast(cc->getOperand(0))) + return cds ->getAsCString(); + return ""; +} + +const Expr* SmackRep::op(const llvm::User* v) { + using namespace llvm; + unsigned opcode; string op; - switch (o.getOpcode()) { + + if (const BinaryOperator* bo = dyn_cast(v)) + opcode = bo->getOpcode(); + + else if (const ConstantExpr* ce = dyn_cast(v)) + opcode = ce->getOpcode(); + + else assert(false && "unexpected operator value."); + + switch (opcode) { using llvm::Instruction; // Integer operations @@ -630,14 +623,14 @@ const Expr* SmackRep::op(llvm::BinaryOperator& o) { assert(false && "unexpected predicate."); } llvm::Value - *l = o.getOperand(0), - *r = o.getOperand(1); + *l = v->getOperand(0), + *r = v->getOperand(1); const Expr* e = Expr::fn(op, (isBool(l) ? b2i(expr(l)) : ptr2val(expr(l))), (isBool(r) ? b2i(expr(r)) : ptr2val(expr(r)))); - return isBool(&o) ? i2b(e) : val2ptr(e); + return isBool(v) ? i2b(e) : val2ptr(e); } const Expr* SmackRep::pred(llvm::CmpInst& ci) { @@ -738,9 +731,111 @@ const Expr* SmackRep::pred(llvm::CmpInst& ci) { return e == NULL ? Expr::fn(o, ptr2val(l), ptr2val(r)) : e; } +string indexedName(string name, int idx) { + stringstream idxd; + idxd << name << "#" << idx; + return idxd.str(); +} + +ProcDecl* SmackRep::proc(llvm::Function* f, int nargs) { + vector< pair > args, rets; + + int i = 0; + for (llvm::Function::const_arg_iterator + arg = f->arg_begin(), e = f->arg_end(); arg != e; ++arg, ++i) { + + args.push_back(make_pair( + arg->hasName() ? id(arg) : indexedName("p",i), + type(arg->getType()) )); + } + + for (; i < nargs; i++) + args.push_back(make_pair(indexedName("p",i), getPtrType())); + + if (!f->getReturnType()->isVoidTy()) + rets.push_back(make_pair(RET_VAR,type(f->getReturnType()))); + + return (ProcDecl*) Decl::procedure( + *program, + f->isVarArg() ? indexedName(id(f),nargs) : id(f), + args, + rets + ); +} + +const Expr* SmackRep::arg(llvm::Function* f, unsigned pos, llvm::Value* v) { + const Expr* arg = expr(v); + if (f && f->isVarArg() && isFloat(v)) + arg = fp2si(arg); + return arg; +} + +const Stmt* SmackRep::call(llvm::Function* f, llvm::CallInst& ci) { + + assert(f && "Call encountered unresolved function."); + + string name = id(f); + vector args; + vector rets; + + for (unsigned i = 0; i < ci.getNumOperands() - 1; i++) + args.push_back(arg(f, i, ci.getOperand(i))); + + if (!ci.getType()->isVoidTy()) + rets.push_back(id(&ci)); + + if (name == "malloc") { + assert(args.size() == 1); + return Stmt::call(MALLOC, ptr2val(args[0]), rets[0]); + + } else if (name == "free") { + assert(args.size() == 1); + return Stmt::call(FREE, args[0]); + + } else if (f->isVarArg() || (f->isDeclaration() && !isSmackName(name))) { + + Decl* p = proc(f,args.size()); + program->addDecl(p); + return Stmt::call(p->getName(), args, rets); + + } else { + return Stmt::call(name, args, rets); + } +} + +string SmackRep::code(llvm::CallInst& ci) { + + llvm::Function* f = ci.getCalledFunction(); + assert(f && "Inline code embedded in unresolved function."); + + string fmt = getString(ci.getOperand(0)); + assert(!fmt.empty() && "__SMACK_code: missing format string."); + + string s = fmt; + for (unsigned i=1; iprint(ss); + s = s.replace(idx-1,3,ss.str()); + + } else { + a->print(ss); + s = s.replace(idx,1,ss.str()); + } + } + return s; +} + string SmackRep::getPrelude() { stringstream s; - s << AUX_PROCS << endl; + s << "// SMACK-PRELUDE-BEGIN" << endl; s << ARITHMETIC << endl; if (SmackOptions::MemoryModelDebug) @@ -767,6 +862,7 @@ string SmackRep::getPrelude() { s << mallocProc() << endl; s << freeProc() << endl; s << allocaProc() << endl; + s << "// SMACK-PRELUDE-END" << endl; return s.str(); } @@ -777,32 +873,33 @@ vector SmackRep::getModifies() { return mods; } -void SmackRep::addStaticInit(const llvm::Value* v) { +unsigned SmackRep::numElements(const llvm::Constant* v) { using namespace llvm; - if (const GlobalVariable* g = dyn_cast(v)) { - - if (g->hasInitializer()) { - const Constant* init = g->getInitializer(); + if (const ArrayType* at = dyn_cast(v->getType())) + return at->getNumElements(); + else + return 1; +} - if (isInt(init)) - staticInits.push_back(Stmt::assign(mem(g),expr(init))); +void SmackRep::addInit(unsigned region, const Expr* addr, const llvm::Constant* val) { + using namespace llvm; - 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())))); - } + if (isInt(val)) { + staticInits.push_back( Stmt::assign(mem(region,addr), expr(val)) ); + + } else if (isa(val->getType())) { + staticInits.push_back( Stmt::assign(mem(region,addr), expr(val)) ); - 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))); - } - } + } else if (dyn_cast(val->getType())) { + + } else if (StructType* st = dyn_cast(val->getType())) { + for (unsigned i = 0; i < st->getNumElements(); i++) { + const Constant* elem = val->getAggregateElement(i); + addInit( region, pa(addr,fieldOffset(st,i),1), elem ); } + + } else { + assert (false && "Unexpected static initializer."); } } @@ -810,9 +907,9 @@ bool SmackRep::hasStaticInits() { return staticInits.size() > 0; } -Procedure* SmackRep::getStaticInit() { - Procedure* proc = new Procedure(STATIC_INIT); - Block* b = new Block(); +Decl* SmackRep::getStaticInit() { + ProcDecl* proc = (ProcDecl*) Decl::procedure(*program, STATIC_INIT); + Block* b = new Block(*proc); for (unsigned i=0; iaddStmt(staticInits[i]); b->addStmt(Stmt::return_()); @@ -820,9 +917,5 @@ Procedure* SmackRep::getStaticInit() { return proc; } -vector SmackRep::getExtraDecls() { - return extraDecls; -} - } // namespace smack diff --git a/lib/smack/SmackRep2dMem.cpp b/lib/smack/SmackRep2dMem.cpp index efbe1c2a3..845de5d63 100644 --- a/lib/smack/SmackRep2dMem.cpp +++ b/lib/smack/SmackRep2dMem.cpp @@ -10,17 +10,35 @@ namespace smack { const string SmackRep2dMem::PTR_TYPE = "$ptr"; const string SmackRep2dMem::REF_TYPE = "$ref"; - -vector SmackRep2dMem::globalDecl(const llvm::Value* g) { - addStaticInit(g); - - vector decls; - string name = id(g); - decls.push_back(Decl::constant(name, REF_TYPE, true)); - decls.push_back(Decl::axiom(Expr::fn(SmackRep::STATIC, Expr::id(name)))); +const string SmackRep2dMem::STATIC = "$static"; +const string SmackRep2dMem::EXTERN = "$extern"; + +vector SmackRep2dMem::globalDecl(const llvm::Value* v) { + using namespace llvm; + vector decls; + vector ax; + string name = id(v); + + if (const GlobalVariable* g = dyn_cast(v)) { + if (g->hasInitializer()) { + const llvm::Constant* init = g->getInitializer(); + unsigned numElems = numElements(init); + if (numElems > 1) + ax.push_back(Attr::attr("count",numElems)); + addInit(getRegion(g), expr(g), init); + } else { + decls.push_back(Decl::axiom(declareIsExternal(Expr::id(name)))); + } + } + decls.push_back(Decl::constant(name, REF_TYPE, ax, true)); + decls.push_back(Decl::axiom(Expr::fn(SmackRep2dMem::STATIC, Expr::id(name)))); return decls; } +const Expr* SmackRep2dMem::declareIsExternal(const Expr* e) { + return Expr::fn(SmackRep2dMem::EXTERN, ptr2ref(e)); +} + vector SmackRep2dMem::getModifies() { vector mods = SmackRep::getModifies(); mods.push_back(ALLOC); @@ -31,6 +49,10 @@ string SmackRep2dMem::getPtrType() { return PTR_TYPE; } +const Expr* SmackRep2dMem::ptr2ref(const Expr* e) { + return Expr::fn(OBJ, e); +} + const Expr* SmackRep2dMem::ptr2val(const Expr* e) { return Expr::fn(OFF, e); } @@ -43,6 +65,14 @@ const Expr* SmackRep2dMem::ref2ptr(const Expr* e) { return Expr::fn(PTR, e, Expr::lit(0)); } +const Expr* SmackRep2dMem::trunc(const Expr* e, llvm::Type* t) { + assert(t->isIntegerTy() && "TODO: implement truncate for non-integer types."); + if (isBool(t)) + return Expr::fn("$p2b",e); + else + return Expr::fn(TRUNC,e,lit(t->getPrimitiveSizeInBits())); +} + const string SmackRep2dMem::POINTERS = "// SMACK 2D Memory Model\n" "\n" @@ -51,7 +81,7 @@ const string SmackRep2dMem::POINTERS = "\n" "function $ptr($ref, int) returns ($ptr);\n" "function $static($ref) returns (bool);\n" - "function $size($ref) returns (int);\n" + "function $extern($ref) returns (bool);\n" "function $obj($ptr) returns ($ref);\n" "function $off($ptr) returns (int);\n" "\n" @@ -66,18 +96,19 @@ const string SmackRep2dMem::POINTERS = "\n" "const unique $NULL: $ref;\n" "axiom $static($NULL);\n" + "axiom(forall r:$ref :: $static(r) ==> !$extern(r));\n" "const $UNDEF: $ptr;\n" "\n" - "function $pa(pointer: $ptr, offset: int, size: int) returns ($ptr);\n" - "function $trunc(p: $ptr) returns ($ptr);\n" + "function $pa(pointer: $ptr, index: int, size: int) returns ($ptr);\n" + "function $trunc(p: $ptr, size: int) returns ($ptr);\n" "function $p2i(p: $ptr) returns ($ptr);\n" "function $i2p(p: $ptr) returns ($ptr);\n" "function $p2b(p: $ptr) returns (bool);\n" "function $b2p(b: bool) returns ($ptr);\n" "\n" - "axiom (forall p:$ptr, o:int, s:int :: {$pa(p,o,s)} $pa(p,o,s) == $ptr($obj(p), $off(p) + o * s));\n" - "axiom (forall p:$ptr, o:int, s:int :: {$pa(p,o,s)} $obj($pa(p,o,s)) == $obj(p));\n" - "axiom (forall p:$ptr :: $trunc(p) == p);\n" + "axiom (forall p:$ptr, i:int, s:int :: {$pa(p,i,s)} $pa(p,i,s) == $ptr($obj(p), $off(p) + i * s));\n" + "axiom (forall p:$ptr, i:int, s:int :: {$pa(p,i,s)} $obj($pa(p,i,s)) == $obj(p));\n" + "axiom (forall p:$ptr, s:int :: $trunc(p,s) == p);\n" "\n" "axiom $b2p(true) == $ptr($NULL,1);\n" "axiom $b2p(false) == $ptr($NULL,0);\n" @@ -85,88 +116,71 @@ const string SmackRep2dMem::POINTERS = "axiom (forall r:$ref, i:int :: $p2b($ptr(r,i)) <==> i != 0);\n" "axiom $p2b($ptr($NULL,0)) == false;\n" "axiom (forall r:$ref, i:int :: $p2i($ptr(r,i)) == $ptr($NULL,i));\n" - "axiom (forall i:int :: (exists r:$ref :: $i2p($ptr($NULL,i)) == $ptr(r,i)));\n" - "\n" - "procedure __SMACK_nondet() returns (p: $ptr);\n" - "procedure __SMACK_nondetInt() returns (p: $ptr);\n" - "ensures $obj(p) == $NULL;\n"; + "axiom (forall i:int :: (exists r:$ref :: $i2p($ptr($NULL,i)) == $ptr(r,i)));\n"; string SmackRep2dMem::memoryModel() { return POINTERS; } string SmackRep2dMem::mallocProc() { - stringstream s; - if (SmackOptions::MemoryModelImpls) { - s << "procedure $malloc(obj_size: int) returns (new: int)" << endl; - s << " modifies $Alloc;" << endl; - s << " requires obj_size > 0;" << endl; - s << "{" << endl; - s << " assume $Alloc[$obj(new)] = $UNALLOCATED;" << endl; - s << " assume !$static($obj(new));" << endl; - s << " assume $off(new) == 0;" << endl; - s << " assume $size($obj(new)) == obj_size;" << endl; - s << " $Alloc[$obj(new)] := $ALLOCATED;" << endl; - s << "}" << endl; - } else { - s << "procedure $malloc(obj_size: int) returns (new: $ptr);" << endl; - s << "modifies $Alloc;" << endl; - s << "ensures old($Alloc)[$obj(new)] == $UNALLOCATED && $Alloc[$obj(new)] == $ALLOCATED;" << endl; - s << "ensures !$static($obj(new));" << endl; - s << "ensures $off(new) == 0;" << endl; - s << "ensures $size($obj(new)) == obj_size;" << endl; - s << "ensures (forall x_obj:$ref :: {$Alloc[x_obj]} x_obj == $obj(new) || old($Alloc)[x_obj] == $Alloc[x_obj]);" << endl; - } - return s.str(); + if (SmackOptions::MemoryModelImpls) + return + "procedure $malloc(n: int) returns (p: $ptr)\n" + "modifies $Alloc;\n" + "{\n" + " assume !$static($obj(p));\n" + " assume $Alloc[$obj(p)] == $UNALLOCATED;\n" + " assume $off(p) == 0;\n" + " $Alloc[$obj(p)] := $ALLOCATED;\n" + "}\n"; + else + return + "procedure $malloc(n: int) returns (p: $ptr);\n" + "modifies $Alloc;\n" + "ensures old($Alloc)[$obj(p)] == $UNALLOCATED;\n" + "ensures $Alloc[$obj(p)] == $ALLOCATED;\n" + "ensures !$static($obj(p));\n" + "ensures $off(p) == 0;\n" + "ensures (forall r: $ref :: {$Alloc[r]} r != $obj(p) ==> $Alloc[r] == old($Alloc)[r]);\n"; } string SmackRep2dMem::freeProc() { - stringstream s; - if (SmackOptions::MemoryModelImpls) { - s << "procedure $free(pointer: $ptr)" << endl; - s << " modifies $Alloc;" << endl; - s << " requires $ALLOC[$obj(pointer)] == $ALLOCATED;" << endl; - s << " // requires !$static($obj(pointer);" << endl; - s << " requires $off(pointer) == 0;" << endl; - s << "{" << endl; - s << " $Alloc[$obj(new)] := $UNALLOCATED;" << endl; - s << "}" << endl; - } else { - s << "procedure $free(pointer: $ptr);" << endl; - s << "modifies $Alloc;" << endl; - s << "requires $Alloc[$obj(pointer)] == $ALLOCATED;" << endl; - s << "// requires !$static($obj(pointer));" << endl; - s << "requires $off(pointer) == 0;" << endl; - s << "ensures $Alloc[$obj(pointer)] != $UNALLOCATED;" << endl; - s << "ensures (forall x:$ref :: {$Alloc[x]} $obj(pointer) == x || old($Alloc)[x] == $Alloc[x]);" << endl; - } - return s.str(); + if (SmackOptions::MemoryModelImpls) + return + "procedure $free(p: $ptr)\n" + "modifies $Alloc;\n" + "{\n" + " $Alloc[$obj(p)] := $UNALLOCATED;\n" + "}\n"; + else + return + "procedure $free(p: $ptr);\n" + "modifies $Alloc;\n" + "ensures $Alloc[$obj(p)] == $UNALLOCATED;\n" + "ensures (forall r: $ref :: {$Alloc[r]} r != $obj(p) ==> $Alloc[r] == old($Alloc)[r]);\n"; } string SmackRep2dMem::allocaProc() { - stringstream s; - if (SmackOptions::MemoryModelImpls) { - s << "procedure $alloca(obj_size: int) returns (new: $ptr)" << endl; - s << " modifies $Alloc;" << endl; - s << " requires obj_size > 0;" << endl; - s << "{" << endl; - s << " assume $Alloc[$obj(new)] = $UNALLOCATED;" << endl; - s << " assume !$static($obj(new));" << endl; - s << " assume $off(new) == 0;" << endl; - s << " assume $size($obj(new)) == obj_size;" << endl; - s << " $Alloc[$obj(new)] := $ALLOCATED;" << endl; - s << "}" << endl; - } else { - s << "procedure $alloca(obj_size: int) returns (new: $ptr);" << endl; - s << "modifies $Alloc;" << endl; - s << "ensures old($Alloc)[$obj(new)] == $UNALLOCATED && $Alloc[$obj(new)] == $ALLOCATED;" << endl; - s << "ensures !$static($obj(new));" << endl; - s << "ensures $off(new) == 0;" << endl; - s << "ensures $size($obj(new)) == obj_size;" << endl; - s << "ensures (forall x_obj:$ref :: {$Alloc[x_obj]} x_obj == $obj(new) || old($Alloc)[x_obj] == $Alloc[x_obj]);" << endl; - } - return s.str(); + if (SmackOptions::MemoryModelImpls) + return + "procedure $alloca(n: int) returns (p: $ptr)\n" + "modifies $Alloc;\n" + "{\n" + " assume !$static($obj(p));\n" + " assume $Alloc[$obj(p)] == $UNALLOCATED;\n" + " assume $off(p) == 0;\n" + " $Alloc[$obj(p)] := $ALLOCATED;\n" + "}\n"; + else + return + "procedure $alloca(n: int) returns (p: $ptr);\n" + "modifies $Alloc;\n" + "ensures old($Alloc)[$obj(p)] == $UNALLOCATED;\n" + "ensures $Alloc[$obj(p)] == $ALLOCATED;\n" + "ensures !$static($obj(p));\n" + "ensures $off(p) == 0;\n" + "ensures (forall r: $ref :: {$Alloc[r]} r != $obj(p) ==> $Alloc[r] == old($Alloc)[r]);\n"; } string SmackRep2dMem::memcpyProc(int dstReg, int srcReg) { @@ -190,4 +204,3 @@ string SmackRep2dMem::memcpyProc(int dstReg, int srcReg) { } // namespace smack - diff --git a/lib/smack/SmackRepFlatMem.cpp b/lib/smack/SmackRepFlatMem.cpp index aafe7eaf6..6618ebafa 100644 --- a/lib/smack/SmackRepFlatMem.cpp +++ b/lib/smack/SmackRepFlatMem.cpp @@ -9,42 +9,60 @@ namespace smack { const string SmackRepFlatMem::CURRADDR = "$CurrAddr"; +const string SmackRepFlatMem::BOTTOM = "$GLOBALS_BOTTOM"; +const string SmackRepFlatMem::IS_EXT = "$isExternal"; const string SmackRepFlatMem::PTR_TYPE = "int"; -vector SmackRepFlatMem::globalDecl(const llvm::Value* g) { - addStaticInit(g); - - vector decls; - string name = id(g); - decls.push_back(Decl::constant(name, getPtrType(), true)); - - unsigned size; +vector SmackRepFlatMem::globalDecl(const llvm::Value* v) { + using namespace llvm; + vector decls; + vector ax; + string name = id(v); - // NOTE: all global variables have pointer type in LLVM - if (g->getType()->isPointerTy()) { - llvm::PointerType *t = (llvm::PointerType*) g->getType(); + if (const GlobalVariable* g = dyn_cast(v)) { + if (g->hasInitializer()) { + const Constant* init = g->getInitializer(); + unsigned numElems = numElements(init); + unsigned size; + + // NOTE: all global variables have pointer type in LLVM + if (g->getType()->isPointerTy()) { + PointerType *t = (PointerType*) g->getType(); - // in case we can determine the size of the element type ... - if (t->getElementType()->isSized()) - size = storageSize(t->getElementType()); + // in case we can determine the size of the element type ... + if (t->getElementType()->isSized()) + size = storageSize(t->getElementType()); - // otherwise (e.g. for function declarations), use a default size - else - size = 1024; + // otherwise (e.g. for function declarations), use a default size + else + size = 1024; - } else - size = storageSize(g->getType()); + } else + size = storageSize(g->getType()); - globalsTop -= size; + bottom -= size; - decls.push_back(Decl::axiom( - Expr::eq(Expr::id(name), Expr::lit(globalsTop)))); - // Expr::fn("$slt", - // Expr::fn(SmackRep::ADD, Expr::id(name), Expr::lit(1024)), - // Expr::lit(globalsTop)) )); + if (numElems > 1) + ax.push_back(Attr::attr("count",numElems)); + + decls.push_back(Decl::axiom(Expr::eq(Expr::id(name),Expr::lit(bottom)))); + addInit(getRegion(g), expr(g), init); + // Expr::fn("$slt", + // Expr::fn(SmackRep::ADD, Expr::id(name), Expr::lit(1024)), + // Expr::lit(bottom)) )); + + } else { + decls.push_back(Decl::axiom(declareIsExternal(Expr::id(name)))); + } + } + decls.push_back(Decl::constant(name, getPtrType(), ax, true)); return decls; } +const Expr* SmackRepFlatMem::declareIsExternal(const Expr* e) { + return Expr::fn(IS_EXT,e); +} + vector SmackRepFlatMem::getModifies() { vector mods = SmackRep::getModifies(); mods.push_back(ALLOC); @@ -56,6 +74,10 @@ string SmackRepFlatMem::getPtrType() { return PTR_TYPE; } +const Expr* SmackRepFlatMem::ptr2ref(const Expr* e) { + return e; +} + const Expr* SmackRepFlatMem::ptr2val(const Expr* e) { return e; } @@ -67,12 +89,20 @@ const Expr* SmackRepFlatMem::val2ptr(const Expr* e) { const Expr* SmackRepFlatMem::ref2ptr(const Expr* e) { return e; } + +const Expr* SmackRepFlatMem::trunc(const Expr* e, llvm::Type* t) { + assert(t->isIntegerTy() && "TODO: implement truncate for non-integer types."); + + if (isBool(t)) + return Expr::fn(I2B,e); + else + return Expr::fn(TRUNC,e,lit(t->getPrimitiveSizeInBits())); +} const string SmackRepFlatMem::POINTERS = "// SMACK Flat Memory Model\n" "\n" "function $ptr(obj:int, off:int) returns (int) {obj + off}\n" - "function $size(int) returns (int);\n" "function $obj(int) returns (int);\n" "function $off(ptr:int) returns (int) {ptr}\n" "\n" @@ -83,103 +113,102 @@ const string SmackRepFlatMem::POINTERS = "axiom $NULL == 0;\n" "const $UNDEF: int;\n" "\n" - "function $pa(pointer: int, offset: int, size: int) returns (int);\n" - "function $trunc(p: int) returns (int);\n" + "function $pa(pointer: int, index: int, size: int) returns (int);\n" + "function $trunc(p: int, size: int) returns (int);\n" "function $p2i(p: int) returns (int);\n" "function $i2p(p: int) returns (int);\n" "function $p2b(p: int) returns (bool);\n" "function $b2p(b: bool) returns (int);\n" "\n" - "axiom (forall p:int, o:int, s:int :: {$pa(p,o,s)} $pa(p,o,s) == p + o * s);\n" - "axiom (forall p:int :: $trunc(p) == p);\n" + "axiom (forall p:int, i:int, s:int :: {$pa(p,i,s)} $pa(p,i,s) == p + i * s);\n" + "axiom (forall p,s:int :: $trunc(p,s) == p);\n" "\n" "axiom $b2p(true) == 1;\n" "axiom $b2p(false) == 0;\n" "axiom (forall i:int :: $p2b(i) <==> i != 0);\n" "axiom $p2b(0) == false;\n" "axiom (forall i:int :: $p2i(i) == i);\n" - "axiom (forall i:int :: $i2p(i) == i);\n" - "procedure __SMACK_nondet() returns (p: int);\n" - "procedure __SMACK_nondetInt() returns (p: int);\n"; + "axiom (forall i:int :: $i2p(i) == i);\n"; string SmackRepFlatMem::memoryModel() { - return POINTERS; + stringstream s; + s << POINTERS; + s << "function " << IS_EXT << "(p: int) returns (bool) { p < " << bottom - 32768 << " }" << endl; + s << "const " << BOTTOM << ": int;" << endl; + s << "axiom " << BOTTOM << " == " << bottom << ";" << endl; + return s.str(); } string SmackRepFlatMem::mallocProc() { - stringstream s; - - if (SmackOptions::MemoryModelImpls) { - s << "procedure $malloc(obj_size: int) returns (new: int)" << endl; - s << " modifies $CurrAddr, $Alloc;" << endl; - s << " requires obj_size > 0;" << endl; - s << "{" << endl; - s << " assume $CurrAddr > 0;" << endl; - s << " new := $CurrAddr;" << endl; - s << " $CurrAddr := $CurrAddr + obj_size;" << endl; - s << " $Alloc[new] := true;" << endl; - s << "}" << endl; - } else { - s << "procedure $malloc(obj_size: int) returns (new: int);" << endl; - s << "modifies $CurrAddr, $Alloc;" << endl; - s << "requires obj_size > 0;" << endl; - s << "ensures 0 < old($CurrAddr);" << endl; - s << "ensures new == old($CurrAddr);" << endl; - s << "ensures $CurrAddr > old($CurrAddr) + obj_size;" << endl; - s << "ensures $size(new) == obj_size;" << endl; - s << "ensures (forall x:int :: new <= x && x < new + obj_size ==> $obj(x) == new);" << endl; - s << "ensures $Alloc[new];" << endl; - s << "ensures (forall x:int :: {$Alloc[x]} x == new || old($Alloc)[x] == $Alloc[x]);" << endl;; - } - return s.str(); + if (SmackOptions::MemoryModelImpls) + return + "procedure $malloc(n: int) returns (p: int)\n" + "modifies $CurrAddr, $Alloc;\n" + "{\n" + " assume $CurrAddr > 0;\n" + " p := $CurrAddr;\n" + " if (n > 0) {\n" + " $CurrAddr := $CurrAddr + n;\n" + " } else {\n" + " $CurrAddr := $CurrAddr + 1;\n" + " }\n" + " $Alloc[p] := true;\n" + "}\n"; + else + return + "procedure $malloc(n: int) returns (p: int);\n" + "modifies $CurrAddr, $Alloc;\n" + "ensures p > 0;\n" + "ensures p == old($CurrAddr);\n" + "ensures $CurrAddr > old($CurrAddr);\n" + "ensures n >= 0 ==> $CurrAddr >= old($CurrAddr) + n;\n" + "ensures $Alloc[p];\n" + "ensures (forall q: int :: {$Alloc[q]} q != p ==> $Alloc[q] == old($Alloc[q]));\n" + "ensures n >= 0 ==> (forall q: int :: p <= q && q < p+n ==> $obj(q) == p);\n"; } string SmackRepFlatMem::freeProc() { - stringstream s; - if (SmackOptions::MemoryModelImpls) { - s << "procedure $free(pointer: int)" << endl; - s << " modifies $Alloc;" << endl; - s << " // requires $Alloc[pointer];" << endl; - s << " // requires $obj(pointer) == pointer;" << endl; - s << "{" << endl; - s << " $Alloc[pointer] := false;" << endl; - s << "}" << endl; - } else { - s << "procedure $free(pointer: int);" << endl; - s << "modifies $Alloc;" << endl; - s << "requires $Alloc[pointer];" << endl; - s << "requires $obj(pointer) == pointer;" << endl; - s << "ensures !$Alloc[pointer];" << endl; - s << "ensures (forall x:int :: {$Alloc[x]} x == pointer || old($Alloc)[x] == $Alloc[x]);" << endl; - } - return s.str(); + if (SmackOptions::MemoryModelImpls) + return + "procedure $free(p: int)\n" + "modifies $Alloc;\n" + "{\n" + " $Alloc[p] := false;\n" + "}\n"; + else + return + "procedure $free(p: int);\n" + "modifies $Alloc;\n" + "ensures !$Alloc[p];\n" + "ensures (forall q: int :: {$Alloc[q]} q != p ==> $Alloc[q] == old($Alloc[q]));\n"; } string SmackRepFlatMem::allocaProc() { - stringstream s; - if (SmackOptions::MemoryModelImpls) { - s << "procedure $alloca(obj_size: int) returns (new: int)" << endl; - s << " modifies $CurrAddr, $Alloc;" << endl; - s << " requires obj_size > 0;" << endl; - s << "{" << endl; - s << " assume $CurrAddr > 0;" << endl; - s << " new := $CurrAddr;" << endl; - s << " $CurrAddr := $CurrAddr + obj_size;" << endl; - s << " $Alloc[new] := true;" << endl; - s << "}" << endl; - } else { - s << "procedure $alloca(obj_size: int) returns (new: int);" << endl; - s << "modifies $CurrAddr, $Alloc;" << endl; - s << "requires obj_size > 0;" << endl; - s << "ensures 0 < old($CurrAddr);" << endl; - s << "ensures new == old($CurrAddr);" << endl; - s << "ensures $CurrAddr > old($CurrAddr) + obj_size;" << endl; - s << "ensures $size(new) == obj_size;" << endl; - s << "ensures (forall x:int :: new <= x && x < new + obj_size ==> $obj(x) == new);" << endl; - s << "ensures $Alloc[new];" << endl; - s << "ensures (forall x:int :: {$Alloc[x]} x == new || old($Alloc)[x] == $Alloc[x]);" << endl; - } - return s.str(); + if (SmackOptions::MemoryModelImpls) + return + "procedure $alloca(n: int) returns (p: int)\n" + "modifies $CurrAddr, $Alloc;\n" + "{\n" + " assume $CurrAddr > 0;\n" + " p := $CurrAddr;\n" + " if (n > 0) {\n" + " $CurrAddr := $CurrAddr + n;\n" + " } else {\n" + " $CurrAddr := $CurrAddr + 1;\n" + " }\n" + " $Alloc[p] := true;\n" + "}\n"; + else + return + "procedure $alloca(n: int) returns (p: int);\n" + "modifies $CurrAddr, $Alloc;\n" + "ensures p > 0;\n" + "ensures p == old($CurrAddr);\n" + "ensures $CurrAddr > old($CurrAddr);\n" + "ensures n >= 0 ==> $CurrAddr >= old($CurrAddr) + n;\n" + "ensures $Alloc[p];\n" + "ensures (forall q: int :: {$Alloc[q]} q != p ==> $Alloc[q] == old($Alloc[q]));\n" + "ensures n >= 0 ==> (forall q: int :: p <= q && q < p+n ==> $obj(q) == p);\n"; } string SmackRepFlatMem::memcpyProc(int dstReg, int srcReg) { @@ -196,4 +225,3 @@ string SmackRepFlatMem::memcpyProc(int dstReg, int srcReg) { } } // namespace smack - diff --git a/test/.gitignore b/test/.gitignore index e4a69738d..5f36c5029 100644 --- a/test/.gitignore +++ b/test/.gitignore @@ -1,4 +1,4 @@ *.ll *.bc *.o -*.bpl \ No newline at end of file +*.bpl diff --git a/test/regtest-corral.py b/test/regtest-corral.py index 269d6ea2e..c2e30c61a 100755 --- a/test/regtest-corral.py +++ b/test/regtest-corral.py @@ -2,81 +2,82 @@ import subprocess import re +import time # list of regression tests with the expected outputs tests = [ - ('simple', r'Program has no bugs'), - ('simple_fail', r'This assertion can fail'), - ('simple_pre', r'Program has no bugs'), - ('simple_pre_fail', r'This assertion can fail'), - ('simple_pre1', r'Program has no bugs'), - ('simple_pre1_fail', r'This assertion can fail'), - ('simple_pre2', r'Program has no bugs'), - ('simple_pre2_fail', r'This assertion can fail'), - ('simple_pre3', r'Program has no bugs'), - ('simple_pre3_fail', r'This assertion can fail'), - ('simple_double_free', r'This assertion can fail'), - ('pointers', r'Program has no bugs'), - ('pointers_fail', r'This assertion can fail'), - ('pointers1', r'Program has no bugs'), - ('pointers1_fail', r'This assertion can fail'), - ('pointers2', r'Program has no bugs'), - ('pointers2_fail', r'This assertion can fail'), - ('pointers3', r'Program has no bugs'), - ('pointers3_fail', r'This assertion can fail'), - ('globals', r'Program has no bugs'), - ('globals_fail', r'This assertion can fail'), - ('loop', r'Program has no bugs'), - ('loop_fail', r'This assertion can fail'), - ('loop1', r'Program has no bugs'), - ('loop1_fail', r'This assertion can fail'), - ('nondet', r'Program has no bugs'), - ('printfs', r'Program has no bugs'), - ('extern_func', r'Program has no bugs'), - ('return_label', r'Program has no bugs'), - ('struct_cast', r'Program has no bugs'), - ('struct_cast_fail', r'This assertion can fail'), - ('struct_cast1', r'Program has no bugs'), - ('struct_cast1_fail', r'This assertion can fail'), - ('nested_struct', r'Program has no bugs'), - ('nested_struct_fail', r'This assertion can fail'), - ('nested_struct1', r'Program has no bugs'), - ('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'), - ('func_ptr1_fail', r'This assertion can fail'), - ('array', r'Program has no bugs'), - ('array1', r'Program has no bugs'), - ('array1_fail', r'This assertion can fail'), - ('array2', r'Program has no bugs'), - ('array2_fail', r'This assertion can fail'), - ('array3', r'Program has no bugs'), - ('array3_fail', r'This assertion can fail'), - ('array4', r'Program has no bugs'), - ('array4_fail', r'This assertion can fail'), - ('array_free', r'Program has no bugs'), - ('array_free_fail', r'This assertion can fail'), - ('array_free1', r'Program has no bugs'), - ('array_free1_fail', r'This assertion can fail'), - ('array_free2', r'Program has no bugs'), - ('array_free2_fail', r'This assertion can fail'), - ('lock', r'Program has no bugs'), - ('lock_fail', r'This assertion can fail'), - ('ase_example', r'Program has no bugs'), - ('ase_example_fail', r'This assertion can fail'), - ('two_arrays', r'Program has no bugs'), - ('two_arrays1', r'Program has no bugs'), - ('two_arrays2', r'Program has no bugs'), - ('two_arrays3', r'Program has no bugs'), - ('two_arrays4', r'Program has no bugs'), - ('two_arrays5', r'Program has no bugs'), - ('two_arrays6', r'Program has no bugs'), - ('two_arrays6_fail', r'This assertion can fail') + ('simple', r'Program has no bugs', 2), + ('simple_fail', r'This assertion can fail', 2), + ('simple_pre', r'Program has no bugs', 2), + ('simple_pre_fail', r'This assertion can fail', 2), + ('simple_pre1', r'Program has no bugs', 2), + ('simple_pre1_fail', r'This assertion can fail', 2), + ('simple_pre2', r'Program has no bugs', 2), + ('simple_pre2_fail', r'This assertion can fail', 2), + ('simple_pre3', r'Program has no bugs', 2), + ('simple_pre3_fail', r'This assertion can fail', 2), +# ('simple_double_free', r'This assertion can fail', 2), + ('pointers', r'Program has no bugs', 2), + ('pointers_fail', r'This assertion can fail', 2), + ('pointers1', r'Program has no bugs', 2), + ('pointers1_fail', r'This assertion can fail', 2), + ('pointers2', r'Program has no bugs', 2), + ('pointers2_fail', r'This assertion can fail', 2), + ('pointers3', r'Program has no bugs', 2), + ('pointers3_fail', r'This assertion can fail', 2), + ('globals', r'Program has no bugs', 2), + ('globals_fail', r'This assertion can fail', 2), + ('loop', r'Program has no bugs', 11), + ('loop_fail', r'This assertion can fail', 11), + ('loop1', r'Program has no bugs', 11), + ('loop1_fail', r'This assertion can fail', 11), + ('nondet', r'Program has no bugs', 2), + ('printfs', r'Program has no bugs', 2), + ('extern_func', r'Program has no bugs', 2), + ('return_label', r'Program has no bugs', 2), + ('struct_cast', r'Program has no bugs', 2), + ('struct_cast_fail', r'This assertion can fail', 2), + ('struct_cast1', r'Program has no bugs', 2), + ('struct_cast1_fail', r'This assertion can fail', 2), + ('nested_struct', r'Program has no bugs', 2), + ('nested_struct_fail', r'This assertion can fail', 2), + ('nested_struct1', r'Program has no bugs', 2), + ('nested_struct1_fail',r'This assertion can fail', 2), + ('nested_struct2', r'Program has no bugs', 2), + ('nested_struct2_fail',r'This assertion can fail', 2), + ('struct_assign', r'Program has no bugs', 2), + ('struct_assign_fail', r'This assertion can fail', 2), + ('func_ptr', r'Program has no bugs', 2), + ('func_ptr_fail', r'This assertion can fail', 2), + ('func_ptr1', r'Program has no bugs', 2), + ('func_ptr1_fail', r'This assertion can fail', 2), + ('array', r'Program has no bugs', 2), + ('array1', r'Program has no bugs', 2), + ('array1_fail', r'This assertion can fail', 2), + ('array2', r'Program has no bugs', 11), + ('array2_fail', r'This assertion can fail', 11), + ('array3', r'Program has no bugs', 11), + ('array3_fail', r'This assertion can fail', 11), + ('array4', r'Program has no bugs', 11), + ('array4_fail', r'This assertion can fail', 11), +# ('array_free', r'Program has no bugs', 11), +# ('array_free_fail', r'This assertion can fail', 11), +# ('array_free1', r'Program has no bugs', 11), +# ('array_free1_fail', r'This assertion can fail', 11), +# ('array_free2', r'Program has no bugs', 11), +# ('array_free2_fail', r'This assertion can fail', 11), + ('lock', r'Program has no bugs', 2), + ('lock_fail', r'This assertion can fail', 2), + ('ase_example', r'Program has no bugs', 11), + ('ase_example_fail', r'This assertion can fail', 11), + ('two_arrays', r'Program has no bugs', 2), + ('two_arrays1', r'Program has no bugs', 2), + ('two_arrays2', r'Program has no bugs', 2), + ('two_arrays3', r'Program has no bugs', 2), + ('two_arrays4', r'Program has no bugs', 2), + ('two_arrays5', r'Program has no bugs', 2), + ('two_arrays6', r'Program has no bugs', 2), + ('two_arrays6_fail', r'This assertion can fail', 2) ] def red(text): @@ -85,25 +86,37 @@ def red(text): def green(text): return '\033[0;32m' + text + '\033[0m' -passed = failed = 0 -for test in tests: +def runtests(): + passed = failed = 0 + for test in tests: - for mem in ['flat', 'twodim']: + for mem in ['flat']: - print "{0:>20} {1:>8}:".format(test[0], "(" + mem + ")"), + print "{0:>20} {1:>8}:".format(test[0], "(" + mem + ")"), - # invoke SMACK - p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=corral', '--mem-mod=' + mem, '-o', test[0] +'.bpl'], stdout=subprocess.PIPE) - smackOutput = p.communicate()[0] + # invoke SMACK + t0 = time.time() + p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=corral', + '--unroll=' + str(test[2]), '--mem-mod=' + mem, '-o', test[0] +'.bpl'], + stdout=subprocess.PIPE) + + smackOutput = p.communicate()[0] + elapsed = time.time() - t0 - # check SMACK output - if re.search(test[1], smackOutput): - print green('PASSED') - passed += 1 - else: - print red('FAILED') - failed += 1 + # check SMACK output + if re.search(test[1], smackOutput): + print green('PASSED') + ' [%.2fs]' % round(elapsed, 2) + passed += 1 + else: + print red('FAILED') + failed += 1 + + return passed, failed + +if __name__ == '__main__': -print '\nPASSED count: ', passed -print 'FAILED count: ', failed + passed, failed = runtests() + + print '\nPASSED count: ', passed + print 'FAILED count: ', failed diff --git a/test/regtest.py b/test/regtest.py index 8de639ed0..52d672e44 100755 --- a/test/regtest.py +++ b/test/regtest.py @@ -2,81 +2,82 @@ import subprocess import re +import time # list of regression tests with the expected outputs tests = [ - ('simple', r'1 verified, 0 errors?'), - ('simple_fail', r'0 verified, 1 errors?'), - ('simple_pre', r'1 verified, 0 errors?'), - ('simple_pre_fail', r'0 verified, 1 errors?'), - ('simple_pre1', r'1 verified, 0 errors?'), - ('simple_pre1_fail', r'0 verified, 1 errors?'), - ('simple_pre2', r'1 verified, 0 errors?'), - ('simple_pre2_fail', r'0 verified, 1 errors?'), - ('simple_pre3', r'1 verified, 0 errors?'), - ('simple_pre3_fail', r'0 verified, 1 errors?'), - ('simple_double_free', r'0 verified, 1 errors?'), - ('pointers', r'1 verified, 0 errors?'), - ('pointers_fail', r'0 verified, 1 errors?'), - ('pointers1', r'1 verified, 0 errors?'), - ('pointers1_fail', r'0 verified, 1 errors?'), - ('pointers2', r'1 verified, 0 errors?'), - ('pointers2_fail', r'0 verified, 1 errors?'), - ('pointers3', r'1 verified, 0 errors?'), - ('pointers3_fail', r'0 verified, 1 errors?'), - ('globals', r'1 verified, 0 errors?'), - ('globals_fail', r'0 verified, 1 errors?'), - ('loop', r'1 verified, 0 errors?'), - ('loop_fail', r'0 verified, 1 errors?'), - ('loop1', r'1 verified, 0 errors?'), - ('loop1_fail', r'0 verified, 1 errors?'), - ('nondet', r'1 verified, 0 errors?'), - ('printfs', r'1 verified, 0 errors?'), - ('extern_func', r'1 verified, 0 errors?'), - ('return_label', r'1 verified, 0 errors?'), - ('struct_cast', r'1 verified, 0 errors?'), - ('struct_cast_fail', r'0 verified, 1 errors?'), - ('struct_cast1', r'1 verified, 0 errors?'), - ('struct_cast1_fail', r'0 verified, 1 errors?'), - ('nested_struct', r'1 verified, 0 errors?'), - ('nested_struct_fail', r'0 verified, 1 errors?'), - ('nested_struct1', r'1 verified, 0 errors?'), - ('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?'), - ('func_ptr1_fail', r'0 verified, 1 errors?'), - ('array', r'1 verified, 0 errors?'), - ('array1', r'1 verified, 0 errors?'), - ('array1_fail', r'0 verified, 1 errors?'), - ('array2', r'1 verified, 0 errors?'), - ('array2_fail', r'0 verified, 1 errors?'), - ('array3', r'1 verified, 0 errors?'), - ('array3_fail', r'0 verified, 1 errors?'), - ('array4', r'1 verified, 0 errors?'), - ('array4_fail', r'0 verified, 1 errors?'), - ('array_free', r'1 verified, 0 errors?'), - ('array_free_fail', r'0 verified, 3 errors?'), - ('array_free1', r'1 verified, 0 errors?'), - ('array_free1_fail', r'0 verified, 4 errors?'), - ('array_free2', r'1 verified, 0 errors?'), - ('array_free2_fail', r'0 verified, 5 errors?'), - ('lock', r'1 verified, 0 errors?'), - ('lock_fail', r'0 verified, 1 errors?'), - ('ase_example', r'1 verified, 0 errors?'), - ('ase_example_fail', r'0 verified, 1 errors?'), - ('two_arrays', r'1 verified, 0 errors?'), - ('two_arrays1', r'1 verified, 0 errors?'), - ('two_arrays2', r'1 verified, 0 errors?'), - ('two_arrays3', r'1 verified, 0 errors?'), - ('two_arrays4', r'1 verified, 0 errors?'), - ('two_arrays5', r'1 verified, 0 errors?'), - ('two_arrays6', r'1 verified, 0 errors?'), - ('two_arrays6_fail', r'0 verified, 1 errors?') + ('simple', r'1 verified, 0 errors?', 2), + ('simple_fail', r'0 verified, 1 errors?', 2), + ('simple_pre', r'1 verified, 0 errors?', 2), + ('simple_pre_fail', r'0 verified, 1 errors?', 2), + ('simple_pre1', r'1 verified, 0 errors?', 2), + ('simple_pre1_fail', r'0 verified, 1 errors?', 2), + ('simple_pre2', r'1 verified, 0 errors?', 2), + ('simple_pre2_fail', r'0 verified, 1 errors?', 2), + ('simple_pre3', r'1 verified, 0 errors?', 2), + ('simple_pre3_fail', r'0 verified, 1 errors?', 2), +# ('simple_double_free', r'0 verified, 1 errors?', 2), + ('pointers', r'1 verified, 0 errors?', 2), + ('pointers_fail', r'0 verified, 1 errors?', 2), + ('pointers1', r'1 verified, 0 errors?', 2), + ('pointers1_fail', r'0 verified, 1 errors?', 2), + ('pointers2', r'1 verified, 0 errors?', 2), + ('pointers2_fail', r'0 verified, 1 errors?', 2), + ('pointers3', r'1 verified, 0 errors?', 2), + ('pointers3_fail', r'0 verified, 1 errors?', 2), + ('globals', r'1 verified, 0 errors?', 2), + ('globals_fail', r'0 verified, 1 errors?', 2), + ('loop', r'1 verified, 0 errors?', 11), + ('loop_fail', r'0 verified, 1 errors?', 11), + ('loop1', r'1 verified, 0 errors?', 11), + ('loop1_fail', r'0 verified, 1 errors?', 11), + ('nondet', r'1 verified, 0 errors?', 2), + ('printfs', r'1 verified, 0 errors?', 2), + ('extern_func', r'1 verified, 0 errors?', 2), + ('return_label', r'1 verified, 0 errors?', 2), + ('struct_cast', r'1 verified, 0 errors?', 2), + ('struct_cast_fail', r'0 verified, 1 errors?', 2), + ('struct_cast1', r'1 verified, 0 errors?', 2), + ('struct_cast1_fail', r'0 verified, 1 errors?', 2), + ('nested_struct', r'1 verified, 0 errors?', 2), + ('nested_struct_fail', r'0 verified, 1 errors?', 2), + ('nested_struct1', r'1 verified, 0 errors?', 2), + ('nested_struct1_fail',r'0 verified, 1 errors?', 2), + ('nested_struct2', r'1 verified, 0 errors?', 2), + ('nested_struct2_fail',r'0 verified, 1 errors?', 2), + ('struct_assign', r'1 verified, 0 errors?', 2), + ('struct_assign_fail', r'0 verified, 1 errors?', 2), + ('func_ptr', r'1 verified, 0 errors?', 2), + ('func_ptr_fail', r'0 verified, 1 errors?', 2), + ('func_ptr1', r'1 verified, 0 errors?', 2), + ('func_ptr1_fail', r'0 verified, 1 errors?', 2), + ('array', r'1 verified, 0 errors?', 2), + ('array1', r'1 verified, 0 errors?', 2), + ('array1_fail', r'0 verified, 1 errors?', 2), + ('array2', r'1 verified, 0 errors?', 11), + ('array2_fail', r'0 verified, 1 errors?', 11), + ('array3', r'1 verified, 0 errors?', 11), + ('array3_fail', r'0 verified, 1 errors?', 11), + ('array4', r'1 verified, 0 errors?', 11), + ('array4_fail', r'0 verified, 1 errors?', 11), +# ('array_free', r'1 verified, 0 errors?', 11), +# ('array_free_fail', r'0 verified, 3 errors?', 11), +# ('array_free1', r'1 verified, 0 errors?', 11), +# ('array_free1_fail', r'0 verified, 4 errors?', 11), +# ('array_free2', r'1 verified, 0 errors?', 11), +# ('array_free2_fail', r'0 verified, 5 errors?', 11), + ('lock', r'1 verified, 0 errors?', 2), + ('lock_fail', r'0 verified, 1 errors?', 2), + ('ase_example', r'1 verified, 0 errors?', 11), + ('ase_example_fail', r'0 verified, 1 errors?', 11), + ('two_arrays', r'1 verified, 0 errors?', 2), + ('two_arrays1', r'1 verified, 0 errors?', 2), + ('two_arrays2', r'1 verified, 0 errors?', 2), + ('two_arrays3', r'1 verified, 0 errors?', 2), + ('two_arrays4', r'1 verified, 0 errors?', 2), + ('two_arrays5', r'1 verified, 0 errors?', 2), + ('two_arrays6', r'1 verified, 0 errors?', 2), + ('two_arrays6_fail', r'0 verified, 1 errors?', 2) ] def red(text): @@ -85,25 +86,37 @@ def red(text): def green(text): return '\033[0;32m' + text + '\033[0m' -passed = failed = 0 -for test in tests: +def runtests(): + passed = failed = 0 + for test in tests: - for mem in ['flat', 'twodim']: + for mem in ['flat']: - print "{0:>20} {1:>8}:".format(test[0], "(" + mem + ")"), + print "{0:>20} {1:>8}:".format(test[0], "(" + mem + ")"), - # invoke SMACK - p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=boogie-inline', '--mem-mod=' + mem, '-o', test[0] +'.bpl'], stdout=subprocess.PIPE) - smackOutput = p.communicate()[0] + # invoke SMACK + t0 = time.time() + p = subprocess.Popen(['smack-verify.py', test[0] + '.bc', '--verifier=boogie-inline', + '--unroll=' + str(test[2]), '--mem-mod=' + mem, '-o', test[0] +'.bpl'], + stdout=subprocess.PIPE) + + smackOutput = p.communicate()[0] + elapsed = time.time() - t0 - # check SMACK output - if re.search(test[1], smackOutput): - print green('PASSED') - passed += 1 - else: - print red('FAILED') - failed += 1 + # check SMACK output + if re.search(test[1], smackOutput): + print green('PASSED') + ' [%.2fs]' % round(elapsed, 2) + passed += 1 + else: + print red('FAILED') + failed += 1 + + return passed, failed + +if __name__ == '__main__': -print '\nPASSED count: ', passed -print 'FAILED count: ', failed + passed, failed = runtests() + + print '\nPASSED count: ', passed + print 'FAILED count: ', failed diff --git a/tools/Makefile b/tools/Makefile new file mode 100644 index 000000000..9cf2708e0 --- /dev/null +++ b/tools/Makefile @@ -0,0 +1,13 @@ +##===- projects/smack/tools/Makefile ----------------------*- Makefile -*-===## + +# +# Relative path to the top of the source tree. +# +LEVEL=.. + +# +# List all of the subdirectories that we will compile. +# +DIRS=smack + +include $(LEVEL)/Makefile.common diff --git a/tools/smack/Makefile b/tools/smack/Makefile new file mode 100644 index 000000000..29617f5b9 --- /dev/null +++ b/tools/smack/Makefile @@ -0,0 +1,17 @@ +##===- projects/smack/tools/smack/Makefile ---------------*- Makefile -*-===## + +# +# Indicate where we are relative to the top of the source tree. +# +LEVEL=../.. + +TOOLNAME=smack +LINK_COMPONENTS = all +# LLVMLIBS = LLVMTransformUtils.a LLVMipa.a LLVMAnalysis.a LLVMTarget.a LLVMMC.a LLVMObject.a LLVMBitReader.a LLVMCore.a LLVMSupport.a +USEDLIBS = smack.a LLVMDataStructure.a AssistDS.a + +# +# Include Makefile.common so we know what to do. +# +include $(LEVEL)/Makefile.common + diff --git a/tools/smack/smack.cpp b/tools/smack/smack.cpp new file mode 100644 index 000000000..032b99f93 --- /dev/null +++ b/tools/smack/smack.cpp @@ -0,0 +1,108 @@ +// +// Copyright (c) 2013 Pantazis Deligiannis (p.deligiannis@imperial.ac.uk) +// This file is distributed under the MIT License. See LICENSE for details. +// + +#include "llvm/LinkAllPasses.h" +#include "llvm/PassManager.h" +#include "llvm/IR/LLVMContext.h" +#include "llvm/IR/Module.h" +#include "llvm/IRReader/IRReader.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/Debug.h" +#include "llvm/Support/ManagedStatic.h" +#include "llvm/Support/PrettyStackTrace.h" +#include "llvm/Support/Signals.h" +#include "llvm/Support/SourceMgr.h" +#include "llvm/Support/ToolOutputFile.h" +#include "llvm/Support/raw_ostream.h" + +#include "smack/BplFilePrinter.h" +#include "smack/DSAAliasAnalysis.h" +#include "smack/SmackModuleGenerator.h" + +static llvm::cl::opt +InputFilename(llvm::cl::Positional, llvm::cl::desc(""), + llvm::cl::Required, llvm::cl::value_desc("filename")); + +static llvm::cl::opt +OutputFilename("o", llvm::cl::desc("Override output filename"), + llvm::cl::init(""), llvm::cl::value_desc("filename")); + +static llvm::cl::opt +DefaultDataLayout("default-data-layout", llvm::cl::desc("data layout string to use if not specified by module"), + llvm::cl::init(""), llvm::cl::value_desc("layout-string")); + +// removes extension from filename if there is one +std::string getFileName(const std::string &str) { + std::string filename = str; + size_t lastdot = str.find_last_of("."); + if (lastdot != std::string::npos) + filename = str.substr(0, lastdot); + return filename; +} + +int main(int argc, char **argv) { + llvm::llvm_shutdown_obj shutdown; // calls llvm_shutdown() on exit + llvm::cl::ParseCommandLineOptions(argc, argv, "SMACK - LLVM bitcode to Boogie transformation\n"); + + llvm::sys::PrintStackTraceOnErrorSignal(); + llvm::PrettyStackTraceProgram PSTP(argc, argv); + llvm::EnableDebugBuffering = true; + + if (OutputFilename.empty()) { +// OutputFilename = getFileName(InputFilename) + ".bpl"; + OutputFilename = "a.bpl"; + } + + std::string error_msg; + llvm::SMDiagnostic err; + llvm::LLVMContext &context = llvm::getGlobalContext(); + llvm::OwningPtr module; + llvm::OwningPtr output; + + module.reset(llvm::ParseIRFile(InputFilename, err, context)); + if (module.get() == 0) { + if (llvm::errs().has_colors()) llvm::errs().changeColor(llvm::raw_ostream::RED); + llvm::errs() << "error: " << "Bitcode was not properly read; " << err.getMessage() << "\n"; + if (llvm::errs().has_colors()) llvm::errs().resetColor(); + return 1; + } + + output.reset(new llvm::tool_output_file(OutputFilename.c_str(), error_msg)); + if (!error_msg.empty()) { + if (llvm::errs().has_colors()) llvm::errs().changeColor(llvm::raw_ostream::RED); + llvm::errs() << "error: " << error_msg << "\n"; + if (llvm::errs().has_colors()) llvm::errs().resetColor(); + return 1; + } + + /////////////////////////////// + // initialise and run passes // + /////////////////////////////// + + llvm::PassManager pass_manager; + llvm::PassRegistry &Registry = *llvm::PassRegistry::getPassRegistry(); + llvm::initializeAnalysis(Registry); + + // add an appropriate DataLayout instance for the module + llvm::DataLayout *dl = 0; + const std::string &moduleDataLayout = module.get()->getDataLayout(); + if (!moduleDataLayout.empty()) + dl = new llvm::DataLayout(moduleDataLayout); + else if (!DefaultDataLayout.empty()) + dl = new llvm::DataLayout(moduleDataLayout); + if (dl) pass_manager.add(dl); + + pass_manager.add(llvm::createInternalizePass()); + pass_manager.add(llvm::createPromoteMemoryToRegisterPass()); + pass_manager.add(llvm::createDeadInstEliminationPass()); + pass_manager.add(llvm::createLowerSwitchPass()); + pass_manager.add(new smack::SmackModuleGenerator()); + pass_manager.add(new smack::BplFilePrinter(output->os())); + pass_manager.run(*module.get()); + + output->keep(); + + return 0; +}