initial gcov integration (#123)

* initial gcov integration

* fix sym_print signature

* misc

* reorg and comment

Author: Kraks

dev-clean/headers/llsc/smt_checker.hpp

@@ -216,7 +216,7 @@ class CachedChecker : public Checker {
         ABORT("Cannot create the test case file, abort.\n");
       }
       for (auto [k, v]: *model) {
-        output << k->name << " == " << v << std::endl;
+        output << k->name << "=" << v << std::endl;
       }
       int n = write(out_fd, output.str().c_str(), output.str().size());
       close(out_fd);

dev-clean/headers/llsc_client.h

@@ -2,15 +2,17 @@
 #define LLSC_CLIENT_HEADERS
 
 #include <stdio.h>
-#include "stdint.h"
+#include <stdint.h>
 #include <stddef.h>
+#include <stdarg.h>
 #include <stdbool.h>
 
 // TODO: support assigning names for symbolic values
 
 /* Construct `byte_size` 8-bitvectors starting at address `addr`.
  */
 void make_symbolic(void* addr, size_t byte_size);
+void llsc_make_symbolic(void* addr, size_t byte_size, char* name);
 
 /* Construct a single bitvector of size `byte_size`*8 at address `addr`.
  */
@@ -22,7 +24,7 @@ void llsc_assert(bool);
 void llsc_assert_eager(bool);
 
 void llsc_assume(bool);
-
+void sym_print(int, ...);
 void print_string(const char *message);
 
 /* llsc_range - Construct a symbolic value in the signed interval

dev-clean/scripts/gcov_driver.py

@@ -0,0 +1,28 @@
+#!/usr/bin/env python3
+
+import os
+import sys
+import glob
+import subprocess
+
+# example
+# python3 driver.py ../llsc_gen/ImpCPSLLSC_quickSortTest/tests quicksort.c
+
+if __name__ == "__main__":
+    tests_folder = sys.argv[1]
+    src_file = sys.argv[2]
+    target = src_file.split(".")[0]
+    cmd = "gcc -fprofile-arcs -ftest-coverage -o {} llsc_client.c {}".format(target, src_file)
+    print("Compiling: {}".format(cmd))
+    os.system(cmd)
+    print("Reading test cases from {}".format(tests_folder))
+    # TODO: find the metainfo file in test_folder
+    for test_case in glob.glob(tests_folder+"/*.test"):
+        print("Testing {}".format(test_case))
+        env = dict(os.environ)
+        # TODO: read the test file and create corresponding files, redirect stdin/stdout/stderr
+        env["LLSC_TEST_FILE"] = test_case
+        # TODO: synthesize argv
+        # argv = "..."
+        subprocess.Popen(["./"+target], env=env)
+    os.system("gcov -b -c {}-{}".format(target, target))

dev-clean/scripts/llsc_client.c

@@ -0,0 +1,72 @@
+#include <stdio.h>
+#include <stdint.h>
+#include <stddef.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <stdbool.h>
+
+#define LLSC_TEST_FILE "LLSC_TEST_FILE"
+
+int32_t is_key(char* key, char* name_prefix, size_t size) {
+  char* p = strstr(key, name_prefix);
+  if (p == NULL) return -1;
+  assert(strlen(name_prefix) < size);
+  char* n = p + strlen(name_prefix);
+  int32_t v = strtol(n, (char**)NULL, 10);
+  assert(v >= 0);
+  return v;
+}
+
+// name can only be alphabet letters, containing no numbers
+void make_symbolic(void* addr, size_t byte_size, char* name_prefix) {
+  const char* path = getenv(LLSC_TEST_FILE);
+  char* line = NULL;
+  size_t len = 0;
+  ssize_t read;
+  FILE* fp = fopen(path, "r");
+  if (fp == NULL) {
+    fprintf(stderr, "Test file %s not exists\n", path);
+    exit(-1);
+  }
+  fprintf(stdout, "Reading test case from %s\n", path);
+
+  uint8_t* reified_data = (uint8_t*)malloc(byte_size);
+  while ((read = getline(&line, &len, fp)) != -1) {
+    char* value_ptr = strstr(line, "=");
+    if (value_ptr == NULL) continue;
+    size_t key_size = value_ptr - line;
+    line[key_size] = '\0';
+    //printf("%s, %s", line, value_ptr+1);
+    int idx = is_key(line, name_prefix, key_size);
+    if (idx == -1) continue;
+    assert(idx >= 0 && idx < byte_size);
+    uint8_t v = (uint8_t) strtol(value_ptr+1, (char **)NULL, 10);
+    reified_data[idx] = v;
+    //printf("%s%d -> %d\n", name_prefix, idx, v);
+  }
+  memcpy(addr, (void*)reified_data, byte_size);
+  free(reified_data);
+  free(line);
+}
+
+void make_symbolic_whole(void* addr, size_t byte_size, char* name) {
+
+}
+
+/*
+int main() {
+  int x;
+  make_symbolic(&x, 4, "x");
+  if (x <= 10) {
+    printf("%d\n", x);
+  } else {
+    if (x <= 15) {
+      printf("%d\n", x);
+    } else {
+      printf("%d\n", x);
+    }
+  }
+  return 0;
+}
+*/

dev-clean/scripts/quicksort.c

@@ -0,0 +1,38 @@
+#include "../headers/llsc_client.h"
+#define SIZE 5
+
+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()
+{
+	llsc_make_symbolic(d, sizeof(int) * SIZE, "x");
+  for (int i = 0; i < SIZE; i++) printf("%d,", d[i]);
+  printf("\n");
+	qsort(0, SIZE-1);
+  for (int i = 0; i < SIZE; i++) printf("%d,", d[i]);
+  printf("\n");
+	return 0;
+}

dev-clean/src/test/scala/sai/llsc/TestLLSC.scala

@@ -137,6 +137,7 @@ class Playground extends TestLLSC {
   //  testcoreutil, Seq("--cons-indep", "--argv=./echo.bc --sym-stdout --sym-arg 8"), nPath(4971)++status(0)))
 
   //testLLSC(llsc, TestPrg(mp1048576, "mp1mTest", "@f", symArg(20), "--solver=disable", nPath(1048576)))
+  //testLLSC(llsc, TestPrg(quicksort, "quickSortTest", "@main", noArg, noOpt, nPath(120)))
   //testLLSC(llsc, TestPrg(printfTest, "printfTest", "@main", noArg, noOpt, nPath(1)++status(0)))
   //testLLSC(llsc, TestPrg(selectTestSym, "selectTest", "@main", noArg, noOpt, nPath(1)))
   //testLLSC(llsc, TestPrg(maze, "mazeTest", "@main", noArg, noOpt, nPath(309)))