Skip to content

Commit 88783e5

Browse files
PROgram52bcPROgram52bc
authored
generate open and openat syscall skeleton (Generative-Program-Analysis#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
1 parent 254f2b3 commit 88783e5

File tree

15 files changed

+176
-31
lines changed

15 files changed

+176
-31
lines changed

‎dev-clean/benchmarks/external_lib/open.c‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#ifdef KLEE
2+
#include <klee/klee.h>
3+
#endif
4+
#include <fcntl.h>
5+
6+
int main()
7+
{
8+
char filename[] = "A";
9+
int fd = open(filename, O_RDONLY);
10+
if (fd == -1) {
11+
// no parameter
12+
sym_exit(1);
13+
} else {
14+
// --add-sym-file A
15+
sym_exit(0);
16+
}
17+
}

‎dev-clean/headers/llsc.hpp‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,10 +38,10 @@ using namespace std::chrono;
3838

3939
#include <llsc/auxiliary.hpp>
4040
#include <llsc/parallel.hpp>
41-
#include <llsc/cli.hpp>
4241
#include <llsc/monitor.hpp>
4342
#include <llsc/value_ops.hpp>
4443
#include <llsc/filesys.hpp>
44+
#include <llsc/cli.hpp>
4545
#include <llsc/state_pure.hpp>
4646

4747
#include <llsc/smt_checker.hpp>
@@ -56,6 +56,7 @@ using namespace std::chrono;
5656
#include <llsc/misc.hpp>
5757

5858
#include <llsc/external_pure.hpp>
59+
#include <llsc/external.hpp>
5960
#include <llsc/intrinsics_pure.hpp>
6061

6162
#endif

‎dev-clean/headers/llsc/cli.hpp‎

Lines changed: 24 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,17 +10,20 @@ inline bool exlib_failure_branch = false;
1010

1111
// XXX: can also specify symbolic argument here?
1212
inline void handle_cli_args(int argc, char** argv) {
13+
extern char *optarg;
1314
int c;
1415
while (1) {
1516
static struct option long_options[] =
1617
{
1718
/* These options set a flag. */
18-
{"disable-solver", no_argument, 0, 'd'},
19-
{"exlib-failure-branch", no_argument, 0, 'f'},
20-
{"no-obj-cache", no_argument, 0, 'O'},
21-
{"no-cex-cache", no_argument, 0, 'C'},
22-
{"cons-indep", no_argument, 0, 'i'},
23-
{0, 0, 0, 0}
19+
{"disable-solver", no_argument, 0, 'd'},
20+
{"exlib-failure-branch", no_argument, 0, 'f'},
21+
{"no-obj-cache", no_argument, 0, 'O'},
22+
{"no-cex-cache", no_argument, 0, 'C'},
23+
{"cons-indep", no_argument, 0, 'i'},
24+
{"add-sym-file", required_argument, 0, '+'},
25+
{"sym-file-size", required_argument, 0, 's'},
26+
{0, 0, 0, 0 }
2427
};
2528
int option_index = 0;
2629

@@ -48,6 +51,18 @@ inline void handle_cli_args(int argc, char** argv) {
4851
case 'i':
4952
use_cons_indep = true;
5053
break;
54+
case '+':
55+
initial_fs.add_file(make_SymFile(std::string(optarg), default_sym_file_size));
56+
#ifdef DEBUG
57+
printf("adding symfile: %s with size %d\n", optarg, default_sym_file_size);
58+
#endif
59+
break;
60+
case 's':
61+
default_sym_file_size = atoi(optarg);
62+
#ifdef DEBUG
63+
printf("set symfile size to %d\n", default_sym_file_size);
64+
#endif
65+
break;
5166
case '?':
5267
// parsing error, should be printed by getopt
5368
default:
@@ -82,6 +97,9 @@ inline void handle_cli_args(int argc, char** argv) {
8297
}
8398
use_objcache = use_objcache && use_global_solver;
8499
use_cexcache = use_cexcache && use_global_solver;
100+
#ifdef DEBUG
101+
std::cout << initial_fs << std::endl;
102+
#endif
85103
}
86104

87105
#endif

‎dev-clean/headers/llsc/external.hpp‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
/* LLSC - External utility functions and library modeling functions */
2+
/* Generated by sai.llsc.TestGenerateExternal */
3+
#ifndef LLSC_EXTERNAL_HEADERS_GEN
4+
#define LLSC_EXTERNAL_HEADERS_GEN
5+
6+
/************* Function Declarations **************/
7+
immer::flex_vector<std::pair<SS, PtrVal>> open(SS, immer::flex_vector<PtrVal>);
8+
9+
/************* Functions **************/
10+
inline immer::flex_vector<std::pair<SS, PtrVal>> open(SS x1, immer::flex_vector<PtrVal> x2) {
11+
PtrVal x3 = x2.at(0);
12+
FS x4 = x1.get_fs();
13+
x1.set_fs(x4);
14+
return immer::flex_vector<std::pair<SS, PtrVal>>{std::make_pair(x1, make_IntV(x4.open_file(get_string(x3, x1), 0), 32))};
15+
}
16+
#endif // LLSC_EXTERNAL_HEADERS_GEN

‎dev-clean/headers/llsc/external_pure.hpp‎

Lines changed: 28 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -74,28 +74,44 @@ inline std::string get_string(PtrVal ptr, SS state) {
7474
return name;
7575
}
7676

77-
inline immer::flex_vector<std::pair<SS, PtrVal>> open(SS state, immer::flex_vector<PtrVal> args) {
78-
PtrVal ptr = args.at(0);
79-
std::string name = get_string(ptr, state);
80-
FS& fs = state.get_fs();
81-
/* TODO: add flags for open_file <2021-11-03, David Deng> */
82-
Fd fd = fs.open_file(name, 0);
83-
state.set_fs(fs);
84-
return immer::flex_vector<std::pair<SS, PtrVal>>{{state, make_IntV(fd)}};
85-
}
86-
8777
inline immer::flex_vector<std::pair<SS, PtrVal>> close(SS state, immer::flex_vector<PtrVal> args) {
8878
Fd fd = proj_IntV(args.at(0));
89-
FS& fs = state.get_fs();
79+
FS fs = state.get_fs();
9080
int status = fs.close_file(fd);
9181
state.set_fs(fs);
9282
return immer::flex_vector<std::pair<SS, PtrVal>>{{state, make_IntV(status)}};
9383
}
9484

9585
inline immer::flex_vector<std::pair<SS, PtrVal>> sym_exit(SS state, immer::flex_vector<PtrVal> args) {
86+
int status;
87+
if (args.size() > 0) {
88+
#ifdef DEBUG
89+
std::cout << "sym_exit: *args.at(0) = " << *args.at(0) << std::endl;
90+
#endif
91+
auto v = args.at(0)->to_IntV();
92+
if (v) {
93+
status = v->i;
94+
} else {
95+
status = 0; // return 0 in case a non-int value is passed as args.at(0)
96+
}
97+
} else {
98+
#ifdef DEBUG
99+
std::cout << "sym_exit: no args passed" << std::endl;
100+
#endif
101+
status = 0;
102+
}
103+
check_pc_to_file(state);
104+
epilogue();
105+
exit(status);
106+
}
107+
108+
/* TODO: Generate both versions of sym_exit <2022-01-24, David Deng> */
109+
inline std::monostate sym_exit(SS state, immer::flex_vector<PtrVal> args, Cont k) {
110+
auto v = args.at(0)->to_IntV();
111+
auto status = v ? v->i : 0;
96112
check_pc_to_file(state);
97113
epilogue();
98-
exit(0);
114+
exit(status);
99115
}
100116

101117
inline immer::flex_vector<std::pair<SS, PtrVal>> llsc_assert(SS state, immer::flex_vector<PtrVal> args) {

‎dev-clean/headers/llsc/filesys.hpp‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -124,6 +124,14 @@ class FS {
124124
Fd next_fd;
125125

126126
public:
127+
friend std::ostream& operator<<(std::ostream& os, const FS& fs) {
128+
os << "FS(size=" << fs.files.size() << ", files:" << std::endl;
129+
for (auto pf: fs.files) {
130+
os << pf.second << std::endl << std::endl;
131+
}
132+
os << ")";
133+
return os;
134+
}
127135
FS(): next_fd(3) {
128136
// default initialize opened_files and files
129137
/* TODO: set up stdin and stdout using fd 1 and 2 <2021-11-03, David Deng> */
@@ -186,4 +194,7 @@ class FS {
186194
* <2021-11-15, David Deng> */
187195
};
188196

197+
inline int default_sym_file_size = 5;
198+
inline FS initial_fs;
199+
189200
#endif

‎dev-clean/headers/llsc/state_pure.hpp‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -122,7 +122,7 @@ class SS {
122122
BlockLabel bb;
123123
FS fs;
124124
public:
125-
SS(Mem heap, Stack stack, PC pc, BlockLabel bb) : heap(heap), stack(stack), pc(pc), bb(bb) {}
125+
SS(Mem heap, Stack stack, PC pc, BlockLabel bb) : heap(heap), stack(stack), pc(pc), bb(bb), fs(initial_fs) {}
126126
SS(Mem heap, Stack stack, PC pc, BlockLabel bb, FS fs) : heap(heap), stack(stack), pc(pc), bb(bb), fs(fs) {}
127127
PtrVal env_lookup(Id id) { return stack.lookup_id(id); }
128128
size_t heap_size() { return heap.size(); }
@@ -181,8 +181,8 @@ class SS {
181181
PC get_PC() { return pc; }
182182
// TODO temp solution
183183
PtrVal getVarargLoc() { return stack.getVarargLoc(); }
184-
void set_fs(FS& new_fs) { fs = new_fs; }
185-
FS& get_fs() { return fs; }
184+
void set_fs(FS new_fs) { fs = new_fs; }
185+
FS get_fs() { return fs; }
186186
};
187187

188188
inline const Mem mt_mem = Mem(immer::flex_vector<PtrVal>{});

‎dev-clean/headers/llsc_imp.hpp‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,9 +38,10 @@ using namespace std::chrono;
3838

3939
#include <llsc/auxiliary.hpp>
4040
#include <llsc/parallel.hpp>
41-
#include <llsc/cli.hpp>
4241
#include <llsc/monitor.hpp>
4342
#include <llsc/value_ops.hpp>
43+
#include <llsc/filesys.hpp>
44+
#include <llsc/cli.hpp>
4445
#include <llsc/state_imp.hpp>
4546
#include <llsc/smt_checker.hpp>
4647
#include <llsc/smt_stp.hpp>

‎dev-clean/src/main/scala/sai/llsc/Codegen.scala‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ trait GenericLLSCCodeGen extends CppSAICodeGenBase {
4040
else if (m.toString.endsWith("$BlockLabel")) "BlockLabel"
4141
else if (m.toString.endsWith("$Mem")) "Mem"
4242
else if (m.toString.endsWith("$SS")) "SS"
43+
else if (m.toString.endsWith("$FS")) "FS"
4344
else if (m.toString.endsWith("$Kind")) "LocV::Kind"
4445
else if (m.toString.endsWith("SMTExpr")) "PtrVal"
4546
else if (m.toString.endsWith("SMTBool")) "PtrVal"
@@ -79,6 +80,8 @@ trait GenericLLSCCodeGen extends CppSAICodeGenBase {
7980
case Node(s, "ss-add-incoming-block", List(ss, bb), _) => es"$ss.add_incoming_block($bb)"
8081
case Node(s, "ss-incoming-block", List(ss), _) => es"$ss.incoming_block()"
8182
case Node(s, "ss-arg", List(ss, i), _) => es"$ss.init_arg($i)"
83+
case Node(s, "ss-get-fs", List(ss), _) => es"$ss.get_fs()"
84+
case Node(s, "ss-set-fs", List(ss, fs), _) => es"$ss.set_fs($fs)"
8285
case Node(s, "get-pc", List(ss), _) => es"$ss.get_PC()"
8386
case Node(s, "null-v", _, _) => es"nullptr"
8487

@@ -95,6 +98,8 @@ trait GenericLLSCCodeGen extends CppSAICodeGenBase {
9598
case Node(s, "print-block-cov", _, _) => es"cov.print_block_cov()"
9699
case Node(s, "print-time", _, _) => es"cov.print_time()"
97100
case Node(s, "print-path-cov", _, _) => es"cov.print_path_cov()"
101+
case Node(s, "get-string", List(ptr, ss), _) => es"get_string($ptr, $ss)"
102+
case Node(s, "fs-open-file", List(fs, p, f), _) => es"$fs.open_file($p, $f)"
98103

99104
case _ => super.shallow(n)
100105
}

‎dev-clean/src/main/scala/sai/llsc/External.scala‎

Lines changed: 44 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -49,14 +49,44 @@ trait GenExternal extends SymExeDefs {
4949
}
5050
}
5151

52+
def gen_open[T: Manifest](ss: Rep[SS], args: Rep[List[Value]], k: (Rep[SS], Rep[Value]) => Rep[T]): Rep[T] = {
53+
val ptr = args(0)
54+
val name: Rep[String] = getString(ptr, ss)
55+
val flags = args(1)
56+
// val mode = args(2) // how to handle optional argument?
57+
val fs: Rep[FS] = ss.getFs
58+
val ret: Rep[Fd] = fs.openFile(name, 0)
59+
ss.setFs(fs)
60+
k(ss, IntV(ret, 32))
61+
}
62+
63+
def gen_openat[T: Manifest](ss: Rep[SS], args: Rep[List[Value]], k: (Rep[SS], Rep[Value]) => Rep[T]): Rep[T] = {
64+
// TODO: implement this <2022-01-23, David Deng> //
65+
// int __fd_openat(int basefd, const char *pathname, int flags, mode_t mode);
66+
// if (fd == AT_FDCWD), call open
67+
k(ss, IntV(0, 32))
68+
}
69+
5270
def llsc_assert(ss: Rep[SS], args: Rep[List[Value]]): Rep[List[(SS, Value)]] =
5371
gen_llsc_assert[List[(SS, Value)]](ss, args, { case (s, v) => List[(SS, Value)]((s, v)) })
5472

5573
def llsc_assert_k(ss: Rep[SS], args: Rep[List[Value]], k: Rep[Cont]): Rep[Unit] =
5674
gen_llsc_assert[Unit](ss, args, { case (s, v) => k(s, v) })
75+
76+
def open(ss: Rep[SS], args: Rep[List[Value]]): Rep[List[(SS, Value)]] =
77+
gen_open[List[(SS, Value)]](ss, args, { case (s, v) => List[(SS, Value)]((s, v)) })
78+
79+
def open_k(ss: Rep[SS], args: Rep[List[Value]], k: Rep[Cont]): Rep[Unit] =
80+
gen_open[Unit](ss, args, { case (s, v) => k(s, v) })
81+
82+
def openat(ss: Rep[SS], args: Rep[List[Value]]): Rep[List[(SS, Value)]] =
83+
gen_openat[List[(SS, Value)]](ss, args, { case (s, v) => List[(SS, Value)]((s, v)) })
84+
85+
def openat_k(ss: Rep[SS], args: Rep[List[Value]], k: Rep[Cont]): Rep[Unit] =
86+
gen_openat[Unit](ss, args, { case (s, v) => k(s, v) })
5787
}
5888

59-
class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] with SAIOps with GenExternal { q =>
89+
class ExternalLLSCDriver(folder: String = "./headers/llsc") extends SAISnippet[Int, Unit] with SAIOps with GenExternal { q =>
6090
import java.io.{File, PrintStream}
6191
import scala.collection.mutable.HashMap
6292

@@ -71,8 +101,12 @@ class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] wit
71101
val ng = init(g)
72102
run(name, ng)
73103
emitln("/* LLSC - External utility functions and library modeling functions */")
104+
emitln("/* Generated by sai.llsc.TestGenerateExternal */")
105+
emitln("#ifndef LLSC_EXTERNAL_HEADERS_GEN")
106+
emitln("#define LLSC_EXTERNAL_HEADERS_GEN")
74107
emitFunctionDecls(stream)
75108
emitFunctions(stream)
109+
emitln("#endif // LLSC_EXTERNAL_HEADERS_GEN")
76110
}
77111
}
78112

@@ -85,7 +119,7 @@ class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] wit
85119
// TODO: refactor into SAIOps <2022-01-18, David Deng> //
86120

87121
def hardTopFun[A:Manifest,B:Manifest](f: Rep[A] => Rep[B], s: String): Rep[A => B] = {
88-
val unwrapped = __hardTopFun(f, 1, xn => Unwrap(f(Wrap[A](xn(0)))))
122+
val unwrapped = __hardTopFun(f, 1, xn => Unwrap(f(Wrap[A](xn(0)))), "inline")
89123
if (!s.trim.isEmpty) {
90124
val n = unwrapped.asInstanceOf[Backend.Sym].n
91125
funNameMap(n) = s
@@ -94,7 +128,7 @@ class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] wit
94128
}
95129

96130
def hardTopFun[A:Manifest,B:Manifest,C:Manifest](f: (Rep[A], Rep[B]) => Rep[C], s: String): Rep[(A, B) => C] = {
97-
val unwrapped = __hardTopFun(f, 2, xn => Unwrap(f(Wrap[A](xn(0)), Wrap[B](xn(1)))))
131+
val unwrapped = __hardTopFun(f, 2, xn => Unwrap(f(Wrap[A](xn(0)), Wrap[B](xn(1)))), "inline")
98132
if (!s.trim.isEmpty) {
99133
val n = unwrapped.asInstanceOf[Backend.Sym].n
100134
funNameMap(n) = s
@@ -103,7 +137,7 @@ class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] wit
103137
}
104138

105139
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] = {
106-
val unwrapped = __hardTopFun(f, 3, xn => Unwrap(f(Wrap[A](xn(0)), Wrap[B](xn(1)), Wrap[C](xn(2)))))
140+
val unwrapped = __hardTopFun(f, 3, xn => Unwrap(f(Wrap[A](xn(0)), Wrap[B](xn(1)), Wrap[C](xn(2)))), "inline")
107141
if (!s.trim.isEmpty) {
108142
val n = unwrapped.asInstanceOf[Backend.Sym].n
109143
funNameMap(n) = s
@@ -112,8 +146,12 @@ class ExternalLLSCDriver(folder: String = ".") extends SAISnippet[Int, Unit] wit
112146
}
113147

114148
def snippet(u: Rep[Int]) = {
115-
hardTopFun(llsc_assert(_,_), "llsc_assert")
116-
hardTopFun(llsc_assert_k(_,_,_), "llsc_assert_k")
149+
// TODO: generate function of same name with multiple signatures? <2022-01-23, David Deng> //
150+
// TODO: llsc_assert_k depends on sym_exit, which doesn't have a _k version right now <2022-01-23, David Deng> //
151+
// hardTopFun(llsc_assert(_,_), "llsc_assert")
152+
// hardTopFun(llsc_assert_k(_,_,_), "llsc_assert_k")
153+
hardTopFun(open(_,_), "open")
154+
// hardTopFun(open_k(_,_,_), "open_k")
117155
()
118156
}
119157
}

0 commit comments

Comments
 (0)