Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
.vscode
ocelot/AtomicRegionInference/build
benchmarks/ctests/*.ll
File renamed without changes.
18 changes: 18 additions & 0 deletions benchmarks/ctests/example01.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
#include <stdio.h>

void Fresh(int x) { printf("Fresh\n"); }
void Consistent(int x, int id) { printf("Consistent\n"); }

void atomic_start() {}
void atomic_end() {}

int tmp() { return 0; }
int (*IO_NAME1)() = tmp;
void log(int x) {}

int app() {
int x = tmp();
Fresh(x);
log(x);
return 0;
}
24 changes: 24 additions & 0 deletions benchmarks/ctests/example02.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
void Fresh(int x) {}
void Consistent(int x, int id) {}

void atomic_start() {}
void atomic_end() {}

int sense() { return 0; }
int (*IO_NAME)() = sense;

int norm(int t) { return t; }

void log(int x) {}

int tmp() {
int t = sense();
int t_norm = norm(t);
return t_norm;
}

void app() {
int x = tmp();
Fresh(x);
log(x);
}
18 changes: 18 additions & 0 deletions benchmarks/ctests/example03.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
void Fresh(int x) {}
void Consistent(int x, int id) {}

void atomic_start() {}
void atomic_end() {}

int input() { return 0; }
int (*IO_NAME)() = input;

void log(int x) {}

void app() {
int x = input();
int y = 1;
int z = x + 1;
log(z);
Fresh(x);
}
18 changes: 16 additions & 2 deletions ocelot/AtomicRegionInference/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -1,8 +1,22 @@
cmake_minimum_required(VERSION 3.1)
cmake_minimum_required(VERSION 3.6)
project(InferAtoms)

# LLVM uses C++17.
set(CMAKE_CXX_STANDARD 17)

# Load LLVMConfig.cmake. If this fails, consider setting `LLVM_DIR` to point
# to your LLVM installation's `lib/cmake/llvm` directory.
find_package(LLVM REQUIRED CONFIG)

# Include the part of LLVM's CMake libraries that defines
# `add_llvm_pass_plugin`.
include(AddLLVM)

# Use LLVM's preprocessor definitions, include directories, and library search
# paths.
add_definitions(${LLVM_DEFINITIONS})
include_directories(${LLVM_INCLUDE_DIRS})
link_directories(${LLVM_LIBRARY_DIRS})

add_subdirectory(src) # Use your pass name here.
# Our pass lives in this subdirectory.
add_subdirectory(src)
26 changes: 26 additions & 0 deletions ocelot/AtomicRegionInference/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
.PHONY: clean_tests clean eg1 eg2

eg1:
TEST=example01 make test
eg2:
TEST=example02 make test
eg3:
TEST=example03 make test

test:
$(MAKE) -C build all
clang -S -emit-llvm\
-fpass-plugin=build/src/InferAtomsPass.dylib\
-fno-discard-value-names\
../../benchmarks/ctests/$(TEST).c\
-o ../../benchmarks/ctests/$(TEST).ll
clang -S -emit-llvm\
-fno-discard-value-names\
../../benchmarks/ctests/$(TEST).c\
-o ../../benchmarks/ctests/$(TEST).orig.ll

clean_tests:
find ../../benchmarks/ctests -name "*.ll" -exec rm -rf {} \;

clean:
rm -rf build
25 changes: 16 additions & 9 deletions ocelot/AtomicRegionInference/README.md
Original file line number Diff line number Diff line change
@@ -1,14 +1,21 @@
# region-inference-pass
# Atomic Region Inference

LLVM Pass for inferring atomic regions
LLVM Pass for inferring atomic regions. Tested to work with LLVM 17.

Build:
To build the pass:

$ mkdir build
$ cd build
$ cmake ..
$ make
```sh
mkdir build
cd build
cmake ..
make
```

Run:
You may bootstrap Clang to use the pass to compile a C file like so:

$ opt -load build/src/libInferAtomicPass.so -atomize something.bc
```sh
clang -S -emit-llvm -fpass-plugin=src/InferAtomsPass.dylib -fno-discard-value-names ../../../benchmarks/ctests/example01.c
```

Or, when testing, use the shortcuts provided in the Makefile (e.g., `make eg1`),
which produce two LLVM IRs with and without the pass enabled.
24 changes: 4 additions & 20 deletions ocelot/AtomicRegionInference/src/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -1,23 +1,7 @@
add_library(InferAtomicPass MODULE
add_llvm_pass_plugin(InferAtomsPass
# List your source files here.
InferAtomicPass.cpp
ConsistentInference.cpp
InferAtoms.cpp
TaintTracker.cpp
InferFreshCons.cpp
Helpers.cpp
)

# Use C++11 to compile our pass (i.e., supply -std=c++11).
target_compile_features(InferAtomicPass PRIVATE cxx_range_for cxx_auto_type)

# LLVM is (typically) built with no C++ RTTI. We need to match that;
# otherwise, we'll get linker errors about missing RTTI data.
set_target_properties(InferAtomicPass PROPERTIES
COMPILE_FLAGS "-fno-rtti"
)

# Get proper shared-library behavior (where symbols are not necessarily
# resolved when the shared library is linked) on OS X.
if(APPLE)
set_target_properties(InferAtomicPass PROPERTIES
LINK_FLAGS "-undefined dynamic_lookup"
)
endif(APPLE)
Loading