Skip to content

GitLab

Commit e16e3797 authored by Dr. Michael Petter's avatar Dr. Michael Petter
Browse files
Options

Merge branch 'equalities' into 'master' 

Equalities

See merge request !1
parents 27ebb08b 23575a39
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 6200 additions and 670 deletions
.lldbinit.in 0 → 100644
View file @ e16e3797
command regex dump 's/(.+)/expression -O -l c++ -- ((llvm::Value*) %1 )->dump()/'
command alias d dump
command script import ${CMAKE_SOURCE_DIR}/lldb/ValueFormatter.py
\ No newline at end of file
CMakeLists.txt
View file @ e16e3797
# If we don't need RTTI or EH, there's no reason to export anything
# from the hello plugin.
#if( NOT LLVM_REQUIRES_RTTI )
# if( NOT LLVM_REQUIRES_EH )
# set(LLVM_EXPORTED_SYMBOL_FILE ${CMAKE_CURRENT_SOURCE_DIR}/Hello.exports)
# endif()
#endif()
if(WIN32 OR CYGWIN)
set(LLVM_LINK_COMPONENTS Core Support)
cmake_minimum_required(VERSION 3.4.3)
project(PAIN
VERSION 1.0.0
LANGUAGES C CXX
)
set(CMAKE_CXX_STANDARD 17)
set (PROJECT_DESCRIPTION "Implements an LLVM analysis pass using abstract interpretation.")
set (PROJECT_HOMEPAGE_URL "https://versioncontrolseidl.in.tum.de/petter/llvm-abstractinterpretation")
if (NOT PATH_TO_LLVM)
message(FATAL_ERROR "
The cmake is supposed to be called with PATH_TO_LLVM pointing to
a precompiled version of LLVM or to to the source code of LLVM
Examples:
cmake -G \"${CMAKE_GENERATOR}\" -DPATH_TO_LLVM=/opt/llvm-9.0.1 ${CMAKE_SOURCE_DIR}
cmake -G \"${CMAKE_GENERATOR}\" -DPATH_TO_LLVM=/llvm-project/llvm ${CMAKE_SOURCE_DIR}
")
endif()
# For older LLVM < 8.0 replace first line with this
# add_llvm_loadable_module(llvm-pain
add_llvm_library(llvm-pain MODULE
if (NOT IS_ABSOLUTE ${PATH_TO_LLVM})
# Convert relative path to absolute path
get_filename_component(PATH_TO_LLVM
"${PATH_TO_LLVM}" REALPATH BASE_DIR "${CMAKE_BINARY_DIR}")
endif()
set (BUILD_AGAINST_PRECOMPILED_LLVM TRUE)
if (EXISTS ${PATH_TO_LLVM}/CMakeLists.txt)
set (BUILD_AGAINST_PRECOMPILED_LLVM FALSE)
endif()
# This enables assertions for Release builds.
# https://stackoverflow.com/questions/22140520/how-to-enable-assert-in-cmake-release-mode
string(REPLACE "-DNDEBUG" "" CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE}")
if (${BUILD_AGAINST_PRECOMPILED_LLVM})
set (search_paths
${PATH_TO_LLVM}
${PATH_TO_LLVM}/lib/cmake
${PATH_TO_LLVM}/lib/cmake/llvm
${PATH_TO_LLVM}/lib/cmake/clang
${PATH_TO_LLVM}/share/clang/cmake/
${PATH_TO_LLVM}/share/llvm/cmake/
)
find_package(LLVM REQUIRED CONFIG PATHS ${search_paths} NO_DEFAULT_PATH)
find_package(Clang REQUIRED CONFIG PATHS ${search_paths} NO_DEFAULT_PATH)
list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}")
else()
set (LLVM_ENABLE_PROJECTS "clang" CACHE BOOL "Build only Clang when building against monorepo" FORCE)
set (LLVM_TARGETS_TO_BUILD "host" CACHE STRING "Only build targets for host architecture" FORCE)
#set (BUILD_SHARED_LIBS "On" CACHE BOOL "Link LLVM libraries dynamically" FORCE)
add_subdirectory(${PATH_TO_LLVM} llvm-build)
if (NOT TARGET clangTooling)
message(FATAL_ERROR "
Cannot find clangTooling target. Did you forget to clone clang sources?
Clean CMake cache and make sure they are available at:
${PATH_TO_LLVM}/tools/clang")
endif()
# Normally, include paths provided by LLVMConfig.cmake
# In this case we can 'steal' them from real targets
get_target_property(llvm_support_includes LLVMSupport INCLUDE_DIRECTORIES)
get_target_property(clang_tooling_includes clangTooling INCLUDE_DIRECTORIES)
set(LLVM_INCLUDE_DIRS ${llvm_support_includes} ${clang_tooling_includes})
list(REMOVE_DUPLICATES LLVM_INCLUDE_DIRS)
# Manually include the llvm CMake modules
list(APPEND CMAKE_MODULE_PATH
"${PATH_TO_LLVM}/cmake"
"${PATH_TO_LLVM}/cmake/modules"
)
set(LLVM_MAIN_SRC_DIR ${PATH_TO_LLVM})
endif()
include(LLVM-Config)
include(HandleLLVMOptions)
include(AddLLVM)
if ("LLVM" IN_LIST LLVM_AVAILABLE_LIBS)
set (LLVM_AVAILABLE_LIBS
LLVM
)
else()
set (LLVM_AVAILABLE_LIBS
LLVMSupport
LLVMCore
LLVMAnalysis
)
endif()
set(PAIN_SOURCES
src/fixpoint.cpp
src/fixpoint.h
src/fixpoint_widening.cpp
src/value_set.cpp
src/value_set.h
src/simple_interval.cpp
src/normalized_conjunction.cpp
src/linear_equality.cpp
src/linear_subspace.cpp
)
set(PAIN_HEADERS
src/fixpoint.h
src/value_set.h
src/simple_interval.h
src/normalized_conjunction.h
src/linear_equality.h
src/general.h
src/global.h
src/abstract_state.h
src/hash_utils.h
src/linear_subspace.h
src/simple_matrix.h
src/sparse_matrix.h
)
include_directories(${LLVM_INCLUDE_DIRS})
add_llvm_library(llvm-pain MODULE
${PAIN_SOURCES}
${PAIN_HEADERS}
DEPENDS
intrinsics_gen
irgen
PLUGIN_TOOL
opt
)
#
# Tests
#
add_llvm_executable(simple_interval_test
test/simple_interval_test.cpp
${PAIN_HEADERS}
${PAIN_SOURCES}
DEPENDS
irgen
intrinsics_gen
)
target_link_libraries(simple_interval_test
PRIVATE ${LLVM_AVAILABLE_LIBS}
)
add_llvm_executable(normalized_conjunction_test
test/normalized_conjunction_test.cpp
${PAIN_HEADERS}
${PAIN_SOURCES}
DEPENDS
irgen
intrinsics_gen
)
target_link_libraries(normalized_conjunction_test
PRIVATE ${LLVM_AVAILABLE_LIBS}
)
add_llvm_executable(linear_subspace_test
test/linear_subspace_test.cpp
${PAIN_HEADERS}
${PAIN_SOURCES}
DEPENDS
irgen
intrinsics_gen
)
target_link_libraries(linear_subspace_test
PRIVATE ${LLVM_AVAILABLE_LIBS}
)
add_llvm_executable(simple_matrix_test
test/simple_matrix_test.cpp
${PAIN_HEADERS}
${PAIN_SOURCES}
)
target_link_libraries(simple_matrix_test
PRIVATE ${LLVM_AVAILABLE_LIBS}
)
add_llvm_executable(sparse_matrix_test
test/sparse_matrix_test.cpp
${PAIN_HEADERS}
${PAIN_SOURCES}
)
target_link_libraries(sparse_matrix_test
PRIVATE ${LLVM_AVAILABLE_LIBS}
)
enable_testing()
add_test(NAME intervalAnalysisTest
COMMAND opt --load $<TARGET_FILE:llvm-pain> --painpass -S ${CMAKE_SOURCE_DIR}/output/add-1.ll
)
add_test(NAME simpleIntervalTest
COMMAND simple_interval_test
)
add_test(NAME normalizedConjunctionTest
COMMAND normalized_conjunction_test
)
add_test(NAME linearSubspaceTest
COMMAND linear_subspace_test
)
add_test(NAME simpleMatrixTest
COMMAND simple_matrix_test
)
add_test(NAME sparseMatrixTest
COMMAND sparse_matrix_test
)
#
# Samples
#
set(SAMPLES
add-1-float
add-1
add-2
add-3
add-4
basic_function
branching
cmp-two-variables-1
cmp-two-variables-2
euler-48
euler
example
for-loop-1
for
func-test-1
func-test-2
func-test-3
func-test-4
func-test-5
func-test-for
func-test-rec-endless
func-test-rec
func-test-switch
gcd
goto
if-and
if-multiple-of-4
if-then-else-2
if-then-else-complicated
if-then-else-two-constraints
if-then-else
multiple-functions
ops
switch-2
switch-3
switch-two-labels
switch
while-1
while-2
while-bigger-steps
while-neg
example-1
A
B
C
D
)
# Older CMake version do not support list transformations
macro(list_transform_prepend in prefix)
foreach(f ${${in}})
list(APPEND temp "${prefix}${f}")
endforeach()
set(${in} "${temp}")
unset(temp)
endmacro()
macro(list_transform_append in suffix out)
foreach(f ${${in}})
list(APPEND ${out} "${f}${suffix}")
endforeach()
endmacro()
list_transform_append(SAMPLES ".c" SAMPLES_C)
list_transform_append(SAMPLES ".bc" SAMPLES_BC)
list_transform_append(SAMPLES ".ll" SAMPLES_LL)
list_transform_prepend(SAMPLES_LL "${CMAKE_SOURCE_DIR}/output/")
list_transform_prepend(SAMPLES_BC "${CMAKE_SOURCE_DIR}/output/")
list_transform_prepend(SAMOLES_C "${CMAKE_SOURCE_DIR}/samples/")
add_custom_target(irgen
DEPENDS ${SAMPLES_LL} ${SAMPLES_BC}
)
file(MAKE_DIRECTORY ${CMAKE_SOURCE_DIR}/output)
if (APPLE)
foreach(src ${SAMPLES})
add_custom_command(
OUTPUT ${CMAKE_SOURCE_DIR}/output/${src}.ll
COMMAND clang --sysroot ${CMAKE_OSX_SYSROOT} -O0 -emit-llvm ${CMAKE_SOURCE_DIR}/samples/${src}.c -Xclang -disable-O0-optnone -c -o ${CMAKE_SOURCE_DIR}/output/${src}.bc
COMMAND opt -S -mem2reg ${CMAKE_SOURCE_DIR}/output/${src}.bc -o ${CMAKE_SOURCE_DIR}/output/${src}.ll
DEPENDS clang opt ${CMAKE_SOURCE_DIR}/samples/${src}.c
COMMENT "Generating LLVM IR for example ${src}"
)
endforeach(src)
else()
foreach(src ${SAMPLES})
add_custom_command(
OUTPUT ${CMAKE_SOURCE_DIR}/output/${src}.ll
COMMAND clang -O0 -emit-llvm ${CMAKE_SOURCE_DIR}/samples/${src}.c -Xclang -disable-O0-optnone -c -o ${CMAKE_SOURCE_DIR}/output/${src}.bc
COMMAND opt -S -mem2reg ${CMAKE_SOURCE_DIR}/output/${src}.bc -o ${CMAKE_SOURCE_DIR}/output/${src}.ll
DEPENDS clang opt ${CMAKE_SOURCE_DIR}/samples/${src}.c
COMMENT "Generating LLVM IR for example ${src}"
)
endforeach(src)
endif()
configure_file(.lldbinit.in .lldbinit)
\ No newline at end of file
README.md
View file @ e16e3797
# Program Optimization Lab 2018
# Program Optimization Lab 202X
Implements an LLVM analysis pass using abstract interpretation.
Implementing an LLVM analysis framework based upon the Seidl Program Optimization Lecture.
## Build
Get the LLVM source code from [here](http://releases.llvm.org/download.html). Then get clang as well, into `llvm/tools`. Create a build directory somewhere, initialise CMake, and build. For example
### Build against a system-wide installed LLVM
Install the LLVM packages from your distro's package manager, e.g. Ubuntu 20.04:
# From your llvm-9.0.0-src, or whatever the version is now
wget http://releases.llvm.org/9.0.0/llvm-9.0.0.src.tar.xz
tar xf llvm-9.0.0.src.tar.xz
# install the necessary LLVM packages
sudo apt install cmake clang libclang-10-dev llvm-10-dev
# now continue by building the project
git clone https://versioncontrolseidl.in.tum.de/petter/llvm-abstractinterpretation.git
cd llvm-abstractinterpretation
mkdir build
cd build
cmake -G "Unix Makefiles" -DPATH_TO_LLVM=/usr/lib/llvm-10 ..
make
You can do this, however the precompiled LLVM binaries come without symbol names, thus debugging
might be a little harder this way. Alterntively consider the following route:
### Build against custom downloaded LLVM Sources
Get the LLVM source code from [here](https://releases.llvm.org/download.html). Then get clang as well, into `llvm/tools`. Create a build directory somewhere, initialise CMake, and build. For example
# From llvm-10.0.0-src, or whatever the version is now
wget https://github.com/llvm/llvm-project/releases/download/llvmorg-10.0.0/llvm-10.0.0.src.tar.xz
tar xf llvm-10.0.0.src.tar.xz
# now also download clang
cd llvm-9.0.0.src/tools
wget http://releases.llvm.org/9.0.0/cfe-9.0.0.src.tar.xz
tar xf cfe-9.0.0.src.tar.xz
mv cfe-9.0.0.src clang
cd llvm-10.0.0.src/tools
wget https://github.com/llvm/llvm-project/releases/download/llvmorg-10.0.0/clang-10.0.0.src.tar.xz
tar xf clang-10.0.0.src.tar.xz
mv clang-10.0.0.src clang
cd ../..
# now continue by building LLVM
mkdir llvm_build
cd llvm_build
cmake ../llvm-?.?.?-src -DLLVM_TARGETS_TO_BUILD=X86
make -j2
The parallel make may run out of memory at the end. You can restart it sequentially by issuing another `make -j1`.
# important: Don't forget to restrict to X86, otherwise prepare for a day of compiling
cmake ../llvm-10.0.0-src -DLLVM_TARGETS_TO_BUILD=X86
# 4x parallelized make, which will probably fail due to RAM consumption
make -j4
# make -j1 in order to catch up, where the parallel make aborted
Now we can initalise the repository.
On a 4 core i7-8550U with 16GB RAM this may take up to 3:00h for a sequentially run make ( `make -j1` ) to account for a poor man's RAM equipment. Also, the build will need at least 50GB of disk space, be sure to have enough room...
cd ..
git clone ssh://git@github.com/PUT/THE/CORRECT/REPOSITORY/IN/HERE.git
cd PUT/THE/CORRECT/REPOSITORY/IN/HERE
python3 init.py
The script should be able to find your LLVM and clang. If it is not, you need to specify them by hand.
At last, let us compile and run the samples.
If there are errors regarding missing header files, you probably need to rebuild llvm.
python3 run.py --make
## Author during Bachelor Thesis 2019/20
If there are errors regarding missing header files, you probably need to rebuild llvm.
* Tim Gymnich
## Useful things
## Authors Lab Course WS 2019/20
The `run.py` script contains everything, up to and including the kitchen sink. It can run the samples, build, run the debugger, as well as build and run the tests. Just read its help message to get all the good stuff. I want to highlight the `-n` option, which causes it to just print out the commands it would run. This is great to just copy-paste the relevant ones into your terminal (or IDE).
* Florian Stamer
* Dmytro Yakymets
## Authors
## Authors Lab Course WS 2018/19
* Ramona Brückl
* Philipp Czerner ([github](https://github.com/suyjuris/), [mail](mailto:philipp.czerner@nicze.de))
* Tim Gymnich
* Thomas Frank
### Authors of previous semesters
## Authors Lab Course SS 2018
* Julian Erhard
* Jakob Gottfriedsen
* Peter Munch
......
init.py deleted 100755 → 0
View file @ 27ebb08b
#!/usr/bin/python3
# coding: utf-8
import argparse
import os
import subprocess
import sys
if sys.version_info[0] < 3:
print("Error: This script only supports Python 3")
sys.exit(5)
parser = argparse.ArgumentParser(description='Setup the project. This creates the necessary symbolic links in the LLVM source code and adds the entries into the right CMakeList.txt. Also initialises the configuration for the run.py script.')
parser.add_argument('--llvm-path', help='path to the LLVM build directory, containing a file bin/opt.')
parser.add_argument('--llvm-src', help='path to the LLVM source directory, containing lib/Analysis ')
parser.add_argument('--clang-path', help='path to the clang build direcotry, containing a file bin/clang')
args = parser.parse_args()
llvm_path = args.llvm_path
llvm_src = args.llvm_src
clang_path = args.clang_path
project_dir = os.path.dirname(os.path.abspath(sys.argv[0]))
project_name = 'AbstractInterpretation'
cmake = 'cmake'
if llvm_path is None:
# Try to guess the correct path
d = os.path.abspath(project_dir)
while os.path.dirname(d) != d:
d = os.path.dirname(d)
for i in os.listdir(d):
if os.path.isfile(d + '/' + i + '/bin/opt'):
llvm_path = d + '/' + i
print('Auto-detecting llvm-path as ' + llvm_path)
break
if llvm_path is not None: break
else:
print('Error: No llvm-path specified (use --llvm-path)')
parser.print_help()
sys.exit(1)
if llvm_src is None:
# Try to guess the correct path
d = os.path.abspath(project_dir)
while os.path.dirname(d) != d:
d = os.path.dirname(d)
for i in os.listdir(d):
if os.path.isfile(d + '/' + i + '/cmake_install.cmake'):
continue
if os.path.isdir(d + '/' + i + '/lib/Analysis'):
llvm_src = d + '/' + i
print('Auto-detecting llvm-src as ' + llvm_src)
break
if llvm_src is not None: break
else:
print('Error: No llvm-src specified (use --llvm-src)')
parser.print_help()
sys.exit(1)
if clang_path is None:
clang_path = llvm_path
print('clang-path not specified, defaulting to ' + clang_path)
opt = llvm_path + '/bin/opt'
llvm_dest = llvm_src + '/lib/Analysis'
clang = clang_path + '/bin/clang'
if not os.path.isfile(opt):
print('Error: no opt exists at ' + opt + ' (maybe you forgot to build LLVM?)')
sys.exit(2)
if not os.path.isdir(llvm_dest):
print('Error: directory does not exist, at ' + llvm_dest)
sys.exit(2)
if not os.path.isfile(clang):
print('Error: no clang exists at ' + clang)
sys.exit(2)
# Create the symbolic link in the LLVM sources
try:
link_name = llvm_dest + '/' + project_name
os.symlink(project_dir, link_name, target_is_directory=True)
print('Created symbolic link from %s to %s' % (link_name, project_dir))
except FileExistsError:
print('Symlink already exists')
# Write the configuration for the run.py script
config_file_name = project_dir + '/.config';
config_file = open(config_file_name, 'w')
config_file.write(llvm_src+'\n'+llvm_path+'\n'+clang_path+'\n')
config_file.close()
print('Wrote configuration to %s' % (config_file_name,))
# Adjust CMakeLists.txt
cmake_file_name = llvm_dest + '/CMakeLists.txt'
line_to_insert = 'add_subdirectory(%s)\n' % (project_name,)
cmake_file = open(cmake_file_name, 'r')
lines = cmake_file.readlines()
needs_changes = line_to_insert not in lines
cmake_file.close()
if needs_changes:
cmake_file = open(cmake_file_name, 'a')
cmake_file.write('\n' + line_to_insert)
cmake_file.close()
print('CMakeLists.txt modified, at %s' % (cmake_file_name,))
# Also regenerate the CMake cache
print('Rebuilding cmake cache')
subprocess.run([cmake, llvm_path], check=True)
else:
print('CMakeLists.txt is fine')
lldb/ValueFormatter.py 0 → 100644
View file @ e16e3797
import lldb
def ValueFormatter(valobj, internal_dict):
frame = lldb.debugger.GetSelectedTarget().GetProcess().GetSelectedThread().GetSelectedFrame()
options = lldb.SBExpressionOptions()
options.SetLanguage(lldb.eLanguageTypeObjC_plus_plus)
options.SetTrapExceptions(False)
options.SetTimeoutInMicroSeconds(5000000) # 5s
addr = valobj.GetValue()
expr = frame.EvaluateExpression('((llvm::Value*) {0})->getName().data()'.format(addr), options)
name = expr.GetSummary()
return '{0}'.format(name)
def __lldb_init_module(debugger, internal_dict):
debugger.HandleCommand("type summary add -F " + __name__ + ".ValueFormatter llvm::Value")
run.py deleted 100755 → 0
View file @ 27ebb08b
#!/usr/bin/python3
# coding: utf-8
import argparse
import os
import platform
import shlex
import subprocess
import sys
if sys.version_info[0] < 3:
print("Error: This script only supports Python 3")
sys.exit(5)
project_dir = os.path.abspath(os.path.dirname(sys.argv[0]))
os.chdir(project_dir)
if not os.path.isfile(".config"):
print("No config file was found. Please run init.py first!")
sys.exit(-1)
config_file = open(".config", "r")
lines = config_file.readlines()
llvm_path = lines[1].strip()
clang_path = lines[2].strip()
config_file.close()
opt = llvm_path + '/bin/opt'
llvm_dis = llvm_path + '/bin/llvm-dis'
llvm_config = llvm_path + '/bin/llvm-config'
clang = clang_path + '/bin/clang'
cmake = 'cmake'
gdb = 'gdb'
lldb = 'lldb'
CXX = os.environ.get('CXX', 'c++')
if not os.path.isfile(<