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
26 changes: 1 addition & 25 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,28 +5,4 @@
GenSym is a symbolic-execution compiler that given an input LLVM IR program, it
produces code performing optimized parallel symbolic execution.

### Usage

upcoming

### Publications

* Towards Partially Evaluating Symbolic Interpreters for All
Shangyin Tan, Guannan Wei, Tiark Rompf
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), co-located with POPL 2022. Philadelphia, PA, USA
[PDF](http://continuation.passing.style/static/papers/pepm22.pdf)

* LLSC: A Parallel Symbolic Execution Compiler for LLVM IR (Demo Paper)
Guannan Wei, Shangyin Tan, Oliver Bračevac, Tiark Rompf
Proceedings of The 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2021)
[PDF (ACM DL)](https://dl.acm.org/doi/10.1145/3468264.3473108)

* Compiling Symbolic Execution with Staging and Algebraic Effect
Guannan Wei, Oliver Bračevac, Shangyin Tan, Tiark Rompf
Proceedings of the ACM on Programming Languages, Volume 4 (OOPSLA 2020). Online
[PDF (ACM DL)](https://dl.acm.org/doi/10.1145/3428232)

* Staged Abstract Interpreters: Fast and Modular Whole-Program Analysis via Meta-Programming
Guannan Wei, Yuxuan Chen, Tiark Rompf
Proceedings of the ACM on Programming Languages, Volume 3 (OOPSLA 2019). Athens, Greece
[PDF (ACM DL)](https://dl.acm.org/doi/10.1145/3360552)
This is the ICSE 23 artifact branch; see [instructions](https://github.com/Generative-Program-Analysis/icse23-artifact-evaluation) for more details.
44 changes: 44 additions & 0 deletions benchmarks/icse23/algorithms/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
SRC_FILES := $(wildcard ./*.c)

CC := clang-11

KLEE_INCL := /icse23/klee/include

GS_INCL := /icse23/GenSym/headers

FLAGS := -emit-llvm -O0 -Xclang -disable-O0-optnone -c
KLEE_FLAGS := -D KLEE -g -I $(KLEE_INCL)
GS_FLAGS := -D GENSYM -fno-discard-value-names -S -I $(GS_INCL)
LLSC_FLAGS := -D LLSC -fno-discard-value-names -S

KLEE_TARGET := $(SRC_FILES:%.c=%.bc)

KLEE_REPLAY_TARGET := $(SRC_FILES:%.c=%-replay)

KLEE_GEN := $(wildcard ./klee-*)

GS_TARGET := $(SRC_FILES:%.c=%.ll)

LLSC_TARGET := $(SRC_FILES:%.c=%_llsc.ll)

all: gensym klee llsc

gensym: $(GS_TARGET)
klee: $(KLEE_TARGET)
llsc: $(LLSC_TARGET)
klee-exe: $(KLEE_REPLAY_TARGET)

$(KLEE_TARGET): %.bc : %.c
$(CC) $(KLEE_FLAGS) $(FLAGS) -o $@ $<

$(KLEE_REPLAY_TARGET): %-replay : %.c
$(CC) $(KLEE_FLAGS) -o $@ $< -lkleeRuntest

$(GS_TARGET): %.ll : %.c
$(CC) $(GS_FLAGS) $(FLAGS) -o $@ $<

$(LLSC_TARGET): %_llsc.ll : %.c
$(CC) $(LLSC_FLAGS) $(FLAGS) -o $@ $<

clean:
$(RM) -rf $(KLEE_TARGET) $(KLEE_REPLAY_TARGET) $(KLEE_GEN) $(GS_TARGET) $(LLSC_TARGET)
42 changes: 42 additions & 0 deletions benchmarks/icse23/algorithms/bubblesort.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
#ifdef KLEE
#include "klee/klee.h"
#endif
#ifdef GENSYM
#include "gensym_client.h"
#endif

#define SIZE 6

void bubble_sort(int *d, int n)
{
for (int k = 1; k < n; k++)
{
for (int i = 1; i < n; i++)
{
if (d[i] < d[i - 1])
{
int temp = d[i];
d[i] = d[i - 1];
d[i - 1] = temp;
}
}
}
}

int main()
{
int data[SIZE];
#ifdef KLEE
klee_make_symbolic(data, sizeof data, "data");
#endif
#ifdef LLSC
make_symbolic(data, sizeof(int) * SIZE);
#endif
#ifdef GENSYM
for (int i = 0; i < SIZE; i++)
make_symbolic_whole(data + i, sizeof(int));
#endif

bubble_sort(data, SIZE);
return 0;
}
79 changes: 79 additions & 0 deletions benchmarks/icse23/algorithms/kmpmatcher.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
#ifdef KLEE
#include "klee/klee.h"
#endif
#ifdef GENSYM
#include "gensym_client.h"
#endif

#define SIZE 10

int pi[10];
int lt, lp;

void compute_prefix_function(char * P)
{
int q = 0;
pi[0] = 0;

for (int i = 1; i < lp; i++)
{
while (q > 0 && P[i] != P[q])
{
q = pi[q - 1];
}

if (P[i] == P[q])
{
q++;
}

pi[i] = q;
}
}

void KMP_matcher(char * P, char * T)
{
compute_prefix_function(P);

int q = 0;

for (int i = 0; i < lt; i++)
{
while (q > 0 && T[i] != P[q])
{
q = pi[q - 1];
}

if (T[i] == P[q])
{
q++;
}

if (q == lp)
{
printf("matched with shift %d\n", i - lp + 1);
q = pi[q - 1];
}
}
}

int main()
{
char P[11] = "helloworld";
char T[SIZE];
#ifdef KLEE
klee_make_symbolic(T, SIZE, "T");
#endif
#ifdef LLSC
make_symbolic(T, SIZE);
#endif
#ifdef GENSYM
make_symbolic(T, SIZE);
#endif
lt = SIZE-1;
lp = 10;

KMP_matcher(P, T);

return 0;
}
56 changes: 56 additions & 0 deletions benchmarks/icse23/algorithms/knapsack.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
#ifdef KLEE
#include "klee/klee.h"
#endif
#ifdef GENSYM
#include "gensym_client.h"
#endif

#include <stdio.h>

#define N 4

int max(int a, int b) { return (a > b) ? a : b; }

int knapSack(int W, int wt[], int val[], int n)
{
// Base Case
if (n == 0 || W == 0) return 0;

// If weight of the nth item is more than
// Knapsack capacity W, then this item cannot
// be included in the optimal solution
if (wt[n - 1] > W)
return knapSack(W, wt, val, n - 1);

// Return the maximum of two cases:
// (1) nth item included
// (2) not included
else
return max(
val[n - 1]
+ knapSack(W - wt[n - 1],
wt, val, n - 1),
knapSack(W, wt, val, n - 1));
}

// Driver program to test above function
int main()
{
//int val[N] = { 60, 100, 120, 130 };
int val[N];
val[0] = 60; val[1] = 100; val[2] = 120; val[3] = 130;
int wt[N];
#ifdef KLEE
klee_make_symbolic(wt, sizeof(int) * N, "wt");
#endif
#ifdef LLSC
make_symbolic(wt, sizeof(int) * N);
#endif
#ifdef GENSYM
for (int i = 0; i < N; i++)
make_symbolic_whole(wt + i, sizeof(int));
#endif
int W = 50;
knapSack(W, wt, val, N);
return 0;
}
95 changes: 95 additions & 0 deletions benchmarks/icse23/algorithms/mergesort.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
#ifdef KLEE
#include "klee/klee.h"
#endif
#ifdef GENSYM
#include "gensym_client.h"
#endif

#define SIZE 7

int d[SIZE];

//https://www.geeksforgeeks.org/merge-sort/
void merge(int arr[], int l, int m, int r)
{
int i, j, k;
int n1 = m - l + 1;
int n2 = r - m;

/* create temp arrays */
int* L = malloc(n1 * sizeof(int));
int* R = malloc(n2 * sizeof(int));

/* Copy data to temp arrays L[] and R[] */
for (i = 0; i < n1; i++)
L[i] = arr[l + i];
for (j = 0; j < n2; j++)
R[j] = arr[m + 1 + j];

/* Merge the temp arrays back into arr[l..r]*/
i = 0; // Initial index of first subarray
j = 0; // Initial index of second subarray
k = l; // Initial index of merged subarray
while (i < n1 && j < n2) {
if (L[i] <= R[j]) {
arr[k] = L[i];
i++;
}
else {
arr[k] = R[j];
j++;
}
k++;
}

/* Copy the remaining elements of L[], if there are any */
while (i < n1) {
arr[k] = L[i];
i++;
k++;
}

/* Copy the remaining elements of R[], if there
are any */
while (j < n2) {
arr[k] = R[j];
j++;
k++;
}
free(L);
free(R);
}

/* l is for left index and r is right index of the
sub-array of arr to be sorted */
void mergeSort(int arr[], int l, int r)
{
if (l < r) {
// Same as (l+r)/2, but avoids overflow for
// large l and h
int m = l + (r - l) / 2;

// Sort first and second halves
mergeSort(arr, l, m);
mergeSort(arr, m + 1, r);

merge(arr, l, m, r);
}
}

int main()
{
#ifdef KLEE
klee_make_symbolic(d, sizeof d, "data");
#endif
#ifdef LLSC
make_symbolic(d, sizeof(int) * SIZE);
#endif
#ifdef GENSYM
for (int i = 0; i < SIZE; i++) {
make_symbolic_whole(d+i, sizeof(int));
}
#endif
mergeSort(d, 0, SIZE - 1);
return 0;
}
Loading