generate open and openat syscall skeleton (Generative-Program-Analysi…

…s#29) * generate open and openat syscall skeleton * added parameters to specify symbolic files in FS * implement return status in sym_exit * added CI test for open * fs refactor - removed reference from get_fs, set_fs - replace manually with generated open * added effect to write_fs * added FS to remap * generated open passes tests * fix assert test * address comments * fixed sym_exit * fix impure header
mkhan45 · Jan 25, 2022 · 88783e5 · 88783e5
1 parent 254f2b3
commit 88783e5
Show file tree

Hide file tree

Showing 15 changed files with 176 additions and 31 deletions.
diff --git a/dev-clean/benchmarks/external_lib/open.c b/dev-clean/benchmarks/external_lib/open.c
@@ -0,0 +1,17 @@
+#ifdef KLEE
+#include <klee/klee.h>
+#endif
+#include <fcntl.h>
+
+int main()
+{
+  char filename[] = "A";
+  int fd = open(filename, O_RDONLY);
+  if (fd == -1) {
+    // no parameter
+    sym_exit(1);
+  } else {
+    // --add-sym-file A
+    sym_exit(0);
+  }
+}
diff --git a/dev-clean/headers/llsc.hpp b/dev-clean/headers/llsc.hpp
@@ -38,10 +38,10 @@ using namespace std::chrono;
 
 #include <llsc/auxiliary.hpp>
 #include <llsc/parallel.hpp>
-#include <llsc/cli.hpp>
 #include <llsc/monitor.hpp>
 #include <llsc/value_ops.hpp>
 #include <llsc/filesys.hpp>
+#include <llsc/cli.hpp>
 #include <llsc/state_pure.hpp>
 
 #include <llsc/smt_checker.hpp>
@@ -56,6 +56,7 @@ using namespace std::chrono;
 #include <llsc/misc.hpp>
 
 #include <llsc/external_pure.hpp>
+#include <llsc/external.hpp>
 #include <llsc/intrinsics_pure.hpp>
 
 #endif
diff --git a/dev-clean/headers/llsc/cli.hpp b/dev-clean/headers/llsc/cli.hpp
@@ -10,17 +10,20 @@ inline bool exlib_failure_branch = false;
 
 // XXX: can also specify symbolic argument here?
 inline void handle_cli_args(int argc, char** argv) {
+  extern char *optarg;
   int c;
   while (1) {
     static struct option long_options[] =
     {
       /* These options set a flag. */
-      {"disable-solver",       no_argument, 0, 'd'},
-      {"exlib-failure-branch", no_argument, 0, 'f'},
-      {"no-obj-cache",         no_argument, 0, 'O'},
-      {"no-cex-cache",         no_argument, 0, 'C'},
-      {"cons-indep",           no_argument, 0, 'i'},
-      {0,                      0,           0, 0}
+      {"disable-solver",       no_argument,       0, 'd'},
+      {"exlib-failure-branch", no_argument,       0, 'f'},
+      {"no-obj-cache",         no_argument,       0, 'O'},
+      {"no-cex-cache",         no_argument,       0, 'C'},
+      {"cons-indep",           no_argument,       0, 'i'},
+      {"add-sym-file",         required_argument, 0, '+'},
+      {"sym-file-size",        required_argument, 0, 's'},
+      {0,                      0,                 0, 0  }
     };
     int option_index = 0;
 
@@ -48,6 +51,18 @@ inline void handle_cli_args(int argc, char** argv) {
       case 'i':
         use_cons_indep = true;
         break;
+      case '+':
+        initial_fs.add_file(make_SymFile(std::string(optarg), default_sym_file_size));
+#ifdef DEBUG
+        printf("adding symfile: %s with size %d\n", optarg, default_sym_file_size);
+#endif
+        break;
+      case 's':
+        default_sym_file_size = atoi(optarg);
+#ifdef DEBUG
+        printf("set symfile size to %d\n", default_sym_file_size);
+#endif
+        break;
       case '?':
         // parsing error, should be printed by getopt
       default:
@@ -82,6 +97,9 @@ inline void handle_cli_args(int argc, char** argv) {
   }
   use_objcache = use_objcache && use_global_solver;
   use_cexcache = use_cexcache && use_global_solver;
+#ifdef DEBUG
+  std::cout << initial_fs << std::endl;
+#endif
 }
 
 #endif
diff --git a/dev-clean/headers/llsc/external.hpp b/dev-clean/headers/llsc/external.hpp
@@ -0,0 +1,16 @@
+/* LLSC - External utility functions and library modeling functions */
+/* Generated by sai.llsc.TestGenerateExternal */
+#ifndef LLSC_EXTERNAL_HEADERS_GEN
+#define LLSC_EXTERNAL_HEADERS_GEN
+
+/************* Function Declarations **************/
+immer::flex_vector<std::pair<SS, PtrVal>> open(SS, immer::flex_vector<PtrVal>);
+
+/************* Functions **************/
+inline immer::flex_vector<std::pair<SS, PtrVal>> open(SS x1, immer::flex_vector<PtrVal> x2) {
+PtrVal x3 = x2.at(0);
+FS x4 = x1.get_fs();
+x1.set_fs(x4);
+return immer::flex_vector<std::pair<SS, PtrVal>>{std::make_pair(x1, make_IntV(x4.open_file(get_string(x3, x1), 0), 32))};
+}
+#endif // LLSC_EXTERNAL_HEADERS_GEN
diff --git a/dev-clean/headers/llsc/external_pure.hpp b/dev-clean/headers/llsc/external_pure.hpp
@@ -74,28 +74,44 @@ inline std::string get_string(PtrVal ptr, SS state) {
   return name;
 }
 
-inline immer::flex_vector<std::pair<SS, PtrVal>> open(SS state, immer::flex_vector<PtrVal> args) {
-  PtrVal ptr = args.at(0);
-  std::string name = get_string(ptr, state);
-  FS& fs = state.get_fs();
-  /* TODO: add flags for open_file <2021-11-03, David Deng> */
-  Fd fd = fs.open_file(name, 0);
-  state.set_fs(fs);
-  return immer::flex_vector<std::pair<SS, PtrVal>>{{state, make_IntV(fd)}};
-}
-
 inline immer::flex_vector<std::pair<SS, PtrVal>> close(SS state, immer::flex_vector<PtrVal> args) {
   Fd fd = proj_IntV(args.at(0));
-  FS& fs = state.get_fs();
+  FS fs = state.get_fs();
   int status = fs.close_file(fd);
   state.set_fs(fs);
   return immer::flex_vector<std::pair<SS, PtrVal>>{{state, make_IntV(status)}};
 }
 
 inline immer::flex_vector<std::pair<SS, PtrVal>> sym_exit(SS state, immer::flex_vector<PtrVal> args) {
+  int status;
+  if (args.size() > 0) {
+#ifdef DEBUG
+    std::cout << "sym_exit: *args.at(0) = " << *args.at(0) << std::endl;
+#endif
+    auto v = args.at(0)->to_IntV();
+    if (v) {
+      status = v->i;
+    } else {
+      status = 0; // return 0 in case a non-int value is passed as args.at(0)
+    }
+  } else {
+#ifdef DEBUG
+    std::cout << "sym_exit: no args passed" << std::endl;
+#endif
+    status = 0;
+  }
+  check_pc_to_file(state);
+  epilogue();
+  exit(status);
+}
+
+/* TODO: Generate both versions of sym_exit <2022-01-24, David Deng> */
+inline std::monostate sym_exit(SS state, immer::flex_vector<PtrVal> args, Cont k) {
+  auto v = args.at(0)->to_IntV();
+  auto status = v ? v->i : 0;
   check_pc_to_file(state);
   epilogue();
-  exit(0);
+  exit(status);
 }
 
 inline immer::flex_vector<std::pair<SS, PtrVal>> llsc_assert(SS state, immer::flex_vector<PtrVal> args) {

diff --git a/dev-clean/headers/llsc/filesys.hpp b/dev-clean/headers/llsc/filesys.hpp
@@ -124,6 +124,14 @@ class FS {
     Fd next_fd;
 
   public:
+    friend std::ostream& operator<<(std::ostream& os, const FS& fs) {
+      os << "FS(size=" << fs.files.size() << ", files:" << std::endl;
+      for (auto pf: fs.files) {
+        os << pf.second << std::endl << std::endl;
+      }
+      os << ")";
+      return os;
+    }
     FS(): next_fd(3) {
         // default initialize opened_files and files
         /* TODO: set up stdin and stdout using fd 1 and 2 <2021-11-03, David Deng> */
@@ -186,4 +194,7 @@ class FS {
      * <2021-11-15, David Deng> */
 };
 
+inline int default_sym_file_size = 5;
+inline FS initial_fs;
+
 #endif
diff --git a/dev-clean/headers/llsc/state_pure.hpp b/dev-clean/headers/llsc/state_pure.hpp
@@ -122,7 +122,7 @@ class SS {
     BlockLabel bb;
     FS fs;
   public:
-    SS(Mem heap, Stack stack, PC pc, BlockLabel bb) : heap(heap), stack(stack), pc(pc), bb(bb) {}
+    SS(Mem heap, Stack stack, PC pc, BlockLabel bb) : heap(heap), stack(stack), pc(pc), bb(bb), fs(initial_fs) {}
     SS(Mem heap, Stack stack, PC pc, BlockLabel bb, FS fs) : heap(heap), stack(stack), pc(pc), bb(bb), fs(fs) {}
     PtrVal env_lookup(Id id) { return stack.lookup_id(id); }
     size_t heap_size() { return heap.size(); }
@@ -181,8 +181,8 @@ class SS {
     PC get_PC() { return pc; }
     // TODO temp solution
     PtrVal getVarargLoc() { return stack.getVarargLoc(); }
-    void set_fs(FS& new_fs) { fs = new_fs; }
-    FS& get_fs() { return fs; }
+    void set_fs(FS new_fs) { fs = new_fs; }
+    FS get_fs() { return fs; }
 };
 
 inline const Mem mt_mem = Mem(immer::flex_vector<PtrVal>{});

diff --git a/dev-clean/headers/llsc_imp.hpp b/dev-clean/headers/llsc_imp.hpp
@@ -38,9 +38,10 @@ using namespace std::chrono;
 
 #include <llsc/auxiliary.hpp>
 #include <llsc/parallel.hpp>
-#include <llsc/cli.hpp>
 #include <llsc/monitor.hpp>
 #include <llsc/value_ops.hpp>
+#include <llsc/filesys.hpp>
+#include <llsc/cli.hpp>
 #include <llsc/state_imp.hpp>
 #include <llsc/smt_checker.hpp>
 #include <llsc/smt_stp.hpp>

diff --git a/dev-clean/src/main/scala/sai/llsc/Codegen.scala b/dev-clean/src/main/scala/sai/llsc/Codegen.scala
@@ -40,6 +40,7 @@ trait GenericLLSCCodeGen extends CppSAICodeGenBase {
     else if (m.toString.endsWith("$BlockLabel")) "BlockLabel"
     else if (m.toString.endsWith("$Mem")) "Mem"
     else if (m.toString.endsWith("$SS")) "SS"
+    else if (m.toString.endsWith("$FS")) "FS"
     else if (m.toString.endsWith("$Kind")) "LocV::Kind"
     else if (m.toString.endsWith("SMTExpr")) "PtrVal"
     else if (m.toString.endsWith("SMTBool")) "PtrVal"
@@ -79,6 +80,8 @@ trait GenericLLSCCodeGen extends CppSAICodeGenBase {
     case Node(s, "ss-add-incoming-block", List(ss, bb), _) => es"$ss.add_incoming_block($bb)"
     case Node(s, "ss-incoming-block", List(ss), _) => es"$ss.incoming_block()"
     case Node(s, "ss-arg", List(ss, i), _) => es"$ss.init_arg($i)"
+    case Node(s, "ss-get-fs", List(ss), _) => es"$ss.get_fs()"
+    case Node(s, "ss-set-fs", List(ss, fs), _) => es"$ss.set_fs($fs)"
     case Node(s, "get-pc", List(ss), _) => es"$ss.get_PC()"
     case Node(s, "null-v", _, _) => es"nullptr"
 
@@ -95,6 +98,8 @@ trait GenericLLSCCodeGen extends CppSAICodeGenBase {
     case Node(s, "print-block-cov", _, _) => es"cov.print_block_cov()"
     case Node(s, "print-time", _, _) => es"cov.print_time()"
     case Node(s, "print-path-cov", _, _) => es"cov.print_path_cov()"
+    case Node(s, "get-string", List(ptr, ss), _) => es"get_string($ptr, $ss)"
+    case Node(s, "fs-open-file", List(fs, p, f), _) => es"$fs.open_file($p, $f)"
 
     case _ => super.shallow(n)
   }

diff --git a/dev-clean/src/main/scala/sai/llsc/External.scala b/dev-clean/src/main/scala/sai/llsc/External.scala
@@ -49,14 +49,44 @@ trait GenExternal extends SymExeDefs {
     }
   }
 
+  def gen_open[T: Manifest](ss: Rep[SS], args: Rep[List[Value]], k: (Rep[SS], Rep[Value]) => Rep[T]): Rep[T] = {
+    val ptr = args(0)
+    val name: Rep[String] = getString(ptr, ss)
+    val flags = args(1)
+    // val mode = args(2) // how to handle optional argument?
+    val fs: Rep[FS] = ss.getFs
+    val ret: Rep[Fd] = fs.openFile(name, 0)
+    ss.setFs(fs)
+    k(ss, IntV(ret, 32))
+  }
+
+  def gen_openat[T: Manifest](ss: Rep[SS], args: Rep[List[Value]], k: (Rep[SS], Rep[Value]) => Rep[T]): Rep[T] = {
+    // 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))
+  }
+
   def llsc_assert(ss: Rep[SS], args: Rep[List[Value]]): Rep[List[(SS, Value)]] =
     gen_llsc_assert[List[(SS, Value)]](ss, args, { case (s, v) => List[(SS, Value)]((s, v)) })
 
   def llsc_assert_k(ss: Rep[SS], args: Rep[List[Value]], k: Rep[Cont]): Rep[Unit] =
     gen_llsc_assert[Unit](ss, args, { case (s, v) => k(s, v) })
+
+  def open(ss: Rep[SS], args: Rep[List[Value]]): Rep[List[(SS, Value)]] =
+    gen_open[List[(SS, Value)]](ss, args, { case (s, v) => List[(SS, Value)]((s, v)) })
+
+  def open_k(ss: Rep[SS], args: Rep[List[Value]], k: Rep[Cont]): Rep[Unit] =
+    gen_open[Unit](ss, args, { case (s, v) => k(s, v) })
+
+  def openat(ss: Rep[SS], args: Rep[List[Value]]): Rep[List[(SS, Value)]] =
+    gen_openat[List[(SS, Value)]](ss, args, { case (s, v) => List[(SS, Value)]((s, v)) })
+
+  def openat_k(ss: Rep[SS], args: Rep[List[Value]], k: Rep[Cont]): Rep[Unit] =
+    gen_openat[Unit](ss, args, { case (s, v) => k(s, v) })
 }
 
-class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] with SAIOps with GenExternal { q =>
+class ExternalLLSCDriver(folder: String = "./headers/llsc") extends SAISnippet[Int, Unit] with SAIOps with GenExternal { q =>
   import java.io.{File, PrintStream}
   import scala.collection.mutable.HashMap
 
@@ -71,8 +101,12 @@ class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] wit
       val ng = init(g)
       run(name, ng)
       emitln("/* LLSC - External utility functions and library modeling functions */")
+      emitln("/* Generated by sai.llsc.TestGenerateExternal */")
+      emitln("#ifndef LLSC_EXTERNAL_HEADERS_GEN")
+      emitln("#define LLSC_EXTERNAL_HEADERS_GEN")
       emitFunctionDecls(stream)
       emitFunctions(stream)
+      emitln("#endif // LLSC_EXTERNAL_HEADERS_GEN")
     }
   }
 
@@ -85,7 +119,7 @@ class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] wit
   // TODO: refactor into SAIOps <2022-01-18, David Deng> //
 
   def hardTopFun[A:Manifest,B:Manifest](f: Rep[A] => Rep[B], s: String): Rep[A => B] = {
-    val unwrapped = __hardTopFun(f, 1, xn => Unwrap(f(Wrap[A](xn(0)))))
+    val unwrapped = __hardTopFun(f, 1, xn => Unwrap(f(Wrap[A](xn(0)))), "inline")
     if (!s.trim.isEmpty) {
       val n = unwrapped.asInstanceOf[Backend.Sym].n
       funNameMap(n) = s
@@ -94,7 +128,7 @@ class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] wit
   }
 
   def hardTopFun[A:Manifest,B:Manifest,C:Manifest](f: (Rep[A], Rep[B]) => Rep[C], s: String): Rep[(A, B) => C] = {
-    val unwrapped = __hardTopFun(f, 2, xn => Unwrap(f(Wrap[A](xn(0)), Wrap[B](xn(1)))))
+    val unwrapped = __hardTopFun(f, 2, xn => Unwrap(f(Wrap[A](xn(0)), Wrap[B](xn(1)))), "inline")
     if (!s.trim.isEmpty) {
       val n = unwrapped.asInstanceOf[Backend.Sym].n
       funNameMap(n) = s
@@ -103,7 +137,7 @@ class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] wit
   }
 
   def hardTopFun[A:Manifest,B:Manifest,C:Manifest,D:Manifest](f: (Rep[A], Rep[B], Rep[C]) => Rep[D], s: String): Rep[(A, B, C) => D] = {
-    val unwrapped = __hardTopFun(f, 3, xn => Unwrap(f(Wrap[A](xn(0)), Wrap[B](xn(1)), Wrap[C](xn(2)))))
+    val unwrapped = __hardTopFun(f, 3, xn => Unwrap(f(Wrap[A](xn(0)), Wrap[B](xn(1)), Wrap[C](xn(2)))), "inline")
     if (!s.trim.isEmpty) {
       val n = unwrapped.asInstanceOf[Backend.Sym].n
       funNameMap(n) = s
@@ -112,8 +146,12 @@ class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] wit
   }
 
   def snippet(u: Rep[Int]) = {
-    hardTopFun(llsc_assert(_,_), "llsc_assert")
-    hardTopFun(llsc_assert_k(_,_,_), "llsc_assert_k")
+    // TODO: generate function of same name with multiple signatures? <2022-01-23, David Deng> //
+    // TODO: llsc_assert_k depends on sym_exit, which doesn't have a _k version right now <2022-01-23, David Deng> //
+    // hardTopFun(llsc_assert(_,_), "llsc_assert")
+    // hardTopFun(llsc_assert_k(_,_,_), "llsc_assert_k")
+    hardTopFun(open(_,_), "open")
+    // hardTopFun(open_k(_,_,_), "open_k")
     ()
   }
 }

diff --git a/dev-clean/src/main/scala/sai/llsc/states/GenericDefs.scala b/dev-clean/src/main/scala/sai/llsc/states/GenericDefs.scala
@@ -27,12 +27,14 @@ trait BasicDefs { self: SAIOps =>
   trait Value
   trait Stack
   trait SS
+  trait FS
 
   type IntData = Long
   type BlockLabel = Int
   type Addr = Int
   type PC = Set[SMTBool]
   type Id[T] = T
+  type Fd = Int
 
   val bConst = Backend.Const
   lazy val gNode = Adapter.g.Def
@@ -84,6 +86,8 @@ trait Opaques { self: SAIOps with BasicDefs =>
     def noop: Rep[Value] = "llsc-external-wrapper".reflectWith[Value]("noop")
   }
 
+  def getString(ptr: Rep[Value], s: Rep[SS]): Rep[String] = "get-string".reflectWith[String](ptr, s)
+
   object Intrinsics {
     val warned = MutableSet[String]()
     def get(id: String): Rep[Value] =

diff --git a/dev-clean/src/main/scala/sai/llsc/states/SymExeState.scala b/dev-clean/src/main/scala/sai/llsc/states/SymExeState.scala
@@ -100,6 +100,8 @@ trait SymExeDefs extends SAIOps with StagedNondet with BasicDefs with ValueDefs
 
     def addIncomingBlock(x: String): Rep[SS] = "ss-add-incoming-block".reflectWith[SS](ss, x.hashCode)
     def incomingBlock: Rep[BlockLabel] = "ss-incoming-block".reflectWith[BlockLabel](ss)
+    def getFs: Rep[FS] = "ss-get-fs".reflectWith[FS](ss)
+    def setFs(fs: Rep[FS]): Unit = "ss-set-fs".reflectWriteWith[FS](ss, fs)(ss)
   }
 
   implicit class SSOpsOpt(ss: Rep[SS]) extends SSOps(ss) {
@@ -125,6 +127,10 @@ trait SymExeDefs extends SAIOps with StagedNondet with BasicDefs with ValueDefs
     }
   }
 
+  implicit class FSOps(fs: Rep[FS]) {
+    def openFile(path: Rep[String], flag: Rep[Int]): Rep[Fd] = "fs-open-file".reflectWith[Fd](fs, path, flag)
+  }
+
   def putState(s: Rep[SS]): Comp[E, Rep[Unit]] = for { _ <- put[Rep[SS], E](s) } yield ()
   def getState: Comp[E, Rep[SS]] = get[Rep[SS], E]