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
85 changes: 85 additions & 0 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -174,6 +174,91 @@ foreach(i RANGE ${dvf_len2})
)
endforeach()
endforeach()

# sliced mta tests (ctest -R sliced_mta_tests -VV)
set(sliced_mta_cmd "mta -mta-enable-slicing=true -stat=true")
file(GLOB sliced_mta_files RELATIVE ${CMAKE_CURRENT_SOURCE_DIR} "${CMAKE_CURRENT_SOURCE_DIR}/test_cases_bc/sliced_mta/*.bc*")
string(REPLACE " " ";" commandtemp ${sliced_mta_cmd})
set(command ${commandtemp})
foreach(filename ${sliced_mta_files})
if (${filename} MATCHES ".pre.bc" OR ${filename} MATCHES ".pre.svf.bc" OR ${filename} MATCHES ".svf.bc")
continue()
endif()
add_test(
NAME sliced_mta_tests/${filename}
COMMAND ${command} ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
)
endforeach()

# mta statistic tests (ctest -R mta_stat_tests -VV)
set(mta_stat_cmd "mta -mta-flow-sensitive=false -stat=true")
set(mta_stat_files
test_cases_bc/sliced_mta/basic.c.bc
test_cases_bc/sliced_mta/indirect_fork_join.c.bc
)
string(REPLACE " " ";" commandtemp ${mta_stat_cmd})
set(command ${commandtemp})
foreach(filename ${mta_stat_files})
add_test(
NAME mta_stat_tests/${filename}
COMMAND ${command} ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
)
endforeach()

# whole-program (no-slicing) FSAM baseline (ctest -R mta_whole_tests -VV)
# Runs the SlicedMTA pipeline with slicing off, exercising runWholeProgramDetection
# (the A/B reference the sliced run is compared against).
set(mta_whole_cmd "mta -mta-enable-slicing=false -stat=true")
file(GLOB mta_whole_files RELATIVE ${CMAKE_CURRENT_SOURCE_DIR} "${CMAKE_CURRENT_SOURCE_DIR}/test_cases_bc/sliced_mta/*.bc*")
string(REPLACE " " ";" commandtemp ${mta_whole_cmd})
set(command ${commandtemp})
foreach(filename ${mta_whole_files})
if (${filename} MATCHES ".pre.bc" OR ${filename} MATCHES ".pre.svf.bc" OR ${filename} MATCHES ".svf.bc")
continue()
endif()
add_test(
NAME mta_whole_tests/${filename}
COMMAND ${command} ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
)
endforeach()

# single unified slice, one slice for ILA + FSPTA (ctest -R mta_single_slice_tests -VV)
# Exercises the SingleSlicer (-mta-slicing-single) single-pass baseline branch.
set(mta_single_cmd "mta -mta-enable-slicing=true -mta-slicing-single=true -stat=true")
file(GLOB mta_single_files RELATIVE ${CMAKE_CURRENT_SOURCE_DIR} "${CMAKE_CURRENT_SOURCE_DIR}/test_cases_bc/sliced_mta/*.bc*")
string(REPLACE " " ";" commandtemp ${mta_single_cmd})
set(command ${commandtemp})
foreach(filename ${mta_single_files})
if (${filename} MATCHES ".pre.bc" OR ${filename} MATCHES ".pre.svf.bc" OR ${filename} MATCHES ".svf.bc")
continue()
endif()
add_test(
NAME mta_single_slice_tests/${filename}
COMMAND ${command} ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
)
endforeach()

# saber with the full SVFG on top of the pointer-only one (ctest -R saber_full_svfg_tests -VV)
# Exercises SVFGBuilder::buildFullSVFG / SVFGOPT (plain saber uses the pointer-only SVFG).
set(saber_full_cmd "saber -leak -saber-full-svfg=true -valid-tests -stat=false")
file(GLOB saber_full_files RELATIVE ${CMAKE_CURRENT_SOURCE_DIR} "${CMAKE_CURRENT_SOURCE_DIR}/test_cases_bc/mem_leak/*.bc*")
string(REPLACE " " ";" commandtemp ${saber_full_cmd})
set(command ${commandtemp})
foreach(filename ${saber_full_files})
if (${filename} MATCHES ".pre.bc" OR ${filename} MATCHES ".pre.svf.bc" OR ${filename} MATCHES ".svf.bc")
continue()
endif()
add_test(
NAME saber_full_svfg_tests/${filename}
COMMAND ${command} ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
)
endforeach()

# graphdb dvf and mta tests (write + read)
# Usage: ctest -R graphdb-dvf_tests -VV
list(APPEND graphdb_dvf_folders
Expand Down
3 changes: 2 additions & 1 deletion generate_bc.sh
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ test_dirs="
mem_leak
double_free
mta
sliced_mta
non_annotated_tests
path_tests
objtype_tests
Expand Down Expand Up @@ -120,4 +121,4 @@ for td in $test_dirs; do
done
done

fi
fi
41 changes: 41 additions & 0 deletions src/sliced_mta/basic.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
// basic.c -- a minimal test for the MSli artifact.
//
// Two worker threads share a counter and a flag; main also touches them. Most of
// the program is independent local arithmetic (compute_*) that never touches the
// shared state, so MSli slices it away -- the analysed slice is far smaller than
// the whole program, yet the reported race statements are identical to the
// whole-program (FSAM) run. Analyses quickly.
#include <pthread.h>

int counter; // shared, written by several threads -> race
int flag; // shared, written/read concurrently -> race
int done_local; // thread-local-ish bookkeeping

// --- independent computation that touches no shared state (sliced away) ---
static int compute_a(int x) { int s = x; for (int i = 0; i < 10; i++) s = s * 3 + i; return s; }
static int compute_b(int x) { return compute_a(x) ^ (x << 2); }
static int compute_c(int x) { int s = 0; for (int i = 0; i < 8; i++) s += compute_b(x + i); return s; }

static void busy_work(int seed) {
volatile int sink = 0;
for (int i = 0; i < 4; i++) sink += compute_c(seed + i);
}

void* worker(void* arg) {
busy_work((int)(long)arg); // noise -> sliced away
counter = counter + 1; // shared write -> races with the other workers
flag = 1; // shared write -> races with main's read
return 0;
}

int main(void) {
pthread_t t1, t2;
busy_work(42); // noise -> sliced away
pthread_create(&t1, 0, worker, (void*)1);
pthread_create(&t2, 0, worker, (void*)2);
int r = flag; // concurrent read of flag -> race
counter = r; // concurrent write of counter -> race
pthread_join(t1, 0);
pthread_join(t2, 0);
return 0;
}
50 changes: 50 additions & 0 deletions src/sliced_mta/indirect_fork_join.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
#include <pthread.h>

typedef void *(*entry_fn)(void *);

pthread_t workers[4];
int shared_slots[4];
int shared_sum;

static void update_slot(int idx, int value) {
shared_slots[idx & 3] = value;
shared_sum += shared_slots[idx & 3];
}

static void *worker_a(void *arg) {
long id = (long)arg;
update_slot((int)id, (int)id + 10);
shared_sum += (int)id;
return 0;
}

static void *worker_b(void *arg) {
long id = (long)arg;
update_slot((int)id + 1, (int)id + 20);
shared_slots[1] += shared_sum;
return 0;
}

static entry_fn pick_worker(int flag) {
if (flag)
return worker_a;
return worker_b;
}

static void spawn_pair(int base) {
entry_fn first = pick_worker(base & 1);
entry_fn second = pick_worker((base + 1) & 1);
pthread_create(&workers[base], 0, first, (void *)(long)(base + 1));
pthread_create(&workers[base + 1], 0, second, (void *)(long)(base + 2));
}

int main(void) {
spawn_pair(0);
spawn_pair(2);
shared_slots[2] = shared_sum;
pthread_join(workers[0], 0);
pthread_join(workers[1], 0);
pthread_join(workers[2], 0);
pthread_join(workers[3], 0);
return shared_slots[0] + shared_sum;
}
45 changes: 45 additions & 0 deletions src/sliced_mta/interproc.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
// interproc.c -- a second test exercising interprocedural slicing.
//
// A pool of worker threads reaches a shared write through a chain of helper
// calls, and main writes the same object concurrently. A separate, larger body
// of helper functions (helper_0..helper_n) does only local work and is never on
// any path to the shared state, so MSli slices it out: the slice keeps just the
// few functions that carry value flow to the racy accesses, while the race
// statements match the whole-program run. Still analyses in a second or two.
#include <pthread.h>

int shared; // the raced object

// --- the kept core: an interprocedural path to the shared write ---
static void write_shared(int v) { shared = v; }
static void mid_layer(int v) { write_shared(v + 1); }
static void entry_layer(int v) { mid_layer(v * 2); }

// --- a large independent helper body that never touches `shared` (sliced away) ---
static int helper_0(int x) { return x * 7 + 1; }
static int helper_1(int x) { return helper_0(x) - 3; }
static int helper_2(int x) { return helper_1(x) ^ x; }
static int helper_3(int x) { return helper_2(x) + helper_0(x); }
static int helper_4(int x) { return helper_3(x) * 2; }
static int helper_5(int x) { return helper_4(x) - helper_1(x); }
static int helper_6(int x) { return helper_5(x) + helper_2(x); }
static int helper_7(int x) { return helper_6(x) ^ helper_3(x); }
static void local_only(int seed) {
volatile int sink = 0;
for (int i = 0; i < 6; i++) sink += helper_7(seed + i);
}

void* worker(void* arg) {
local_only((int)(long)arg); // noise -> sliced away
entry_layer((int)(long)arg); // interprocedural path to `shared` -> race
return 0;
}

int main(void) {
pthread_t pool[3];
local_only(99); // noise -> sliced away
for (int i = 0; i < 3; i++) pthread_create(&pool[i], 0, worker, (void*)(long)i);
shared = 100; // main writes `shared` concurrently -> race
for (int i = 0; i < 3; i++) pthread_join(pool[i], 0);
return 0;
}
66 changes: 66 additions & 0 deletions src/sliced_mta/lock_paths.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,66 @@
#include <pthread.h>

typedef struct Item {
int count;
int shadow;
} Item;

pthread_mutex_t primary_lock;
pthread_mutex_t secondary_lock;
Item global_item;
int unlocked_total;

static void lock_primary(void) {
pthread_mutex_lock(&primary_lock);
}

static void unlock_primary(void) {
pthread_mutex_unlock(&primary_lock);
}

static void locked_increment(Item *item, int delta) {
lock_primary();
item->count += delta;
item->shadow = item->count + delta;
unlock_primary();
}

static void nested_locked_update(Item *item, int delta) {
pthread_mutex_lock(&primary_lock);
item->count += delta;
pthread_mutex_lock(&secondary_lock);
item->shadow += item->count;
pthread_mutex_unlock(&secondary_lock);
pthread_mutex_unlock(&primary_lock);
}

static void conditional_update(Item *item, int delta) {
if (delta & 1) {
pthread_mutex_lock(&primary_lock);
item->count += delta;
pthread_mutex_unlock(&primary_lock);
} else {
item->count += delta;
}
}

static void *locked_worker(void *arg) {
long id = (long)arg;
locked_increment(&global_item, (int)id);
nested_locked_update(&global_item, (int)id + 3);
conditional_update(&global_item, (int)id + 4);
unlocked_total += global_item.count;
return 0;
}

int main(void) {
pthread_t t1;
pthread_t t2;
pthread_create(&t1, 0, locked_worker, (void *)1);
pthread_create(&t2, 0, locked_worker, (void *)2);
conditional_update(&global_item, 8);
unlocked_total += global_item.shadow;
pthread_join(t1, 0);
pthread_join(t2, 0);
return unlocked_total;
}
26 changes: 26 additions & 0 deletions src/sliced_mta/no_data_race.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
// no_data_race.c -- a threaded program with NO data races.
//
// Two workers touch disjoint globals and main touches a third; no object is
// shared between concurrent threads, so both MSli and the whole-program FSAM
// report zero races. This exercises the pipeline's "no race pairs" paths (the
// slicing/PTA/final stages that early-out when the pre-analysis finds nothing).
#include <pthread.h>

int g_a; // written only by worker_a
int g_b; // written only by worker_b
int g_main; // touched only by main

static int compute(int x) { int s = x; for (int i = 0; i < 10; i++) s = s * 3 + i; return s; }

void* worker_a(void* arg) { g_a = compute((int)(long)arg); return 0; }
void* worker_b(void* arg) { g_b = compute((int)(long)arg) ^ 7; return 0; }

int main(void) {
pthread_t ta, tb;
pthread_create(&ta, 0, worker_a, (void*)1);
pthread_create(&tb, 0, worker_b, (void*)2);
g_main = 5; // main-only, races nothing
pthread_join(ta, 0);
pthread_join(tb, 0);
return 0;
}
Loading