diff --git a/README.md b/README.md index 20759fecb..87f4f0c0d 100644 --- a/README.md +++ b/README.md @@ -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. diff --git a/benchmarks/icse23/algorithms/Makefile b/benchmarks/icse23/algorithms/Makefile new file mode 100644 index 000000000..e33faa17b --- /dev/null +++ b/benchmarks/icse23/algorithms/Makefile @@ -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) diff --git a/benchmarks/icse23/algorithms/bubblesort.c b/benchmarks/icse23/algorithms/bubblesort.c new file mode 100644 index 000000000..a18db256c --- /dev/null +++ b/benchmarks/icse23/algorithms/bubblesort.c @@ -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; +} diff --git a/benchmarks/icse23/algorithms/kmpmatcher.c b/benchmarks/icse23/algorithms/kmpmatcher.c new file mode 100644 index 000000000..2a319906f --- /dev/null +++ b/benchmarks/icse23/algorithms/kmpmatcher.c @@ -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; +} diff --git a/benchmarks/icse23/algorithms/knapsack.c b/benchmarks/icse23/algorithms/knapsack.c new file mode 100644 index 000000000..3b25a83f7 --- /dev/null +++ b/benchmarks/icse23/algorithms/knapsack.c @@ -0,0 +1,56 @@ +#ifdef KLEE +#include "klee/klee.h" +#endif +#ifdef GENSYM +#include "gensym_client.h" +#endif + +#include + +#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; +} diff --git a/benchmarks/icse23/algorithms/mergesort.c b/benchmarks/icse23/algorithms/mergesort.c new file mode 100644 index 000000000..59bf95981 --- /dev/null +++ b/benchmarks/icse23/algorithms/mergesort.c @@ -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; +} diff --git a/benchmarks/icse23/algorithms/nqueen.c b/benchmarks/icse23/algorithms/nqueen.c new file mode 100644 index 000000000..a27fbc455 --- /dev/null +++ b/benchmarks/icse23/algorithms/nqueen.c @@ -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 +#include + +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; +} diff --git a/benchmarks/icse23/algorithms/quicksort.c b/benchmarks/icse23/algorithms/quicksort.c new file mode 100644 index 000000000..62fc4e5f9 --- /dev/null +++ b/benchmarks/icse23/algorithms/quicksort.c @@ -0,0 +1,50 @@ +#ifdef KLEE +#include "klee/klee.h" +#endif +#ifdef GENSYM +#include "gensym_client.h" +#endif + +#define SIZE 7 + +int d[SIZE]; + +void qsort(int l, int r) +{ + if (l < r) + { + int x = d[r]; + int j = l - 1; + + for (int i = l; i <= r; i++) + { + if (d[i] <= x) + { + j++; + int temp = d[i]; + d[i] = d[j]; + d[j] = temp; + } + } + + qsort(l, j - 1); + qsort(j + 1, 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 + qsort(0, SIZE-1); + return 0; +} diff --git a/build.sbt b/build.sbt index 4eeb4e1de..166e540d8 100644 --- a/build.sbt +++ b/build.sbt @@ -32,7 +32,7 @@ scalacOptions ++= Seq( autoCompilerPlugins := true //https://www.scala-sbt.org/release/docs/Running-Project-Code.html -fork := true +//fork := true run / javaOptions ++= Seq( "-Xms4G", "-Xmx32G", @@ -60,5 +60,5 @@ lazy val lms = ProjectRef(file("./third-party/lms-clean"), "lms-clean") lazy val gensym = (project in file(".")).dependsOn(lms % "test->test; compile->compile") .configs(Bench) .settings(inConfig(Bench)(Defaults.testSettings)) - .settings(assembly / mainClass := Some("gensym.RunGenSym")) - + .settings(assembly / mainClass := Some("gensym.RunGenSym"), + assembly / test := {}) diff --git a/docker-image/Dockerfile b/docker-image/Dockerfile index 68af1f6d4..44d896aa9 100644 --- a/docker-image/Dockerfile +++ b/docker-image/Dockerfile @@ -12,6 +12,8 @@ VOLUME ["/var/tmp"] # Initial setup RUN mkdir /icse23 COPY init_setup.sh /icse23/init_setup.sh +COPY sync.sh /icse23/sync.sh +COPY paper.pdf /icse23/paper.pdf RUN bash /icse23/init_setup.sh ENV PATH="/icse23/scala-2.12.10/bin:${PATH}" diff --git a/docker-image/init_setup.sh b/docker-image/init_setup.sh index 706d3a301..be55e386c 100644 --- a/docker-image/init_setup.sh +++ b/docker-image/init_setup.sh @@ -1,6 +1,6 @@ # General dependencies apt-get update -DEBIAN_FRONTEND=noninteractive apt-get install -y git g++ cmake bison flex wget libboost-all-dev python perl minisat curl gnupg2 locales openjdk-8-jdk vim build-essential file g++-multilib gcc-multilib libcap-dev libgoogle-perftools-dev libncurses5-dev libsqlite3-dev libtcmalloc-minimal4 python3-pip unzip graphviz doxygen clang-11 llvm-11 llvm-11-dev llvm-11-tools cloc +DEBIAN_FRONTEND=noninteractive apt-get install -y git g++ cmake bison flex wget libboost-all-dev python perl minisat curl gnupg2 locales openjdk-8-jdk vim build-essential file g++-multilib gcc-multilib libcap-dev libgoogle-perftools-dev libncurses5-dev libsqlite3-dev libtcmalloc-minimal4 python3-pip unzip graphviz doxygen clang-11 llvm-11 llvm-11-dev llvm-11-tools cloc zsh autoconf automake gperf rsync gettext autopoint bison texinfo # Setup the locale locale-gen en_US.UTF-8 @@ -40,7 +40,6 @@ cp bin/libz3.so /usr/lib/x86_64-linux-gnu/ ldconfig # Python - pip install --upgrade pip pip install pandas @@ -66,10 +65,31 @@ git clone -j 8 -b icse23 --recurse-submodules https://github.com/Generative-Prog # Benchmarks cd /icse23/GenSym/benchmarks -git clone -j 4 https://github.com/Generative-Program-Analysis/coreutils-linked.git coreutils +git clone -j 4 -b icse23 https://github.com/Generative-Program-Analysis/coreutils-linked.git coreutils +make +cd /icse23/GenSym/benchmarks/icse23/algorithms make +# Coreutils with gcov +# see /icse23/coreutils-src/obj-gcov/src +cd /icse23 +git clone https://github.com/coreutils/coreutils.git -j10 coreutils-src +cd coreutils-src +git checkout 8d13292 -b test-8.32 +./bootstrap +mkdir obj-gcov +cd obj-gcov +FORCE_UNSAFE_CONFIGURE=1 ../configure --disable-nls CFLAGS="-g -fprofile-arcs -ftest-coverage -Wno-stringop-overflow" +make -j10 + # Top-level instructions cd /icse23 git clone https://github.com/Generative-Program-Analysis/icse23-artifact-evaluation +# Prepare Libraries for separate compilation +cd /icse23/GenSym +/icse23/icse23-artifact-evaluation/table4/compilation_test.py prepare --no-build + +# Generate external +cd /icse23/GenSym +sbt "runMain gensym.GenerateExternal" diff --git a/docker-image/sync.sh b/docker-image/sync.sh new file mode 100644 index 000000000..19f34727f --- /dev/null +++ b/docker-image/sync.sh @@ -0,0 +1,12 @@ +# Sync GenSym +cd /icse23/GenSym +git pull origin icse23 + +# Sync benchmarks +cd /icse23/GenSym/benchmarks/coreutils +git pull origin icse23 + +# Sync doc + +cd /icse23/icse23-artifact-evaluation +git pull origin main diff --git a/headers/gensym/cli.hpp b/headers/gensym/cli.hpp index 3c2576662..23b1be99c 100644 --- a/headers/gensym/cli.hpp +++ b/headers/gensym/cli.hpp @@ -160,7 +160,7 @@ inline void handle_cli_args(int argc, char** argv) { break; } case 13: - initial_fs = set_file(initial_fs, std::string("/") + optarg, set_file_type(make_SymFile(optarg, default_sym_file_size), S_IFREG)); + initial_fs = set_file(initial_fs, std::string("/") + optarg, make_SymFile(optarg, default_sym_file_size)); initial_fs.sym_objs = initial_fs.sym_objs.push_back(SymObj(std::string(optarg) + "-data", default_sym_file_size, false)); initial_fs.sym_objs = initial_fs.sym_objs.push_back(SymObj(std::string(optarg) + "-data-stat", stat_size, false)); n_sym_files++; diff --git a/headers/gensym/defs.hpp b/headers/gensym/defs.hpp index d89380dae..544634a60 100644 --- a/headers/gensym/defs.hpp +++ b/headers/gensym/defs.hpp @@ -30,16 +30,16 @@ struct NullDerefException { immer::box ss; }; -inline int vararg_id = -1; +extern int vararg_id; // Default bitwidth when creating integers or symbolic values -inline unsigned int default_bw = 32; +extern unsigned int default_bw; // The bitwidth of addresses (64 by default) -inline unsigned int addr_bw = 64; -inline unsigned int addr_index_bw = addr_bw; +extern unsigned int addr_bw; +extern unsigned int addr_index_bw; // Used to assign a unique ID for each SymV value -inline std::atomic g_sym_id = 0; +extern std::atomic g_sym_id; /* Stat */ @@ -68,52 +68,52 @@ inline atomic_ulong num_check_model_pc_size = 0; /* Global options */ -inline bool use_thread_pool = false; +extern bool use_thread_pool; // The number of total threads (including the main thread) -inline unsigned int n_thread = 1; +extern unsigned int n_thread; // The number of queues when using thread pool -inline unsigned int n_queue = 1; +extern unsigned int n_queue; // Use solver or not -inline bool use_solver = true; +extern bool use_solver; // Indicates if there is only one solver instance -inline bool use_global_solver = false; +extern bool use_global_solver; // Use hash consing or not -inline bool use_hashcons = true; +extern bool use_hashcons; // Use object caching or not -inline bool use_objcache = true; +extern bool use_objcache; // Use counterexample caching or not -inline bool use_cexcache = true; +extern bool use_cexcache; // Use branch query caching or not -inline bool use_brcache = true; +extern bool use_brcache; // Use constraint independence resolving or not -inline bool use_cons_indep = true; +extern bool use_cons_indep; // Only generate testcases for states that cover new blocks or not -inline bool only_output_covernew = false; +extern bool only_output_covernew; // Output ktest format or not -inline bool output_ktest = false; +extern bool output_ktest; // Prefer generating human-readable file test cases -inline bool readable_file_tests = false; +extern bool readable_file_tests; // Only compatible when using KLEE's POSIX model at the momemt (?) // Simulate possible failure in external functions (results in state forking) // Currently including malloc, calloc, memalign. GW: what else? -inline bool exlib_failure_branch = false; +extern bool exlib_failure_branch; // Timeout in seconds (one hour by default) -inline unsigned int timeout = 3600; +extern unsigned int timeout; // Print the number of executed instructions -inline bool print_inst_cnt = false; +extern bool print_inst_cnt; // Print block/branch coverage detail at the end of execution -inline bool print_cov_detail = false; +extern bool print_cov_detail; // Print detailed log // 0 - disabled // 1 - print every second // 2 - print at the end of execution -inline uint32_t print_detailed_log = 0; +extern uint32_t print_detailed_log; // The maximum size of symbolic location (used in memory read) -inline unsigned int max_sym_array_size = 0; +extern unsigned int max_sym_array_size; // The upper bound for the number of feasible symbolic size on malloc and memcpy -inline unsigned int max_size_bound = 400; +extern unsigned int max_size_bound; // Use simplification when constructing SymV values -inline bool use_symv_simplify = false; +extern bool use_symv_simplify; // Output directory name inline std::string output_dir_str = std::string("gensym-") + get_current_datetime(); @@ -124,7 +124,7 @@ inline std::string output_log_str; // Output log file stream inline std::ofstream gs_log; // Disable output log in stdout -inline bool stdout_log = true; +extern bool stdout_log; enum class SearcherKind { randomPath, randomWeight }; // The path searcher to be used diff --git a/headers/gensym/external_shared.hpp b/headers/gensym/external_shared.hpp index 5012cbe7d..cb3386245 100644 --- a/headers/gensym/external_shared.hpp +++ b/headers/gensym/external_shared.hpp @@ -80,8 +80,7 @@ inline T __sym_exit(SS& state, List& args, __Cont k) { set_exit_code(status); return k(state, nullptr); } else { - cov().print_all(true); - cov().print_all(true, std::cout); + cov().print_all(); _exit(status); } } @@ -121,27 +120,48 @@ inline std::string get_string_at(SS& state, PtrVal ptr) { return proj_List_String(get_sym_string_at(state, ptr)); } + +inline std::string get_concrete_file_path(PtrVal ptr, SS& state) { + std::string name; + ASSERT(std::dynamic_pointer_cast(ptr) != nullptr, "Non-location value"); + /* TODO: more comprehensive concretization, do forks eventually <2022-08-25, David Deng> */ + if (std::dynamic_pointer_cast(state.at_simpl(ptr))) { + std::cout << "symbolic file path. Concretize to A" << std::endl; + return "-"; + } + char c = proj_IntV_char(state.at_simpl(ptr)); // c = *ptr + while (c != '\0') { + name += c; + ptr = ptr + 1; + c = proj_IntV_char(state.at_simpl(ptr)); // c = *ptr + } + return name; +} + inline UIntData get_int_arg(SS& state, PtrVal x) { - auto x_i = x->to_IntV(); + auto x_i = std::dynamic_pointer_cast(x); // Todo: add this concretization tp path constraints - if (x_i) return x_i->as_signed(); - auto sym_v = x->to_SymV(); - ASSERT(sym_v != nullptr, "get value of non-symbolic variable"); - std::pair res = get_sat_value(state.get_PC(), sym_v); - ASSERT(res.first, "Unfeasible path"); - return res.second; + if (x_i) { + return x_i->as_signed(); + } else { + auto sym_v = std::dynamic_pointer_cast(x); + ASSERT(sym_v, "get value of non-symbolic variable"); + std::pair res = get_sat_value(state.get_PC(), sym_v); + ASSERT(res.first, "Un-feasible path"); + return res.second; + } } inline double get_float_arg(SS& state, PtrVal x) { - // Note: since we don't have symbolic floating point numbers, we just - // extract the concrete floats here. - return (double)proj_FloatV(x); + auto x_f = std::dynamic_pointer_cast(x); + ASSERT(x_f, "getting Non-FloatV"); + return (double)x_f->f; } inline std::string get_string_arg(SS& state, PtrVal ptr) { std::string name; char c = get_int_arg(state, state.at_simpl(ptr)); // c = *ptr - ASSERT(ptr->to_LocV() != nullptr, "Non-location value"); + ASSERT(std::dynamic_pointer_cast(ptr) != nullptr, "Non-location value"); while (c != '\0') { name += c; ptr = ptr + 1; @@ -176,9 +196,9 @@ inline void copy_state2native(SS& state, PtrVal ptr, char* buf, int size) { inline char* get_pointer_arg(SS& state, PtrVal loc) { if (is_LocV_null(loc)) return nullptr; - ASSERT(loc->to_LocV(), "Non LocV"); + ASSERT(std::dynamic_pointer_cast(loc), "Non LocV"); size_t count = get_pointer_realsize(loc); - char* buf = (char*)malloc(count); + char * buf = (char*)malloc(count); copy_state2native(state, loc, buf, count); return buf; } @@ -186,7 +206,7 @@ inline char* get_pointer_arg(SS& state, PtrVal loc) { template inline T __print_string(SS& state, List& args, __Cont k) { PtrVal x = args.at(0); - if (x->to_LocV()) { + if (std::dynamic_pointer_cast(x)) { std::cout << get_string_at(state, x); return k(state, make_IntV(0)); } @@ -406,7 +426,7 @@ template inline T __gs_warning_once(SS& state, List& args, __Cont k) { static std::set warned; PtrVal x = args.at(0); - if (x->to_LocV()) { + if (std::dynamic_pointer_cast(x)) { std::string message = get_string_at(state, x); if (warned.count(message) == 0) { warned.insert(message); diff --git a/runtime/include/gensym/runtime.hpp b/runtime/include/gensym/runtime.hpp new file mode 100644 index 000000000..979bdb4e4 --- /dev/null +++ b/runtime/include/gensym/runtime.hpp @@ -0,0 +1,9 @@ +#pragma once + +// Minimal public runtime header. +// We intentionally keep this small first. +// Later we will add declarations here step by step. + +namespace gensym_runtime { + void runtime_link_test(); +} diff --git a/runtime/src/defs.cpp b/runtime/src/defs.cpp new file mode 100644 index 000000000..d3b10a4c0 --- /dev/null +++ b/runtime/src/defs.cpp @@ -0,0 +1,37 @@ +#include + +std::atomic g_sym_id = 0; +int vararg_id = -1; + +unsigned int default_bw = 32; +unsigned int addr_bw = 64; +unsigned int addr_index_bw = addr_bw; + +bool use_thread_pool = false; +unsigned int n_thread = 1; +unsigned int n_queue = 1; + +bool use_solver = true; +bool use_global_solver = false; +bool use_hashcons = true; +bool use_objcache = true; +bool use_cexcache = true; +bool use_brcache = true; +bool use_cons_indep = true; +bool only_output_covernew = false; +bool output_ktest = false; +bool readable_file_tests = false; + +unsigned int timeout = 3600; + +bool exlib_failure_branch = false; + +bool print_inst_cnt = false; +bool print_cov_detail = false; +uint32_t print_detailed_log = 0; + +unsigned int max_sym_array_size = 0; +unsigned int max_size_bound = 400; +bool use_symv_simplify = false; + +bool stdout_log = true; diff --git a/runtime/src/runtime.cpp b/runtime/src/runtime.cpp new file mode 100644 index 000000000..8a78f5bb8 --- /dev/null +++ b/runtime/src/runtime.cpp @@ -0,0 +1,5 @@ +#include + +namespace gensym_runtime { + void runtime_link_test() {} +} diff --git a/scripts/RQ4.sh b/scripts/RQ4.sh new file mode 100644 index 000000000..682827acc --- /dev/null +++ b/scripts/RQ4.sh @@ -0,0 +1,171 @@ +#!/usr/bin/env bash +# Uses the test_benchmark script to run experiment. Specifies programs, options, and collect output + +################### +# Static Config # +################### + +PROJ_DIR=`realpath ..` # project root directory +LOG_DIR=`realpath ./logs` # directory to store the log files +BM_SCRIPT=`realpath ./test_benchmark` # the test_benchmark script +export BM_EXPAND_SCRIPT=`realpath ./braces_expand.py` # the script to perform braces expansion, will be detected by BM_SCRIPT +declare -A inputs=( +[posix]=`realpath ../benchmarks/icse23/gensym_posix/` +[uclibc]=`realpath ../benchmarks/icse23/gensym_uclibc/` +) +GCOV_DIR=`realpath ../gcov` # TODO: point to gcov executables +ENV_SCRIPT="~/sai_install/env.sh" # TODO (OPTIONAL): set up PATH, CPLUS_INCLUDE_PATH, LD_LIBRARY_PATH, LIBRARY_PATH, etc. + +#################### +# Dynamic Config # +#################### + +# whether to generate external lib at the beginning of the experiment +GEN_EXTERNAL=true +# --no-scala for BM_SCRIPT +BM_SCALA=true +# --no-cpp for BM_SCRIPT +BM_CPP=true +# --no-runtime for BM_SCRIPT +BM_RUNTIME=true +# whether to use gcov to measure concrete coverage, require --output-ktest in RUNTIME_OPTION +GCOV=false +# extra arguments passed to BM_SCRIPT +BM_OPTIONS="--njobs 192 --timeout 500" +# global options for the final executable, appended to all benchmarks +RUNTIME_OPTION="--solver=z3 --thread=1 --search=random-path --output-ktest --output-tests-cov-new" +# use the hash of the specified branch. Only affect the result of runtime, but not scala/cpp compilation. +USE_BRANCH="" + +# candidate source files in ${inputs}, .ll is appended +candidates=( +base32 +base64 +comm +cut +dirname +echo +fold +pathchk +expand +paste +) + +# runtime options for executable +# for path comparison + +declare -A options=( +[base32_posix]='--argv="prg -sym-stdout -sym-stdin 2 -sym-files 1 12 -d A"' +[base32_uclibc]='--argv="prg -d A" --sym-stdin 2 --sym-stdout --sym-file-size=12 --add-sym-file A' +[base64_posix]='--argv="prg -sym-stdout -sym-stdin 2 -sym-files 1 11 -d A"' +[base64_uclibc]='--argv="prg -d A" --sym-stdin 2 --sym-stdout --sym-file-size=11 --add-sym-file A' +[comm_posix]='--argv="prg -sym-stdout -sym-stdin 2 -sym-files 2 4 A B"' +[comm_uclibc]='--argv="prg A B" --sym-stdin 2 --sym-stdout --sym-file-size=4 --add-sym-file=A --add-sym-file=B' +[cut_posix]='--argv="prg -sym-stdout -sym-stdin 2 -sym-files 1 15 -b 1-2 A"' +[cut_uclibc]='--argv="prg -b 1-2 A" --sym-stdin 2 --sym-stdout --sym-file-size=15 --add-sym-file A' +[dirname_posix]='--argv="prg -sym-stdout -sym-stdin 2 -sym-arg 15"' +[dirname_uclibc]='--argv="prg #15" --sym-stdin 2 --sym-stdout' +[echo_posix]='--argv="prg -sym-stdout -sym-stdin 2 -sym-arg 11"' +[echo_uclibc]='--argv="prg #11" --sym-stdin 2 --sym-stdout' +[fold_posix]='--argv="prg -sym-stdout -sym-stdin 2 -sym-files 1 7 A"' +[fold_uclibc]='--argv="prg A" --sym-stdout --sym-stdin 2 --sym-file-size=7 --add-sym-file A' +[pathchk_posix]='--argv="prg --sym-stdin 2 --sym-stdout -sym-arg 2"' +[pathchk_uclibc]='--argv="prg #2" --sym-stdin 2 --sym-stdout' +[expand_posix]='--argv="prg -sym-stdout -sym-stdin 2 -sym-files 1 8 A"' +[expand_uclibc]='--argv="prg A" --sym-stdout --sym-stdin 2 --sym-file-size=8 --add-sym-file A' +[paste_posix]='--argv="prg -sym-stdout -sym-stdin 2 -sym-files 3 5 -s A B C"' +[paste_uclibc]='--argv="prg -s A B C" --sym-stdout --sym-stdin 2 --sym-file-size=5 --add-sym-file=A --add-sym-file=B --add-sym-file=C' +) + +################### +# Script starts # +################### + +mkdir -p $LOG_DIR +if [ -f "$ENV_SCRIPT" ]; then + source "$ENV_SCRIPT" # set up PATH, CPLUS_INCLUDE_PATH, LD_LIBRARY_PATH, LIBRARY_PATH +fi +TS=`date +%y%m%d%H%M%S` # get a time stamp +cd $PROJ_DIR + +if [ "${BM_SCALA}" = "false" ]; then + BM_OPTIONS="${BM_OPTIONS} --no-scala" +fi +if [ "${BM_CPP}" = "false" ]; then + BM_OPTIONS="${BM_OPTIONS} --no-cpp" +fi +if [ "${BM_RUNTIME}" = "false" ]; then + BM_OPTIONS="${BM_OPTIONS} --no-runtime" +fi + +if [ -z "$USE_BRANCH" ]; then + USE_BRANCH=HEAD +else + echo [run_experiment] Using branch hash $USE_BRANCH. + echo [run_experiment] WARNING: overriding the branch hash may result in inconsistent compilation result, should make sure the previously compiled programs are correct. +fi + +COMMIT_HASH=h_$(git rev-parse --short "$USE_BRANCH") +echo [run_experiment] hash: $COMMIT_HASH + +# generate external wrappers +if [ "${GEN_EXTERNAL}" = "true" ]; then + echo [run_experiment] generating external functions... + sbt "runMain gensym.GenerateExternal" + # bloop run sai -m gensym.GenerateExternal +fi + +# iterate through each set of input LLVM files (e.g. posix and uclibc) +for i in "${!inputs[@]}"; do + idir="${inputs[$i]}" # the input LLVM directory + + # set up output destination + OUTFILE="${LOG_DIR}/full_${TS}_${COMMIT_HASH}_${i}.log" + OUTFILERUNTIME="${LOG_DIR}/runtime_${TS}_${COMMIT_HASH}_${i}.log" + + # duplicate all output to OUTFILE + exec 1> >(tee -ia ${OUTFILE}) + exec 2> >(tee -ia ${OUTFILE} >&2) + + echo [run_experiment] OUTFILE: $OUTFILE + echo [run_experiment] OUTFILERUNTIME: $OUTFILERUNTIME + + echo "name,opt,time,blocks,br,paths,threads,task-in-q,queries" >> ${OUTFILERUNTIME} + for f in ${candidates[@]}; do + if [ -v "options[${f}_${i}]" ]; then + echo [run_experiment] using input specific option with key: ${f}_${i} + option="${options[${f}_${i}]} $RUNTIME_OPTION" + elif [ -v "options[${f}]" ]; then + echo [run_experiment] using generic input option with key: ${f} + option="${options[${f}]} $RUNTIME_OPTION" + else + echo [run_experiment] no option found for input file ${f} of type ${i} + echo [run_experiment] HINT: add an item to the "options=(...)" array with key [${f}] or [${f}_${i}] + option="$RUNTIME_OPTION" + fi + # write only succinct output to OUTFILERUNTIME + BM_OPTIONS="${BM_OPTIONS} --succinct-log ${OUTFILERUNTIME}" + HEAD=${COMMIT_HASH}_${f}_${i} + ${BM_SCRIPT} ${BM_OPTIONS} -- $idir/$f.ll $HEAD $option + if [ $? -eq 0 ] && [ "$GCOV" = "true" ]; then + ( cd gs_gen/$HEAD/tests + gcov_file=${gcov_gcda_map[$f]:-$f} + pwd + echo performing gcov measurement... + rm -f $GCOV_DIR/src/*.gcda + klee-replay $GCOV_DIR/src/$f *.ktest + cd $GCOV_DIR + pwd + echo f: $f + echo gcov_file: $gcov_file + gcov src/${gcov_file} | tee >(grep -A1 '^File' | grep -vx '\-\-' - >> $OUTFILERUNTIME) + ) + fi + done + # redirect output back to stdout + exec 1> /dev/tty + exec 2> /dev/tty + echo [run_experiment] output written to ${OUTFILE} + echo [run_experiment] runtime output written to ${OUTFILERUNTIME} + echo [run_experiment] executable at `realpath gs_gen/$HEAD` +done diff --git a/scripts/test_benchmark b/scripts/test_benchmark index 3f52dde71..b9c9b4322 100755 --- a/scripts/test_benchmark +++ b/scripts/test_benchmark @@ -66,8 +66,8 @@ echo "[test_benchmark] runtime timeout: $RUNTIME_TIMEOUT" if [ "$SCALA_COMPILE" = "true" ] || [ ! -d "gs_gen/${HEAD}" ]; then export SBT_OPTS="-Xms4G -Xmx32G -Xss1024M -XX:MaxMetaspaceSize=8G -XX:ReservedCodeCacheSize=2048M" /usr/bin/time --format "[test_benchmark] scala compilation time => real: %e,\tuser: %U,\tsys: %S" \ - bloop run sai -m gensym.RunGenSym -- -J-Xms4g -J-Xmx8g -J-Xss1024M -J-XX:MaxMetaspaceSize=8G -J-XX:ReservedCodeCacheSize=2048M ${LL} --use-argv --output=${HEAD} --engine=ImpCPS --main-opt=O0 --entrance=main - # sbt "runMain gensym.RunGenSym ${LL} --use-argv --output=${HEAD} --engine=ImpCPS --main-opt=O0 --entrance=main" + # bloop run sai -m gensym.RunGenSym -- -J-Xms4g -J-Xmx8g -J-Xss1024M -J-XX:MaxMetaspaceSize=8G -J-XX:ReservedCodeCacheSize=2048M ${LL} --use-argv --output=${HEAD} --engine=ImpCPS --main-opt=O0 --entrance=main + sbt "runMain gensym.RunGenSym ${LL} --use-argv --output=${HEAD} --engine=ImpCPS --main-opt=O0 --entrance=main" check_failure "Failed to perform scala compilation with input ${LL}" fi @@ -109,10 +109,9 @@ if [ "$RUNTIME" = "true" ]; then if [ -z "$SUCCINCT_LOG" ]; then eval "$cmd" else - echo "--------------------" >> ${SUCCINCT_LOG} - echo "$HEAD $OPT" >> ${SUCCINCT_LOG} + echo -n "$HEAD,$OPT," >> ${SUCCINCT_LOG} # duplicate to stdout, but write the splitted last line to SUCCINCT_LOG - eval "$cmd" | tee >(tail -n 1 | sed 's/#\(blocks\|br\|paths\|threads\|task-in-q\|queries\)/\n&/g' >> ${SUCCINCT_LOG}) + eval "$cmd" | tee >(tail -n 1 | sed 's/#\(blocks\|br\|paths\|threads\|task-in-q\|queries\): /,/g' | sed 's/[; ]//g' >> ${SUCCINCT_LOG}) fi done fi diff --git a/src/main/scala/gensym/Driver.scala b/src/main/scala/gensym/Driver.scala index 2c182cad7..104b046dd 100644 --- a/src/main/scala/gensym/Driver.scala +++ b/src/main/scala/gensym/Driver.scala @@ -125,7 +125,12 @@ abstract class GenericGSDriver[A: Manifest, B: Manifest] def makeWithAllCores: Int = { val cores = Process("nproc", new File(s"$folder/$appName")).!!.replaceAll("[\\n\\t ]", "").toInt - Process(s"make -j$cores", new File(s"$folder/$appName")).! + make(cores) + } + + def makeWithHalfCores: Int = { + val cores = Process("nproc", new File(s"$folder/$appName")).!!.replaceAll("[\\n\\t ]", "").toInt + make(cores/2) } // returns the number of paths, obtained by parsing the output diff --git a/src/main/scala/gensym/External.scala b/src/main/scala/gensym/External.scala index c1606696a..9f556c92c 100644 --- a/src/main/scala/gensym/External.scala +++ b/src/main/scala/gensym/External.scala @@ -22,59 +22,27 @@ import scala.collection.mutable.{Map => MutableMap, Set => MutableSet} @virtualize trait GenExternal extends SymExeDefs { trait Auto - def info(msg: String) = unchecked("INFO(\"[FS] \" << \"" + msg + "\")") - def info_obj(p: Rep[_], l: String = ""): Rep[Unit] = unchecked("INFO(\"", if (l == "") "" else l + ": ", "\" << ", p, ")") - def info_ptrval(p: Rep[Value], l: String = ""): Rep[Unit] = unchecked("INFO(\"", if (l == "") "" else l + ": ", "\" << ", p, "->toString())") - - def stop[T: Manifest](ss: Rep[SS]): Rep[T] = { - if (manifest[T] == manifest[Unit]) - "stop".reflectCtrlWith[T](ss, List[Value](), unchecked[(SS, Value) => Rep[T]]("halt")) - else - "stop".reflectCtrlWith[T](ss, List[Value]()) - } + val debug: Boolean = false + def rawInfo(seq: Any*): Rep[Unit] = if (debug) unchecked(seq: _*) + def info(s: String): Rep[Unit] = rawInfo("std::cout << \"", s, "\" << std::endl") + def info_obj(p: Rep[_], l: String = ""): Rep[Unit] = rawInfo("std::cout << \"", if (l == "") "" else l + ": ", "\" << ", p, " << std::endl") + def info_ptrval(p: Rep[Value], l: String = ""): Rep[Unit] = rawInfo("std::cout << \"", if (l == "") "" else l + ": ", "\" << ", p, "->toString() << std::endl") import FS._ type ExtCont[T] = (Rep[SS], Rep[FS], Rep[Value]) => Rep[T] type Ext[T] = (Rep[SS], Rep[FS], Rep[List[Value]], ExtCont[T]) => Rep[T] - def brFs[T: Manifest](ss: Rep[SS], fs: Rep[FS], cond: Rep[Value], - tk: (Rep[SS], Rep[FS]) => Rep[T], fk: (Rep[SS], Rep[FS]) => Rep[T]) = { - if (cond.isConc) { - if (cond.int == 0) fk(ss, fs) - else tk(ss, fs) - } else symExecBrFs(ss, fs, cond, !cond, tk, fk) - } - - def symExecBrFs[T: Manifest](ss: Rep[SS], fs: Rep[FS], tCond: Rep[Value], fCond: Rep[Value], - tk: (Rep[SS], Rep[FS]) => Rep[T], fk: (Rep[SS], Rep[FS]) => Rep[T]) = { - unchecked("INFO(\"symExecBrFs: tCond is symbolic: \" << ", tCond, "->toString())") - val ssf = ss.fork - val tpcSat = checkPC(ss.addPC(tCond).pc) - val fpcSat = checkPC(ssf.addPC(fCond).pc) - if (tpcSat && fpcSat) { - unchecked("INFO(\"symExecBrFs: both satisfiable\")") - Coverage.incPath(1) - // false branch - fk(ssf.addPC(fCond), FS.dcopy(fs)) - // true branch - tk(ss.addPC(tCond), fs) - // TODO: add second stage ++ operation <2022-08-19, David Deng> // - // This version would lose result on non CPS versions - // resF ++ resT - } else if (tpcSat) { - unchecked("INFO(\"symExecBrFs: only true satisfiable\")") - tk(ss.addPC(tCond), fs) - } else { - unchecked("INFO(\"symExecBrFs: only false satisfiable\")") - fk(ssf.addPC(fCond), fs) - } - } - + // TODO: sym_exit return type in C should be void def sym_exit[T: Manifest](ss: Rep[SS], args: Rep[List[Value]]): Rep[T] = "sym_exit".reflectWith[T](ss, args) - def getSymString(ptr: Rep[Value], s: Rep[SS]): Rep[List[Value]] = "get_sym_string_at".reflectCtrlWith[List[Value]](s, ptr) + // TODO: Utility functions + // 1. object constructors, factories (e.g. new_stream, new_stat) + // Use the apply() method on classes as constructors/factories + // <2022-05-12, David Deng> // + def getStringAt(ptr: Rep[Value], s: Rep[SS]): Rep[String] = "get_string_at".reflectWith[String](ptr, s) + def getConcreteFilePath(ptr: Rep[Value], s: Rep[SS]): Rep[String] = "get_concrete_file_path".reflectWith[String](ptr, s) def hasPermission(flags: Rep[Value], f: Rep[File]): Rep[Value] = { // the requested permission @@ -86,8 +54,9 @@ trait GenExternal extends SymExeDefs { val mode: Rep[Value] = f.readStatField("st_mode") val bw = f.readStatBw("st_mode") + // TODO: add missing flags <2022-08-19, David Deng> // val canRead = ((mode & IntV(S_IRUSR, bw)) | (mode & IntV(S_IRGRP, bw)) | (mode & IntV(S_IROTH, bw))) - val illegalRead = IntOp2.eq(canRead, IntV(0, bw)) + val illegalRead = IntOp2.eq(canRead, IntV(0, bw)) // cast to boolean val canWrite = ((mode & IntV(S_IWUSR, bw)) | (mode & IntV(S_IWGRP, bw)) | (mode & IntV(S_IWOTH, bw))) val illegalWrite = IntOp2.eq(canWrite, IntV(0, bw)) @@ -95,107 +64,80 @@ trait GenExternal extends SymExeDefs { !((readAccess & illegalRead) | (writeAccess & illegalWrite)) } - // returns a SymV that encodes each element in the list equals the element in the other list - def listEq(l1: Rep[List[Value]], l2: Rep[List[Value]]): Rep[Value] = - l1.zip(l2).foldLeft[Value](SymV.fromBool(true))((symv, pair) => - IntOp2("and", symv, IntOp2.eq(pair._1, pair._2))) - - // takes the current ss, fs, a symbolic file path, - // the continuation k takes the new ss, fs, and a concrete path, - // with the assumption that the symbolic file path is resolved to the concrete path. - // The continuation tk can be called multiple times - // The continuation fk will be called only one time when the resolution failed. - def resolvePath[T: Manifest](ss: Rep[SS], fs: Rep[FS], symPath: Rep[List[Value]], - tk: (Rep[SS], Rep[FS], Rep[String]) => Rep[T], fk: (Rep[SS], Rep[FS]) => Rep[T]): Rep[T] = { - if (symPath.foldLeft[Boolean](true)((b, v) => b && v.isConc)) { - info("symPath is concrete") - // if symPath is concrete - tk(ss, fs, "proj_List_String".reflectWith[String](symPath)) - } else { - info_obj(symPath.size, "symPath.size") - // resolve for a number of possible concrete paths - val concPaths = fs.rootFile.children - .filter(nf => { - // TODO: handle absolute paths and recursively traverse the FS <2022-10-01, David Deng> // - val (name, _) = nf - // exclude stdin, stdout, and stderr - name.substring(0, 1) != "@" && - // the symbolic name must be long enough - name.length < symPath.size - }).map(_._1) - info_obj(concPaths.size, "concPaths.size") - if (concPaths.size > 0) { - // val init: Rep[T] = if (manifest[T] == manifest[Unit]) () else List() - concPaths.foldLeft[Unit](())((acc, concPath) => { - // whether it is possible that the path matches the symbolic path - val cond = listEq(concPath.split("").map((s: Rep[String]) => IntV(s(0).asRepOf[Long], 8): Rep[Value]), symPath) - // TODO: add path constraint to the final null byte in string <2022-10-01, David Deng> // - info_ptrval(cond, "path equal condition") - symExecBrFs[T](ss.fork, FS.dcopy(fs), cond, !cond, - (ss, fs) => { - // match - tk(ss, fs, concPath) - }, - (ss, fs) => { - // not match - stop[T](ss) - }) - acc - }) - } else { - fk(ss, fs) - } - // TODO: collect results for non-CPS version <2022-10-01, David Deng> // - // NOTE: will end up having one more path here due to the use of foreach // - stop[T](ss.fork) - } - } - /* * int open(const char *pathname, int flags); * int open(const char *pathname, int flags, mode_t mode); */ - // type Res = Either[Unit, List[(SS, Value)]] - // How to write union type? def open[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"open syscall\")") - val path: Rep[List[Value]] = getSymString(args(0), ss) + rawInfo("std::cout << \"open syscall\" << std::endl") + val path: Rep[String] = getConcreteFilePath(args(0), ss) + info_obj(path, "path") val flags = args(1) - resolvePath(ss, fs, path, (ss, fs, concPath) => { - info_obj(concPath, "concPath") - if (!(flags.int & O_CREAT: Rep[Boolean]) && (flags.int & O_EXCL)) { - k(ss.setErrorLoc(flag("EACCES")), fs, IntV(-1, 32)) - } else if (!fs.hasFile(concPath) && !(flags.int & O_CREAT: Rep[Boolean])) { - k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - } else if (fs.hasFile(concPath) && (flags.int & O_CREAT: Rep[Boolean]) && (flags.int & O_EXCL)) { - k(ss.setErrorLoc(flag("EEXIST")), fs, IntV(-1, 32)) - } else if ((flags.int & O_TRUNC: Rep[Boolean]) && (flags.int & O_RDONLY)) { - // The (undefined) effect of O_RDONLY | O_TRUNC varies among implementations. - k(ss.setErrorLoc(flag("EEXIST")), fs, IntV(-1, 32)) + if (!(flags.int & O_CREAT: Rep[Boolean]) && (flags.int & O_EXCL)) { + k(ss.setErrorLoc(flag("EACCES")), fs, IntV(-1, 32)) + } else if (!fs.hasFile(path) && !(flags.int & O_CREAT: Rep[Boolean])) { + k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) + } else if (fs.hasFile(path) && (flags.int & O_CREAT: Rep[Boolean]) && (flags.int & O_EXCL)) { + k(ss.setErrorLoc(flag("EEXIST")), fs, IntV(-1, 32)) + } else if ((flags.int & O_TRUNC: Rep[Boolean]) && (flags.int & O_RDONLY)) { + // The (undefined) effect of O_RDONLY | O_TRUNC varies among implementations. + k(ss.setErrorLoc(flag("EEXIST")), fs, IntV(-1, 32)) + } else { + if (!fs.hasFile(path)) { + val f = File(getPathSegments(path).last, List[Value](), List.fill(StatType.size(null))(IntV(0, 8))) + val regF = _set_file_type(f, S_IFREG) + fs.setFile(path, regF) + } + val file = fs.getFile(path) + val hp: Rep[Value] = hasPermission(flags, file) + if (hp.isConc) { + if (hp.int == 0) { + k(ss.setErrorLoc(flag("EACCES")), fs, IntV(-1, 32)) + } else { + if (flags.int & O_TRUNC) { + file.content = List[Value]() + } + val fd: Rep[Fd] = fs.getFreshFd() + fs.setStream(fd, Stream(file)) + k(ss, fs, IntV(fd, 32)) + } } else { - if (!fs.hasFile(concPath)) { - val f = File(getPathSegments(concPath).last, List[Value]()) - val regF = _set_file_type(f, S_IFREG) - fs.setFile(concPath, regF) + // TODO: abstract it to a separate function? <2022-08-18, David Deng> // + // hp symbolic + rawInfo("std::cout << \"open: hp is symbolic: \" << ", hp, "->toString() << std::endl;") + val tpcSat = checkPC(ss.copyPC.addPC(hp)) + val fpcSat = checkPC(ss.copyPC.addPC(!hp)) + if (tpcSat && fpcSat) { + rawInfo("std::cout << \"open: both satisfiable\" << std::endl;") + Coverage.incPath(1) + // false branch + k(ss.fork.addPC(!hp).setErrorLoc(flag("EACCES")), FS.dcopy(fs), IntV(-1, 32)) // does not have permission + + // true branch + if (flags.int & O_TRUNC) { + file.content = List[Value]() + } + val fd: Rep[Fd] = fs.getFreshFd() + fs.setStream(fd, Stream(file)) + k(ss.addPC(hp), fs, IntV(fd, 32)) + // TODO: add second stage ++ operation <2022-08-19, David Deng> // + // This version would lose result on non CPS versions + // resF ++ resT + } else if (tpcSat) { + rawInfo("std::cout << \"open: only true satisfiable\" << std::endl;") + if (flags.int & O_TRUNC) { + file.content = List[Value]() + } + val fd: Rep[Fd] = fs.getFreshFd() + fs.setStream(fd, Stream(file)) + k(ss.addPC(hp), fs, IntV(fd, 32)) + } else { + rawInfo("std::cout << \"open: only false satisfiable\" << std::endl;") + k(ss.addPC(!hp).setErrorLoc(flag("EACCES")), fs, IntV(-1, 32)) // does not have permission } - info("fs.getFile") - val file = fs.getFile(concPath) - info("hasPermission") - val hp: Rep[Value] = hasPermission(flags, file) - brFs[T](ss, fs, hp, - (ss, fs) => { - if (flags.int & O_TRUNC) { - file.content = List[Value]() - } - val fd: Rep[Fd] = fs.getFreshFd() - fs.setStream(fd, Stream(file)) - k(ss, fs, IntV(fd, 32)) - }, - (ss, fs) => k(ss.setErrorLoc(flag("EACCES")), fs, IntV(-1, 32)) // does not have permission - ) + // TODO: fix benchmark tests <2022-08-17, David Deng> // } - }, (ss, fs) => k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - ) + } } /* @@ -203,8 +145,10 @@ trait GenExternal extends SymExeDefs { * int openat(int dirfd, const char *pathname, int flags, mode_t mode); */ def openat[T: Manifest](ss: Rep[SS], args: Rep[List[Value]], k: (Rep[SS], Rep[Value]) => Rep[T]): Rep[T] = { - unchecked("INFO(\"openat syscall\")") + rawInfo("std::cout << \"openat syscall\" << std::endl") // TODO: implement this <2022-01-23, David Deng> // + // int __fd_openat(int basefd, const char *pathname, int flags, mode_t mode); + // if (fd == AT_FDCWD), call open k(ss, IntV(0, 32)) } @@ -212,9 +156,9 @@ trait GenExternal extends SymExeDefs { * int close(int fd); */ def close[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"close syscall\")") + rawInfo("std::cout << \"close syscall\" << std::endl") val fd: Rep[Fd] = args(0).int.toInt - unchecked("INFO(\"fd: \" << ", fd, ")") + rawInfo("std::cout << \"fd: \" << ", fd, " << std::endl") if (!fs.hasStream(fd)) k(ss.setErrorLoc(flag("EBADF")), fs, IntV(-1, 32)) else { @@ -233,7 +177,7 @@ trait GenExternal extends SymExeDefs { * ssize_t read(int fd, void *buf, size_t count); */ def read[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"read syscall\")") + rawInfo("std::cout << \"read syscall\" << std::endl") val fd: Rep[Int] = args(0).int.toInt info_obj(fd, "fd") val loc: Rep[Value] = args(1) @@ -256,7 +200,7 @@ trait GenExternal extends SymExeDefs { * ssize_t write(int fd, const void *buf, size_t count); */ def write[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"write syscall\")") + rawInfo("std::cout << \"write syscall\" << std::endl") val fd: Rep[Int] = args(0).int.toInt // NOTE: .int => Rep[Long], .toInt => Rep[Int] info_obj(fd, "fd") val buf: Rep[Value] = args(1) @@ -280,7 +224,7 @@ trait GenExternal extends SymExeDefs { * off_t lseek(int fd, off_t offset, int whence); */ def lseek[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"lseek syscall\")") + rawInfo("std::cout << \"lseek syscall\" << std::endl") val fd: Rep[Fd] = args(0).int.toInt val o: Rep[Long] = args(1).int val w: Rep[Int] = args(2).int.toInt @@ -307,29 +251,24 @@ trait GenExternal extends SymExeDefs { * int stat(const char *pathname, struct stat *statbuf); */ def stat[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"stat syscall\")") + rawInfo("std::cout << \"stat syscall\" << std::endl") val ptr = args(0) - val path: Rep[List[Value]] = getSymString(ptr, ss) + val name: Rep[String] = getConcreteFilePath(ptr, ss) val buf: Rep[Value] = args(1) - resolvePath(ss, fs, path, (ss, fs, concPath) => { - if (!fs.hasFile(concPath)) { - info("stat does not have file") - k(ss, fs, IntV(-1, 32)) - } else { - info("stat has file") - val stat = fs.getFile(concPath).stat - val ss1 = ss.updateSeq(buf, stat) - k(ss1, fs, IntV(0, 32)) - } - }, (ss, fs) => k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - ) + if (!fs.hasFile(name)) { + k(ss, fs, IntV(-1, 32)) + } else { + val stat = fs.getFile(name).stat + val ss1 = ss.updateSeq(buf, stat) + k(ss1, fs, IntV(0, 32)) + } } /* * int fstat(int fd, struct stat *statbuf); */ def fstat[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"fstat syscall\")") + rawInfo("std::cout << \"fstat syscall\" << std::endl") val fd: Rep[Fd] = args(0).int.toInt val buf: Rep[Value] = args(1) if (!fs.hasStream(fd)) @@ -345,7 +284,8 @@ trait GenExternal extends SymExeDefs { * int lstat(const char *pathname, struct stat *statbuf); */ def lstat[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"lstat syscall\")") + rawInfo("std::cout << \"lstat syscall\" << std::endl") + // TODO: handle symlink <2022-08-09, David Deng> // stat(ss, fs, args, k) } @@ -353,73 +293,59 @@ trait GenExternal extends SymExeDefs { * int statfs(const char *path, struct statfs *buf); */ def statfs[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"statfs syscall\")") - val path: Rep[List[Value]] = getSymString(args(0), ss) - resolvePath(ss, fs, path, (ss, fs, concPath) => { - if (!fs.hasFile(concPath)) { - k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - } else { - val buf: Rep[Value] = args(1) - val statFs = fs.statFs - k(ss.updateSeq(buf, statFs), fs, IntV(0, 32)) - } - }, (ss, fs) => k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - ) + rawInfo("std::cout << \"statfs syscall\" << std::endl") + val name: Rep[String] = getConcreteFilePath(args(0), ss) + if (!fs.hasFile(name)) { + k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) + } else { + val buf: Rep[Value] = args(1) + val statFs = fs.statFs + k(ss.updateSeq(buf, statFs), fs, IntV(0, 32)) + } } /* * int mkdir(const char *pathname, mode_t mode); */ def mkdir[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"mkdir syscall\")") - val path: Rep[List[Value]] = getSymString(args(0), ss) - resolvePath(ss, fs, path, (ss, fs, concPath) => { - // TODO: set mode <2022-05-28, David Deng> // - val mode: Rep[Value] = args(1) - val name: Rep[String] = getPathSegments(concPath).last - if (fs.hasFile(concPath)) k(ss, fs, IntV(-1, 32)) - else { - val f = _set_file_type(File(name, List[Value](), List.fill(144)(IntV(0, 8))), S_IFDIR) - unchecked("/* mkdir: fs.setFile */") - fs.setFile(concPath, f) - unchecked("/* mkdir: return */") - k(ss, fs, IntV(0, 32)) - } - }, (ss, fs) => k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - ) + rawInfo("std::cout << \"mkdir syscall\" << std::endl") + val path: Rep[String] = getConcreteFilePath(args(0), ss) + // TODO: set mode <2022-05-28, David Deng> // + val mode: Rep[Value] = args(1) + val name: Rep[String] = getPathSegments(path).last + // TODO: set errno <2022-05-28, David Deng> // + if (fs.hasFile(path)) k(ss, fs, IntV(-1, 32)) + else { + // TODO: refactor a get_dir method? <2022-05-28, David Deng> // + val f = _set_file_type(File(name, List[Value](), List.fill(144)(IntV(0, 8))), S_IFDIR) + rawInfo("/* mkdir: fs.setFile */") + fs.setFile(path, f) + rawInfo("/* mkdir: return */") + k(ss, fs, IntV(0, 32)) + } } /* * int rmdir(const char *pathname); */ def rmdir[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"rmdir syscall\")") - val path: Rep[List[Value]] = getSymString(args(0), ss) - resolvePath(ss, fs, path, (ss, fs, concPath) => { - val dir = fs.getFile(concPath) - if (dir == NullPtr[File]) - k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - else { - brFs[T](ss, fs, _has_file_type(dir, S_IFDIR), - (ss, fs) => { - // is a dir - fs.removeFile(concPath) - k(ss, fs, IntV(0, 32)) - }, - (ss, fs) => { - // is not a dir - k(ss.setErrorLoc(flag("ENOTDIR")), fs, IntV(-1, 32)) - }) - } - }, (ss, fs) => k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - ) + rawInfo("std::cout << \"rmdir syscall\" << std::endl") + val path: Rep[String] = getConcreteFilePath(args(0), ss) + val dir = fs.getFile(path) + // TODO: set errno <2022-05-28, David Deng> // + if (dir == NullPtr[File] || !_has_file_type(dir, S_IFDIR)) k(ss, fs, IntV(-1, 32)) + else { + // TODO: first get the parent to optimize <2022-05-28, David Deng> // + fs.removeFile(path) + k(ss, fs, IntV(0, 32)) + } } /* * int creat(const char *pathname, mode_t mode); */ def creat[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"creat syscall\")") + rawInfo("std::cout << \"creat syscall\" << std::endl") // A call to creat() is equivalent to calling open() with flags equal to O_CREAT|O_WRONLY|O_TRUNC. open(ss, fs, List(args(0), IntV(O_CREAT | O_WRONLY | O_TRUNC), args(1)), k) } @@ -428,75 +354,62 @@ trait GenExternal extends SymExeDefs { * int unlink(const char *pathname); */ def unlink[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"unlink syscall\")") - val path: Rep[List[Value]] = getSymString(args(0), ss) - resolvePath(ss, fs, path, (ss, fs, concPath) => { - val file = fs.getFile(concPath) - if (file == NullPtr[File]) - k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - else { - brFs[T](ss, fs, _has_file_type(file, S_IFREG), - (ss, fs) => { - // is a regular file - fs.removeFile(concPath) - k(ss, fs, IntV(0, 32)) - }, - (ss, fs) => { - // is not a regular file - k(ss.setErrorLoc(flag("EISDIR")), fs, IntV(-1, 32)) - }) - } - }, (ss, fs) => k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - ) + rawInfo("std::cout << \"unlink syscall\" << std::endl") + val path: Rep[String] = getConcreteFilePath(args(0), ss) + val file = fs.getFile(path) + // TODO: set errno <2022-05-28, David Deng> // + if (file == NullPtr[File] || !_has_file_type(file, S_IFREG)) k(ss, fs, IntV(-1, 32)) + else { + // TODO: first get the parent to optimize <2022-05-28, David Deng> // + fs.removeFile(path) + k(ss, fs, IntV(0, 32)) + } } /* * int chmod(const char *pathname, mode_t mode); */ def chmod[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"chmod syscall\")") - val path: Rep[List[Value]] = getSymString(args(0), ss) - resolvePath(ss, fs, path, (ss, fs, concPath) => { - val file = fs.getFile(concPath) - val mode: Rep[Value] = args(1) - if (file == NullPtr[File]) k(ss, fs, IntV(-1, 32)) - else { - _set_file_mode(file, mode.int.toInt) - k(ss, fs, IntV(0, 32)) - } - }, (ss, fs) => k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - ) + rawInfo("std::cout << \"chmod syscall\" << std::endl") + val path: Rep[String] = getConcreteFilePath(args(0), ss) + val file = fs.getFile(path) + val mode: Rep[Value] = args(1) + // TODO: set errno <2022-05-28, David Deng> // + if (file == NullPtr[File]) k(ss, fs, IntV(-1, 32)) + else { + _set_file_mode(file, mode.int.toInt) + k(ss, fs, IntV(0, 32)) + } } /* * int chown(const char *pathname, uid_t owner, gid_t group); */ def chown[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"chown syscall\")") - val path: Rep[List[Value]] = getSymString(args(0), ss) - resolvePath(ss, fs, path, (ss, fs, concPath) => { - val file = fs.getFile(concPath) - val owner: Rep[Value] = args(1) - val group: Rep[Value] = args(2) - if (file == NullPtr[File]) k(ss, fs, IntV(-1, 32)) - else { - file.writeStatField("st_uid", owner) - file.writeStatField("st_gid", group) - k(ss, fs, IntV(0, 32)) - } - }, (ss, fs) => k(ss.setErrorLoc(flag("ENOENT")), fs, IntV(-1, 32)) - ) + rawInfo("std::cout << \"chown syscall\" << std::endl") + val path: Rep[String] = getConcreteFilePath(args(0), ss) + val file = fs.getFile(path) + val owner: Rep[Value] = args(1) + val group: Rep[Value] = args(2) + // TODO: set errno <2022-05-28, David Deng> // + if (file == NullPtr[File]) k(ss, fs, IntV(-1, 32)) + else { + // TODO: If the owner or group is specified as -1, then that ID is not changed. <2022-05-28, David Deng> // + file.writeStatField("st_uid", owner) + file.writeStatField("st_gid", group) + k(ss, fs, IntV(0, 32)) + } } /* * int ioctl(int fd, int request, ...); */ def ioctl[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"ioctl syscall\")") + rawInfo("std::cout << \"ioctl syscall\" << std::endl") val fd: Rep[Fd] = args(0).int.toInt - unchecked("INFO(\"with fd:\" << ", fd, ")") + rawInfo("std::cout << \"with fd:\" << ", fd, " << std::endl") val request: Rep[Value] = args(1) - unchecked("INFO(\"with request:\" << ", request, "->toString())") + rawInfo("std::cout << \"with request:\" << ", request, "->toString() << std::endl") if (!fs.hasStream(fd) || fd <= 2) { k(ss.setErrorLoc(flag("EBADF")), fs, IntV(-1, 32)) } else { @@ -507,15 +420,41 @@ trait GenExternal extends SymExeDefs { val mode: Rep[Value] = fs.getStream(fd).file.readStatField("st_mode") val bw = Constants.BYTE_SIZE * StructCalc()(null).getFieldOffsetSize(StatType.types, getFieldIdx(statFields, "st_mode"))._2 val ischr: Rep[Value] = IntOp2.eq(mode & IntV(cmacro[Int]("S_IFMT"), bw), IntV(cmacro[Int]("S_IFCHR"), bw)) - brFs(ss, fs, ischr, - (ss, fs) => { - info("is character") - k(ss, fs, IntV(0, 32)) - }, - (ss, fs) => { - info("is not a character, return error") - k(ss.setErrorLoc(flag("ENOTTY")), fs, IntV(-1, 32)) - }) + + if (ischr.isConc) { + if (ischr.int == 0) { + k(ss.setErrorLoc(flag("ENOTTY")), fs, IntV(-1, 32)) + } else { + // set up termios values + k(ss, fs, IntV(0, 32)) + } + } else { + // TODO: abstract it to a separate function? <2022-08-18, David Deng> // + // ischr symbolic + rawInfo("std::cout << \"ioctl: ischr is symbolic: \" << ", ischr, "->toString() << std::endl;") + val ss1 = ss.fork + val tpcSat = checkPC(ss.addPC(ischr).pc) + val fpcSat = checkPC(ss1.addPC(!ischr).pc) + if (tpcSat && fpcSat) { + rawInfo("std::cout << \"ioctl: both satisfiable\" << std::endl;") + Coverage.incPath(1) + // false branch + k(ss1.setErrorLoc(flag("ENOTTY")), FS.dcopy(fs), IntV(-1, 32)) // does not have permission + + // true branch + // set up termios values + k(ss, fs, IntV(0, 32)) + // TODO: add second stage ++ operation <2022-08-19, David Deng> // + // This version would lose result on non CPS versions + // resF ++ resT + } else if (tpcSat) { + rawInfo("std::cout << \"ioctl: only true satisfiable\" << std::endl;") + k(ss, fs, IntV(0, 32)) + } else { + rawInfo("std::cout << \"ioctl: only false satisfiable\" << std::endl;") + k(ss1.setErrorLoc(flag("ENOTTY")), fs, IntV(-1, 32)) // does not have permission + } + } } else { k(ss.setErrorLoc(flag("EINVAL")), fs, IntV(-1, 32)) } @@ -526,7 +465,7 @@ trait GenExternal extends SymExeDefs { * int fcntl(int fd, int cmd, ...); */ def fcntl[T: Manifest](ss: Rep[SS], fs: Rep[FS], args: Rep[List[Value]], k: ExtCont[T]): Rep[T] = { - unchecked("INFO(\"fcntl syscall\")") + rawInfo("std::cout << \"fcntl syscall\" << std::endl") val fd: Rep[Value] = args(0) val cmd: Rep[Value] = args(1) k(ss, fs, IntV(-1, 32)) @@ -553,32 +492,32 @@ trait GenExternal extends SymExeDefs { // NOTE: return type might not be necessary if using pointers <2022-05-27, David Deng> // def _set_file_type(f: Rep[File], mask: Rep[Int]): Rep[File] = { - unchecked("/* _set_file_type */") - val bw = f.readStatBw("st_mode") - val mode = f.readStatField("st_mode") + rawInfo("/* _set_file_type */") // want to unset the file type bits and leave the other bits unchanged - val newMode = (mode & flag("~S_IFMT", bw)) | IntV(mask, bw) - f.writeStatField("st_mode", newMode) + val clearMask: Rep[IntV] = flag("~S_IFMT") + val stat = f.readStatField("st_mode") + val newStat = IntV((stat.int & clearMask.int) | mask, 32) + f.writeStatField("st_mode", newStat) f } def _set_file_mode(f: Rep[File], mask: Rep[Int]): Rep[File] = { - unchecked("/* _set_file_mode */") - val bw = f.readStatBw("st_mode") - val mode = f.readStatField("st_mode") + rawInfo("/* _set_file_mode */") // preserve the file type bits - val newMode = (mode & flag("S_IFMT", bw)) | IntV(mask, bw) - f.writeStatField("st_mode", newMode) + val clearMask: Rep[IntV] = flag("S_IFMT") + val stat = f.readStatField("st_mode") + val newStat = IntV((stat.int & clearMask.int) | mask, 32) + f.writeStatField("st_mode", newStat) f } def _errno_location[T: Manifest](ss: Rep[SS], args: Rep[List[Value]], k: (Rep[SS], Rep[Value]) => Rep[T]): Rep[T] = k(ss, ss.getErrorLoc) - def _has_file_type(f: Rep[File], mask: Rep[Int]): Rep[Value] = { + // TODO: rename? <2022-05-28, David Deng> // + def _has_file_type(f: Rep[File], mask: Rep[Int]): Rep[Boolean] = { val stat = f.readStatField("st_mode") - val bw = f.readStatBw("st_mode") - IntOp2.neq(stat & IntV(mask, bw), IntV(0, bw)) // cast to boolean + stat.int & mask } def _get_preferred_cex(f: Rep[File]): Rep[List[Value]] = f.getPreferredCex() @@ -614,6 +553,7 @@ trait GenExternal extends SymExeDefs { ss.setFs(fs) val end = unchecked[Auto]("steady_clock::now()") val duration = unchecked[Auto]("duration_cast(", end, " - ", start, ").count() ") + // rawInfo("std::cout << \"Time Taken: \" << ", duration, " << std::endl") unchecked("fs_time += ", duration) k(ss, ret) } @@ -723,6 +663,7 @@ class ExternalGSDriver(folder: String = "./headers/gensym") extends SAISnippet[I hardTopFun(gen_k(brg_fs(fcntl(_,_,_,_))), "syscall_fcntl", "inline") hardTopFun(_set_file(_,_,_), "set_file", "inline") hardTopFun(_set_file_type(_,_), "set_file_type", "inline") + hardTopFun(_has_file_type(_,_), "has_file_type", "inline") hardTopFun(_get_preferred_cex(_), "get_preferred_cex", "inline") hardTopFun(gen_p(_errno_location), "__errno_location", "inline") hardTopFun(gen_k(_errno_location), "__errno_location", "inline") diff --git a/src/main/scala/gensym/FileSys.scala b/src/main/scala/gensym/FileSys.scala index 92ad64d47..70b7c6ceb 100644 --- a/src/main/scala/gensym/FileSys.scala +++ b/src/main/scala/gensym/FileSys.scala @@ -23,6 +23,8 @@ trait FileSysDefs extends ExternalUtil { self: SAIOps with BasicDefs with ValueD // %struct.stat = type { i64, i64, i64, i32, i32, i32, i32 (padding), i64, i64, i64, i64, %struct.timespec, %struct.timespec, %struct.timespec, [3 x i64] } // %struct.timespec = type { i64, i64 } + // TODO: model nested fields? <2022-08-09, David Deng> // + val statFields = ListMap[String, LLVMType]( "st_dev" -> IntType(64), "st_ino" -> IntType(64), @@ -127,6 +129,7 @@ trait FileSysDefs extends ExternalUtil { self: SAIOps with BasicDefs with ValueD def parent: Rep[File] = "ptr-field-@".reflectMutableWith[File](file, "parent") // assign ptr-field + // TODO: Is this valid? <2022-05-12, David Deng> // def name_=(rhs: Rep[String]): Unit = "ptr-field-assign".reflectCtrlWith(file, "name", rhs) def content_=(rhs: Rep[List[Value]]): Unit = "ptr-field-assign".reflectCtrlWith(file, "content", rhs) def stat_=(rhs: Rep[List[Value]]): Unit = "ptr-field-assign".reflectCtrlWith(file, "stat", rhs) @@ -243,15 +246,18 @@ trait FileSysDefs extends ExternalUtil { self: SAIOps with BasicDefs with ValueD IntOp2.eq(readStatField("st_uid"), IntV(1000, readStatBw("st_uid"))), // klee_prefer_cex(s, s->st_gid == defaults->st_gid); IntOp2.eq(readStatField("st_gid"), IntV(1000, readStatBw("st_gid"))), - // NOTE: 16 byte nested struct not modeled <2022-08-30, David Deng> // + + // TODO: 16 byte nested struct not modeled <2022-08-30, David Deng> // // klee_prefer_cex(s, s->st_atime == defaults->st_atime); // klee_prefer_cex(s, s->st_mtime == defaults->st_mtime); // klee_prefer_cex(s, s->st_ctime == defaults->st_ctime); - ).filter(v => !v.isConc) + ) + cex } } + // TODO: Change to pointer type for dup syscall? <2022-05-20, David Deng> // object Stream { def apply(f: Rep[File]) = "Stream::create".reflectCtrlWith[Stream](f) def apply(f: Rep[File], m: Rep[Int]) = "Stream::create".reflectCtrlWith[Stream](f, m) @@ -279,7 +285,7 @@ trait FileSysDefs extends ExternalUtil { self: SAIOps with BasicDefs with ValueD def write(c: Rep[List[Value]], n: Rep[Long]): Rep[Long] = { val content = c.take(n.toInt) - strm.file.writeAt(content, strm.cursor, IntV(0, 8)) + strm.file.writeAt(content, strm.cursor, cmacro("IntV0")) strm.cursor = strm.cursor + content.size; return content.size } @@ -348,6 +354,7 @@ trait FileSysDefs extends ExternalUtil { self: SAIOps with BasicDefs with ValueD def getPathSegments(path: Rep[String]): Rep[List[String]] = path.split("/").filter(_.length > 0) + // TODO: use option type? <2022-05-26, David Deng> // def getFileFromPathSegments(file: Rep[File], segs: Rep[List[String]]): Rep[File] = { segs.foldLeft(file: Rep[File])((f: Rep[File], seg: Rep[String]) => { if (f == NullPtr[File] || !f.hasChild(seg)) NullPtr[File] @@ -384,7 +391,7 @@ trait FileSysDefs extends ExternalUtil { self: SAIOps with BasicDefs with ValueD fs.preferredCex = fs.preferredCex ++ f.getPreferredCex() } - // TODO: recursively find and remove file from rootFile <2022-07-28, David Deng> // + // TODO: This is wrong <2022-07-28, David Deng> // def removeFile(name: Rep[String]): Rep[Unit] = fs.rootFile.removeChild(name) def hasStream(fd: Rep[Fd]): Rep[Boolean] = fs.openedFiles.contains(fd) def getStream(fd: Rep[Fd]): Rep[Stream] = fs.openedFiles(fd) diff --git a/src/main/scala/gensym/RunGenSym.scala b/src/main/scala/gensym/RunGenSym.scala index 403472cb8..6526ac550 100644 --- a/src/main/scala/gensym/RunGenSym.scala +++ b/src/main/scala/gensym/RunGenSym.scala @@ -1,6 +1,7 @@ package gensym import gensym.llvm.parser.Parser._ +import gensym.utils.Utils case class Config(nSym: Int, useArgv: Boolean, mainFileOpt: String) { require(!(nSym > 0 && useArgv)) @@ -51,6 +52,23 @@ object RunGenSym { } def main(args: Array[String]): Unit = { + val bang = "--repeat=" + if (args(0).startsWith(bang)) { + val (rc :: nargs) = args(0).substring(bang.length).split(',').map(_.toInt).toList + var idx = 1 + for (n <- nargs) { + val s = args.slice(idx, idx + n) + for (i <- 1 to rc) { + val (name, time) = Utils.time { mainInner(s) } + System.err.println(f"run repeat mode: $name $time") + } + idx += n + } + } + else mainInner(args) + } + + def mainInner(args: Array[String]): String = { val usage = """ |Usage: gensym [--entrance=] [--output=] [--nSym=] | [--use-argv] [--noOpt] [--engine=] [--main-O0] @@ -70,8 +88,8 @@ object RunGenSym { |--emit-block-id-map - emit a map from block names to id in common.h |--emit-var-id-map - emit a map from variable names to id in common.h |--switch-type= - compilation variants of `switch` statement (default=nonMerge) - | =merge - only fork `m` paths of distinct targets - | =nonMerge - fork `n` paths where `n` is the total number of feasible cases (including default) + | =merge - only fork `m` paths of distinct targets + | =nonMerge - fork `n` paths where `n` is the total number of feasible cases (including default) |--help - print this help message """ @@ -83,8 +101,8 @@ object RunGenSym { case (options, r"--noOpt") => options + ("optimize" -> false) case (options, r"--engine=([a-zA-Z]+)$e") => options + ("engine" -> e) case (options, r"--main-opt=O(\d)$n") => options + ("mainOpt" -> ("O"+n)) - case (options, r"emit-block-id-map") => options + ("blockIdMap" -> true) - case (options, r"emit-var-id-map") => options + ("varIdMap" -> true) + case (options, r"--emit-block-id-map") => options + ("blockIdMap" -> true) + case (options, r"--emit-var-id-map") => options + ("varIdMap" -> true) case (options, r"--switch-type=(\w+)$t") => options + ("switchType" -> SwitchType.fromString(t)) case (options, r"--lib=([-_A-Za-z0-9\/\.]+)$p") => options + ("lib" -> p) case (options, "--help") => println(usage.stripMargin); sys.exit(0) @@ -95,7 +113,7 @@ object RunGenSym { val output = options.getOrElse("output", filepath.split("\\/").last.split("\\.")(0)).toString val nSym = options.getOrElse("nSym", 0).asInstanceOf[Int] val useArgv = options.getOrElse("useArgv", false).asInstanceOf[Boolean] - val optimize = options.getOrElse("optimize", Config.opt).asInstanceOf[Boolean] + val optimize = options.getOrElse("optimize", true).asInstanceOf[Boolean] val engine = options.getOrElse("engine", "ImpCPS").toString val mainOpt = options.getOrElse("mainOpt", Config.o0).toString val emitBlockIdMap = options.getOrElse("blockIdMap", Config.emitBlockIdMap).asInstanceOf[Boolean] @@ -120,5 +138,6 @@ object RunGenSym { | nSym=$nSym, useArgv=$useArgv, optimize=$optimize, mainOpt=$mainOpt, switchType=$switchType""" println(info.stripMargin) gensym.run(parseFile(filepath), output, entrance, Config(nSym, useArgv, mainOpt), libPath) + output } } diff --git a/src/main/scala/llvm/Benchmarks.scala b/src/main/scala/llvm/Benchmarks.scala index b3a24823b..926924aa5 100644 --- a/src/main/scala/llvm/Benchmarks.scala +++ b/src/main/scala/llvm/Benchmarks.scala @@ -116,22 +116,7 @@ object Benchmarks { lazy val argv2Test = parseFile("benchmarks/llvm/argv2.ll") lazy val unprintableCharTest = parseFile("benchmarks/llvm/unprintable_char.ll") - - lazy val echo_linked = parseFile("benchmarks/coreutils/echo.ll") - lazy val cat_linked = parseFile("benchmarks/coreutils/cat.ll") - lazy val true_linked = parseFile("benchmarks/coreutils/true.ll") - lazy val false_linked = parseFile("benchmarks/coreutils/false.ll") - lazy val base32_linked = parseFile("benchmarks/coreutils/base32.ll") - lazy val base64_linked = parseFile("benchmarks/coreutils/base64.ll") - lazy val comm_linked = parseFile("benchmarks/coreutils/comm.ll") - lazy val cut_linked = parseFile("benchmarks/coreutils/cut.ll") - lazy val dirname_linked = parseFile("benchmarks/coreutils/dirname.ll") - lazy val expand_linked = parseFile("benchmarks/coreutils/expand.ll") - lazy val fold_linked = parseFile("benchmarks/coreutils/fold.ll") - lazy val join_linked = parseFile("benchmarks/coreutils/join.ll") - lazy val link_linked = parseFile("benchmarks/coreutils/link.ll") - lazy val paste_linked = parseFile("benchmarks/coreutils/paste.ll") - lazy val pathchk_linked = parseFile("benchmarks/coreutils/pathchk.ll") + lazy val md5sum_linked = parseFile("benchmarks/coreutils/md5sum.ll") lazy val sort_linked = parseFile("benchmarks/coreutils/sort.ll") lazy val wc_linked = parseFile("benchmarks/coreutils/wc.ll") @@ -141,6 +126,44 @@ object Benchmarks { lazy val true_gs_linked = parseFile("benchmarks/coreutils/true_gs_linked.ll") } +object ICSE23CoreutilsPOSIX { + val prefix = "/icse23/GenSym/benchmarks/coreutils/gensym_posix" + lazy val echo = parseFile(s"$prefix/echo.ll") + lazy val cat = parseFile(s"$prefix/cat.ll") + lazy val tru = parseFile(s"$prefix/true.ll") + lazy val fls = parseFile(s"$prefix/false.ll") + lazy val base32 = parseFile(s"$prefix/base32.ll") + lazy val base64 = parseFile(s"$prefix/base64.ll") + lazy val comm = parseFile(s"$prefix/comm.ll") + lazy val cut = parseFile(s"$prefix/cut.ll") + lazy val dirname = parseFile(s"$prefix/dirname.ll") + lazy val expand = parseFile(s"$prefix/expand.ll") + lazy val fold = parseFile(s"$prefix/fold.ll") + lazy val join = parseFile(s"$prefix/join.ll") + lazy val link = parseFile(s"$prefix/link.ll") + lazy val paste = parseFile(s"$prefix/paste.ll") + lazy val pathchk = parseFile(s"$prefix/pathchk.ll") +} + +object ICSE23CoreutilsUClibc { + val prefix = "/icse23/GenSym/benchmarks/coreutils/gensym_uclibc" + lazy val echo = parseFile(s"$prefix/echo.ll") + lazy val cat = parseFile(s"$prefix/cat.ll") + lazy val tru = parseFile(s"$prefix/true.ll") + lazy val fls = parseFile(s"$prefix/false.ll") + lazy val base32 = parseFile(s"$prefix/base32.ll") + lazy val base64 = parseFile(s"$prefix/base64.ll") + lazy val comm = parseFile(s"$prefix/comm.ll") + lazy val cut = parseFile(s"$prefix/cut.ll") + lazy val dirname = parseFile(s"$prefix/dirname.ll") + lazy val expand = parseFile(s"$prefix/expand.ll") + lazy val fold = parseFile(s"$prefix/fold.ll") + lazy val join = parseFile(s"$prefix/join.ll") + lazy val link = parseFile(s"$prefix/link.ll") + lazy val paste = parseFile(s"$prefix/paste.ll") + lazy val pathchk = parseFile(s"$prefix/pathchk.ll") +} + object TestComp { object ArrayExamples { val prefix = "benchmarks/test-comp/array-examples" diff --git a/src/test/scala/gensym/TestCases.scala b/src/test/scala/gensym/TestCases.scala index e213b93ac..51a8f011f 100644 --- a/src/test/scala/gensym/TestCases.scala +++ b/src/test/scala/gensym/TestCases.scala @@ -160,60 +160,47 @@ object TestCases { TestPrg(kleefslib64Test, "kleelib64", "@main", noArg, noOpt, nPath(10)++status(0)), ) + val all: List[TestPrg] = concrete ++ memModel ++ symbolicSimple ++ symbolicSmall ++ external ++ argv +} + +object CoreutilsPOSIX { + import ICSE23CoreutilsPOSIX._ lazy val coreutils: List[TestPrg] = List( - TestPrg(echo_linked, "echo_linked_posix", "@main", noMainFileOpt, "--argv=./echo.bc --sym-stdout --sym-arg 2 --sym-arg 7", nPath(216136)++status(0)), - // [0.75008s/6.94065s/82.0174s] #blocks: 473/2224; #br: 160/96/1128; #paths: 216136; #threads: 1; #task-in-q: 0; #queries: 646097/53 (0) - // gcov 84.17% - TestPrg(cat_linked, "cat_linked_posix", "@main", noMainFileOpt, "--argv=./cat.bc --sym-stdout --sym-stdin 2 --sym-arg 2", nPath(28567)++status(0)), - // [17.5964s/122.277s/152.538s] #blocks: 1114/2484; #br: 371/297/1664; #paths: 28567; #threads: 1; #task-in-q: 0; #queries: 976797/71 (0) - // gcov 81.4% - TestPrg(base32_linked, "base32_linked_posix", "@main", noMainFileOpt, "--argv=./base32 --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10621)++status(0)), - // [11.0384s/81.2135s/95.0274s] #blocks: 1170/2718; #br: 417/284/1860; #paths: 10621; #threads: 1; #task-in-q: 0; #queries: 475353/38 (0) - // gcov 73.33% - TestPrg(base64_linked, "base64_linked_posix", "@main", noMainFileOpt, "--argv=./base64.bc --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10624)++status(0)), - // [11.1519s/81.5593s/95.0264s] #blocks: 1164/2694; #br: 411/286/1889; #paths: 10624; #threads: 1; #task-in-q: 0; #queries: 475379/38 (0) - // gcov 73.33% - TestPrg(comm_linked, "comm_linked_posix", "@main", noMainFileOpt, "--argv=./comm.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 -sym-files 2 2", nPath(23846)++status(0)), - // [19.4591s/134.449s/164.537s] #blocks: 1230/2719; #br: 406/314/2077; #paths: 23846; #threads: 1; #task-in-q: 0; #queries: 993577/52 (0) - // gcov 72.41% - TestPrg(cut_linked, "cut_linked_posix", "@main", noMainFileOpt, "--argv=./cut.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 2 -sym-files 2 2", nPath(28481)++status(0)), // or --sym-args 0 2 2 - // [31.0933s/98.3556s/134.029s] #blocks: 1056/2751; #br: 388/242/2124; #paths: 28481; #threads: 1; #task-in-q: 0; #queries: 238501/100 (0) - // gcov 67.44% - TestPrg(dirname_linked, "dirname_linked_posix", "@main", noMainFileOpt, "--argv=./dirname.bc --sym-stdout --sym-stdin 2 --sym-arg 6 --sym-arg 10", nPath(287386)++status(0)), - // [1.14461s/18.4733s/115.025s] #blocks: 590/2295; #br: 219/93/2130; #paths: 287386; #threads: 1; #task-in-q: 0; #queries: 3720763/21 (0) - // gcov 100.00% - TestPrg(expand_linked, "expand_linked_posix", "@main", noMainFileOpt, "--argv=./expand.bc --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10870)++status(0)), - // [21.482s/101.299s/116.022s] #blocks: 1167/2554; #br: 408/294/2145; #paths: 10870; #threads: 1; #task-in-q: 0; #queries: 478319/41 (0) - // gcov 71.05% - TestPrg(false_linked, "false_linked_posix", "@main", noMainFileOpt, "--argv=./false.bc --sym-stdout --sym-arg 10", nPath(16)++status(0)), - // [0.012289s/0.032464s/1.00143s] #blocks: 391/2108; #br: 159/44/2276; #paths: 16; #threads: 1; #task-in-q: 0; #queries: 165/3 (0) - // gcov 100.00% - TestPrg(true_linked, "true_linked_posix", "@main", noMainFileOpt, "--argv=./true.bc --sym-stdout --sym-arg 10", nPath(16)++status(0)), - // [0.012326s/0.032479s/1.0014s] #blocks: 391/2108; #br: 159/44/2276; #paths: 16; #threads: 1; #task-in-q: 0; #queries: 165/3 (0) - // gcov 100.00% - TestPrg(fold_linked, "fold_linked_posix", "@main", noMainFileOpt, "--argv=./fold.bc --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(11015)++status(0)), - // [11.2871s/95.8641s/110.53s] #blocks: 1212/2603; #br: 417/301/2279; #paths: 11015; #threads: 1; #task-in-q: 0; #queries: 478287/46 (0) - // gcov 74.36% - TestPrg(join_linked, "join_linked_posix", "@main", noMainFileOpt, "--argv=./join.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 -sym-files 2 2", nPath(25046)++status(0)), - // [32.7084s/230.442s/263.047s] #blocks: 1444/3172; #br: 461/369/2511; #paths: 25046; #threads: 1; #task-in-q: 0; #queries: 983311/87 (0) - // gcov 71.75% - TestPrg(link_linked, "link_linked_posix", "@main", noMainFileOpt, "--argv=./link.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 --sym-arg 1 -sym-files 2 2", nPath(11233)++status(0)), - // [9.39498s/116.469s/142.031s] #blocks: 891/2282; #br: 334/208/2511; #paths: 11233; #threads: 1; #task-in-q: 0; #queries: 1238401/91 (0) - // gcov 60.00% - TestPrg(paste_linked, "paste_linked_posix", "@main", noMainFileOpt, "--argv=./paste.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 -sym-files 2 2", nPath(22622)++status(0)), - // [19.9342s/142.499s/170.043s] #blocks: 1180/2510; #br: 393/306/2513; #paths: 22622; #threads: 1; #task-in-q: 0; #queries: 974269/46 (0) - // gcov 76.08% - TestPrg(pathchk_linked, "pathchk_linked_posix", "@main", noMainFileOpt, "--argv=./pathchk.bc --sym-stdout --sym-stdin 2 --sym-arg 2", nPath(10614)++status(0)), - // [10.6848s/77.1473s/91.5263s] #blocks: 878/2418; #br: 314/226/2515; #paths: 10614; #threads: 1; #task-in-q: 0; #queries: 475423/30 (0) - // gcov 40.29% + TestPrg(echo, "echo_linked_posix", "@main", noMainFileOpt, "--argv=./echo.bc --sym-stdout --sym-arg 2 --sym-arg 7", nPath(216136)++status(0)), + TestPrg(cat, "cat_linked_posix", "@main", noMainFileOpt, "--argv=./cat.bc --sym-stdout --sym-stdin 2 --sym-arg 2", nPath(28567)++status(0)), + TestPrg(base32, "base32_linked_posix", "@main", noMainFileOpt, "--argv=./base32 --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10621)++status(0)), + TestPrg(base64, "base64_linked_posix", "@main", noMainFileOpt, "--argv=./base64.bc --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10624)++status(0)), + TestPrg(comm, "comm_linked_posix", "@main", noMainFileOpt, "--argv=./comm.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 -sym-files 2 2", nPath(23846)++status(0)), + TestPrg(cut, "cut_linked_posix", "@main", noMainFileOpt, "--argv=./cut.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 2 -sym-files 2 2", nPath(28481)++status(0)), // or --sym-args 0 2 2 + TestPrg(dirname, "dirname_linked_posix", "@main", noMainFileOpt, "--argv=./dirname.bc --sym-stdout --sym-stdin 2 --sym-arg 6 --sym-arg 10", nPath(287386)++status(0)), + TestPrg(expand, "expand_linked_posix", "@main", noMainFileOpt, "--argv=./expand.bc --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10870)++status(0)), + TestPrg(fls, "false_linked_posix", "@main", noMainFileOpt, "--argv=./false.bc --sym-stdout --sym-arg 10", nPath(16)++status(0)), + TestPrg(tru, "true_linked_posix", "@main", noMainFileOpt, "--argv=./true.bc --sym-stdout --sym-arg 10", nPath(16)++status(0)), + TestPrg(fold, "fold_linked_posix", "@main", noMainFileOpt, "--argv=./fold.bc --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(11015)++status(0)), + TestPrg(join, "join_linked_posix", "@main", noMainFileOpt, "--argv=./join.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 -sym-files 2 2", nPath(25046)++status(0)), + TestPrg(link, "link_linked_posix", "@main", noMainFileOpt, "--argv=./link.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 --sym-arg 1 -sym-files 2 2", nPath(11233)++status(0)), + TestPrg(paste, "paste_linked_posix", "@main", noMainFileOpt, "--argv=./paste.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 -sym-files 2 2", nPath(22622)++status(0)), + TestPrg(pathchk, "pathchk_linked_posix", "@main", noMainFileOpt, "--argv=./pathchk.bc --sym-stdout --sym-stdin 2 --sym-arg 2", nPath(10614)++status(0)), ) +} - val all: List[TestPrg] = concrete ++ memModel ++ symbolicSimple ++ symbolicSmall ++ external ++ argv - - // FIXME: out of range - // TestPrg(struct, "structTest", "@main", noArg, 1), - // FIXME: seg fault - // TestPrg(largeStackArray, "largeStackArrayTest", "@main", noArg, 1), - // TestPrg(makeSymbolicArray, "makeSymbolicArrayTest", "@main", noArg, 1), - // TestPrg(ptrtoint, "ptrToIntTest", "@main", noArg, 1) +object CoreutilsUClibc { + import ICSE23CoreutilsPOSIX._ + lazy val coreutils: List[TestPrg] = List( + TestPrg(echo, "echo_linked_uclibc", "@main", noMainFileOpt, "--argv=./echo.bc --sym-stdout --sym-arg 2 --sym-arg 7", nPath(216136)++status(0)), + TestPrg(cat, "cat_linked_uclibc", "@main", noMainFileOpt, "--argv=./cat.bc --sym-stdout --sym-stdin 2 --sym-arg 2", nPath(28567)++status(0)), + TestPrg(base32, "base32_linked_uclibc", "@main", noMainFileOpt, "--argv=./base32 --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10621)++status(0)), + TestPrg(base64, "base64_linked_uclibc", "@main", noMainFileOpt, "--argv=./base64.bc --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10624)++status(0)), + TestPrg(comm, "comm_linked_uclibc", "@main", noMainFileOpt, "--argv=./comm.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 -sym-files 2 2", nPath(23846)++status(0)), + TestPrg(cut, "cut_linked_uclibc", "@main", noMainFileOpt, "--argv=./cut.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 2 -sym-files 2 2", nPath(28481)++status(0)), // or --sym-args 0 2 2 + TestPrg(dirname, "dirname_linked_uclibc", "@main", noMainFileOpt, "--argv=./dirname.bc --sym-stdout --sym-stdin 2 --sym-arg 6 --sym-arg 10", nPath(287386)++status(0)), + TestPrg(expand, "expand_linked_uclibc", "@main", noMainFileOpt, "--argv=./expand.bc --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(10870)++status(0)), + TestPrg(fls, "false_linked_uclibc", "@main", noMainFileOpt, "--argv=./false.bc --sym-stdout --sym-arg 10", nPath(16)++status(0)), + TestPrg(tru, "true_linked_uclibc", "@main", noMainFileOpt, "--argv=./true.bc --sym-stdout --sym-arg 10", nPath(16)++status(0)), + TestPrg(fold, "fold_linked_uclibc", "@main", noMainFileOpt, "--argv=./fold.bc --sym-stdout --sym-stdin 2 --sym-arg 2 -sym-files 2 2", nPath(11015)++status(0)), + TestPrg(join, "join_linked_uclibc", "@main", noMainFileOpt, "--argv=./join.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 -sym-files 2 2", nPath(25046)++status(0)), + TestPrg(link, "link_linked_uclibc", "@main", noMainFileOpt, "--argv=./link.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 --sym-arg 1 -sym-files 2 2", nPath(11233)++status(0)), + TestPrg(paste, "paste_linked_uclibc", "@main", noMainFileOpt, "--argv=./paste.bc --sym-stdout --sym-stdin 2 --sym-arg 2 --sym-arg 1 -sym-files 2 2", nPath(22622)++status(0)), + TestPrg(pathchk, "pathchk_linked_uclibc", "@main", noMainFileOpt, "--argv=./pathchk.bc --sym-stdout --sym-stdin 2 --sym-arg 2", nPath(10614)++status(0)), + ) } diff --git a/src/test/scala/gensym/TestGS.scala b/src/test/scala/gensym/TestGS.scala index 3bebcd1a1..59e7624f8 100644 --- a/src/test/scala/gensym/TestGS.scala +++ b/src/test/scala/gensym/TestGS.scala @@ -29,6 +29,8 @@ import TestCases._ abstract class TestGS extends FunSuite { import java.time.LocalDateTime + val cores: Option[Int] = None + case class TestResult(time: LocalDateTime, commit: String, engine: String, testName: String, extSolverTime: Double, intSolverTime: Double, wholeTime: Double, blockCov: Double, partialBrCov: Double, fullBrCov: Double, pathNum: Int, brQueryNum: Int, @@ -60,7 +62,10 @@ abstract class TestGS extends FunSuite { else gs.insName + "_" + name test(name) { val code = gs.run(m, outname, f, config, libPath) - val mkRet = code.makeWithAllCores + val mkRet = cores match { + case None => code.makeWithHalfCores + case Some(n) => code.make(n) + } assert(mkRet == 0, "make failed") if (runCode) { val (output, ret) = code.runWithStatus(cliArg) diff --git a/src/test/scala/icse23/CompileCoreutils.scala b/src/test/scala/icse23/CompileCoreutils.scala new file mode 100644 index 000000000..0c080de61 --- /dev/null +++ b/src/test/scala/icse23/CompileCoreutils.scala @@ -0,0 +1,51 @@ +package icse23 + +import lms.core._ +import lms.core.Backend._ +import lms.core.virtualize +import lms.macros.SourceContext +import lms.core.stub.{While => _, _} + +import gensym._ +import gensym.lmsx._ +import gensym.llvm._ +import gensym.llvm.IR._ +import gensym.llvm.Benchmarks._ +import gensym.llvm.parser.Parser._ +import gensym.Config._ +import gensym.TestPrg._ +import gensym.TestCases._ +import gensym.Constants._ +import gensym.utils.Utils.time + +import sys.process._ +import org.scalatest.FunSuite + +class CompileCoreutilsPOSIX extends TestGS { + import gensym.llvm.parser.Parser._ + Config.enableOpt + // Change None to Some(n) if you want to use n cores to compile c++ files with g++ + override val cores: Option[Int] = None + + val runtimeOptions = "--output-tests-cov-new --thread=1 --search=random-path --solver=z3 --output-ktest --cons-indep".split(" +").toList.toSeq + val cases = CoreutilsPOSIX.coreutils.map { t => + t.copy(runOpt = runtimeOptions ++ t.runOpt, runCode = false) + } + + testGS(new ImpCPSGS, cases) +} + +class CompileCoreutilsUClibc extends TestGS { + import gensym.llvm.parser.Parser._ + Config.enableOpt + + // Change None to Some(n) if you want to use n cores to compile c++ files with g++ + override val cores: Option[Int] = None + + val runtimeOptions = "--output-tests-cov-new --thread=1 --search=random-path --solver=z3 --output-ktest --cons-indep".split(" +").toList.toSeq + val cases = CoreutilsUClibc.coreutils.map { t => + t.copy(runOpt = runtimeOptions ++ t.runOpt, runCode = false) + } + + testGS(new ImpCPSGS, cases) +} \ No newline at end of file diff --git a/src/test/scala/icse23/KickTheTires.scala b/src/test/scala/icse23/KickTheTires.scala new file mode 100644 index 000000000..2c5d37498 --- /dev/null +++ b/src/test/scala/icse23/KickTheTires.scala @@ -0,0 +1,29 @@ +package icse23 + +import lms.core._ +import lms.core.Backend._ +import lms.core.virtualize +import lms.macros.SourceContext +import lms.core.stub.{While => _, _} + +import gensym._ +import gensym.lmsx._ +import gensym.llvm._ +import gensym.llvm.IR._ +import gensym.llvm.Benchmarks._ +import gensym.llvm.parser.Parser._ +import gensym.Config._ +import gensym.TestPrg._ +import gensym.TestCases._ +import gensym.Constants._ +import gensym.utils.Utils.time + +import sys.process._ +import org.scalatest.FunSuite + +class KickTheTires extends TestGS { + import gensym.llvm.parser.Parser._ + Config.enableOpt + val gs = new ImpCPSGS + testGS(gs, TestPrg(branch, "branch", "@f", symArg(2), noOpt, nPath(4))) +} \ No newline at end of file diff --git a/third-party/lms-clean b/third-party/lms-clean index 44af36bb0..b6f019aef 160000 --- a/third-party/lms-clean +++ b/third-party/lms-clean @@ -1 +1 @@ -Subproject commit 44af36bb07956c3edfd409e079a8251708c6060c +Subproject commit b6f019aef1df5f1f12bcd0b43a9136d7f9ce7704