Skip to content

Icse23 cherry pick #38

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 32 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
218b0ec
add kick the tires check
Kraks Jan 25, 2023
c901ebd
update docker
Kraks Jan 25, 2023
73a9edc
algo benchmarks
Kraks Jan 25, 2023
c3aaa80
fix
Kraks Jan 25, 2023
8766ff3
benchmark for llsc
Kraks Jan 26, 2023
6811fb9
missing
Kraks Jan 26, 2023
fa97681
fix
Kraks Jan 26, 2023
00c5920
sync
Kraks Jan 26, 2023
b0b818a
fix typo
Kraks Jan 26, 2023
215f7d6
add --repeat to RunGenSym
songlinj-purdue Jan 24, 2023
6dfd619
add compilation script
songlinj-purdue Jan 26, 2023
1fd8dd9
rename compilation script
songlinj-purdue Jan 26, 2023
0933192
remove artifact script, add prepare to docker init
songlinj-purdue Jan 27, 2023
81701e6
coreutils gcov in docker
Kraks Jan 27, 2023
12d8d87
misc
Kraks Jan 27, 2023
7030c73
compile coreutils facility
Kraks Jan 27, 2023
880ef88
not using all cores
Kraks Jan 27, 2023
4616e39
add benchmarks
Jan 5, 2023
f796e7e
update scripts
Jan 27, 2023
e2ec6af
restore file system to icse initial submission
Jan 27, 2023
7a8f33f
Revert "add benchmarks"
PROgram52bc Jan 28, 2023
6d8fc1b
disable fork
Kraks Jan 28, 2023
7c9bddc
update
Kraks Jan 28, 2023
e8b323d
update
Kraks Jan 29, 2023
0bc2236
update readme
Kraks Jan 29, 2023
61c8c35
update lms to use graph scheduler
songlinj-purdue Feb 9, 2023
a4c37b6
update lms-clean
Kraks Feb 20, 2023
b729f83
Merge branch 'main' into icse23-cherry-pick
Kraks Feb 20, 2023
45da968
revert some changes
Kraks Feb 20, 2023
7d699d8
revert more
Kraks Feb 20, 2023
8356ef4
comment coreutils cases
Kraks Feb 23, 2023
7e7340a
comment icse tests
Kraks Apr 11, 2023
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
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;
}
63 changes: 63 additions & 0 deletions benchmarks/icse23/algorithms/nqueen.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
#ifdef KLEE
#include "klee/klee.h"
#endif
#ifdef GENSYM
#include "gensym_client.h"
#endif

// https://www.geeksforgeeks.org/n-queen-problem-backtracking-3/
#define N 5
#include <stdbool.h>
#include <stdio.h>

bool isSafe(int board[N][N], int row, int col) {
int i, j;
for (i = 0; i < col; i++)
if (board[row][i])
return false;
for (i = row, j = col; i >= 0 && j >= 0; i--, j--)
if (board[i][j])
return false;
for (i = row, j = col; j >= 0 && i < N; i++, j--)
if (board[i][j])
return false;
return true;
}

bool solveNQUtil(int board[N][N], int col) {
if (col >= N) return true;
for (int i = 0; i < N; i++) {
if (isSafe(board, i, col)) {
board[i][col] = 1;
if (solveNQUtil(board, col + 1))
return true;
board[i][col] = 0; // BACKTRACK
}
}
return false;
}

bool solveNQ() {
int board[N][N];
#ifdef KLEE
klee_make_symbolic(board, sizeof(int) * N * N, "board");
#endif
#ifdef LLSC
make_symbolic(board, sizeof(int) * N * N);
#endif
#ifdef GENSYM
for (int i = 0; i < N * N; i++)
make_symbolic_whole((int*)board + i, sizeof(int));
#endif
if (solveNQUtil(board, 0) == false) {
return false;
}

return true;
}

int main()
{
solveNQ();
return 0;
}
Loading